check out the test case 1

dune-project

@@ -11,7 +11,7 @@
 
 (authors "Song Yahui, Darius Foo")
 
-(maintainers "e0210374@u.nus.edu, darius.foo.tw@gmail.com")
+(maintainers "yahui_s@nus.edu.sg, darius.foo.tw@gmail.com")
 (license MIT)
 
 (package

src/demo/1_State_Monad.ml

@@ -22,7 +22,7 @@ let read_n_write ()
   read ()
 
 
-(* Figure 38 *)
+(* Figure 37 *)
 let state_handler () 
 (*@ ex ret i; Norm(i->1/\ret=1, ret) @*)
 = let i = ref 0 in 
@@ -32,7 +32,7 @@ let state_handler ()
   | effect (Write v) k -> i := v; resume k ()
 
 
-(* Figure 39 *)
+(* Figure 38 *)
 let write_handler j  
 (*@ ex r1;   Read(emp, r1); 
     ex r2;   req j-> r2; ens j-> r1+1; 
@@ -42,7 +42,7 @@ let write_handler j
   | effect (Write v) k -> j := v; resume k ()
 
 
-(* Figure 39 *)
+(* Figure 38 *)
 let read_handler  ()
 (*@ ex ret i; Norm(i->1/\ret=1, ret) @*)
 = let i = ref 0 in 
@@ -56,7 +56,7 @@ let exchange (m:int)
 = perform (Exchange m)
 
 
-(* Figure 40 *)
+(* Figure 39 *)
 let exc_handler (l) (new_v:int)
 (*@ ex old; req l-> old ; ens l-> new_v; Norm (res=old, res)   @*)
 = match exchange new_v with 

src/demo/1_bug.ml

@@ -0,0 +1,28 @@
+effect Read : int 
+effect Write : int -> unit 
+effect Exchange: int -> int
+
+
+let read () 
+(*@ ex ret; Read(emp, ret); Norm(emp, ret) @*)
+= perform Read
+
+
+let write n 
+(*@ ex ret; Write(emp, n,  ret); Norm(emp, ret) @*)
+= perform (Write n)
+
+
+(* ASK DARIUS : the enatilment checking does not terminate *)
+let test1 ()
+(* ex r1; Read(emp, r1); 
+    ex r2 r3; Write(r2=r1+1, (r2), r3); 
+    ex r4; Read(emp, r4); 
+    ex r5 r6; Write(r5=r4+1, (r5), r6); 
+    ex r7; Read(emp, r7); Norm (res=r7, res)  @*)
+= 
+  let x = read () in 
+  write (x+1);
+  let z = read () in 
+  write (z+1);
+  read ()