Skip to content

Commit 0c437de

Browse files
chengluyuchengluyu
committed
Recognize overlapping tuple patterns
1 parent bfdf811 commit 0c437de

File tree

4 files changed

+171
-79
lines changed

4 files changed

+171
-79
lines changed

‎hkmc2/shared/src/main/scala/hkmc2/semantics/ucs/Normalization.scala

Lines changed: 13 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -41,21 +41,16 @@ class Normalization(tl: TraceLogger)(using raise: Raise):
4141
case Split.Let(name, term, tail) => Split.Let(name, term, tail ++ those)
4242
case Split.Else(_) /* impossible */ | Split.End => those)
4343

44-
/** We don't care about `Pattern.Name` because they won't appear in `specialize`. */
44+
/** We don't care about `Pattern.Var` because they won't appear in `specialize`. */
4545
extension (lhs: Pattern)
4646
/** Checks if two patterns are the same. */
4747
def =:=(rhs: Pattern): Bool = (lhs, rhs) match
4848
case (c1: Pattern.ClassLike, c2: Pattern.ClassLike) => c1.sym === c2.sym
4949
case (Pattern.Lit(l1), Pattern.Lit(l2)) => l1 === l2
5050
case (Pattern.Tuple(n1, b1), Pattern.Tuple(n2, b2)) => n1 == n2 && b1 == b2
5151
case (_, _) => false
52-
/** Checks if `self` can be subsumed under `rhs`. */
53-
def <:<(rhs: Pattern): Bool =
54-
def mk(pattern: Pattern): Option[Literal | ClassSymbol | ModuleSymbol] = lhs match
55-
case c: Pattern.ClassLike => S(c.sym)
56-
case Pattern.Lit(l) => S(l)
57-
case _ => N
58-
compareCasePattern(mk(lhs), mk(rhs))
52+
/** Checks if `lhs` can be subsumed under `rhs`. */
53+
def <:<(rhs: Pattern): Bool = compareCasePattern(lhs, rhs)
5954
/**
6055
* If two class-like patterns has different `refined` flag. Report the
6156
* inconsistency as a warning.
@@ -195,31 +190,21 @@ class Normalization(tl: TraceLogger)(using raise: Raise):
195190
end Normalization
196191

197192
object Normalization:
198-
/**
199-
* Hard-coded subtyping relations used in normalization and coverage checking.
200-
*/
201-
def compareCasePattern(
202-
lhs: Opt[Literal | ClassSymbol | ModuleSymbol],
203-
rhs: Opt[Literal | ClassSymbol | ModuleSymbol]
204-
): Bool = (lhs, rhs) match
205-
case (S(lhs), S(rhs)) => compareCasePattern(lhs, rhs)
206-
case (_, _) => false
207193
/**
208194
* Hard-coded subtyping relations used in normalization and coverage checking.
209195
* TODO use base classes and also handle modules
210196
*/
211-
def compareCasePattern(
212-
lhs: Literal | ClassSymbol | ModuleSymbol,
213-
rhs: Literal | ClassSymbol | ModuleSymbol
214-
): Bool = (lhs, rhs) match
215-
case (_, s: ClassSymbol) if s.nme === "Object" => true
216-
case (s1: ClassSymbol, s2: ClassSymbol) if s1.nme === "Int" && s2.nme === "Num" => true
197+
def compareCasePattern(lhs: Pattern, rhs: Pattern): Bool = (lhs, rhs) match
198+
case (_, Pattern.ClassLike(s: ClassSymbol, _, _, _)) if s.nme === "Object" => true
199+
case (Pattern.Tuple(n1, false), Pattern.Tuple(n2, false)) if n1 == n2 => true
200+
case (Pattern.Tuple(n1, _), Pattern.Tuple(n2, true)) if n2 <= n1 => true
201+
case (Pattern.ClassLike(s1: ClassSymbol, _, _, _), Pattern.ClassLike(s2: ClassSymbol, _, _, _)) if s1.nme === "Int" && s2.nme === "Num" => true
217202
// case (s1: ClassSymbol, s2: ClassSymbol) => s1 <:< s2 // TODO: find a way to check inheritance
218-
case (Tree.IntLit(_), s: ClassSymbol) if s.nme === "Int" || s.nme === "Num" => true
219-
case (Tree.StrLit(_), s: ClassSymbol) if s.nme === "Str" => true
220-
case (Tree.DecLit(_), s: ClassSymbol) if s.nme === "Num" => true
221-
case (Tree.BoolLit(_), s: ClassSymbol) if s.nme === "Bool" => true
222-
case (Tree.UnitLit(true), s: ClassSymbol) if s.nme === "Unit" => true // TODO: how about undefined?
203+
case (Pattern.Lit(Tree.IntLit(_)), Pattern.ClassLike(s: ClassSymbol, _, _, _)) if s.nme === "Int" || s.nme === "Num" => true
204+
case (Pattern.Lit(Tree.StrLit(_)), Pattern.ClassLike(s: ClassSymbol, _, _, _)) if s.nme === "Str" => true
205+
case (Pattern.Lit(Tree.DecLit(_)), Pattern.ClassLike(s: ClassSymbol, _, _, _)) if s.nme === "Num" => true
206+
case (Pattern.Lit(Tree.BoolLit(_)), Pattern.ClassLike(s: ClassSymbol, _, _, _)) if s.nme === "Bool" => true
207+
case (Pattern.Lit(Tree.UnitLit(true)), Pattern.ClassLike(s: ClassSymbol, _, _, _)) if s.nme === "Unit" => true // TODO: how about undefined?
223208
case (_, _) => false
224209

