;--------------------------------------------------------------------
; RSC-REPOSITORY                                               GET/97
;--------------------------------------------------------------------
;                  Copyright@1996 by F. Luis Neves
;
; Author(s):       FLN (F. Luis Neves)
; Revisions:       24.Mar.96 Rev:  8 May, 1996
;                            Rev:  5 Dec, 1996
;                            Rev: 10 Dec, 1996 (variable size c.)
;                            Rev:  2 Apr, 1997 (partial populations)
;                            Rev:  3 Jan, 1998 (final revisions)
;                            Rev:  8 Jan, 1998 (RPrb and CPrb added)
;                            Rev:  9 Jan, 1998 (2p-crossover added)
;                            Rev: 10 Jan, 1998 (best survives added)
;                            Rev: 10 Jan, 1998 (unif-crossover added)
;                            Rev: 21 Jan, 1998 (decimal-list genes)
;                                   
;--------------------------------------------------------------------
;
; Comments: GEnetic algorithms Tool
; 
; (a) Filiation: GET < FDEP
; (b) Interface:
;                        -----------
;                       |           |
;                       |           |
;             INIT ---> |           | EMPTY:Bool --->
;                       |           |
;         INS(A,B) ---> |    GET    |
;                       |           |
;       <--- SEL(A,I):B |           | <--- REM(A)
;                       |           |
;                       |           |
;                        -----------
;
; (c) State: S = A -> B
; (d) Model:
;
;--------------------------------------------------------------------
; Note: If I = {1,2,...} then B = B1:... B2:... B_:...;

;N int.cam - a CAMILA library for small integers (-32768..32767)

;A J.N. Oliveira (jno@di.uminho.pt)

;D
; This library provides a few functions useful in simple
; integer arithmetics.
; Note that CAMILA type INT ranges from -32768 to 32767.
; For long integer arithmetics other data types are required.
;E


FUNC intAvg(l:INT-seq,p:INT):INT
;
; intAvg(l,p) averages sequence l of integers, p adds decimal precision.
;
RETURN let (a=length(l),
            b=intSUM(l) .* intPot(10,p)) 
       in b ./ a; 

FUNC intSUM(l:INT-seq):INT
;
; intSUM(l) sums sequence l of integers.
;
RETURN add-orio(0,l);

FUNC intMIN(s:INT-set):INT
;
; intMIN(s) computes minimum of a set of INT.
;
RETURN min-orio(32767,s);

FUNC intMAX(s:INT-set):INT
;
; intMIN(s) computes maximum of a set of INT.
;
RETURN max-orio(0,s);

FUNC intMUL(l:INT-seq):INT
;
; intMUL(l) reduces sequence l of integers via multiplication.
;
RETURN mul-orio(1,l);

FUNC intPot(a:INT,b:INT):INT
;
; intPot(a,b) computes a^b.
;
RETURN let (l=< a | i <- inseg(b) >) in intMUL(l);

FUNC intSet2IncIntSeq(s:INT-set):INT-seq
;
; intSet2IncIntSeq(s) sorts s in INT-increasing order.
;
RETURN
    if s=={}
    then <>
    else let (m=intMIN(s),
              t={ x | x <- s: x != m})
         in <m>^intSet2IncIntSeq(t);

FUNC intSet2IntSeq(s:INT-set):INT-seq
;
; intSet2IntSeq(s) sorts s in INT-decreasing order.
;
RETURN
    if s=={}
    then <>
    else let (m=intMAX(s),
              t={ x | x <- s: x != m})
         in <m>^intSet2IntSeq(t);

FUNC intFF2index(ff:A->INT):A-seq 
;
; intFF2index(ff) builds index of ff (range INT-increasing ordering).
;
RETURN
    if ff==[] then <>
    else let (m=intMIN(ran(ff)),
              X={ a | a <- dom(ff): ff[a] == m },
              l=< a | a <- X >)
         in l ^ intFF2index(ff\X);

FUNC intAsRealRound(n:INT,i:INT):INT
;
; intAsRealRound(n,i) regards n as a real number with i decimal places
; and rounds it.
;
RETURN let (p=intPot(10,i),
            d= n ./ p,
            r= rem(n,p))
       in  if (r < p./2) then d else d .+ 1;

FUNC intAsReal2STR(i:INT,d:INT):STR
;
; intAsReal2STR(n,i) regards n as a real number with i decimal places
; and converts into to a string.
;
RETURN let (x=intPot(10,d),
            d=div(i,x),
            r=rem(i,x))
       in strcat(itoa(d),".",itoa(r));


TYPE

; PV = CS (Chromsize)              x
;      PS (Population Size)        x
;      SS (Segment Size)           x  (for binary representation only)
;      PC (Probability-Crossover)  x
;      PU (Probability-UCrossover) x
;      PM (Probability-Mutation)   x
;      VC (Variable Size Chrom.)   x
;      CT (Crossover type)         x
;      BS (Best survives)          x
;      GR (Gene Representation)    x  GR = 0 (binary),
;                                     GR = 1 (decimal)
;                                     GR = 2 (decimal-list)
;      MV (Maximum Gene Value)        for decimal representation only
; PP = ID (Individual) -> C (Chromossome) x F (Fitness) x S (Chrom.Size)
;                                         x RP (Relative Probability)
;                                         x CP (Cumulative Probability)

G = I -> R;
I = INT;
R = B1:Gene-list B2:Fit B3:CSize B4:RProb B5:CProb;
P = CS:CSize
    PS:PSize
    SS:SSize
    PC:PCVal
    PU:PUVal
    PM:PMVal
    VC:VSize
    CT:CType
    BS:BSurv
    GR:GRepr
    MV:MGVal;

Fit = INT;
Gene = INT | INT-list;
RProb = INT;
CProb = INT;
CSize = INT;
PSize = INT;
SSize = INT;
PCVal = INT;
PUVal = INT;
PMVal = INT;
VSize = BOOL;
CType = INT;
BSurv = BOOL;
GRepr = INT;
MGVal = INT | INT-set;

ENDTYPE

;--------------------------------------------------------------------
; Note: If I = {1,2,...} then SEL(a,1) = B1(S[a]); SEL(a,2) = B2(S[a]); ...

FUNC gpINIT():Void
STATE G <- [];

FUNC gpINS(a:I,b:R):Void
PRE a notin dom(G)
STATE G <- G + [a->b];

FUNC gpREM(a:I):Void
STATE G <- G \ {a};

FUNC gpSEL(a:I,i:INT):R
PRE a in dom(G)
RETURN if (i == 1 -> p1(G[a]),
           i == 2 -> p2(G[a]),
           i == 3 -> p3(G[a]),
           i == 4 -> p4(G[a]),
           i == 5 -> p5(G[a]));

FUNC gpEMPTY(): Bool
RETURN G == [];

;--------------------------------------------------------------------
; Genetic Programming auxiliary functions

FUNC perc(a:INT,b:INT):INT
PRE b != 0 -> 0
RETURN
     if (a<32   -> ((a .* 1000)./b)./10,
         a<64   -> ((a .*  500)./b)./ 5,
         a<160  -> ((a .*  200)./b)./ 2,
         a<320  ->  (a .*  100)./b,
         a<640  -> ((a .*   50)./b).* 2,
         a<1280 -> ((a .*   25)./b).* 4)
     otherwise ((a./b) .* 100);

FUNC prob(i:INT,j:INT):BOOL
RETURN rand(j) < i;

FUNC rand2(i:INT,j:INT):INT
RETURN rand(j .- i .+ 1) .+ i;

FUNC rchoice(s:ANY-set):ANY
PRE s != {}
RETURN nth(rand(card(s)).+1,< x | x<-s >);

rcprob(s) = let (tf = add-orio(0,{ p2(s[k]) | k <- dom(s) }))
            in _rcprob_(s,tf,0);

_rcprob_(s,tf,cf) =
    if (s == []) then []
    else let (x = choice(dom(s)),
              y = s[x],
              cx = p1(y),
              fx = p2(y),
              sx = p3(y),
              rfx = perc(fx,tf),
              cfx = cf .+ rfx)
         in [ x -> R(cx,fx,sx,rfx,cfx) ] + _rcprob_(s\{x},tf,cfx);

;
; One-point crossover for variable size chromosomes
;
vcrossover(s,i) =
    if i > PS(GV) then []
    else if (prob(PC(GV),100))
         then _vcross_(s,i) + vcrossover(s,i.+2)
         else _ncross_(s,i) + vcrossover(s,i.+1);

