ref.mlw 1.13 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1

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

   A mutable variable, or ``reference'' in ML terminology, is simply a
MARCHE Claude's avatar
MARCHE Claude committed
5
   record with a single mutable field [contents].
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
6

MARCHE Claude's avatar
MARCHE Claude committed
7 8 9 10 11 12
*)

(** {2 Generic references}

   Creation, access, and assignment are provided as [ref], prefix [!], and
   infix [:=], respectively.
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
13
*)
14 15 16 17 18

module Ref

  type ref 'a = {| mutable contents : 'a |}

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

21
  let ref (v: 'a) = {} {| contents = v |} { result = {| contents = v |} }
22

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

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

end

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

a few operations specific to integer references *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
32

33 34 35 36 37
module Refint

  use export int.Int
  use export module Ref

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
41 42 43
  let (+=)   (r: ref int) (v: int) = {} r := !r + v { !r = old !r + v }
  let (-=)   (r: ref int) (v: int) = {} r := !r - v { !r = old !r - v }
  let ( *= ) (r: ref int) (v: int) = {} r := !r * v { !r = old !r * v }
44 45

end
46

MARCHE Claude's avatar
MARCHE Claude committed
47
(***
48 49 50 51
Local Variables:
compile-command: "unset LANG; make -C .. modules/ref"
End:
*)