;-------------------------------------------------------------------- ; RSC-REPOSITORY SET/97 ;-------------------------------------------------------------------- ; Copyright@1996 by F. Luis Neves ; ; Author(s): FLN (F. Luis Neves) ; Revisions: 25.Fev.97 Rev: 13 May, 1997 (NonRec. models) ; Rev: 12 Jun, 1997 (Decomposition) ; Rev: 22 Jul, 1997 ; (A->B->C) => (A->1)*(B->C) ; Rev: 12 Dec, 1997 (Abs/Rep functions) ; Rev: 3 Jan, 1998 (Final revisions) ; ;-------------------------------------------------------------------- ; ; Comments: SEts Tool ; TYPE ; SETS model EKey = STR; EInf = Sets; MSets = EKey -> EInf; ; end of SETS model ; SETS sublanguage Cst :: A:STR; Var :: A:STR; List :: A:Sets; Prod :: A:Sets-list; Plus :: A:Sets-list; Pset :: A:Sets B:Sets; Ffun :: A:Sets B:Sets; Sets = Cst | Var | Pset | List | Ffun | Prod | Plus; ; end of SETS sublanguage ; SETS reificator Reif = RKey -> RInf; RInf = Pat:X Act:X Abs:STR Rep:STR; ; end of SETS reificator ENDTYPE ;-------------------------------------------------------------------- ; ; Auxiliary functions ; FUNC fprint(f:STR,m:STR,l:STR-list) RETURN progn(fp <- fopen(f,m), _fprint_(fp,l), fclose(fp)); _fprint_(f,l) = if (l == <>) then princ("") else let (h = head(l), t = tail(l)) in progn(if (is-STR(h) -> fputs(h,f), is-SYM(h) -> fputs(symstr(h),f), is-INT(h) -> fputs(itoa(h),f), is-BOOL(h) -> fputs(symstr(h),f)) otherwise (princ(h)), _fprint_(f,t)); ;-------------------------------------------------------------------- ; ; Subc'alculo de Isomorfismo em SETS ; FUNC RR0(x:X):X RETURN x; ; ; (2.22) A x B = B x A ; FUNC RR1(x:X):X RETURN if xMatch(x,O("*",<'A,'B>)) then O("*",) else x; ABS1(x) = "const(p2,p1)"; REP1(x) = "const(p2,p1)"; INV1(x) = ""; ; ; (2.23) A x (B x C) = (A x B) x C ; FUNC RR2(x:X):X RETURN if xMatch(x,O("*",<'A,O("*",<'B,'C>)>)) then O("*",),RX(RX(x))>) else x; ABS2(x) = "const(comp(p1,p1),const(comp(p2,p1),p2))"; REP2(x) = "const(const(p1,comp(p1,p2)),comp(p2,p2))"; INV2(x) = ""; FUNC RR3(x:X):X RETURN if xMatch(x,O("*",),'C>)) then O("*",)>) else x; ABS3(x) = "const(const(p1,comp(p1,p2)),comp(p2,p2))"; REP3(x) = "const(comp(p1,p1),const(comp(p2,p1),p2))"; INV3(x) = ""; ; ; (2.24) A x 1 = A ; FUNC RR4(x:X):X RETURN if xMatch(x,O("*",<'A,O("1",<>)>)) then LX(x) else x; ABS4(x) = "nilit"; REP4(x) = "p1"; INV4(x) = ""; FUNC RR5(x:X):X RETURN if is-V(x) then O("*",)>) else x; ABS5(x) = "p1"; REP5(x) = "nilit"; INV5(x) = ""; ; ; (2.25) A + B = B + A ; FUNC RR6(x:X):X RETURN if xMatch(x,O("+",<'A,'B>)) then O("+",) else x; ABS6(x) = ""; REP6(x) = ""; INV6(x) = ""; ; ; (2.26) A + (B + C) = (A + B) + C ; FUNC RR7(x:X):X RETURN if xMatch(x,O("+",<'A,O("+",<'B,'C>)>)) then O("+",),RX(RX(x))>) else x; FUNC RR8(x:X):X RETURN if xMatch(x,O("+",),'C>)) then O("+",)>) else x; ; ; (2.27) A + 0 = A ; FUNC RR9(x:X):X RETURN if xMatch(x,O("+",<'A,O("0",<>)>)) then LX(x) else x; FUNC RR10(x:X):X RETURN if is-V(x) then O("+",)>) else x; ; ; (2.28) A x 0 = 0 ; FUNC RR11(x:X):X RETURN if xMatch(x,O("*",<'A,O("0",<>)>)) then O("0",<>) else x; ; ; (2.29) A x (B + C) = (A x B) + (A x C) ; FUNC RR12(x:X):X RETURN if xMatch(x,O("*",<'A,O("+",<'B,'C>)>)) then O("+",),O("*",)>) else x; FUNC RR13(x:X):X RETURN if xMatch(x,O("+",),O("*",<'A,'C>)>)) && LX(LX(x)) == LX(RX(x)) then O("*",)>) else x; ; ; (2.33) A ^ 0 = 1 ; FUNC RR14(x:X):X RETURN if xMatch(x,O("^",<'A,O("0",<>)>)) then O("1",<>) else x; ; ; (2.34) A ^ (B + C) = (A ^ B) + (A ^ C) ; FUNC RR15(x:X):X RETURN if xMatch(x,O("^",<'A,O("+",<'B,'C>)>)) then O("+",),O("^",)>) else x; FUNC RR16(x:X):X RETURN if xMatch(x,O("+",),O("^",<'A,'C>)>)) && LX(LX(x)) == LX(RX(x)) then O("^",)>) else x; ; ; (2.35) A ^ 1 = A ; FUNC RR17(x:X):X RETURN if xMatch(x,O("^",<'A,O("1",<>)>)) then LX(x) else x; FUNC RR18(x:X):X RETURN if is-V(x) then O("^",)>) else x; ; ; (2.36) 1 ^ A = 1 ; FUNC RR19(x:X):X RETURN if xMatch(x,O("^",),'A>)) then O("1",<>) else x; ; ; (2.37) (B x C) ^ A = (B ^ A) x (C ^ A) ; FUNC RR20(x:X):X RETURN if xMatch(x,O("^",),'A>)) then O("*",),O("^",)>) else x; FUNC RR21(x:X):X RETURN if xMatch(x,O("*",),O("^",<'C,'A>)>)) && RX(LX(x)) == RX(RX(x)) then O("^",),RX(LX(x))>) else x; ; ; (2.38) C ^ (A x B) = (C ^ B) ^ A ; FUNC RR22(x:X):X RETURN if xMatch(x,O("^",<'C,O("*",<'A,'B>)>)) then O("^",),LX(RX(x))>) else x; ABS22(x) = "uncurry"; REP22(x) = "curry"; INV22(x) = ""; FUNC RR23(x:X):X RETURN if xMatch(x,O("^",),'A>)) then O("^",)>) else x; ABS23(x) = "curry"; REP23(x) = "uncurry"; INV23(x) = ""; ; ; (2.39) A -> B = (B + 1) ^ A ; FUNC RR24(x:X):X RETURN if xMatch(x,O("->",<'A,'B>)) then O("^",)>),LX(x)>) else x; FUNC RR25(x:X):X RETURN if xMatch(x,O("^",)>),'A>)) then O("->",) else x; ; ; (2.40) A-list = A ^ n (n >= 0) ; ;FUNC RR40(x:X):X ;RETURN if xMatch(x,O("->",'N,'A)) ; then ... ; ; (2.63) (B + C) -> A = (B -> A) x (C -> A) ; FUNC RR26(x:X):X RETURN if xMatch(x,O("->",),'A>)) then O("*",",),O("->",)>) else x; FUNC RR27(x:X):X RETURN if xMatch(x,O("*",",<'B,'A>),O("->",<'C,'A>)>)) && RX(LX(x)) == RX(RX(x)) then O("->",),RX(LX(x))>) else x; ; ; (2.64) 0 -> A = 1 ; FUNC RR28(x:X):X RETURN if xMatch(x,O("->",),'A>)) then O("1",<>) else x; ABS28(x) = "[]"; REP28(x) = "nil"; INV28(x) = ""; ; ; (2.64) A -> 1 = 2 ^ A ; FUNC RR29(x:X):X RETURN if xMatch(x,O("->",<'A,O("1",<>)>)) then O("^",),LX(x)>) else x; ABS29(x) = "ffAset"; REP29(x) = "dom"; INV29(x) = ""; FUNC RR30(x:X):X RETURN if xMatch(x,O("^",),'A>)) then O("->",)>) else x; ABS30(x) = "dom"; REP30(x) = "ffAset"; INV30(x) = ""; ; ; (2.64-2.65) 1 -> A = A + 1 ; FUNC RR31(x:X):X RETURN if xMatch(x,O("->",),'A>)) then O("+",)>) else x; FUNC RR32(x:X):X RETURN if xMatch(x,O("+",<'A,O("1",<>)>)) then O("->",),LX(x)>) else x; ; ; (2.65) A -> (B x C) => (A -> B) x (A -> C) ; FUNC RR33(x:X):X RETURN if xMatch(x,O("->",<'A,O("*",<'B,'C>)>)) then O("*",",),O("->",)>) else x; ABS33(x) = "join"; REP33(x) = "nJoinInv"; INV33(x) = ""; ;"dom(" ++ xString(LX(x)) ++ ") = dom(" ++ xString(RX(x)) ++ ")"; ; ; (2.70) (A x B) -> C => A -> (B -> C) ; Inv(x) = () notin rng(x) ; FUNC RR34(x:X):X RETURN if xMatch(x,O("->",),'C>)) then O("->",",)>) else x; ABS34(x) = "?"; REP34(x) = "?"; INV34(x) = ""; ;xString(RX(x)) ++ " != []"; ; ; (2.71) A -> (B -> C) => 2 ^ A x ((A x B) -> C) ; FUNC RR35(x:X):X RETURN if xMatch(x,O("->",<'A,O("->",<'B,'C>)>)) then O("*",),LX(x)>),O("->",),RX(RX(x))>)>) else x; ABS35(x) = "..."; REP35(x) = "..."; INV35(x) = ""; ; ; (2.72) A -> D x (B -> C) => (A -> D) x ((A x B) -> C) ; FUNC RR36(x:X):X RETURN if xMatch(x,O("->",<'A,O("*",<'D,O("->",<'B,'C>)>)>)) then O("*",",),O("->",),RX(RX(RX(x)))>)>) else x; ABS36(x) = "nJoin"; REP36(x) = "nJoinInv"; INV36(x) = ""; ;"proj1(dom("++xString(RX(x))++")) in dom("++xString(LX(x))++")"; ; ; (2.75) A -> (B + C) => (A -> B) x (A -> C) ; FUNC RR37(x:X):X RETURN if xMatch(x,O("->",<'A,O("+",<'B,'C>)>)) then O("*",",),O("->",)>) else x; ABS37(x) = "djd"; REP37(x) = ""; INV37(x) = ""; ;"dom(" ++ xString(LX(x)) ++ ") * dom(" ++ xString(RX(x)) ++ ") = {}"; ; ; (2.9) A -> B => 2 ^ (A x B) ; FUNC RR38(x:X):X RETURN if xMatch(x,O("->",<'A,'B>)) then O("^",),O("*",)>) else x; ABS38(x) = "mkf"; REP38(x) = "mkr"; INV38(x) = ""; ;"forall (a,b), (a',b') in " ++ xString(x) ++ ": (a = a' => b = b')"; FUNC RR39(x:X):X RETURN if xMatch(x,O("->",<'A,O("->",<'B,'C>)>)) then O("*",",)>),O("->",),RX(RX(x))>)>) else x; ;-------------------------------------------------------------------- ; ; SETS Rewrite System functionality ; rrInfo <- []; rrReif <- [ 1 -> O("*",<'A,'B>), 2 -> O("*",<'A,O("*",<'B,'C>)>), 3 -> O("*",),'C>), 4 -> O("*",<'A,O("1",<>)>), 5 -> 'A, 6 -> O("+",<'A,'B>), 7 -> O("+",<'A,O("+",<'B,'C>)>), 8 -> O("+",),'C>), 9 -> O("+",<'A,O("0",<>)>), 10 -> 'A, 11 -> O("*",<'A,O("0",<>)>), 12 -> O("*",<'A,O("+",<'B,'C>)>), 13 -> O("+",),O("*",<'A,'C>)>), 14 -> O("^",<'A,O("0",<>)>), 15 -> O("^",<'A,O("+",<'B,'C>)>), 16 -> O("+",),O("^",<'A,'C>)>), 17 -> O("^",<'A,O("1",<>)>), 18 -> 'A, 19 -> O("^",),'A>), 20 -> O("^",),'A>), 21 -> O("*",),O("^",<'C,'A>)>), 22 -> O("^",<'C,O("*",<'A,'B>)>), 23 -> O("^",),'A>), 24 -> O("->",<'A,'B>), 25 -> O("^",)>),'A>), 26 -> O("->",),'A>), 27 -> O("*",",<'B,'A>),O("->",<'C,'A>)>), 28 -> O("->",),'A>), 29 -> O("->",<'A,O("1",<>)>), 30 -> O("^",),'A>), 31 -> O("->",),'A>), 32 -> O("+",<'A,O("1",<>)>), ; Inequacional 33 -> O("->",<'A,O("*",<'B,'C>)>), 34 -> O("->",),'C>), 35 -> O("->",<'A,O("->",<'B,'C>)>), 36 -> O("->",<'A,O("*",<'D,O("->",<'B,'C>)>)>), 37 -> O("->",<'A,O("+",<'B,'C>)>), 38 -> O("->",<'A,'B>), 39 -> O("->",<'A,O("->",<'B,'C>)>) ]; FUNC rrINIT():Reif STATE rrInfo <- [ 1 -> RInf(rrReif[1],RR1(rrReif[1]),"const(p2,p1)","const(p2,p1)"), 2 -> RInf(rrReif[2],RR2(rrReif[2]),"?","?"), 3 -> RInf(rrReif[3],RR3(rrReif[3]),"?","?"), 4 -> RInf(rrReif[4],RR4(rrReif[4]),"?","?"), 5 -> RInf(rrReif[5],RR5(rrReif[5]),"?","?"), 6 -> RInf(rrReif[6],RR6(rrReif[6]),"?","?"), 7 -> RInf(rrReif[7],RR7(rrReif[7]),"?","?"), 8 -> RInf(rrReif[8],RR8(rrReif[8]),"?","?"), 9 -> RInf(rrReif[9],RR9(rrReif[9]),"?","?"), 10 -> RInf(rrReif[10],RR10(rrReif[10]),"?","?"), 11 -> RInf(rrReif[11],RR11(rrReif[11]),"?","?"), 12 -> RInf(rrReif[12],RR12(rrReif[12]),"?","?"), 13 -> RInf(rrReif[13],RR13(rrReif[13]),"?","?"), 14 -> RInf(rrReif[14],RR14(rrReif[14]),"?","?"), 15 -> RInf(rrReif[15],RR15(rrReif[15]),"?","?"), 16 -> RInf(rrReif[16],RR16(rrReif[16]),"?","?"), 17 -> RInf(rrReif[17],RR17(rrReif[17]),"?","?"), 18 -> RInf(rrReif[18],RR18(rrReif[18]),"?","?"), 19 -> RInf(rrReif[19],RR19(rrReif[19]),"?","?"), 20 -> RInf(rrReif[20],RR20(rrReif[20]),"?","?"), 21 -> RInf(rrReif[21],RR21(rrReif[21]),"?","?"), 22 -> RInf(rrReif[22],RR22(rrReif[22]),"uncurry","curry"), 23 -> RInf(rrReif[23],RR23(rrReif[23]),"curry","uncurry"), 24 -> RInf(rrReif[24],RR24(rrReif[24]),"?","?"), 25 -> RInf(rrReif[25],RR25(rrReif[25]),"?","?"), 26 -> RInf(rrReif[26],RR26(rrReif[26]),"?","?"), 27 -> RInf(rrReif[27],RR27(rrReif[27]),"?","?"), 28 -> RInf(rrReif[28],RR28(rrReif[28]),"?","?"), 29 -> RInf(rrReif[29],RR29(rrReif[29]),"ffAset","dom"), 30 -> RInf(rrReif[30],RR30(rrReif[30]),"dom","ffAset"), 31 -> RInf(rrReif[31],RR31(rrReif[31]),"?","?"), 32 -> RInf(rrReif[32],RR32(rrReif[32]),"?","?"), ; Inequacional 33 -> RInf(rrReif[33],RR33(rrReif[33]),"join","nJoinInv"), 34 -> RInf(rrReif[34],RR34(rrReif[34]),"pcurry","puncurry"), 35 -> RInf(rrReif[35],RR35(rrReif[35]),"nJoin","nJoinInv"), 36 -> RInf(rrReif[36],RR36(rrReif[36]),"nJoin","nJoinInv"), 37 -> RInf(rrReif[37],RR37(rrReif[37]),"coJoin","coJoinInv"), 38 -> RInf(rrReif[38],RR38(rrReif[38]),"mkf","mkr"), 39 -> RInf(rrReif[39],RR39(rrReif[39]),"nJoin","nJoinInv")]; FUNC rrSHOW(i:INT) PRE i in dom(rrReif) RETURN let (e = rrReif[i]) in xString(e) ^ <"=>"> ^ xString(RootMatch(e,i)); FUNC ReifStep(a:STR,r:STR,i:STR) RETURN princ("\nabs = ",a,"\nrep = ",r,"\ninv = ",i); FUNC rrGetPat(i:INT):X PRE rrInfo != [] && i > 0 && i < 40 RETURN Pat(rrInfo[i]); FUNC rrGetAct(i:INT):X PRE rrInfo != [] && i > 0 && i < 40 RETURN Act(rrInfo[i]); FUNC rrGetAbs(i:INT) PRE rrInfo != [] && i > 0 && i < 40 RETURN Abs(rrInfo[i]); FUNC rrGetRep(i:INT) PRE rrInfo != [] && i > 0 && i < 40 RETURN Rep(rrInfo[i]); FUNC rrSAVE() RETURN do(rrINIT(), fp<-fopen("_","w"), fprint("_","a",<"\\documentstyle{article}\n">), fprint("_","a",<"\\begin{document}\n">), fprint("_","a",<"\\begin{eqnarray}\n">), ; foreach(i,inseg(32),fprint("_","a",SETS2TEX(xSets(rrGetPat(i)))), foreach(i,inseg(32),fprint("_","a",xTeX(rrGetPat(i))), fprint("_","a",<"& \\cong_{",i,"} &">), ; fprint("_","a",SETS2TEX(xSets(rrGetAct(i)))), fprint("_","a",xTeX(rrGetAct(i))), fprint("_","a",<"\\\\\n">)), foreach(i,<33,34,35,36,37,38,39>,fprint("_","a",SETS2TEX(xSets(rrGetPat(i)))), fprint("_","a",<"& \\unlhd_{",i,"} &">), fprint("_","a",SETS2TEX(xSets(rrGetAct(i)))), fprint("_","a",<"\\\\">)), fprint("_","a",<"\n\\end{eqnarray}">), fprint("_","a",<"\\end{document}\n">), sh("mv _ _rules_.tex")); ; ; SETS Functionality ; FUNC CAM2SETS(f:STR):MSets RETURN do(sh("seca " ++ f ++ " > _1_"), sh("./cam2set < _1_ > _2_"), nload("_2_"), sh("rm -f _1_ _2_")); FUNC XMT2SETS(f:STR):MSets RETURN do(sh("seca " ++ f ++ " > _1_"), sh("./cam2set < _1_ > _2_"), sh("seca _2_ > _3_"), load("_3_"), sh("rm -f _1_ _2_ _3_")); ; ; Flat Sets Model ; FUNC FLATSETS(k:EKey,s:MSets):Sets PRE k in dom(s) RETURN [ k -> _FlatSets_(k,s[k],s) ]; _FlatSets_(k,e,s) = let (f = _SetsSubst_(k,e,s)) in if (e == f) then e else _FlatSets_(k,f,s); _SetsSubst_(k,e,s) = if is-Cst(e) then e else if is-Var(e) then let (v = A(e)) in if v in dom(s) && v != k then if is-Cst(s[v]) then e else s[v] else e ; in if v in dom(s) then s[v] else e else if is-Pset(e) then Pset(_SetsSubst_(k,A(e),s),_SetsSubst_(k,B(e),s)) else if is-List(e) then List(_SetsSubst_(k,A(e),s)) else if is-Ffun(e) then Ffun(_SetsSubst_(k,A(e),s),_SetsSubst_(k,B(e),s)) else if is-Prod(e) then Prod(< _SetsSubst_(k,x,s) | x <- A(e) >) else if is-Plus(e) then Plus(< _SetsSubst_(k,x,s) | x <- A(e) >); ; ; Sets Decomposition ; FUNC SETSDEC(e:Sets):INT->Sets | Sets RETURN if is-Prod(e) then if 'true in { is-Cst(x) && is-Var(x) | x <- A(e) } then e else [ i -> nth(i,A(e)) | i <- inseg(length(A(e))) ] else e; ; ; X-Expression to Sets format ; FUNC xSets(x:X):Sets RETURN if isC(x) then Cst(OX(x)) else if is-V(x) then Var(symstr(x)) else let (o = OX(x), l = LX(x), r = RX(x)) in if (o == "*" -> if xProdOrio(x) then Prod(xFlatOrio(x)) else Prod(), o == "+" -> if xPlusOrio(x) then Plus(xFlatOrio(x)) else Plus(), o == "^" -> Pset(xSets(l),xSets(r)), o == "->" -> if (l == 'N) then List(xSets(r)) else Ffun(xSets(l),xSets(r))); FUNC xProdOrio(x:X):BOOL RETURN if is-O(x) then let (o = OX(x), l = LX(x), r = RX(x)) in if (o == "*" && is-V(l) || isC(l) || xProdOrio(l) && is-V(r) || isC(r) || xProdOrio(r)) then true else false else false; FUNC xPlusOrio(x:X):BOOL RETURN if is-O(x) then let (o = OX(x), l = LX(x), r = RX(x)) in if (o == "+" && is-V(l) || isC(l) || xPlusOrio(l) && is-V(r) || isC(r) || xPlusOrio(r)) then true else false else false; FUNC xFlatOrio(x:X):X RETURN if isC(x) then < Cst(OX(x)) > else if is-V(x) then < Var(symstr(x)) > else let (o = OX(x), l = LX(x), r = RX(x)) in xFlatOrio(l) ^ xFlatOrio(r); ; ; Abstraction function string ; FUNC xAbs2Str(x:X):STR-list RETURN if isC(x) || is-V(x) || is-F(x) then else let (o = OX(x), l = LX(x), r = RX(x)) in if (l == "id" && r == "id") then <"id"> else if (o == "->") then if (r == "id" -> <"("> ^ xAbs2Str(l) ^ <"->*)">, l == "id" -> <"(*->"> ^ xAbs2Str(r) ^ <")">) otherwise (xAbs2Str(l) ^ <"->"> ^ xAbs2Str(r)) else if (o == "*") then if (r == "id" -> <"prod("> ^ xAbs2Str(l) ^ <",id)">, l == "id" -> <"prod(id,"> ^ xAbs2Str(r) ^ <")">) otherwise (xAbs2Str(l) ^ <"*"> ^ xAbs2Str(r)) else if (o == "+") then if (r == "id" -> <"const("> ^ xAbs2Str(l) ^ <",id)">, l == "id" -> <"const(id,"> ^ xAbs2Str(r) ^ <")">) otherwise (xAbs2Str(l) ^ <"*"> ^ xAbs2Str(r)) else xAbs2Str(l) ^ ^ xAbs2Str(r); ; ; Abstraction function TeX string ; FUNC xAbs2TeX(x:X):STR-list RETURN if isC(x) || is-V(x) || is-F(x) then else let (o = OX(x), l = LX(x), r = RX(x)) in if (l == "id" && r == "id") then <"id"> else if (o == "->") then if (r == "id" -> <"("> ^ xAbs2TeX(l) ^ <" \\hookrightarrow\\star)">, l == "id" -> <"(\\star\\hookrightarrow "> ^ xAbs2TeX(r) ^ <")">) otherwise (xAbs2TeX(l) ^ <" \\hookrightarrow "> ^ xAbs2TeX(r)) else if (o == "*") then if (r == "id" -> <"prod("> ^ xAbs2TeX(l) ^ <",id)">, l == "id" -> <"prod(id,"> ^ xAbs2TeX(r) ^ <")">) otherwise (xAbs2TeX(l) ^ <" \\times "> ^ xAbs2TeX(r)) else if (o == "+") then if (r == "id" -> <"const("> ^ xAbs2TeX(l) ^ <",id)">, l == "id" -> <"const(id,"> ^ xAbs2TeX(r) ^ <")">) otherwise (xAbs2TeX(l) ^ <" + "> ^ xAbs2TeX(r)) else xAbs2TeX(l) ^ ^ xAbs2TeX(r); ; ; Expression abstraction function ; FUNC xAbsFun(x:X):X RETURN if (isC(x) -> "id", is-V(x) -> "id", is-F(x) -> x) otherwise(let (o = OX(x), l = LX(x), r = RX(x)) in if (l == "id" && r == "id" -> "id", xAbsFun(l) == "id" && xAbsFun(r) == "id" -> "id", l == "id" || xAbsFun(l) == "id" -> O(o,<"id",xAbsFun(r)>), r == "id" || xAbsFun(r) == "id" -> O(o,)) otherwise (O(o,))); ; ; Expression representation function ; FUNC xRepFun(x:X):X RETURN if (isC(x) -> "id", is-V(x) -> "id", is-F(x) -> x) otherwise (let (o = OX(x), l = LX(x), r = RX(x)) in O(o,)); ; ; If xFirstMatch replaces the expression match with abstraction function ; x2 is the template ; FUNC xAbsMatch(a:STR,x1,x2:X):X RETURN if xMatch(x1,x2) then a else if (is-O(x1) && not(isC(x1))) then if (xAbsMatch(a,LX(x1),x2) == a -> O(OX(x1),), xAbsMatch(a,RX(x1),x2) == a -> O(OX(x1),)) otherwise (O(OX(x1),)) else x1; ; ; If xFirstMatch replaces the expression match with representation function ; x2 is the template ; FUNC xRepMatch(r:STR,x1,x2:X):X RETURN if xMatch(x1,x2) then r else if (is-O(x1) && not(isC(x1))) then if (xRepMatch(r,LX(x1),x2) == r -> O(OX(x1),), xRepMatch(r,RX(x1),x2) == r -> O(OX(x1),)) otherwise (O(OX(x1),)) else x1; ; ; Sets to X-Expression format ; FUNC SETS2BSETS(e:Sets):X ;RETURN if is-Cst(e) then strsym(A(e)) RETURN if is-Cst(e) then O(A(e),<>) else if is-Var(e) then strsym(A(e)) else if is-Pset(e) then O("^",) else if is-List(e) then O("->",<'N,SETS2BSETS(A(e))>) ;List(SetsSubst(A(e),s)) else if is-Ffun(e) then O("->",) else if is-Prod(e) then ProdBinary(A(e)) ;(< SetsSubst(x,s) | x <- A(e) >) else if is-Plus(e) then PlusBinary(A(e)) ;Plus(< SetsSubst(x,s) | x <- A(e) >) else e; ProdBinary(l) = if l == <> then 'error else let (h = head(l), t = tail(l)) in if length(l) == 1 then SETS2BSETS(h) else if length(l) == 2 then O("*",) else O("*",); PlusBinary(l) = if l == <> then 'error else let (h = head(l), t = tail(l)) in if length(l) == 1 then SETS2BSETS(h) else if length(l) == 2 then O("+",) else O("+",); ; ; Sets to Camila ; FUNC SETS2CAM(e:Sets):STR RETURN if is-Cst(e) then < A(e) > else if is-Var(e) then < A(e) > else if is-Pset(e) then if (A(e) == 2) then <";\n"> ^ _Sets2CAM_(A(e)) ^ <"-set"> else <"("> ^ _Sets2CAM_(A(e)) ^ <"^"> ^ SETS2CAM(B(e)) ^ <")"> else if is-List(e) then <";\n"> ^ _Sets2CAM_(A(e)) ^ <"-list"> else if is-Ffun(e) then <"("> ^ _Sets2CAM_(A(e)) ^ <"->"> ^ SETS2CAM(B(e)) ^ <")"> else if is-Prod(e) then <";\n"> ^ _Prod2CAM_(A(e),1) else if is-Plus(e) then <";\n"> ^ _Plus2CAM_(A(e)); _Sets2CAM_(e) = if is-Cst(e) then < A(e) > else if is-Var(e) then < A(e) > ; else <"("> ^ SETS2CAM(e) ^ <")">; else SETS2CAM(e); _Prod2CAM_(l,i) = if (l == <>) then <> else let (h = head(l), t = tail(l)) in if length(l) == 1 then <"P"++itoa(i) ++ ":"> ^ SETS2CAM(h) else <"P"++itoa(i) ++ ":"> ^ SETS2CAM(h) ^ ; <"P"++itoa(i.+1) ++ ":"> ^ _Prod2CAM_(t,i.+1); _Plus2CAM_(l) = if (l == <>) then <> else let (h = head(l), t = tail(l)) in if length(l) == 1 then SETS2CAM(h) else SETS2CAM(h) ^ <"|"> ^ _Plus2CAM_(t); ; ; Sets to TeX ; FUNC SETS2TEX(e:Sets):STR RETURN if is-Cst(e) then < A(e) > else if is-Var(e) then < A(e) > else if is-Pset(e) then if (is-Cst(A(e)) && A(A(e)) == "2") then <"2^{"> ^ _Sets2TEX_(B(e)) ^ <"}"> else <"{"> ^ _Sets2TEX_(A(e)) ^ <"}^{"> ^ SETS2TEX(B(e)) ^ <"}"> else if is-List(e) then <"("> ^ _Sets2TEX_(A(e)) ^ <")\^{\\star}"> else if is-Ffun(e) then <"("> ^ _Sets2TEX_(A(e)) ^ <" \\hookrightarrow "> ^ SETS2TEX(B(e)) ^ <")"> else if is-Prod(e) then _Prod2TEX_(A(e)) else if is-Plus(e) then _Plus2TEX_(A(e)); _Sets2TEX_(e) = if is-Cst(e) then < A(e) > else if is-Var(e) then < A(e) > ; else <"("> ^ SETS2TEX(e) ^ <")">; else SETS2TEX(e); _Prod2TEX_(l) = if (l == <>) then <> else let (h = head(l), t = tail(l)) in if (length(l) == 1 -> SETS2TEX(h), length(l) == 2 -> <"("> ^ SETS2TEX(h) ^ <" \\times "> ^ _Prod2TEX_(t) ^ <")">) otherwise (SETS2TEX(h) ^ <" \\times "> ^ _Prod2TEX_(t)); _Plus2TEX_(l) = if (l == <>) then <> else let (h = head(l), t = tail(l)) in if (length(l) == 1 -> SETS2TEX(h), length(l) == 2 -> <"("> ^ SETS2TEX(h) ^ <" \\times "> ^ _Plus2TEX_(t) ^ <")">) otherwise (SETS2TEX(h) ^ <" + "> ^ _Plus2TEX_(t)); ; ; Sets to String ; FUNC SETS2STR(e:Sets):STR RETURN if is-Cst(e) then < A(e) > else if is-Var(e) then < A(e) > else if is-Pset(e) then if A(e) == 2 then <"("> ^ _Sets2STR_(A(e)) ^ <")-set"> else <"("> ^ _Sets2STR_(A(e)) ^ <"->"> ^ SETS2STR(B(e)) ^ <")"> else if is-List(e) then <"("> ^ _Sets2STR_(A(e)) ^ <")-list"> else if is-Ffun(e) then <"("> ^ _Sets2STR_(A(e)) ^ <"->"> ^ SETS2STR(B(e)) ^ <")"> else if is-Prod(e) then _Prod2STR_(A(e)) else if is-Plus(e) then _Plus2STR_(A(e)); _Sets2STR_(e) = if is-Cst(e) then < A(e) > else if is-Var(e) then < A(e) > ; else <"("> ^ SETS2STR(e) ^ <")">; else SETS2STR(e); _Prod2STR_(l) = if (l == <>) then <> else let (h = head(l), t = tail(l)) in if length(l) == 1 then SETS2STR(h) else SETS2STR(h) ^ <" * "> ^ _Prod2STR_(t); _Plus2STR_(l) = if (l == <>) then <> else let (h = head(l), t = tail(l)) in if length(l) == 1 then SETS2STR(h) else SETS2STR(h) ^ <" + "> ^ _Plus2STR_(t); ; ; Sets to File ; FUNC SETS2FILE(e:Sets,f:STR) RETURN fprint(f,"w",SETS2STR(e)); ; ; Non Recursive Sets Model ; FUNC SETSNREC(k:EKey,m:MSets):MSets PRE k in dom(m) && SETSRENT(k,m) -> "Non recursive model?" RETURN m + [ k -> Prod(< Var("K"), Ffun(Var("K"),_SetsNRec_(m[k],[ k -> Var("K") ])) >) ]; _SetsNRec_(e,s) = if is-Cst(e) then e else if is-Var(e) then let (v = A(e)) in if v in dom(s) then if is-Cst(s[v]) then e else s[v] else e ; in if v in dom(s) then s[v] else e else if is-Pset(e) then Pset(_SetsNRec_(A(e),s),_SetsNRec_(B(e),s)) else if is-List(e) then List(_SetsNRec_(A(e),s)) else if is-Ffun(e) then Ffun(_SetsNRec_(A(e),s),_SetsNRec_(B(e),s)) else if is-Prod(e) then Prod(< _SetsNRec_(x,s) | x <- A(e) >) else if is-Plus(e) then Plus(< _SetsNRec_(x,s) | x <- A(e) >); ;RETURN let (x = { m[x] | x <- SETSRENT(m,s) } U SETSRENT(m,s), y = m / x) ;in m + _SetsNRec_(y); ;_SetsNRec_(m) = let (d = [ x -> _SetsRDep_(m[x],m) | x <- dom(m) ]) ;in _UnRecLaw1_(d,m); ; ; 1st UnRecursive Law ; _UnRecLaw1_(d,s) = if d == [] then [] else let (x = choice(dom(d)), y = d[x]) in if x notin y then [ x -> s[x] ] + _UnRecLaw1_(d\{x},s) else let (f = _FlatSets_(s[x],s\{x})) in [ x -> Prod(< Var("K"), Ffun(Var("K"),_SetsSubst_(f,[x -> Var("K")])) >) ] + _UnRecLaw1_(d\{x},s); ; ; Sets Entities Dependencies ; FUNC SETSEDEP(k:EKey,m:MSets):EKey -> EKey-set RETURN [ k -> _SetsRDep_(k,m[k],m) ]; ; ; Sets Recursive Entities ; FUNC SETSRENT(k:EKey,m:MSets):BOOL PRE k in dom(m) ;RETURN { x | x <- s : x in _SetsRDep_(k,m[k],m) }; RETURN k in _SetsRDep_(k,m[k],m); ; ; Sets Recursive Dependencies ; _SetsRDep_(k,e,m) = if is-Cst(e) then {} else if is-Var(e) then let (v = A(e)) in if v in dom(m) && v != k then { v } U _SetsRDep_(k,m[v],m\{v}) else { v } else if is-Pset(e) then _SetsRDep_(k,A(e),m) U _SetsRDep_(k,B(e),m) else if is-List(e) then _SetsRDep_(k,A(e),m) else if is-Ffun(e) then _SetsRDep_(k,A(e),m) U _SetsRDep_(k,B(e),m) else if is-Prod(e) then UNION({ _SetsRDep_(k,x,m) | x <- A(e) }) else if is-Plus(e) then UNION({ _SetsRDep_(k,x,m) | x <- A(e) }); ;-------------------------------------------------------------------- ; ; Model-Oriented Match Functionality ; ;-------------------------------------------------------------------- ; ; Degree of match ; FUNC rscDegreeMatch(x:X):INT RETURN if (erMatch(x) || ffMatch(x)) then 100 else let (t = xComplex(x) .- xOpr(x), m = xMetaSym(x)) in pdiv(m,t); ;-------------------------------------------------------------------- ; ER model (Entity-Relationship) ; FUNC erMatch(x:X):BOOL RETURN let (pattern = O("^",),'X>)) in xMatch(x,pattern) && ; not(xFirstMatch(RX(x),pattern)) && (is-V(RX(x)) || isC(x) || xProdOrio(RX(x))); ; ; If erFirstMatch replaces the expression match with '_er_ ; FUNC erMetaMatch(x1:X):X RETURN if erMatch(x1) then '_er_ else if is-O(x1) && OX(x1) == "*" then if (LX(x1) == '_er_ -> O(OX(x1),<'_er_,erMetaMatch(RX(x1))>), RX(x1) == '_er_-> O(OX(x1),)) otherwise (O(OX(x1),)) else x1; ; ; Applies erMetaMatch until no more applications are possible ; FUNC erApplyMetaMatch(x:X):X RETURN let (y = erMetaMatch(x)) in if x == y then x else erApplyMetaMatch(y); ; ; Applies A->B => 2^(A*B) until no more applications are possible ; FUNC erApplyFinalRule(x:X):X RETURN let (y = FirstMatch(x,38)) in if x == y then x else erApplyFinalRule(y); ; ; Degree of match ; FUNC erDegreeMatch(x:X):INT RETURN if erMatch(x) then 100 else let (t = xComplex(x) .- xOpr(x), m = xMetaSym(x)) in pdiv(m,t); ;-------------------------------------------------------------------- ; FF model (Finite Function) ; FUNC ffMatch(x:X):BOOL RETURN let (pattern = O("->",<'X,'Y>)) in xMatch(x,pattern) && ; not(xFirstMatch(RX(x),pattern)) && (is-V(RX(x)) || isC(RX(x)) || xProdOrio(RX(x))) && (is-V(LX(x)) || isC(LX(x)) || xProdOrio(LX(x))); ; ; If ffFirstMatch replaces the expression match with '_ff_ ; FUNC ffMetaMatch(x1:X):X RETURN if ffMatch(x1) then '_ff_ else if is-O(x1) && OX(x1) == "*" then if (LX(x1) == '_ff_ -> O(OX(x1),<'_ff_,ffMetaMatch(RX(x1))>), RX(x1) == '_ff_ -> O(OX(x1),)) otherwise (O(OX(x1),)) else x1; ; ; Applies ffMetaMatch until no more applications are possible ; FUNC ffApplyMetaMatch(x:X):X RETURN let (y = ffMetaMatch(x)) in if x == y then x else ffApplyMetaMatch(y); ; ; Degree of match ; FUNC ffDegreeMatch(x:X):INT RETURN if ffMatch(x) then 100 else let (t = xComplex(x) .- xOpr(x), m = xMetaSym(x)) in pdiv(m,t); ;-------------------------------------------------------------------- ; FD model (Functional Depedence) ; FUNC fdMatch(x:X):BOOL RETURN let (pattern = O("->",<'X,O("*",<'Y,'Z>)>)) in xMatch(x,pattern) && xProdOrio(RX(x)); ; ; If fdFirstMatch replaces the expression match with '_fd_ ; FUNC fdMetaMatch(x1:X):X RETURN if fdMatch(x1) then '_fd_ else if is-O(x1) && OX(x1) == "*" then if (LX(x1) == '_fd_ -> O(OX(x1),<'_fd_,fdMetaMatch(RX(x1))>), RX(x1) == '_fd_ -> O(OX(x1),)) otherwise (O(OX(x1),)) else x1; ; ; Applies fdMetaMatch until no more applications are possible ; FUNC fdApplyMetaMatch(x:X):X RETURN let (y = fdMetaMatch(x)) in if x == y then x else fdApplyMetaMatch(y); ; ; Degree of match ; FUNC fdDegreeMatch(x:X):INT RETURN if fdMatch(x) then 100 else let (t = xComplex(x) .- xOpr(x), m = xMetaSym(x)) in pdiv(m,t);