module Exp where
data Exp = App Exp Exp | Lam Exp |
	Zero | Succ Exp | Pred Exp |
	If0 Exp Exp Exp | Fix Exp |
	Var Int

subst :: Exp -> (Int->Exp) -> Exp
subst (Var n) f = f n
subst (App t u) f = App (subst t f) (subst u f)
subst (Lam t) f = Lam (subst t (Var 0 <: f))
subst (Fix t) f = Fix (subst t (Var 0 <: f))
subst Zero f = Zero
subst (Succ t) f = Succ (subst t f)
subst (Pred t) f = Pred (subst t f)
subst (If0 c t e) f = If0 (subst c f) (subst t f) (subst e f)

(<:) :: Exp -> (Int->Exp) -> Int -> Exp
t <: e = aux where aux 0 = t
                   aux n = lift (e(n-1))

lift :: Exp -> Exp
lift t = subst t (Var . (+1))

subst0 :: Exp -> Exp -> Exp
subst0 t u = subst u (t <: (Var . (subtract 1)))

expand :: Exp -> Exp
expand e = App (lift e) (Var 0)

addPCF :: Exp
addPCF = Fix (Lam (Lam (If0 (Var 0) (Var 1) (App(App(Var 2)(Succ(Var 1)))(Pred(Var 0))))))

doublePCF :: Exp
doublePCF = Lam (App(App addPCF (Var 0))(Var 0))

factSchema :: Exp
factSchema = Lam(Lam(Fix(Lam(If0 (Var 0) (Var 2) (App (App (Var 3) (Var 0)) (App (Var 1)(Pred(Var 0))))))))

appPrec :: Int
appPrec = 5

lamPrec :: Int
lamPrec = appPrec - 1

addPrec :: Int
addPrec = appPrec - 2

countSucc (Succ e) = let (k,e') = countSucc e in  (k+1,e')
countSucc e = (0,e)
countPred (Pred e) = let (k,e') = countPred e in  (k+1,e')
countPred e = (0,e)

instance Show Exp where
    showsPrec n e = showAll n 0 (map ((('v':).).showsPrec 0) [1..]) e

showAll _ _ xs (Var n) = xs!!n
showAll n m xs p@(App t u)
	| n<appPrec = showAll lamPrec m xs t . (' ':) . showAll appPrec m xs u
        | otherwise = ('(' :) . showAll 0 m xs p . (')':)
showAll n m xs p@(Lam b)
        | n<lamPrec = let v= ('x':) . showsPrec 0 m
                      in ('\\' :) . v . ('.' :) . showAll 0 (m+1) (v:xs) b
        | otherwise = ('(' :) . showAll 0 m xs p . (')':)
showAll n m xs p@(Fix b)
        | n<lamPrec = let v= ('f':) . showsPrec 0 m
                      in  v . (" = "++) . showAll 0 (m+1) (v:xs) b
        | otherwise = ('(' :) . showAll 0 m xs p . (')':)
showAll n m xs Zero = ('0':)
showAll n m xs p@(Succ e) =
        if n<addPrec then let (k,e')=countSucc e in
                              showAll addPrec m xs e' . ('+':) . showsPrec 0 (k+1)
        else  ('(' :) . showAll 0 m xs p . (')':)
showAll n m xs p@(Pred e) =
        if n<addPrec then let (k,e')=countPred e in
                              showAll addPrec m xs e' . ('-':) . showsPrec 0 (k+1)
        else  ('(' :) . showAll 0 m xs p . (')':)
showAll n m xs (If0 c t e) =
        (" if "++) . showAll 0 m xs c. ("==0 then " ++) . showAll 0 m xs t.
        (" else "++) . showAll n m xs e