;--------------------------------------------------------------------
; 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:
;
;--------------------------------------------------------------------
;

( deftype S EQ X )
;---------------------
;C = INT;

( deftype V SYM )
;---------------------

( deftype F STR )
;---------------------
;X = C | V | F | O;

( deftype X ALT V F O )
;---------------------
;O = OX:STR LX:X RX:X;

( deftype O TUP
  ( OX STR )
  ( AX LIST X )
)
;---------------------
;--------------------------------------------------------------------
; Auxiliary functions

( def LX lambda
  ( o )
  ( p1
    ( AX o )
  )
)
;---------------------

( def RX lambda
  ( o )
  ( p2
    ( AX o )
  )
)
;---------------------

( def isC lambda
  ( x )
  ( and
    ( is O x )
    ( equal
      ( AX x )
      ( makeseq )
    )
  )
)
;---------------------
;
; x/y (x,y reals and result x 100)
;

( def pdiv lambda
  ( x y )
  ( mul x
    ( div 100 y )
  )
)
;---------------------
;
; Number of variables
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xVar )
        ( quote
          (
            (
              ( X )
            )
            ( INT )
          )
        )
      )
    )
  )
)
;---------------------

( def xVar lambda
  ( x )
  ( cond
    (
      ( isC x ) 0
    )
    (
      ( is V x ) 1
    )
    (
      ( is O x )
      ( intSUM
        ( seq
          ( xVar a )
          ( from a
            ( AX x )
          )
        )
      )
    )
    ( true 0 )
  )
)
;---------------------
;
; Number of constants
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xCon )
        ( quote
          (
            (
              ( X )
            )
            ( INT )
          )
        )
      )
    )
  )
)
;---------------------

( def xCon lambda
  ( x )
  ( cond
    (
      ( isC x ) 1
    )
    (
      ( is V x ) 0
    )
    (
      ( is O x )
      ( intSUM
        ( seq
          ( xCon a )
          ( from a
            ( AX x )
          )
        )
      )
    )
    ( true 0 )
  )
)
;---------------------
;
; Number of operators 
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xOpr )
        ( quote
          (
            (
              ( X )
            )
            ( INT )
          )
        )
      )
    )
  )
)
;---------------------

( def xOpr lambda
  ( x )
  ( cond
    (
      ( isC x ) 0
    )
    (
      ( is V x ) 0
    )
    (
      ( is O x )
      ( add 1
        ( intSUM
          ( seq
            ( xOpr a )
            ( from a
              ( AX x )
            )
          )
        )
      )
    )
    ( true 0 )
  )
)
;---------------------
;
; Number of meta-symbols ('_xx_,'_er_,'_ff_,...) 
;
;           isC(x) -> 0,
;           is-V(x) -> 0,

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xMetaSym )
        ( quote
          (
            (
              ( X )
            )
            ( INT )
          )
        )
      )
    )
  )
)
;---------------------

( def xMetaSym lambda
  ( x )
  ( cond
    (
      ( equal x '_xx_ ) 1
    )
    (
      ( equal x '_er_ ) 1
    )
    (
      ( equal x '_ff_ ) 1
    )
    (
      ( equal x '_fd_ ) 1
    )
    (
      ( is O x )
      ( intSUM
        ( seq
          ( xMetaSym a )
          ( from a
            ( AX x )
          )
        )
      )
    )
    ( true 0 )
  )
)
;---------------------
;
; Expression complexity
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xComplex )
        ( quote
          (
            (
              ( X )
            )
            ( INT )
          )
        )
      )
    )
  )
)
;---------------------

( def xComplex lambda
  ( x )
  ( cond
    (
      ( is V x ) 1
    )
    (
      ( isC x ) 1
    )
    (
      ( is O x )
      ( add 1
        ( intSUM
          ( seq
            ( xComplex a )
            ( from a
              ( AX x )
            )
          )
        )
      )
    )
    ( true 100 )
  )
)
;---------------------
;
; Expression print
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xPrint )
        ( quote
          (
            (
              ( X )
            )
            ( Void )
          )
        )
      )
    )
  )
)
;---------------------

