1	# rule transcong (opt-in): an `Equal.trans` that an `Equal.cong` feeds (the
2	# name is the two calls, as in fromrev), which a rewrite says shorter.
3	# `Equal.trans(T, a, b, c, Equal.cong(S, T, x => F(x), u, v, e), r)` proves
4	# `{F(u) == c : T}` from `r : {F(v) == c : T}`,
5	# and spells F(u) and F(v) out once more each, as a and b; the rewrite
6	# `%Equal.sym(S, u, v, e) : {F(_) == c : T}`, then `r` on the next line,
7	# names the motive once and drops the middle term (`%e` alone when e is
8	# itself an Equal.sym). With the cong last, `Equal.trans(T, a, b, c, r,
9	# Equal.cong(S, T, x => F(x), u, v, e))` is `%e : {a == F(_) : T}`, then `r`.
10	# The rewrite is a statement: in an argument it goes in parentheses,
11	# `(%e : P; r)`. A let has no type to check it against, so in one
12	# (`+q = Equal.trans(..)`) the rewrite needs an annotation and is left alone.
13	# Exactly: a leaf of a name kind whose text is `Equal.trans`, then, next in
14	# its chain, a group opened by `(` whose kids, split at their comma leaves,
15	# are six arguments (five comma leaves among the kids' own nodes), the fifth
16	# or the sixth of which is exactly a leaf of a name kind whose text is
17	# `Equal.cong` and a group opened by `(` (the kids end right after the group
18	# or go on with a comma); not among the own nodes of a let statement (a `=`
19	# or `<-` among its tokens, as src/syntax/tree.bend reads it) and not after
20	# a `=` or `<-` leaf earlier in its own chain (a let inside a group, as in a
21	# lambda's body written in an argument, which the tree keeps as one chain
22	# rather than statements: the rest of that chain is the let's value, or code
23	# after it the rule leaves alone), and found at any depth otherwise, under
24	# statements and inside groups. One finding for
25	# each, on the `Equal.trans` leaf. The rule reads the shape, not the types:
26	# a motive that `_` cannot mark (a cong under a binder of the lambda's own,
27	# or a chain whose middle term is not the cong's) is still reported. Laws
28	# and proofs are where it looks, so nothing is exempt.
29	import Base
30	import ../../src.bend as Src
31	import ../../finding.bend as F
32	import ../../syntax/lex.bend as Lex
33	import ../../syntax/tree.bend as Tree
34	
35	# is the node a leaf of a name kind with this text?
36	def named(nn: Tree.Node, +tt: String) -> Bool:
37	  match nn:
38	    case Tree.Leaf{Lex.Tok{k, t, _l, _c}}:
39	      Bool.and(Lex.is_name(k), String.eq(t, tt))
40	    case _other:
41	      False{}
42	
43	# is the node a group opened by `(`?
44	def paren(nn: Tree.Node) -> Bool:
45	  match nn:
46	    case Tree.Group{Lex.Tok{_k, o, _l, _c}, _kids, _cl}:
47	      String.eq(o, "(")
48	    case _other:
49	      False{}
50	
51	# is the node a comma leaf?
52	def comma(nn: Tree.Node) -> Bool:
53	  match nn:
54	    case Tree.Leaf{Lex.Tok{k, _t, _l, _c}}:
55	      Lex.is_comma(k)
56	    case _other:
57	      False{}
58	
59	# does the chain end here, or go on with a comma?
60	def ends(nn: Tree.Node) -> Bool:
61	  match nn:
62	    case Tree.NCons{h, _t}:
63	      comma(h)
64	    case _other:
65	      True{}
66	
67	# past the `Equal.cong` leaf: a `(` group, then the argument's end
68	def cong.call(nn: Tree.Node) -> Bool:
69	  match nn:
70	    case Tree.NCons{g, after}:
71	      Bool.and(paren(g), ends(after))
72	    case _other:
73	      False{}
74	
75	# does the chain open an argument that is exactly an `Equal.cong` call?
76	def cong(nn: Tree.Node) -> Bool:
77	  match nn:
78	    case Tree.NCons{h, t}:
79	      Bool.and(named(h, "Equal.cong"), cong.call(t))
80	    case _other:
81	      False{}
82	
83	# the comma leaves among a chain's own nodes
84	def commas(nn: Tree.Node) -> Nat:
85	  match nn:
86	    case Tree.NCons{h, rest}:
87	      Nat.add(Bool.pick(Nat, comma(h), 1n, 0n), commas(rest))
88	    case _other:
89	      0n
90	
91	# is an argument with nc commas before it the fifth or the sixth?
92	def late(+nc: Nat) -> Bool:
93	  Bool.or(Nat.is_eq(nc, 4n), Nat.is_eq(nc, 5n))
94	
95	# from here on in a group's kids, does the fifth or sixth argument open with
96	# an `Equal.cong` call? nc: the commas so far; fresh: an argument opens here;
97	# seen: one did already
98	def fed(nn: Tree.Node, +nc: Nat, +fresh: Bool, +seen: Bool) -> Bool:
99	  match nn:
100	    case Tree.NCons{+h, +rest}:
101	      +here = Bool.and(fresh, Bool.and(late(nc), cong(Tree.NCons{h, rest})))
102	      +cm = comma(h)
103	      fed(rest, Nat.add(nc, Bool.pick(Nat, cm, 1n, 0n)), cm, Bool.or(seen, here))
104	    case _other:
105	      seen
106	
107	# are a call's kids six arguments, the fifth or the sixth an `Equal.cong`?
108	def shape(+kids: Tree.Node) -> Bool:
109	  Bool.and(Nat.is_eq(commas(kids), 5n), fed(kids, 0n, True{}, False{}))
110	
111	# past the `Equal.trans` leaf: a `(` group of that shape
112	def args(nn: Tree.Node) -> Bool:
113	  match nn:
114	    case Tree.NCons{Tree.Group{Lex.Tok{_k, o, _l, _c}, kids, _cl}, _after}:
115	      Bool.and(String.eq(o, "("), shape(kids))
116	    case _other:
117	      False{}
118	
119	# the finding at the `Equal.trans` leaf
120	def cite(+ll: U32, +cc: U32, +path: String) -> F.Finding:
121	  F.Finding{path, ll, cc, 11, "transcong",
122	    "this Equal.trans is fed an Equal.cong: rewrite instead, `%e : {F(_) == c : T}` with the other proof below it, which names the motive once and drops the middle term."}
123	
124	# the finding when a node and the chain after it open the shape
125	def site(hh: Tree.Node, rest: Tree.Node, +path: String) -> List<&2, F.Finding>:
126	  match hh:
127	    case Tree.Leaf{Lex.Tok{k, t, +l, +c}}:
128	      Bool.pick(List<&2, F.Finding>, Bool.and(Bool.and(Lex.is_name(k), String.eq(t, "Equal.trans")), args(rest)),
129	        [cite(l, c, path)], [])
130	    case _other:
131	      []
132	
133	# is the node a `=` or `<-` leaf, a let's?
134	def binds(nn: Tree.Node) -> Bool:
135	  match nn:
136	    case Tree.Leaf{Lex.Tok{Lex.TEq{}, _t, _l, _c}}:
137	      True{}
138	    case Tree.Leaf{Lex.Tok{Lex.TBind{}, _t, _l, _c}}:
139	      True{}
140	    case _other:
141	      False{}
142	
143	# is the statement a let?
144	def is_let(sk: Tree.StmtKind) -> Bool:
145	  match sk:
146	    case Tree.SLet{}:
147	      True{}
148	    case _other:
149	      False{}
150	
151	# every site under the node, at any depth; top: the node is not among a
152	# let's own nodes, nor after a `=` or `<-` leaf in its chain
153	def walk(nn: Tree.Node, +top: Bool, +path: String) -> List<&2, F.Finding>:
154	  match nn:
155	    case Tree.NCons{+h, +rest}:
156	      +here = site(h, rest, path)
157	      List.concat(&2, F.Finding, [Bool.pick(List<&2, F.Finding>, top, here, []), walk(h, True{}, path),
158	        walk(rest, Bool.and(top, Bool.not(binds(h))), path)])
159	    case Tree.Group{_o, kids, _cl}:
160	      walk(kids, True{}, path)
161	    case Tree.Stmt{sk, kids, body}:
162	      List.concat(&2, F.Finding, [walk(kids, Bool.not(is_let(sk)), path), walk(body, True{}, path)])
163	    case _other:
164	      Nil{}
165	
166	# the rule
167	def check(ss: Src.Src) -> List<&2, F.Finding>:
168	  Src.Src{path, _text, _toks, tree, _bound, _items} = ss
169	  walk(tree, True{}, path)