import StdEnv
-import qualified Data.Map as DM
-from Data.Map import instance Functor (Map k)
-import qualified Data.Set as DS
-import Data.Functor
-import Data.Func
+import Control.Monad => qualified join
+import Control.Monad.State
+import Control.Monad.Trans
+import Control.Monad.Writer
import Data.Either
+import Data.Func
import Data.List
+import Data.Tuple
+import Data.Map => qualified put, union, difference, find, updateAt
import Data.Maybe
-import Control.Applicative
-import Control.Monad
-import Control.Monad.Trans
-import qualified Control.Monad.State as MS
-import Control.Monad.State => qualified gets, put, modify
-import Control.Monad.RWST => qualified put
-
-import ast
-
-check :: AST -> Either [String] (AST, [([Char], Scheme)])
-check (AST fs) = pure (AST fs, [])/*case inferAST preamble fs of
- Left e = Left e
- Right s = Right (AST fs, 'DM'.toList s)
+import Text
+
+import ast, scc
+
+import StdDebug
+
+check :: ![Either TypeDef Function] -> Either [String] (Expression, [([Char], Scheme)])
+check tdfs
+ # dups = filter (\x->length x > 1) (groupBy (\(Function i _ _) (Function j _ _)->i == j) functions)
+ | length dups > 0 = Left ["Duplicate functions: ":[toString n\\[(Function n _ _):_]<-dups]]
+ = case partition (\a->a=:(Function ['start'] _ _)) functions of
+ ([], _) = Left ["No start function defined"]
+ ([Function _ [] e:_], fs)
+ # e = makeExpression fs e
+ = tuple e <$> runInfer (infer (fromList (conses ++ builtin)) e)
+ ([Function _ _ _:_], _) = Left ["Start cannot have arguments"]
where
- preamble = 'DM'.fromList
- [(['if'], Forall [['a']] $ TFun TBool $ TFun (TVar ['a']) $ TFun (TVar ['a']) $ TVar ['a'])
- ,(['eq'], Forall [] $ TFun TInt $ TFun TInt TBool)
- ,(['mul'], Forall [] $ TFun TInt $ TFun TInt TInt)
- ,(['div'], Forall [] $ TFun TInt $ TFun TInt TInt)
- ,(['add'], Forall [] $ TFun TInt $ TFun TInt TInt)
- ,(['sub'], Forall [] $ TFun TInt $ TFun TInt TInt)
+ functions = rights tdfs
+ conses = flatten $ map (\(TypeDef n t cs)->
+ let cons = Forall t o foldr (-->) (foldl TApp (TVar n) (map TVar t))
+ in map (appSnd cons) cs) $ lefts tdfs
+ builtin =
+ [(['_if'], Forall [['a']] $ TBool --> TVar ['a'] --> TVar ['a'] --> TVar ['a'])
+ ,(['_eq'], Forall [] $ TInt --> TInt --> TBool)
+ ,(['_mul'], Forall [] $ TInt --> TInt --> TInt)
+ ,(['_add'], Forall [] $ TInt --> TInt --> TInt)
+ ,(['_sub'], Forall [] $ TInt --> TInt --> TInt)
+ ,(['_div'], Forall [] $ TInt --> TInt --> TInt)
]
-*/
-:: TypeEnv :== 'DM'.Map [Char] Scheme
-:: Constraint :== (Type, Type)
-:: Subst :== 'DM'.Map [Char] Type
-:: Unifier :== (Subst, [Constraint])
-:: Infer a :== RWST TypeEnv [Constraint] InferState (Either [String]) a
-:: InferState = { count :: Int }
-:: Scheme = Forall [[Char]] Type
-:: Solve a :== StateT Unifier (Either [String]) a
+makeExpression :: [Function] Expression -> Expression
+makeExpression fs start = foldr mkExpr start $ scc $ map (appSnd vars) nicefuns
+where
+ mkExpr :: [[Char]] -> (Expression -> Expression)
+ mkExpr scc = Let [(l, e)\\(l, e)<-nicefuns, s<-scc | s == l]
-nullSubst :: Subst
-nullSubst = 'DM'.newMap
+ nicefuns :: [([Char], Expression)]
+ nicefuns = [(l, foldr ((o) o Lambda) id i e)\\(Function l i e)<-fs]
-uni :: Type Type -> Infer ()
-uni t1 t2 = tell [(t1, t2)]
+ vars :: Expression -> [[Char]]
+ vars (Var v) = [v]
+ vars (App l r) = vars l ++ vars r
+ vars (Lambda l e) = flt l e
+ vars (Let ns e) = flatten [[v\\v<-vars e | not (isMember v (map fst ns))]:map (uncurry flt) ns]
+ vars _ = []
-inEnv :: ([Char], Scheme) (Infer a) -> Infer a
-inEnv (x, sc) m = local (\e->'DM'.put x sc $ 'DM'.del x e) m
+ flt i e = [v\\v<-vars e | v <> i]
-letters :: [[Char]]
-letters = [1..] >>= flip replicateM ['a'..'z']
+instance toString Scheme where
+ toString (Forall [] t) = toString t
+ toString (Forall as t) = concat ["A.", join " " (map toString as), ": ", toString t]
-fresh :: Infer Type
-fresh = get >>= \s=:{count}->'Control.Monad.RWST'.put {s & count=count + 1} >>| pure (TVar $ letters !! count)
+:: TypeEnv :== Map [Char] Scheme
+:: Subst :== Map [Char] Type
-class Substitutable a
-where
- apply :: Subst a -> a
- ftv :: a -> [[Char]]
+:: Infer a :== StateT [Int] (WriterT [([Char], Scheme)] (Either [String])) a
-instance Substitutable Type
-where
- apply s t=:(TVar a) = maybe t id $ 'DM'.get a s
- apply s (TFun t1 t2) = TFun (apply s t1) (apply s t2)
- apply _ t = t
+runInfer :: (Infer (Subst, Type)) -> Either [String] [([Char], Scheme)]
+runInfer i = case runWriterT (evalStateT i [0..]) of
+ Left e = Left e
+ Right ((s, t), w) = pure [(['start'], generalize newMap (apply s t)):w]
- ftv (TVar a) = [a]
- ftv (TFun t1 t2) = union (ftv t1) (ftv t2)
- ftv t = []
+fresh :: Infer Type
+fresh = getState >>= \[s:ss]->put ss >>| pure (TVar (['v':[c\\c<-:toString s]]))
-instance Substitutable Scheme
-where
- apply s (Forall as t) = Forall as $ apply (foldr 'DM'.del s as) t
- ftv (Forall as t) = difference (ftv t) as
+(oo) infixl 9 :: Subst Subst -> Subst
+(oo) s1 s2 = 'Data.Map'.union (apply s1 <$> s2) s1
-instance Substitutable [a] | Substitutable a
-where
- apply s ls = map (apply s) ls
- ftv t = foldr (union o ftv) [] t
+class Substitutable a where
+ apply :: Subst a -> a
+ ftv :: a -> [[Char]]
+
+instance Substitutable Type where
+ apply s t=:(TVar v) = fromMaybe t (get v s)
+ apply s (t1 --> t2) = apply s t1 --> apply s t2
+ apply s (TApp t1 t2) = TApp (apply s t1) (apply s t2)
+ apply _ x = x
+
+ ftv (TVar v) = [v]
+ ftv (t1 --> t2) = on union ftv t1 t2
+ ftv (TApp t1 t2) = on union ftv t1 t2
+ ftv _ = []
+
+instance Substitutable Scheme where
+ apply s (Forall as t) = Forall as $ apply (foldr del s as) t
+ ftv (Forall as t) = difference (ftv t) (removeDup as)
instance Substitutable TypeEnv where
- apply s env = fmap (apply s) env
- ftv env = ftv $ 'DM'.elems env
+ apply s env = apply s <$> env
+ ftv env = ftv (elems env)
-instance Substitutable Constraint where
- apply s (t1, t2) = (apply s t1, apply s t2)
- ftv (t1, t2) = union (ftv t1) (ftv t2)
+instance Substitutable [a] | Substitutable a where
+ apply s l = apply s <$> l
+ ftv t = foldr (union o ftv) [] t
-instantiate :: Scheme -> Infer Type
-instantiate (Forall as t) = mapM (const fresh) as
- >>= \as`->let s = 'DM'.fromList $ zip2 as as` in pure $ apply s t
+occursCheck :: [Char] -> (a -> Bool) | Substitutable a
+occursCheck a = isMember a o ftv
+
+err :: [String] -> Infer a
+err e = liftT (liftT (Left e))
+
+unify :: Type Type -> Infer Subst
+unify (l --> r) (l` --> r`)
+ = unify l l`
+ >>= \s1->on unify (apply s1) r r`
+ >>= \s2->pure (s1 oo s2)
+unify (TVar a) (TVar t)
+ | a == t = pure newMap
+unify (TVar a) t
+ | occursCheck a t = err ["Infinite type: ", toString a, " to ", toString t]
+ = pure (singleton a t)
+unify t (TVar a) = unify (TVar a) t
+unify TInt TInt = pure newMap
+unify TBool TBool = pure newMap
+unify (TApp l r) (TApp l` r`)
+ = unify l l`
+ >>= \s1->on unify (apply s1) r r`
+ >>= \s2->pure (s1 oo s2)
+unify t1 t2 = err ["Cannot unify: ", toString t1, " with ", toString t2]
+
+unifyl :: [Type] -> Infer Subst
+unifyl [t1,t2:ts] = unify t1 t2 >>= \s->unifyl (map (apply s) [t2:ts])
+unifyl _ = pure newMap
+
+instantiate :: Scheme -> Infer Type
+instantiate (Forall as t)
+ = sequence [fresh\\_<-as]
+ >>= \as`->pure (apply (fromList $ zip2 as as`) t)
generalize :: TypeEnv Type -> Scheme
generalize env t = Forall (difference (ftv t) (ftv env)) t
-//:: Expression
-// = Lit Value
-// | Var [Char]
-// | App Expression Expression
-// | Lambda [Char] Expression
-// | Builtin [Char] [Expression]
-inferExpr :: TypeEnv Expression -> Either [String] Scheme
-inferExpr env ex = case runRWST (infer ex) env {count=0} of
- Left e = Left e
- Right (ty, st, cs) = case runStateT solver ('DM'.newMap, cs) of
- Left e = Left e
- Right (s, _) = Right (closeOver (apply s ty))
-
-closeOver :: Type -> Scheme
-closeOver t = normalize (generalize 'DM'.newMap t)
-
-normalize :: Scheme -> Scheme
-normalize t = t
-
-inferAST :: TypeEnv [Function] -> Either [String] TypeEnv
-inferAST env [] = Right env
-inferAST env [Function name args body:rest] = case inferExpr env (foldr Lambda body args) of
- Left e = Left e
- Right ty = inferAST ('DM'.put name ty env) rest
-
-inferFunc :: [Function] -> Infer ()
-inferFunc [] = pure ()
-inferFunc [Function name args body:rest]
- = ask
- >>= \en->infer (foldr Lambda body args)
- >>= \t1->inEnv (name, generalize en t1) (inferFunc rest)
- >>= \_->pure ()
-
-infer :: Expression -> Infer Type
-infer (Lit v) = case v of
- Int _ = pure TInt
- Bool _ = pure TBool
- Char _ = pure TChar
-infer (Var s) = asks ('DM'.get s)
- >>= maybe (liftT $ Left ["Unbound variable " +++ toString s]) instantiate
-infer (App e1 e2)
- = infer e1
- >>= \t1->infer e2
- >>= \t2->fresh
- >>= \tv->uni t1 (TFun t2 tv)
- >>| pure tv
-infer (Lambda s e)
- = fresh
- >>= \tv->inEnv (s, Forall [] tv) (infer e)
- >>= \t-> pure (TFun tv t)
-//infer (Let x e1 e2)
-// = ask
-// >>= \en->infer e1
-// >>= \t1->inEnv (x, generalize en t1) (infer e2)
-
-unifies :: Type Type -> Solve Unifier
-unifies TInt TInt = pure ('DM'.newMap, [])
-unifies TBool TBool = pure ('DM'.newMap, [])
-unifies TChar TChar = pure ('DM'.newMap, [])
-unifies (TVar a) (TVar b)
- | a == b = pure ('DM'.newMap, [])
-unifies (TVar v) t = tbind v t
-unifies t (TVar v) = tbind v t
-unifies (TFun t1 t2) (TFun t3 t4) = unifyMany [t1, t2] [t3, t4]
-unifies t1 t2 = liftT $ Left ["Cannot unify " +++ toString t1 +++ " with " +++ toString t2]
-
-unifyMany :: [Type] [Type] -> Solve Unifier
-unifyMany [] [] = pure ('DM'.newMap, [])
-unifyMany [t1:ts1] [t2:ts2] = unifies t1 t2
- >>= \(su1, cs1)->unifyMany (apply su1 ts1) (apply su1 ts2)
- >>= \(su2, cs2)->pure (su2 `compose` su1, cs1 ++ cs2)
-unifyMany t1 t2 = liftT $ Left ["Length difference in unifyMany"]
-
-(`compose`) infix 1 :: Subst Subst -> Subst
-(`compose`) s1 s2 = 'DM'.union (apply s1 <$> s2) s1
-
-tbind :: [Char] Type -> Solve Unifier
-tbind a (TVar b)
- | a == b = pure ('DM'.newMap, [])
-tbind a t
- | occursCheck a t = liftT $ Left ["Infinite type " +++ toString a +++ toString t]
- = pure $ ('DM'.singleton a t, [])
-
-occursCheck :: [Char] a -> Bool | Substitutable a
-occursCheck a t = isMember a $ ftv t
-
-solver :: Solve Subst
-solver = getState >>= \(su, cs)->case cs of
- [] = pure su
- [(t1, t2):cs0] = unifies t1 t2
- >>= \(su1, cs1)->'MS'.put (su1 `compose` su, cs1 ++ (apply su1 cs0))
- >>| solver
+infer :: TypeEnv Expression -> Infer (Subst, Type)
+infer env (Lit (Int _)) = pure (newMap, TInt)
+infer env (Lit (Bool _)) = pure (newMap, TBool)
+infer env (Var x) = maybe (err ["Unbound variable: ", toString x])
+ (\s->tuple newMap <$> instantiate s) $ get x env
+infer env (App e1 e2)
+ = fresh
+ >>= \tv-> infer env e1
+ >>= \(s1, t1)->infer (apply s1 env) e2
+ >>= \(s2, t2)->unify (apply s2 t1) (t2 --> tv)
+ >>= \s3-> pure (s3 oo s2 oo s1, apply s3 tv)
+infer env (Lambda x b)
+ = fresh
+ >>= \tv-> infer ('Data.Map'.put x (Forall [] tv) env) b
+ >>= \(s1, t1)->pure (s1, apply s1 tv --> t1)
+//Non recursion
+//infer env (Let [(x, e1)] e2)
+// = infer env e1
+// >>= \(s1, t1)->infer ('Data.Map'.put x (generalize (apply s1 env) t1) env) e2
+// >>= \(s2, t2)->liftT (tell [(x, Forall [] t1)])
+// >>| pure (s1 oo s2, t2)
+//Single recursion
+//infer env (Let [(x, e1)] e2)
+// = fresh
+// >>= \tv-> let env` = 'Data.Map'.put x (Forall [] tv) env
+// in infer env` e1
+// >>= \(s1,t1)-> infer ('Data.Map'.put x (generalize (apply s1 env`) t1) env`) e2
+// >>= \(s2, t2)->pure (s1 oo s2, t2)
+//Multiple recursion
+infer env (Let xs e2)
+ # (ns, bs) = unzip xs
+ = sequence [fresh\\_<-ns]
+ >>= \tvs-> let env` = foldr (\(k, v)->'Data.Map'.put k (Forall [] v)) env (zip2 ns tvs)
+ in unzip <$> sequence (map (infer env`) bs)
+ >>= \(ss,ts)-> unifyl ts
+ >>= \s-> liftT (tell [(n, generalize (apply s env`) t)\\t<-ts & n<-ns])
+ >>| let env`` = foldr (\(n, s, t) m->'Data.Map'.put n (generalize (apply s env`) t) m) env` (zip3 ns ss ts)
+ in infer env`` e2
+ >>= \(s2, t2)->pure (s oo s2, t2)
repositories / minfp.git / blobdiff