ref.mlw 1020 Bytes
Newer Older
1 2 3 4 5 6
(* References *)

module Ref

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

7
  logic (!) (x: ref 'a) : 'a = x.contents
8

9 10
  (* parameter ref : v:'a -> {} ref 'a { result = {| contents = v |} } *)
  let ref (v: 'a) = {} {| contents = v |} { result = {| contents = v |} }
11

12 13
  (* parameter (!) : r:ref 'a -> {} 'a reads r { result = !r } *)
  let (!) (r:ref 'a) = {} r.contents { result = !r }
14

15 16
  (* parameter (:=) : r:ref 'a -> v:'a -> {} unit writes r { !r = v } *)
  let (:=) (r:ref 'a) (v:'a) = {} r.contents <- v { !r = v }
17 18 19 20 21 22 23 24

end

module Refint

  use export int.Int
  use export module Ref

25
  (* parameter incr : r:ref int -> {} unit writes r { !r = old !r + 1 } *)
26
  let incr (r: ref int) = {} r := !r + 1 { !r = old !r + 1 }
27

28
  (* parameter decr : r:ref int -> {} unit writes r { !r = old !r - 1 } *)
29 30 31
  let decr (r: ref int) = {} r := !r - 1 { !r = old !r - 1 }

  let (+=) (r: ref int) (v: int) = {} r := !r + v { !r = old !r + v }
32 33

end
34 35 36 37 38 39

(*
Local Variables:
compile-command: "unset LANG; make -C .. modules/ref"
End:
*)