oldify.mlw 532 Bytes
Newer Older
1
module M
2

3 4
  use import module stdlib.Ref

5
  logic q1 int int int
6

7
parameter r : ref int
8 9

parameter f1 : y:int ->
10
             {} unit writes r { q1 r (old r) y }
11

12
let g1 () = {} f1 !r { q1 r (old r) (old r) }
13

14 15
  logic foo int : int
  logic q int int int
16

17
parameter f : t:ref int -> x:int -> 
18
             {} unit reads t writes t { q t (old t) x }
19

20
let g (t:ref int) =
21 22
  {}
  f t (foo !t)
23
  { q t (old t) (foo (old t)) }
24

25
end
26 27 28 29 30 31

(*
Local Variables: 
compile-command: "unset LANG; make -C ../../.. bench/programs/good/oldify"
End: 
*)