ref.mlw 815 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

27
  parameter decr : r:ref int -> {} unit writes r { !r = old !r - 1 }
28 29

end
30 31 32 33 34 35

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