check.icl

   1 implementation module check
   2
   3 import StdEnv
   4
   5 import Data.Either
   6 import Data.List
   7 import Control.Monad
   8
   9 import ast
  10
  11 check :: [Function] -> Either [String] Expression
  12 check fs
  13         # dups = filter (\x->length x > 1) (groupBy (\(Function i _ _) (Function j _ _)->i == j) fs)
  14         | length dups > 0 = Left ["Duplicate functions: ":[toString n\\[(Function n _ _):_]<-dups]]
  15         = case partition (\a->a=:(Function ['start'] _ _)) fs of
  16                 ([], _) = Left ["No start function defined"]
  17                 ([Function _ [] e], fs) = Right (foldr (\(Function i a e)->Let i a e) e fs)
  18                 ([Function _ _ _], _) = Left ["Start cannot have arguments"]
  19 where
  20         funs = [i\\(Function i _ _)<-fs]
  21
  22 //import qualified Data.Map as DM
  23 //from Data.Map import instance Functor (Map k)
  24 //import qualified Data.Set as DS
  25 //import Data.Functor
  26 //import Data.Func
  27 //import Data.Either
  28 //import Data.List
  29 //import Data.Maybe
  30 //import Control.Applicative
  31 //import Control.Monad
  32 //import Control.Monad.Trans
  33 //import qualified Control.Monad.State as MS
  34 //import Control.Monad.State => qualified gets, put, modify
  35 //import Control.Monad.RWST => qualified put
  36 //
  37 //import ast
  38 //
  39 //check :: AST -> Either [String] (AST, [([Char], Scheme)])
  40 //check (AST fs) = pure (AST fs, [])/*case inferAST preamble fs of
  41 //      Left e = Left e
  42 //      Right s = Right (AST fs, 'DM'.toList s)
  43 //where
  44 //      preamble = 'DM'.fromList
  45 //              [(['if'], Forall [['a']] $ TFun TBool $ TFun (TVar ['a']) $ TFun (TVar ['a']) $ TVar ['a'])
  46 //              ,(['eq'], Forall [] $ TFun TInt $ TFun TInt TBool)
  47 //              ,(['mul'], Forall [] $ TFun TInt $ TFun TInt TInt)
  48 //              ,(['div'], Forall [] $ TFun TInt $ TFun TInt TInt)
  49 //              ,(['add'], Forall [] $ TFun TInt $ TFun TInt TInt)
  50 //              ,(['sub'], Forall [] $ TFun TInt $ TFun TInt TInt)
  51 //              ]
  52 //*/
  53 //
  54 //:: TypeEnv    :== 'DM'.Map [Char] Scheme
  55 //:: Constraint :== (Type, Type)
  56 //:: Subst      :== 'DM'.Map [Char] Type
  57 //:: Unifier    :== (Subst, [Constraint])
  58 //:: Infer a    :== RWST TypeEnv [Constraint] InferState (Either [String]) a
  59 //:: InferState =   { count :: Int }
  60 //:: Scheme     =   Forall [[Char]] Type
  61 //:: Solve a    :== StateT Unifier (Either [String]) a
  62 //
  63 //nullSubst :: Subst
  64 //nullSubst = 'DM'.newMap
  65 //
  66 //uni :: Type Type -> Infer ()
  67 //uni t1 t2 = tell [(t1, t2)]
  68 //
  69 //inEnv :: ([Char], Scheme) (Infer a) -> Infer a
  70 //inEnv (x, sc) m = local (\e->'DM'.put x sc $ 'DM'.del x e) m
  71 //
  72 //letters :: [[Char]]
  73 //letters = [1..] >>= flip replicateM ['a'..'z']
  74 //
  75 //fresh :: Infer Type
  76 //fresh = get >>= \s=:{count}->'Control.Monad.RWST'.put {s & count=count + 1} >>| pure (TVar $ letters !! count)
  77 //
  78 //class Substitutable a
  79 //where
  80 //      apply :: Subst a -> a
  81 //      ftv   :: a -> [[Char]]
  82 //
  83 //instance Substitutable Type
  84 //where
  85 //      apply s t=:(TVar a) = maybe t id $ 'DM'.get a s
  86 //      apply s (TFun t1 t2)  = TFun (apply s t1) (apply s t2)
  87 //      apply _ t = t
  88 //
  89 //      ftv (TVar a)     = [a]
  90 //      ftv (TFun t1 t2) = union (ftv t1) (ftv t2)
  91 //      ftv t            = []
  92 //
  93 //instance Substitutable Scheme
  94 //where
  95 //      apply s (Forall as t)   = Forall as $ apply (foldr 'DM'.del s as) t
  96 //      ftv (Forall as t) = difference (ftv t) as
  97 //
  98 //instance Substitutable [a] | Substitutable a
  99 //where
 100 //      apply s ls = map (apply s) ls
 101 //      ftv t = foldr (union o ftv) [] t
 102 //
 103 //instance Substitutable TypeEnv where
 104 //      apply s env = fmap (apply s) env
 105 //      ftv env = ftv $ 'DM'.elems env
 106 //
 107 //instance Substitutable Constraint where
 108 //      apply s (t1, t2) = (apply s t1, apply s t2)
 109 //      ftv (t1, t2) = union (ftv t1) (ftv t2)
 110 //
 111 //instantiate ::  Scheme -> Infer Type
 112 //instantiate (Forall as t) = mapM (const fresh) as
 113 //      >>= \as`->let s = 'DM'.fromList $ zip2 as as` in pure $ apply s t
 114 //
 115 //generalize :: TypeEnv Type -> Scheme
 116 //generalize env t = Forall (difference (ftv t) (ftv env)) t
 117 //
 118 ////:: Expression
 119 ////    = Lit Value
 120 ////    | Var [Char]
 121 ////    | App Expression Expression
 122 ////    | Lambda [Char] Expression
 123 ////    | Builtin [Char] [Expression]
 124 //inferExpr :: TypeEnv Expression -> Either [String] Scheme
 125 //inferExpr env ex = case runRWST (infer ex) env {count=0} of
 126 //      Left e = Left e
 127 //      Right (ty, st, cs) = case runStateT solver ('DM'.newMap, cs) of
 128 //              Left e = Left e
 129 //              Right (s, _) = Right (closeOver (apply s ty))
 130 //
 131 //closeOver :: Type -> Scheme
 132 //closeOver t = normalize (generalize 'DM'.newMap t)
 133 //
 134 //normalize :: Scheme -> Scheme
 135 //normalize t = t
 136 //
 137 //inferAST :: TypeEnv [Function] -> Either [String] TypeEnv
 138 //inferAST env [] = Right env
 139 //inferAST env [Function name args body:rest] = case inferExpr env (foldr Lambda body args) of
 140 //      Left e = Left e
 141 //      Right ty = inferAST ('DM'.put name ty env) rest
 142 //
 143 //inferFunc :: [Function] -> Infer ()
 144 //inferFunc [] = pure ()
 145 //inferFunc [Function name args body:rest]
 146 //      =      ask
 147 //      >>= \en->infer (foldr Lambda body args)
 148 //      >>= \t1->inEnv (name, generalize en t1) (inferFunc rest)
 149 //      >>= \_->pure ()
 150 //
 151 //infer :: Expression -> Infer Type
 152 //infer (Lit v) = case v of
 153 //      Int  _ = pure TInt
 154 //      Bool _ = pure TBool
 155 //infer (Var s) = asks ('DM'.get s)
 156 //      >>= maybe (liftT $ Left ["Unbound variable " +++ toString s]) instantiate
 157 //infer (App e1 e2)
 158 //      =        infer e1
 159 //      >>= \t1->infer e2
 160 //      >>= \t2->fresh
 161 //      >>= \tv->uni t1 (TFun t2 tv)
 162 //      >>|      pure tv
 163 //infer (Lambda s e)
 164 //      =        fresh
 165 //      >>= \tv->inEnv (s, Forall [] tv) (infer e)
 166 //      >>= \t-> pure (TFun tv t)
 167 ////infer (Let x e1 e2)
 168 ////    =        ask
 169 ////    >>= \en->infer e1
 170 ////    >>= \t1->inEnv (x, generalize en t1) (infer e2)
 171 //
 172 //unifies :: Type Type -> Solve Unifier
 173 //unifies TInt TInt = pure ('DM'.newMap, [])
 174 //unifies TBool TBool = pure ('DM'.newMap, [])
 175 //unifies (TVar a) (TVar b)
 176 //      | a == b = pure ('DM'.newMap, [])
 177 //unifies (TVar v) t = tbind v t
 178 //unifies t (TVar v) = tbind v t
 179 //unifies (TFun t1 t2) (TFun t3 t4) = unifyMany [t1, t2] [t3, t4]
 180 //unifies t1 t2 = liftT $ Left ["Cannot unify " +++ toString t1 +++ " with " +++ toString t2]
 181 //
 182 //unifyMany :: [Type] [Type] -> Solve Unifier
 183 //unifyMany [] [] = pure ('DM'.newMap, [])
 184 //unifyMany [t1:ts1] [t2:ts2] = unifies t1 t2
 185 //      >>= \(su1, cs1)->unifyMany (apply su1 ts1) (apply su1 ts2)
 186 //      >>= \(su2, cs2)->pure (su2 `compose` su1, cs1 ++ cs2)
 187 //unifyMany t1 t2 = liftT $ Left ["Length difference in unifyMany"]
 188 //
 189 //(`compose`) infix 1 :: Subst Subst -> Subst
 190 //(`compose`) s1 s2 = 'DM'.union (apply s1 <$> s2) s1
 191 //
 192 //tbind ::  [Char] Type -> Solve Unifier
 193 //tbind a (TVar b)
 194 //      | a == b = pure ('DM'.newMap, [])
 195 //tbind a t
 196 //      | occursCheck a t = liftT $ Left ["Infinite type " +++ toString a +++ toString t]
 197 //      = pure $ ('DM'.singleton a t, [])
 198 //
 199 //occursCheck ::  [Char] a -> Bool | Substitutable a
 200 //occursCheck a t = isMember a $ ftv t
 201 //
 202 //solver :: Solve Subst
 203 //solver = getState >>= \(su, cs)->case cs of
 204 //      [] = pure su
 205 //      [(t1, t2):cs0] = unifies t1 t2
 206 //              >>= \(su1, cs1)->'MS'.put (su1 `compose` su, cs1 ++ (apply su1 cs0))
 207 //              >>| solver