From d81ba67093ba9f7a9c2f6d47ec51651f99b4b5b3 Mon Sep 17 00:00:00 2001
From: pimjager <pim@pimjager.nl>
Date: Thu, 5 May 2016 18:27:12 +0200
Subject: [PATCH] Small improvements, some errors here and there

---
 examples/Markus/identity(2).spl               | 42 ++++++++++---------
 examples/Markus/infinite_type_shouldfail.spl  |  4 ++
 examples/Markus/overloading.spl               |  6 ++-
 .../polymorphic_value_again_shouldfail.spl    |  8 ++--
 .../Markus/polymorphic_value_shouldfail.spl   |  3 +-
 examples/Markus/recursion.spl                 |  1 +
 .../Markus/self_application_shouldfail(1).spl |  2 +
 examples/Markus/stress_test.spl               |  7 ++--
 sem.icl                                       | 17 ++++----
 9 files changed, 52 insertions(+), 38 deletions(-)

diff --git a/examples/Markus/identity(2).spl b/examples/Markus/identity(2).spl
index cba491c..b06167a 100644
--- a/examples/Markus/identity(2).spl
+++ b/examples/Markus/identity(2).spl
@@ -1,31 +1,31 @@
-// Various versions of the identity function
+//// Various versions of the identity function//
 
 // Identity for integers
 // The type signature forces the function to have a more concrete type than it could have.
 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
-//// Type checking should figure out the type forall a . a -> a
-//id_poly_without(x)
-//{
-//  return x;
-//}//
+// Polymorphic identity without type signature
+// Type checking should figure out the type forall a . a -> a
+id_poly_without(x)
+{
+  return x;
+}//
 
 
 // Clumsy polymorphic identity
 // Type checking should give type forall a . a -> a
-id_poly_wtf(x) :: a -> a
+id_poly_wtf(x)
 {
   var a = x;
   var b = a;
@@ -34,12 +34,14 @@ id_poly_wtf(x) :: a -> a
 }//
 
 
-//// Clumsy identity for integers
-//// Type checking should give type Int -> Int
-//id_int_wtf(x)
-//{
-//  var a = x;
-//  Int b = a;
-//  var c = b;
-//  return c;
-//}
+// Clumsy identity for integers
+// Type checking should give type Int -> Int
+id_int_wtf(x)
+{
+  var a = x;
+  Int b = a;
+  var c = b;
+  return c;
+}
+
+main() {return;}
\ No newline at end of file
diff --git a/examples/Markus/infinite_type_shouldfail.spl b/examples/Markus/infinite_type_shouldfail.spl
index 603cec0..73ac5ed 100644
--- a/examples/Markus/infinite_type_shouldfail.spl
+++ b/examples/Markus/infinite_type_shouldfail.spl
@@ -4,3 +4,7 @@ f(x)
 {
   return f( (x, x) );
 }
+
+main() {return;}
+
+//result: right now no type error... 
\ No newline at end of file
diff --git a/examples/Markus/overloading.spl b/examples/Markus/overloading.spl
index 4d8c615..f3ba7a3 100644
--- a/examples/Markus/overloading.spl
+++ b/examples/Markus/overloading.spl
@@ -1,9 +1,11 @@
 // At this point you maybe don't see what the problem is.
 // Wait until you try to implement your code generator.
 
-var a = equal(1, 2);
-
 equal(x, y)
 {
   return x == y;
 }
+
+a() {return equal(1, 2);}
+
+main() {return;}
\ No newline at end of file
diff --git a/examples/Markus/polymorphic_value_again_shouldfail.spl b/examples/Markus/polymorphic_value_again_shouldfail.spl
index a9bda2e..0381134 100644
--- a/examples/Markus/polymorphic_value_again_shouldfail.spl
+++ b/examples/Markus/polymorphic_value_again_shouldfail.spl
@@ -1,11 +1,13 @@
 // Another variant of the polymorphic value problem.
 
 // This is perfectly fine
-var tuple1 = (1:[], True:[]);
+tuple1() { return (1:[], True:[]); }
 
 // This should fail.
-var l = [];
-var tuple2 = (1:l, True:l);
+l() { return [];}
+tuple2() { return (1:l, True:l);}
 
 
 main() { return; }
+
+//result: does not fail!
\ No newline at end of file
diff --git a/examples/Markus/polymorphic_value_shouldfail.spl b/examples/Markus/polymorphic_value_shouldfail.spl
index 0b868ee..99c5a36 100644
--- a/examples/Markus/polymorphic_value_shouldfail.spl
+++ b/examples/Markus/polymorphic_value_shouldfail.spl
@@ -3,12 +3,13 @@
 
 // The empty list [] usually has polymorphic type forall a.[a], but you
 // cannot give the variable l this type. See below what can go wrong.
