From e10098cde7bac9a7a1576000fa29d15f1fcd8970 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Thu, 2 Jul 2015 16:06:02 -0700
Subject: Type parameters in method/function signatures are no longer
 auto-declared.  Although convenient and concise, the auto-declare behavior
 has on many occasions caused confusion when a type name has accidentally been
 mistyped (and Dafny had then accepted and auto-declared the name). Note, the
 behavior of filling in missing type parameters is still supported.  This
 mode, although unusual (even original?) in languages, is different from the
 auto- declare behavior.  For auto-declare, identifiers could be used in the
 program without having a declaration.  For fill-in parameters, the implicitly
 declared type parameters remain anonymous.

---
 Test/hofs/TreeMapSimple.dfy | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

(limited to 'Test/hofs/TreeMapSimple.dfy')

diff --git a/Test/hofs/TreeMapSimple.dfy b/Test/hofs/TreeMapSimple.dfy
index a853b82c..6b8f1377 100644
--- a/Test/hofs/TreeMapSimple.dfy
+++ b/Test/hofs/TreeMapSimple.dfy
@@ -6,7 +6,7 @@ datatype List<A> = Nil | Cons(head: A,tail: List<A>)
 datatype Tree<A> = Branch(val: A,trees: List<Tree<A>>)
 
 function ListData(xs : List) : set
-  ensures forall x :: x in ListData(xs) ==> x < xs;
+  ensures forall x :: x in ListData(xs) ==> x < xs
 {
   match xs
     case Nil => {}
@@ -14,32 +14,32 @@ function ListData(xs : List) : set
 }
 
 function TreeData(t0 : Tree) : set
-  ensures forall t :: t in TreeData(t0) ==> t < t0;
+  ensures forall t :: t in TreeData(t0) ==> t < t0
 {
   var Branch(x,ts) := t0;
   {x} + set t, y | t in ListData(ts) && y in TreeData(t) :: y
 }
 
-function Pre(f : A -> B, s : set<A>) : bool
-  reads (set x, y | x in s && y in f.reads(x) :: y);
+function Pre<A,B>(f : A -> B, s : set<A>) : bool
+  reads (set x, y | x in s && y in f.reads(x) :: y)
 {
   forall x :: x in s ==> f.reads(x) == {} && f.requires(x)
 }
 
-function method Map(xs : List<A>, f : A -> B): List<B>
-  reads Pre.reads(f, ListData(xs));
-  requires Pre(f, ListData(xs));
-  decreases xs;
+function method Map<A,B>(xs : List<A>, f : A -> B): List<B>
+  reads Pre.reads(f, ListData(xs))
+  requires Pre(f, ListData(xs))
+  decreases xs
 {
   match xs
     case Nil => Nil
     case Cons(x,xs) => Cons(f(x),Map(xs,f))
 }
 
-function method TMap(t0 : Tree<A>, f : A -> B) : Tree<B>
-  reads Pre.reads(f, TreeData(t0));
-  requires Pre(f, TreeData(t0));
-  decreases t0;
+function method TMap<A,B>(t0 : Tree<A>, f : A -> B) : Tree<B>
+  reads Pre.reads(f, TreeData(t0))
+  requires Pre(f, TreeData(t0))
+  decreases t0
 {
   var Branch(x,ts) := t0;
   Branch(f(x),Map(ts, t  requires t in ListData(ts)
-- 
cgit v1.2.3