From 079fe4889a4220df26a7e86f1929967dbe427893 Mon Sep 17 00:00:00 2001
From: pimjager <pim@pimjager.nl>
Date: Fri, 6 May 2016 11:45:36 +0200
Subject: [PATCH] identity example now almost correctly typed

---
 AST.dcl                         |  1 +
 AST.icl                         |  2 ++
 examples/Markus/identity(2).spl |  4 +--
 sem.icl                         | 58 +++++++++++++++++++++++++--------
 4 files changed, 49 insertions(+), 16 deletions(-)

diff --git a/AST.dcl b/AST.dcl
index 0bfe1ba..1592143 100644
--- a/AST.dcl
+++ b/AST.dcl
@@ -45,6 +45,7 @@ instance toString AST
 instance toString FieldSelector
 instance toString Op2
 instance toString Expr
+instance toString VarDecl
 
 instance zero Pos
 instance == Op1
diff --git a/AST.icl b/AST.icl
index ae4934f..e1f5bc5 100644
--- a/AST.icl
+++ b/AST.icl
@@ -51,6 +51,8 @@ printStatements [s:ss] i = (case s of
 
 instance print VarDecl where
 	print (VarDecl _ t i e) = maybe ["var"] print t ++ [" ":i:"=":print e] ++ [";"]
+instance toString VarDecl where
+    toString v = concat (print v) 
 
 instance toString Type where
 	toString t = concat $ print t
diff --git a/examples/Markus/identity(2).spl b/examples/Markus/identity(2).spl
index b06167a..04ff196 100644
--- a/examples/Markus/identity(2).spl
+++ b/examples/Markus/identity(2).spl
@@ -6,13 +6,13 @@ id_int(x) :: Int -> Int
 {
   return x;
 }//
-//
+////
 
 // Polymorphic identity with type signature
 id_poly_with(x) :: a -> a
 {
   return x;
-}////
+}//////
 
 
 // Polymorphic identity without type signature
diff --git a/sem.icl b/sem.icl
index 34675d2..082cfe9 100644
--- a/sem.icl
+++ b/sem.icl
@@ -55,7 +55,7 @@ sem (AST fd) = case foldM (const $ hasNoDups fd) () fd
             		>>| hasMain fd
                     >>| evalStateT (type fd) (zero, variableStream) of
 	Left e = Left [e]
-    Right fds = Right (AST fds)
+    Right (_,fds) = Right (AST fds)
 where
 		hasNoDups :: [FunDecl] FunDecl -> Either SemError ()
 		hasNoDups fds (FunDecl p n _ _ _ _)
@@ -298,7 +298,7 @@ instance infer [a] | infer a where
 
 //the type class inferes the type of an AST element (VarDecl or FunDecl)
 //and adds it to the AST element
-class type a :: a -> Typing a
+class type a :: a -> Typing (Substitution, a)
 
 instance type VarDecl where
     type (VarDecl p expected k e) = 
@@ -312,31 +312,57 @@ instance type VarDecl where
         let vtype = subst (compose s2 s1) given in
         generalize vtype >>= \t ->
         changeGamma (extend k t) >>| 
-        pure (VarDecl p (Just vtype) k e)
+        pure (compose s2 s1, VarDecl p (Just vtype) k e)
 
 instance type FunDecl where
     type (FunDecl p f args expected vds stmts) = 
+        gamma >>= \outerScope-> //functions are infered in their own scopde
         introduce f >>|
         mapM introduce args >>= \argTs->
-        type vds >>= \tVds->
-        infer stmts >>= \(s1, result)->
-        let given = foldr (->>) result argTs in 
+        type vds >>= \(s1, tVds)->
         applySubst s1 >>|
+        infer stmts >>= \(s2, result)->
+        applySubst s1 >>|
+        let argTs_ = map (subst $ compose s2 s1) argTs in 
+        //abort (concat $ intersperse "\n" $ map toString argTs_) >>|
+        let given = foldr (->>) result argTs_ in 
         (case expected of
             Nothing = pure zero
             Just expected_ = lift (unify expected_ given))
-        >>= \s2 ->
-        let ftype = subst (compose s2 s1) given in
+        >>= \s3 ->
+        let ftype = subst (compose s3 $ compose s2 s1) given in
         generalize ftype >>= \t->
+        putGamma outerScope >>|
         changeGamma (extend f t) >>| 
-        pure (FunDecl p f args (Just ftype) tVds stmts)
-
-instance toString (Maybe a) | toString a where
-    toString Nothing = "Nothing"
-    toString (Just e) = concat ["Just ", toString e]
+        pure (compose s3 $ compose s2 s1, FunDecl p f args (Just ftype) tVds stmts)
 
 instance type [a] | type a where
-    type dcls = mapM type dcls
+    type []     = pure (zero, [])
+    type [v:vs] = 
+        type v >>= \(s1, v_)->
+        applySubst s1 >>|
+        type vs >>= \(s2, vs_)->
+        applySubst (compose s2 s1) >>|
+        pure (compose s2 s1, [v_:vs_])
+
+//        mapM processGamma dcls//
+
+////add the infered type in Gamma to AST constructs
+//class processGamma a :: a -> Typing a//
+
+//instance processGamma VarDecl where
+//    processGamma v=:(VarDecl p _ k e) = 
+//        gamma >>= \g -> case 'Map'.member k g of
+//            False = undef
+//            True  = instantiate ('Map'.find k g) >>= \t->
+//                    pure (VarDecl p (Just t) k e)//
+
+//instance processGamma FunDecl where
+//    processGamma v=:(FunDecl p k args _ vds stmts) = 
+//        gamma >>= \g -> case 'Map'.member k g of
+//            False = undef
+//            True  = instantiate ('Map'.find k g) >>= \t->
+//                    pure (FunDecl p k args (Just t) vds stmts) 
 
 introduce :: String -> Typing Type
 introduce k = 
@@ -379,6 +405,10 @@ instance toString SemError where
     toString (Error e) = concat ["Unknown error during semantical",
         "analysis: ", e]
 
+instance toString (Maybe a) | toString a where
+    toString Nothing = "Nothing"
+    toString (Just e) = concat ["Just ", toString e]
+
 instance MonadTrans (StateT (Gamma, [TVar])) where
     liftT m = StateT \s-> m >>= \a-> return (a, s)
 
-- 
2.20.1