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
 208     Op2Expr _ e1 op e2 =
 209         infer e1 >>= \(s1, t1) ->
 210         infer e2 >>= \(s2, t2) ->
 211         fresh >>= \tv ->
 212         let given = t1 ->> t2 ->> tv in
 213         op2Type op >>= \expected ->
 214         lift (unify expected given) >>= \s3 ->
 215         pure ((compose s1 $ compose s2 s3), subst s3 tv)
 216
 217     Op1Expr _ op e1 =
 218         infer e1 >>= \(s1, t1) ->
 219         fresh >>= \tv ->
 220         let given = t1 ->> tv in
 221         op1Type op >>= \expected ->
 222         lift (unify expected given) >>= \s2 ->
 223         pure ((compose s1 s2), subst s2 tv)
 224
 225
 226
 227     IntExpr _ _ = pure $ (zero, IntType)
 228     BoolExpr _ _ = pure $ (zero, BoolType)
 229     CharExpr _ _ = pure $ (zero, CharType)
 230
 231
 232 op2Type :: Op2 -> Typing Type
 233 op2Type op
 234 | elem op [BiPlus, BiMinus, BiTimes, BiDivide, BiMod]
 235   = pure (IntType ->> IntType ->> IntType)
 236 | elem op [BiEquals, BiUnEqual]
 237   = fresh >>= \t1-> fresh >>= \t2-> pure (t1 ->> t2 ->> BoolType)
 238 | elem op [BiLesser, BiGreater, BiLesserEq, BiGreaterEq]
 239   = pure (IntType ->> IntType ->> BoolType)
 240 | elem op [BiAnd, BiOr]
 241   = pure (BoolType ->> BoolType ->> BoolType)
 242 | op == BiCons
 243   = fresh >>= \t1-> pure (t1 ->> ListType t1 ->> ListType t1)
 244
 245 op1Type :: Op1 -> Typing Type
 246 op1Type UnNegation = pure $ (BoolType ->> BoolType)
 247 op1Type UnMinus = pure $ (IntType ->> IntType)
 248
 249
 250 Mapmap :: (a->b) ('Map'.Map k a) -> ('Map'.Map k b)
 251 Mapmap _ 'Map'.Tip = 'Map'.Tip
 252 Mapmap f ('Map'.Bin sz k v ml mr) = 'Map'.Bin sz k (f v)
 253                                         (Mapmap f ml)
 254                                         (Mapmap f mr)
 255
 256 instance toString Scheme where
 257     toString (Forall x t) =
 258         concat ["Forall ": map ((+++) "\n") x] +++ toString t
 259
 260 instance toString Gamma where
 261     toString mp =
 262         concat [concat [k, ": ", toString v, "\n"]\\(k, v)<-'Map'.toList mp]
 263
 264 instance toString SemError where
 265     toString (SanityError p e) = concat [toString p,
 266         "SemError: SanityError: ", e]
 267     toString se = "SemError: "
 268
 269 instance MonadTrans (StateT (Gamma, [TVar])) where
 270     liftT m = StateT \s-> m >>= \a-> return (a, s)
 271
 272 //// ------------------------
 273 //// First step: Inference
 274 //// ------------------------//
 275
 276 //unify :: Type Type -> Infer ()
 277 //unify t1 t2 = tell [(t1, t2)]//
 278
 279 //fresh :: Infer Type
 280 //fresh = (gets id) >>= \vars-> (put $ tail vars) >>| (pure $ IdType $ head vars)//
 281
 282 //op2Type :: Op2 -> Infer Type
 283 //op2Type op
 284 //| elem op [BiPlus, BiMinus, BiTimes, BiDivide, BiMod]
 285 //      = pure (IntType ->> IntType ->> IntType)
 286 //| elem op [BiEquals, BiUnEqual]
 287 //      = fresh >>= \t1-> fresh >>= \t2-> pure (t1 ->> t2 ->> BoolType)
 288 //| elem op [BiLesser, BiGreater, BiLesserEq, BiGreaterEq]
 289 //      = pure (IntType ->> IntType ->> BoolType)
 290 //| elem op [BiAnd, BiOr]
 291 //      = pure (BoolType ->> BoolType ->> BoolType)
 292 //| op == BiCons
 293 //      = fresh >>= \t1-> pure (t1 ->> ListType t1 ->> ListType t1)//
 294
 295 //op1Type :: Op1 -> Infer Type
 296 //op1Type UnNegation = pure $ (BoolType ->> BoolType)
 297 //op1Type UnMinus = pure $ (IntType ->> IntType)//
 298
 299 ////instantiate :: Scheme -> Infer Type
 300 ////instantiate (Forall as t) = mapM (const fresh) as//
 301
 302 //lookupEnv :: String -> Infer Type
 303 //lookupEnv ident = asks ('Map'.get ident)
 304 //      >>= \m->case m of
 305 //              Nothing = liftT $ Left $ UndeclaredVariableError zero ident
 306 //              Just (Forall as t) = pure t //instantiate ???//
 307
 308 //class infer a :: a -> Infer Type
 309 //instance infer Expr where
 310 //      infer (VarExpr _ (VarDef ident fs)) = lookupEnv ident
 311 //    infer (Op2Expr _ e1 op e2) =
 312 //        infer e1 >>= \t1 ->
 313 //        infer e2 >>= \t2 ->
 314 //        fresh >>= \frsh ->
 315 //        let given = t1 ->> (t2 ->> frsh) in
 316 //        op2Type op >>= \expected ->
 317 //        unify expected given >>|
 318 //        return frsh
 319 //      infer (Op1Expr _ op e) =
 320 //        infer e >>= \t1 ->
 321 //        fresh >>= \frsh ->
 322 //        let given = t1 ->> frsh in
 323 //        op1Type op >>= \expected ->
 324 //        unify expected given >>|
 325 //        pure frsh
 326 //      infer (IntExpr _ _) = pure IntType
 327 //      infer (CharExpr _ _) = pure CharType
 328 //      infer (BoolExpr _ _) = pure BoolType
 329 //      infer (FunExpr _ f args sels) =  //todo, iets met field selectors
 330 //        lookupEnv f >>= \expected ->
 331 //        fresh >>= \frsh ->
 332 //        mapM infer args >>= \argTypes ->
 333 //        let given = foldr (->>) frsh argTypes in
 334 //        unify expected given >>|
 335 //        pure frsh
 336 //      infer (EmptyListExpr _) = ListType <$> fresh
 337 //      infer (TupleExpr _ (e1, e2)) =
 338 //              infer e1 >>= \et1->infer e2 >>= \et2->pure $ TupleType (et1, et2)//
 339
 340 ////:: VarDef = VarDef String [FieldSelector]
 341 ////:: FieldSelector = FieldHd | FieldTl | FieldFst | FieldSnd
 342 ////:: Op1 = UnNegation | UnMinus
 343 ////:: Op2 = BiPlus | BiMinus | BiTimes | BiDivide | BiMod | BiEquals | BiLesser |
 344 ////    BiGreater | BiLesserEq | BiGreaterEq | BiUnEqual | BiAnd | BiOr | BiCons
 345 ////:: FunDecl = FunDecl Pos String [String] (Maybe Type) [VarDecl] [Stmt]
 346 ////:: FunCall = FunCall String [Expr]
 347 ////:: Stmt
 348 ////    = IfStmt Expr [Stmt] [Stmt]
 349 ////    | WhileStmt Expr [Stmt]
 350 ////    | AssStmt VarDef Expr
 351 ////    | FunStmt FunCall
 352 ////    | ReturnStmt (Maybe Expr)
 353 ////:: Pos = {line :: Int, col :: Int}
 354 ////:: AST = AST [VarDecl] [FunDecl]
 355 ////:: VarDecl = VarDecl Pos Type String Expr
 356 ////:: Type
 357 ////    = TupleType (Type, Type)
 358 ////    | ListType Type
 359 ////    | IdType String
 360 ////    | IntType
 361 ////    | BoolType
 362 ////    | CharType
 363 ////    | VarType
 364 ////    | VoidType
 365 ////    | (->>) infixl 7 Type Type