1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/order.bend as O
4	import ../../../spec/lib/common.bend as SC
5	import ../../../spec/containers/balanced_search_tree/main.bend as S
6	import ../../../src/containers/balanced_search_tree.bend as M
7	import ./ord.bend as OR
8	
9	# The specification's first_where and last_where over sorted entries split
10	# by a key k: entries below k never qualify upward and always downward,
11	# entries above k the other way round. (source: tools/generators/tm_hand/navl.src)
12	
13	
14	def fw_app_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +incl: Bool, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +ys: List<&2, M.Entry<K, V>>, +b: Bool, +hb: {S.ordering_ok(cmp(k, S.key(K, V, e)), incl) == b : Bool}, +ih: {S.first_where(~K, ~V, ~cmp, k, incl, SC.append(M.Entry<K, V>, t, ys)) == OR.orm(M.Entry<K, V>, S.first_where(~K, ~V, ~cmp, k, incl, t), S.first_where(~K, ~V, ~cmp, k, incl, ys)) : Maybe<&2, M.Entry<K, V>>}) -> {S.first_where(~K, ~V, ~cmp, k, incl, SC.append(M.Entry<K, V>, Con{e, t}, ys)) == OR.orm(M.Entry<K, V>, S.first_where(~K, ~V, ~cmp, k, incl, Con{e, t}), S.first_where(~K, ~V, ~cmp, k, incl, ys)) : Maybe<&2, M.Entry<K, V>>}:
15	  match b:
16	    case True{}:
17	      %Equal.sym(Bool, S.ordering_ok(cmp(k, S.key(K, V, e)), incl), True{}, hb) : {S.pick(Maybe<&2, M.Entry<K, V>>, _, Some{e}, S.first_where(~K, ~V, ~cmp, k, incl, SC.append(M.Entry<K, V>, t, ys))) == OR.orm(M.Entry<K, V>, S.pick(Maybe<&2, M.Entry<K, V>>, _, Some{e}, S.first_where(~K, ~V, ~cmp, k, incl, t)), S.first_where(~K, ~V, ~cmp, k, incl, ys)) : Maybe<&2, M.Entry<K, V>>}
18	      {==}
19	    case False{}:
20	      %Equal.sym(Bool, S.ordering_ok(cmp(k, S.key(K, V, e)), incl), False{}, hb) : {S.pick(Maybe<&2, M.Entry<K, V>>, _, Some{e}, S.first_where(~K, ~V, ~cmp, k, incl, SC.append(M.Entry<K, V>, t, ys))) == OR.orm(M.Entry<K, V>, S.pick(Maybe<&2, M.Entry<K, V>>, _, Some{e}, S.first_where(~K, ~V, ~cmp, k, incl, t)), S.first_where(~K, ~V, ~cmp, k, incl, ys)) : Maybe<&2, M.Entry<K, V>>}
21	      ih
22	
23	def fw_app(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +incl: Bool, +xs: List<&2, M.Entry<K, V>>, +ys: List<&2, M.Entry<K, V>>) -> {S.first_where(~K, ~V, ~cmp, k, incl, SC.append(M.Entry<K, V>, xs, ys)) == OR.orm(M.Entry<K, V>, S.first_where(~K, ~V, ~cmp, k, incl, xs), S.first_where(~K, ~V, ~cmp, k, incl, ys)) : Maybe<&2, M.Entry<K, V>>}:
24	  match xs:
25	    case Nil{}:
26	      {==}
27	    case Con{+e, +t}:
28	      fw_app_c(~K, ~V, ~cmp, k, incl, e, t, ys, S.ordering_ok(cmp(k, S.key(K, V, e)), incl), {==}, fw_app(~K, ~V, ~cmp, k, incl, t, ys))
29	
30	# nothing below k is at or above it
31	def fw_none(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +k: K, +incl: Bool, +es: List<&2, M.Entry<K, V>>, +h: {OR.ltall(~K, ~V, ~cmp, k, es) == True{} : Bool}) -> {S.first_where(~K, ~V, ~cmp, k, incl, es) == None{} : Maybe<&2, M.Entry<K, V>>}:
32	  match es:
33	    case Nil{}:
34	      {==}
35	    case Con{+e, +t}:
36	      %Equal.sym(Cmp, cmp(k, S.key(K, V, e)), GT{}, OR.lt_gt(~K, ~cmp, ~o, S.key(K, V, e), k, L.and_left(Cmp.is_lt(cmp(S.key(K, V, e), k)), OR.ltall(~K, ~V, ~cmp, k, t), h))) : {S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(_, incl), Some{e}, S.first_where(~K, ~V, ~cmp, k, incl, t)) == None{} : Maybe<&2, M.Entry<K, V>>}
37	      fw_none(~K, ~V, ~cmp, ~o, k, incl, t, L.and_right(Cmp.is_lt(cmp(S.key(K, V, e), k)), OR.ltall(~K, ~V, ~cmp, k, t), h))
38	
39	# everything above k qualifies: the first
40	def fw_head(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +incl: Bool, +es: List<&2, M.Entry<K, V>>, +h: {OR.gtall(~K, ~V, ~cmp, k, es) == True{} : Bool}) -> {S.first_where(~K, ~V, ~cmp, k, incl, es) == S.head(M.Entry<K, V>, es) : Maybe<&2, M.Entry<K, V>>}:
41	  match es:
42	    case Nil{}:
43	      {==}
44	    case Con{+e, +t}:
45	      %Equal.sym(Cmp, cmp(k, S.key(K, V, e)), LT{}, O.lt_is(cmp(k, S.key(K, V, e)), L.and_left(Cmp.is_lt(cmp(k, S.key(K, V, e))), OR.gtall(~K, ~V, ~cmp, k, t), h))) : {S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(_, incl), Some{e}, S.first_where(~K, ~V, ~cmp, k, incl, t)) == Some{e} : Maybe<&2, M.Entry<K, V>>}
46	      {==}
47	
48	def lw_app(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +incl: Bool, +xs: List<&2, M.Entry<K, V>>, +ys: List<&2, M.Entry<K, V>>, +b: Maybe<&2, M.Entry<K, V>>) -> {S.last_where(~K, ~V, ~cmp, k, incl, SC.append(M.Entry<K, V>, xs, ys), b) == S.last_where(~K, ~V, ~cmp, k, incl, ys, S.last_where(~K, ~V, ~cmp, k, incl, xs, b)) : Maybe<&2, M.Entry<K, V>>}:
49	  match xs:
50	    case Nil{}:
51	      {==}
52	    case Con{+e, +t}:
53	      lw_app(~K, ~V, ~cmp, k, incl, t, ys, S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(cmp(S.key(K, V, e), k), incl), Some{e}, b))
54	
55	# nothing above k is at or below it: the candidate stays
56	def lw_none(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +k: K, +incl: Bool, +es: List<&2, M.Entry<K, V>>, +b: Maybe<&2, M.Entry<K, V>>, +h: {OR.gtall(~K, ~V, ~cmp, k, es) == True{} : Bool}) -> {S.last_where(~K, ~V, ~cmp, k, incl, es, b) == b : Maybe<&2, M.Entry<K, V>>}:
57	  match es:
58	    case Nil{}:
59	      {==}
60	    case Con{+e, +t}:
61	      %Equal.sym(Cmp, cmp(S.key(K, V, e), k), GT{}, OR.lt_gt(~K, ~cmp, ~o, k, S.key(K, V, e), L.and_left(Cmp.is_lt(cmp(k, S.key(K, V, e))), OR.gtall(~K, ~V, ~cmp, k, t), h))) : {S.last_where(~K, ~V, ~cmp, k, incl, t, S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(_, incl), Some{e}, b)) == b : Maybe<&2, M.Entry<K, V>>}
62	      lw_none(~K, ~V, ~cmp, ~o, k, incl, t, b, L.and_right(Cmp.is_lt(cmp(k, S.key(K, V, e))), OR.gtall(~K, ~V, ~cmp, k, t), h))
63	
64	def last_orm(-K: Data, -V: Data, +u: List<&2, M.Entry<K, V>>, +e: M.Entry<K, V>, +a: Maybe<&2, M.Entry<K, V>>, +b: Maybe<&2, M.Entry<K, V>>) -> {OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, Con{e, u}), a) == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, Con{e, u}), b) : Maybe<&2, M.Entry<K, V>>}:
65	  match u:
66	    case Nil{}:
67	      {==}
68	    case Con{+e2, +u2}:
69	      last_orm(K, V, u2, e2, a, b)
70	
71	def lw_all_c(-K: Data, -V: Data, +e: M.Entry<K, V>, +t: List<&2, M.Entry<K, V>>, +b: Maybe<&2, M.Entry<K, V>>) -> {OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, t), Some{e}) == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, Con{e, t}), b) : Maybe<&2, M.Entry<K, V>>}:
72	  match t:
73	    case Nil{}:
74	      {==}
75	    case Con{+e2, +u}:
76	      last_orm(K, V, u, e2, Some{e}, b)
77	
78	# everything below k qualifies: the last, or the candidate when none
79	def lw_all(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +incl: Bool, +es: List<&2, M.Entry<K, V>>, +b: Maybe<&2, M.Entry<K, V>>, +h: {OR.ltall(~K, ~V, ~cmp, k, es) == True{} : Bool}) -> {S.last_where(~K, ~V, ~cmp, k, incl, es, b) == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, es), b) : Maybe<&2, M.Entry<K, V>>}:
80	  match es:
81	    case Nil{}:
82	      {==}
83	    case Con{+e, +t}:
84	      %Equal.sym(Cmp, cmp(S.key(K, V, e), k), LT{}, O.lt_is(cmp(S.key(K, V, e), k), L.and_left(Cmp.is_lt(cmp(S.key(K, V, e), k)), OR.ltall(~K, ~V, ~cmp, k, t), h))) : {S.last_where(~K, ~V, ~cmp, k, incl, t, S.pick(Maybe<&2, M.Entry<K, V>>, S.ordering_ok(_, incl), Some{e}, b)) == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, Con{e, t}), b) : Maybe<&2, M.Entry<K, V>>}
85	      %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, incl, t, Some{e}), OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, t), Some{e}), lw_all(~K, ~V, ~cmp, k, incl, t, Some{e}, L.and_right(Cmp.is_lt(cmp(S.key(K, V, e), k)), OR.ltall(~K, ~V, ~cmp, k, t), h))) : {_ == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, Con{e, t}), b) : Maybe<&2, M.Entry<K, V>>}
86	      lw_all_c(K, V, e, t, b)
87	
88	def ltall_app(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +k: K, +xs: List<&2, M.Entry<K, V>>, +ys: List<&2, M.Entry<K, V>>, +hx: {OR.ltall(~K, ~V, ~cmp, k, xs) == True{} : Bool}, +hy: {OR.ltall(~K, ~V, ~cmp, k, ys) == True{} : Bool}) -> {OR.ltall(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, xs, ys)) == True{} : Bool}:
89	  match xs:
90	    case Nil{}:
91	      hy
92	    case Con{+e, +t}:
93	      L.and_intro(Cmp.is_lt(cmp(S.key(K, V, e), k)), OR.ltall(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, t, ys)), L.and_left(Cmp.is_lt(cmp(S.key(K, V, e), k)), OR.ltall(~K, ~V, ~cmp, k, t), hx), ltall_app(~K, ~V, ~cmp, k, t, ys, L.and_right(Cmp.is_lt(cmp(S.key(K, V, e), k)), OR.ltall(~K, ~V, ~cmp, k, t), hx), hy))