1	import Base
2	import ./invariants.bend as Inv
3	import ./map_insert.bend as I
4	import ./map_critbit_parts.bend as Parts
5	import ./map_routing.bend as R
6	
7	law branch:
8	  for -V: Data
9	  for +p: Nat
10	  for +lo: Map<&2, V>
11	  for +hi: Map<&2, V>
12	  for +key: String
13	  for bit: Bool
14	  for route: {Map.bit(key, p) == (key, bit) : String & Bool}
15	  for left: {Maybe.is_some(&2, String, I.seek_found(V, Map.seek(&2, V, lo, key))) == True{} : Bool}
16	  for right: {Maybe.is_some(&2, String, I.seek_found(V, Map.seek(&2, V, hi, key))) == True{} : Bool}
17	  {Maybe.is_some(&2, String, I.seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key))) == True{} : Bool}
18	def branch(V, p, lo, hi, key, bit, route, left, right):
19	  match bit:
20	    case False{}:
21	      %Equal.sym(Maybe<&2, String>, I.seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key)), I.seek_found(V, Map.seek(&2, V, lo, key)), I.seek_left(V, lo, hi, p, key, route)) : {Maybe.is_some(&2, String, _) == True{} : Bool}
22	      left
23	    case True{}:
24	      %Equal.sym(Maybe<&2, String>, I.seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key)), I.seek_found(V, Map.seek(&2, V, hi, key)), I.seek_right(V, lo, hi, p, key, route)) : {Maybe.is_some(&2, String, _) == True{} : Bool}
25	      right
26	
27	law from_parts:
28	  for -V: Data
29	  for +p: Nat
30	  for +lo: Map<&2, V>
31	  for +hi: Map<&2, V>
32	  for +key: String
33	  for facts: Parts.NodeFacts(V, p, lo, hi)
34	  for left: {Inv.critbit(V, lo) == True{} : Bool} -> {Inv.nonempty(V, lo) == True{} : Bool} -> {Maybe.is_some(&2, String, I.seek_found(V, Map.seek(&2, V, lo, key))) == True{} : Bool}
35	  for right: {Inv.critbit(V, hi) == True{} : Bool} -> {Inv.nonempty(V, hi) == True{} : Bool} -> {Maybe.is_some(&2, String, I.seek_found(V, Map.seek(&2, V, hi, key))) == True{} : Bool}
36	  {Maybe.is_some(&2, String, I.seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key))) == True{} : Bool}
37	def from_parts(V, p, lo, hi, key, facts, left, right):
38	  match facts:
39	    case (common, nl, nh, bl, bh, rl, rh, vl, vh):
40	      branch(V, p, lo, hi, key, I.route_bit(Map.bit(key, p)), I.route_shape(key, p), left(vl, nl), right(vh, nh))
41	
42	# A valid nonempty native tree cannot seek into an empty child.
43	law nonempty_seek:
44	  for -V: Data
45	  for tree: Map<&2, V>
46	  for +key: String
47	  for valid: {Inv.critbit(V, tree) == True{} : Bool}
48	  for occupied: {Inv.nonempty(V, tree) == True{} : Bool}
49	  {Maybe.is_some(&2, String, I.seek_found(V, Map.seek(&2, V, tree, key))) == True{} : Bool}
50	def nonempty_seek(V, tree, key, valid, occupied):
51	  match tree:
52	    case MTip{}: Empty.absurd({Maybe.is_some(&2, String, I.seek_found(V, Map.seek(&2, V, MTip{}, key))) == True{} : Bool}, R.false_true(occupied))
53	    case MLeaf{stored, value}: {==}
54	    case MNode{+p, +lo, +hi}:
55	      from_parts(V, p, lo, hi, key, Parts.node_parts(V, p, lo, hi, valid), v => n => nonempty_seek(V, lo, key, v, n), v => n => nonempty_seek(V, hi, key, v, n))
56	
57	law empty_seek_is_tip:
58	  for -V: Data
59	  for tree: Map<&2, V>
60	  for +key: String
61	  for valid: {Inv.critbit(V, tree) == True{} : Bool}
62	  for missing: {I.seek_found(V, Map.seek(&2, V, tree, key)) == None{} : Maybe<&2, String>}
63	  {tree == MTip{} : Map<&2, V>}
64	def empty_seek_is_tip(V, tree, key, valid, missing):
65	  match tree:
66	    case MTip{}: {==}
67	    case MLeaf{stored, value}:
68	      Empty.absurd({MLeaf{stored, value} == MTip{} : Map<&2, V>}, R.false_true(Equal.sym(Bool, True{}, False{}, Equal.cong(Maybe<&2, String>, Bool, m => Maybe.is_some(&2, String, m), Some{stored}, None{}, missing))))
69	    case MNode{+p, +lo, +hi}:
70	      present = nonempty_seek(V, MNode{p, lo, hi}, key, valid, {==})
71	      absent = Equal.cong(Maybe<&2, String>, Bool, m => Maybe.is_some(&2, String, m), I.seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key)), None{}, missing)
72	      Empty.absurd({MNode{p, lo, hi} == MTip{} : Map<&2, V>}, R.false_true(Equal.trans(Bool, False{}, Maybe.is_some(&2, String, I.seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key))), True{}, Equal.sym(Bool, Maybe.is_some(&2, String, I.seek_found(V, Map.seek(&2, V, MNode{p, lo, hi}, key))), False{}, absent), present)))