ref.mlw 526 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
  parameter ref : v:'a -> {} ref 'a { result = {| contents = v |} }
10

11 12 13
  parameter (!) : r:ref 'a -> {} 'a reads r { result = !r }

  parameter (:=) : r:ref 'a -> v:'a -> {} unit writes r { !r = v }
14 15 16 17 18 19 20 21

end

module Refint

  use export int.Int
  use export module Ref

22
  parameter incr : r:ref int -> {} unit writes r { !r = old !r + 1 }
23

24
  parameter decr : r:ref int -> {} unit writes r { !r = old !r - 1 }
25 26

end