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 Data.Either
  11 import Data.Maybe
  12 import Data.Monoid
  13 import Data.List
  14 import Data.Functor
  15
  16 import StdString
  17 import StdList
  18 import StdMisc
  19 import StdEnum
  20 import RWST
  21 import GenEq
  22
  23 from Text import class Text(concat), instance Text String
  24
  25 import AST
  26
  27
  28 :: Scheme = Forall [TVar] Type
  29 :: Gamma :== 'Map'.Map String Scheme //map from Variables! to types
  30 :: Substitution :== 'Map'.Map TVar Type
  31 :: Constraints :== [(Type, Type)]
  32 :: Infer a :== RWST Gamma Constraints [String] (Either SemError) a
  33 :: SemError
  34         = ParseError Pos String
  35         | UnifyError Pos Type Type
  36     | InfiniteTypeError Pos Type
  37     | FieldSelectorError Pos Type FieldSelector
  38         | OperatorError Pos Op2 Type
  39     | UndeclaredVariableError Pos String
  40     | ArgumentMisMatchError Pos String
  41         | SanityError Pos String
  42         | Error String
  43
  44 instance zero Gamma where
  45         zero = 'Map'.newMap
  46
  47 variableStream :: [String]
  48 variableStream = map toString [1..]
  49
  50 sem :: AST -> Either [SemError] Constraints
  51 sem (AST fd) = case foldM (const $ hasNoDups fd) () fd
  52                 >>| foldM (const isNiceMain) () fd
  53                 >>| hasMain fd of
  54         Left e = Left [e]
  55         _ = case execRWST (constraints fd) zero variableStream of
  56                 Left e = Left [e]
  57                 Right (a, b) = Right b
  58 where
  59                 constraints :: [FunDecl] -> Infer ()
  60         constraints _ = pure ()
  61         //TODO: fix
  62                 //constraints fds = mapM_ funconstraint fds >>| pure ()
  63
  64                 funconstraint :: FunDecl -> Infer ()
  65                 funconstraint fd=:(FunDecl _ ident args mt vardecls stmts) = case mt of
  66                         Nothing = abort "Cannot infer functions yet"
  67                         Just t = inEnv (ident, (Forall [] t)) (
  68                                 mapM_ vardeclconstraint vardecls >>| pure ())
  69
  70                 vardeclconstraint :: VarDecl -> Infer ()
  71         vardeclconstraint _ = pure ()
  72         //TODO: fix!
  73                 //vardeclconstraint (VarDecl p mt ident expr) = infer expr
  74                         //>>= \it->inEnv (ident, (Forall [] it)) (pure ())
  75
  76                 hasNoDups :: [FunDecl] FunDecl -> Either SemError ()
  77                 hasNoDups fds (FunDecl p n _ _ _ _)
  78                 # mbs = map (\(FunDecl p` n` _ _ _ _)->if (n == n`) (Just p`) Nothing) fds
  79                 = case catMaybes mbs of
  80                         [] = Left $ SanityError p "HUH THIS SHOULDN'T HAPPEN"
  81                         [x] = pure ()
  82                         [_:x] = Left $ SanityError p (concat
  83                                 [n, " multiply defined at ", toString p])
  84
  85                 hasMain :: [FunDecl] -> Either SemError ()
  86                 hasMain [(FunDecl _ "main" _ _ _ _):fd] = pure ()
  87                 hasMain [_:fd] = hasMain fd
  88                 hasMain [] = Left $ SanityError zero "no main function defined"
  89
  90                 isNiceMain :: FunDecl -> Either SemError ()
  91                 isNiceMain (FunDecl p "main" as mt _ _) = case (as, mt) of
  92                         ([_:_], _) = Left $ SanityError p "main must have arity 0"
  93                         ([], t) = (case t of
  94                                 Nothing = pure ()
  95                                 Just VoidType = pure ()
  96                                 _ = Left $ SanityError p "main has to return Void")
  97                 isNiceMain _ = pure ()
  98
  99 instance toString Scheme where
 100         toString (Forall x t) =
 101                 concat ["Forall ": map ((+++) "\n") x] +++ toString t
 102
 103 instance toString Gamma where
 104         toString mp =
 105                 concat [concat [k, ": ", toString v, "\n"]\\(k, v)<-'Map'.toList mp]
 106
 107 instance toString SemError where
 108         toString (SanityError p e) = concat [toString p,
 109                 "SemError: SanityError: ", e]
 110         toString se = "SemError: "
 111
 112 inEnv :: (String, Scheme) (Infer a) -> Infer a
 113 inEnv (x, sc) m = local ('Map'.put x sc) m
 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 prefers left!
 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
 173
 174
 175
 176 Mapmap :: (a->b) ('Map'.Map k a) -> ('Map'.Map k b)
 177 Mapmap _ 'Map'.Tip = 'Map'.Tip
 178 Mapmap f ('Map'.Bin sz k v ml mr) = 'Map'.Bin sz k (f v)
 179                                         (Mapmap f ml)
 180                                         (Mapmap f mr)
 181
 182 //// ------------------------
 183 //// First step: Inference
 184 //// ------------------------//
 185
 186 //unify :: Type Type -> Infer ()
 187 //unify t1 t2 = tell [(t1, t2)]//
 188
 189 //fresh :: Infer Type
 190 //fresh = (gets id) >>= \vars-> (put $ tail vars) >>| (pure $ IdType $ head vars)//
 191
 192 //op2Type :: Op2 -> Infer Type
 193 //op2Type op
 194 //| elem op [BiPlus, BiMinus, BiTimes, BiDivide, BiMod]
 195 //      = pure (IntType ->> IntType ->> IntType)
 196 //| elem op [BiEquals, BiUnEqual]
 197 //      = fresh >>= \t1-> fresh >>= \t2-> pure (t1 ->> t2 ->> BoolType)
 198 //| elem op [BiLesser, BiGreater, BiLesserEq, BiGreaterEq]
 199 //      = pure (IntType ->> IntType ->> BoolType)
 200 //| elem op [BiAnd, BiOr]
 201 //      = pure (BoolType ->> BoolType ->> BoolType)
 202 //| op == BiCons
 203 //      = fresh >>= \t1-> pure (t1 ->> ListType t1 ->> ListType t1)//
 204
 205 //op1Type :: Op1 -> Infer Type
 206 //op1Type UnNegation = pure $ (BoolType ->> BoolType)
 207 //op1Type UnMinus = pure $ (IntType ->> IntType)//
 208
 209 ////instantiate :: Scheme -> Infer Type
 210 ////instantiate (Forall as t) = mapM (const fresh) as//
 211
 212 //lookupEnv :: String -> Infer Type
 213 //lookupEnv ident = asks ('Map'.get ident)
 214 //      >>= \m->case m of
 215 //              Nothing = liftT $ Left $ UndeclaredVariableError zero ident
 216 //              Just (Forall as t) = pure t //instantiate ???//
 217
 218 //class infer a :: a -> Infer Type
 219 //instance infer Expr where
 220 //      infer (VarExpr _ (VarDef ident fs)) = lookupEnv ident
 221 //    infer (Op2Expr _ e1 op e2) =
 222 //        infer e1 >>= \t1 ->
 223 //        infer e2 >>= \t2 ->
 224 //        fresh >>= \frsh ->
 225 //        let given = t1 ->> (t2 ->> frsh) in
 226 //        op2Type op >>= \expected ->
 227 //        unify expected given >>|
 228 //        return frsh
 229 //      infer (Op1Expr _ op e) =
 230 //        infer e >>= \t1 ->
 231 //        fresh >>= \frsh ->
 232 //        let given = t1 ->> frsh in
 233 //        op1Type op >>= \expected ->
 234 //        unify expected given >>|
 235 //        pure frsh
 236 //      infer (IntExpr _ _) = pure IntType
 237 //      infer (CharExpr _ _) = pure CharType
 238 //      infer (BoolExpr _ _) = pure BoolType
 239 //      infer (FunExpr _ f args sels) =  //todo, iets met field selectors
 240 //        lookupEnv f >>= \expected ->
 241 //        fresh >>= \frsh ->
 242 //        mapM infer args >>= \argTypes ->
 243 //        let given = foldr (->>) frsh argTypes in
 244 //        unify expected given >>|
 245 //        pure frsh
 246 //      infer (EmptyListExpr _) = ListType <$> fresh
 247 //      infer (TupleExpr _ (e1, e2)) =
 248 //              infer e1 >>= \et1->infer e2 >>= \et2->pure $ TupleType (et1, et2)//
 249
 250 ////:: VarDef = VarDef String [FieldSelector]
 251 ////:: FieldSelector = FieldHd | FieldTl | FieldFst | FieldSnd
 252 ////:: Op1 = UnNegation | UnMinus
 253 ////:: Op2 = BiPlus | BiMinus | BiTimes | BiDivide | BiMod | BiEquals | BiLesser |
 254 ////    BiGreater | BiLesserEq | BiGreaterEq | BiUnEqual | BiAnd | BiOr | BiCons
 255 ////:: FunDecl = FunDecl Pos String [String] (Maybe Type) [VarDecl] [Stmt]
 256 ////:: FunCall = FunCall String [Expr]
 257 ////:: Stmt
 258 ////    = IfStmt Expr [Stmt] [Stmt]
 259 ////    | WhileStmt Expr [Stmt]
 260 ////    | AssStmt VarDef Expr
 261 ////    | FunStmt FunCall
 262 ////    | ReturnStmt (Maybe Expr)
 263 ////:: Pos = {line :: Int, col :: Int}
 264 ////:: AST = AST [VarDecl] [FunDecl]
 265 ////:: VarDecl = VarDecl Pos Type String Expr
 266 ////:: Type
 267 ////    = TupleType (Type, Type)
 268 ////    | ListType Type
 269 ////    | IdType String
 270 ////    | IntType
 271 ////    | BoolType
 272 ////    | CharType
 273 ////    | VarType
 274 ////    | VoidType
 275 ////    | (->>) infixl 7 Type Type