_vcross_(s,k) =
    let (x = rchoice(dom(s)),
         y = rchoice(dom(s)),
         sx = gpSEL(x,3), sy = gpSEL(y,3),
         cp = if sx < sy then rand(sx) else rand(sy),
         cx = gpSEL(x,1), cy = gpSEL(y,1),
         nx = < nth(i,cx) | i <- inseg(cp) > ^
              < nth(i,cy) | i <- {j | j <- inseg(sy):gt(j,cp)} >,
         ny = < nth(i,cy) | i <- inseg(cp) > ^
              < nth(i,cx) | i <- {j | j <- inseg(sx):gt(j,cp)} >,
         fx = gpSEL(x,2), fy = gpSEL(y,2),
         rfx = gpSEL(x,4), rfy = gpSEL(y,4),
         cfx = gpSEL(x,5), cfy = gpSEL(y,5))
    in [ k -> R(nx,fx,sy,rfx,cfx),
         k.+1 -> R(ny,fy,sx,rfy,cfy) ];

;
; To be replaced by the specific evaluation function...
;
_evalf_(c) = if c == <> then 0 else intSUM(c);
;_evalf_(c) = if c == <> then 0
;             else let (h = head(c),t = tail(c))
;                  in if (h == 1) then 1 .+ _evalf_(t)
;                     else _evalf_(t);

;_evalf_(c) = _eval2_(c,1);
_eval2_(c,i) = if c == <> then 0
               else let (h = hd(c), t = tl(c))
                    in div(h,i) .+ rem(h,i) .+ _eval2_(t,i.+1);

;--------------------------------------------------------------------
; Genetic Programming main functions

;
; Default parameters
;
GV <- P(10,10,1,25,60,10,false,1,true,1,37);

FUNC gpSTART()
STATE do(gpINIT(),
         if (GR(GV) == 0 -> _start0_(),
             GR(GV) == 1 -> _start1_(),
             GR(GV) == 2 -> _start2_()));

_start0_() = 
    if not(VC(GV))
    then foreach(k,inseg(PS(GV)),
         let (b = R(< rem(rand(i),2) | i <- inseg(CS(GV)) >,0,0,0,0))
         in gpINS(k,b))
    else foreach(k,inseg(PS(GV)),
         let (r = rand(CS(GV)),
              b = R(< rem(rand(i),2) | i <- inseg(r) >,0,0,0,0))
         in gpINS(k,b));

_start1_() =
    if not(VC(GV))
    then foreach(k,inseg(PS(GV)),
         let (b = R(< rand(MV(GV)) | i <- inseg(CS(GV)) >,0,0,0,0))
         in gpINS(k,b))
    else foreach(k,inseg(PS(GV)),
         let (r = rand(CS(GV)),
              b = R(< rand(MV(GV)) | i <- inseg(r) >,0,r,0,0))
         in gpINS(k,b));

_start2_() =
    if not(VC(GV))
    then foreach(k,inseg(PS(GV)),
         let (b = R(< < rand(MV(GV)) | j <- inseg(SS(GV)) > | i <- inseg(CS(GV)) >,0,0,0,0))
         in gpINS(k,b))
    else foreach(k,inseg(PS(GV)),
         let (r = rand(CS(GV)),
              b = R(< < rand(MV(GV)) | j <- inseg(SS(GV)) > | i <- inseg(r) >,0,r,0,0))
         in gpINS(k,b));



FUNC gpPSTART(s:INT-set)
PRE GR(GV) == 1 || GR(GV) == 2
STATE progn(gpINIT(),
            if (GR(GV) == 1 -> _pstart1_(s),
                GR(GV) == 2 -> _pstart2_(s)));

_pstart1_(s) =
    if not(VC(GV))
    then foreach(k,inseg(PS(GV)),
         let (b = R(< rchoice(s) | i <- inseg(CS(GV)) >,0,0,0,0))
         in gpINS(k,b))
    else foreach(k,inseg(PS(GV)),
         let (r = rand(CS(GV)),
              b = R(< rchoice(s) | i <- inseg(r) >,0,r,0,0))
         in gpINS(k,b));

_pstart2_(s) =
    if not(VC(GV))
    then foreach(k,inseg(PS(GV)),
         let (b = R(< < rchoice(s) | j <- inseg(SS(GV)) > | i <- inseg(CS(GV)) >,0,0,0,0))
         in gpINS(k,b))
    else foreach(k,inseg(PS(GV)),
         let (r = rand(CS(GV)),
              b = R(< < rchoice(s) | j <- inseg(SS(GV)) > | i <- inseg(r) >,0,r,0,0))
         in gpINS(k,b));


FUNC gpSELECT()
STATE G <- let (t = intMAX({ p5(G[x]) | x <- dom(G) }))
           in if (BS(GV))
              then let (b = gpBEST(), x = choice(dom(b)))
                   in [ 1 -> b[x] ] + _roleta_(G,2,t)
              else _roleta_(G,1,t);

_roleta_(s,n,t) =
    if n > PS(GV) then []
    else _select_(s,n,rand(t)) + _roleta_(s,n.+1,t);

_select_(s,i,p) =
    if (s == []) then []
    else let (x = choice(dom(s)),
              y = s[x],
              cx = p1(y),
              fx = p2(y),
              sx = p3(y),
              rfx = p4(y),
              cfx = p5(y))
         in if (p > cfx) then _select_(s\{x},i,p)
            else [ i -> R(cx,fx,sx,rfx,cfx) ];

FUNC gpCROSSOVER()
STATE if (BS(GV))
      then let (b = gpBEST(),
                x = choice(dom(b)),
                o = if (CT(GV) == 1 -> crossover1(G,2),
                        CT(GV) == 2 -> crossover2(G,2),
                        CT(GV) == 3 -> ucrossover(G,2)),
                p = if card(dom(o)) == PS(GV)
                    then o \ { rchoice(dom(o)) }
                    else o)
           in G <- [ 1 -> b[x] ] + p
      else let (o = if (CT(GV) == 1 -> crossover1(G,1),
                        CT(GV) == 2 -> crossover2(G,1),
                        CT(GV) == 3 -> ucrossover(G,1)),
                p = if card(dom(o)) == PS(GV)
                    then o
                    else o \ { rchoice(dom(o)) })
           in G <- p;

;
; One-point crossover
;
crossover1(s,i) =
    if i > PS(GV) then []
    else if (prob(PC(GV),100))
         then _cross1_(s,i) + crossover1(s,i.+2)
         else _ncross_(s,i) + crossover1(s,i.+1);

_cross1_(s,k) =
    let (x = rchoice(dom(s)),
         y = rchoice(dom(s)),
         cs = CS(GV),
         cp = rand(cs),
         cx = gpSEL(x,1), cy = gpSEL(y,1),
         nx = < nth(i,cx) | i <- inseg(cp) > ^
              < nth(i,cy) | i <- {k | k <- inseg(cs):gt(k,cp)} >,
         ny = < nth(i,cy) | i <- inseg(cp) > ^
              < nth(i,cx) | i <- {k | k <- inseg(cs):gt(k,cp)} >,
         fx = gpSEL(x,2), fy = gpSEL(y,2),
         sx = gpSEL(x,3), sy = gpSEL(y,3),
         rfx = gpSEL(x,4), rfy = gpSEL(y,4),
         cfx = gpSEL(x,5), cfy = gpSEL(y,5))
    in [ k -> R(nx,fx,sx,rfx,cfx),
         k.+1 -> R(ny,fy,sy,rfy,cfy) ];

_ncross_(s,k) = let (x = rchoice(dom(s))) in [ k -> s[x] ];

;
; Two-point crossover
;
crossover2(s,i) =
    if i > PS(GV) then []
    else if (prob(PC(GV),100))
         then _cross2_(s,i) + crossover2(s,i.+2)
         else _ncross_(s,i) + crossover2(s,i.+1);

_cross2_(s,k) =
    let (x = rchoice(dom(s)),
         y = rchoice(dom(s)),
         cs = CS(GV),
         cp1 = rand(cs), cp2 = rand2(cp1,cs),
;p1 = princ("\ncp1=",cp1),
;p2 = princ("\ncp2=",cp2),
         cx = gpSEL(x,1), cy = gpSEL(y,1),
         nx = < nth(i,cx) | i <- inseg(cp1) > ^
              < nth(i,cy) | i <- {k | k <- inseg(cp2):gt(k,cp1)}> ^
              < nth(i,cx) | i <- {k | k <- inseg(cs):gt(k,cp2)} >,
         ny = < nth(i,cy) | i <- inseg(cp1) > ^
              < nth(i,cx) | i <- {k | k <- inseg(cp2):gt(k,cp1)}> ^
              < nth(i,cy) | i <- {k | k <- inseg(cs):gt(k,cp2)} >,
         fx = gpSEL(x,2), fy = gpSEL(y,2),
         sx = gpSEL(x,3), sy = gpSEL(y,3),
         rfx = gpSEL(x,4), rfy = gpSEL(y,4),
         cfx = gpSEL(x,5), cfy = gpSEL(y,5))
    in [ k -> R(nx,fx,sx,rfx,cfx),
         k.+1 -> R(ny,fy,sy,rfy,cfy) ];

