fixed and improved scheme for inferring type parameters

3 files changed, 70 insertions, 2 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index b216cc32..1725be19 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -486,6 +486,10 @@ Execution trace:
 Dafny program verifier finished with 3 verified, 4 errors

 

 -------------------- ResolutionErrors.dfy --------------------

+ResolutionErrors.dfy(466,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)

+ResolutionErrors.dfy(471,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)

+ResolutionErrors.dfy(485,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)

+ResolutionErrors.dfy(497,24): Error: Wrong number of type arguments (0 instead of 2) passed to class/datatype: Tree

 ResolutionErrors.dfy(396,2): Error: More than one default constructor

 ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context

 ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts

@@ -550,7 +554,7 @@ ResolutionErrors.dfy(377,10): Error: second argument to ==> must be of type bool
 ResolutionErrors.dfy(382,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

 ResolutionErrors.dfy(434,7): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(440,12): Error: ghost variables are allowed only in specification contexts

-64 resolution/type errors detected in ResolutionErrors.dfy

+68 resolution/type errors detected in ResolutionErrors.dfy

 

 -------------------- ParseErrors.dfy --------------------

 ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator

@@ -1403,7 +1407,7 @@ Dafny program verifier finished with 12 verified, 3 errors
 

 -------------------- NoTypeArgs.dfy --------------------

 

-Dafny program verifier finished with 12 verified, 0 errors

+Dafny program verifier finished with 15 verified, 0 errors

 

 -------------------- EqualityTypes.dfy --------------------

 EqualityTypes.dfy(31,13): Error: a type declaration that requires equality support cannot be replaced by a codatatype

diff --git a/Test/dafny0/NoTypeArgs.dfy b/Test/dafny0/NoTypeArgs.dfy
index c41c7990..88418de7 100644
--- a/Test/dafny0/NoTypeArgs.dfy
+++ b/Test/dafny0/NoTypeArgs.dfy
@@ -80,3 +80,15 @@ ghost method Lemma(xs: List, ys: List)
       assert forall a, b, c :: concat(a, concat(b, c)) == concat(concat(a, b), c);

   }

 }

+

+// ------ Here are some test cases where the inferred arguments will be a prefix of the given ones

+

+method DoAPrefix<A, B, C>(xs: List) returns (ys: List<A>)

+{

+  ys := xs;

+}

+

+function FDoAPrefix<A, B, C>(xs: List): List<A>

+{

+  xs

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index d5fecdf8..bcd1a077 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -447,3 +447,55 @@ method AssignSuchThatFromGhost()
   g :| assume g < g;  // the compiler will complain here, despite the LHS being

                       // ghost -- and rightly so, since an assume is used

 }

+

+// ------------------------ inferred type arguments ----------------------------

+

+// Put the following tests in a separate module, so that the method bodies will

+// be type checked even if there are resolution errors in other modules.

+module NoTypeArgs0 {

+  datatype List<T> = Nil | Cons(T, List);

+  datatype Tree<A,B> = Leaf(A, B) | Node(Tree, Tree<B,A>);

+

+  method DoAPrefix0<A, B, C>(xs: List) returns (ys: List<A>)

+  {

+    ys := xs;

+  }

+

+  method DoAPrefix1<A, B, C>(xs: List) returns (ys: List<B>)

+  {

+    ys := xs;  // error: List<B> cannot be assign to a List<A>

+  }

+

+  method DoAPrefix2<A, B, C>(xs: List) returns (ys: List<B>)

+  {

+    ys := xs;  // error: List<B> cannot be assign to a List<A>

+  }

+

+  function FTree0(t: Tree): Tree

+  {

+    match t

+    case Leaf(_,_) => t

+    case Node(x, y) => x

+  }  

+

+  function FTree1(t: Tree): Tree

+  {

+    match t

+    case Leaf(_,_) => t

+    case Node(x, y) => y  // error: y does not have the right type

+  }

+

+  function FTree2<A,B,C>(t: Tree): Tree<A,B>

+  {

+    t

+  }

+}

+

+module NoTypeArgs1 {

+  datatype Tree<A,B> = Leaf(A, B) | Node(Tree, Tree<B,A>);

+

+  function FTree3<T>(t: Tree): Tree<T,T>  // error: type of 't' does not have enough type parameters

+  {

+    t

+  }

+}