module CN(Term, Lam, App, Var, Bet, Rep, beta, app, subst, lift, 
	  unrep, cbv, cbn) 

where

data Term = Var Integer | App Term Term | Lam Term | Rep Term | Bet Term
	    deriving Eq

showterm (Var n)   = show n
showterm (App r s) = "(" ++ show r ++ " " ++ show s ++ ")"
showterm (Lam r)   = "(L " ++ showterm r ++ ")"
showterm (Rep r)   = "(R " ++ showterm r ++ ")"
showterm (Bet r)   = "(B " ++ showterm r ++ ")"

instance Show Term where show = showterm

lift :: Term -> Integer -> Term
lift (Var k)   n = Var (k + if k < n then 0 else 1)
lift (App r s) n = App (lift r n) (lift s n)
lift (Lam r)   n = Lam (lift r (n + 1))
lift (Rep r)   n = Rep (lift r n)
lift (Bet r)   n = Bet (lift r n)

subst :: Term -> Term -> Integer -> Term 
subst (Var k)    s n = if k == n then s else (Var (k - if k < n then 0 else 1))
subst (App r r') s n = App (subst r s n) (subst r' s n) 
subst (Lam r)    s n = Lam (subst r (lift s 0) (n + 1))
subst (Rep r)    s n = Rep (subst r s n)
subst (Bet r)    s n = Bet (subst r s n)


beta :: Term -> Term -- in normal form
beta r = app r []

app :: Term -> [Term] -> Term
app (Lam r) (s:l) = Bet (app (subst r s 0) l)
app (Lam r)  []   = Lam (beta r)
app (Rep r)   l   = Rep (app r l)
app (Bet r)   l   = Bet (app r l)
app (Var k)   l   = foldl App (Var k) (map beta l)
app (App r s) l   = Rep (app r (s:l))

-- Some aux functions

unrep :: Term -> Term -- not continuous
unrep (Var k)   = Var k
unrep (App r s) = App (unrep r) (unrep s)
unrep (Lam r)   = Lam (unrep r)
unrep (Rep r)   = unrep r
unrep (Bet r)   = unrep r

cbn :: Term -> Term
cbn (Var k) = Var k
cbn (App r s) = case (cbn r) of
		(Lam r') -> (cbn (subst r' s 0))
		r' -> (r' `App` (cbn s))
cbn (Lam r) = Lam (cbn r)
cbn (Rep r) = Rep (cbn r)

cbv :: Term -> Term
cbv (Var k) = Var k
cbv (App r s) = case (cbv r) of
		(Lam r') -> (cbv (subst r' (cbv s) 0))
		r' -> (r' `App` (cbv s))
cbv (Lam r) = Lam (cbv r)
cbv (Rep r) = Rep (cbv r)