225210
final case class VarSet(declared: Set[BlockLocalSymbol]):

‎hkmc2/shared/src/test/mlscript/ucs/normalization/UnifySubScrutinees.mls

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -43,14 +43,14 @@ fun sum(acc, xs) =
4343
//│ > xs@30 is Cons($param0@31, $param1@32) and
4444
//│ > let x@33 = $param0@31#0
4545
//│ > let xs@34 = $param1@32#0
46-
//│ > else globalThis:block#3#666.sum‹member:sum›(builtin:+#99(acc@29#666, x@33#666), xs@34#666)
46+
//│ > else globalThis:block#3#666.sum‹member:sum›(builtin:+#100(acc@29#666, x@33#666), xs@34#666)
4747
//│ > xs@30 is Nil then acc@29#666
4848
//│ Normalized:
4949
//│ > if
5050
//│ > xs@30 is Cons($param0@31, $param1@32) and
5151
//│ > let x@33 = $param0@31#0
5252
//│ > let xs@34 = $param1@32#0
53-
//│ > else globalThis:block#3#666.sum‹member:sum›(builtin:+#99(acc@29#666, x@33#666), xs@34#666)
53+
//│ > else globalThis:block#3#666.sum‹member:sum›(builtin:+#100(acc@29#666, x@33#666), xs@34#666)
5454
//│ > xs@30 is Nil then acc@29#666
5555

5656
:todo
@@ -70,7 +70,7 @@ fun test(xs) =
7070
//│ > let x@52 = $param0@45#1
7171
//│ > $param1@46 is Cons($param0@48, $param1@49) and
7272
//│ > let y@53 = $param0@48#1
73-
//│ > $param1@49 is Nil then builtin:+#100(x@52#666, y@53#666)
73+
//│ > $param1@49 is Nil then builtin:+#101(x@52#666, y@53#666)
7474
//│ > xs@39 is Some($param0@40) and $param0@40 is Cons($param0@41, $param1@42) and $param0@41 is "mul" and $param1@42 is Cons($param0@45, $param1@46) and
7575
//│ > let x@47 = $param0@45#0
7676
//│ > $param1@46 is Cons($param0@48, $param1@49) and
@@ -89,7 +89,7 @@ fun test(xs) =
8989
//│ > let x@52 = $param0@45#1
9090
//│ > $param1@46 is Cons($param0@48, $param1@49) and
9191
//│ > let y@53 = $param0@48#1
92-
//│ > $param1@49 is Nil then builtin:+#100(x@52#666, y@53#666)
92+
//│ > $param1@49 is Nil then builtin:+#101(x@52#666, y@53#666)
9393
//│ > $param0@41 is "mul" and $param1@42 is Cons($param0@45, $param1@46) and
9494
//│ > let x@47 = $param0@45#0
9595
//│ > $param1@46 is Cons($param0@48, $param1@49) and