( def xPrint lambda
  ( x )
  ( cond
    (
      ( isC x )
      ( princ
        ( OX x )
      )
    )
    (
      ( is V x )
      ( princ x )
    )
    (
      ( is O x )
      ( let
        (
          ( o
            ( OX x )
          )
          ( a
            ( AX x )
          )
        )
        ( progn
          ( princ o "(" )
          ( foreach a
            ( AX x )
            ( xPrint a )
          )
          ( princ ")" )
        )
      )
    )
  )
)
;---------------------
;
; Expression string
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xString )
        ( quote
          (
            (
              ( X )
            )
            ( LIST STR )
          )
        )
      )
    )
  )
)
;---------------------

( def xString lambda
  ( x )
  ( cond
    (
      ( isC x )
      ( makeseq
        ( OX x )
      )
    )
    (
      ( is V x )
      ( makeseq
        ( symstr x )
      )
    )
    (
      ( is F x )
      ( makeseq x )
    )
    (
      ( is O x )
      ( let
        (
          ( o
            ( OX x )
          )
          ( a
            ( AX x )
          )
        )
        ( xInfix o a )
      )
    )
    ( true
      ( makeseq )
    )
  )
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xInfix )
        ( quote
          (
            (
              ( STR )
              ( LIST X )
            )
            ( LIST STR )
          )
        )
      )
    )
  )
)
;---------------------

( def xInfix lambda
  ( o a )
  ( if
    ( equal a
      ( makeseq )
    )
    ( makeseq )
    ( let
      (
        ( h
          ( hd a )
        )
        ( t
          ( tl a )
        )
      )
      ( if
        ( equal t
          ( makeseq )
        )
        ( append
          ( append
            ( makeseq o "(" )
            ( xString h )
          )
          ( makeseq ")" )
        )
        ( append
          ( append
            ( append
              ( makeseq "(" )
              ( xString h )
            )
            ( CONC
              ( seq
                ( append
                  ( makeseq o )
                  ( xString x )
                )
                ( from x t )
              )
            )
          )
          ( makeseq ")" )
        )
      )
    )
  )
)
;---------------------
;
; Expression TeX string
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xTeX )
        ( quote
          (
            (
              ( X )
            )
            ( LIST STR )
          )
        )
      )
    )
  )
)
;---------------------

( def xTeX lambda
  ( x )
  ( cond
    (
      ( isC x )
      ( makeseq
        ( OX x )
      )
    )
    (
      ( is V x )
      ( makeseq
        ( symstr x )
      )
    )
    (
      ( is F x )
      ( makeseq x )
    )
    (
      ( is O x )
      ( let
        (
          ( o
            ( OX x )
          )
          ( a
            ( AX x )
          )
        )
        ( xTeXInfix o a )
      )
    )
    ( true
      ( makeseq )
    )
  )
)
;---------------------

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xTeXInfix )
        ( quote
          (
            (
              ( STR )
              ( LIST X )
            )
            ( LIST STR )
          )
        )
      )
    )
  )
)
;---------------------

( def xTeXInfix lambda
  ( o a )
  ( if
    ( equal a
      ( makeseq )
    )
    ( makeseq )
    ( let
      (
        ( h
          ( hd a )
        )
        ( t
          ( tl a )
        )
        ( s
          ( cond
            (
              ( equal o "*" ) " \\times "
            )
            (
              ( equal o "^" ) "^"
            )
            (
              ( equal o "+" ) " + "
            )
            (
              ( equal o "->" ) " \\hookrightarrow "
            )
          )
        )
      )
      ( if
        ( equal t
          ( makeseq )
        )
        ( append
          ( append
            ( makeseq s "{(" )
            ( xTeX h )
          )
          ( makeseq ")}" )
        )
        ( append
          ( append
            ( append
              ( makeseq "{(" )
              ( xTeX h )
            )
            ( CONC
              ( seq
                ( append
                  ( makeseq s )
                  ( xTeX x )
                )
                ( from x t )
              )
            )
          )
          ( makeseq ")}" )
        )
      )
    )
  )
)
;---------------------
;
; Expression subterms which does not match a given template x2
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xNotMatch )
        ( quote
          (
            ( ANY
              ( X )
            )
            ( INT )
          )
        )
      )
    )
  )
)
;---------------------

