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 class Typeable a where
 103     ftv :: a -> [TVar]
 104     subst :: Substitution a -> a
 105
 106 instance Typeable Scheme where
 107     ftv (Forall bound t) = difference (ftv t) bound
 108     subst s (Forall bound t) = Forall bound $ subst s_ t
 109         where s_ = 'Map'.filterWithKey (\k _ -> not (elem k bound)) s
 110
 111 instance Typeable [a] | Typeable a where
 112     ftv types   = foldr (\t ts-> ftv t ++ ts) [] types
 113     subst s ts  = map (\t->subst s t) ts
 114
 115 instance Typeable Type where
 116     ftv (TupleType (t1, t2))    = ftv t1 ++ ftv t2
 117     ftv (ListType t)            = ftv t
 118     ftv (IdType tvar)           = [tvar]
 119     ftv (t1 ->> t2)             = ftv t1 ++ ftv t2
 120     ftv _                       = []
 121     subst s (TupleType (t1, t2))= TupleType (subst s t1, subst s t2)
 122     subst s (ListType t1)       = ListType (subst s t1)
 123     subst s (t1 ->> t2)         = (subst s t1) ->> (subst s t2)
 124     subst s t1=:(IdType tvar)   = 'Map'.findWithDefault t1 tvar s
 125     subst s t                   = t
 126
 127 instance Typeable Gamma where
 128     ftv gamma       = concatMap id $ map ftv ('Map'.elems gamma)
 129     subst s gamma   = Mapmap (subst s) gamma
 130
 131 //// ------------------------
 132 //// algorithm U, Unification
 133 //// ------------------------
 134 instance zero Substitution where zero = 'Map'.newMap
 135
 136 compose :: Substitution Substitution -> Substitution
 137 compose s1 s2 = 'Map'.union (Mapmap (subst s2) s1) s2
 138 //Note: just like function compositon compose does snd first
 139
 140 occurs :: TVar a -> Bool | Typeable a
 141 occurs tvar a = elem tvar (ftv a)
 142
 143 unify :: Type Type -> Either SemError Substitution
 144 unify t1=:(IdType tv) t2 = unify t2 t1
 145 unify t1 t2=:(IdType tv)    | t1 == (IdType tv) = Right zero
 146                             | occurs tv t1 = Left $ InfiniteTypeError zero t1
 147                             | otherwise = Right $ 'Map'.singleton tv t1
 148 unify (ta1->>ta2) (tb1->>tb2) = unify ta1 tb1 >>= \s1->
 149                                 unify tb1 tb2 >>= \s2->
 150                                 Right $ compose s1 s2
 151 unify (TupleType (ta1,ta2)) (TupleType (tb1,tb2)) = unify ta1 tb1 >>= \s1->
 152                                                     unify ta2 tb2 >>= \s2->
 153                                                     Right $ compose s1 s2
 154 unify (ListType t1) (ListType t2) = unify t1 t2
 155 unify t1 t2 | t1 == t2  = Right zero
 156             | otherwise = Left $ UnifyError zero t1 t2
 157
 158 //// ------------------------
 159 //// Algorithm M, Inference and Solving
 160 //// ------------------------
 161 //The typing monad
 162 :: Typing a :== StateT (Gamma, [TVar]) (Either SemError) a
 163 gamma :: Typing Gamma
 164 gamma = gets fst
 165 putGamma :: Gamma -> Typing ()
 166 putGamma g = modify (appFst $ const g) >>| pure ()
 167 changeGamma :: (Gamma -> Gamma) -> Typing ()
 168 changeGamma f = modify (appFst f) >>| pure ()
 169 withGamma :: (Gamma -> a) -> Typing a
 170 withGamma f = f <$> gamma
 171 fresh :: Typing Type
 172 fresh = gets snd >>= \vars->
 173         modify (appSnd $ const $ tail vars) >>|
 174         pure (IdType (head vars))
 175
 176 lift :: (Either SemError a) -> Typing a
 177 lift (Left e) = liftT $ Left e
 178 lift (Right v) = pure v
 179
 180 //instantiate maps a schemes type variables to variables with fresh names
 181 //and drops the quantification: i.e. forall a,b.a->[b] becomes c->[d]
 182 instantiate :: Scheme -> Typing Type
 183 instantiate (Forall bound t) =
 184     mapM (const fresh) bound >>= \newVars->
 185     let s = 'Map'.fromList (zip (bound,newVars)) in
 186     pure (subst s t)
 187
 188 //generalize quentifies all free type variables in a type which are not
 189 //in the gamma
 190 generalize :: Type -> Typing Scheme
 191 generalize t = gamma >>= \g-> pure $ Forall (difference (ftv t) (ftv g)) t
 192
 193 lookup :: String -> Typing Scheme
 194 lookup k = gamma >>= \g-> case 'Map'.member k g of
 195     False = liftT (Left $ UndeclaredVariableError zero k)
 196     True = pure ('Map'.find k g)
 197
 198 //The inference class
 199 //When tying it all together we will treat the program is a big
 200 //let x=e1 in let y=e2 in ....
 201 class infer a :: a -> Typing (Substitution, Type)
 202
 203 instance infer Expr where
 204  infer e = case e of
 205     VarExpr _ (VarDef k fs) = (\t->(zero,t)) <$> (lookup k >>= instantiate)
 206     //instantiate is key for the let polymorphism!
 207     //TODO: field selectors
 208
 209     Op2Expr _ e1 op e2 =
 210         infer e1 >>= \(s1, t1) ->
 211         infer e2 >>= \(s2, t2) ->
 212         fresh >>= \tv ->
 213         let given = t1 ->> t2 ->> tv in
 214         op2Type op >>= \expected ->
 215         lift (unify expected given) >>= \s3 ->
 216         pure ((compose s1 $ compose s2 s3), subst s3 tv)
 217
 218     Op1Expr _ op e1 =
 219         infer e1 >>= \(s1, t1) ->
 220         fresh >>= \tv ->
 221         let given = t1 ->> tv in
 222         op1Type op >>= \expected ->
 223         lift (unify expected given) >>= \s2 ->
 224         pure (compose s1 s2, subst s2 tv)
 225
 226     EmptyListExpr _ = (\tv->(zero,tv)) <$> fresh
 227
 228     TupleExpr _ (e1, e2) =
 229         infer e1 >>= \(s1, t1) ->
 230         infer e2 >>= \(s2, t2) ->
 231         pure (compose s1 s2, TupleType (t1,t2))
 232
 233     FunExpr _ f args fs = //todo: fieldselectors
 234         lookup f >>= instantiate >>= \expected ->
 235         let accTypSub = (\(s,ts) e->infer e >>= \(s_,et)->pure (compose s_ s,ts++[et])) in
 236         foldM accTypSub (zero,[]) args >>= \(s1, argTs)->
 237         fresh >>= \tv->
 238         let given = foldr (->>) tv argTs in
 239         lift (unify expected given) >>= \s2->
 240         pure (compose s1 s2, subst s2 tv)
 241
 242     IntExpr _ _ = pure $ (zero, IntType)
 243     BoolExpr _ _ = pure $ (zero, BoolType)
 244     CharExpr _ _ = pure $ (zero, CharType)
 245
 246
 247 op2Type :: Op2 -> Typing Type
 248 op2Type op
 249 | elem op [BiPlus, BiMinus, BiTimes, BiDivide, BiMod]
 250   = pure (IntType ->> IntType ->> IntType)
 251 | elem op [BiEquals, BiUnEqual]
 252   = fresh >>= \t1-> fresh >>= \t2-> pure (t1 ->> t2 ->> BoolType)
 253 | elem op [BiLesser, BiGreater, BiLesserEq, BiGreaterEq]
 254   = pure (IntType ->> IntType ->> BoolType)
 255 | elem op [BiAnd, BiOr]
 256   = pure (BoolType ->> BoolType ->> BoolType)
 257 | op == BiCons
 258   = fresh >>= \t1-> pure (t1 ->> ListType t1 ->> ListType t1)
 259
 260 op1Type :: Op1 -> Typing Type
 261 op1Type UnNegation = pure $ (BoolType ->> BoolType)
 262 op1Type UnMinus = pure $ (IntType ->> IntType)
 263
 264
 265 Mapmap :: (a->b) ('Map'.Map k a) -> ('Map'.Map k b)
 266 Mapmap _ 'Map'.Tip = 'Map'.Tip
 267 Mapmap f ('Map'.Bin sz k v ml mr) = 'Map'.Bin sz k (f v)
 268                                         (Mapmap f ml)
 269                                         (Mapmap f mr)
 270
 271 instance toString Scheme where
 272     toString (Forall x t) =
 273         concat ["Forall ": map ((+++) "\n") x] +++ toString t
 274
 275 instance toString Gamma where
 276     toString mp =
 277         concat [concat [k, ": ", toString v, "\n"]\\(k, v)<-'Map'.toList mp]
 278
 279 instance toString SemError where
 280     toString (SanityError p e) = concat [toString p,
 281         "SemError: SanityError: ", e]
 282     toString se = "SemError: "
 283
 284 instance MonadTrans (StateT (Gamma, [TVar])) where
 285     liftT m = StateT \s-> m >>= \a-> return (a, s)
 286
 287 //// ------------------------
 288 //// First step: Inference
 289 //// ------------------------//
 290
 291 //unify :: Type Type -> Infer ()
 292 //unify t1 t2 = tell [(t1, t2)]//
 293
 294 //fresh :: Infer Type
 295 //fresh = (gets id) >>= \vars-> (put $ tail vars) >>| (pure $ IdType $ head vars)//
 296
 297 //op2Type :: Op2 -> Infer Type
 298 //op2Type op
 299 //| elem op [BiPlus, BiMinus, BiTimes, BiDivide, BiMod]
 300 //      = pure (IntType ->> IntType ->> IntType)
 301 //| elem op [BiEquals, BiUnEqual]
 302 //      = fresh >>= \t1-> fresh >>= \t2-> pure (t1 ->> t2 ->> BoolType)
 303 //| elem op [BiLesser, BiGreater, BiLesserEq, BiGreaterEq]
 304 //      = pure (IntType ->> IntType ->> BoolType)
 305 //| elem op [BiAnd, BiOr]
 306 //      = pure (BoolType ->> BoolType ->> BoolType)
 307 //| op == BiCons
 308 //      = fresh >>= \t1-> pure (t1 ->> ListType t1 ->> ListType t1)//
 309
 310 //op1Type :: Op1 -> Infer Type
 311 //op1Type UnNegation = pure $ (BoolType ->> BoolType)
 312 //op1Type UnMinus = pure $ (IntType ->> IntType)//
 313
 314 ////instantiate :: Scheme -> Infer Type
 315 ////instantiate (Forall as t) = mapM (const fresh) as//
 316
 317 //lookupEnv :: String -> Infer Type
 318 //lookupEnv ident = asks ('Map'.get ident)
 319 //      >>= \m->case m of
 320 //              Nothing = liftT $ Left $ UndeclaredVariableError zero ident
 321 //              Just (Forall as t) = pure t //instantiate ???//
 322
 323 //class infer a :: a -> Infer Type
 324 //instance infer Expr where
 325 //      infer (VarExpr _ (VarDef ident fs)) = lookupEnv ident
 326 //    infer (Op2Expr _ e1 op e2) =
 327 //        infer e1 >>= \t1 ->
 328 //        infer e2 >>= \t2 ->
 329 //        fresh >>= \frsh ->
 330 //        let given = t1 ->> (t2 ->> frsh) in
 331 //        op2Type op >>= \expected ->
 332 //        unify expected given >>|
 333 //        return frsh
 334 //      infer (Op1Expr _ op e) =
 335 //        infer e >>= \t1 ->
 336 //        fresh >>= \frsh ->
 337 //        let given = t1 ->> frsh in
 338 //        op1Type op >>= \expected ->
 339 //        unify expected given >>|
 340 //        pure frsh
 341 //      infer (IntExpr _ _) = pure IntType
 342 //      infer (CharExpr _ _) = pure CharType
 343 //      infer (BoolExpr _ _) = pure BoolType
 344 //      infer (FunExpr _ f args sels) =  //todo, iets met field selectors
 345 //        lookupEnv f >>= \expected ->
 346 //        fresh >>= \frsh ->
 347 //        mapM infer args >>= \argTypes ->
 348 //        let given = foldr (->>) frsh argTypes in
 349 //        unify expected given >>|
 350 //        pure frsh
 351 //      infer (EmptyListExpr _) = ListType <$> fresh
 352 //      infer (TupleExpr _ (e1, e2)) =
 353 //              infer e1 >>= \et1->infer e2 >>= \et2->pure $ TupleType (et1, et2)//
 354
 355 ////:: VarDef = VarDef String [FieldSelector]
 356 ////:: FieldSelector = FieldHd | FieldTl | FieldFst | FieldSnd
 357 ////:: Op1 = UnNegation | UnMinus
 358 ////:: Op2 = BiPlus | BiMinus | BiTimes | BiDivide | BiMod | BiEquals | BiLesser |
 359 ////    BiGreater | BiLesserEq | BiGreaterEq | BiUnEqual | BiAnd | BiOr | BiCons
 360 ////:: FunDecl = FunDecl Pos String [String] (Maybe Type) [VarDecl] [Stmt]
 361 ////:: FunCall = FunCall String [Expr]
 362 ////:: Stmt
 363 ////    = IfStmt Expr [Stmt] [Stmt]
 364 ////    | WhileStmt Expr [Stmt]
 365 ////    | AssStmt VarDef Expr
 366 ////    | FunStmt FunCall
 367 ////    | ReturnStmt (Maybe Expr)
 368 ////:: Pos = {line :: Int, col :: Int}
 369 ////:: AST = AST [VarDecl] [FunDecl]
 370 ////:: VarDecl = VarDecl Pos Type String Expr
 371 ////:: Type
 372 ////    = TupleType (Type, Type)
 373 ////    | ListType Type
 374 ////    | IdType String
 375 ////    | IntType
 376 ////    | BoolType
 377 ////    | CharType
 378 ////    | VarType
 379 ////    | VoidType
 380 ////    | (->>) infixl 7 Type Type