1 {-
    2     Haskell version of ...
    3 
    4 ! rewrite functions for Boyer benchmark 
    5 ! Started by Tony Kitto on 30 March 1988
    6 
    7 ! Changes Log
    8 ! 08-04-88 ADK bug fix  = rewrite(Atom(x),A) returns Atom(x) not Nil
    9 ! 25-05-88 ADK added applysubst to this module and assoclist replaced by LUT
   10 
   11 Haskell version:
   12 
   13     23-06-93 JSM initial version
   14 
   15 -}
   16 
   17 module Rewritefns (applysubst, rewrite) where
   18 
   19 import Lisplikefns
   20 
   21 applysubst :: Lisplist -> Lisplist -> Lisplist
   22 applysubst alist Nil           = Nil
   23 applysubst alist term@(Atom x) = 
   24     case assoc (term, alist) of 
   25         Cons (yh, yt) -> yt
   26         _             -> term
   27 applysubst alist (Cons (x, y)) = Cons (x, applysubstlst alist y)
   28 
   29 applysubstlst :: Lisplist -> Lisplist -> Lisplist
   30 applysubstlst alist Nil           = Nil
   31 applysubstlst alist (Atom x)      = error "Malformed list"
   32 applysubstlst alist (Cons (x, y)) = 
   33     Cons (applysubst alist x, applysubstlst alist y)
   34 
   35 
   36 rewrite :: Lisplist -> LUT -> Lisplist
   37 rewrite Nil term             = Nil
   38 rewrite expr@(Atom x) term   = expr
   39 rewrite (Cons (l1, l2)) term = 
   40     rewritewithlemmas (Cons (l1, rewriteargs l2 term)) 
   41         (getLUT (tv l1, term)) term
   42 
   43 rewriteargs :: Lisplist -> LUT -> Lisplist
   44 rewriteargs Nil term           = Nil
   45 rewriteargs (Atom x) term      = error "Malformed list"
   46 rewriteargs (Cons (x, y)) term = Cons (rewrite x term, rewriteargs y term)
   47 
   48 rewritewithlemmas :: Lisplist -> [Lisplist] -> LUT -> Lisplist
   49 rewritewithlemmas t [] term = t
   50 rewritewithlemmas t (lh:lt) term 
   51     | b = rewrite (applysubst u (caddr lh)) term
   52     | otherwise = rewritewithlemmas t lt term
   53       where (b, u) = onewayunify t (cadr lh)
   54 
   55 
   56 onewayunify :: Lisplist -> Lisplist -> (Bool, Lisplist)
   57 onewayunify t1 t2 = onewayunify1 t1 t2 Nil
   58 
   59 onewayunify1 :: Lisplist -> Lisplist -> Lisplist -> (Bool, Lisplist)
   60 onewayunify1 t1 t2 u | atom t2          = case assoc (t2, u) of
   61                             Cons (x, y) -> (t1 == y, u)
   62                             _           -> (True, Cons (Cons (t2, t1), u))
   63                      | atom t1          = (False, u)
   64                      | car t1 == car t2 = onewayunify1lst (cdr t1) (cdr t2) u
   65                      | otherwise        = (False, u)
   66 
   67 onewayunify1lst :: Lisplist -> Lisplist -> Lisplist -> (Bool, Lisplist)
   68 onewayunify1lst Nil _  u = (True, u)
   69 onewayunify1lst l1  l2 u 
   70     | b = onewayunify1lst (cdr l1) (cdr l2) u1
   71     | otherwise = (False, u1)
   72       where (b, u1) = onewayunify1 (car l1) (car l2) u
   73