src/syntax/process/case_usefulness.ghul

1		namespace Syntax.Process is
2		// Decides whether a pattern vector matches anything the rows
3		// above it do not, and produces witnesses — the value shapes that
4		// escape — when it does.
5		//
6		// Both questions a `case` needs are this one query: the arms are
7		// exhaustive when a row of wildcards is useless against all of
8		// them, and an arm is redundant when its own row is useless
9		// against the arms before it.
10		//
11		// The walk is driven by the patterns rather than by the values
12		// they range over, which is what keeps it affordable: a column is
13		// only ever split by the constructors some row actually names, so
14		// the width of the search follows the arms that were written, not
15		// the size of the type. Enumerating the product of the columns
16		// would instead cost the product of the domains, and an enum with
17		// a few hundred members in three columns would price the check
18		// out of a pass that runs on every keystroke.
19		class CASE_USEFULNESS is
20		// Spent one per visited node. A `case` whose arms interact
21		// badly enough to exhaust it is answered as though a value
22		// escapes: the author is asked for an `else` that may not be
23		// needed, rather than being told a gap is covered when the
24		// walk never finished proving it.
25		_budget: int
26
27		_BUDGET_PER_QUERY: int static => 20000
28
29		init() is
30		super.init()
31		si
32
33		// Up to `limit` witnesses that `query` admits and no row of
34		// `matrix` matches. Empty when `query` adds nothing.
35		find_witnesses(
36		matrix: Collections.List[Collections.List[CASE_PATTERN]],
37		domains: Collections.List[PATTERN_DOMAIN?],
38		query: Collections.List[CASE_PATTERN],
39		limit: int
40		) -> Collections.List[Collections.List[CASE_PATTERN]] is
41		_budget = _BUDGET_PER_QUERY
42
43		return _witnesses(matrix, domains, query, limit)
44		si
45
46		_witnesses(
47		matrix: Collections.List[Collections.List[CASE_PATTERN]],
48		domains: Collections.List[PATTERN_DOMAIN?],
49		query: Collections.List[CASE_PATTERN],
50		limit: int
51		) -> Collections.List[Collections.List[CASE_PATTERN]] is
52		let result = Collections.LIST[Collections.List[CASE_PATTERN]]()
53
54		if limit <= 0 then
55		return result
56		fi
57
58		_budget = _budget - 1
59
60		if _budget <= 0 then
61		result.add(CASE_PATTERN_BUILDER.wildcards(query.count))
62
63		return result
64		fi
65
66		if query.count == 0 then
67		// Nothing left to distinguish values by, so a value
68		// escapes exactly when no row survived to match it.
69		if matrix.count == 0 then
70		result.add(Collections.LIST[CASE_PATTERN]())
71		fi
72
73		return result
74		fi
75
76		let head = query[0]
77
78		if let constructor = head.constructor then
79		_collect_specialized(matrix, domains, query, constructor, head.fields, limit, result)
80
81		return result
82		fi
83
84		let domain = domains[0]
85		let present = _constructors_in_first_column(matrix)
86		let is_complete = domain? /\ _is_complete(domain, present)
87
88		// A value escapes in one of two ways, and both are
89		// reported so that fixing the ones named does not just
90		// reveal the rest one recompile at a time.
91		//
92		// It can take an alternative no row names at all — only
93		// possible while the column is short of its domain — in
94		// which case only a row headed by a wildcard can still
95		// match it.
96		if !is_complete then
97		let tail_witnesses =
98		_witnesses(_default_matrix(matrix), _tail_domains(domains), _tail_patterns(query), limit)
99
100		if tail_witnesses.count > 0 then
101		let missing = _missing(domain, present)
102
103		if missing.count == 0 then
104		for tail in tail_witnesses do
105		result.add(_prepend(CASE_PATTERN(), tail))
106
107		if result.count >= limit then
108		return result
109		fi
110		od
111		else
112		for m in missing do
113		for tail in tail_witnesses do
114		result.add(
115		_prepend(
116		CASE_PATTERN(m, CASE_PATTERN_BUILDER.wildcards(m.arity)),
117		tail
118		)
119		)
120
121		if result.count >= limit then
122		return result
123		fi
124		od
125		od
126		fi
127		fi
128		fi
129
130		// Or it can take an alternative some row does name, and
131		// escape underneath it on one of that alternative's own
132		// fields.
133		for c in _covered_constructors(domain, present, is_complete) do
134		_collect_specialized(
135		matrix,
136		domains,
137		query,
138		c,
139		CASE_PATTERN_BUILDER.wildcards(c.arity),
140		limit - result.count,
141		result
142		)
143
144		if result.count >= limit then
145		return result
146		fi
147		od
148
149		return result
150		si
151
152		// The alternatives worth descending under. A complete column
153		// is walked in the domain's own order, which is the order a
154		// diagnostic reads best in; an incomplete one is walked over
155		// just the alternatives some row named, since the rest are
156		// reported whole rather than descended into.
157		_covered_constructors(
158		domain: PATTERN_DOMAIN?,
159		present: Collections.List[PATTERN_CONSTRUCTOR],
160		is_complete: bool
161		) -> Collections.List[PATTERN_CONSTRUCTOR] static is
162		if is_complete /\ domain? then
163		return domain.constructors
164		fi
165
166		return present
167		si
168
169		// Recurse under `constructor`, then fold the sub-witnesses
170		// back up into it.
171		_collect_specialized(
172		matrix: Collections.List[Collections.List[CASE_PATTERN]],
173		domains: Collections.List[PATTERN_DOMAIN?],
174		query: Collections.List[CASE_PATTERN],
175		constructor: PATTERN_CONSTRUCTOR,
176		head_fields: Collections.List[CASE_PATTERN],
177		limit: int,
178		into: Collections.LIST[Collections.List[CASE_PATTERN]]
179		) is
180		if limit <= 0 then
181		return
182		fi
183
184		let arity = constructor.arity
185
186		if head_fields.count != arity then
187		return
188		fi
189
190		let sub_domains = _concat_domains(constructor.field_domains, _tail_domains(domains))
191		let sub_query = _concat_patterns(head_fields, _tail_patterns(query))
192
193		let witnesses = _witnesses(_specialize(matrix, constructor, arity), sub_domains, sub_query, limit)
194
195		for witness in witnesses do
196		let fields = Collections.LIST[CASE_PATTERN]()
197
198		for i in 0..arity do
199		fields.add(witness[i])
200		od
201
202		let rest = Collections.LIST[CASE_PATTERN]()
203
204		for i in arity..witness.count do
205		rest.add(witness[i])
206		od
207
208		into.add(_prepend(CASE_PATTERN(constructor, fields), rest))
209		od
210		si
211
212		// The rows that can still match once the first column is
213		// known to hold `constructor`, with that column replaced by
214		// the constructor's fields.
215		_specialize(
216		matrix: Collections.List[Collections.List[CASE_PATTERN]],
217		constructor: PATTERN_CONSTRUCTOR,
218		arity: int
219		) -> Collections.List[Collections.List[CASE_PATTERN]] static is
220		let result = Collections.LIST[Collections.List[CASE_PATTERN]]()
221
222		for row in matrix do
223		let head = row[0]
224
225		if head.is_wildcard then
226		result.add(_concat_patterns(CASE_PATTERN_BUILDER.wildcards(arity), _tail_patterns(row)))
227		elif head.constructor! == constructor then
228		if head.fields.count == arity then
229		result.add(_concat_patterns(head.fields, _tail_patterns(row)))
230		fi
231		fi
232		od
233
234		return result
235		si
236
237		// The rows that can still match once the first column is
238		// known to hold none of the constructors any row names.
239		_default_matrix(
240		matrix: Collections.List[Collections.List[CASE_PATTERN]]
241		) -> Collections.List[Collections.List[CASE_PATTERN]] static is
242		let result = Collections.LIST[Collections.List[CASE_PATTERN]]()
243
244		for row in matrix do
245		if row[0].is_wildcard then
246		result.add(_tail_patterns(row))
247		fi
248		od
249
250		return result
251		si
252
253		_constructors_in_first_column(
254		matrix: Collections.List[Collections.List[CASE_PATTERN]]
255		) -> Collections.List[PATTERN_CONSTRUCTOR] static is
256		let result = Collections.LIST[PATTERN_CONSTRUCTOR]()
257
258		for row in matrix do
259		if let constructor = row[0].constructor then
260		if !_contains(result, constructor) then
261		result.add(constructor)
262		fi
263		fi
264		od
265
266		return result
267		si
268
269		_is_complete(
270		domain: PATTERN_DOMAIN,
271		present: Collections.List[PATTERN_CONSTRUCTOR]
272		) -> bool static is
273		for c in domain.constructors do
274		if !_contains(present, c) then
275		return false
276		fi
277		od
278
279		return true
280		si
281
282		_missing(
283		domain: PATTERN_DOMAIN?,
284		present: Collections.List[PATTERN_CONSTRUCTOR]
285		) -> Collections.List[PATTERN_CONSTRUCTOR] static is
286		let result = Collections.LIST[PATTERN_CONSTRUCTOR]()
287
288		if !domain? then
289		return result
290		fi
291
292		for c in domain.constructors do
293		if !_contains(present, c) then
294		result.add(c)
295		fi
296		od
297
298		return result
299		si
300
301		_contains(
302		constructors: Collections.List[PATTERN_CONSTRUCTOR],
303		constructor: PATTERN_CONSTRUCTOR
304		) -> bool static is
305		for c in constructors do
306		if c == constructor then
307		return true
308		fi
309		od
310
311		return false
312		si
313
314		_prepend(
315		head: CASE_PATTERN,
316		tail: Collections.List[CASE_PATTERN]
317		) -> Collections.List[CASE_PATTERN] static is
318		let result = Collections.LIST[CASE_PATTERN]()
319
320		result.add(head)
321
322		for p in tail do
323		result.add(p)
324		od
325
326		return result
327		si
328
329		_tail_patterns(patterns: Collections.List[CASE_PATTERN]) -> Collections.List[CASE_PATTERN] static is
330		let result = Collections.LIST[CASE_PATTERN]()
331
332		for i in 1..patterns.count do
333		result.add(patterns[i])
334		od
335
336		return result
337		si
338
339		_tail_domains(domains: Collections.List[PATTERN_DOMAIN?]) -> Collections.List[PATTERN_DOMAIN?] static is
340		let result = Collections.LIST[PATTERN_DOMAIN?]()
341
342		for i in 1..domains.count do
343		result.add(domains[i])
344		od
345
346		return result
347		si
348
349		_concat_patterns(
350		first: Collections.List[CASE_PATTERN],
351		second: Collections.List[CASE_PATTERN]
352		) -> Collections.List[CASE_PATTERN] static is
353		let result = Collections.LIST[CASE_PATTERN]()
354
355		for p in first do
356		result.add(p)
357		od
358
359		for p in second do
360		result.add(p)
361		od
362
363		return result
364		si
365
366		_concat_domains(
367		first: Collections.List[PATTERN_DOMAIN?],
368		second: Collections.List[PATTERN_DOMAIN?]
369		) -> Collections.List[PATTERN_DOMAIN?] static is
370		let result = Collections.LIST[PATTERN_DOMAIN?]()
371
372		for d in first do
373		result.add(d)
374		od
375
376		for d in second do
377		result.add(d)
378		od
379
380		return result
381		si
382		si
383		si