Dafny: allow various forms of leaving off type arguments in declarations

4 files changed, 128 insertions, 2 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 6f160a66..6c6b54eb 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -498,7 +498,9 @@ ResolutionErrors.dfy(305,16): Error: arguments must have the same type (got DTD_
 ResolutionErrors.dfy(306,25): Error: arguments must have the same type (got bool and int)

 ResolutionErrors.dfy(309,18): Error: ghost fields are allowed only in specification contexts

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

-46 resolution/type errors detected in ResolutionErrors.dfy

+ResolutionErrors.dfy(343,2): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)

+ResolutionErrors.dfy(355,18): Error: incorrect type of datatype constructor argument (found GList<T$0>, expected GList<int>)

+48 resolution/type errors detected in ResolutionErrors.dfy

 

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

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

@@ -1250,6 +1252,10 @@ Execution trace:
 

 Dafny program verifier finished with 12 verified, 3 errors

 

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

+

+Dafny program verifier finished with 12 verified, 0 errors

+

 -------------------- SplitExpr.dfy --------------------

 

 Dafny program verifier finished with 5 verified, 0 errors

diff --git a/Test/dafny0/NoTypeArgs.dfy b/Test/dafny0/NoTypeArgs.dfy
new file mode 100644
index 00000000..c41c7990
--- /dev/null
+++ b/Test/dafny0/NoTypeArgs.dfy
@@ -0,0 +1,82 @@
+datatype List<T> = Nil | Cons(hd: T, tl: List);

+

+method M0() {

+  var l: List;

+  l := Cons(5, Nil);

+  assert l.hd == 5;

+

+  var k: MyClass<bool>;

+  k := new MyClass;

+  k.data := false;

+

+  var h := new MyClass;

+  h.data := false;

+

+  var y := new MyClass.Init(120);

+  var z: int := y.data;

+}

+

+method M1() {  // same thing as above, but with types filled in explicitly

+  var l: List<int>;

+  l := Cons(5, Nil);

+  assert l.hd == 5;

+

+  var k: MyClass<bool>;

+  k := new MyClass<bool>;

+  k.data := false;

+

+  var h := new MyClass<bool>;

+  h.data := false;

+

+  var y := new MyClass<int>.Init(120);

+  var z: int := y.data;

+}

+

+class MyClass<G> {

+  var data: G;

+  method Init(g: G)

+    modifies this;

+  {

+    data := g;

+  }

+}

+

+// ---------------------------------------------------

+

+// The followinng functions and methods are oblivious of the fact that

+// List takes a type parameter.

+

+function concat(xs: List, ys: List): List

+{

+  match xs

+  case Nil => ys

+  case Cons(x, tail) => Cons(x, concat(tail, ys))

+}

+

+function reverse(xs: List): List

+{

+  match xs

+  case Nil => Nil

+  case Cons(t, rest) => concat(reverse(rest), Cons(t, Nil))

+}

+

+ghost method Theorem(xs: List)

+  ensures reverse(reverse(xs)) == xs;

+{

+  match (xs) {

+    case Nil =>

+    case Cons(t, rest) =>

+      Lemma(reverse(rest), Cons(t, Nil));

+  }

+}

+

+ghost method Lemma(xs: List, ys: List)

+  ensures reverse(concat(xs, ys)) == concat(reverse(ys), reverse(xs));

+{

+  match (xs) {

+    case Nil =>

+      assert forall ws :: concat(ws, Nil) == ws;

+    case Cons(t, rest) =>

+      assert forall a, b, c :: concat(a, concat(b, c)) == concat(concat(a, b), c);

+  }

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 34cfc762..274cc95a 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -317,3 +317,40 @@ method PrintOnlyNonGhosts(a: int, ghost b: int)
   print "a: ", a, "\n";

   print "b: ", b, "\n";  // error: print statement cannot take ghosts

 }

+

+// ------------------- auto-added type arguments ------------------------------

+

+class GenericClass<T> { var data: T; }

+

+method MG0(a: GenericClass, b: GenericClass)

+  requires a != null && b != null;

+  modifies a;

+{

+  a.data := b.data;  // allowed, since both a and b get the same auto type argument

+}

+

+method G_Caller()

+{

+  var x := new GenericClass;

+  MG0(x, x);  // fine

+  var y := new GenericClass;

+  MG0(x, y);  // also fine (and now y's type argument is constrained to be that of x's)

+  var z := new GenericClass<int>;

+  y.data := z.data;  // this will have the effect of unifying all type args so far to be 'int'

+  assert x.data == 5;  // this is type correct

+

+  var w := new GenericClass<bool>;

+  MG0(x, w);  // error: types don't match up

+}

+

+datatype GList<T> = GNil | GCons(hd: T, tl: GList);

+

+method MG1(l: GList, n: nat)

+{

+  if (n != 0) {

+    MG1(l, n-1);

+    MG1(GCons(12, GCons(20, GNil)), n-1);

+  }

+  var t := GCons(100, GNil);

+  t := GCons(120, l);  // error: types don't match up (List<T$0> versus List<int>)

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index d09e1cc2..b1402e83 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -17,7 +17,8 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             ModulesCycle.dfy Modules0.dfy Modules1.dfy BadFunction.dfy

             Comprehensions.dfy Basics.dfy ControlStructures.dfy

             Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy

-            TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy

+            TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy NoTypeArgs.dfy

+            SplitExpr.dfy

             LoopModifies.dfy Refinement.dfy RefinementErrors.dfy

             ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy

             CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy