From 91c4d57eb84d5d15e011902a1da1b70131e5a222 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Fri, 12 Dec 2014 20:46:48 -0800
Subject: Language change: All functions and methods declared lexically outside
 any class are now automatically static, and fields are no longer allowed to
 be declared there.  Stated differently, all heap state must now be declared
 inside an explicitly declared class, and functions and methods declared
 outside any class can be viewed as belonging to the module.  The motivating
 benefit of this change is to no longer need the 'static' keyword when
 declaring a module of functions and methods.

---
 Test/hofs/Monads.dfy | 50 +++++++++++++++++++++++++-------------------------
 1 file changed, 25 insertions(+), 25 deletions(-)

(limited to 'Test/hofs')

diff --git a/Test/hofs/Monads.dfy b/Test/hofs/Monads.dfy
index 9e7c5460..a221f818 100644
--- a/Test/hofs/Monads.dfy
+++ b/Test/hofs/Monads.dfy
@@ -4,22 +4,22 @@
 abstract module Monad {
   type M<A>;
 
-  static function method Return(x: A): M<A>
-  static function method Bind(m: M<A>, f:A -> M<B>):M<B>
+  function method Return(x: A): M<A>
+  function method Bind(m: M<A>, f:A -> M<B>):M<B>
     reads f.reads;
     requires forall a :: f.requires(a);
 
   // return x >>= f = f x
-  static lemma LeftIdentity(x : A, f : A -> M<B>)
+  lemma LeftIdentity(x : A, f : A -> M<B>)
     requires forall a :: f.requires(a);
     ensures Bind(Return(x),f) == f(x);
 
   // m >>= return = m
-  static lemma RightIdentity(m : M<A>)
+  lemma RightIdentity(m : M<A>)
     ensures Bind(m,Return) == m;
 
   // (m >>= f) >>= g = m >>= (x => f(x) >>= g)
-  static lemma Associativity(m : M<A>, f:A -> M<B>, g: B -> M<C>)
+  lemma Associativity(m : M<A>, f:A -> M<B>, g: B -> M<C>)
     requires forall a :: f.requires(a);
     requires forall b :: g.requires(b);
 	ensures Bind(Bind(m,f),g) ==
@@ -32,24 +32,24 @@ abstract module Monad {
 module Identity refines Monad {
   datatype M<A> = I(A);
 
-  static function method Return<A>(x: A): M<A>
+  function method Return<A>(x: A): M<A>
   { I(x) }
 
-  static function method Bind<A,B>(m: M<A>, f:A -> M<B>):M<B>
+  function method Bind<A,B>(m: M<A>, f:A -> M<B>):M<B>
   {
     var I(x) := m; f(x)
   }
 
-  static lemma LeftIdentity<A,B>(x : A, f : A -> M<B>)
+  lemma LeftIdentity<A,B>(x : A, f : A -> M<B>)
   {
   }
 
-  static lemma RightIdentity<A>(m : M<A>)
+  lemma RightIdentity<A>(m : M<A>)
   {
     assert Bind(m,Return) == m;
   }
 
-  static lemma Associativity<A,B,C>(m : M<A>, f:A -> M<B>, g: B -> M<C>)
+  lemma Associativity<A,B,C>(m : M<A>, f:A -> M<B>, g: B -> M<C>)
   {
 	assert
 	  Bind(Bind(m,f),g) ==
@@ -64,26 +64,26 @@ module Identity refines Monad {
 module Maybe refines Monad {
   datatype M<A> = Just(A) | Nothing;
 
-  static function method Return<A>(x: A): M<A>
+  function method Return<A>(x: A): M<A>
   { Just(x) }
 
-  static function method Bind<A,B>(m: M<A>, f:A -> M<B>):M<B>
+  function method Bind<A,B>(m: M<A>, f:A -> M<B>):M<B>
   {
     match m
 	  case Nothing => Nothing
 	  case Just(x) => f(x)
   }
 
-  static lemma LeftIdentity<A,B>(x : A, f : A -> M<B>)
+  lemma LeftIdentity<A,B>(x : A, f : A -> M<B>)
   {
   }
 
-  static lemma RightIdentity<A>(m : M<A>)
+  lemma RightIdentity<A>(m : M<A>)
   {
     assert Bind(m,Return) == m;
   }
 
-  static lemma Associativity<A,B,C>(m : M<A>, f:A -> M<B>, g: B -> M<C>)
+  lemma Associativity<A,B,C>(m : M<A>, f:A -> M<B>, g: B -> M<C>)
   {
 	assert
 	  Bind(Bind(m,f),g) ==
@@ -98,24 +98,24 @@ module Maybe refines Monad {
 module List refines Monad {
   datatype M<A> = Cons(hd: A,tl: M<A>) | Nil;
 
-  static function method Return<A>(x: A): M<A>
+  function method Return<A>(x: A): M<A>
   { Cons(x,Nil) }
 
-  static function method Concat(xs: M<A>, ys: M<A>): M<A>
+  function method Concat(xs: M<A>, ys: M<A>): M<A>
   {
     match xs
 	  case Nil => ys
 	  case Cons(x,xs) => Cons(x,Concat(xs,ys))
   }
 
-  static function method Join(xss: M<M<A>>) : M<A>
+  function method Join(xss: M<M<A>>) : M<A>
   {
     match xss
 	  case Nil => Nil
 	  case Cons(xs,xss) => Concat(xs,Join(xss))
   }
 
-  static function method Map(xs: M<A>, f: A -> B):M<B>
+  function method Map(xs: M<A>, f: A -> B):M<B>
     reads f.reads;
 	requires forall a :: f.requires(a);
   {
@@ -124,12 +124,12 @@ module List refines Monad {
 	  case Cons(x,xs) => Cons(f(x),Map(xs,f))
   }
 
-  static function method Bind<A,B>(m: M<A>, f:A -> M<B>):M<B>
+  function method Bind<A,B>(m: M<A>, f:A -> M<B>):M<B>
   {
     Join(Map(m,f))
   }
 
-  static lemma LeftIdentity<A,B>(x : A, f : A -> M<B>)
+  lemma LeftIdentity<A,B>(x : A, f : A -> M<B>)
   {
     calc {
 	     Bind(Return(x),f);
@@ -141,7 +141,7 @@ module List refines Monad {
 	}
   }
 
-  static lemma RightIdentity<A>(m : M<A>)
+  lemma RightIdentity<A>(m : M<A>)
   {
     match m
 	  case Nil => calc {
@@ -166,11 +166,11 @@ module List refines Monad {
 	    }
   }
 
-  static lemma ConcatAssociativity<A>(xs : M<A>, ys : M<A>, zs: M<A>)
+  lemma ConcatAssociativity<A>(xs : M<A>, ys : M<A>, zs: M<A>)
     ensures Concat(Concat(xs,ys),zs) == Concat(xs,Concat(ys,zs));
   {}
 
-  static lemma BindMorphism(xs : M<A>, ys: M<A>, f : A -> M<B>)
+  lemma BindMorphism(xs : M<A>, ys: M<A>, f : A -> M<B>)
     requires forall a :: f.requires(a);
 	ensures Bind(Concat(xs,ys),f) == Concat(Bind(xs,f),Bind(ys,f));
   {
@@ -194,7 +194,7 @@ module List refines Monad {
 	  }
   }
 
-  static lemma Associativity<A,B,C>(m : M<A>, f:A -> M<B>, g: B -> M<C>)
+  lemma Associativity<A,B,C>(m : M<A>, f:A -> M<B>, g: B -> M<C>)
   {
     match m
 	  case Nil => calc {
-- 
cgit v1.2.3