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

module Ref

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
9
  (* val ref : v:'a -> {} ref 'a { result = {| contents = v |} } *)
10
  let ref (v: 'a) = {} {| contents = v |} { result = {| contents = v |} }
11

Andrei Paskevich's avatar
Andrei Paskevich committed
12
  (* val (!) : r:ref 'a -> {} 'a reads r { result = !r } *)
13
  let (!) (r:ref 'a) = {} r.contents { result = !r }
14

Andrei Paskevich's avatar
Andrei Paskevich committed
15
  (* val (:=) : r:ref 'a -> v:'a -> {} unit writes r { !r = v } *)
16
  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

Andrei Paskevich's avatar
Andrei Paskevich committed
25
  (* val 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

Andrei Paskevich's avatar
Andrei Paskevich committed
28
  (* val 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:
*)