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 (mkLambda 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 mkLambda :: [[Char]] Expression -> Expression
  36 mkLambda [] e = e
  37 mkLambda [a:as] e = Lambda a (mkLambda as e)
  38
  39 import Text.GenPrint
  40 derive gPrint Scheme, Type
  41
  42 //Polytypes
  43 :: Scheme = Forall [[Char]] Type
  44 :: TypeEnv :== 'Data.Map'.Map [Char] Scheme
  45 :: Subst   :== 'Data.Map'.Map [Char] Type
  46 nullSubst = 'Data.Map'.newMap
  47
  48 :: Infer a :== StateT [Int] (Either [String]) a
  49 runInfer :: (Infer (Subst, Type)) -> Either [String] Scheme
  50 runInfer i = uncurry closeOver <$> evalStateT i [0..]
  51 where
  52         closeOver :: Subst Type -> Scheme
  53         closeOver sub ty = normalize (generalize 'Data.Map'.newMap (apply sub ty))
  54
  55         normalize :: Scheme -> Scheme
  56         normalize i = i
  57 //      normalize (Forall ts body) = Forall (snd <$> ord) (normtype body)
  58 //      where
  59 //              ord = zip2 (removeDup $ fv body) (fmap letters)
  60 //
  61 //      fv (TVar a) = [a]
  62 //      fv (TFun a b) = fv a ++ fv b
  63 //      fv _ = []
  64 //
  65 //      normtype (TFun a b) = TFun (normtype a) (normtype b)
  66 //      normtype (TCon a)   = TCon a
  67 //      normtype (TVar a)   =
  68 //                case lookup a ord of
  69 //                      Just x = TVar x
  70 //                      Nothing = Left ["type variable not in signature"]
  71
  72 fresh :: Infer Type
  73 fresh = getState >>= \[s:ss]->put ss >>| pure (TVar (['v':[c\\c<-:toString s]]))
  74
  75 compose :: Subst Subst -> Subst
  76 compose s1 s2 = 'Data.Map'.union (apply s1 <$> s2) s1
  77
  78 class Substitutable a where
  79         apply :: Subst a -> a
  80         ftv :: a -> [[Char]]
  81
  82 instance Substitutable Type where
  83         apply s t=:(TVar v) = 'Data.Map'.findWithDefault t v s
  84         apply s (TFun t1 t2) = on TFun (apply s) t1 t2
  85         apply _ x = x
  86
  87         ftv (TVar v) = [v]
  88         ftv (TFun t1 t2) = on union ftv t1 t2
  89         ftv _ = []
  90
  91 instance Substitutable Scheme where
  92         apply s (Forall as t) = Forall as $ apply (foldr 'Data.Map'.del s as) t
  93         ftv (Forall as t) = difference (ftv t) (removeDup as)
  94
  95 instance Substitutable TypeEnv where
  96         apply s env = apply s <$> env
  97         ftv env = ftv ('Data.Map'.elems env)
  98
  99 instance Substitutable [a] | Substitutable a where
 100         apply s l = apply s <$>  l
 101         ftv t = foldr (union o ftv) [] t
 102
 103 occursCheck :: [Char] -> (a -> Bool) | Substitutable a
 104 occursCheck a = isMember a o ftv
 105
 106 unify :: Type Type -> Infer Subst
 107 unify (TFun l r) (TFun l` r`)
 108         =        unify l l`
 109         >>= \s1->on unify (apply s1) r r`
 110         >>= \s2->pure (compose s1 s2)
 111 unify (TVar a) t = bind a t
 112 unify t (TVar a) = bind a t
 113 unify TInt TInt = pure nullSubst
 114 unify TBool TBool = pure nullSubst
 115 unify t1 t2 = liftT (Left ["Cannot unify: ", toString t1, " with ", toString t2])
 116
 117 bind :: [Char] Type -> Infer Subst
 118 bind a (TVar t) | a == t = pure nullSubst
 119 bind a t
 120         | occursCheck a t = liftT (Left ["Infinite type: ", toString a, " and ", toString t])
 121         = pure ('Data.Map'.singleton a t)
 122
 123 instantiate :: Scheme -> Infer Type
 124 instantiate (Forall as t)
 125         =         sequence [fresh\\_<-as]
 126         >>= \as`->pure (apply ('Data.Map'.fromList $ zip2 as as`) t)
 127
 128 generalize :: TypeEnv Type -> Scheme
 129 generalize env t = Forall (difference (ftv t) (ftv env)) t
 130
 131 infer :: TypeEnv Expression -> Infer (Subst, Type)
 132 infer env (Lit (Int _)) = pure (nullSubst, TInt)
 133 infer env (Lit (Bool _)) = pure (nullSubst, TBool)
 134 infer env (Var x) = case 'Data.Map'.get x env of
 135         Nothing = liftT (Left ["Unbound variable: ", toString x])
 136         Just s = tuple nullSubst <$> instantiate s
 137 infer env (App e1 e2)
 138         =              fresh
 139         >>= \tv->      infer env e1
 140         >>= \(s1, t1)->infer (apply s1 env) e2
 141         >>= \(s2, t2)->unify (apply s2 t1) (TFun t2 tv)
 142         >>= \s3->      pure (compose (compose s3 s2) s1, apply s3 tv)
 143 infer env (Lambda x b)
 144         =              fresh
 145         >>= \tv->      infer ('Data.Map'.put x (Forall [] tv) env) b
 146         >>= \(s1, t1)->pure (s1, TFun (apply s1 tv) t1)
 147 infer env (Builtin c a) = undef
 148 infer env (Let x e1 e2)
 149         =              infer env e1
 150         >>= \(s1, t1)->let env` = apply s1 env in infer ('Data.Map'.put x (generalize env` t1) env) e2
 151         >>= \(s2, t2)->pure (compose s1 s2, t2)