module Lambda
( Exp (Var, Lambda, App, Pair, Pi1, Pi2, Inl, Inr, Caseof, Unit, Abort, Absurd)
, simplifyAll
, simplifySteps
, showReduction
, usestypecons
, isOpenExp
)
where
import Format
data Exp = Var Integer
| Lambda Exp
| App Exp Exp
| Pair Exp Exp
| Pi1 Exp
| Pi2 Exp
| Inl Exp
| Inr Exp
| Caseof Exp Exp Exp
| Unit
| Abort Exp
| Absurd Exp
deriving (Eq, Ord)
instance Show Exp where
show = showexp
showexp :: Exp -> String
showexp (Var n) = show n
showexp (Lambda e) = "λ" ++ showexp e ++ ""
showexp (App f g) = "(" ++ showexp f ++ " " ++ showexp g ++ ")"
showexp (Pair a b) = "(" ++ showexp a ++ "," ++ showexp b ++ ")"
showexp (Pi1 m) = "(" ++ "FST " ++ showexp m ++ ")"
showexp (Pi2 m) = "(" ++ "SND " ++ showexp m ++ ")"
showexp (Inl m) = "(" ++ "INL " ++ showexp m ++ ")"
showexp (Inr m) = "(" ++ "INR " ++ showexp m ++ ")"
showexp (Caseof m n p) = "(" ++ "CASE " ++ showexp m ++ " OF " ++ showexp n ++ "; " ++ showexp p ++ ")"
showexp Unit = "*"
showexp (Abort a) = "(ABORT " ++ showexp a ++ ")"
showexp (Absurd a) = "(ABSURD " ++ showexp a ++ ")"
showReduction :: Exp -> String
showReduction (Lambda e) = "λ" ++ showReduction e
showReduction (App (Lambda f) x) = betaColor (App (Lambda f) x)
showReduction (Var e) = show e
showReduction (App rs x) = "(" ++ showReduction rs ++ " " ++ showReduction x ++ ")"
showReduction e = show e
betaColor :: Exp -> String
betaColor (App (Lambda e) x) =
"(" ++
formatSubs1 ++ "λ" ++ formatFormula ++
indexColor 1 e ++
" " ++
formatSubs2 ++ showexp x ++ formatFormula
++ ")"
betaColor e = show e
indexColor :: Integer -> Exp -> String
indexColor n (Lambda e) = "λ" ++ indexColor (succ n) e
indexColor n (App f g) = "(" ++ indexColor n f ++ " " ++ indexColor n g ++ ")"
indexColor n (Var m)
| n == m = formatSubs1 ++ show m ++ formatFormula
| otherwise = show m
indexColor _ e = show e
simplifyAll :: Exp -> Exp
simplifyAll = last . simplifySteps
simplifySteps :: Exp -> [Exp]
simplifySteps e
| e == s = [e]
| otherwise = e : simplifySteps s
where s = simplify e
simplify :: Exp -> Exp
simplify (Lambda e) = Lambda (simplify e)
simplify (App (Lambda f) x) = betared (App (Lambda f) x)
simplify (App (Var e) x) = App (Var e) (simplify x)
simplify (App (App f g) x) = App (simplify (App f g)) (simplify x)
simplify (App a b) = App (simplify a) (simplify b)
simplify (Var e) = Var e
simplify (Pair a b) = Pair (simplify a) (simplify b)
simplify (Pi1 (Pair a _)) = a
simplify (Pi1 m) = Pi1 (simplify m)
simplify (Pi2 (Pair _ b)) = b
simplify (Pi2 m) = Pi2 (simplify m)
simplify (Inl m) = Inl (simplify m)
simplify (Inr m) = Inr (simplify m)
simplify (Caseof (Inl m) a _) = App a m
simplify (Caseof (Inr m) _ b) = App b m
simplify (Caseof a b c) = Caseof (simplify a) (simplify b) (simplify c)
simplify Unit = Unit
simplify (Abort a) = Abort (simplify a)
simplify (Absurd a) = Absurd (simplify a)
betared :: Exp -> Exp
betared (App (Lambda e) x) = substitute 1 x e
betared e = e
substitute :: Integer
-> Exp
-> Exp
-> Exp
substitute n x (Lambda e) = Lambda (substitute (succ n) (incrementFreeVars 0 x) e)
substitute n x (App f g) = App (substitute n x f) (substitute n x g)
substitute n x (Pair a b) = Pair (substitute n x a) (substitute n x b)
substitute n x (Pi1 a) = Pi1 (substitute n x a)
substitute n x (Pi2 a) = Pi2 (substitute n x a)
substitute n x (Inl a) = Inl (substitute n x a)
substitute n x (Inr a) = Inr (substitute n x a)
substitute n x (Caseof a b c) = Caseof (substitute n x a) (substitute n x b) (substitute n x c)
substitute _ _ Unit = Unit
substitute n x (Abort a) = Abort (substitute n x a)
substitute n x (Absurd a) = Absurd (substitute n x a)
substitute n x (Var m)
| n == m = x
| n < m = Var (m-1)
| otherwise = Var m
incrementFreeVars :: Integer -> Exp -> Exp
incrementFreeVars n (App f g) = App (incrementFreeVars n f) (incrementFreeVars n g)
incrementFreeVars n (Lambda e) = Lambda (incrementFreeVars (succ n) e)
incrementFreeVars n (Var m)
| m > n = Var (succ m)
| otherwise = Var m
incrementFreeVars n (Pair a b) = Pair (incrementFreeVars n a) (incrementFreeVars n b)
incrementFreeVars n (Pi1 a) = Pi1 (incrementFreeVars n a)
incrementFreeVars n (Pi2 a) = Pi2 (incrementFreeVars n a)
incrementFreeVars n (Inl a) = Inl (incrementFreeVars n a)
incrementFreeVars n (Inr a) = Inr (incrementFreeVars n a)
incrementFreeVars n (Caseof a b c) = Caseof (incrementFreeVars n a) (incrementFreeVars n b) (incrementFreeVars n c)
incrementFreeVars _ Unit = Unit
incrementFreeVars n (Abort a) = Abort (incrementFreeVars n a)
incrementFreeVars n (Absurd a) = Absurd (incrementFreeVars n a)
usestypecons :: Exp -> Bool
usestypecons (Var _) = False
usestypecons (App a b) = usestypecons a || usestypecons b
usestypecons (Lambda b) = usestypecons b
usestypecons _ = True
isOpenExp :: Exp -> Bool
isOpenExp (Var n) = n == 0
isOpenExp (App a b) = isOpenExp a || isOpenExp b
isOpenExp (Lambda a) = isOpenExp a
isOpenExp (Pair a b) = isOpenExp a || isOpenExp b
isOpenExp (Pi1 a) = isOpenExp a
isOpenExp (Pi2 a) = isOpenExp a
isOpenExp (Inl a) = isOpenExp a
isOpenExp (Inr a) = isOpenExp a
isOpenExp (Caseof a b c) = isOpenExp a || isOpenExp b || isOpenExp c
isOpenExp Unit = False
isOpenExp (Abort a) = isOpenExp a
isOpenExp (Absurd a) = isOpenExp a