1	import Base
2	import ../../lib/common.bend as C
3	import ../../../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	
9	def 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.
19	def 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	
26	def keep(c: Cmp) -> Bool:
27	  match c:
28	    case EQ{}:
29	      False{}
30	    case _:
31	      True{}
32	
33	def 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.
41	def 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	
48	def 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.
56	def 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	
63	def 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.
71	def 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	
78	def 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.
82	def 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	
89	def 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	
96	def 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	
103	def is_some(-V: Data, m: Maybe<&2, V>) -> Bool:
104	  match m:
105	    case None{}:
106	      False{}
107	    case Some{v}:
108	      True{}
109	
110	def 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	
117	def 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	
140	def 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	
144	def 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))))