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