‎hkmc2/shared/src/test/mlscript/ucs/normalization/UnifyTupleElements.mls

Lines changed: 153 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -4,54 +4,165 @@
44
:import ../Prelude/Option.mls
55
//│ Imported 3 member(s)
66

7-
fun add_6(x, y) =
7+
:import ../Prelude/Tuple.mls
8+
//│ Imported 2 member(s)
9+
10+
// Normalization should unify fixed-length tuple patterns.
11+
fun sum_options(x, y) =
812
if [x, y] is
913
[Some(xv), Some(yv)] then xv + yv
1014
[Some(xv), None] then xv
1115
[None, Some(yv)] then yv
1216
[None, None] then 0
1317
//│ Desugared:
1418
//│ > if
15-
//│ > let $scrut@16 = [x@14#666, y@15#666]
16-
//│ > $scrut@16 is []=2 and
17-
//│ > let $first0@18 = $scrut@16#10.0
18-
//│ > let $first1@17 = $scrut@16#11.1
19-
//│ > $first0@18 is Some($param0@21) and
20-
//│ > let xv@23 = $param0@21#1
21-
//│ > $first1@17 is Some($param0@19) and
22-
//│ > let yv@24 = $param0@19#1
23-
//│ > else builtin:+#98(xv@23#666, yv@24#666)
24-
//│ > $scrut@16 is []=2 and
25-
//│ > let $first0@18 = $scrut@16#7.0
26-
//│ > let $first1@17 = $scrut@16#8.1
27-
//│ > $first0@18 is Some($param0@21) and
28-
//│ > let xv@22 = $param0@21#0
29-
//│ > $first1@17 is None then xv@22#666
30-
//│ > $scrut@16 is []=2 and
31-
//│ > let $first0@18 = $scrut@16#4.0
32-
//│ > let $first1@17 = $scrut@16#5.1
33-
//│ > $first0@18 is None and $first1@17 is Some($param0@19) and
34-
//│ > let yv@20 = $param0@19#0
35-
//│ > else yv@20#666
36-
//│ > $scrut@16 is []=2 and
37-
//│ > let $first0@18 = $scrut@16#1.0
38-
//│ > let $first1@17 = $scrut@16#2.1
39-
//│ > $first0@18 is None $first1@17 is None then 0
19+
//│ > let $scrut@31 = [x@29#666, y@30#666]
20+
//│ > $scrut@31 is []=2 and
21+
//│ > let $first0@33 = $scrut@31#10.0
22+
//│ > let $first1@32 = $scrut@31#11.1
23+
//│ > $first0@33 is Some($param0@36) and
24+
//│ > let xv@38 = $param0@36#1
25+
//│ > $first1@32 is Some($param0@34) and
26+
//│ > let yv@39 = $param0@34#1
27+
//│ > else builtin:+#98(xv@38#666, yv@39#666)
28+
//│ > $scrut@31 is []=2 and
29+
//│ > let $first0@33 = $scrut@31#7.0
30+
//│ > let $first1@32 = $scrut@31#8.1
31+
//│ > $first0@33 is Some($param0@36) and
32+
//│ > let xv@37 = $param0@36#0
33+
//│ > $first1@32 is None then xv@37#666
34+
//│ > $scrut@31 is []=2 and
35+
//│ > let $first0@33 = $scrut@31#4.0
36+
//│ > let $first1@32 = $scrut@31#5.1
37+
//│ > $first0@33 is None and $first1@32 is Some($param0@34) and
38+
//│ > let yv@35 = $param0@34#0
39+
//│ > else yv@35#666
40+
//│ > $scrut@31 is []=2 and
41+
//│ > let $first0@33 = $scrut@31#1.0
42+
//│ > let $first1@32 = $scrut@31#2.1
43+
//│ > $first0@33 is None $first1@32 is None then 0
44+
//│ Normalized:
45+
//│ > if
46+
//│ > let $scrut@31 = [x@29#666, y@30#666]
47+
//│ > $scrut@31 is []=2 and
48+
//│ > let $first0@33 = $scrut@31#10.0
49+
//│ > let $first1@32 = $scrut@31#11.1
50+
//│ > $first0@33 is Some($param0@36) and
51+
//│ > let xv@38 = $param0@36#1
52+
//│ > $first1@32 is Some($param0@34) and
53+
//│ > let yv@39 = $param0@34#1
54+
//│ > else builtin:+#98(xv@38#666, yv@39#666)
55+
//│ > let xv@37 = $param0@36#0
56+
//│ > $first1@32 is None then xv@37#666
57+
//│ > $first0@33 is None and
58+
//│ > $first1@32 is Some($param0@34) and
59+
//│ > let yv@35 = $param0@34#0
60+
//│ > else yv@35#666
61+
//│ > $first1@32 is None then 0
62+
63+
64+
65+
66+
// ========================================================================== //
67+
68+
69+
// Normalization should also unify the sub-scrutinees at the same position of
70+
// tuple patterns of different lengths.
71+
72+
73+
fun foo(xs) = if xs is
74+
[Some(x)] then x
75+
[Some(y), ..rest] then y
76+
//│ Desugared:
77+
//│ > if
78+
//│ > xs@44 is []=1 and
79+
//│ > let $first0@46 = xs@44#4.0
80+
//│ > $first0@46 is Some($param0@47) and
81+
//│ > let x@50 = $param0@47#1
82+
//│ > else x@50#666
83+
//│ > xs@44 is []>=1 and
84+
//│ > let $first0@46 = xs@44#1.0
85+
//│ > let $rest@45 = globalThis:import#Tuple#666.tupleSlice‹member:tupleSlice›(xs@44#2, 1, 0)
86+
//│ > $first0@46 is Some($param0@47) and
87+
//│ > let y@48 = $param0@47#0
88+
//│ > let rest@49 = $rest@45#0
89+
//│ > else y@48#666
4090
//│ Normalized:
4191
//│ > if
42-
//│ > let $scrut@16 = [x@14#666, y@15#666]
43-
//│ > $scrut@16 is []=2 and
44-
//│ > let $first0@18 = $scrut@16#10.0
45-
//│ > let $first1@17 = $scrut@16#11.1
46-
//│ > $first0@18 is Some($param0@21) and
47-
//│ > let xv@23 = $param0@21#1
48-
//│ > $first1@17 is Some($param0@19) and
49-
//│ > let yv@24 = $param0@19#1
50-
//│ > else builtin:+#98(xv@23#666, yv@24#666)
51-
//│ > let xv@22 = $param0@21#0
52-
//│ > $first1@17 is None then xv@22#666
53-
//│ > $first0@18 is None and
54-
//│ > $first1@17 is Some($param0@19) and
55-
//│ > let yv@20 = $param0@19#0
56-
//│ > else yv@20#666
57-
//│ > $first1@17 is None then 0
92+
//│ > xs@44 is []=1 and
93+
//│ > let $first0@46 = xs@44#4.0
94+
//│ > $first0@46 is Some($param0@47) and
95+
//│ > let x@50 = $param0@47#1
96+
//│ > else x@50#666
97+
//│ > let $rest@45 = globalThis:import#Tuple#666.tupleSlice‹member:tupleSlice›(xs@44#2, 1, 0)
98+
//│ > xs@44 is []>=1 and
99+
//│ > let $first0@46 = xs@44#1.0
100+
//│ > let $rest@45 = globalThis:import#Tuple#666.tupleSlice‹member:tupleSlice›(xs@44#2, 1, 0)
101+
//│ > $first0@46 is Some($param0@47) and
102+
//│ > let y@48 = $param0@47#0
103+
//│ > let rest@49 = $rest@45#0
104+
//│ > else y@48#666
105+
106+
fun do_something(x) = "done"
107+
108+
109+
fun foo(zs) = if zs is
110+
[Some(x), Some(y)] then x + y
111+
[None, ..rest] then do_something(rest)
112+
//│ Desugared:
113+
//│ > if
114+
//│ > zs@58 is []=2 and
115+
//│ > let $first0@60 = zs@58#4.0
116+
//│ > let $first1@63 = zs@58#5.1
117+
//│ > $first0@60 is Some($param0@64) and
118+
//│ > let x@65 = $param0@64#0
119+
//│ > $first1@63 is Some($param0@66) and
120+
//│ > let y@67 = $param0@66#0
121+
//│ > else builtin:+#99(x@65#666, y@67#666)
122+
//│ > zs@58 is []>=1 and
123+
//│ > let $first0@60 = zs@58#1.0
124+
//│ > let $rest@59 = globalThis:import#Tuple#666.tupleSlice‹member:tupleSlice›(zs@58#2, 1, 0)
125+
//│ > $first0@60 is None and
126+
//│ > let rest@61 = $rest@59#0
127+
//│ > else globalThis:block#3#666.do_something‹member:do_something›(rest@61#666)
128+
//│ Normalized:
129+
//│ > if
130+
//│ > zs@58 is []=2 and
131+
//│ > let $first0@60 = zs@58#4.0
132+
//│ > let $first1@63 = zs@58#5.1
133+
//│ > $first0@60 is Some($param0@64) and
134+
//│ > let x@65 = $param0@64#0
135+
//│ > $first1@63 is Some($param0@66) and
136+
//│ > let y@67 = $param0@66#0
137+
//│ > else builtin:+#99(x@65#666, y@67#666)
138+
//│ > let $rest@59 = globalThis:import#Tuple#666.tupleSlice‹member:tupleSlice›(zs@58#2, 1, 0)
139+
//│ > let $rest@59 = globalThis:import#Tuple#666.tupleSlice‹member:tupleSlice›(zs@58#2, 1, 0)
140+
//│ > $first0@60 is None and
141+
//│ > let rest@61 = $rest@59#0
142+
//│ > else globalThis:block#3#666.do_something‹member:do_something›(rest@61#666)
143+
//│ > zs@58 is []>=1 and
144+
//│ > let $first0@60 = zs@58#1.0
145+
//│ > let $rest@59 = globalThis:import#Tuple#666.tupleSlice‹member:tupleSlice›(zs@58#2, 1, 0)
146+
//│ > $first0@60 is None and
147+
//│ > let rest@61 = $rest@59#0
148+
//│ > else globalThis:block#3#666.do_something‹member:do_something›(rest@61#666)
149+
150+
:expect 4
151+
foo([Some(1), Some(3)])
152+
//│ = 4
153+
154+
:expect 'done'
155+
foo([None, Some(1), Some(2)])
156+
//│ = 'done'
157+
158+
:re
159+
foo([Some(0)])
160+
//│ ═══[RUNTIME ERROR] Error: match error
161+
162+
:re
163+
foo([Some(0), Some(1), Some(2)])
164+
//│ ═══[RUNTIME ERROR] Error: match error
165+
166+
:re
167+
foo([])
168+
//│ ═══[RUNTIME ERROR] Error: match error

‎hkmc2/shared/src/test/mlscript/ucs/patterns/RestTuple.mls

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -35,11 +35,7 @@ fun stupid(xs) = if xs is
3535
//│ ys = rest;
3636
//│ return ys
3737
//│ } else {
38-
//│ if (Array.isArray(xs) && xs.length === 0) {
39-
//│ return "empty"
40-
//│ } else {
41-
//│ throw new globalThis.Error("match error")
42-
//│ }
38+
//│ throw new globalThis.Error("match error")
4339
//│ }
4440
//│ };
4541
//│ undefined

0 commit comments

Comments
 (0)