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 Text
  14
  15 import ast
  16
  17 check :: [Function] -> Either [String] (Expression, Scheme)
  18 check fs
  19         # dups = filter (\x->length x > 1) (groupBy (\(Function i _ _) (Function j _ _)->i == j) fs)
  20         | length dups > 0 = Left ["Duplicate functions: ":[toString n\\[(Function n _ _):_]<-dups]]
  21         = case partition (\a->a=:(Function ['start'] _ _)) fs of
  22                 ([], _) = Left ["No start function defined"]
  23                 ([Function _ [] e], fs)
  24                         # e = foldr (\(Function i a e)->Let i (foldr ((o) o Lambda) id a e)) e fs
  25                         = (\x->(e, x)) <$> runInfer (infer preamble e)
  26                 ([Function _ _ _], _) = Left ["Start cannot have arguments"]
  27
  28 instance toString Scheme where
  29         toString (Forall as t) = concat ["A.", join " " (map toString as), ": ", toString t]
  30
  31 instance toString Type where
  32         toString (TVar a) = toString a
  33         toString TInt = "Int"
  34         toString TBool = "Bool"
  35         toString (a --> b) = concat ["(", toString a, ") -> ", toString b]
  36
  37 :: TypeEnv :== Map [Char] Scheme
  38 preamble :: TypeEnv
  39 preamble = fromList
  40         [(['_if'],  Forall [['_ift']]
  41                 $ TBool --> TVar ['_ift'] --> TVar ['_ift'] --> TVar ['_ift'])
  42         ,(['_eq'],  Forall [['_eq']] $ TInt --> TInt --> TBool)
  43         ,(['_mul'], Forall [['_mul']] $ TInt --> TInt --> TInt)
  44         ,(['_add'], Forall [['_add']] $ TInt --> TInt --> TInt)
  45         ,(['_sub'], Forall [['_sub']] $ TInt --> TInt --> TInt)
  46         ]
  47 :: Subst   :== Map [Char] Type
  48
  49 :: Infer a :== StateT [Int] (Either [String]) a
  50 runInfer :: (Infer (Subst, Type)) -> Either [String] Scheme
  51 runInfer i = uncurry ((o) (generalize newMap) o apply)
  52         <$> evalStateT i [0..]
  53
  54 fresh :: Infer Type
  55 fresh = getState >>= \[s:ss]->put ss >>| pure (TVar (['v':[c\\c<-:toString s]]))
  56
  57 (oo) infixr 9 :: Subst Subst -> Subst
  58 (oo) s1 s2 = 'Data.Map'.union (apply s1 <$> s2) s1
  59
  60 class Substitutable a where
  61         apply :: Subst a -> a
  62         ftv :: a -> [[Char]]
  63
  64 instance Substitutable Type where
  65         apply s t=:(TVar v) = fromMaybe t (get v s)
  66         apply s (t1 --> t2) = apply s t1 --> apply s t2
  67         apply _ x = x
  68
  69         ftv (TVar v) = [v]
  70         ftv (t1 --> t2) = on union ftv t1 t2
  71         ftv _ = []
  72
  73 instance Substitutable Scheme where
  74         apply s (Forall as t) = Forall as $ apply (foldr del s as) t
  75         ftv (Forall as t) = difference (ftv t) (removeDup as)
  76
  77 instance Substitutable TypeEnv where
  78         apply s env = apply s <$> env
  79         ftv env = ftv (elems env)
  80
  81 instance Substitutable [a] | Substitutable a where
  82         apply s l = apply s <$>  l
  83         ftv t = foldr (union o ftv) [] t
  84
  85 occursCheck :: [Char] -> (a -> Bool) | Substitutable a
  86 occursCheck a = isMember a o ftv
  87
  88 unify :: Type Type -> Infer Subst
  89 unify (l --> r) (l` --> r`)
  90         =        unify l l`
  91         >>= \s1->on unify (apply s1) r r`
  92         >>= \s2->pure (s1 oo s2)
  93 unify (TVar a) (TVar t)
  94         | a == t = pure newMap
  95 unify (TVar a) t
  96         | occursCheck a t = liftT (Left ["Infinite type: ", toString a, " to ", toString t])
  97         = pure (singleton a t)
  98 unify t (TVar a) = unify (TVar a) t
  99 unify TInt TInt = pure newMap
 100 unify TBool TBool = pure newMap
 101 unify t1 t2 = liftT (Left ["Cannot unify: ", toString t1, " with ", toString t2])
 102
 103 instantiate :: Scheme -> Infer Type
 104 instantiate (Forall as t)
 105         =         sequence [fresh\\_<-as]
 106         >>= \as`->pure (apply (fromList $ zip2 as as`) t)
 107
 108 generalize :: TypeEnv Type -> Scheme
 109 generalize env t = Forall (difference (ftv t) (ftv env)) t
 110
 111 infer :: TypeEnv Expression -> Infer (Subst, Type)
 112 infer env (Lit (Int _)) = pure (newMap, TInt)
 113 infer env (Lit (Bool _)) = pure (newMap, TBool)
 114 infer env (Var x) = case get x env of
 115         Nothing = liftT (Left ["Unbound variable: ", toString x])
 116         Just s = (\x->(newMap, x)) <$> instantiate s
 117 infer env (App e1 e2)
 118         =              fresh
 119         >>= \tv->      infer env e1
 120         >>= \(s1, t1)->infer (apply s1 env) e2
 121         >>= \(s2, t2)->unify (apply s2 t1) (t2 --> tv)
 122         >>= \s3->      pure (s1 oo s2 oo s3, apply s3 tv)
 123 infer env (Lambda x b)
 124         =              fresh
 125         >>= \tv->      infer ('Data.Map'.put x (Forall [] tv) env) b
 126         >>= \(s1, t1)->pure (s1, apply s1 tv --> t1)
 127 //infer env (Let x e1 e2)
 128 //      =              infer env e1
 129 //      >>= \(s1, t1)->infer ('Data.Map'.put x (generalize (apply s1 env) t1) env) e2
 130 //      >>= \(s2, t2)->pure (s1 oo s2, t2)
 131 infer env (Let x e1 e2)
 132         =              fresh
 133         >>= \tv->      infer ('Data.Map'.put x (Forall [] tv) env) e1
 134         >>= \(s1, t1)->infer ('Data.Map'.put x (generalize (apply s1 env) t1) env) e2
 135         >>= \(s2, t2)->pure (s1 oo s2, t2)