Added Typing Monad and instantiate

diff --git a/sem.icl b/sem.icl
index 1c4f345..16a426c 100644 (file)
--- a/sem.icl
+++ b/sem.icl
@@ -7,18 +7,19 @@ from StdFunc import o, flip, const, id
 
 import Control.Monad
 import Control.Monad.Trans
-//import Control.Monad.State
+import Control.Monad.State
 import Data.Either
 import Data.Maybe
 import Data.Monoid
 import Data.List
 import Data.Functor
+import Data.Tuple
 
 import StdString
+import StdTuple
 import StdList
 import StdMisc
 import StdEnum
-import RWST
 import GenEq
 
 from Text import class Text(concat), instance Text String
@@ -30,7 +31,6 @@ import AST
 :: 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 
@@ -53,22 +53,24 @@ sem (AST fd) = case foldM (const $ hasNoDups fd) () fd
                >>| foldM (const isNiceMain) () fd
                >>| hasMain fd of
        Left e = Left [e]
-       _ = case execRWST (constraints fd) zero variableStream of
-               Left e = Left [e]
-               Right (a, b) = Right b
+    _ = Right []
+       //_ = case execRWST (constraints fd) zero variableStream of
+       //      Left e = Left [e]
+       //      Right (a, b) = Right b
 where
-               constraints :: [FunDecl] -> Infer ()
+               constraints :: [FunDecl] -> Typing ()
         constraints _ = pure ()
         //TODO: fix
                //constraints fds = mapM_ funconstraint fds >>| pure ()
 
-               funconstraint :: FunDecl -> Infer ()
+               funconstraint :: FunDecl -> Typing ()
                funconstraint fd=:(FunDecl _ ident args mt vardecls stmts) = case mt of
                        Nothing = abort "Cannot infer functions yet"
-                       Just t = inEnv (ident, (Forall [] t)) (
-                               mapM_ vardeclconstraint vardecls >>| pure ())
+            _ = pure ()
+                       //Just t = inEnv (ident, (Forall [] t)) (
+                       //      mapM_ vardeclconstraint vardecls >>| pure ())
 
-               vardeclconstraint :: VarDecl -> Infer ()
+               vardeclconstraint :: VarDecl -> Typing ()
         vardeclconstraint _ = pure ()
         //TODO: fix!
                //vardeclconstraint (VarDecl p mt ident expr) = infer expr
@@ -110,9 +112,6 @@ instance toString SemError where
                "SemError: SanityError: ", e]
        toString se = "SemError: "
 
-inEnv :: (String, Scheme) (Infer a) -> Infer a
-inEnv (x, sc) m = local ('Map'.put x sc) m
-
 class Typeable a where
     ftv :: a -> [TVar]
     subst :: Substitution a -> a
@@ -149,7 +148,7 @@ 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!
+//Note: unlike function composition, compose is left biased!
 
 occurs :: TVar a -> Bool | Typeable a
 occurs tvar a = elem tvar (ftv a)
@@ -172,10 +171,30 @@ unify t1 t2 | t1 == t2  = Right zero
 //// ------------------------
 //// 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]
+//The typing monad
+:: Typing a :== StateT (Gamma, [TVar]) (Either SemError) a
+gamma :: Typing Gamma
+gamma = gets fst
+putGamma :: Gamma -> Typing ()
+putGamma g = modify (appFst $ const g) >>| pure ()
+withGamma :: (Gamma -> Gamma) -> Typing ()
+withGamma f = modify (appFst f) >>| pure ()
+fresh :: Typing Type
+fresh = gets snd >>= \vars-> 
+        modify (appSnd $ const $ tail vars) >>| 
+        pure (IdType (head vars))
+
+//instantiate maps a schemes type variables to variables with fresh names
+//and drops the quantification: i.e. forall a,b.a->[b] becomes c->[d]
+instantiate :: Scheme -> Typing Type
+instantiate (Forall bound t) = 
+    mapM (const fresh) bound >>= \newVars->
+    let s = 'Map'.fromList (zip (bound,newVars)) in
+    pure (subst s t)
+//generalize quentifies all free type variables in a type which are not
+//in the gamma
+generalize :: Type -> Typing Scheme
+generalize t = gamma >>= \g-> pure $ Forall (difference (ftv t) (ftv g)) t