module Named where

data Exp = Var String | Lam String Exp | App Exp Exp

instance Show Exp where
    show (Var x) = x
    show (Lam x e) = "(\\"++x++" -> "++(show e)++")"
    show (App e1 e2) = "("++(show e1)++" "++(show e2)++")"

freeVars e = fv [] e where
    fv bvs (Var x) = if x `elem` bvs then [] else [x]
    fv bvs (Lam x e) = fv (x:bvs) e
    fv bvs (App e1 e2) = fv bvs e1 ++ fv bvs e2

subst targ repl e = subs e where
    fvRepl = freeVars repl
    newname newFV x = gen x where 
        gen x = if x' `elem` (fvRepl++newFV) then gen x' else x' 
          where x' = x++"'"
    subs (Var x) = if x == targ then repl else (Var x)
    subs (Lam x e) = 
        if x == targ then (Lam x e) else
        if x `elem` fvRepl then
            let x' = newname (freeVars e) x 
            in subs $ Lam x' $ subst x (Var x') e
        else Lam x (subs e)
    subs (App e1 e2) = App (subs e1) (subs e2)

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

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

x = Var "x"
x' = Var "x'"
y = Var "y"
f = Var "f"
g = Var "g"
m = Var "m"
n = Var "n"
e1 = Lam "x" $ App x y
e2 = Lam "x" $ App x (App y x')
e3 = Lam "x" $ App (App x (App y x')) (Lam "y" $ App y x')
omega = App (Lam "x" $ App x x) (Lam "x" $ App x x) 
k = Lam "x" $ Lam "y" $ x
s = Lam "f" $ Lam "g" $ Lam "x" $ App (App f x) (App g x)
zero = Lam "f" $ Lam "x" $ x
one = Lam "f" $ Lam "x" $ App f x
two = Lam "f" $ Lam "x" $ App f (App f x)
three = Lam "f" $ Lam "x" $ App f (App f (App f x))
four = Lam "f" $ Lam "x" $ App f (App f (App f (App f x)))
plus = Lam "m" $ Lam "n" $ Lam "f" $ Lam "x" $ App (App m f) (App (App n f) x)
times = Lam "m" $ Lam "n" $ Lam "f" $ App m (App n f)

expon = Lam "m" $ Lam "n" $ App m n
exp1 = Lam "m" $ Lam "n" $ Lam "f" $ Lam "x" $ App (App (App m n) f) x
exp2 = Lam "m" $ Lam "n" $ App (App m (App times n)) one
exp2' = Lam "m" $ Lam "n" $ App (App n (App times m)) one