From: pimjager Date: Thu, 28 Apr 2016 14:31:09 +0000 (+0200) Subject: Start of algorithm U X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=5164fe6570837a900ec12ca06c126c471238bae0;p=cc1516.git Start of algorithm U --- diff --git a/AST.dcl b/AST.dcl index f415045..5b2bfad 100644 --- a/AST.dcl +++ b/AST.dcl @@ -6,10 +6,11 @@ from StdOverloaded import class toString, class ==, class zero, class < :: Pos = {line :: Int, col :: Int} :: AST = AST [FunDecl] :: VarDecl = VarDecl Pos (Maybe Type) String Expr +:: TVar :== String :: Type = TupleType (Type, Type) | ListType Type - | IdType String + | IdType TVar | IntType | BoolType | CharType diff --git a/sem.icl b/sem.icl index 6108e3a..3b5d15d 100644 --- a/sem.icl +++ b/sem.icl @@ -10,7 +10,7 @@ import Control.Monad.Trans import Data.Either import Data.Maybe import Data.Monoid -import Data.List +import Data.List import Data.Functor import StdString @@ -24,8 +24,10 @@ 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 @@ -41,9 +43,6 @@ import AST instance zero Gamma where zero = 'Map'.newMap -//runInfer :: Gamma (Infer a) -> Either SemError a -//runInfer env m = evalRWST m env variableStream - variableStream :: [String] variableStream = map toString [1..] @@ -57,7 +56,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 @@ -66,8 +67,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 _ _ _ _) @@ -105,100 +108,146 @@ instance toString SemError where "SemError: SanityError: ", e] toString se = "SemError: " -// ------------------------ -// First step: Inference -// ------------------------ - -unify :: Type Type -> Infer () -unify 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) = - 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 +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 (outside of Monad) +//// ------------------------ +instance zero Substitution where zero = 'Map'.newMap +compose :: Substitution Substitution -> Substitution +compose s1 s2 = undef +//unify :: + + + + +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