src/rules/calls.bend
bolt@1.23.0.0 · 298 lines · 0 definitions
1# src/rules/calls: what the recursion rules (pick, strict, tail, concat,
2# index) share. A file's defs, each with its name, its signature and its body;
3# a call's arguments; whether a def calls itself; its parameters, and the type
4# of the one it walks; and whether it is exempt (a law or a proof never runs,
5# and a def with no type fills a law: it is a proof).
6import Base
7import bolt@1.23.0.0/src/paths.bend as Paths
8import bolt@1.23.0.0/src/syntax/lex.bend as Lex
9import bolt@1.23.0.0/src/syntax/tree.bend as Tree
10import bolt@1.23.0.0/src/syntax/bind.bend as Bind
11import bolt@1.23.0.0/src/lazy/lazy.bend as Lazy
12
13# a def: its name, its own tokens (the signature) and the statements under it
14type Def is Data:
15 Def{name: String, sig: Tree.Node, body: Tree.Node}
16
17# a def with a name joins the others; one without (half-written) does not
18def defs.push(mm: Maybe<&2, String>, sig: Tree.Node, body: Tree.Node, acc: List<&2, Def>) -> List<&2, Def>:
19 match mm:
20 case None{}:
21 acc
22 case Some{name}:
23 Def{name, sig, body} <> acc
24
25# the defs of a parsed source, in order
26def defs(root: Tree.Node) -> List<&2, Def>:
27 match root:
28 case Tree.NCons{Tree.Stmt{Tree.SDef{}, +kids, body}, rest}:
29 defs.push(Bind.declared(kids), kids, body, defs(rest))
30 case Tree.NCons{h, rest}:
31 defs(rest)
32 case other:
33 Nil{}
34
35# a leaf's kind, none for anything else: kind tests read this, never a text
36def leaf.kind(nn: Tree.Node) -> Maybe<&2, Lex.TokKind>:
37 match nn:
38 case Tree.Leaf{Lex.Tok{k, t, l, c}}:
39 Some{k}
40 case other:
41 None{}
42
43# a kind test on a kind, when there is one
44def kind.of(~test: Lex.TokKind -> Bool, mm: Maybe<&2, Lex.TokKind>) -> Bool:
45 match mm:
46 case None{}:
47 False{}
48 case Some{k}:
49 test(k)
50
51# a leaf of this kind?
52def kind.leaf(~test: Lex.TokKind -> Bool, nn: Tree.Node) -> Bool:
53 kind.of(~test, leaf.kind(nn))
54
55# a `:`
56def kind.colon(kk: Lex.TokKind) -> Bool:
57 match kk:
58 case Lex.TColon{}:
59 True{}
60 case other:
61 False{}
62
63# a capitalized name
64def kind.upper(kk: Lex.TokKind) -> Bool:
65 match kk:
66 case Lex.TUpper{}:
67 True{}
68 case other:
69 False{}
70
71# `->`
72def kind.arrow(kk: Lex.TokKind) -> Bool:
73 match kk:
74 case Lex.TArrow{}:
75 True{}
76 case other:
77 False{}
78
79# a plain operator (`-`, `~`, `+`)
80def kind.oper(kk: Lex.TokKind) -> Bool:
81 match kk:
82 case Lex.TOp{}:
83 True{}
84 case other:
85 False{}
86
87# a leaf's text, "" for anything else
88def leaf.text(nn: Tree.Node) -> String:
89 match nn:
90 case Tree.Leaf{Lex.Tok{k, t, l, c}}:
91 t
92 case other:
93 ""
94
95# the arguments of a group, split at its top-level commas (each a chain)
96def args.go(kids: Tree.Node, +cur: Tree.Node, +acc: List<&2, Tree.Node>) -> List<&2, Tree.Node>:
97 match kids:
98 case Tree.NCons{+h, +rest}:
99 Lazy.either(List<&2, Tree.Node>, kind.leaf(~Lex.is_comma, h),
100 _u => args.go(rest, Tree.NNil{}, Tree.reverse(cur, Tree.NNil{}) <> acc),
101 _v => args.go(rest, Tree.NCons{h, cur}, acc))
102 case other:
103 List.reverse(&2, Tree.Node, Tree.reverse(cur, Tree.NNil{}) <> acc)
104
105# the arguments of a group
106def args(kids: Tree.Node) -> List<&2, Tree.Node>:
107 args.go(kids, Tree.NNil{}, [])
108
109# the nth argument, or nothing
110def arg(as: List<&2, Tree.Node>, nn: Nat) -> Tree.Node:
111 match as nn:
112 case Con{h, t} 0n:
113 h
114 case Con{h, t} 1n+p:
115 arg(t, p)
116 case Nil{} m:
117 Tree.NNil{}
118
119# is there a call of the name, `name(..)`, anywhere under the node?
120def calls(nn: Tree.Node, +name: String) -> Bool:
121 match nn:
122 case Tree.NCons{Tree.Leaf{Lex.Tok{k, +t, l, c}}, Tree.NCons{Tree.Group{Lex.Tok{_, +o, _, _}, kids, _}, rest}}:
123 +a = calls(kids, name)
124 +b = calls(rest, name)
125 Bool.or(Bool.and(String.eq(o, "("), String.eq(t, name)), Bool.or(a, b))
126 case Tree.Group{open, kids, close}:
127 calls(kids, name)
128 case Tree.Stmt{kind, kids, body}:
129 +a = calls(kids, name)
130 +b = calls(body, name)
131 Bool.or(a, b)
132 case Tree.NCons{h, t}:
133 +a = calls(h, name)
134 +b = calls(t, name)
135 Bool.or(a, b)
136 case other:
137 False{}
138
139# the kids of a signature's first `(` group: the parameters; hit: a group
140# before sig was one, so the search stops there
141def params.of.go(sig: Tree.Node, hit: Maybe<&2, Tree.Node>) -> Tree.Node:
142 match sig:
143 case Tree.NCons{Tree.Group{Lex.Tok{k, +o, l, c}, kids, close}, rest}:
144 match hit:
145 case Some{x}:
146 x
147 case None{}:
148 params.of.go(rest, Bool.pick(Maybe<&2, Tree.Node>, String.eq(o, "("), Some{kids}, None{}))
149 case Tree.NCons{h, rest}:
150 match hit:
151 case Some{x}:
152 x
153 case None{}:
154 params.of.go(rest, None{})
155 case other:
156 match hit:
157 case Some{x}:
158 x
159 case None{}:
160 Tree.NNil{}
161
162# the kids of a signature's first `(` group: the parameters
163def params.of(sig: Tree.Node) -> Tree.Node:
164 params.of.go(sig, None{})
165
166# a def's parameters, each its chain up to a comma (`+xs: List<&2, U32>`)
167def params(sig: Tree.Node) -> List<&2, Tree.Node>:
168 args(params.of(sig))
169
170# a parameter's name: its first lowercase name before the colon ("" for a
171# type parameter like `-A: Type`)
172def param_name(pp: Tree.Node) -> String:
173 match pp:
174 case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TName{}, t, l, c}}, rest}:
175 t
176 case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TColon{}, t, l, c}}, rest}:
177 ""
178 case Tree.NCons{h, rest}:
179 param_name(rest)
180 case other:
181 ""
182
183def names.go(ps: List<&2, Tree.Node>, acc: List<&2, String>) -> List<&2, String>:
184 match ps:
185 case Nil{}:
186 List.reverse(&2, String, acc)
187 case Con{p, rest}:
188 names.go(rest, param_name(p) <> acc)
189
190# the names of a def's parameters
191def names(sig: Tree.Node) -> List<&2, String>:
192 names.go(params(sig), [])
193
194# does a chain hold a top-level colon?
195def has_colon(pp: Tree.Node) -> Bool:
196 match pp:
197 case Tree.NCons{h, rest}:
198 Lazy.or_else(kind.leaf(~kind.colon, h), _u => has_colon(rest))
199 case other:
200 False{}
201
202# does the chain open with a `-` or `~` operator?
203def is_live.sign(pp: Tree.Node) -> Bool:
204 match pp:
205 case Tree.NCons{+h, rest}:
206 +t = leaf.text(h)
207 Bool.and(kind.leaf(~kind.oper, h), Bool.or(String.eq(t, "-"), String.eq(t, "~")))
208 case other:
209 False{}
210
211# a live parameter: typed, and neither erased (`-A: Type`) nor a template
212# (`~f: A -> B`); a bare quantity name (`a` in `List.get(a, ..)`) is not one
213def is_live(+pp: Tree.Node) -> Bool:
214 Bool.and(Bool.not(is_live.sign(pp)), has_colon(pp))
215
216# the head of a parameter's type: the first capitalized name after the
217# colon, "" for none; hit: a name before pp was it, so the search stops there
218def type_head.go(pp: Tree.Node, +after: Bool, hit: Maybe<&2, String>) -> String:
219 match pp:
220 case Tree.NCons{+h, rest}:
221 match hit:
222 case Some{s}:
223 s
224 case None{}:
225 type_head.go(rest, Bool.or(after, kind.leaf(~kind.colon, h)),
226 Bool.pick(Maybe<&2, String>, Bool.and(after, kind.leaf(~kind.upper, h)), Some{leaf.text(h)}, None{}))
227 case other:
228 match hit:
229 case Some{s}:
230 s
231 case None{}:
232 ""
233
234# the head of a parameter's type: the first capitalized name after the colon
235# (`List` in `+xs: +List<A>`), "" for none
236def type_head(pp: Tree.Node, +after: Bool) -> String:
237 type_head.go(pp, after, None{})
238
239def walked.go(ps: List<&2, Tree.Node>, found: Maybe<&2, String>) -> String:
240 match ps found:
241 case Con{+p, rest} None{}:
242 walked.go(rest, Lazy.stop(Maybe<&2, String>, Bool.not(is_live(p)), None{},
243 _u => Some{type_head(p, False{})}))
244 case Con{p, rest} Some{t}:
245 t
246 case Nil{} Some{t}:
247 t
248 case Nil{} None{}:
249 ""
250
251# the type head of the first live parameter: the one a self-call must shrink
252def walked(sig: Tree.Node) -> String:
253 walked.go(params(sig), None{})
254
255# does the def walk a list or a string (its first live parameter's type)?
256def seq(sig: Tree.Node) -> Bool:
257 +h = walked(sig)
258 Bool.or(String.eq(h, "List"), String.eq(h, "String"))
259
260# a `{` group after the arrow, or a proof further on
261def returns_proof.or(+brace: Bool, more: Bool) -> Bool:
262 Bool.or(brace, more)
263
264# does the signature return a proof, `-> {a == b : T}`?
265def returns_proof(sig: Tree.Node) -> Bool:
266 match sig:
267 case Tree.NCons{h, +rest}:
268 match rest:
269 case Tree.NCons{+g, r2}:
270 Lazy.either(Bool, kind.leaf(~kind.arrow, h), _u => returns_proof.or(Tree.opens(g, "{"), returns_proof(r2)),
271 _v => returns_proof(rest))
272 case _r:
273 returns_proof(rest)
274 case other:
275 False{}
276
277# does a chain hold a top-level `->`?
278def has_arrow(pp: Tree.Node) -> Bool:
279 match pp:
280 case Tree.NCons{h, rest}:
281 Lazy.or_else(kind.leaf(~kind.arrow, h), _u => has_arrow(rest))
282 case other:
283 False{}
284
285# does the signature write a type: a `:` among its parameters, or a `->`?
286def typed(+sig: Tree.Node) -> Bool:
287 Lazy.or_else(has_colon(params.of(sig)), _u => has_arrow(sig))
288
289# is the def a proof? One that returns a proof (`-> {a == b : T}`), or one
290# written with no type at all (`def f(x, y):`), which is how Bend fills the
291# law named f
292def proof(+sig: Tree.Node) -> Bool:
293 Bool.or(returns_proof(sig), Bool.not(typed(sig)))
294
295# a law file, a proof file, or a def that is a proof: none of it runs, so its
296# cost does not matter
297def exempt(+path: String, sig: Tree.Node) -> Bool:
298 Bool.or(Paths.is_law_file(path), proof(sig))