;
; Uniform crossover
;
ucrossover(s,i) =
    if i > PS(GV) then []
    else if (prob(PC(GV),100))
         then _ucross_(s,i) + ucrossover(s,i.+2)
         else _ncross_(s,i) + ucrossover(s,i.+1);

_ucross_(s,k) =
    let (x = rchoice(dom(s)),
         y = rchoice(dom(s)),
         cs = CS(GV),
         cx = gpSEL(x,1), cy = gpSEL(y,1),
         <nx,ny> = _ucrossover_(cx,cy),
         fx = gpSEL(x,2), fy = gpSEL(y,2),
         sx = gpSEL(x,3), sy = gpSEL(y,3),
         rfx = gpSEL(x,4), rfy = gpSEL(y,4),
         cfx = gpSEL(x,5), cfy = gpSEL(y,5))
    in [ k -> R(nx,fx,sx,rfx,cfx),
         k.+1 -> R(ny,fy,sy,rfy,cfy) ];

_ucrossover_(cx,cy) =
    if (cx == <> || cy == <>) then <<>,<>>
    else let (hx = hd(cx), hy = hd(cy),
              tx = tl(cx), ty = tl(cy),
              tt = _ucrossover_(tx,ty))
         in if (prob(PU(GV),100))
            then <cons(hy,p1(tt)),cons(hx,p2(tt))>
            else <cons(hx,p1(tt)),cons(hy,p2(tt))>;


FUNC gpMUTATION()
STATE if (GR(GV) == 0 -> G <- mutation(G),
          GR(GV) == 1 -> G <- mutation10(G),
          GR(GV) == 2 -> G <- mutation10l(G));

mutation(s) =
    if (s == []) then []
    else let (x = choice(dom(s)),
              c = < _mutate_(k) | k <- gpSEL(x,1) >,
              fx = gpSEL(x,2),
              sx = gpSEL(x,3),
              rfx = gpSEL(x,4),
              cfx = gpSEL(x,5))
         in [ x -> R(c,fx,sx,rfx,cfx) ] + mutation(s\{x});

_mutate_(bit) = if (prob(PM(GV),100))
                then if (bit == 0 -> 1,
                         bit == 1 -> 0)
                else bit;

mutation10(s) =
    if (s == []) then []
    else let (x = choice(dom(s)),
              c = < _mutate10_(k) | k <- gpSEL(x,1) >,
              fx = gpSEL(x,2),
              sx = gpSEL(x,3),
              rfx = gpSEL(x,4),
              cfx = gpSEL(x,5))
         in [ x -> R(c,fx,sx,rfx,cfx) ] + mutation10(s\{x});

mutation10l(s) =
    if (s == []) then []
    else let (x = choice(dom(s)),
              c = < ((_mutate10_)-list)(k) | k <- gpSEL(x,1) >,
              fx = gpSEL(x,2),
              sx = gpSEL(x,3),
              rfx = gpSEL(x,4),
              cfx = gpSEL(x,5))
         in [ x -> R(c,fx,sx,rfx,cfx) ] + mutation10l(s\{x});

_mutate10_(dig) = if (prob(PM(GV),100))
                  then let (v = if is-INT(MV(GV))
                                then rand(MV(GV)) 
                                else rchoice(MV(GV)))
                       in v
                  else dig;


FUNC gpEVAL()
STATE G <- rcprob(evalf(G));

evalf(s) = if (s == []) then []
           else let (x = choice(dom(s)),
                     cx = gpSEL(x,1),
                     sx = gpSEL(x,3))
                in [ x -> R(cx,_evalf_(cx),sx,0,0) ] + evalf(s\{x});

FUNC gpBEST():I->R
RETURN [ k -> G[k] | k <- dom(G)
                   : gpSEL(k,2) == max-orio(0,{gpSEL(x,2) | x <- dom(G)}) ];

FUNC gpBESTVAL():I->R
PRE not(gpEMPTY())
RETURN let (m = max-orio(0,{ gpSEL(x,2) | x <- dom(G) }),
;            b = ([ k -> <gpSEL(k,1),gpSEL(k,2)> | k <- dom(G) : gpSEL(k,2) == m ]),
            b = ([ k -> G[k] | k <- dom(G) : gpSEL(k,2) == m ]),
            c = choice(dom(b)))
;       in < _evalf_(b[c]),b[c] >;
;       in [ c->b[c] ];
       in B1(b[c]);

FUNC gpEVOLUTION(n:INT)
STATE progn(gpSTART(),gpEVAL(),
fp <- fopen("w","_"),
            princ("> Best(",0,"): ",
;            mypptex(gpBESTVAL()),
            gpBESTVAL(),
            "\n> thinking..."),
            foreach(x,inseg(n),gpSELECT(),gpCROSSOVER(),gpMUTATION(),gpEVAL(),
                    princ(" best (",x,"): ",
;                    mypptex(gpBESTVAL()),
                    gpBESTVAL(),
                    "\n> thinking...")),
fclose(fp));

mypp(x) = let (a = choice(dom(x)), b = x[a])
          in "IND(" ++
             itoa(a) ++
             ") with CROM(" ++
             "<" ++ pplst(p1(b)) ++ ">" ++
             ") and EVAL(" ++
             itoa(p2(b)) ++
             ")";

mypptex(x) = let (a = choice(dom(x)), b = x[a],
                  s = itoa(a) ++
             " & " ++
             "$<" ++ pplst(p1(b)) ++ ">$" ++
             " & " ++
             itoa(p2(b)) ++
             "\\\\ \n\\hline\\\\\n")
             in fprint("_","a",<s>);


pplst(l) = if l == <> then "" else itoa(hd(l)) ++ "," ++ pplst(tl(l));
               

FUNC gpSETTINGS(p:P)
STATE GV <- P(CS(p),PS(p),SS(p),PC(p),PU(p),PM(p),VC(p),CT(p),BS(p),GR(p),MV(p).+1);

FUNC gpSHOWSETTINGS()
RETURN princ(
  "CS (Chromsize)                   = ",CS(GV),
  "\nPS (Population Size)             = ",PS(GV),
  "\nSS (Segment Size)                = ",SS(GV)," (decimal list representation only)",
  "\nPC (Probability Crossover)       = ",PC(GV),"%",
  "\nPU (Probability Unif. Crossover) = ",PU(GV),"%",
  "\nPM (Probability Mutation)        = ",PM(GV),"%",
  "\nVC (Variable Size Chrom.)        = ",VC(GV)," (true/false)",
  "\nCT (Crossover type)              = ",CT(GV)," (1=one-point, 2=two-point,3=unif.)",
  "\nBS (Best survives)               = ",BS(GV)," (true/false)",
  "\nGR (Gene Representation)         = ",GR(GV)," (0=binary, 1=decimal, 2=decimal-list)",
  "\nMV (Maximum Gene Value)          = ",MV(GV).-1," (decimal and dec-list representation only)",
  "\n"
);

FUNC gpRULES(a:I):INT-list
PRE a in dom(G)
RETURN let (c = 1, ps = SS(GV), cx = gpSEL(a,1))
       in _c2rules_(c,ps,cx);

_c2rules_(c,ps,cx) =
    let (l = length(cx))
    in if gt(c,l) then <>
       else let (cp = < nth(i,cx) | i <- inseg(l)
                                  : (geq(i,c) && leq(i,c .+ ps .- 1)) >)
            in cons(bin2dec(cp),_c2rules_(add(c,ps),ps,cx));

bin2dec(s) = if s == <> then 0
             else if (hd(s) == 1)
                  then let (l = sub(length(s),1),
                            v = if (l == 0 -> 1,
                                    l == 1 -> 2,
                                    l == 2 -> 4,
                                    l == 3 -> 8,
                                    l == 4 -> 16,
                                    l == 5 -> 32,
                                    l == 6 -> 64,
                                    l == 7 -> 128,
                                    l == 8 -> 256,
                                    l == 9 -> 512,
                                    l == 10 -> 1024)
                                 otherwise (princ("\n!..out of range...\n")))
                       in add(v,bin2dec(tl(s)))
                  else bin2dec(tl(s));