( def xNotMatch lambda
  ( x1 x2 )
  ( cond
    (
      ( isC x2 )
      ( if
        ( isC x1 ) 1 0
      )
    )
    (
      ( is V x2 )
      ( if
        ( is V x1 ) 1 0
      )
    )
    (
      ( is O x2 )
      ( if
        ( is O x1 )
        ( if
          ( xMatch x1 x2 )
          ( intSUM
            ( seq
              ( xNotMatch a x2 )
              ( from a
                ( AX x1 )
              )
            )
          )
          ( add 1
            ( intSUM
              ( seq
                ( xNotMatch a x2 )
                ( from a
                  ( AX x1 )
                )
              )
            )
          )
        ) 0
      )
    )
    ( true 0 )
  )
)
;---------------------
;
; Expression match - x2 is the template
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xMatch )
        ( quote
          (
            ( ANY
              ( X )
            )
            ( SYM )
          )
        )
      )
    )
  )
)
;---------------------

( def xMatch lambda
  ( x1 x2 )
  ( cond
    (
      ( and
        ( isC x1 )
        ( isC x2 )
      )
      ( equal x1 x2 )
    )
    (
      ( is V x2 ) true
    )
    (
      ( is F x1 ) true
    )
    (
      ( and
        ( is O x1 )
        ( is O x2 )
      )
      ( let
        (
          ( o1
            ( OX x1 )
          )
          ( o2
            ( OX x2 )
          )
          ( a1
            ( AX x1 )
          )
          ( a2
            ( AX x2 )
          )
        )
        ( and
          ( equal o1 o2 )
          ( _xMatch_ a1 a2 )
        )
      )
    )
    ( true false )
  )
)
;---------------------

( def _xMatch_ lambda
  ( a1 a2 )
  ( cond
    (
      ( and
        ( equal a1
          ( makeseq )
        )
        ( equal a2
          ( makeseq )
        )
      ) true
    )
    (
      ( and
        ( nequal a1
          ( makeseq )
        )
        ( equal a2
          ( makeseq )
        )
      ) false
    )
    (
      ( and
        ( equal a1
          ( makeseq )
        )
        ( nequal a2
          ( makeseq )
        )
      ) false
    )
    ( true
      ( let
        (
          ( h1
            ( hd a1 )
          )
          ( h2
            ( hd a2 )
          )
          ( t1
            ( tl a1 )
          )
          ( t2
            ( tl a2 )
          )
        )
        ( and
          ( xMatch h1 h2 )
          ( _xMatch_ t1 t2 )
        )
      )
    )
  )
)
;---------------------
;
; Expression first match (is there any match?) - x2 is the template
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xFirstMatch )
        ( quote
          (
            ( ANY
              ( X )
            )
            ( SYM )
          )
        )
      )
    )
  )
)
;---------------------

( def xFirstMatch lambda
  ( x1 x2 )
  ( if
    ( xMatch x1 x2 ) true
    ( if
      ( is O x1 )
      ( reduce false or
        ( seq
          ( xFirstMatch x x2 )
          ( from x
            ( AX x1 )
          )
        )
      ) false
    )
  )
)
;---------------------
;
; Expression near match
;
;           _xNearMatch2_(x1,x2,39) -> 25)

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xNearMatch )
        ( quote
          (
            ( ANY
              ( X )
            )
            ( INT )
          )
        )
      )
    )
  )
)
;---------------------

( def xNearMatch lambda
  ( x1 x2 )
  ( cond
    (
      ( xMatch x1 x2 ) 100
    )
    (
      ( _xNearMatch1_ x1 x2 33 39 ) 50
    )
    (
      ( _xNearMatch1_ x2 x1 33 39 ) 50
    )
    ( true 0 )
  )
)
;---------------------

( def _xNearMatch1_ lambda
  ( x1 x2 i j )
  ( if
    ( gt i j ) false
    ( if
      ( xMatch
        ( FirstMatch x1 i ) x2
      ) true
      ( _xNearMatch1_ x1 x2
        ( add i 1 ) j
      )
    )
  )
)
;---------------------
;
; pouco eficiente...
;

