programs: more benchmarks

bench/programs/good/complex_arg_1.mlw

+exception Exception
+
+parameter f0 : tt:unit ->
+   { }
+   unit
+   { true }
+
+parameter f1 : tt:unit ->
+  { }
+  unit
+  raises Exception
+  { true } | Exception -> { true }
+
+let f () =
+  { }
+  f0 (f1 ())
+  { true } | Exception -> { true }
+
+(*
+Local Variables: 
+compile-command: "unset LANG; make -C ../../.. bench/programs/good/complex_arg_1"
+End: 
+*)

bench/programs/good/complex_arg_2.mlw

+exception Exception of int
+
+parameter t : int ref
+
+parameter m : a:int -> b:int ->
+    { }
+    unit reads t raises Exception
+    { true } | Exception -> { true }
+
+let test () =
+  { }
+  (m ( assert { true } ; 0) 0)
+  { true } | Exception -> { true }
+
+
+(*
+Local Variables: 
+compile-command: "unset LANG; make -C ../../.. bench/programs/good/complex_arg_2"
+End: 
+*)

bench/programs/good/oldify.mlw

+
+{
+  logic q1(int, int, int)
+}
+
+parameter r : int ref
+
+parameter f1 : y:int ->
+             {} unit writes r { q1(!r, old(!r), y) }
+
+let g1 () = {} f1 !r { q1(!r, old(!r), old(!r)) }
+
+{
+  logic foo(int) : int
+  logic q(int, int, int)
+}
+
+parameter f : t:int ref -> x:int -> 
+             {} unit reads t writes t { q(!t, old(!t), x) }
+
+let g (t:int ref) =
+  {}
+  f t (foo !t)
+  { q(!t, old(!t), foo(old(!t))) }
+
+
+(*
+Local Variables: 
+compile-command: "unset LANG; make -C ../../.. bench/programs/good/oldify"
+End: 
+*)

bench/programs/good/poly.mlw

+
+let f (x:'a) = {} x { result=x }
+
+let p () =
+  {}
+  if f True then f 1 else f 2 
+  { result = 1 }
+
+(*
+Local Variables: 
+compile-command: "unset LANG; make -C ../../.. bench/programs/good/poly"
+End: 
+*)

bench/programs/good/see.mlw

+
+(* Side effect in expressions (Bart Jacobs' tricky example) *)
+
+parameter b  : int ref
+parameter b1 : int ref
+parameter b2 : int ref
+
+let f () = 
+  {} b := 1 - !b; !b { result = !b and !b = 1 - old(!b) }
+
+let k () = 
+  {} 
+  begin
+    b := 0;
+    b1 := (1 - (f ())) + (f ());
+    b2 := (f ()) * (1 - (f ())) 
+  end
+  { !b1 = 0 and !b2 = 1 }
+
+(*
+Local Variables: 
+compile-command: "unset LANG; make -C ../../.. bench/programs/good/see"
+End: 
+*)

bench/valid/complex_arg_1.mlw

+../programs/good/complex_arg_1.mlw
\ No newline at end of file

bench/valid/complex_arg_2.mlw

+../programs/good/complex_arg_2.mlw
\ No newline at end of file

bench/valid/oldify.mlw

+../programs/good/oldify.mlw
\ No newline at end of file

bench/valid/poly.mlw

+../programs/good/poly.mlw
\ No newline at end of file

bench/valid/see.mlw

+../programs/good/see.mlw
\ No newline at end of file