ref.mlw 947 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 26
  (* parameter incr : r:ref int -> {} unit writes r { !r = old !r + 1 } *)
  let incr (r:ref int) = {} r := !r + 1 { !r = old !r + 1 }
27

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

end
32 33 34 35 36 37

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