-var l = [];
 
 f()
 {
+  var l = [];
   // If l has polymorphic type forall a . [a], the next two lines are possible.
   l = 1:l;
   l = True:l;
   return;
 }
+main() {return;}
\ No newline at end of file
diff --git a/examples/Markus/recursion.spl b/examples/Markus/recursion.spl
index 6dbd124..b802743 100644
--- a/examples/Markus/recursion.spl
+++ b/examples/Markus/recursion.spl
@@ -12,3 +12,4 @@ gcd(m, n)
   else // n > m
     return gcd(m, n - m);
 }
+main() {return;}
\ No newline at end of file
diff --git a/examples/Markus/self_application_shouldfail(1).spl b/examples/Markus/self_application_shouldfail(1).spl
index 41397da..d048983 100644
--- a/examples/Markus/self_application_shouldfail(1).spl
+++ b/examples/Markus/self_application_shouldfail(1).spl
@@ -4,3 +4,5 @@ f(x)
 {
   return x(x);
 }
+main() {return;}
+//result: proper infinite type
\ No newline at end of file
diff --git a/examples/Markus/stress_test.spl b/examples/Markus/stress_test.spl
index 11e52b2..0cb22c5 100644
--- a/examples/Markus/stress_test.spl
+++ b/examples/Markus/stress_test.spl
@@ -2,7 +2,8 @@
 
 f0(x) { return (x, x); }
 f1(x) { return f0(f0(x)); }
-// f2(x) { return f1(f1(x)); }
-// f3(x) { return f2(f2(x)); }
-// f4(x) { return f3(f3(x)); }
+f2(x) { return f1(f1(x)); }
+f3(x) { return f2(f2(x)); }
+//f4(x) { return f3(f3(x)); } //using f4 gives Heap-full
 // f5(x) { return f4(f4(x)); }
+main() {return;}
\ No newline at end of file
diff --git a/sem.icl b/sem.icl
index 791ae69..7f7cdf4 100644
--- a/sem.icl
+++ b/sem.icl
@@ -222,7 +222,6 @@ instance infer Expr where
         pure ((compose s3 $ compose s2 s1), subst s3 tv)
 
     Op1Expr _ op e1 =
-        abort "infereing op1" >>|
         infer e1 >>= \(s1, t1) -> 
         fresh >>= \tv ->
         let given = t1 ->> tv in 
@@ -230,10 +229,9 @@ instance infer Expr where
         lift (unify expected given) >>= \s2 ->
         pure (compose s2 s1, subst s2 tv)
 
-    EmptyListExpr _ = abort "infereing []" >>| (\tv->(zero,tv)) <$> fresh
+    EmptyListExpr _ = (\tv->(zero,tv)) <$> fresh
 
     TupleExpr _ (e1, e2) = 
-        abort "infereing (,)" >>|
         infer e1 >>= \(s1, t1) -> 
         infer e2 >>= \(s2, t2) ->
         pure (compose s2 s1, TupleType (t1,t2))
@@ -242,7 +240,6 @@ instance infer Expr where
         lookup f >>= \expected ->
         let accST = (\(s,ts) e->infer e >>= \(s_,et)->pure (compose s_ s,ts++[et])) in
         foldM accST (zero,[]) args >>= \(s1, argTs)->
-        //abort (concat (["argsTs: "] ++ (map toString argTs))) >>|
         fresh >>= \tv->
         let given = foldr (->>) tv argTs in
         lift (unify expected given) >>= \s2->
@@ -327,15 +324,17 @@ class type a :: a -> Typing a
 
 instance type VarDecl where
     type (VarDecl p expected k e) = 
-        infer e >>= \(s, given) ->
-        applySubst s >>| 
+        infer e >>= \(s1, given) ->
+        applySubst s1 >>| 
         case expected of
             Nothing = pure zero
             Just expected_ = lift (unify expected_ given)
-        >>|
-        generalize given >>= \t ->
+        >>= \s2->
+        applySubst s2 >>|
+        let vtype = subst (compose s2 s1) given in
+        generalize vtype >>= \t ->
         changeGamma (extend k t) >>| 
-        pure (VarDecl p (Just given) k e)
+        pure (VarDecl p (Just vtype) k e)
 
 instance type FunDecl where
     type (FunDecl p f args expected vds stmts) = 
-- 
2.20.1