From: pimjager <pim@pimjager.nl>
Date: Thu, 28 Apr 2016 16:32:13 +0000 (+0200)
Subject: Added Typing Monad and instantiate
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=4d84f0ca9371e73bed08baa712ce28c8234bf705;p=cc1516.git

Added Typing Monad and instantiate
---

diff --git a/sem.icl b/sem.icl
index 1c4f345..16a426c 100644
--- 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