src/rules/style/transcong.bend

bolt@1.27.0.0 · 169 lines · 17 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.27.0.0/src/src.bend as Src
31import bolt@1.27.0.0/src/finding.bend as F
32import bolt@1.27.0.0/src/syntax/lex.bend as Lex
33import bolt@1.27.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)