Skip to content

Commit ebe5242

Browse files
committed
feat(check): not / and / or narrowing predicates
Wires `not <cond>`, `<cond> and <cond>`, `<cond> or <cond>` into interpretCondition. The Refinement.Negate method (previously dead code) becomes the implementation of `not`; the binary cases follow standard short-circuit narrowing semantics. `not c`: flip truthy and falsy. `a and b`: - WhenTrue: both truthy. Apply a's WhenTrue, then merge b's WhenTrue on top. b is computed against the a-truthy frame, so its refinement reflects what's known at that point in the short-circuit evaluation. Example: `if x != null and y != null:` narrows both x and y. - WhenFalse: at least one falsy. This is a disjunction we can't express as a single refinement map without losing info, so we leave it empty. Matches Pyright/mypy. `a or b`: mirror image of and. - WhenFalse: both falsy. Sequential apply. - WhenTrue: at least one truthy, conservatively empty. Right-operand frame matters. For `if x != null and x.field > 5:`, the right hand x.field needs x narrowed to non-null - otherwise the field-access narrowing logic would be working from the original nullable type. interpretAnd / interpretOr build the right-side frame by layering the appropriate left-side refinement before interpreting the right. mergeRefinementMaps overlays the right's narrowings on top of the left's. When both refine the same symbol, the right wins because it was computed in the tighter frame. Concretely: `if x != null and type_of(x) == "int":` - left says x is int (non- null), right (under that frame) further says x is int. Right wins since they agree; if right had refined further (e.g. x is the int arm of a union), that tighter narrowing would survive. Combined with the Negate-based not, this unlocks the De Morgan patterns too: `if not (x == null or y == null):` correctly narrows both x and y to non-null, by flipping or's WhenFalse (both non-null) into the outer WhenTrue. Five new snapshot cases cover: bare not, simple and-chain, the short-circuit "right sees left" property, or's symmetric falsy narrowing in the else branch, and the De Morgan composition.
1 parent 35d6990 commit ebe5242

1 file changed

Lines changed: 139 additions & 0 deletions

File tree

Lines changed: 139 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,139 @@
1+
### TITLE ###
2+
NotInvertsRefinement
3+
### DESCRIPTION ###
4+
`if not (x == null):` should be equivalent to `if x != null:` -
5+
truthy branch narrows x to non-null.
6+
### INPUT ###
7+
fn f(x: int?):
8+
if not (x == null):
9+
y = x
10+
### STDOUT ###
11+
# Identifier types
12+
x @ 2:13 -> int?
13+
y @ 3:9 -> <no-type>
14+
x @ 3:13 -> int
15+
16+
# Symbol types
17+
f (fn): <no-type>
18+
x (param): int?
19+
y (local): int
20+
21+
# Diagnostics
22+
(none)
23+
### TITLE ###
24+
AndChainsRefinements
25+
### DESCRIPTION ###
26+
`if x != null and y != null:` should narrow both x and y to non-null
27+
in the body. The right operand is evaluated with the left's truthy
28+
refinement active.
29+
### INPUT ###
30+
fn f(x: int?, y: str?):
31+
if x != null and y != null:
32+
a = x
33+
b = y
34+
### STDOUT ###
35+
# Identifier types
36+
x @ 2:8 -> int?
37+
y @ 2:22 -> str?
38+
a @ 3:9 -> <no-type>
39+
x @ 3:13 -> int
40+
b @ 4:9 -> <no-type>
41+
y @ 4:13 -> str
42+
43+
# Symbol types
44+
a (local): int
45+
b (local): str
46+
f (fn): <no-type>
47+
x (param): int?
48+
y (param): str?
49+
50+
# Diagnostics
51+
(none)
52+
### TITLE ###
53+
AndShortCircuitRightSeesLeftNarrowed
54+
### DESCRIPTION ###
55+
In `x != null and type_of(x) == "int"`, the right hand sees x as
56+
non-null (left's truthy refinement). With base type int?, the
57+
right operand's narrowing to int is still useful (type_of can
58+
further refine within the non-null component).
59+
### INPUT ###
60+
fn f(x: int?):
61+
if x != null and type_of(x) == "int":
62+
y = x
63+
### STDOUT ###
64+
# Identifier types
65+
x @ 2:8 -> int?
66+
type_of @ 2:22 -> dynamic
67+
x @ 2:30 -> int?
68+
y @ 3:9 -> <no-type>
69+
x @ 3:13 -> int
70+
71+
# Symbol types
72+
f (fn): <no-type>
73+
x (param): int?
74+
y (local): int
75+
76+
# Diagnostics
77+
(none)
78+
### TITLE ###
79+
OrFalsyBothFalse
80+
### DESCRIPTION ###
81+
`if x == null or y == null:` truthy = at least one is null (no
82+
refinement we can express). Falsy = both non-null - narrows both
83+
in the else.
84+
### INPUT ###
85+
fn f(x: int?, y: str?):
86+
if x == null or y == null:
87+
a = 0
88+
else:
89+
b = x
90+
c = y
91+
### STDOUT ###
92+
# Identifier types
93+
x @ 2:8 -> int?
94+
y @ 2:21 -> str?
95+
a @ 3:9 -> <no-type>
96+
b @ 5:9 -> <no-type>
97+
x @ 5:13 -> int
98+
c @ 6:9 -> <no-type>
99+
y @ 6:13 -> str
100+
101+
# Symbol types
102+
a (local): int
103+
b (local): int
104+
c (local): str
105+
f (fn): <no-type>
106+
x (param): int?
107+
y (param): str?
108+
109+
# Diagnostics
110+
(none)
111+
### TITLE ###
112+
NotAndDeMorgan
113+
### DESCRIPTION ###
114+
`not (x == null or y == null)` should give us "both non-null"
115+
via the Negate path - flipping or's WhenFalse into the outer
116+
WhenTrue.
117+
### INPUT ###
118+
fn f(x: int?, y: str?):
119+
if not (x == null or y == null):
120+
a = x
121+
b = y
122+
### STDOUT ###
123+
# Identifier types
124+
x @ 2:13 -> int?
125+
y @ 2:26 -> str?
126+
a @ 3:9 -> <no-type>
127+
x @ 3:13 -> int
128+
b @ 4:9 -> <no-type>
129+
y @ 4:13 -> str
130+
131+
# Symbol types
132+
a (local): int
133+
b (local): str
134+
f (fn): <no-type>
135+
x (param): int?
136+
y (param): str?
137+
138+
# Diagnostics
139+
(none)

0 commit comments

Comments
 (0)