ref.mlw 1.07 KB
Newer Older
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
1

MARCHE Claude's avatar
MARCHE Claude committed
2
(** {1 References}
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
3 4

   A mutable variable, or ``reference'' in ML terminology, is simply a
MARCHE Claude's avatar
MARCHE Claude committed
5 6 7 8 9 10 11
   record with a single mutable field [contents].
*)

(** {2 Generic references}

   Creation, access, and assignment are provided as [ref], prefix [!], and
   infix [:=], respectively.
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
12
*)
13 14 15

module Ref

16
  type ref 'a = { mutable contents : 'a }
17

Andrei Paskevich's avatar
Andrei Paskevich committed
18
  function (!) (x: ref 'a) : 'a = x.contents
19

20
  let ref (v: 'a) ensures { result = { contents = v } } = { contents = v }
21

22
  let (!) (r:ref 'a) ensures { result = !r } = r.contents
23

24
  let (:=) (r:ref 'a) (v:'a) ensures { !r = v } = r.contents <- v
25 26 27

end

MARCHE Claude's avatar
MARCHE Claude committed
28 29 30
(** {2 Integer References}

a few operations specific to integer references *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
31

32 33 34
module Refint

  use export int.Int
35
  use export Ref
36

37 38
  let incr (r: ref int) ensures { !r = old !r + 1 } = r := !r + 1
  let decr (r: ref int) ensures { !r = old !r - 1 } = r := !r - 1
39

40 41 42
  let (+=)   (r: ref int) (v: int) ensures { !r = old !r + v } = r := !r + v
  let (-=)   (r: ref int) (v: int) ensures { !r = old !r - v } = r := !r - v
  let ( *= ) (r: ref int) (v: int) ensures { !r = old !r * v } = r := !r * v
43 44

end