Skip to content
← Back

src/syntax/process/condition_analysis.ghul

1
namespace Syntax.Process is
2
use Logging.Logger;
3
use Source.LOCATION;
4
use Semantic.Types.Type;
5
6
// The then/else narrowing environments a boolean condition
7
// implies: `then_env` holds while the condition is true,
8
// `else_env` while it is false.
9
class CONDITION_FACTS is
10
then_env: NARROW_ENV public;
11
else_env: NARROW_ENV public;
12
13
init(then_env: NARROW_ENV, else_env: NARROW_ENV) is
14
self.then_env = then_env;
15
self.else_env = else_env;
16
si
17
si
18
19
// Pure analysis of a *walked* boolean condition AST: given the
20
// environment in force before the condition, produce the
21
// environments in force along its true and false edges.
22
//
23
// `isa T(x)` leaves contribute a type narrow on their target; an
24
// `x?` (has-value) leaf contributes a presence fact (`x` known to
25
// hold a value on the true edge); `/\` `\/` `!` compose the
26
// leaves; anything else is opaque (no narrowing either way).
27
// Narrowing targets are resolved through the `resolve_target`
28
// delegate supplied at construction — in the compiler it is the
29
// visitor's scope-aware lookup; in tests it is a stub.
30
class CONDITION_ANALYZER is
31
_resolve_target: (Trees.Expressions.Expression) -> Semantic.Symbols.Symbol?;
32
_resolve_path: (Trees.Expressions.Expression) -> ACCESS_PATH?;
33
34
// Editor-only sink for narrowing-site hints. When set,
35
// each narrowing introduction (`x?`, `isa T(x)`, `if let ...`,
36
// etc.) is announced through the logger carrying its per-site
37
// slug so the editor can render — and independently suppress —
38
// each kind. Null in the pure-analysis tests, which exercise
39
// the environments directly and don't need the diagnostics.
40
// Only `want_hint_for` and `hint` are consulted.
41
_logger: Logger?;
42
43
// Depth counter for facts-only recursion. `pre_binary` in
44
// compile_operators pre-analyses the left of `/\` / `\/` to
45
// thread the right's narrowing environment; the enclosing
46
// condition context (if / while / assert) then analyses the
47
// whole condition. Without suppression the same narrowing
48
// site emits an inlay on each pass. Non-zero while a caller
49
// is inside `analyze_condition_facts_only`.
50
_silent_depth: int;
51
52
init(
53
resolve_target: (Trees.Expressions.Expression) -> Semantic.Symbols.Symbol?,
54
resolve_path: (Trees.Expressions.Expression) -> ACCESS_PATH?
55
) is
56
_resolve_target = resolve_target;
57
_resolve_path = resolve_path;
58
si
59
60
init(
61
resolve_target: (Trees.Expressions.Expression) -> Semantic.Symbols.Symbol?,
62
resolve_path: (Trees.Expressions.Expression) -> ACCESS_PATH?,
63
logger: Logger
64
) is
65
_resolve_target = resolve_target;
66
_resolve_path = resolve_path;
67
_logger = logger;
68
si
69
70
// Record a narrowing-introduction inlay. Editor-only: gated on
71
// analysis mode and the client's open-files set so a narrowing in
72
// a file the user is not viewing costs nothing. `label` is the
73
// terse ghost text (a single-glyph direction sigil); `detail`
74
// carries only the narrowed-to type. NARROWING_INLAY_MERGER
75
// assembles the hover sentence at read-out, folding a true/false
76
// edge pair (`narrowing-<kind>` + `narrowing-<kind>-complement`)
77
// at one location into a single hint.
78
_inlay(location: LOCATION, code: string, label: string, detail: string) is
79
let logger = _logger;
80
81
if _silent_depth > 0 \/ !logger? \/ !logger.want_hint_for(location) then
82
return;
83
fi
84
85
logger.inlay(location, code, label, detail);
86
si
87
88
// Compute a condition's true/false narrowing envs WITHOUT
89
// emitting narrowing-introduction inlays for sites walked. Used
90
// by compile_operators.pre_binary to thread the right operand's
91
// env; the enclosing if / while / assert then calls
92
// `analyze_condition` on the whole condition, which is the one
93
// walk that emits.
94
analyze_condition_facts_only(
95
cond: Trees.Expressions.Expression,
96
in_env: NARROW_ENV
97
) -> CONDITION_FACTS is
98
_silent_depth = _silent_depth + 1;
99
try
100
return analyze_condition(cond, in_env);
101
finally
102
_silent_depth = _silent_depth - 1;
103
yrt
104
si
105
106
// True iff a presence-fact hint for `target` would carry
107
// information — i.e. `target`'s current observed type is
108
// still optional. When it isn't, `target` is already known
109
// to hold a value and the hint would only be noise. Safe
110
// for the presence hints (`x?` / `x != null`) because their
111
// fact is a set-add, not a compose-against-existing.
112
_presence_hint_would_add(target: Semantic.Symbols.Symbol) -> bool =>
113
let t = target.type in t? /\ t.is_optional;
114
115
// Drill `type` to the underlying Classy (peeling Symbols.GENERIC
116
// wrapping for specialized generics, and peeling INTERSECTION
117
// for stacked-narrow types like `Declared & Variant[T]`). Null
118
// if `type` isn't a NAMED of a Classy.
119
get_classy_for_narrowing(type: Type?) -> Semantic.Symbols.Classy? is
120
if !type? then
121
return null;
122
fi
123
124
if isa Semantic.Types.INTERSECTION(type) then
125
for m in type.members do
126
let inner = get_classy_for_narrowing(m);
127
if inner? then
128
return inner;
129
fi
130
od
131
return null;
132
fi
133
134
if !isa Semantic.Types.NAMED(type) then
135
return null;
136
fi
137
138
// A bounded type variable narrows through its bound: `T`
139
// constrained to a union resolves variants of that union.
140
if type.is_type_variable then
141
return get_classy_for_narrowing(type.bound_type);
142
fi
143
144
let symbol mut = type.symbol;
145
146
if isa Semantic.Symbols.GENERIC(symbol) then
147
symbol = symbol.symbol;
148
fi
149
150
if !isa Semantic.Symbols.Classy(symbol) then
151
return null;
152
fi
153
154
return symbol;
155
si
156
157
// Pick the type that carries the receiver's generic args for
158
// variant-type construction. ONE_OF holds its original union
159
// NAMED/GENERIC as `underlying_type`; INTERSECTION returns the
160
// first member that yields a usable underlying (a NAMED whose
161
// symbol is a union or variant); any other NAMED can be used
162
// directly.
163
pick_underlying_type(receiver_type: Type?) -> Semantic.Types.NAMED? is
164
if !receiver_type? then
165
return null;
166
fi
167
168
if isa Semantic.Types.ONE_OF(receiver_type) then
169
return receiver_type.underlying_type;
170
fi
171
172
if isa Semantic.Types.INTERSECTION(receiver_type) then
173
for m in receiver_type.members do
174
let inner = pick_underlying_type(m);
175
if inner? /\ get_classy_for_narrowing(inner)? then
176
return inner;
177
fi
178
od
179
return null;
180
fi
181
182
if isa Semantic.Types.NAMED(receiver_type) then
183
// A bounded type variable carries the variant's generic
184
// args through its bound (`T: List[E]` supplies `E`).
185
if receiver_type.is_type_variable then
186
return pick_underlying_type(receiver_type.bound_type);
187
fi
188
189
return receiver_type;
190
fi
191
192
return null;
193
si
194
195
// If `target_type` names a variant of `receiver_type`'s
196
// union, return the variant specialized with the receiver's
197
// generic args; otherwise return `target_type` unchanged.
198
// Lets `isa V(x)` / `cast V(x)` resolve a bare variant of a
199
// generic union (`isa CONS(l)` for `l: List[int]`) to its
200
// closed-generic form so IL emission references a loadable
201
// type — the open generic class itself isn't a valid
202
// operand for `isinst` / `castclass`.
203
specialize_variant_for_receiver(receiver_type: Type?, target_type: Type?) -> Type? is
204
if !target_type? \/ !receiver_type? then
205
return target_type;
206
fi
207
208
let classy = get_classy_for_narrowing(target_type);
209
210
if !classy? \/ !classy.is_variant then
211
return target_type;
212
fi
213
214
return
215
let specialized = try_get_variant_type_for_classy(receiver_type, classy) in
216
if specialized? then specialized else target_type fi;
217
si
218
219
// For an `isa V(x)` check where `V` is a variant of the
220
// receiver's union, return the variant type with the same
221
// generic args as the receiver. Null when not applicable.
222
// Receiver shapes covered: the wide union, a ONE_OF over it,
223
// or an already-narrowed singleton variant of it. Variants
224
// share their generic parameters with the union, so a
225
// variant-NAMED receiver carries the same arg list and the
226
// singleton-build below picks them up unchanged.
227
try_get_variant_type_for_classy(
228
receiver_type: Type,
229
variant: Semantic.Symbols.Classy
230
) -> Type? is
231
if !variant.is_variant then
232
return null;
233
fi
234
235
let receiver_classy = get_classy_for_narrowing(receiver_type);
236
237
if !receiver_classy? then
238
return null;
239
fi
240
241
// Resolve the receiver's union — directly when the
242
// receiver is the union, or the variant's owner when the
243
// receiver is itself a variant of one.
244
let union_classy: Semantic.Symbols.Classy? mut = null;
245
246
if receiver_classy.is_union then
247
union_classy = receiver_classy;
248
elif receiver_classy.is_variant then
249
if let owner: Semantic.Symbols.Classy = receiver_classy.owner then
250
union_classy = owner;
251
fi
252
fi
253
254
if !union_classy? \/ !union_classy.is_union then
255
return null;
256
fi
257
258
// Verify `variant` actually belongs to that union.
259
let is_member mut = false;
260
for s in union_classy.symbols do
261
if s == variant then
262
is_member = true;
263
fi
264
od
265
266
if !is_member then
267
return null;
268
fi
269
270
// No in-set check here: IL emission needs the
271
// specialized variant type even when the runtime test is
272
// statically false, because a bare open-generic variant
273
// class is not loadable by the CLR. Narrowing-soundness
274
// checks (e.g. ONE_OF.contains_subtype) belong at the
275
// call site that consumes this as a narrow target.
276
let underlying = pick_underlying_type(receiver_type);
277
278
if !underlying? then
279
return null;
280
fi
281
282
return Semantic.Types.ONE_OF.build_singleton_subtype(underlying, variant);
283
si
284
285
// Build the complement narrowing — the in-set members of
286
// `receiver_type` that don't appear in `eliminated`. When
287
// `receiver_type` is itself a ONE_OF the in-set is its
288
// narrowed members, not the full root; otherwise it is
289
// every alternative of the closed root (variants of a
290
// union, direct subclasses of a closed class). Returns a
291
// singleton type, a ONE_OF, or null when the chain exhausts
292
// the in-set or the receiver isn't a closed root.
293
try_get_complement_after_eliminated(
294
receiver_type: Type,
295
eliminated: Collections.Iterable[Semantic.Symbols.Classy]
296
) -> Type? is
297
// The complement of an optional receiver is optional:
298
// the eliminating test also fails for null, so the
299
// complement edge keeps the null case. Compute over the
300
// stripped type and re-flag the result. Callers that can
301
// prove the value present strip the flag back off.
302
let is_receiver_optional = receiver_type.is_optional;
303
let receiver = receiver_type.as_non_optional();
304
305
let classy = get_classy_for_narrowing(receiver);
306
307
if !classy? \/ !classy.is_closed_root then
308
return null;
309
fi
310
311
// Closed classes with generic receivers need extra
312
// specialisation work — subclasses don't always share
313
// the base's type parameter list. Variants share their
314
// owner union's argument_names slot-for-slot by language
315
// design, so unions don't hit this constraint.
316
if classy.is_class /\ isa Semantic.Types.GENERIC(receiver) then
317
return null;
318
fi
319
320
// The universe is the closed root's in-set, optionally
321
// including the root itself. For unions the root never
322
// appears at runtime (only its variants do). For closed
323
// classes the root joins the universe when concrete —
324
// otherwise a caller could construct a bare root
325
// instance and the singleton-collapse narrow would
326
// produce an unsound method resolution.
327
let universe = Collections.LIST[Semantic.Symbols.Classy]();
328
329
if classy.is_class /\ !classy.is_abstract then
330
universe.add(classy);
331
fi
332
333
for s in classy.closed_alternatives do
334
universe.add(s);
335
od
336
337
let one_of = cast Semantic.Types.ONE_OF?(receiver);
338
339
let complement = Collections.LIST[Semantic.Symbols.Classy]();
340
341
for member in universe do
342
if one_of? /\ !one_of.contains_subtype(member) then
343
continue;
344
fi
345
346
let is_eliminated mut = false;
347
348
for e in eliminated do
349
if e == member then
350
is_eliminated = true;
351
fi
352
od
353
354
if !is_eliminated then
355
complement.add(member);
356
fi
357
od
358
359
let underlying = pick_underlying_type(receiver);
360
361
if !underlying? then
362
return null;
363
fi
364
365
let result = Semantic.Types.ONE_OF.create(underlying, complement);
366
367
if result? /\ is_receiver_optional then
368
return result.as_optional();
369
fi
370
371
return result;
372
si
373
374
// Narrow target for `isa C(x)` where C is a direct subclass
375
// of `x`'s closed root class. Null when not applicable —
376
// receiver is open / imported / not the right root, target
377
// isn't a direct subclass, or the receiver is generic (the
378
// generic case needs a parameter-flow rule we don't have
379
// yet).
380
try_get_closed_subclass_narrow_type(
381
receiver_type: Type,
382
target_classy: Semantic.Symbols.Classy
383
) -> Type? is
384
if !target_classy.is_class then
385
return null;
386
fi
387
388
let receiver_classy = get_classy_for_narrowing(receiver_type);
389
390
if !receiver_classy? \/ receiver_classy.is_open then
391
return null;
392
fi
393
394
if !receiver_classy.is_class then
395
return null;
396
fi
397
398
if isa Semantic.Types.GENERIC(receiver_type) then
399
return null;
400
fi
401
402
// Verify target_classy is in receiver's closed in-set:
403
// walking the ONE_OF when one is in play, otherwise the
404
// root's direct subclasses.
405
let one_of: Semantic.Types.ONE_OF? mut = null;
406
if isa Semantic.Types.ONE_OF(receiver_type) then
407
one_of = receiver_type;
408
fi
409
410
if one_of? then
411
if !one_of.contains_subtype(target_classy) then
412
return null;
413
fi
414
else
415
let is_member mut = false;
416
for s in receiver_classy.closed_subclasses do
417
if s == target_classy then
418
is_member = true;
419
fi
420
od
421
422
if !is_member then
423
return null;
424
fi
425
fi
426
427
return Semantic.Types.NAMED(target_classy);
428
si
429
430
// Analyze a walked boolean condition into its true/false
431
// narrowing environments. Always returns fresh (copied)
432
// environments — callers may mutate them freely.
433
analyze_condition(cond: Trees.Expressions.Expression?, in_env: NARROW_ENV) -> CONDITION_FACTS is
434
if !cond? then
435
return _opaque(cond, in_env);
436
fi
437
438
if isa Trees.Expressions.BINARY(cond) then
439
let binary = cond;
440
441
let op = binary.operation.name;
442
443
if op =~ "/\\" then
444
let l = analyze_condition(binary.left, in_env);
445
let r = analyze_condition(binary.right, l.then_env);
446
447
return CONDITION_FACTS(
448
r.then_env,
449
NARROW_ENV.join(l.else_env, r.else_env)
450
);
451
elif op =~ "\\/" then
452
let l = analyze_condition(binary.left, in_env);
453
let r = analyze_condition(binary.right, l.else_env);
454
455
return CONDITION_FACTS(
456
NARROW_ENV.join(l.then_env, r.then_env),
457
r.else_env
458
);
459
elif op =~ "==" then
460
return _analyze_null_compare(binary, in_env);
461
fi
462
elif isa Trees.Expressions.UNARY(cond) then
463
let unary = cond;
464
465
if unary.operation.name =~ "!" then
466
let inner = analyze_condition(unary.right, in_env);
467
468
// `!` swaps the true and false edges.
469
return CONDITION_FACTS(inner.else_env, inner.then_env);
470
fi
471
elif isa Trees.Expressions.ISA(cond) then
472
return _analyze_isa(cond, in_env);
473
elif isa Trees.Expressions.HAS_VALUE(cond) then
474
return _analyze_has_value(cond, in_env);
475
fi
476
477
return _opaque(cond, in_env);
478
si
479
480
// A condition that discriminates no variable's type — both
481
// edges keep the incoming environment. A `ref` argument the
482
// condition evaluates writes its target, so it counts as a
483
// definite assignment on both edges; short-circuit joins above
484
// then confine that fact to the edges the write actually reached.
485
_opaque(cond: Trees.Expressions.Expression?, in_env: NARROW_ENV) -> CONDITION_FACTS is
486
let then_env = in_env.copy();
487
let else_env = in_env.copy();
488
489
_mark_ref_assignments(cond, then_env, else_env);
490
491
return CONDITION_FACTS(then_env, else_env);
492
si
493
494
// Operators whose right operand is evaluated only for some
495
// values of the left: `/\`, `\/` and the `??` null-coalesce.
496
_is_short_circuit(operation: string) -> bool =>
497
operation =~ "/\\" \/ operation =~ "\\/" \/ operation =~ "??";
498
499
// Mark every variable the expression writes through a `ref`
500
// argument as assigned on both edges. Recurses only through
501
// unconditionally-evaluated positions: a `ref` behind a
502
// short-circuit operand or a lambda body is not guaranteed to
503
// run, so it is left for its own evaluation to record.
504
_mark_ref_assignments(expr: Trees.Expressions.Expression?, then_env: NARROW_ENV, else_env: NARROW_ENV) is
505
if !expr? then
506
return;
507
fi
508
509
if isa Trees.Expressions.REFERENCE(expr) then
510
let reference = expr;
511
512
// Only a slot the callee writes assigns its target; the
513
// resolved call recorded that on the REFERENCE.
514
if reference.writes_target then
515
let target = _resolve_target(reference.left);
516
517
if target? then
518
then_env.set_assigned(target);
519
else_env.set_assigned(target);
520
fi
521
fi
522
elif isa Trees.Expressions.CALL(expr) then
523
let call = expr;
524
525
_mark_ref_assignments(call.function, then_env, else_env);
526
527
for argument in call.arguments.expressions do
528
_mark_ref_assignments(argument, then_env, else_env);
529
od
530
elif isa Trees.Expressions.MEMBER(expr) then
531
_mark_ref_assignments(expr.left, then_env, else_env);
532
elif isa Trees.Expressions.INDEX(expr) then
533
let index = expr;
534
535
_mark_ref_assignments(index.left, then_env, else_env);
536
_mark_ref_assignments(index.index, then_env, else_env);
537
elif isa Trees.Expressions.UNARY(expr) then
538
_mark_ref_assignments(expr.right, then_env, else_env);
539
elif isa Trees.Expressions.CAST(expr) then
540
_mark_ref_assignments(expr.right, then_env, else_env);
541
elif isa Trees.Expressions.HAS_VALUE(expr) then
542
_mark_ref_assignments(expr.left, then_env, else_env);
543
elif isa Trees.Expressions.UNWRAP(expr) then
544
_mark_ref_assignments(expr.left, then_env, else_env);
545
elif isa Trees.Expressions.BINARY(expr) then
546
let binary = expr;
547
548
_mark_ref_assignments(binary.left, then_env, else_env);
549
550
// The right operand of a short-circuiting operator only
551
// runs for some left values, so a `ref` there is not a
552
// definite write; the left operand always runs.
553
if !_is_short_circuit(binary.operation.name) then
554
_mark_ref_assignments(binary.right, then_env, else_env);
555
fi
556
fi
557
si
558
559
// `x != null` / `x == null` — the comparison narrows the
560
// non-null operand. `!=` puts it on the true edge, `==` on the
561
// false edge. The `==` real operation covers both surface
562
// forms; `actual_operation` distinguishes them.
563
_analyze_null_compare(binary: Trees.Expressions.BINARY, in_env: NARROW_ENV) -> CONDITION_FACTS is
564
let then_env = in_env.copy();
565
let else_env = in_env.copy();
566
567
let operand: Trees.Expressions.Expression? mut = null;
568
569
if isa Trees.Expressions.NULL(binary.right) then
570
operand = binary.left;
571
elif isa Trees.Expressions.NULL(binary.left) then
572
operand = binary.right;
573
fi
574
575
if operand? then
576
let target = _resolve_target(operand);
577
let is_not_equal = binary.actual_operation =~ "!=";
578
579
if target? then
580
if is_not_equal then
581
then_env.set_non_null(target);
582
else
583
else_env.set_non_null(target);
584
fi
585
586
if _presence_hint_would_add(target) then
587
_inlay(
588
operand.location,
589
"narrowing-null-compare",
590
"►",
591
INLAY_TYPE.render(target.type!.as_non_optional())
592
);
593
fi
594
else
595
let path = _resolve_path(operand);
596
597
if path? then
598
if is_not_equal then
599
then_env.set_non_null_path(path);
600
else
601
else_env.set_non_null_path(path);
602
fi
603
604
let path_type = operand.value?.type;
605
606
_inlay(
607
operand.location,
608
"narrowing-null-compare",
609
"►",
610
if path_type? then INLAY_TYPE.render(path_type.as_non_optional()) else "" fi
611
);
612
fi
613
fi
614
fi
615
616
return CONDITION_FACTS(then_env, else_env);
617
si
618
619
// Apply the cast target as a then-edge narrow on the if-let
620
// scrutinee — mirrors `_analyze_isa`'s then-edge logic so
621
// `if let p: V = e` and `isa V(e)` produce the same flow
622
// facts (and therefore the same downstream inference shape).
623
//
624
// The scrutinee is walked AFTER this hook runs, so the load
625
// picks up the narrowed symbol type. The narrow target is
626
// specialised against the scrutinee's symbol type (via
627
// `_resolve_target`), so a bare variant target becomes its
628
// receiver-specialised form (e.g. `CONS[int]` not `CONS`)
629
// when the receiver type is already known — otherwise it is
630
// left as the unspecialised written form, and a later body-
631
// retry iteration with a settled receiver gets a chance to
632
// re-narrow tighter.
633
apply_refutable_binding_then_narrow(
634
scrutinee: Trees.Expressions.Expression?,
635
narrow_type: Type?,
636
in_env: NARROW_ENV
637
) -> NARROW_ENV is
638
if !scrutinee? \/ !narrow_type? then
639
return in_env;
640
fi
641
642
if narrow_type.is_error \/ narrow_type.is_inferred then
643
return in_env;
644
fi
645
646
let target = _resolve_target(scrutinee);
647
let target_path: ACCESS_PATH? mut =
648
if !target? then _resolve_path(scrutinee) else null fi;
649
650
if !target? /\ !target_path? then
651
return in_env;
652
fi
653
654
// Specialise the narrow target against the scrutinee's
655
// current symbol type so a variant target narrows to its
656
// closed-generic form (e.g. `CONS[int]` for an
657
// `l: List[int]` receiver). For a path scrutinee we take
658
// the value's static type from the walked expression.
659
let receiver: Type? mut = null;
660
661
if target? /\ target.type? then
662
receiver = target.type;
663
664
if isa Semantic.Types.INFERRED_VARIABLE_TYPE(receiver) then
665
let placeholder = cast Semantic.Types.INFERRED_VARIABLE_TYPE(receiver);
666
let resolved = placeholder.origin.try_get_inferred_type();
667
668
if resolved? /\ !resolved.is_sentinel then
669
receiver = resolved;
670
fi
671
fi
672
elif !target? /\ scrutinee.value? then
673
receiver = scrutinee.value.type;
674
fi
675
676
let specialized_narrow: Type mut = narrow_type;
677
678
if receiver? then
679
let specialized =
680
specialize_variant_for_receiver(receiver, narrow_type);
681
682
if specialized? then
683
specialized_narrow = specialized;
684
fi
685
fi
686
687
let result = in_env.copy();
688
689
if target? then
690
result.set_non_null(target);
691
result.set_narrow(target, specialized_narrow);
692
693
_inlay(
694
scrutinee.location,
695
"narrowing-if-let",
696
"►",
697
INLAY_TYPE.render(specialized_narrow)
698
);
699
else
700
result.set_non_null_path(target_path!);
701
result.set_path_narrow(target_path, specialized_narrow);
702
703
_inlay(
704
scrutinee.location,
705
"narrowing-if-let",
706
"►",
707
INLAY_TYPE.render(specialized_narrow)
708
);
709
fi
710
711
return result;
712
si
713
714
// Apply variant-complement narrowing to the else edge of a
715
// REFUTABLE_BINDING. Mirrors the variant branch of
716
// `_analyze_isa`'s else narrowing.
717
//
718
// The receiver type is passed in because by the time this
719
// runs the scrutinee's symbol type may have been mutated by
720
// the then-edge narrowing to the cast target (the variant
721
// itself, not the union we want to compute the complement
722
// over). The caller captures the receiver before applying
723
// the then-narrow.
724
//
725
// Multi-clause bindings suppress complement narrowing
726
// entirely: the else edge can be reached because clause 0's
727
// test passed but clause N's failed, in which case clause 0's
728
// scrutinee genuinely *is* its narrow target (not the
729
// complement). Same soundness reasoning as the guarded
730
// single-clause case below.
731
apply_refutable_binding_else_narrow(
732
rb: Trees.Statements.REFUTABLE_BINDING,
733
receiver_type: Type?,
734
in_env: NARROW_ENV
735
) -> NARROW_ENV is
736
if !receiver_type? then
737
return in_env;
738
fi
739
740
if rb.clauses.count != 1 then
741
return in_env;
742
fi
743
744
let clause = rb.clauses[0];
745
746
let narrow_type_expression = clause.narrow_type_expression;
747
748
if !narrow_type_expression? \/ !narrow_type_expression.type? then
749
return in_env;
750
fi
751
752
// Guarded if-let: the else arm is reached on two paths —
753
// the type test rejected the scrutinee (`e` is not `V`),
754
// OR the test succeeded but the guard was false (`e` is
755
// `V`). Narrowing to the variant complement on the
756
// second path would be unsound. Mirrors how
757
// `analyze_condition` joins the `/\` else edges: `isa V(x)
758
// /\ guard` widens the `x` narrow back on else (line
759
// 272), it doesn't narrow to the complement.
760
if clause.guard? then
761
return in_env;
762
fi
763
764
let narrow_type = narrow_type_expression.type;
765
let scrutinee = clause.scrutinee;
766
767
let target = _resolve_target(scrutinee);
768
let target_path: ACCESS_PATH? mut =
769
if !target? then _resolve_path(scrutinee) else null fi;
770
771
if !target? /\ !target_path? then
772
return in_env;
773
fi
774
775
let narrow_classy = get_classy_for_narrowing(narrow_type);
776
777
if !narrow_classy? then
778
return in_env;
779
fi
780
781
// Variant-of-union and direct-subclass-of-closed-root are
782
// the two closed-domain shapes that can produce a non-empty
783
// else complement.
784
if !narrow_classy.is_variant /\ !narrow_classy.is_class then
785
return in_env;
786
fi
787
788
// Compute the complement against the target's CURRENT
789
// narrow when there is one — an earlier arm in the same
790
// if/elif chain may already have eliminated other
791
// alternatives, and the complement is "what's left minus
792
// this arm's target", not "the declared root minus this
793
// arm's target". The declared receiver is the fallback for
794
// the first arm where no narrow yet exists.
795
let effective_receiver: Type mut = receiver_type;
796
let current: Type? mut =
797
if target? then in_env.narrowed_type_of(target) else in_env.narrowed_type_of_path(target_path!) fi;
798
799
if current? then
800
effective_receiver = current;
801
fi
802
803
let one_of: Semantic.Types.ONE_OF? mut = null;
804
if isa Semantic.Types.ONE_OF(effective_receiver) then
805
one_of = effective_receiver;
806
fi
807
808
if one_of? /\ !one_of.contains_subtype(narrow_classy) then
809
return in_env;
810
fi
811
812
let eliminated = Collections.LIST[Semantic.Symbols.Classy]();
813
eliminated.add(narrow_classy);
814
815
let complement mut = try_get_complement_after_eliminated(effective_receiver, eliminated);
816
817
if !complement? then
818
return in_env;
819
fi
820
821
// The else edge is null-free when the scrutinee was
822
// already proven to hold a value before the binding.
823
let was_non_null =
824
if target? then in_env.is_non_null(target) else in_env.is_non_null_path(target_path!) fi;
825
826
if complement.is_optional /\ was_non_null then
827
complement = complement.as_non_optional();
828
fi
829
830
let result = in_env.copy();
831
832
// The complement is computed against the effective receiver
833
// — the current narrow when an earlier arm already narrowed
834
// the target — so it is the absolute narrowed type for the
835
// else edge and must replace any prior narrow rather than
836
// compose with it.
837
if target? then
838
result.replace_narrow(target, complement);
839
840
_inlay(
841
scrutinee.location,
842
"narrowing-if-let-complement",
843
"►",
844
INLAY_TYPE.render(complement)
845
);
846
else
847
result.replace_path_narrow(target_path!, complement);
848
849
_inlay(
850
scrutinee.location,
851
"narrowing-if-let-complement",
852
"►",
853
INLAY_TYPE.render(complement)
854
);
855
fi
856
857
return result;
858
si
859
860
861
_analyze_isa(`isa: Trees.Expressions.ISA, in_env: NARROW_ENV) -> CONDITION_FACTS is
862
let then_env = in_env.copy();
863
let else_env = in_env.copy();
864
865
let target = _resolve_target(`isa.right);
866
let target_path: ACCESS_PATH? mut =
867
if !target? then _resolve_path(`isa.right) else null fi;
868
let isa_type = `isa.type_expression.type;
869
870
if target? \/ target_path? then
871
// `isa T(x)` is true only for a non-null `x` of a
872
// matching type — so the true edge knows both. Same
873
// reasoning holds for a member-access path receiver.
874
if target? then
875
then_env.set_non_null(target);
876
else
877
then_env.set_non_null_path(target_path!);
878
fi
879
880
// When `isa V(x)` names a variant of `x`'s union, the
881
// narrow target is the variant specialized with the
882
// receiver's generic args (a bare `isa CONS(l)` for
883
// `l: List[int]` narrows to `CONS[int]`, not the
884
// unspecialized variant), and the else edge narrows
885
// to the complement. Otherwise fall back to the
886
// literal isa_type for the then edge with no else
887
// narrow, since the complement of an open class
888
// hierarchy (e.g. `Animal \ Cat`) isn't representable.
889
let receiver_type = `isa.right?.value?.type;
890
891
let isa_classy = get_classy_for_narrowing(isa_type);
892
893
let variant_narrow: Type? mut = null;
894
895
if isa_classy? /\ isa_classy.is_variant /\ receiver_type? then
896
// Only push a narrow when the variant is
897
// actually a member of the receiver's narrowed
898
// set — a statically-false `isa V(x)` shouldn't
899
// mutate the then-environment. Specialization
900
// for IL emission is handled separately at
901
// compile_expressions.visit(ISA).
902
let one_of: Semantic.Types.ONE_OF? mut = null;
903
if isa Semantic.Types.ONE_OF(receiver_type) then
904
one_of = receiver_type;
905
fi
906
907
if !one_of? \/ one_of.contains_subtype(isa_classy) then
908
variant_narrow = try_get_variant_type_for_classy(receiver_type, isa_classy);
909
fi
910
fi
911
912
let closed_subclass_narrow: Type? mut = null;
913
914
if !variant_narrow? /\ isa_classy? /\ isa_classy.is_class /\ receiver_type? then
915
closed_subclass_narrow =
916
try_get_closed_subclass_narrow_type(receiver_type, isa_classy);
917
fi
918
919
if let then_narrow =
920
if variant_narrow? then variant_narrow else closed_subclass_narrow fi
921
then
922
// isa_classy and receiver_type are non-null whenever
923
// then_narrow is — both narrow branches above
924
// require them.
925
let else_narrow: Type? mut = null;
926
927
if target? then
928
else_narrow = _set_narrow_with_complement(
929
target, receiver_type!, then_narrow, isa_classy!, then_env, else_env);
930
else
931
else_narrow = _set_path_narrow_with_complement(
932
target_path!, receiver_type!, then_narrow, isa_classy!, then_env, else_env);
933
fi
934
935
_inlay(
936
`isa.right.location,
937
"narrowing-isa",
938
"►",
939
INLAY_TYPE.render(then_narrow)
940
);
941
942
if else_narrow? then
943
_inlay(
944
`isa.right.location,
945
"narrowing-isa-complement",
946
"►",
947
INLAY_TYPE.render(else_narrow)
948
);
949
fi
950
elif isa_type? /\ !isa_type.is_error /\ !isa_type.is_inferred then
951
if target? then
952
then_env.set_narrow(target, isa_type);
953
else
954
then_env.set_path_narrow(target_path!, isa_type);
955
fi
956
957
_inlay(
958
`isa.right.location,
959
"narrowing-isa",
960
"►",
961
INLAY_TYPE.render(isa_type)
962
);
963
fi
964
fi
965
966
return CONDITION_FACTS(then_env, else_env);
967
si
968
969
// Narrow `target` to `then_narrow` on the true edge, and — when
970
// representable — to the complement of `eliminated` within the
971
// receiver's closed set on the false edge. Shared by `isa` and
972
// the default-variant `?` present-test. Returns the complement
973
// when one was applied, so the caller can announce the false
974
// edge to the editor.
975
_set_narrow_with_complement(
976
target: Semantic.Symbols.Symbol,
977
receiver_type: Type,
978
then_narrow: Type,
979
eliminated: Semantic.Symbols.Classy,
980
then_env: NARROW_ENV,
981
else_env: NARROW_ENV
982
) -> Type? is
983
then_env.set_narrow(target, then_narrow);
984
985
if let complement =
986
_else_edge_complement(receiver_type, eliminated, else_env.is_non_null(target))
987
then
988
else_env.set_narrow(target, complement);
989
return complement;
990
fi
991
992
return null;
993
si
994
995
// Path-keyed mirror of `_set_narrow_with_complement`. Same
996
// then/else shape, keyed on ACCESS_PATH.
997
_set_path_narrow_with_complement(
998
target_path: ACCESS_PATH,
999
receiver_type: Type,
1000
then_narrow: Type,
1001
eliminated: Semantic.Symbols.Classy,
1002
then_env: NARROW_ENV,
1003
else_env: NARROW_ENV
1004
) -> Type? is
1005
then_env.set_path_narrow(target_path, then_narrow);
1006
1007
if let complement =
1008
_else_edge_complement(receiver_type, eliminated, else_env.is_non_null_path(target_path))
1009
then
1010
else_env.set_path_narrow(target_path, complement);
1011
return complement;
1012
fi
1013
1014
return null;
1015
si
1016
1017
// The complement narrow for the false edge of an `isa` /
1018
// default-variant `?` test, with the null-free strip already
1019
// applied when the target was known present on the way in.
1020
// Null when the complement isn't representable.
1021
_else_edge_complement(
1022
receiver_type: Type,
1023
eliminated: Semantic.Symbols.Classy,
1024
was_non_null: bool
1025
) -> Type? is
1026
let eliminated_set = Collections.LIST[Semantic.Symbols.Classy]();
1027
eliminated_set.add(eliminated);
1028
1029
if let complement = try_get_complement_after_eliminated(receiver_type, eliminated_set) then
1030
if complement.is_optional /\ was_non_null then
1031
return complement.as_non_optional();
1032
fi
1033
1034
return complement;
1035
fi
1036
1037
return null;
1038
si
1039
1040
// `x?` on a union with a default variant compiles to
1041
// `isa Default(x)` (see compile_access.visit_has_value), so it
1042
// narrows the same way: the true edge to the default variant
1043
// specialized to the receiver, the false edge to the complement.
1044
// No-op when the default variant isn't in the receiver's
1045
// narrowed set (a statically-false `x?`).
1046
_narrow_default_variant_has_value(
1047
has_value_location: LOCATION,
1048
target: Semantic.Symbols.Symbol,
1049
receiver_type: Type,
1050
variant: Semantic.Symbols.Classy,
1051
then_env: NARROW_ENV,
1052
else_env: NARROW_ENV
1053
) is
1054
let one_of: Semantic.Types.ONE_OF? mut = null;
1055
if isa Semantic.Types.ONE_OF(receiver_type) then
1056
one_of = receiver_type;
1057
fi
1058
1059
if one_of? /\ !one_of.contains_subtype(variant) then
1060
return;
1061
fi
1062
1063
if let variant_narrow = try_get_variant_type_for_classy(receiver_type, variant) then
1064
let else_narrow = _set_narrow_with_complement(
1065
target, receiver_type, variant_narrow, variant, then_env, else_env);
1066
1067
_inlay(
1068
has_value_location,
1069
"narrowing-default-variant",
1070
"►",
1071
INLAY_TYPE.render(variant_narrow)
1072
);
1073
1074
if else_narrow? then
1075
_inlay(
1076
has_value_location,
1077
"narrowing-default-variant-complement",
1078
"►",
1079
INLAY_TYPE.render(else_narrow)
1080
);
1081
fi
1082
fi
1083
si
1084
1085
// Path-keyed mirror of `_narrow_default_variant_has_value`.
1086
_narrow_default_variant_has_value_path(
1087
has_value_location: LOCATION,
1088
target_path: ACCESS_PATH,
1089
receiver_type: Type,
1090
variant: Semantic.Symbols.Classy,
1091
then_env: NARROW_ENV,
1092
else_env: NARROW_ENV
1093
) is
1094
let one_of: Semantic.Types.ONE_OF? mut = null;
1095
if isa Semantic.Types.ONE_OF(receiver_type) then
1096
one_of = receiver_type;
1097
fi
1098
1099
if one_of? /\ !one_of.contains_subtype(variant) then
1100
return;
1101
fi
1102
1103
if let variant_narrow = try_get_variant_type_for_classy(receiver_type, variant) then
1104
let else_narrow = _set_path_narrow_with_complement(
1105
target_path, receiver_type, variant_narrow, variant, then_env, else_env);
1106
1107
_inlay(
1108
has_value_location,
1109
"narrowing-default-variant",
1110
"►",
1111
INLAY_TYPE.render(variant_narrow)
1112
);
1113
1114
if else_narrow? then
1115
_inlay(
1116
has_value_location,
1117
"narrowing-default-variant-complement",
1118
"►",
1119
INLAY_TYPE.render(else_narrow)
1120
);
1121
fi
1122
fi
1123
si
1124
1125
// `x?` — the has-value test. On the true edge `x` is known to
1126
// hold a value; for a union with a default variant both edges
1127
// narrow (see `_narrow_default_variant_has_value`). For an
1128
// optional reference or a NULLABLE[T] / MAYBE[T] value type the
1129
// false edge learns nothing (absence isn't representable).
1130
_analyze_has_value(has_value: Trees.Expressions.HAS_VALUE, in_env: NARROW_ENV) -> CONDITION_FACTS is
1131
let then_env = in_env.copy();
1132
let else_env = in_env.copy();
1133
1134
let target = _resolve_target(has_value.left);
1135
let target_path: ACCESS_PATH? mut =
1136
if !target? then _resolve_path(has_value.left) else null fi;
1137
1138
if target? then
1139
let emit_presence_hint = _presence_hint_would_add(target);
1140
1141
then_env.set_non_null(target);
1142
1143
if emit_presence_hint then
1144
_inlay(
1145
has_value.left.location,
1146
"narrowing-presence",
1147
"►",
1148
INLAY_TYPE.render(target.type!.as_non_optional())
1149
);
1150
fi
1151
1152
let receiver_type = has_value.left.value?.type;
1153
1154
if receiver_type? then
1155
let union_classy =
1156
cast Semantic.Symbols.UNION?(
1157
get_classy_for_narrowing(
1158
pick_underlying_type(receiver_type)));
1159
1160
if union_classy? then
1161
if let default_variant = union_classy.default_variant then
1162
_narrow_default_variant_has_value(
1163
has_value.left.location,
1164
target, receiver_type, default_variant, then_env, else_env);
1165
fi
1166
fi
1167
fi
1168
elif target_path? then
1169
then_env.set_non_null_path(target_path);
1170
1171
let path_type = has_value.left.value?.type;
1172
1173
_inlay(
1174
has_value.left.location,
1175
"narrowing-presence",
1176
"►",
1177
if path_type? then INLAY_TYPE.render(path_type.as_non_optional()) else "" fi
1178
);
1179
1180
let receiver_type = has_value.left.value?.type;
1181
1182
if receiver_type? then
1183
let union_classy =
1184
cast Semantic.Symbols.UNION?(
1185
get_classy_for_narrowing(
1186
pick_underlying_type(receiver_type)));
1187
1188
if union_classy? then
1189
if let default_variant = union_classy.default_variant then
1190
_narrow_default_variant_has_value_path(
1191
has_value.left.location,
1192
target_path, receiver_type, default_variant, then_env, else_env);
1193
fi
1194
fi
1195
fi
1196
fi
1197
1198
return CONDITION_FACTS(then_env, else_env);
1199
si
1200
1201
si
1202
si