;--------------------------------------------------------------------
; RSC-REPOSITORY                                               RET/97
;--------------------------------------------------------------------
;                    Copyright@1997 by F. Luis Neves
;
; Author(s):         FLN (F. Luis Neves)
; Revisions:         25.Fev.97 Rev: 24 Mar, 1997
;                              Rev: 18 Jun, 1997 (xDMatch,xMetaMatch)
;                              Rev:  1 Dec, 1997 (Abs/Rep Functions)
;                              Rev:  3 Dec, 1997 (Final revisions)
;                              Rev: 25 Jan, 1998 (X = V | X-list)
;
;--------------------------------------------------------------------
;
; Comments: REwrite system Tool
; 
; (a) Filiation: RET < EXPT
; (b) Interface:
;                        -----------
;                       |           |
;           CON(B) ---> |           | <--- RST(X)
;                       |           |
;           VAR(A) ---> |    RET    | <--- LST(X)
;                       |           |
;          PUSH(B) ---> |           | POP(P):B --->
;                       |           |
;                        -----------
;
; (c) State: S = X; X = C + V + O x X^2
; (c) State: S = X; X = V + O x X-list
; (d) Model:
;
;--------------------------------------------------------------------
;

TYPE

S = X;
;C = INT;
V = SYM;
F = STR;
;X = C | V | F | O;
X = V | F | O;
;O = OX:STR LX:X RX:X;
O = OX:STR AX:X-list;

ENDTYPE

;--------------------------------------------------------------------
; Auxiliary functions

LX(o) = p1(AX(o));
RX(o) = p2(AX(o));
isC(x) = is-O(x) && AX(x) == <>;

;
; x/y (x,y reals and result x 100)
;
pdiv(x,y) = x .* div(100,y);

;
; Number of variables
;
FUNC xVar(x:X):INT
;RETURN if (isC(x) -> 0,
RETURN if (is-V(x) -> 1,
           is-O(x) -> intSUM(< xVar(a) | a <- AX(x) >))
       otherwise (0);

;
; Number of constants
;
FUNC xCon(x:X):INT
RETURN if (isC(x) -> 1,
           is-V(x) -> 0,
           is-O(x) -> intSUM(< xCon(a) | a <- AX(x) >))
       otherwise (0);

;
; Number of operators 
;
FUNC xOpr(x:X):INT
RETURN if (isC(x) -> 0,
           is-V(x) -> 0,
           is-O(x) -> 1 .+ intSUM(< xOpr(a) | a <- AX(x) >))
       otherwise (0);

;
; Number of meta-symbols ('_xx_,'_er_,'_ff_,...) 
;
FUNC xMetaSym(x:X):INT
RETURN if (x == '_xx_ -> 1,
           x == '_er_ -> 1,
           x == '_ff_ -> 1,
           x == '_fd_ -> 1,
;           isC(x) -> 0,
;           is-V(x) -> 0,
           is-O(x) -> intSUM(< xMetaSym(a) | a <- AX(x) >))
       otherwise (0);

;
; Expression complexity
;
FUNC xComplex(x:X):INT
RETURN if (is-V(x) -> 1,
;           isC(x) -> 1,
           is-O(x) -> 1 .+ intSUM(< xComplex(a) | a <- AX(x) >))
       otherwise (100);

;
; Number of common nodes between expressions
;
FUNC xCommon(x1,x2:X):INT
RETURN if (is-V(x1) -> if is-V(x2) then 1 else 0,
           is-O(x1) -> if is-O(x2)
                       then let (ae = AX(x1),ap = AX(x2))
                       in if OX(x1) != OX(x2)
                          then _xCommon_(ae,ap)
                          else 1 .+ _xCommon_(ae,ap));

_xCommon_(ae,ap) =
    if (ae == <> -> 0,
        ap == <> -> 0)
    otherwise (let (he = hd(ae), te = tl(ae),
                    hp = hd(ap), tp = tl(ap))
               in xCommon(he,hp) .+ _xCommon_(te,tp));

;
; Expression print
;
FUNC xPrint(x:X):Void
RETURN if (isC(x) -> princ(OX(x)),
           is-V(x) -> princ(x),
           is-O(x) -> let (o = OX(x), a = AX(x))
                      in do(princ(o,"("),
                            foreach(a,AX(x),xPrint(a)),
                            princ(")")));

;
; Expression string
;
FUNC xString(x:X):STR-list
RETURN if (isC(x) -> <OX(x)>,
           is-V(x) -> <symstr(x)>,
           is-F(x) -> <x>,
           is-O(x) -> let (o = OX(x),
                           a = AX(x))
                      in xInfix(o,a))
       otherwise (<>);

FUNC xInfix(o:STR,a:X-list):STR-list
RETURN if (a == <>) then <>
       else let (h = hd(a), t = tl(a))
            in if (t == <>) then <o,"(">^xString(h)^<")">
               else <"(">^xString(h)^CONC(<<o>^xString(x) | x <- t>)^<")">;

;
; Expression TeX string
;
FUNC xTeX(x:X):STR-list
RETURN if (isC(x) -> <OX(x)>,
           is-V(x) -> <symstr(x)>,
           is-F(x) -> <x>,
           is-O(x) -> let (o = OX(x),
                           a = AX(x))
                      in xTeXInfix(o,a))
       otherwise (<>);

FUNC xTeXInfix(o:STR,a:X-list):STR-list
RETURN if (a == <>) then <>
       else let (h = hd(a), t = tl(a),
                 s = if (o == "*" -> " \\times ",
                         o == "^" -> "^",
                         o == "+" -> " + ",
                         o == "->" -> " \\hookrightarrow ")
                     otherwise (o))
            in if (t == <>) then <s,"{(">^xTeX(h)^<")}">
               else <"{(">^xTeX(h)^CONC(<<s>^xTeX(x) | x <- t>)^<")}">;

;
; Expression subterms which does not match a given template x2
;
FUNC xNotMatch(x1,x2:X):INT
RETURN if (isC(x2) -> if isC(x1) then 1 else 0,
           is-V(x2) -> if is-V(x1) then 1 else 0,
           is-O(x2) -> if is-O(x1)
                       then if xMatch(x1,x2)
                            then intSUM(< xNotMatch(a,x2) | a <- AX(x1) >)
                            else 1 .+ intSUM(< xNotMatch(a,x2) | a <- AX(x1) >)
                       else 0)
       otherwise (0);

;
; Expression match - x2 is the template
;
FUNC xMatch(x1,x2:X):BOOL
RETURN if (isC(x1) && isC(x2) -> x1 == x2,
           is-V(x2)             -> true,
           is-F(x1)             -> true,
           is-O(x1) && is-O(x2) -> let (o1 = OX(x1), o2 = OX(x2),
                                        a1 = AX(x1), a2 = AX(x2))
                                   in (o1 == o2) && _xMatch_(a1,a2))
       otherwise (false);

_xMatch_(a1,a2) =
    if (a1 == <> && a2 == <> -> true,
        a1 != <> && a2 == <> -> false,
        a1 == <> && a2 != <> -> false)
    otherwise (let (h1 = hd(a1), h2 = hd(a2),
                    t1 = tl(a1), t2 = tl(a2))
               in xMatch(h1,h2) && _xMatch_(t1,t2));

;
; Expression first match (is there any match?) - x2 is the template
;
FUNC xFirstMatch(x1,x2:X):BOOL
RETURN if xMatch(x1,x2) then true
       else if is-O(x1)
            then ||-orio(false,< xFirstMatch(x,x2) | x <- AX(x1) >)
            else false;

;
; Expression near match
;
FUNC xNearMatch(x1,x2:X):INT
RETURN if (xMatch(x1,x2) -> 100,
           _xNearMatch1_(x1,x2,33,39) -> 50,
           _xNearMatch1_(x2,x1,33,39) -> 50)
;           _xNearMatch2_(x1,x2,39) -> 25)
       otherwise (0);

_xNearMatch1_(x1,x2,i,j) =
  if (i > j) then false
  else if xMatch(FirstMatch(x1,i),x2) then true
       else _xNearMatch1_(x1,x2,i.+1,j);

;
; pouco eficiente...
;
_xNearMatch2_(x1,x2,k) =
  let (m = { xMatch(FirstMatch(x0,i),FirstMatch(x2,j)) | i <- inseg(k),
                                                         j <- inseg(k) })
  in if 'true in m then true else false;

;
; If xFirstMatch replaces the expression match with '_xx_
; x2 is the template
;
FUNC xMetaMatch(x1,x2:X):X
RETURN
  if xMatch(x1,x2) then '_xx_
  else if is-O(x1)
       then let (o = OX(x1), a = AX(x1))
            in O(o,_xMetaMatch_(a,x2))
       else x1;
;       then if (LX(x1) == '_xx_ -> O(OX(x1),<'_xx_,xMetaMatch(RX(x1),x2)>),
;                RX(x1) == '_xx_ -> O(OX(x1),<xMetaMatch(RX(x1),x2),'_xx_>),
;                xMetaMatch(LX(x1),x2) == '_xx_ -> O(OX(x1),<'_xx_,RX(x1)>),
;                xMetaMatch(RX(x1),x2) == '_xx_ -> O(OX(x1),<LX(x1),'_xx_>))
;            otherwise (O(OX(x1),<xMetaMatch(LX(x1),x2),xMetaMatch(RX(x1),x2)>))
;       else x1;

