src/rules/style/transcong.bend
bolt@1.24.0.0 · 169 lines · 0 definitions
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.
29import Base
30import bolt@1.24.0.0/src/src.bend as Src
31import bolt@1.24.0.0/src/finding.bend as F
32import bolt@1.24.0.0/src/syntax/lex.bend as Lex
33import bolt@1.24.0.0/src/syntax/tree.bend as Tree
34
35# is the node a leaf of a name kind with this text?
36def 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 `(`?
44def 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?
52def 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?
60def 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
68def 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?
76def 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
84def 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?
92def 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
98def 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`?
108def 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
112def 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
120def 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
125def 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?
134def 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?
144def 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
153def 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
167def check(ss: Src.Src) -> List<&2, F.Finding>:
168 Src.Src{path, _text, _toks, tree, _bound, _items} = ss
169 walk(tree, True{}, path)