X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=sem.icl;h=1c4f345b1d3e294f7d7a9b7c02fbd4ec4b04d044;hb=1fd43a877fe687b4670bb6d82861df3407b68b91;hp=e05a1e4ba93621b3bec5bf3f0d4d472131acbcb3;hpb=de448d981d7f4b3d78dc09d9eea4c492ec44bc76;p=cc1516.git diff --git a/sem.icl b/sem.icl index e05a1e4..1c4f345 100644 --- a/sem.icl +++ b/sem.icl @@ -7,10 +7,12 @@ from StdFunc import o, flip, const, id import Control.Monad import Control.Monad.Trans +//import Control.Monad.State import Data.Either import Data.Maybe import Data.Monoid -import Data.List +import Data.List +import Data.Functor import StdString import StdList @@ -23,13 +25,16 @@ from Text import class Text(concat), instance Text String import AST -:: Scheme = Forall [String] Type -:: Gamma :== 'Map'.Map String Scheme + +:: Scheme = Forall [TVar] Type +:: Gamma :== 'Map'.Map String Scheme //map from Variables! to types +:: Substitution :== 'Map'.Map TVar Type :: Constraints :== [(Type, Type)] :: Infer a :== RWST Gamma Constraints [String] (Either SemError) a :: SemError = ParseError Pos String | UnifyError Pos Type Type + | InfiniteTypeError Pos Type | FieldSelectorError Pos Type FieldSelector | OperatorError Pos Op2 Type | UndeclaredVariableError Pos String @@ -40,7 +45,7 @@ import AST instance zero Gamma where zero = 'Map'.newMap -variableStream :: [String] +variableStream :: [TVar] variableStream = map toString [1..] sem :: AST -> Either [SemError] Constraints @@ -53,7 +58,9 @@ sem (AST fd) = case foldM (const $ hasNoDups fd) () fd Right (a, b) = Right b where constraints :: [FunDecl] -> Infer () - constraints fds = mapM_ funconstraint fds >>| pure () + constraints _ = pure () + //TODO: fix + //constraints fds = mapM_ funconstraint fds >>| pure () funconstraint :: FunDecl -> Infer () funconstraint fd=:(FunDecl _ ident args mt vardecls stmts) = case mt of @@ -62,8 +69,10 @@ where mapM_ vardeclconstraint vardecls >>| pure ()) vardeclconstraint :: VarDecl -> Infer () - vardeclconstraint (VarDecl p mt ident expr) = infer expr - >>= \it->inEnv (ident, (Forall [] it)) (pure ()) + vardeclconstraint _ = pure () + //TODO: fix! + //vardeclconstraint (VarDecl p mt ident expr) = infer expr + //>>= \it->inEnv (ident, (Forall [] it)) (pure ()) hasNoDups :: [FunDecl] FunDecl -> Either SemError () hasNoDups fds (FunDecl p n _ _ _ _) @@ -101,93 +110,174 @@ instance toString SemError where "SemError: SanityError: ", e] toString se = "SemError: " -uni :: Type Type -> Infer () -uni t1 t2 = tell [(t1, t2)] - inEnv :: (String, Scheme) (Infer a) -> Infer a inEnv (x, sc) m = local ('Map'.put x sc) m -fresh :: Infer Type -fresh = (gets id) >>= \vars-> (put $ tail vars) >>| (pure $ IdType $ head vars) - -op2Type :: Op2 -> Infer Type -op2Type op -| elem op [BiPlus, BiMinus, BiTimes, BiDivide, BiMod] - = pure (IntType ->> IntType ->> IntType) -| elem op [BiEquals, BiUnEqual] - = fresh >>= \t1-> fresh >>= \t2-> pure (t1 ->> t2 ->> BoolType) -| elem op [BiLesser, BiGreater, BiLesserEq, BiGreaterEq] - = pure (IntType ->> IntType ->> BoolType) -| elem op [BiAnd, BiOr] - = pure (BoolType ->> BoolType ->> BoolType) -| op == BiCons - = fresh >>= \t1-> pure (t1 ->> ListType t1 ->> ListType t1) - -op1Type :: Op1 -> Infer Type -op1Type UnNegation = pure $ (BoolType ->> BoolType) -op1Type UnMinus = pure $ (IntType ->> IntType) - -//instantiate :: Scheme -> Infer Type -//instantiate (Forall as t) = mapM (const fresh) as - -lookupEnv :: String -> Infer Type -lookupEnv ident = asks ('Map'.get ident) - >>= \m->case m of - Nothing = liftT $ Left $ UndeclaredVariableError zero ident - Just (Forall as t) = pure t //instantiate ??? - -class infer a :: a -> Infer Type -instance infer Expr where - infer (VarExpr _ (VarDef ident fs)) = lookupEnv ident - infer (Op2Expr _ e1 op e2) = case op of - BiPlus = pure IntType - BiMinus = pure IntType - BiTimes = pure IntType - BiDivide = pure IntType - BiMod = pure IntType - BiLesser = pure IntType - BiGreater = pure IntType - BiLesserEq = pure IntType - BiGreaterEq = pure IntType - BiAnd = pure BoolType - BiOr = pure BoolType - BiEquals = infer e1 - BiUnEqual = infer e1 // maybe check e2? - BiCons = infer e1 >>= \it1->pure $ ListType it1 - infer (Op1Expr _ op e) = case op of - UnMinus = pure IntType - UnNegation = pure BoolType - infer (IntExpr _ _) = pure IntType - infer (CharExpr _ _) = pure CharType - infer (BoolExpr _ _) = pure BoolType - infer (FunExpr _ _ _ _) = undef - infer (EmptyListExpr _) = undef - infer (TupleExpr _ (e1, e2)) = - infer e1 >>= \et1->infer e2 >>= \et2->pure $ TupleType (et1, et2) - -//:: VarDef = VarDef String [FieldSelector] -//:: FieldSelector = FieldHd | FieldTl | FieldFst | FieldSnd -//:: Op1 = UnNegation | UnMinus -//:: Op2 = BiPlus | BiMinus | BiTimes | BiDivide | BiMod | BiEquals | BiLesser | -// BiGreater | BiLesserEq | BiGreaterEq | BiUnEqual | BiAnd | BiOr | BiCons -//:: FunDecl = FunDecl Pos String [String] (Maybe Type) [VarDecl] [Stmt] -//:: FunCall = FunCall String [Expr] -//:: Stmt -// = IfStmt Expr [Stmt] [Stmt] -// | WhileStmt Expr [Stmt] -// | AssStmt VarDef Expr -// | FunStmt FunCall -// | ReturnStmt (Maybe Expr) -//:: Pos = {line :: Int, col :: Int} -//:: AST = AST [VarDecl] [FunDecl] -//:: VarDecl = VarDecl Pos Type String Expr -//:: Type -// = TupleType (Type, Type) -// | ListType Type -// | IdType String -// | IntType -// | BoolType -// | CharType -// | VarType -// | VoidType -// | (->>) infixl 7 Type Type +class Typeable a where + ftv :: a -> [TVar] + subst :: Substitution a -> a + +instance Typeable Scheme where + ftv (Forall bound t) = difference (ftv t) bound + subst s (Forall bound t) = Forall bound $ subst s_ t + where s_ = 'Map'.filterWithKey (\k _ -> not (elem k bound)) s + +instance Typeable [a] | Typeable a where + ftv types = foldr (\t ts-> ftv t ++ ts) [] types + subst s ts = map (\t->subst s t) ts + +instance Typeable Type where + ftv (TupleType (t1, t2)) = ftv t1 ++ ftv t2 + ftv (ListType t) = ftv t + ftv (IdType tvar) = [tvar] + ftv (t1 ->> t2) = ftv t1 ++ ftv t2 + ftv _ = [] + subst s (TupleType (t1, t2))= TupleType (subst s t1, subst s t2) + subst s (ListType t1) = ListType (subst s t1) + subst s (t1 ->> t2) = (subst s t1) ->> (subst s t2) + subst s t1=:(IdType tvar) = 'Map'.findWithDefault t1 tvar s + subst s t = t + +instance Typeable Gamma where + ftv gamma = concatMap id $ map ftv ('Map'.elems gamma) + subst s gamma = Mapmap (subst s) gamma + +//// ------------------------ +//// algorithm U, Unification +//// ------------------------ +instance zero Substitution where zero = 'Map'.newMap + +compose :: Substitution Substitution -> Substitution +compose s1 s2 = 'Map'.union (Mapmap (subst s1) s2) s1 +//Note: unlike function composition, compose prefers left! + +occurs :: TVar a -> Bool | Typeable a +occurs tvar a = elem tvar (ftv a) + +unify :: Type Type -> Either SemError Substitution +unify t1=:(IdType tv) t2 = unify t2 t1 +unify t1 t2=:(IdType tv) | t1 == (IdType tv) = Right zero + | occurs tv t1 = Left $ InfiniteTypeError zero t1 + | otherwise = Right $ 'Map'.singleton tv t1 +unify (ta1->>ta2) (tb1->>tb2) = unify ta1 tb1 >>= \s1-> + unify tb1 tb2 >>= \s2-> + Right $ compose s1 s2 +unify (TupleType (ta1,ta2)) (TupleType (tb1,tb2)) = unify ta1 tb1 >>= \s1-> + unify ta2 tb2 >>= \s2-> + Right $ compose s1 s2 +unify (ListType t1) (ListType t2) = unify t1 t2 +unify t1 t2 | t1 == t2 = Right zero + | otherwise = Left $ UnifyError zero t1 t2 + +//// ------------------------ +//// Algorithm M, Inference and Solving +//// ------------------------ +//:: Typing a :== StateT (Gamma, [TVar]) Either a + +//map a schemes type variables to variables with fresh names +//i.e. a->[b] becomes c->[d] + + + + + +Mapmap :: (a->b) ('Map'.Map k a) -> ('Map'.Map k b) +Mapmap _ 'Map'.Tip = 'Map'.Tip +Mapmap f ('Map'.Bin sz k v ml mr) = 'Map'.Bin sz k (f v) + (Mapmap f ml) + (Mapmap f mr) + +//// ------------------------ +//// First step: Inference +//// ------------------------// + +//unify :: Type Type -> Infer () +//unify t1 t2 = tell [(t1, t2)]// + +//fresh :: Infer Type +//fresh = (gets id) >>= \vars-> (put $ tail vars) >>| (pure $ IdType $ head vars)// + +//op2Type :: Op2 -> Infer Type +//op2Type op +//| elem op [BiPlus, BiMinus, BiTimes, BiDivide, BiMod] +// = pure (IntType ->> IntType ->> IntType) +//| elem op [BiEquals, BiUnEqual] +// = fresh >>= \t1-> fresh >>= \t2-> pure (t1 ->> t2 ->> BoolType) +//| elem op [BiLesser, BiGreater, BiLesserEq, BiGreaterEq] +// = pure (IntType ->> IntType ->> BoolType) +//| elem op [BiAnd, BiOr] +// = pure (BoolType ->> BoolType ->> BoolType) +//| op == BiCons +// = fresh >>= \t1-> pure (t1 ->> ListType t1 ->> ListType t1)// + +//op1Type :: Op1 -> Infer Type +//op1Type UnNegation = pure $ (BoolType ->> BoolType) +//op1Type UnMinus = pure $ (IntType ->> IntType)// + +////instantiate :: Scheme -> Infer Type +////instantiate (Forall as t) = mapM (const fresh) as// + +//lookupEnv :: String -> Infer Type +//lookupEnv ident = asks ('Map'.get ident) +// >>= \m->case m of +// Nothing = liftT $ Left $ UndeclaredVariableError zero ident +// Just (Forall as t) = pure t //instantiate ???// + +//class infer a :: a -> Infer Type +//instance infer Expr where +// infer (VarExpr _ (VarDef ident fs)) = lookupEnv ident +// infer (Op2Expr _ e1 op e2) = +// infer e1 >>= \t1 -> +// infer e2 >>= \t2 -> +// fresh >>= \frsh -> +// let given = t1 ->> (t2 ->> frsh) in +// op2Type op >>= \expected -> +// unify expected given >>| +// return frsh +// infer (Op1Expr _ op e) = +// infer e >>= \t1 -> +// fresh >>= \frsh -> +// let given = t1 ->> frsh in +// op1Type op >>= \expected -> +// unify expected given >>| +// pure frsh +// infer (IntExpr _ _) = pure IntType +// infer (CharExpr _ _) = pure CharType +// infer (BoolExpr _ _) = pure BoolType +// infer (FunExpr _ f args sels) = //todo, iets met field selectors +// lookupEnv f >>= \expected -> +// fresh >>= \frsh -> +// mapM infer args >>= \argTypes -> +// let given = foldr (->>) frsh argTypes in +// unify expected given >>| +// pure frsh +// infer (EmptyListExpr _) = ListType <$> fresh +// infer (TupleExpr _ (e1, e2)) = +// infer e1 >>= \et1->infer e2 >>= \et2->pure $ TupleType (et1, et2)// + +////:: VarDef = VarDef String [FieldSelector] +////:: FieldSelector = FieldHd | FieldTl | FieldFst | FieldSnd +////:: Op1 = UnNegation | UnMinus +////:: Op2 = BiPlus | BiMinus | BiTimes | BiDivide | BiMod | BiEquals | BiLesser | +//// BiGreater | BiLesserEq | BiGreaterEq | BiUnEqual | BiAnd | BiOr | BiCons +////:: FunDecl = FunDecl Pos String [String] (Maybe Type) [VarDecl] [Stmt] +////:: FunCall = FunCall String [Expr] +////:: Stmt +//// = IfStmt Expr [Stmt] [Stmt] +//// | WhileStmt Expr [Stmt] +//// | AssStmt VarDef Expr +//// | FunStmt FunCall +//// | ReturnStmt (Maybe Expr) +////:: Pos = {line :: Int, col :: Int} +////:: AST = AST [VarDecl] [FunDecl] +////:: VarDecl = VarDecl Pos Type String Expr +////:: Type +//// = TupleType (Type, Type) +//// | ListType Type +//// | IdType String +//// | IntType +//// | BoolType +//// | CharType +//// | VarType +//// | VoidType +//// | (->>) infixl 7 Type Type