module Rules where import Rewriting {- -------------------- -- if true x y = x if false x y = y -- NOTE: using variables below to abbreviate later cases does NOT work! and true true = true and true false = false and false true = false and false false = false or true true = true or true false = true or false true = true or false false = false gt zero x = false gt (suck x) zero = true gt (suck x) (suck y) = gt x y plus zero m = m plus (suck n) m = plus n (suck m) mult zero m = zero mult (suck n) m = plus m (mult n m) square x = mult x x one = suck zero two = suck one three = suck two omega = suck omega -- NOTE: using omega on the left of comparisons loops under left/normal! fib zero = zero fib one = one fib (suck (suck n)) = plus (fib (suck n)) (fib n) -} -------------------- -- Shorthands for constants and variables -------------------- uc n x = App (Con n) [x] bc n x y = App (Con n) [x,y] tc f a b c = App (Con f) [a,b,c] [true,false,zero,one,two,three,omega] = map con ["true","false","zero","one","two","three","omega"] [suck,square,fib] = map uc ["1+","square","fib"] [und,orr,plus,mult,gt,eq,twice] = map bc ["and","or","plus","mult","gt","eq","twice"] [iff,fiba] = map tc ["if","fiba"] [x,y,n,m,a,b,p,q] = map var ["x","y","n","m","a","b","p","q"] -------------------- -- Some sample rules -------------------- rules = Rules [ (lhs,rhs), -- twice rule (iff true x y, x), (iff false x y, y), (und true true, true), (und true false, false), (und false true, false), (und false false, false), (orr true true, true), (orr true false, true), (orr false true, true), (orr false false, false), (gt zero x, false), (gt (suck x) zero, true), (gt (suck x) (suck y), gt x y), (eq zero zero, true), (eq (suck x) zero, false), (eq zero (suck y), false), (eq (suck x) (suck y), eq x y), (plus zero m, m), (plus (suck n) m, plus n (suck m)), (mult zero m, zero), (mult (suck n) m, plus m (mult n m)), (square x, mult x x), (one, suck zero), (two, suck one), (three, suck two), (omega, suck omega), (fib zero, zero), (fib (suck zero), one), (fib (suck (suck n)), plus (fib (suck n)) (fib n)), (fiba p q zero, p), (fiba p q (suck zero), q), (fiba p q (suck n), fiba q (plus p q) n) ] try = run 100 rules -------------------- -- Some sample terms -------------------- top = iff (gt (mult two two) three) a b top1 = iff (eq (mult two two) (plus one three)) a b top2 = plus two (iff (orr (gt omega (mult two two)) (gt (plus two three) omega)) a b) tsq = App (Con "twice") [con "square", con "two"] ttsq = App (Con "twice") [con "twice", con "square", con "two"] fib5 = fib (suck (suck (suck (suck (suck zero))))) fib8 = fib (suck (suck (suck (suck (suck (suck (suck (suck zero)))))))) fiba8 = fiba zero one (suck (suck (suck (suck (suck (suck (suck (suck zero)))))))) num 0 = zero num n = suck (num (n-1)) fibb n = fib (num n) fibab n = fiba zero one (num n) compare n = (test fibb, test fibab) where test f = length (calc rules (f n)) runLong term = putStr (showCalc (term : (calc rules term))) -------------------- -- More samples (from development & testing) -------------------- rules1 = Rules [(lhs,rhs)] lhs = App (Con "twice") [var "f", var "x"] rhs = App (Var "f") [App (Var "f") [var "x"]] test = App (Con "twice") [con "twice", con "twice", var "f", var "x"] li = App (Con "h") [var "x"] ri = App (Con "f") [App (Con "h") [var "x"]] inf = Rules [(li,ri)] deep = App (Con "g") [App (Con "h") [App (Con "f") [var "y"]]] args (App f ts) = ts sev = App (Con "f") [App (Con "g") [var "x", var "y"], var "x", App (Con "h") [var "y", var "x"], App (Var "x") [var "x"]] simp = subst [("x", App (Var "f") [var "z"])] fxy = App (Con "f") [var "x", var "y"] -- half is for testing Maybe utilities half n = let (d,m) = n `divMod` 2 in if m ==0 then Just d else Nothing