114 lines
3.4 KiB
Text
114 lines
3.4 KiB
Text
data Exp where
|
|
EVar : Char -> Exp
|
|
EAbs : Pair Char Type -> Exp -> Exp
|
|
EApp : Exp -> Exp -> Exp
|
|
EInt : Int -> Exp
|
|
EAdd : Exp -> Exp -> Exp
|
|
|
|
data Type where
|
|
TLit : Char -> Type
|
|
TArr : Type -> Type -> Type
|
|
|
|
data Maybe a where
|
|
Nothing : Maybe a
|
|
Just : a -> Maybe a
|
|
|
|
data Ctx where
|
|
Ctx : List (Pair Char Type) -> Ctx
|
|
|
|
data Tri a b c where
|
|
Tri : a -> b -> c -> Tri a b c
|
|
|
|
lookupVar : Char -> Ctx -> Maybe Type
|
|
lookupVar c ctx = case ctx of
|
|
Ctx ls => case ls of
|
|
Nil => Nothing
|
|
Cons a as => case a of
|
|
Pair name type => case (asciiCode name) == (asciiCode c) of
|
|
True => Just type
|
|
_ => lookupVar c (Ctx as)
|
|
|
|
insertVar : Char -> Type -> Ctx -> Ctx
|
|
insertVar c t ctx = case ctx of
|
|
Ctx ls => Ctx (Cons (Pair c t) ls)
|
|
|
|
infer : Ctx -> Exp -> Maybe (Pair Type Ctx)
|
|
infer ctx e = case ctx of
|
|
Ctx ls => case e of
|
|
EVar c => case lookupVar c ctx of
|
|
Nothing => Nothing
|
|
Just t => Just (Pair t ctx)
|
|
EAbs pair e => case pair of
|
|
Pair name targ =>
|
|
let newCtx = insertVar name targ ctx
|
|
in case infer newCtx e of
|
|
Nothing => Nothing
|
|
Just p => case p of
|
|
Pair tret newCtx => Just (Pair (TArr targ tret) newCtx)
|
|
EApp e1 e2 => case infer ctx e1 of
|
|
Just p => case p of
|
|
Pair t ctx => case t of
|
|
TArr t1 t2 => case infer ctx e2 of
|
|
Just p => case p of
|
|
Pair t ctx => case eq t1 t of
|
|
True => Just (Pair t2 ctx)
|
|
_ => Nothing
|
|
Nothing => Nothing
|
|
_ => Nothing
|
|
Nothing => Nothing
|
|
EInt i => Just (Pair (TLit 'i') ctx)
|
|
EAdd e1 e2 =>
|
|
case infer ctx e1 of
|
|
Just p => case p of
|
|
Pair t ctx => case eq t (TLit 'i') of
|
|
True => case infer ctx e2 of
|
|
Just p => case p of
|
|
Pair t ctx => case eq t (TLit 'i') of
|
|
True => Just (Pair (TLit 'i') ctx)
|
|
_ => Nothing
|
|
_ => Nothing
|
|
_ => Nothing
|
|
_ => Nothing
|
|
|
|
eq : Type -> Type -> Bool
|
|
eq t1 t2 = case t1 of
|
|
TArr left1 right1 => case t2 of
|
|
TArr left2 right2 => (eq left1 left2) && (eq right1 right2)
|
|
_ => False
|
|
TLit l1 => case t2 of
|
|
TLit l2 => (asciiCode l1) == (asciiCode l2)
|
|
_ => False
|
|
|
|
|
|
|
|
.&& l r = case l of
|
|
True => r
|
|
_ => False
|
|
|
|
.++ : List a -> List a -> List a
|
|
.++ xs ys = case xs of
|
|
Nil => ys
|
|
Cons a as => Cons a (as ++ ys)
|
|
|
|
emptyCtx = Ctx Nil
|
|
|
|
expression = (EApp
|
|
(EAbs (Pair 'a' (TLit 'i'))
|
|
(EAbs (Pair 'x' (TArr (TLit 'a') (TLit 'b')))
|
|
(EVar 'x')))
|
|
(EInt 100))
|
|
|
|
-- (\a : int . (\x : (a -> b) . x)) 100
|
|
-- should infer the type (a -> b) -> (a -> b), which it does
|
|
|
|
pretty : Type -> List Char
|
|
pretty t = case t of
|
|
TLit t => Cons t Nil
|
|
TArr t1 t2 => Cons '(' ((pretty t1) ++ (" -> ") ++ (pretty t2) ++ (Cons ')' Nil))
|
|
|
|
getType c e = case infer c e of
|
|
Nothing => printStr "fail"
|
|
Just p => case p of
|
|
Pair t e => printStr (pretty t)
|
|
|
|
main = getType emptyCtx expression
|