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