check.icl

   1 implementation module check
   2
   3 import StdEnv
   4
   5 import Data.Either
   6 import Data.List
   7 import Data.Functor
   8 import Data.Func
   9 import Data.Maybe
  10 import Data.Tuple
  11 import Control.Monad
  12 import Control.Monad.Trans
  13 import Control.Monad.State
  14
  15 import qualified Data.Map
  16 from Data.Map import instance Functor (Map k)
  17
  18 import ast
  19
  20 import StdDebug
  21 check :: [Function] -> Either [String] Expression
  22 check fs
  23         # dups = filter (\x->length x > 1) (groupBy (\(Function i _ _) (Function j _ _)->i == j) fs)
  24         | length dups > 0 = Left ["Duplicate functions: ":[toString n\\[(Function n _ _):_]<-dups]]
  25         = case partition (\a->a=:(Function ['start'] _ _)) fs of
  26                 ([], _) = Left ["No start function defined"]
  27                 ([Function _ [] e], fs)
  28                         # e = foldr (\(Function i a e)->Let i a e) e fs
  29                         = case runInfer (infer 'Data.Map'.newMap e) of
  30                                 Left e = Left e
  31                                 Right s
  32                                         = Left [printToString s]
  33                 ([Function _ _ _], _) = Left ["Start cannot have arguments"]
  34
  35 import Text.GenPrint
  36 derive gPrint Scheme, Type
  37
  38 //Polytypes
  39 :: Scheme = Forall [[Char]] Type
  40 :: TypeEnv :== 'Data.Map'.Map [Char] Scheme
  41 :: Subst   :== 'Data.Map'.Map [Char] Type
  42 nullSubst = 'Data.Map'.newMap
  43
  44 :: Infer a :== StateT [Int] (Either [String]) a
  45 runInfer :: (Infer (Subst, Type)) -> Either [String] Scheme
  46 runInfer i = uncurry closeOver <$> evalStateT i [0..]
  47 where
  48         closeOver :: Subst Type -> Scheme
  49         closeOver sub ty = normalize (generalize 'Data.Map'.newMap (apply sub ty))
  50
  51         normalize :: Scheme -> Scheme
  52         normalize i = i
  53 //      normalize (Forall ts body) = Forall (snd <$> ord) (normtype body)
  54 //      where
  55 //              ord = zip2 (removeDup $ fv body) (fmap letters)
  56 //
  57 //      fv (TVar a) = [a]
  58 //      fv (TFun a b) = fv a ++ fv b
  59 //      fv _ = []
  60 //
  61 //      normtype (TFun a b) = TFun (normtype a) (normtype b)
  62 //      normtype (TCon a)   = TCon a
  63 //      normtype (TVar a)   =
  64 //                case lookup a ord of
  65 //                      Just x = TVar x
  66 //                      Nothing = Left ["type variable not in signature"]
  67
  68 fresh :: Infer Type
  69 fresh = getState >>= \[s:ss]->put ss >>| pure (TVar (['v':[c\\c<-:toString s]]))
  70
  71 compose :: Subst Subst -> Subst
  72 compose s1 s2 = 'Data.Map'.union (apply s1 <$> s2) s1
  73
  74 class Substitutable a where
  75         apply :: Subst a -> a
  76         ftv :: a -> [[Char]]
  77
  78 instance Substitutable Type where
  79         apply s t=:(TVar v) = 'Data.Map'.findWithDefault t v s
  80         apply s (TFun t1 t2) = on TFun (apply s) t1 t2
  81         apply _ x = x
  82
  83         ftv (TVar v) = [v]
  84         ftv (TFun t1 t2) = on union ftv t1 t2
  85         ftv _ = []
  86
  87 instance Substitutable Scheme where
  88         apply s (Forall as t) = Forall as $ apply (foldr 'Data.Map'.del s as) t
  89         ftv (Forall as t) = difference (ftv t) (removeDup as)
  90
  91 instance Substitutable TypeEnv where
  92         apply s env = apply s <$> env
  93         ftv env = ftv ('Data.Map'.elems env)
  94
  95 instance Substitutable [a] | Substitutable a where
  96         apply s l = apply s <$>  l
  97         ftv t = foldr (union o ftv) [] t
  98
  99 occursCheck :: [Char] -> (a -> Bool) | Substitutable a
 100 occursCheck a = isMember a o ftv
 101
 102 unify :: Type Type -> Infer Subst
 103 unify (TFun l r) (TFun l` r`)
 104         =        unify l l`
 105         >>= \s1->on unify (apply s1) r r`
 106         >>= \s2->pure (compose s1 s2)
 107 unify (TVar a) t = bind a t
 108 unify t (TVar a) = bind a t
 109 unify TInt TInt = pure nullSubst
 110 unify TBool TBool = pure nullSubst
 111 unify t1 t2 = liftT (Left ["Cannot unify: ", toString t1, " with ", toString t2])
 112
 113 bind :: [Char] Type -> Infer Subst
 114 bind a (TVar t) | a == t = pure nullSubst
 115 bind a t
 116         | occursCheck a t = liftT (Left ["Infinite type: ", toString a, " and ", toString t])
 117         = pure ('Data.Map'.singleton a t)
 118
 119 instantiate :: Scheme -> Infer Type
 120 instantiate (Forall as t)
 121         =         sequence [fresh\\_<-as]
 122         >>= \as`->pure (apply ('Data.Map'.fromList $ zip2 as as`) t)
 123
 124 generalize :: TypeEnv Type -> Scheme
 125 generalize env t = Forall (difference (ftv t) (ftv env)) t
 126
 127 infer :: TypeEnv Expression -> Infer (Subst, Type)
 128 infer env (Lit (Int _)) = pure (nullSubst, TInt)
 129 infer env (Lit (Bool _)) = pure (nullSubst, TBool)
 130 infer env (Var x) = case 'Data.Map'.get x env of
 131         Nothing = liftT (Left ["Unbound variable: ", toString x])
 132         Just s = tuple nullSubst <$> instantiate s
 133 infer env (App e1 e2)
 134         =              fresh
 135         >>= \tv->      infer env e1
 136         >>= \(s1, t1)->infer (apply s1 env) e2
 137         >>= \(s2, t2)->unify (apply s2 t1) (TFun t2 tv)
 138         >>= \s3->      pure (compose (compose s3 s2) s1, apply s3 tv)
 139 infer env (Lambda x b)
 140         =              fresh
 141         >>= \tv->      infer ('Data.Map'.put x (Forall [] tv) env) b
 142         >>= \(s1, t1)->pure (s1, TFun (apply s1 tv) t1)
 143 infer env (Builtin c a) = undef
 144 infer env (Let i args e b) = undef