import "cn.hs"      -- implementation of continuous normalization
import "cnparse.hs" -- parsing and showing of terms

b = term "L L L . 2 . 1 0"
k = term "L L 1"                           
i = term "L 0"                             
s = term "L L L . 2 0 . 1 0"               
y = term "L . (L . 1 . 0 0) (L . 1 . 0 0)"
t = term "L L . 0 . 1 1 0"
theta = t `App` t                   -- another fixpoint combinator
why r = r `App` (why r)             -- rather infinite fixpoint operator
church n = Lam (Lam (iterate (App (Var 1)) (Var 0) !! n)) -- Church numerals

-- Some examples with Church arithmetic          
   -- compare beta (b `App` (church 2 `App` (Var 0)) `App` (church 3 `App` (Var 0)))
   -- with    beta (b `App` (church 3 `App` (Var 0)) `App` (church 2 `App` (Var 0)))
   -- compare beta (b `App` (church 3) `App` (church 2))
   -- with    beta (b `App` (church 2) `App` (church 3))
   -- try     beta (church 2 `App` (church 3))

skk     = s `App` k `App` k
omega   = term "L . 0 0"            -- Lam (Var 0 `App` (Var 0))
oomega  = omega `App` omega         -- not terminating
omega2  = term "L . 0 0 0"          -- Lam ((Var 0) `App` (Var 0) `App` (Var 0))
oomega2 = omega2 `App` omega2       -- diverging and increasing
la      = la `App` (Var 0)          -- Rep's forever (infinitely left applications)
ra      = (Var 0) `App` ra          -- no Rep's      (infinitely right applications)
tn  n   = foldl App (Var 0) (map Var [1..n]) -- 0 1 .. n