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).
6	import Base
7	import ../paths.bend as Paths
8	import ../syntax/lex.bend as Lex
9	import ../syntax/tree.bend as Tree
10	import ../syntax/bind.bend as Bind
11	import ../lazy/lazy.bend as Lazy
12	
13	# a def: its name, its own tokens (the signature) and the statements under it
14	type 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
18	def 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
26	def 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
36	def 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
44	def 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?
52	def kind.leaf(~test: Lex.TokKind -> Bool, nn: Tree.Node) -> Bool:
53	  kind.of(~test, leaf.kind(nn))
54	
55	# a `:`
56	def 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
64	def kind.upper(kk: Lex.TokKind) -> Bool:
65	  match kk:
66	    case Lex.TUpper{}:
67	      True{}
68	    case other:
69	      False{}
70	
71	# `->`
72	def 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 (`-`, `~`, `+`)
80	def 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
88	def 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)
96	def 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
106	def args(kids: Tree.Node) -> List<&2, Tree.Node>:
107	  args.go(kids, Tree.NNil{}, [])
108	
109	# the nth argument, or nothing
110	def 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?
120	def 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
141	def 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
163	def 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>`)
167	def 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`)
172	def 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	
183	def 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
191	def names(sig: Tree.Node) -> List<&2, String>:
192	  names.go(params(sig), [])
193	
194	# does a chain hold a top-level colon?
195	def 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?
203	def 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
213	def 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
218	def 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
236	def type_head(pp: Tree.Node, +after: Bool) -> String:
237	  type_head.go(pp, after, None{})
238	
239	def 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
252	def 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)?
256	def 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
261	def returns_proof.or(+brace: Bool, more: Bool) -> Bool:
262	  Bool.or(brace, more)
263	
264	# does the signature return a proof, `-> {a == b : T}`?
265	def 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 `->`?
278	def 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 `->`?
286	def 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
292	def 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
297	def exempt(+path: String, sig: Tree.Node) -> Bool:
298	  Bool.or(Paths.is_law_file(path), proof(sig))