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