1	import Base
2	import ../rose/type.bend as R
3	import ../rose/ops.bend as RO
4	import ./edge/type.bend as E
5	import ./type.bend as C
6	
7	def keys(-N: Data, c: C.Compound<N>) -> List<&2, String>:
8	  match c:
9	    case C.Compound{rs, _}:
10	      RO.keys(N, rs)
11	
12	def edges(-N: Data, c: C.Compound<N>) -> List<&2, E.Edge>:
13	  match c:
14	    case C.Compound{_, es}:
15	      es
16	
17	# ---- invariants ----
18	def has(+ks: List<&2, String>, +k: String) -> Bool:
19	  List.contains(~String, ~String.eq, ks, k)
20	
21	def ends_resolve(es: List<&2, E.Edge>, +ks: List<&2, String>) -> Bool:
22	  match es:
23	    case []:
24	      True{}
25	    case e <> rest:
26	      match e:
27	        case E.Edge{a, b, _, _}:
28	          has(ks, a) && has(ks, b) && ends_resolve(rest, ks)
29	
30	# Every edge joins two keys the forest has.
31	def resolves(-N: Data, +c: C.Compound<N>) -> Bool:
32	  ends_resolve(edges(N, c), keys(N, c))
33	
34	def distinct(+ks: List<&2, String>) -> Bool:
35	  Nat.is_eq(Set.size(Set.from_list(ks)), List.length(&2, String, ks))
36	
37	# No key names two things.
38	def unique(-N: Data, c: C.Compound<N>) -> Bool:
39	  distinct(keys(N, c))
40	
41	# ---- lifting: an edge as seen when only some keys are visible ----
42	# A key shows as itself when visible, else as its nearest visible ancestor, else not at all ("").
43	def above_of(+k: String, ps: List<&2, RO.Place>) -> List<&2, String>:
44	  match ps:
45	    case []:
46	      []
47	    case p <> rest:
48	      match p:
49	        case RO.Place{pk, ab}:
50	          Bool.pick(List<&2, String>, String.eq(k, pk), ab, above_of(k, rest))
51	
52	def visible_or(hit: Bool, +k: String, rest: String) -> String:
53	  match hit:
54	    case True{}:
55	      k
56	    case False{}:
57	      rest
58	
59	def first_visible(cands: List<&2, String>, +visible: List<&2, String>) -> String:
60	  match cands:
61	    case []:
62	      ""
63	    case +c <> rest:
64	      visible_or(has(visible, c), c, first_visible(rest, visible))
65	
66	def shown_as(+k: String, +ps: List<&2, RO.Place>, +visible: List<&2, String>) -> String:
67	  first_visible(k <> above_of(k, ps), visible)
68	
69	def drawn(+a: String, +b: String, es: List<&2, E.Edge>) -> Bool:
70	  match es:
71	    case []:
72	      False{}
73	    case e <> rest:
74	      match e:
75	        case E.Edge{x, y, _, _}:
76	          (String.eq(a, x) && String.eq(b, y)) || drawn(a, b, rest)
77	
78	def keep(c: Bool, e: E.Edge, rest: List<&2, E.Edge>) -> List<&2, E.Edge>:
79	  match c:
80	    case True{}:
81	      e <> rest
82	    case False{}:
83	      rest
84	
85	# An edge is kept when both ends show, as two different things, not already drawn.
86	def keep_edge(+a: String, +b: String, l: String, t: String, +rest: List<&2, E.Edge>) -> List<&2, E.Edge>:
87	  keep(Bool.not(String.is_empty(a)) && Bool.not(String.is_empty(b)) && Bool.not(String.eq(a, b)) && Bool.not(drawn(a, b, rest)), E.Edge{a, b, l, t}, rest)
88	
89	def lift_edges(es: List<&2, E.Edge>, +ps: List<&2, RO.Place>, +visible: List<&2, String>) -> List<&2, E.Edge>:
90	  match es:
91	    case []:
92	      []
93	    case e <> rest:
94	      match e:
95	        case E.Edge{a, b, l, t}:
96	          keep_edge(shown_as(a, ps, visible), shown_as(b, ps, visible), l, t, lift_edges(rest, ps, visible))
97	
98	# The compound's edges between the visible keys, each end moved up to what shows.
99	def lift(-N: Data, c: C.Compound<N>, +visible: List<&2, String>) -> List<&2, E.Edge>:
100	  match c:
101	    case C.Compound{rs, es}:
102	      lift_edges(List.reverse(&2, E.Edge, es), RO.places(N, rs, []), visible)