import Data.Char as Char import qualified Table import EnvSimple import Parser import Repl import Debug.Trace type Symbol = String data Value = VNum Integer | VCtor Symbol Int [Value] | VRec (Table.T Symbol Value) | VFun Symbol Environment Expr data Type = TInt | TName Symbol [Type] | TFun Type Type | TVar (Table.T Symbol [Type]) | TRec (Table.T Symbol Type) deriving Eq data Expr = EId Symbol | ENum Integer | EPlus Expr Expr | ETimes Expr Expr | EFun Symbol Type Expr | EApp Expr Expr | ELet Symbol Type Expr Expr | ERecord [(Symbol, Expr)] | EMember Expr Symbol | ETypeVar Symbol [Symbol] [(Symbol, [Type])] Expr | ETypeRec Symbol [Symbol] [(Symbol, Type)] Expr | ETypeDef Symbol [Symbol] Type Expr | ECase Expr [(Pattern, Expr)] deriving Eq data Pattern = ElsePat | VarPat Symbol | CtorPat Symbol [Symbol] | NumPat Integer deriving Eq type Environment = Env Value -- evaluation eval :: Environment -> Expr -> Value eval env (ENum n) = VNum n eval env (EFun arg _ body) = VFun arg env body eval env (EId id) = lookup_variable env id eval env (EPlus e1 e2) = case (eval env e1, eval env e2) of (VNum x1, VNum x2) -> VNum (x1 + x2) _ -> error "addition of non-numbers" eval env (ETimes e1 e2) = case (eval env e1, eval env e2) of (VNum x1, VNum x2) -> VNum (x1 * x2) _ -> error "multiplication of non-numbers" eval env (EApp f a) = let val = eval env a in case eval env f of VFun p e b -> eval (bind_variable e p val) b VCtor ctor 0 args -> error "constructor applied to too many arguments" VCtor ctor ar args -> VCtor ctor (ar-1) (args ++ [val]) _ -> error "application of non-function" eval env (ERecord fields) = VRec (Table.map (\f e -> eval env e) (Table.of_list fields)) eval env (EMember e f) = case eval env e of VRec fields -> Table.lookup fields f _ -> error "not a record" eval env (ELet x _ e b) = eval new_env b where new_env = bind_variable env x v v = eval new_env e eval env (ETypeVar _ _ ctors e) = eval new_env e where new_env = foldl (\env (c,args) -> bind_variable env c (VCtor c (length args) [])) env ctors eval env (ETypeRec _ _ _ e) = eval env e eval env (ETypeDef _ _ _ e) = eval env e eval env (ECase e pats) = iter pats where val = eval env e iter [] = error "no matching pattern in case expression" iter ((ElsePat, e):ps) = eval env e iter ((VarPat x, e):ps) = case maybe_lookup_variable env x of -- check whether x is a constructor or a variable Nothing -> eval (bind_variable env x val) e Just (VCtor c 0 []) -> case val of VCtor d 0 [] | c == d -> eval env e _ -> iter ps iter ((NumPat n, e):ps) = case val of VNum k | n == k -> eval env e _ -> iter ps iter ((CtorPat c xs,e):ps) = case val of VCtor d 0 args | c == d && length xs == length args -> eval (foldl (\env (x,a) -> bind_variable env x a) env (zip xs args)) e _ -> iter ps -- data structures for type information type TypeDefs = Table.T Symbol Type type Declarations = Table.T Symbol Type type TypeSubst = Table.T Symbol Type data Types = TY TypeDefs TypeSubst Int -- type definitions, variable values, number of used variables new_type_info defs = TY defs Table.empty 0 lookup_type :: Types -> Symbol -> Type lookup_type (TY defs _ _) name = Table.lookup defs name maybe_lookup_type :: Types -> Symbol -> Maybe Type maybe_lookup_type (TY defs _ _) name = Table.maybe_lookup defs name define_type :: Types -> Symbol -> Type -> Types define_type (TY defs vars n) name typ = TY (Table.bind defs name typ) vars n lookup_type_variable :: Types -> Symbol -> Type lookup_type_variable (TY _ vars _) name = iter (Table.lookup vars name) where iter (TName n []) = case Table.maybe_lookup vars n of Just t -> iter t Nothing -> TName n [] iter typ = typ maybe_lookup_type_variable :: Types -> Symbol -> Maybe Type maybe_lookup_type_variable (TY _ vars _) name = iter (Table.maybe_lookup vars name) where iter Nothing = Nothing iter (Just (TName n [])) = case Table.maybe_lookup vars n of Just t -> iter (Just t) Nothing -> Just (TName n []) iter (Just typ) = Just typ is_variable :: Types -> Symbol -> Bool is_variable (TY defs _ _) n = case Table.maybe_lookup defs n of Just _ -> False Nothing -> True set_variable :: Types -> Symbol -> Type -> Types set_variable (TY defs vars n) name typ = TY defs (Table.bind vars name typ) n new_variable :: Types -> (Symbol, Types) new_variable (TY defs vars n) = ("a[" ++ show n ++ "]", TY defs vars (n+1)) -- utility functions for types uncurry_type :: Type -> ([Type], Type) uncurry_type (TFun a b) = let (arg_types, ret_type) = uncurry_type b in (a:arg_types, ret_type) uncurry_type a = ([], a) expand_type_variable :: Types -> Type -> Type expand_type_variable types (TName n []) = case maybe_lookup_type_variable types n of Nothing -> TName n [] Just _ -> expand_type_variable types (lookup_type_variable types n) expand_type_variable _ typ = typ expand_type :: Types -> Type -> Type expand_type types TInt = TInt expand_type types (TName n []) = case maybe_lookup_type_variable types n of Nothing -> TName n [] Just _ -> expand_type types (lookup_type_variable types n) expand_type types (TName n args) = TName n (map (expand_type types) args) expand_type types (TFun a b) = TFun (expand_type types a) (expand_type types b) expand_type types (TVar vars) = TVar (Table.map (\ _ args -> map (expand_type types) args) vars) expand_type types (TRec fields) = TRec (Table.map (\_ t -> expand_type types t) fields) -- type checking type_check types decl expr = type_check_step types decl expr -- trace ("## type checking " ++ show expr ++ "\n") $ -- let (typ, new_types) = type_check_step types decl expr in -- (trace ("## type of " ++ show expr ++ " is " ++ show (expand_type types typ) -- ++ " [" ++ pp_type types typ ++ "]") $ -- (typ, new_types)) type_check :: Types -> TypeDefs -> Expr -> Type type_check_step types decl (ENum n) = TInt type_check_step types decl (EId id) = Table.lookup decl id type_check_step types decl (EFun x t body) = let ret_typ = type_check types (Table.bind decl x t) body in TFun t ret_typ type_check_step types decl (EPlus e1 e2) = let et1 = type_check types decl e1 in let et2 = type_check types decl e2 in if et1 == TInt && et2 == TInt then TInt else error "type error" type_check_step types decl (ETimes e1 e2) = let et1 = type_check types decl e1 in let et2 = type_check types decl e2 in if et1 == TInt && et2 == TInt then TInt else error "type error" type_check_step types decl (EApp f a) = case type_check types decl f of TFun pt rt -> let at = type_check types decl a in if at == pt then rt else error "type error" _ -> error "type error" type_check_step types decl (ELet x t e b) = let x_type = expand_type types t in let new_decl = Table.bind decl x x_type in let et = type_check types new_decl e in if et == x_type then let x_type2 = expand_type types x_type in let new_decl2 = Table.bind decl x x_type2 in type_check types new_decl2 b else error "type error" type_check_step types decl (ERecord fields) = let field_types = foldl (\table (f,e) -> Table.bind table f (type_check types decl e)) Table.empty fields in TRec field_types type_check_step types decl (EMember e f) = case type_check types decl e of TRec fields -> Table.lookup fields f _ -> error "type error" type_check_step types decl (ETypeVar name params variants e) = let ctors = foldl (\table (c,args) -> Table.bind table c args) Table.empty variants in let typ = TVar ctors in let new_types = define_type types name typ in let new_decl = foldl (\decl (c,args) -> Table.bind decl c (foldr (\t a -> TFun a t) typ args)) Table.empty variants in type_check new_types new_decl e type_check_step types decl (ETypeRec name params fields e) = let field_types = foldl (\table (f,t) -> Table.bind table f t) Table.empty fields in let new_types = define_type types name (TRec field_types) in type_check new_types decl e type_check_step types decl (ETypeDef name params t e) = let new_types = define_type types name t in type_check new_types decl e type_check_step types decl (ECase e pats) = let typ = type_check types decl e in let pat_types = foldl (\pt p -> let ptyp = check_pat types typ p in ptyp : pt) [] pats in case pat_types of [] -> error "malformed case statement" (p:ps) -> if foldl (\ok pat -> ok && p == pat) True ps then p else error "type error" where check_pat types typ (g, b) = let (new_types, new_decl) = check_guard types typ g in type_check new_types new_decl b check_guard types typ ElsePat = (types, decl) check_guard types typ (NumPat n) = if typ == TInt then (types, decl) else error "type error" check_guard types typ (VarPat x) = case Table.maybe_lookup decl x of -- check whether x is a constructor or a variable Nothing -> (types, Table.bind decl x typ) Just ct -> let (arg_typ, ret_typ) = uncurry_type ct in case arg_typ of [] -> if typ == ret_typ then (types, decl) else error "type error" _ -> error "type error" check_guard types typ (CtorPat c xs) = let ct = Table.lookup decl c in let (arg_typ, ret_typ) = uncurry_type ct in if typ == ret_typ then if length xs == length arg_typ then let new_decl = foldl (\decl (x,t) -> Table.bind decl x t) decl (zip xs arg_typ) in (types, new_decl) else error "type error" else error "type error" desugar :: PExpr -> Expr desugar (PId id) = EId id desugar (PNum n) = ENum n desugar (PPlus e1 e2) = EPlus (desugar e1) (desugar e2) desugar (PTimes e1 e2) = ETimes (desugar e1) (desugar e2) desugar (PMinus e1 e2) = EPlus (desugar e1) (ETimes (ENum (-1)) (desugar e2)) desugar (PEqual e1 e2) = ECase (desugar (PMinus e1 e2)) [ (NumPat 0, EId "%True"), (ElsePat, EId "%False") ] desugar (PFun [] b) = EFun "()" (TName "unit" []) (desugar b) desugar (PFun [(p,Just t)] b) = EFun p (desugar_type t) (desugar b) desugar (PFun ((p,Just t):args) b) = EFun p (desugar_type t) (desugar (PFun args b)) desugar (PApp f []) = EApp (desugar f) (EId "()") desugar (PApp f [a]) = EApp (desugar f) (desugar a) desugar (PApp f args) = foldl (\f a -> EApp f a ) (desugar f) (map desugar args) desugar (PRecord fields) = ERecord (map (\(f,e) -> (f, desugar e)) fields) desugar (PMember e f) = EMember (desugar e) f desugar (PDecl (PLet x (Just t) e) b) = ELet x (desugar_type t) (desugar e) (desugar b) desugar (PDecl (PLetFun f args (Just t) b) e) = ELet f (desugar_type ft) (desugar (PFun args b)) (desugar e) where ft = foldr (\a b -> (PArrow a b)) t (map (\(_, Just t) -> t) args) desugar (PDecl (PTypeVar name params ctors) e) = ETypeVar name params (map (\(c,args) -> (c, map desugar_type args)) ctors) (desugar e) desugar (PDecl (PTypeRec name params fields) e) = ETypeRec name params (map (\(f,t) -> (f, desugar_type t)) fields) (desugar e) desugar (PDecl (PTypeDef t params t2) e) = ETypeDef t params (desugar_type t2) (desugar e) desugar (PIf c t e) = ECase (desugar c) [ (VarPat "%True", desugar t), (ElsePat, desugar e) ] desugar (PCase e pats) = ECase (desugar e) (map (\(p,e) -> (desugar_pat p, desugar e)) pats) desugar (PListLit es t) = foldr (\x y -> (EApp (EApp (EId "%Cons") (desugar x)) y)) (case t of Nothing -> EId "%Nil" Just e -> desugar e) es desugar _ = error "unsupported syntactic construct" desugar_pat :: PPattern -> Pattern desugar_pat PElsePat = ElsePat desugar_pat (PVarPat x) = VarPat x desugar_pat (PCtorPat c xs) = CtorPat c xs desugar_pat (PNumPat n) = NumPat n desugar_type :: PExpr -> Type desugar_type (PId "int") = TInt desugar_type (PId n) = TName n [] desugar_type (PApp (PId n) args) = TName n (map desugar_type args) desugar_type (PArrow a b) = TFun (desugar_type a) (desugar_type b) desugar_type _ = error "invalid type annotation" show_list :: String -> String -> (a -> String) -> [a] -> String show_list l r sh [] = "" show_list l r sh xs = l ++ foldl1 (\ x y -> x ++ ", " ++ y) (map sh xs) ++ r show_list_acc :: String -> String -> (b -> a -> (String, b)) -> b -> [a] -> (String, b) show_list_acc l r sh acc [] = ("", acc) show_list_acc l r sh acc (x:xs) = let (str,new_acc) = foldl (\(str,acc) y -> let (s,a) = sh acc y in (str ++ ", " ++ s, a)) (sh acc x) xs in (l ++ str ++ r, new_acc) instance Show Value where show (VNum n) = show n show (VCtor c _ args) = c ++ show_list "(" ")" show args show (VRec fields) = show_list "[" "]" (\(f,v) -> f ++ " = " ++ show v) (Table.to_list fields) show (VFun a _ b) = "fun (" ++ a ++ ") { " ++ show b ++ " }" -- pp_type types typ = fst (pretty_print_type Table.empty (expand_type types typ)) pretty_print_type :: Table.T Symbol String -> Type -> (String, Table.T Symbol String) pretty_print_type names TInt = ("int", names) pretty_print_type names (TName n []) = case n of ('a' : '[' : _) -> case Table.maybe_lookup names n of Just str -> (str, names) Nothing -> let used = Table.size names in let str = if used < 26 then [Char.chr (97 + used)] else if used < 26 * 26 then [Char.chr (97 + used `div` 26), Char.chr (97 + used `mod` 26)] else [Char.chr (97 + used `div` 26), Char.chr (97 + used `mod` 26)] ++ show (used `div` (26 * 26)) in (str, Table.bind names n str) _ -> (n, names) pretty_print_type names (TName n args) = let (str, new_names) = show_list_acc "(" ")" pretty_print_type names args in (n ++ str, new_names) pretty_print_type names (TFun a b) = let (str1, names1) = pretty_print_type names a in let (str2, names2) = pretty_print_type names1 b in ("(" ++ str1 ++ " -> " ++ str2 ++ ")", names2) pretty_print_type names (TVar vars) = foldl (\(str,names) (c,fields) -> let (str, new_names) = show_list_acc "(" ")" pretty_print_type names fields in (str ++ "| " ++ c, new_names)) ("", names) (Table.to_list vars) pretty_print_type names (TRec fields) = show_list_acc "[" "]" (\names (f,t) -> let (str, new_names) = pretty_print_type names t in (f ++ " : " ++ str, new_names)) names (Table.to_list fields) instance Show Type where show TInt = "int" show (TName n []) = n show (TName n args) = n ++ show_list "(" ")" show args show (TFun a b) = "(" ++ show a ++ " -> " ++ show b ++ ")" show (TVar vars) = foldl (\str (c,fields) -> str ++ "| " ++ c ++ show_list "(" ")" show fields) "" (Table.to_list vars) show (TRec fields) = show_list "[" "]" (\(f,t) -> f ++ " : " ++ show t) (Table.to_list fields) instance Show Expr where show (EId x) = x show (ENum n) = show n show (EPlus e1 e2) = "(" ++ show e1 ++ " + " ++ show e2 ++ ")" show (ETimes e1 e2) = "(" ++ show e1 ++ " * " ++ show e2 ++ ")" show (EFun a t b) = "fun (" ++ a ++ " : " ++ show t ++ ") { " ++ show b ++ " }" show (EApp f a) = show fn ++ show_list "(" ")" show args where (fn, args) = collect_args f [a] collect_args (EApp g b) args = collect_args g (b:args) collect_args g args = (g, args) show (ERecord fields) = show_list "[" "]" (\(f,e) -> f ++ " = " ++ show e) fields show (EMember e f) = show e ++ "." ++ f show (ELet x t b e) = "let " ++ x ++ " :" ++ show t ++ " = " ++ show b ++ "; " ++ show e show (ECase e pats) = foldl (++) ("case " ++ show e) (map (\(p,e) -> " | " ++ show p ++ " => " ++ show e) pats) show (ETypeVar n ps ctors e) = foldl (++) ("type " ++ n ++ show_list "(" ")" id ps ++ " =") (map (\(c,args) -> " | " ++ c ++ show_list "(" ")" show args) ctors) ++ "; " ++ show e show (ETypeRec n ps fields e) = "type " ++ n ++ show_list "(" ")" id ps ++ " = {" ++ show_list "(" ")" (\(c,t) -> c ++ " : " ++ show t) fields ++ "}; " ++ show e show (ETypeDef n ps t e) = "type " ++ n ++ show_list "(" ")" id ps ++ " = " ++ show t ++ "; " ++ show e instance Show Pattern where show ElsePat = "else" show (VarPat x) = x show (NumPat n) = show n show (CtorPat c xs) = c ++ show_list "(" ")" id xs -- for debugging -- -- show_table tab = -- Table.fold -- (\key val str -> str ++ key ++ " = " ++ show val ++ "\n") -- "" -- tab -- -- instance Show Types where -- show (TY defs vars n) = -- "defs:\n" ++ show_table defs ++ "\nvars: " ++ show_table vars ++ "num: " ++ show n type_unit = TName "unit" [] type_bool = TName "bool" [] type_unit_def = TVar Table.empty type_bool_def = TVar (Table.bind (Table.bind Table.empty "True" []) "False" []) builtin_types = foldl (\types (n,t) -> Table.bind types n t) Table.empty [("unit", type_unit_def), ("bool", type_bool_def)] (builtin_env, builtin_decls) = foldl (\(env, decls) (ctor, val, typ) -> (bind_variable env ctor val, Table.bind decls ctor typ)) (empty_env, Table.empty) [("()", VCtor "()" 0 [], type_unit), ("True", VCtor "True" 0 [], type_bool), ("False", VCtor "False" 0 [], type_bool), ("%True", VCtor "True" 0 [], type_bool), ("%False", VCtor "False" 0 [], type_bool)] run str = ("", show (eval builtin_env (desugar (parse str)))) run_tc str = let types = new_type_info builtin_types in let typ = type_check types builtin_decls (desugar (parse str)) in expand_type types typ main :: IO () main = repl run (Just (fst . pretty_print_type Table.empty . run_tc))