_xMetaMatch_(a1,x2) =
    if (a1 == <>) then <>
    else let (h = hd(a1), t = tl(a1))
         in if h == '_xx_ then cons(h,_xMetaMatch_(t,x2))
            else cons(xMetaMatch(h,x2),_xMetaMatch_(t,x2));

;
; Degree of match
;
FUNC xDegreeMatch(x1,x2:X):INT
RETURN
  if (xMatch(x1,x2)      -> 100,
      xFirstMatch(x1,x2) -> div(100,xComplex(xMetaMatch(x1,x2))))
  otherwise (0);


;--------------------------------------------------------------------
;
; Rewrite functions
;
;--------------------------------------------------------------------
;
;
; Root Match: applies the rule (if possible) to the root only
;
FUNC RootMatch(x:X,i:INT):X
RETURN if (i == 0 -> RR0(x),
           i == 1 -> RR1(x),
           i == 2 -> RR2(x),
           i == 3 -> RR3(x),
           i == 4 -> RR4(x),
           i == 5 -> RR5(x),
           i == 6 -> RR6(x),
           i == 7 -> RR7(x),
           i == 8 -> RR8(x),
           i == 9 -> RR9(x),
           i == 10 -> RR10(x),
           i == 11 -> RR11(x),
           i == 12 -> RR12(x),
           i == 13 -> RR13(x),
           i == 14 -> RR14(x),
           i == 15 -> RR15(x),
           i == 16 -> RR16(x),
           i == 17 -> RR17(x),
           i == 18 -> RR18(x),
           i == 19 -> RR19(x),
           i == 20 -> RR20(x),
           i == 21 -> RR21(x),
           i == 22 -> RR22(x),
           i == 23 -> RR23(x),
           i == 24 -> RR24(x),
           i == 25 -> RR25(x),
           i == 26 -> RR26(x),
           i == 27 -> RR27(x),
           i == 28 -> RR28(x),
           i == 29 -> RR29(x),
           i == 30 -> RR30(x),
           i == 31 -> RR31(x),
           i == 32 -> RR32(x),
; Inequacional
           i == 33 -> RR33(x),
           i == 34 -> RR34(x),
           i == 35 -> RR35(x),
           i == 36 -> RR36(x),
           i == 37 -> RR37(x),
           i == 38 -> RR38(x),
           i == 39 -> RR39(x));

;
; First Match: applies the rule (if possible) to the first expression match
;
FUNC FirstMatch(x:X,i:INT):X
RETURN if (isC(x) || is-V(x)) then RootMatch(x,i)
       else let (x1 = RootMatch(x,i))
            in if (x != x1) then x1
               else let (o = OX(x), a = AX(x))
                    in O(o,_FirstMatch_(a,i));

_FirstMatch_(a,i) =
    if (a == <>) then <>
    else let (h = hd(a), t = tl(a), r = FirstMatch(h,i))
         in if (h != r) then cons(r,t) else cons(h,_FirstMatch_(t,i));

;
; Applies a list of Root Match rules
;
FUNC ApplyRootMatch(x:X,l:INT-list):X
RETURN if (l == <>) then x
       else let (h = head(l), t = tail(l), r = RootMatch(x,h))
            in ApplyRootMatch(r,t);

;
; Applies a list of FirstMatch rules
;
FUNC ApplyFirstMatch(x:X,l:INT-list):X
RETURN if (l == <>) then x
       else let (h = head(l), t = tail(l), r = FirstMatch(x,h))
            in ApplyFirstMatch(r,t);


