sem.icl

   1 implementation module sem
   2
   3 import qualified Data.Map as Map
   4
   5 from Data.Func import $
   6 from StdFunc import o, flip, const, id
   7
   8 import Control.Monad
   9 import Control.Monad.Trans
  10 import Control.Monad.State
  11 import Data.Either
  12 import Data.Maybe
  13 import Data.Monoid
  14 import Data.List
  15 import Data.Functor
  16 import Data.Tuple
  17
  18 import StdString
  19 import StdTuple
  20 import StdList
  21 import StdMisc
  22 import StdEnum
  23 import GenEq
  24
  25 from Text import class Text(concat), instance Text String
  26
  27 import AST
  28
  29
  30 :: Scheme = Forall [TVar] Type
  31 :: Gamma :== 'Map'.Map String Scheme //map from Variables! to types
  32 :: Substitution :== 'Map'.Map TVar Type
  33 :: Constraints :== [(Type, Type)]
  34 :: SemError
  35         = ParseError Pos String
  36         | UnifyError Pos Type Type
  37     | InfiniteTypeError Pos Type
  38     | FieldSelectorError Pos Type FieldSelector
  39         | OperatorError Pos Op2 Type
  40     | UndeclaredVariableError Pos String
  41     | ArgumentMisMatchError Pos String
  42         | SanityError Pos String
  43         | Error String
  44
  45 instance zero Gamma where
  46         zero = 'Map'.newMap
  47
  48 variableStream :: [TVar]
  49 variableStream = map toString [1..]
  50
  51 sem :: AST -> Either [SemError] Constraints
  52 sem (AST fd) = case foldM (const $ hasNoDups fd) () fd
  53                 >>| foldM (const isNiceMain) () fd
  54                 >>| hasMain fd of
  55         Left e = Left [e]
  56     _ = Right []
  57         //_ = case execRWST (constraints fd) zero variableStream of
  58         //      Left e = Left [e]
  59         //      Right (a, b) = Right b
  60 where
  61                 constraints :: [FunDecl] -> Typing ()
  62         constraints _ = pure ()
  63         //TODO: fix
  64                 //constraints fds = mapM_ funconstraint fds >>| pure ()
  65
  66                 funconstraint :: FunDecl -> Typing ()
  67                 funconstraint fd=:(FunDecl _ ident args mt vardecls stmts) = case mt of
  68                         Nothing = abort "Cannot infer functions yet"
  69             _ = pure ()
  70                         //Just t = inEnv (ident, (Forall [] t)) (
  71                         //      mapM_ vardeclconstraint vardecls >>| pure ())
  72
  73                 vardeclconstraint :: VarDecl -> Typing ()
  74         vardeclconstraint _ = pure ()
  75         //TODO: fix!
  76                 //vardeclconstraint (VarDecl p mt ident expr) = infer expr
  77                         //>>= \it->inEnv (ident, (Forall [] it)) (pure ())
  78
  79                 hasNoDups :: [FunDecl] FunDecl -> Either SemError ()
  80                 hasNoDups fds (FunDecl p n _ _ _ _)
  81                 # mbs = map (\(FunDecl p` n` _ _ _ _)->if (n == n`) (Just p`) Nothing) fds
  82                 = case catMaybes mbs of
  83                         [] = Left $ SanityError p "HUH THIS SHOULDN'T HAPPEN"
  84                         [x] = pure ()
  85                         [_:x] = Left $ SanityError p (concat
  86                                 [n, " multiply defined at ", toString p])
  87
  88                 hasMain :: [FunDecl] -> Either SemError ()
  89                 hasMain [(FunDecl _ "main" _ _ _ _):fd] = pure ()
  90                 hasMain [_:fd] = hasMain fd
  91                 hasMain [] = Left $ SanityError zero "no main function defined"
  92
  93                 isNiceMain :: FunDecl -> Either SemError ()
  94                 isNiceMain (FunDecl p "main" as mt _ _) = case (as, mt) of
  95                         ([_:_], _) = Left $ SanityError p "main must have arity 0"
  96                         ([], t) = (case t of
  97                                 Nothing = pure ()
  98                                 Just VoidType = pure ()
  99                                 _ = Left $ SanityError p "main has to return Void")
 100                 isNiceMain _ = pure ()
 101
 102 instance toString Scheme where
 103         toString (Forall x t) =
 104                 concat ["Forall ": map ((+++) "\n") x] +++ toString t
 105
 106 instance toString Gamma where
 107         toString mp =
 108                 concat [concat [k, ": ", toString v, "\n"]\\(k, v)<-'Map'.toList mp]
 109
 110 instance toString SemError where
 111         toString (SanityError p e) = concat [toString p,
 112                 "SemError: SanityError: ", e]
 113         toString se = "SemError: "
 114
 115 class Typeable a where
 116     ftv :: a -> [TVar]
 117     subst :: Substitution a -> a
 118
 119 instance Typeable Scheme where
 120     ftv (Forall bound t) = difference (ftv t) bound
 121     subst s (Forall bound t) = Forall bound $ subst s_ t
 122         where s_ = 'Map'.filterWithKey (\k _ -> not (elem k bound)) s
 123
 124 instance Typeable [a] | Typeable a where
 125     ftv types   = foldr (\t ts-> ftv t ++ ts) [] types
 126     subst s ts  = map (\t->subst s t) ts
 127
 128 instance Typeable Type where
 129     ftv (TupleType (t1, t2))    = ftv t1 ++ ftv t2
 130     ftv (ListType t)            = ftv t
 131     ftv (IdType tvar)           = [tvar]
 132     ftv (t1 ->> t2)             = ftv t1 ++ ftv t2
 133     ftv _                       = []
 134     subst s (TupleType (t1, t2))= TupleType (subst s t1, subst s t2)
 135     subst s (ListType t1)       = ListType (subst s t1)
 136     subst s (t1 ->> t2)         = (subst s t1) ->> (subst s t2)
 137     subst s t1=:(IdType tvar)   = 'Map'.findWithDefault t1 tvar s
 138     subst s t                   = t
 139
 140 instance Typeable Gamma where
 141     ftv gamma       = concatMap id $ map ftv ('Map'.elems gamma)
 142     subst s gamma   = Mapmap (subst s) gamma
 143
 144 //// ------------------------
 145 //// algorithm U, Unification
 146 //// ------------------------
 147 instance zero Substitution where zero = 'Map'.newMap
 148
 149 compose :: Substitution Substitution -> Substitution
 150 compose s1 s2 = 'Map'.union (Mapmap (subst s1) s2) s1
 151 //Note: unlike function composition, compose is left biased!
 152
 153 occurs :: TVar a -> Bool | Typeable a
 154 occurs tvar a = elem tvar (ftv a)
 155
 156 unify :: Type Type -> Either SemError Substitution
 157 unify t1=:(IdType tv) t2 = unify t2 t1
 158 unify t1 t2=:(IdType tv)    | t1 == (IdType tv) = Right zero
 159                             | occurs tv t1 = Left $ InfiniteTypeError zero t1
 160                             | otherwise = Right $ 'Map'.singleton tv t1
 161 unify (ta1->>ta2) (tb1->>tb2) = unify ta1 tb1 >>= \s1->
 162                                 unify tb1 tb2 >>= \s2->
 163                                 Right $ compose s1 s2
 164 unify (TupleType (ta1,ta2)) (TupleType (tb1,tb2)) = unify ta1 tb1 >>= \s1->
 165                                                     unify ta2 tb2 >>= \s2->
 166                                                     Right $ compose s1 s2
 167 unify (ListType t1) (ListType t2) = unify t1 t2
 168 unify t1 t2 | t1 == t2  = Right zero
 169             | otherwise = Left $ UnifyError zero t1 t2
 170
 171 //// ------------------------
 172 //// Algorithm M, Inference and Solving
 173 //// ------------------------
 174 //The typing monad
 175 :: Typing a :== StateT (Gamma, [TVar]) (Either SemError) a
 176 gamma :: Typing Gamma
 177 gamma = gets fst
 178 putGamma :: Gamma -> Typing ()
 179 putGamma g = modify (appFst $ const g) >>| pure ()
 180 withGamma :: (Gamma -> Gamma) -> Typing ()
 181 withGamma f = modify (appFst f) >>| pure ()
 182 fresh :: Typing Type
 183 fresh = gets snd >>= \vars->
 184         modify (appSnd $ const $ tail vars) >>|
 185         pure (IdType (head vars))
 186
 187 //instantiate maps a schemes type variables to variables with fresh names
 188 //and drops the quantification: i.e. forall a,b.a->[b] becomes c->[d]
 189 instantiate :: Scheme -> Typing Type
 190 instantiate (Forall bound t) =
 191     mapM (const fresh) bound >>= \newVars->
 192     let s = 'Map'.fromList (zip (bound,newVars)) in
 193     pure (subst s t)
 194 //generalize quentifies all free type variables in a type which are not
 195 //in the gamma
 196 generalize :: Type -> Typing Scheme
 197 generalize t = gamma >>= \g-> pure $ Forall (difference (ftv t) (ftv g)) t
 198
 199
 200
 201
 202
 203 Mapmap :: (a->b) ('Map'.Map k a) -> ('Map'.Map k b)
 204 Mapmap _ 'Map'.Tip = 'Map'.Tip
 205 Mapmap f ('Map'.Bin sz k v ml mr) = 'Map'.Bin sz k (f v)
 206                                         (Mapmap f ml)
 207                                         (Mapmap f mr)
 208
 209 //// ------------------------
 210 //// First step: Inference
 211 //// ------------------------//
 212
 213 //unify :: Type Type -> Infer ()
 214 //unify t1 t2 = tell [(t1, t2)]//
 215
 216 //fresh :: Infer Type
 217 //fresh = (gets id) >>= \vars-> (put $ tail vars) >>| (pure $ IdType $ head vars)//
 218
 219 //op2Type :: Op2 -> Infer Type
 220 //op2Type op
 221 //| elem op [BiPlus, BiMinus, BiTimes, BiDivide, BiMod]
 222 //      = pure (IntType ->> IntType ->> IntType)
 223 //| elem op [BiEquals, BiUnEqual]
 224 //      = fresh >>= \t1-> fresh >>= \t2-> pure (t1 ->> t2 ->> BoolType)
 225 //| elem op [BiLesser, BiGreater, BiLesserEq, BiGreaterEq]
 226 //      = pure (IntType ->> IntType ->> BoolType)
 227 //| elem op [BiAnd, BiOr]
 228 //      = pure (BoolType ->> BoolType ->> BoolType)
 229 //| op == BiCons
 230 //      = fresh >>= \t1-> pure (t1 ->> ListType t1 ->> ListType t1)//
 231
 232 //op1Type :: Op1 -> Infer Type
 233 //op1Type UnNegation = pure $ (BoolType ->> BoolType)
 234 //op1Type UnMinus = pure $ (IntType ->> IntType)//
 235
 236 ////instantiate :: Scheme -> Infer Type
 237 ////instantiate (Forall as t) = mapM (const fresh) as//
 238
 239 //lookupEnv :: String -> Infer Type
 240 //lookupEnv ident = asks ('Map'.get ident)
 241 //      >>= \m->case m of
 242 //              Nothing = liftT $ Left $ UndeclaredVariableError zero ident
 243 //              Just (Forall as t) = pure t //instantiate ???//
 244
 245 //class infer a :: a -> Infer Type
 246 //instance infer Expr where
 247 //      infer (VarExpr _ (VarDef ident fs)) = lookupEnv ident
 248 //    infer (Op2Expr _ e1 op e2) =
 249 //        infer e1 >>= \t1 ->
 250 //        infer e2 >>= \t2 ->
 251 //        fresh >>= \frsh ->
 252 //        let given = t1 ->> (t2 ->> frsh) in
 253 //        op2Type op >>= \expected ->
 254 //        unify expected given >>|
 255 //        return frsh
 256 //      infer (Op1Expr _ op e) =
 257 //        infer e >>= \t1 ->
 258 //        fresh >>= \frsh ->
 259 //        let given = t1 ->> frsh in
 260 //        op1Type op >>= \expected ->
 261 //        unify expected given >>|
 262 //        pure frsh
 263 //      infer (IntExpr _ _) = pure IntType
 264 //      infer (CharExpr _ _) = pure CharType
 265 //      infer (BoolExpr _ _) = pure BoolType
 266 //      infer (FunExpr _ f args sels) =  //todo, iets met field selectors
 267 //        lookupEnv f >>= \expected ->
 268 //        fresh >>= \frsh ->
 269 //        mapM infer args >>= \argTypes ->
 270 //        let given = foldr (->>) frsh argTypes in
 271 //        unify expected given >>|
 272 //        pure frsh
 273 //      infer (EmptyListExpr _) = ListType <$> fresh
 274 //      infer (TupleExpr _ (e1, e2)) =
 275 //              infer e1 >>= \et1->infer e2 >>= \et2->pure $ TupleType (et1, et2)//
 276
 277 ////:: VarDef = VarDef String [FieldSelector]
 278 ////:: FieldSelector = FieldHd | FieldTl | FieldFst | FieldSnd
 279 ////:: Op1 = UnNegation | UnMinus
 280 ////:: Op2 = BiPlus | BiMinus | BiTimes | BiDivide | BiMod | BiEquals | BiLesser |
 281 ////    BiGreater | BiLesserEq | BiGreaterEq | BiUnEqual | BiAnd | BiOr | BiCons
 282 ////:: FunDecl = FunDecl Pos String [String] (Maybe Type) [VarDecl] [Stmt]
 283 ////:: FunCall = FunCall String [Expr]
 284 ////:: Stmt
 285 ////    = IfStmt Expr [Stmt] [Stmt]
 286 ////    | WhileStmt Expr [Stmt]
 287 ////    | AssStmt VarDef Expr
 288 ////    | FunStmt FunCall
 289 ////    | ReturnStmt (Maybe Expr)
 290 ////:: Pos = {line :: Int, col :: Int}
 291 ////:: AST = AST [VarDecl] [FunDecl]
 292 ////:: VarDecl = VarDecl Pos Type String Expr
 293 ////:: Type
 294 ////    = TupleType (Type, Type)
 295 ////    | ListType Type
 296 ////    | IdType String
 297 ////    | IntType
 298 ////    | BoolType
 299 ////    | CharType
 300 ////    | VarType
 301 ////    | VoidType
 302 ////    | (->>) infixl 7 Type Type