check.icl

   1 implementation module check
   2
   3 import StdEnv
   4 import Data.Either
   5 import Data.List
   6 import Data.Functor
   7 import Data.Func
   8 import Data.Maybe
   9 import Data.Monoid
  10 import Control.Applicative
  11 import Control.Monad
  12 import Control.Monad.Trans
  13 import Control.Monad.RWST
  14 import qualified Data.Map as DM
  15 from Data.Map import instance Functor (Map k)
  16
  17 import ast
  18
  19 check :: AST -> Either [String] AST
  20 check (AST fs) = case find (\f->f=:(Function ['start'] [] _)) fs of
  21         Nothing = Left ["No start function defined"]
  22         Just _ = Right (AST fs)
  23
  24 :: Type
  25         = TVar [Char]
  26         | TInt
  27         | TBool
  28         | TChar
  29         | TFun Type Type
  30 instance == Type where
  31         (==) (TVar a) (TVar b) = a == b
  32         (==) TInt TInt = True
  33         (==) TBool TBool = True
  34         (==) TChar TChar = True
  35         (==) (TFun a1 a2) (TFun b1 b2) = a1 == b1 && a2 == b2
  36         (==) _ _ = False
  37 instance toString Type where
  38         toString (TVar s) = toString s
  39         toString TInt = "Int"
  40         toString TBool = "Bool"
  41         toString TChar = "Char"
  42         toString (TFun t1 t2) = toString t1 +++ " -> " +++ toString t2
  43 :: Scheme = Scheme [[Char]] Type
  44 class Types a where
  45         ftv :: a -> [[Char]]
  46         apply :: Subst a -> a
  47 instance Types Type where
  48         ftv (TVar n) = [n]
  49         ftv TInt = []
  50         ftv TBool = []
  51         ftv TChar = []
  52         ftv (TFun t1 t2) = union (ftv t1) (ftv t2)
  53
  54         apply s (TVar n) = case 'DM'.get n s of
  55                 Nothing = TVar n
  56                 Just t = t
  57         apply s (TFun t1 t2) = TFun (apply s t1) (apply s t2)
  58         apply s t = t
  59 instance Types Scheme where
  60         ftv (Scheme vars t) = difference (ftv t) vars
  61         apply s (Scheme vars t) = Scheme vars (apply (foldr 'DM'.del s vars) t)
  62 instance Types [a] | Types a where
  63         ftv l = foldr union [] (map ftv l)
  64         apply s l = map (apply s) l
  65
  66 :: Subst :== 'DM'.Map [Char] Type
  67 composeSubst s1 s2 = 'DM'.union ((apply s1) <$> s2) s1
  68
  69 :: TypeEnv = TypeEnv ('DM'.Map [Char] Scheme)
  70 remove :: TypeEnv [Char] -> TypeEnv
  71 remove (TypeEnv env) var = TypeEnv ('DM'.del var env)
  72
  73 instance Types TypeEnv where
  74         ftv (TypeEnv env) = ftv ('DM'.elems env)
  75         apply s (TypeEnv env) = TypeEnv (apply s <$> env)
  76
  77 generalize :: TypeEnv Type -> Scheme
  78 generalize env t = Scheme (difference (ftv t) (ftv env)) t
  79
  80 :: TI a :== RWST TIEnv () TIState (Either [String]) a
  81 :: TIState = {tiSupply :: Int, tiSubst :: Subst}
  82 :: TIEnv :== [Int]
  83
  84 mgu :: Type Type -> TI Subst
  85 mgu (TFun l r) (TFun l` r`) = composeSubst <$> mgu l l` <*> mgu r r`
  86 mgu (TVar u) t = varBind u t
  87 mgu t (TVar u) = varBind u t
  88 mgu TInt TInt = pure 'DM'.newMap
  89 mgu TBool TBool = pure 'DM'.newMap
  90 mgu TChar TChar = pure 'DM'.newMap
  91 mgu t1 t2 = liftT (Left ["cannot unify: " +++ toString t1 +++ " with " +++ toString t2])
  92
  93 varBind :: [Char] Type -> TI Subst
  94 varBind u t
  95         | t == TVar u = pure 'DM'.newMap
  96         | isMember u (ftv t) = liftT (Left ["occur check fails: " +++ toString u +++ " vs. " +++ toString t])
  97         = pure ('DM'.singleton u t)
  98
  99 newTyVar :: [Char] -> TI Type
 100 newTyVar prefix
 101         =   get
 102         >>= \t->put {t & tiSupply=t.tiSupply+1}
 103         >>| pure (TVar (prefix ++ fromString (toString t.tiSupply)))
 104
 105 instantiate :: Scheme -> TI Type
 106 instantiate (Scheme vars t)
 107         = mapM (\_->newTyVar ['a']) vars
 108         >>= \nvars->pure (apply ('DM'.fromList (zip2 vars nvars)) t)
 109
 110 class infer a :: TypeEnv a -> TI (Subst, Type)
 111 instance infer Value where
 112         infer _ (Int _) = pure ('DM'.newMap, TInt)
 113         infer _ (Bool _) = pure ('DM'.newMap, TBool)
 114         infer _ (Char _) = pure ('DM'.newMap, TChar)
 115 instance infer Expression where
 116         infer e (Lit a) = infer e a
 117         infer (TypeEnv env) (Var v) = case 'DM'.get v env of
 118                 Nothing = liftT (Left ["unbound variable: " +++ toString v])
 119                 Just s = instantiate s >>= \t->pure ('DM'.newMap, t)
 120         infer env (App e1 e2)
 121                 =              newTyVar ['a']
 122                 >>= \tv      ->infer env e1
 123                 >>= \(s1, t1)->infer (apply s1 env) e2
 124                 >>= \(s2, t2)->mgu (apply s2 t1) (TFun t2 tv)
 125                 >>= \s3->pure (composeSubst s3 (composeSubst s2 s1), apply s3 tv)
 126         //infer env (Lambda s e)
 127         //      =        newTyVar ['l']
 128         //      >>= \tv->pure undef//inEnv (s, Forall [] tv) (infer e)
 129         //      >>= \t-> pure (TFun tv t)