Start of algorithm U

diff --git a/AST.dcl b/AST.dcl
index f415045..5b2bfad 100644 (file)
--- 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 (file)
--- 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