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