check.icl

   1 implementation module check
   2
   3 import StdEnv
   4
   5 import Control.Monad => qualified join
   6 import Control.Monad.State
   7 import Control.Monad.Trans
   8 import Control.Monad.Writer
   9 import Data.Either
  10 import Data.Func
  11 import Data.List
  12 import Data.Tuple
  13 import Data.Map => qualified put, union, difference, find, updateAt
  14 import Data.Maybe
  15 import Text
  16
  17 import ast, scc
  18
  19 check :: [Either TypeDef Function] -> Either [String] (Expression, [([Char], Scheme)])
  20 check fs
  21         # fs = [v\\(Right v)<-fs]
  22         # dups = filter (\x->length x > 1) (groupBy (\(Function i _ _) (Function j _ _)->i == j) fs)
  23         | length dups > 0 = Left ["Duplicate functions: ":[toString n\\[(Function n _ _):_]<-dups]]
  24         = case partition (\a->a=:(Function ['start'] _ _)) fs of
  25                 ([], _) = Left ["No start function defined"]
  26                 ([Function _ [] e:_], fs)
  27                         # e = makeExpression fs e
  28                         = (\x->(e, x)) <$> runInfer (infer (fromList builtin) e)
  29                 ([Function _ _ _:_], _) = Left ["Start cannot have arguments"]
  30 where
  31         builtin =
  32                 [(['_if'],  Forall [['a']] $ TBool --> TVar ['a'] --> TVar ['a'] --> TVar ['a'])
  33                 ,(['_fst'], Forall [['a'], ['b']] $ TTuple (TVar ['a']) (TVar ['b']) --> TVar ['a'])
  34                 ,(['_snd'], Forall [['a'], ['b']] $ TTuple (TVar ['a']) (TVar ['b']) --> TVar ['b'])
  35                 ,(['_eq'],  Forall [] $ TInt --> TInt --> TBool)
  36                 ,(['_mul'], Forall [] $ TInt --> TInt --> TInt)
  37                 ,(['_add'], Forall [] $ TInt --> TInt --> TInt)
  38                 ,(['_sub'], Forall [] $ TInt --> TInt --> TInt)
  39                 ,(['_div'], Forall [] $ TInt --> TInt --> TInt)
  40                 ]
  41
  42 makeExpression :: [Function] Expression -> Expression
  43 makeExpression fs start = foldr mkExpr start $ scc $ map (appSnd vars) nicefuns
  44 where
  45         mkExpr :: [[Char]] -> (Expression -> Expression)
  46         mkExpr scc = Let [(l, e)\\(l, e)<-nicefuns, s<-scc | s == l]
  47
  48         nicefuns :: [([Char], Expression)]
  49         nicefuns = [(l, foldr ((o) o Lambda) id i e)\\(Function l i e)<-fs]
  50
  51         vars :: Expression -> [[Char]]
  52         vars (Var v) = [v]
  53         vars (App l r) = vars l ++ vars r
  54         vars (Lambda l e) = flt l e
  55         vars (Let ns e) = flatten [[v\\v<-vars e | not (isMember v (map fst ns))]:map (uncurry flt) ns]
  56         vars _ = []
  57
  58         flt i e = [v\\v<-vars e | v <> i]
  59
  60 instance toString Scheme where
  61         toString (Forall [] t) = toString t
  62         toString (Forall as t) = concat ["A.", join " " (map toString as), ": ", toString t]
  63
  64 :: TypeEnv :== Map [Char] Scheme
  65 :: Subst :== Map [Char] Type
  66
  67 :: Infer a :== StateT [Int] (WriterT [([Char], Scheme)] (Either [String])) a
  68
  69 runInfer :: (Infer (Subst, Type)) -> Either [String] [([Char], Scheme)]
  70 runInfer i = case runWriterT (evalStateT i [0..]) of
  71         Left e = Left e
  72         Right ((s, t), w) = pure [(['start'], generalize newMap (apply s t)):w]
  73
  74 fresh :: Infer Type
  75 fresh = getState >>= \[s:ss]->put ss >>| pure (TVar (['v':[c\\c<-:toString s]]))
  76
  77 (oo) infixl 9 :: Subst Subst -> Subst
  78 (oo) s1 s2 = 'Data.Map'.union (apply s1 <$> s2) s1
  79
  80 class Substitutable a where
  81         apply :: Subst a -> a
  82         ftv :: a -> [[Char]]
  83
  84 instance Substitutable Type where
  85         apply s t=:(TVar v) = fromMaybe t (get v s)
  86         apply s (t1 --> t2) = apply s t1 --> apply s t2
  87         apply _ x = x
  88
  89         ftv (TVar v) = [v]
  90         ftv (t1 --> t2) = on union ftv t1 t2
  91         ftv _ = []
  92
  93 instance Substitutable Scheme where
  94         apply s (Forall as t) = Forall as $ apply (foldr del s as) t
  95         ftv (Forall as t) = difference (ftv t) (removeDup as)
  96
  97 instance Substitutable TypeEnv where
  98         apply s env = apply s <$> env
  99         ftv env = ftv (elems env)
 100
 101 instance Substitutable [a] | Substitutable a where
 102         apply s l = apply s <$>  l
 103         ftv t = foldr (union o ftv) [] t
 104
 105 occursCheck :: [Char] -> (a -> Bool) | Substitutable a
 106 occursCheck a = isMember a o ftv
 107
 108 err :: [String] -> Infer a
 109 err e = liftT (liftT (Left e))
 110
 111 unify :: Type Type -> Infer Subst
 112 unify (l --> r) (l` --> r`)
 113         =        unify l l`
 114         >>= \s1->on unify (apply s1) r r`
 115         >>= \s2->pure (s1 oo s2)
 116 unify (TVar a) (TVar t)
 117         | a == t = pure newMap
 118 unify (TVar a) t
 119         | occursCheck a t = err ["Infinite type: ", toString a, " to ", toString t]
 120         = pure (singleton a t)
 121 unify t (TVar a) = unify (TVar a) t
 122 unify TInt TInt = pure newMap
 123 unify TBool TBool = pure newMap
 124 unify (TTuple l r) (TTuple l` r`)
 125         = unify l l`
 126         >>= \s1->on unify (apply s1) r r`
 127         >>= \s2->pure (s1 oo s2)
 128 unify t1 t2 = err ["Cannot unify: ", toString t1, " with ", toString t2]
 129
 130 unifyl :: [Type] -> Infer Subst
 131 unifyl [t1,t2:ts] = unify t1 t2 >>= \s->unifyl (map (apply s) [t2:ts])
 132 unifyl _ = pure newMap
 133
 134 instantiate :: Scheme -> Infer Type
 135 instantiate (Forall as t)
 136         =         sequence [fresh\\_<-as]
 137         >>= \as`->pure (apply (fromList $ zip2 as as`) t)
 138
 139 generalize :: TypeEnv Type -> Scheme
 140 generalize env t = Forall (difference (ftv t) (ftv env)) t
 141
 142 infer :: TypeEnv Expression -> Infer (Subst, Type)
 143 infer env (Lit (Int _)) = pure (newMap, TInt)
 144 infer env (Lit (Bool _)) = pure (newMap, TBool)
 145 infer env (Var x) = maybe (err ["Unbound variable: ", toString x])
 146         (\s->tuple newMap <$> instantiate s) $ get x env
 147 infer env (App e1 e2)
 148         =              fresh
 149         >>= \tv->      infer env e1
 150         >>= \(s1, t1)->infer (apply s1 env) e2
 151         >>= \(s2, t2)->unify (apply s2 t1) (t2 --> tv)
 152         >>= \s3->      pure (s3 oo s2 oo s1, apply s3 tv)
 153 infer env (Tuple a b)
 154         =              infer env a
 155         >>= \(s1, t1)->infer env b
 156         >>= \(s2, t2)->pure (s1 oo s2, TTuple t1 t2)
 157 infer env (Lambda x b)
 158         =              fresh
 159         >>= \tv->      infer ('Data.Map'.put x (Forall [] tv) env) b
 160         >>= \(s1, t1)->pure (s1, apply s1 tv --> t1)
 161 //Non recursion
 162 //infer env (Let [(x, e1)] e2)
 163 //      =              infer env e1
 164 //      >>= \(s1, t1)->infer ('Data.Map'.put x (generalize (apply s1 env) t1) env) e2
 165 //      >>= \(s2, t2)->liftT (tell [(x, Forall [] t1)])
 166 //      >>|            pure (s1 oo s2, t2)
 167 //Single recursion
 168 //infer env (Let [(x, e1)] e2)
 169 //      =              fresh
 170 //      >>= \tv->      let env` = 'Data.Map'.put x (Forall [] tv) env
 171 //                     in infer env` e1
 172 //      >>= \(s1,t1)-> infer ('Data.Map'.put x (generalize (apply s1 env`) t1) env`) e2
 173 //      >>= \(s2, t2)->pure (s1 oo s2, t2)
 174 //Multiple recursion
 175 infer env (Let xs e2)
 176         # (ns, bs) = unzip xs
 177         =              sequence [fresh\\_<-ns]
 178         >>= \tvs->     let env` = foldr (\(k, v)->'Data.Map'.put k (Forall [] v)) env (zip2 ns tvs)
 179                        in  unzip <$> sequence (map (infer env`) bs)
 180         >>= \(ss,ts)-> unifyl ts
 181         >>= \s->       liftT (tell [(n, generalize (apply s env`) t)\\t<-ts & n<-ns])
 182         >>|            let env`` = foldr (\(n, s, t) m->'Data.Map'.put n (generalize (apply s env`) t) m) env` (zip3 ns ss ts)
 183                        in infer env`` e2
 184         >>= \(s2, t2)->pure (s oo s2, t2)