spec/containers/balanced_search_tree/recursive.bend
bend-collections-laws-containers@1.0.0.0 · 149 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-containers@1.0.0.0/src/containers/types/balanced_search_tree.bend as E
4
5# Independent model: a finite map as its list of entries in strictly
6# increasing key order (w.r.t. the comparator ~cmp). Nothing here refers to
7# trees, heights or rebalancing.
8
9def ins_at(~K: Data, ~cmp: K -> K -> Cmp, -V: Data, c: Cmp, +k: K, +v: V, +e: E.Entry<K, V>, t: List<&2, E.Entry<K, V>>, rest: List<&2, E.Entry<K, V>>) -> List<&2, E.Entry<K, V>>:
10 match c:
11 case LT{}:
12 Con{E.Entry{k, v}, Con{e, t}}
13 case EQ{}:
14 Con{E.Entry{k, v}, t}
15 case GT{}:
16 Con{e, rest}
17
18# Map k to v: replace the entry with key k, or insert it in key order.
19def ins(~K: Data, ~cmp: K -> K -> Cmp, -V: Data, +k: K, +v: V, xs: List<&2, E.Entry<K, V>>) -> List<&2, E.Entry<K, V>>:
20 match xs:
21 case Nil{}:
22 Con{E.Entry{k, v}, Nil{}}
23 case Con{+e, +t}:
24 ins_at(~K, ~cmp, V, cmp(k, E.key(K, V, e)), k, v, e, t, ins(~K, ~cmp, V, k, v, t))
25
26def keep(c: Cmp) -> Bool:
27 match c:
28 case EQ{}:
29 False{}
30 case _:
31 True{}
32
33def keep_at(-K: Data, -V: Data, b: Bool, +e: E.Entry<K, V>, rest: List<&2, E.Entry<K, V>>) -> List<&2, E.Entry<K, V>>:
34 match b:
35 case True{}:
36 Con{e, rest}
37 case False{}:
38 rest
39
40# Entries whose key is not k.
41def del(~K: Data, ~cmp: K -> K -> Cmp, -V: Data, +k: K, xs: List<&2, E.Entry<K, V>>) -> List<&2, E.Entry<K, V>>:
42 match xs:
43 case Nil{}:
44 Nil{}
45 case Con{+e, t}:
46 keep_at(K, V, keep(cmp(k, E.key(K, V, e))), e, del(~K, ~cmp, V, k, t))
47
48def find_at(-K: Data, -V: Data, c: Cmp, +e: E.Entry<K, V>, rest: Maybe<&2, V>) -> Maybe<&2, V>:
49 match c e:
50 case EQ{} E.Entry{k, v}:
51 Some{v}
52 case _ _:
53 rest
54
55# Value of the first entry with key k.
56def find(~K: Data, ~cmp: K -> K -> Cmp, -V: Data, +k: K, xs: List<&2, E.Entry<K, V>>) -> Maybe<&2, V>:
57 match xs:
58 case Nil{}:
59 None{}
60 case Con{+e, t}:
61 find_at(K, V, cmp(k, E.key(K, V, e)), e, find(~K, ~cmp, V, k, t))
62
63def lb_at(-K: Data, -V: Data, c: Cmp, +e: E.Entry<K, V>, rest: Maybe<&2, E.Entry<K, V>>) -> Maybe<&2, E.Entry<K, V>>:
64 match c:
65 case LT{}:
66 rest
67 case _:
68 Some{e}
69
70# First entry whose key is >= k.
71def lower(~K: Data, ~cmp: K -> K -> Cmp, -V: Data, +k: K, xs: List<&2, E.Entry<K, V>>) -> Maybe<&2, E.Entry<K, V>>:
72 match xs:
73 case Nil{}:
74 None{}
75 case Con{+e, t}:
76 lb_at(K, V, cmp(E.key(K, V, e), k), e, lower(~K, ~cmp, V, k, t))
77
78def in_range(lo_key: Cmp, key_hi: Cmp) -> Bool:
79 Bool.and(Bool.not(Cmp.is_gt(lo_key)), Cmp.is_lt(key_hi))
80
81# Entries with lo <= key < hi, in order.
82def range(~K: Data, ~cmp: K -> K -> Cmp, -V: Data, +lo: K, +hi: K, xs: List<&2, E.Entry<K, V>>) -> List<&2, E.Entry<K, V>>:
83 match xs:
84 case Nil{}:
85 Nil{}
86 case Con{+e, t}:
87 keep_at(K, V, in_range(cmp(lo, E.key(K, V, e)), cmp(E.key(K, V, e), hi)), e, range(~K, ~cmp, V, lo, hi, t))
88
89def value(-V: Data, m: Maybe<&2, V>) -> Result<&2, &2, E.Error, V>:
90 match m:
91 case None{}:
92 Fail{E.KeyNotFound{}}
93 case Some{v}:
94 Done{v}
95
96def entry(-K: Data, -V: Data, m: Maybe<&2, E.Entry<K, V>>, err: E.Error) -> Result<&2, &2, E.Error, E.Entry<K, V>>:
97 match m:
98 case None{}:
99 Fail{err}
100 case Some{e}:
101 Done{e}
102
103def is_some(-V: Data, m: Maybe<&2, V>) -> Bool:
104 match m:
105 case None{}:
106 False{}
107 case Some{v}:
108 True{}
109
110def remove_at(~K: Data, ~cmp: K -> K -> Cmp, -V: Data, m: Maybe<&2, V>, +k: K, +xs: List<&2, E.Entry<K, V>>) -> List<&2, E.Entry<K, V>> & E.Obs<K, V>:
111 match m:
112 case None{}:
113 (xs, E.OVal{Fail{E.KeyNotFound{}}})
114 case Some{v}:
115 (del(~K, ~cmp, V, k, xs), E.OVal{Done{v}})
116
117def step(~K: Data, ~cmp: K -> K -> Cmp, -V: Data, +xs: List<&2, E.Entry<K, V>>, op: E.Op<K, V>) -> List<&2, E.Entry<K, V>> & E.Obs<K, V>:
118 match op:
119 case E.Length{}:
120 (xs, E.ONat{C.length(E.Entry<K, V>, xs)})
121 case E.Insert{+k, +v}:
122 (ins(~K, ~cmp, V, k, v, xs), E.OUnit{})
123 case E.Remove{+k}:
124 remove_at(~K, ~cmp, V, find(~K, ~cmp, V, k, xs), k, xs)
125 case E.Lookup{+k}:
126 (xs, E.OVal{value(V, find(~K, ~cmp, V, k, xs))})
127 case E.Contains{+k}:
128 (xs, E.OBool{is_some(V, find(~K, ~cmp, V, k, xs))})
129 case E.Min{}:
130 (xs, E.OEntry{entry(K, V, C.head(E.Entry<K, V>, xs), E.EmptyTree{})})
131 case E.Max{}:
132 (xs, E.OEntry{entry(K, V, C.last(E.Entry<K, V>, xs), E.EmptyTree{})})
133 case E.LowerBound{+k}:
134 (xs, E.OEntry{entry(K, V, lower(~K, ~cmp, V, k, xs), E.KeyNotFound{})})
135 case E.Range{+lo, +hi}:
136 (xs, E.OList{range(~K, ~cmp, V, lo, hi, xs)})
137 case E.ToList{}:
138 (xs, E.OList{xs})
139
140def cons_obs(-K: Data, -V: Data, o: E.Obs<K, V>, r: List<&2, E.Entry<K, V>> & List<&2, E.Obs<K, V>>) -> List<&2, E.Entry<K, V>> & List<&2, E.Obs<K, V>>:
141 (m, os) = r
142 (m, Con{o, os})
143
144def run(~K: Data, ~cmp: K -> K -> Cmp, -V: Data, ops: List<&2, E.Op<K, V>>, +xs: List<&2, E.Entry<K, V>>) -> List<&2, E.Entry<K, V>> & List<&2, E.Obs<K, V>>:
145 match ops:
146 case Nil{}:
147 (xs, Nil{})
148 case Con{+op, rest}:
149 cons_obs(K, V, Pair.snd(List<&2, E.Entry<K, V>>, E.Obs<K, V>, step(~K, ~cmp, V, xs, op)), run(~K, ~cmp, V, rest, Pair.fst(List<&2, E.Entry<K, V>>, E.Obs<K, V>, step(~K, ~cmp, V, xs, op))))