module Debruijn where

data Exp = Var Int | Lam Exp | App Exp Exp

instance Show Exp where
    show e = go (-1) e where
        go n (Var x) = if x <= n then "x"++(show $ n - x) else "c"++(show $ x - n)
        go n (Lam e) = "(\\x"++(show $ n + 1)++" -> "++(go (n + 1) e)++")"
        go n (App e1 e2) = "("++(go n e1)++" "++(go n e2)++")"

subst repl e = go 0 e where
    go n (Var i) = case compare i n of
        EQ -> incr n repl 
        LT -> Var i
        GT -> Var (i - 1)
    go n (Lam e) = Lam $ go (n+1) e
    go n (App e1 e2) = App (go n e1) (go n e2)

incr v e = go 0 e where
    go n (Var i) = Var $ if i >= n then i+v else i
    go n (Lam e) = Lam $ go (n+1) e
    go n (App e1 e2) = App (go n e1) (go n e2)

normalize e = case e of
    Var x -> Var x
    Lam e -> Lam $ normalize e
    App e1 e2 -> case normalize e1 of
        Lam e -> normalize $ subst e2 e
        f -> App f $ normalize e2

----------------------

x0 = Var 0
x1 = Var 1
x2 = Var 2
x3 = Var 3
x4 = Var 4
e1 = Lam $ App x0 x1
e2 = Lam $ App x0 (App x1 x2)
e3 = Lam $ App (App x0 (App x1 x2)) (Lam $ App x0 x3)
omega = App (Lam $ App x0 x0) (Lam $ App x0 x0) 
k = Lam $ Lam $ x1
s = Lam $ Lam $ Lam $ App (App x2 x0) (App x1 x0)
zero = Lam $ Lam $ x0
one = Lam $ Lam $ App x1 x0
two = Lam $ Lam $ App x1 (App x1 x0)
plus = Lam $ Lam $ Lam $ Lam $ App (App x3 x1) (App (App x2 x1) x0)
times = Lam $ Lam $ Lam $ App x2 (App x1 x0)