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