1 (* -------------------------------------------------------------------------- *)
  2 
  3 (* [treeMap k c a] is an abstract type for association maps with keys of type
  4    [k] and values of type [a]. Entries are internally ordered using the key
  5    ordering [cmp]. *)
  6 
  7 abstract treeMap k (cmp: term) +a
  8 
  9 (* [treeMap k c a] is an exclusive type. That is, a map has a unique owner. *)
 10 
 11 fact exclusive (treeMap k cmp a)
 12 
 13 (* -------------------------------------------------------------------------- *)
 14 
 15 (* Operations on maps. *)
 16 
 17 val create : [k, a] (cmp: (k, k) -> int) -> treeMap k cmp a
 18 
 19 val singleton : [k, a] (cmp: (k, k) -> int, consumes k, consumes a) -> treeMap k cmp a
 20 
 21 val cardinal : [k, cmp: term, a] treeMap k cmp a -> int
 22 
 23 val is_empty : [k, cmp: term, a] treeMap k cmp a -> bool
 24 
 25 val add : [k, cmp: term, a] (consumes k, consumes a, treeMap k cmp a) -> ()
 26 
 27 val find : [k, cmp: term, a] duplicable a => (k, treeMap k cmp a) -> option a
 28 
 29 val update : [k, c: term, a, preserved : perm, consumed : perm] (
 30   x: k,
 31   m: treeMap k c a,
 32   f: (consumes a | preserved * consumes consumed) -> a
 33 | preserved * consumes consumed
 34 ) -> ()
 35 
 36 val mem : [k, cmp: term, a] (k, treeMap k cmp a) -> bool
 37 
 38 val min_binding : [k, cmp: term, a] duplicable k => duplicable a => treeMap k cmp a -> option (k, a)
 39 val max_binding : [k, cmp: term, a] duplicable k => duplicable a => treeMap k cmp a -> option (k, a)
 40 
 41 val extract_min_binding : [k, cmp: term, a] treeMap k cmp a -> option (k, a)
 42 val extract_max_binding : [k, cmp: term, a] treeMap k cmp a -> option (k, a)
 43 
 44 val remove : [k, cmp: term, a] (k, treeMap k cmp a) -> option (k, a)
 45 
 46 val iter : [k, c: term, a, p : perm] (
 47   m: treeMap k c a,
 48   f: (k, a | p) -> bool
 49   | p
 50 ) -> bool
 51 
 52 val for_all :
 53   =iter
 54 
 55 (* TEMPORARY add sugar for this declaration? *)
 56 
 57 val exists : [k, c: term, a, p : perm] (
 58   m: treeMap k c a,
 59   f: (k, a | p) -> bool
 60   | p
 61 ) -> bool
 62 
 63 val map: [k, c: term, a1, a2, b, p : perm] duplicable k => (
 64   consumes m: treeMap k c a1,
 65   f: (k, consumes d: a1 | p) -> (b | d @ a2)
 66   | p
 67 ) -> (treeMap k c b | m @ treeMap k c a2)
 68 
 69 val copy: [k, c: term, a, b] duplicable k => (m: treeMap k c a, f: a -> b) -> treeMap k c b
 70 
 71 val fold_ascending : [k, c: term, a1, a2, b, p : perm] (
 72   consumes m: treeMap k c a1,
 73   consumes accu: b,
 74   f: (k, consumes d: a1, consumes accu: b | p) -> (b | d @ a2)
 75   | p
 76 ) -> (b | m @ treeMap k c a2)
 77 
 78 val fold_descending : [k, c: term, a1, a2, b, p : perm] (
 79   consumes m: treeMap k c a1,
 80   consumes accu: b,
 81   f: (k, consumes d: a1, consumes accu: b | p) -> (b | d @ a2)
 82   | p
 83 ) -> (b | m @ treeMap k c a2)
 84 
 85 val fold :
 86   =fold_ascending
 87 
 88 val merge : [k, cmp: term, a, b, c] (
 89   consumes treeMap k cmp a,
 90   consumes treeMap k cmp b,
 91   f: (k, consumes option a, consumes option b) -> option c
 92 ) -> treeMap k cmp c
 93 
 94 val split : [k, cmp: term, a] (
 95   k,
 96   consumes treeMap k cmp a
 97 ) -> (treeMap k cmp a, option a, treeMap k cmp a)
 98 
 99 val filter : [k, cmp: term, a, b] (
100   consumes treeMap k cmp a,
101   p: (k, consumes a) -> option b
102 ) -> treeMap k cmp b
103 
104 val partition : [k, cmp: term, a, b, c] (
105   consumes treeMap k cmp a,
106   p: (k, consumes a) -> choice::choice b c
107 ) -> (treeMap k cmp b, treeMap k cmp c)
108 
109 val compare : [k, cmp: term, a] (
110   (a, a) -> int,
111   treeMap k cmp a,
112   treeMap k cmp a
113 ) -> int
114 
115 val equal : [k, cmp: term, a] (
116   (a, a) -> int,
117   treeMap k cmp a,
118   treeMap k cmp a
119 ) -> bool
120 
121 val bindings : [k, c: term, a] duplicable k => duplicable a => (
122   m: treeMap k c a
123 ) -> list::list (k, a)