( def _xNearMatch2_ lambda
  ( x1 x2 k )
  ( let
    (
      ( m
        ( set
          ( xMatch
            ( FirstMatch x0 i )
            ( FirstMatch x2 j )
          )
          ( from i
            ( inseg k )
          )
          ( from j
            ( inseg k )
          )
        )
      )
    )
    ( if
      ( member 'true m ) true false
    )
  )
)
;---------------------
;
; If xFirstMatch replaces the expression match with '_xx_
; x2 is the template
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xMetaMatch )
        ( quote
          (
            ( ANY
              ( X )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def xMetaMatch lambda
  ( x1 x2 )
  ( if
    ( xMatch x1 x2 ) '_xx_
    ( if
      ( is O x1 )
      ( let
        (
          ( o
            ( OX x1 )
          )
          ( a
            ( AX x1 )
          )
        )
        ( O o
          ( _xMetaMatch_ a x2 )
        )
      ) 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;

( def _xMetaMatch_ lambda
  ( a1 x2 )
  ( if
    ( equal a1
      ( makeseq )
    )
    ( makeseq )
    ( let
      (
        ( h
          ( hd a1 )
        )
        ( t
          ( tl a1 )
        )
      )
      ( if
        ( equal h '_xx_ )
        ( cons h
          ( _xMetaMatch_ t x2 )
        )
        ( cons
          ( xMetaMatch h x2 )
          ( _xMetaMatch_ t x2 )
        )
      )
    )
  )
)
;---------------------
;
; Degree of match
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote xDegreeMatch )
        ( quote
          (
            ( ANY
              ( X )
            )
            ( INT )
          )
        )
      )
    )
  )
)
;---------------------

( def xDegreeMatch lambda
  ( x1 x2 )
  ( cond
    (
      ( xMatch x1 x2 ) 100
    )
    (
      ( xFirstMatch x1 x2 )
      ( div 100
        ( xComplex
          ( xMetaMatch x1 x2 )
        )
      )
    )
    ( true 0 )
  )
)
;---------------------
;--------------------------------------------------------------------
;
; Rewrite functions
;
;--------------------------------------------------------------------
;
;
; Root Match: applies the rule (if possible) to the root only
;
; Inequacional

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote RootMatch )
        ( quote
          (
            (
              ( X )
              ( INT )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

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

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote FirstMatch )
        ( quote
          (
            (
              ( X )
              ( INT )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def FirstMatch lambda
  ( x i )
  ( if
    ( or
      ( isC x )
      ( is V x )
    )
    ( RootMatch x i )
    ( let
      (
        ( x1
          ( RootMatch x i )
        )
      )
      ( if
        ( nequal x x1 ) x1
        ( let
          (
            ( o
              ( OX x )
            )
            ( a
              ( AX x )
            )
          )
          ( O o
            ( _FirstMatch_ a i )
          )
        )
      )
    )
  )
)
;---------------------

( def _FirstMatch_ lambda
  ( a i )
  ( if
    ( equal a
      ( makeseq )
    )
    ( makeseq )
    ( let
      (
        ( h
          ( hd a )
        )
        ( t
          ( tl a )
        )
        ( r
          ( FirstMatch h i )
        )
      )
      ( if
        ( nequal h r )
        ( cons r t )
        ( cons h
          ( _FirstMatch_ t i )
        )
      )
    )
  )
)
;---------------------
;
; Applies a list of Root Match rules
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote ApplyRootMatch )
        ( quote
          (
            (
              ( X )
              ( LIST INT )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def ApplyRootMatch lambda
  ( x l )
  ( if
    ( equal l
      ( makeseq )
    ) x
    ( let
      (
        ( h
          ( head l )
        )
        ( t
          ( tail l )
        )
        ( r
          ( RootMatch x h )
        )
      )
      ( ApplyRootMatch r t )
    )
  )
)
;---------------------
;
; Applies a list of FirstMatch rules
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote ApplyFirstMatch )
        ( quote
          (
            (
              ( X )
              ( LIST INT )
            )
            ( X )
          )
        )
      )
    )
  )
)
;---------------------

( def ApplyFirstMatch lambda
  ( x l )
  ( if
    ( equal l
      ( makeseq )
    ) x
    ( let
      (
        ( h
          ( head l )
        )
        ( t
          ( tail l )
        )
        ( r
          ( FirstMatch x h )
        )
      )
      ( ApplyFirstMatch r t )
    )
  )
)
;---------------------