;-------------------------------------------------------------------- ; 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 = Cst | Var | Pset | List | Ffun | Prod | Plus; ; 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; ; 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);