;--------------------------------------------------------------------
; 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
PRE xMatch(x,O("*",<'A,'B>)) -> x
RETURN O("*",<RX(x),LX(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
PRE xMatch(x,O("*",<'A,O("*",<'B,'C>)>)) -> x
RETURN O("*",<O("*",<LX(x),LX(RX(x))>),RX(RX(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
PRE xMatch(x,O("*",<O("*",<'A,'B>),'C>)) -> x
RETURN O("*",<LX(LX(x)),O("*",<RX(LX(x)),RX(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
PRE xMatch(x,O("*",<'A,O("1",<>)>)) -> x
RETURN LX(x);

ABS4(x) = "nilit";
REP4(x) = "p1";
INV4(x) = "";

FUNC RR5(x:X):X
PRE is-V(x) -> x
RETURN O("*",<x,O("1",<>)>);

ABS5(x) = "p1";
REP5(x) = "nilit";
INV5(x) = "";

;
; (2.25) A + B = B + A
;
FUNC RR6(x:X):X
PRE xMatch(x,O("+",<'A,'B>)) -> x
RETURN O("+",<RX(x),LX(x)>);

ABS6(x) = "";
REP6(x) = "";
INV6(x) = "";

;
; (2.26) A + (B + C) = (A + B) + C
;
FUNC RR7(x:X):X
PRE xMatch(x,O("+",<'A,O("+",<'B,'C>)>)) -> x
RETURN O("+",<O("+",<LX(x),LX(RX(x))>),RX(RX(x))>);

FUNC RR8(x:X):X
PRE xMatch(x,O("+",<O("+",<'A,'B>),'C>)) -> x
RETURN O("+",<LX(LX(x)),O("+",<RX(LX(x)),RX(x)>)>);

;
; (2.27) A + 0 = A
;
FUNC RR9(x:X):X
PRE xMatch(x,O("+",<'A,O("0",<>)>)) -> x
RETURN LX(x);

FUNC RR10(x:X):X
PRE is-V(x) -> x
RETURN O("+",<x,O("0",<>)>);

;
; (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("*",<LX(x),LX(RX(x))>),O("*",<LX(x),RX(RX(x))>)>) else x;

FUNC RR13(x:X):X
RETURN if xMatch(x,O("+",<O("*",<'A,'B>),O("*",<'A,'C>)>)) && LX(LX(x)) == LX(RX(x))
       then O("*",<LX(LX(x)),O("+",<RX(LX(x)),RX(RX(x))>)>) 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("^",<LX(x),LX(RX(x))>),O("^",<LX(x),RX(RX(x))>)>) else x;

FUNC RR16(x:X):X
RETURN if xMatch(x,O("+",<O("^",<'A,'B>),O("^",<'A,'C>)>)) && LX(LX(x)) == LX(RX(x))
       then O("^",<LX(LX(x)),O("+",<RX(LX(x)),RX(RX(x))>)>) 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("^",<x,O("1",<>)>) else x;

;
; (2.36) 1 ^ A = 1
;
FUNC RR19(x:X):X
RETURN if xMatch(x,O("^",<O("1",<>),'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("^",<O("*",<'B,'C>),'A>))
       then O("*",<O("^",<LX(LX(x)),RX(x)>),O("^",<RX(LX(x)),RX(x)>)>) else x;

FUNC RR21(x:X):X
RETURN if xMatch(x,O("*",<O("^",<'B,'A>),O("^",<'C,'A>)>)) && RX(LX(x)) == RX(RX(x))
       then O("^",<O("*",<LX(LX(x)),LX(RX(x))>),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("^",<O("^",<LX(x),RX(RX(x))>),LX(RX(x))>) else x;

ABS22(x) = "uncurry";
REP22(x) = "curry";
INV22(x) = "";

FUNC RR23(x:X):X
RETURN if xMatch(x,O("^",<O("^",<'C,'B>),'A>))
       then O("^",<LX(LX(x)),O("*",<RX(x),RX(LX(x))>)>) 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("^",<O("+",<RX(x),O("1",<>)>),LX(x)>) else x;

FUNC RR25(x:X):X
RETURN if xMatch(x,O("^",<O("+",<'B,O("1",<>)>),'A>))
       then O("->",<RX(x),LX(LX(x))>) 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("->",<O("+",<'B,'C>),'A>))
       then O("*",<O("->",<LX(LX(x)),RX(x)>),O("->",<RX(LX(x)),RX(x)>)>) else x;

FUNC RR27(x:X):X
RETURN if xMatch(x,O("*",<O("->",<'B,'A>),O("->",<'C,'A>)>)) && RX(LX(x)) == RX(RX(x))
       then O("->",<O("+",<LX(LX(x)),LX(RX(x))>),RX(LX(x))>) else x;

;
; (2.64) 0 -> A = 1
;
FUNC RR28(x:X):X
RETURN if xMatch(x,O("->",<O("0",<>),'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("^",<O("2",<>),LX(x)>) else x;

ABS29(x) = "ffAset";
REP29(x) = "dom";
INV29(x) = "";

FUNC RR30(x:X):X
RETURN if xMatch(x,O("^",<O("2",<>),'A>)) then O("->",<RX(x),O("1",<>)>) 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("->",<O("1",<>),'A>)) then O("+",<RX(x),O("1",<>)>) else x;

FUNC RR32(x:X):X
RETURN if xMatch(x,O("+",<'A,O("1",<>)>)) then O("->",<O("1",<>),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("->",<LX(x),LX(RX(x))>),O("->",<LX(x),RX(RX(x))>)>)
       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("->",<O("*",<'A,'B>),'C>))
       then O("->",<LX(LX(x)),O("->",<RX(LX(x)),RX(x)>)>)
       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("*",<O("^",<O("2",<>),LX(x)>),O("->",<O("*",<LX(x),LX(RX(x))>),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("->",<LX(x),LX(RX(x))>),O("->",<O("*",<LX(x),LX(RX(RX(x)))>),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("->",<LX(x),LX(RX(x))>),O("->",<LX(x),RX(RX(x))>)>) 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("2",<>),O("*",<LX(x),RX(x)>)>)
       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("->",<LX(x),O("1",<>)>),O("->",<O("*",<LX(x),LX(RX(x))>),RX(RX(x))>)>)
       else x;

;--------------------------------------------------------------------
;
; SETS Rewrite System functionality
;

rrInfo <- [];

rrReif <- [       1 -> O("*",<'A,'B>),
                  2 -> O("*",<'A,O("*",<'B,'C>)>),
                  3 -> O("*",<O("*",<'A,'B>),'C>),
                  4 -> O("*",<'A,O("1",<>)>),
                  5 -> 'A,
                  6 -> O("+",<'A,'B>),
                  7 -> O("+",<'A,O("+",<'B,'C>)>),
                  8 -> O("+",<O("+",<'A,'B>),'C>),
                  9 -> O("+",<'A,O("0",<>)>),
                  10 -> 'A,
                  11 -> O("*",<'A,O("0",<>)>),
                  12 -> O("*",<'A,O("+",<'B,'C>)>),
                  13 -> O("+",<O("*",<'A,'B>),O("*",<'A,'C>)>),
                  14 -> O("^",<'A,O("0",<>)>),
                  15 -> O("^",<'A,O("+",<'B,'C>)>),
                  16 -> O("+",<O("^",<'A,'B>),O("^",<'A,'C>)>),
                  17 -> O("^",<'A,O("1",<>)>),
                  18 -> 'A,
                  19 -> O("^",<O("1",<>),'A>),
                  20 -> O("^",<O("*",<'B,'C>),'A>),
                  21 -> O("*",<O("^",<'B,'A>),O("^",<'C,'A>)>),
                  22 -> O("^",<'C,O("*",<'A,'B>)>),
                  23 -> O("^",<O("^",<'C,'B>),'A>),
                  24 -> O("->",<'A,'B>),
                  25 -> O("^",<O("+",<'B,O("1",<>)>),'A>),
                  26 -> O("->",<O("+",<'B,'C>),'A>),
                  27 -> O("*",<O("->",<'B,'A>),O("->",<'C,'A>)>),
                  28 -> O("->",<O("0",<>),'A>),
                  29 -> O("->",<'A,O("1",<>)>),
                  30 -> O("^",<O("2",<>),'A>),
                  31 -> O("->",<O("1",<>),'A>),
                  32 -> O("+",<'A,O("1",<>)>),
; Inequacional
                  33 -> O("->",<'A,O("*",<'B,'C>)>),
                  34 -> O("->",<O("*",<'A,'B>),'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]),"abs1","rep1"),
                  2 -> RInf(rrReif[2],RR2(rrReif[2]),"abs2?","rep2?"),
                  3 -> RInf(rrReif[3],RR3(rrReif[3]),"abs3?","rep3?"),
                  4 -> RInf(rrReif[4],RR4(rrReif[4]),"abs4?","rep4?"),
                  5 -> RInf(rrReif[5],RR5(rrReif[5]),"abs5?","rep5?"),
                  6 -> RInf(rrReif[6],RR6(rrReif[6]),"abs6?","rep6?"),
                  7 -> RInf(rrReif[7],RR7(rrReif[7]),"abs7?","rep7?"),
                  8 -> RInf(rrReif[8],RR8(rrReif[8]),"abs8?","rep8?"),
                  9 -> RInf(rrReif[9],RR9(rrReif[9]),"abs9?","rep9"),
                  10 -> RInf(rrReif[10],RR10(rrReif[10]),"abs10?","rep10?"),
                  11 -> RInf(rrReif[11],RR11(rrReif[11]),"abs11?","rep11?"),
                  12 -> RInf(rrReif[12],RR12(rrReif[12]),"abs12?","rep12?"),
                  13 -> RInf(rrReif[13],RR13(rrReif[13]),"abs13?","rep13?"),
                  14 -> RInf(rrReif[14],RR14(rrReif[14]),"abs14?","rep14?"),
                  15 -> RInf(rrReif[15],RR15(rrReif[15]),"abs15?","rep15?"),
                  16 -> RInf(rrReif[16],RR16(rrReif[16]),"abs16?","rep16?"),
                  17 -> RInf(rrReif[17],RR17(rrReif[17]),"abs17?","rep17?"),
                  18 -> RInf(rrReif[18],RR18(rrReif[18]),"abs18?","rep18?"),
                  19 -> RInf(rrReif[19],RR19(rrReif[19]),"abs19?","rep19?"),
                  20 -> RInf(rrReif[20],RR20(rrReif[20]),"abs20?","rep20?"),
                  21 -> RInf(rrReif[21],RR21(rrReif[21]),"abs21?","rep21?"),
                  22 -> RInf(rrReif[22],RR22(rrReif[22]),"abs22","rep22"),
                  23 -> RInf(rrReif[23],RR23(rrReif[23]),"abs23","rep23"),
                  24 -> RInf(rrReif[24],RR24(rrReif[24]),"abs24?","rep24?"),
                  25 -> RInf(rrReif[25],RR25(rrReif[25]),"abs25?","rep25?"),
                  26 -> RInf(rrReif[26],RR26(rrReif[26]),"abs26?","rep26?"),
                  27 -> RInf(rrReif[27],RR27(rrReif[27]),"abs27?","rep27?"),
                  28 -> RInf(rrReif[28],RR28(rrReif[28]),"abs28?","rep28?"),
                  29 -> RInf(rrReif[29],RR29(rrReif[29]),"abs29","rep29"),
                  30 -> RInf(rrReif[30],RR30(rrReif[30]),"abs30?","rep30"),
                  31 -> RInf(rrReif[31],RR31(rrReif[31]),"abs31?","rep31?"),
                  32 -> RInf(rrReif[32],RR32(rrReif[32]),"abs31?","rep32?"),
; Inequacional
                  33 -> RInf(rrReif[33],RR33(rrReif[33]),"abs33","rep33"),
                  34 -> RInf(rrReif[34],RR34(rrReif[34]),"abs34","rep34"),
                  35 -> RInf(rrReif[35],RR35(rrReif[35]),"abs35","rep35"),
                  36 -> RInf(rrReif[36],RR36(rrReif[36]),"abs36","rep36"),
                  37 -> RInf(rrReif[37],RR37(rrReif[37]),"abs37","rep37"),
                  38 -> RInf(rrReif[38],RR38(rrReif[38]),"abs38","rep38"),
                  39 -> RInf(rrReif[39],RR39(rrReif[39]),"abs39","rep39")];

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(<xSets(l),xSets(r)>),
                   o == "+"  -> if xPlusOrio(x)
                                then Plus(xFlatOrio(x))
                                else Plus(<xSets(l),xSets(r)>),
                   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 <x>
       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) ^ <o> ^ xAbs2Str(r);

;
; Abstraction function TeX string
;
FUNC xAbs2TeX(x:X):STR-list
RETURN if isC(x) || is-V(x) || is-F(x) then <x>
       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) ^ <o> ^ 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,<xAbsFun(l),"id">))
                    otherwise (O(o,<xAbsFun(l),xAbsFun(r)>)));

;
; 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,<xAbsFun(l),xAbsFun(r)>));

;
; 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),<a,RX(x1)>),
                xAbsMatch(a,RX(x1),x2) == a -> O(OX(x1),<LX(x1),a>))
            otherwise (O(OX(x1),<xAbsMatch(a,LX(x1),x2),xAbsMatch(a,RX(x1),x2)>))
       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),<r,RX(x1)>),
                xRepMatch(r,RX(x1),x2) == r -> O(OX(x1),<LX(x1),r>))
            otherwise (O(OX(x1),<xRepMatch(r,LX(x1),x2),xRepMatch(r,RX(x1),x2)>))
       else x1;

;
; Sets to X-Expression format
;
FUNC Sets2X(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("^",<Sets2X(A(e)),Sets2X(B(e))>)
       else if is-List(e) then O("->",<'N,Sets2X(A(e))>)
;List(SetsSubst(A(e),s))
       else if is-Ffun(e) then O("->",<Sets2X(A(e)),Sets2X(B(e))>)
       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 Sets2X(h)
            else if length(l) == 2
                 then O("*",<Sets2X(h),Sets2X(nth(2,l))>)
                 else O("*",<Sets2X(h),ProdBinary(t)>);

PlusBinary(l) = 
    if l == <> then 'error
    else let (h = head(l), t = tail(l))
         in if length(l) == 1
            then Sets2X(h)
            else if length(l) == 2
                 then O("+",<Sets2X(h),Sets2X(nth(2,l))>)
                 else O("+",<Sets2X(h),PlusBinary(t)>);

;
; 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) ^
                                              <" + "> ^
                                              _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("^",<O("2",<>),'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),<erMetaMatch(LX(x1)),'_er_>))
            otherwise (O(OX(x1),<erMetaMatch(LX(x1)),erMetaMatch(RX(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),<ffMetaMatch(LX(x1)),'_ff_>))
            otherwise (O(OX(x1),<ffMetaMatch(LX(x1)),ffMetaMatch(RX(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),<fdMetaMatch(LX(x1)),'_fd_>))
            otherwise (O(OX(x1),<fdMetaMatch(LX(x1)),fdMetaMatch(RX(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);


;--------------------------------------------------------------------
; RSC-REPOSITORY                                               ART/97
;--------------------------------------------------------------------
;                  Copyright@1996 by F. Luis Neves
;
; Author(s):       FLN (F. Luis Neves)
; Revisions:       25.Fev.97 Rev: 22 Mar, 1997
;                            Rev: 24 Mar, 1997
;                            Rev:  3 Jan, 1998 (Final revisions)
;
;--------------------------------------------------------------------
;
;
; Comments: Automatic Reification Tool (SETS)
;

;
; Total reification: with all rules available
;
FUNC rfSTART(x:X,t:INT,n:INT)
PRE is-X(x)
STATE progn(gpSETTINGS(P(9,50,0,25,60,10,false,1,true,1,39)),
            gpSHOWSETTINGS(),rrINIT(),
            gpSTART(),rfEVAL(x,t),
            princ("> Best(",0,"): ",rfBESTVAL(),"\n> thinking..."),
            foreach(i,inseg(n),
                    rfSELECT(),gpCROSSOVER(),gpMUTATION(),rfEVAL(x,t),
                    princ(" best (",i,"): ",rfBESTVAL(),"\n> thinking...")),
;                    rfSHOWBEST(x));
;                    rfSHOWREIF(x));
                    rfSHOWRESULT(x));

;
; Partial reification: only with rules applied to finite functions
;
FUNC rfPSTART(x:X,t:INT,n:INT)
PRE is-X(x)
;STATE progn(gpSETTINGS(P(5,20,0,25,60,0,false,1,true,1,39)),
STATE progn(gpSETTINGS(P(10,50,3,50,60,1,false,2,true,2,39)),
            gpSHOWSETTINGS(),rrINIT(),
            gpPSTART({24,26,28,29,30,31,33,34,35,36,37,38,39}),rfEVAL(x,t),
            princ("> Best(",0,"): ",rfBESTVAL(),"%\n> thinking..."),
            foreach(i,inseg(n),
                    rfSELECT(),gpCROSSOVER(),gpMUTATION(),rfEVAL(x,t),
                    princ(" best (",i,"): ",rfBESTVAL(),"%\n> thinking...")),
;                    rfSHOWBEST(x));
;                    rfSHOWREIF(x));
                    rfSHOWRESULT(x));

FUNC rfPSTARTBAMS(x:X,t:INT,n:INT)
PRE is-X(x)
;STATE progn(gpSETTINGS(P(15,30,0,25,60,1,false,3,true,1,39)),
;STATE progn(gpSETTINGS(P(15,50,0,50,60,1,false,2,true,1,39)),
;STATE progn(gpSETTINGS(P(5,50,3,50,60,10,false,2,true,1,39)),
STATE progn(gpSETTINGS(P(10,50,3,50,60,1,false,2,true,2,39)),
            gpSHOWSETTINGS(),rrINIT(),
            gpPSTART({1,4,12,13,24,25,26,28,29,30,31,33,34,35,36,37,38,39}),
            rfEVAL(x,t),
            princ("> Best(",0,"): ",rfBESTVAL(),"%\n> thinking..."),
            foreach(i,inseg(n),
                    gpSELECT(),gpCROSSOVER(),gpMUTATION(),rfEVAL(x,t),
                    princ(" best (",i,"): ",rfBESTVAL(),"%\n> thinking...")),
;                    rfSHOWBEST(x));
;                   rfSHOWREIF(x));
                   rfSHOWRESULT(x));

FUNC rfPSTARTPPD(x:X,t:INT,n:INT)
PRE is-X(x)
;STATE progn(gpSETTINGS(P(25,30,0,25,60,0,false,1,true,1,39)),
;STATE progn(gpSETTINGS(P(15,50,0,25,60,1,false,2,true,1,39)),
STATE progn(gpSETTINGS(P(10,50,3,50,60,1,false,2,true,2,39)),
            gpSHOWSETTINGS(),rrINIT(),
            gpPSTART({1,4,12,13,24,25,26,28,29,30,31,33,34,35,36,37,38,39}),
            rfEVAL(x,t),
            princ("> Best(",0,"): ",rfBESTVAL(),"%\n> thinking..."),
            foreach(i,inseg(n),
                    gpSELECT(),gpCROSSOVER(),gpMUTATION(),rfEVAL(x,t),
                    princ(" best (",i,"): ",rfBESTVAL(),"%\n> thinking...")),
;                    rfSHOWBEST(x));
;                   rfSHOWREIF(x));
                   rfSHOWRESULT(x));


FUNC rfSELECT()
STATE let (p = roleta(G,rfBEST()))
      in if (card(dom(p)) < card(dom(G)))
         then G <- _fullsel_(p,G)
         else G <- p;

_fullsel_(p,s) = if (geq(card(dom(p)),card(dom(s)))) then p
                 else let (x = rchoice(dom(s)), k = choice(dom(s)-dom(p)))
                      in _fullsel_(p + [ k->s[x] ],s);

FUNC rfBEST():I->R
RETURN [ k -> G[k] | k <- dom(G) : gpSEL(k,2) == rfBESTVAL() ];

FUNC rfBESTVAL():INT
PRE not(gpEMPTY())
RETURN max-orio(0,{ gpSEL(x,2) | x <- dom(G) });

FUNC rfBESTOFALL():I->R
RETURN [ k -> G[k] | k <- dom(G)
                   : gpSEL(k,2) == rfBESTVAL() &&
                     gpSEL(k,3) == min-orio(CS(GV),{gpSEL(x,3) | x <- dom(G)})];

FUNC rfPOPRULES():INT-set
RETURN elems(CONC(< B1(G[x]) | x <- dom(G) >));

FUNC rfSHOWBEST(x:X)
RETURN let (b = rfBESTOFALL(), k = choice(dom(b)))
       in xPrint(ApplyFirstMatch(x,B1(b[k])));

FUNC rfPREPARE(s:STR)
RETURN x <- Sets2X(FLATSETS(s,M)[s]);

FUNC rfSHOWREIF(x:X)
RETURN let (b = rfBEST(), k = choice(dom(b)), c = B1(b[k]))
       in if (GR(GV) == 2)
          then _showreif_(x,CONC(c))
          else _showreif_(x,c);

_showreif_(x,c) =
    if (c == <>) then ""
;   else let (h = head(c), t = tail(c), r = FirstMatchInv(x,h))
    else let (h = head(c), t = tail(c), r = FirstMatch(x,h),
              i = xAbsMatch(rrGetAbs(h),x,rrGetPat(h)),
              j = xRepMatch(rrGetRep(h),x,rrGetPat(h)))
         in if is-X(r)
            then progn(if (x != r)
                       then princ("\n> applying ",h,"... ",xString(r),
                                  "\n> abs = ",xAbs2Str(xAbsFun(i)),
                                  "\n> rep = ",xAbs2Str(xRepFun(j))),
                       _showreif_(r,t))
            else progn(princ("\n> applying ",h,"... ",xString(E(r)),
                             "\n> ... invariant: ",I(r)),
                       _showreif_(E(r),t));

FUNC rfSAVEREIF(x:X,f:STR)
RETURN let (b = rfBEST(), k = choice(dom(b)), c = B1(b[k]))
       in do(fp <- fopen("_","w"),
             if (GR(GV) == 2)
             then _savereif_(x,CONC(c))
             else _savereif_(x,c),
             sh("mv _ " ++ f));

_savereif_(x,c) =
    if (c == <>) then ""
;   else let (h = head(c), t = tail(c), r = FirstMatchInv(x,h))
    else let (h = head(c), t = tail(c), r = FirstMatch(x,h),
              i = xAbsMatch(rrGetAbs(h),x,rrGetPat(h)),
              j = xRepMatch(rrGetRep(h),x,rrGetPat(h)))
         in progn(if (x != r)
                  then do (fprint("_","a",<"\n\n> applying ",h,"... ">),
                           fprint("_","a",xString(r)),
                           fprint("_","a",<"\n\n> abs = ">),
                           fprint("_","a",xAbs2Str(xAbsFun(i))),
                           fprint("_","a",<"\n> rep = ">),
                           fprint("_","a",xAbs2Str(xRepFun(j)))),
                  _savereif_(r,t));

FUNC rfTEXREIF(x:X)
RETURN let (b = rfBEST(), k = choice(dom(b)), c = B1(b[k]))
       in do(fp <- fopen("_","w"),
             fprint("_","a",<"\\documentstyle{article}\n">),
             fprint("_","a",<"\\begin{document}\n">),
             fprint("_","a",<"\\section*{Data Reification}\n">),
             fprint("_","a",<"\\footnotesize{\n">),
             fprint("_","a",<"\n\\begin{eqnarray*}\n">),
             fprint("_","a",<" & & ">),
             fprint("_","a",SETS2TEX(xSets(x))),
             fprint("_","a",<"\\\\\n">),
;             fprint("_","a",<"\\\\">),
             if (GR(GV) == 2)
             then _texreif_(x,CONC(c))
             else _texreif_(x,c),
             fprint("_","a",<"\n\\end{eqnarray*}\n">),
             fprint("_","a",<"}\n\\end{document}\n">),
             sh("mv _ _reif_.tex"));
;,fclose(fp));

_texreif_(x,c) = 
    if (c == <>) then ""
;   else let (h = head(c), t = tail(c), r = FirstMatchInv(x,h))
    else let (h = head(c), t = tail(c), r = FirstMatch(x,h),
              i = xAbsMatch(rrGetAbs(h),x,rrGetPat(h)),
              j = xRepMatch(rrGetRep(h),x,rrGetPat(h)))
         in if (x != r)
            then progn(fprint("_","a",<"\n">),
;                      fprint("_","a",SETS2TEX(xSets(x))),
                       if h in inseg(32)
                       then fprint("_","a",<" & \\cong_{",h,"} & ">)
                       else fprint("_","a",<" & \\unlhd_{",h,"} & ">),
                       fprint("_","a",SETS2TEX(xSets(r))),
                       fprint("_","a",<"\\\\">),
                       fprint("_","a",<"\n & & > abs = ">),
                       fprint("_","a",xAbs2TeX(xAbsFun(i))),
                       fprint("_","a",<"\\\\">),
                       fprint("_","a",<"\n & & > rep = ">),
                       fprint("_","a",xAbs2TeX(xRepFun(j))),
                       fprint("_","a",<"\\\\">),
                       fprint("_","a",<"\n">),
                       fprint("_","a",<"\\\\">),
                       _texreif_(r,t))
            else _texreif_(r,t);

FUNC rfSHOWRESULT(x:X)
RETURN let (b = rfBEST(), k = choice(dom(b)), c = B1(b[k]))
;       in xString(erApplyFinalRule(ApplyFirstMatch(x,c)));
       in if (GR(GV) == 2)
          then xString(ApplyFirstMatch(x,CONC(c)))
          else xString(ApplyFirstMatch(x,c));

;
; Evaluation function (t = evaluation type)
; t = 1 => ER_MODEL
; t = 2 => ER_MODELSIZE
; t = 3 => FF_MODEL
; t = 4 => FF_MODELSIZE
; t = 5 => RSC_MODEL
; t = 6 => RSC_MODELSIZE
;
FUNC rfEVAL(x:X,t:INT)
STATE G <- rcprob(_reify_(x,t,G));

_reify_(e,t,s) = if (s == []) then []
                 else let (x = choice(dom(s)),
                           cx = gpSEL(x,1),
                           rx = if (GR(GV) == 2) then CONC(cx) else cx,
                           fx = rfEVALSETS(ApplyFirstMatch(e,rx),t),
                           sx = gpSEL(x,3))
                      in [ x -> R(cx,fx,sx,0,0) ] + _reify_(e,t,s\{x});

;
; Evaluates models in SETS (t = evaluation type)
; t = 1 => ER_MODEL
; t = 2 => ER_MODELSIZE
; t = 3 => FF_MODEL
; t = 4 => FF_MODELSIZE
; t = 5 => RSC_MODEL
; t = 6 => RSC_MODELSIZE
;
FUNC rfEVALSETS(x:X,t:INT):INT
RETURN if (t == 1 -> ER_EVAL(x),
           t == 2 -> ER_EVALSIZE(x),
           t == 3 -> FF_EVAL(x),
           t == 4 -> FF_EVALSIZE(x),
           t == 5 -> RSC_EVAL(x),
           t == 6 -> RSC_EVALSIZE(x))
;          t == 3 -> -1.*RSC_EVAL(x))
       otherwise(RSC_EVAL(x));

;
; Relational Model Evaluation function (ER_EVAL: X -> [0..10])
;
FUNC ER_EVAL(x:X):INT
RETURN erDegreeMatch(erApplyMetaMatch(x));

;
; Relational Model Evaluation function (ER_EVALSIZE: X -> [0..10])
; (size is important)
;
FUNC ER_EVALSIZE(x:X):INT
RETURN let (r = erApplyMetaMatch(x))
       in pdiv(erDegreeMatch(r),xComplex(r))./100;

;
; Relational Model Evaluation function (FF_EVAL: X -> [0..10])
;
FUNC FF_EVAL(x:X):INT
RETURN ffDegreeMatch(ffApplyMetaMatch(x));

;
; Relational Model Evaluation function (FF_EVALSIZE: X -> [0..10])
; (size is important)
;
FUNC FF_EVALSIZE(x:X):INT
RETURN let (r = ffApplyMetaMatch(x))
       in pdiv(ffDegreeMatch(r),xComplex(r))./100;

;
; Reusable Software Component Evaluation function (RSC_EVAL: X -> [0..10])
;
FUNC RSC_EVAL(x:X):INT
RETURN rscDegreeMatch(ffApplyMetaMatch(erApplyMetaMatch(x)));

;
; Reusable Software Component Evaluation function (RSC_EVAL: X -> [0..10])
; (size is important)
;
FUNC RSC_EVALSIZE(x:X):INT
RETURN let (r = ffApplyMetaMatch(erApplyMetaMatch(x)))
       in pdiv(rscDegreeMatch(r),xComplex(r))./100;


;fName <- "ppd.cam";
;fName <- "bams.cam";
;sName <- "BAMS";

FUNC rfERSTART(x:X,n:INT):Void
PRE is-X(x)
;STATE progn(gpSETTINGS(P(15,30,0,25,60,1,false,3,true,1,39)),
;STATE progn(gpSETTINGS(P(15,50,0,50,60,1,false,2,true,1,39)),
STATE progn(gpSETTINGS(P(5,50,3,50,60,1,false,2,true,2,39)),
            gpSHOWSETTINGS(),rrINIT(),
            gpPSTART({1,4,12,13,24,25,26,28,29,30,31,33,34,35,36,37,38,39}),
            rfEVAL(x,1),
            princ("> Best(",0,"): ",rfBESTVAL(),"%\n> thinking..."),
            foreach(i,inseg(n),
                    gpSELECT(),gpCROSSOVER(),gpMUTATION(),rfEVAL(x,1),
                    princ(" best (",i,"): ",rfBESTVAL(),"%\n> thinking...")),
                    rfSHOWRESULT(x));

CAM2SETS(fName);
rfPREPARE(choice(dom(M)));
rfERSTART(x,5);
rfSAVEREIF(x,"_.reif");
rfTEXREIF(x);
sh("mv _reif_.tex " ++ fName ++ ".reif.tex");
sh("latex " ++ fName ++ ".reif.tex");