From 63885f9bc83ecd4fd5022ee3716a13eb527692ea Mon Sep 17 00:00:00 2001
From: Luyu Cheng <chengluyu@live.cn>
Date: Tue, 12 Nov 2024 22:18:00 +0800
Subject: [PATCH] Recognize overlapping tuple patterns

---
 .../hkmc2/semantics/ucs/Normalization.scala   |  41 ++--
 .../ucs/normalization/UnifyTupleElements.mls  | 195 ++++++++++++++----
 .../test/mlscript/ucs/patterns/RestTuple.mls  |   6 +-
 3 files changed, 167 insertions(+), 75 deletions(-)

diff --git a/hkmc2/shared/src/main/scala/hkmc2/semantics/ucs/Normalization.scala b/hkmc2/shared/src/main/scala/hkmc2/semantics/ucs/Normalization.scala
index 4f4091fa8..3d661ce52 100644
--- a/hkmc2/shared/src/main/scala/hkmc2/semantics/ucs/Normalization.scala
+++ b/hkmc2/shared/src/main/scala/hkmc2/semantics/ucs/Normalization.scala
@@ -41,7 +41,7 @@ class Normalization(tl: TraceLogger)(using raise: Raise):
         case Split.Let(name, term, tail) => Split.Let(name, term, tail ++ those)
         case Split.Else(_) /* impossible */ | Split.End => those)
 
-  /** We don't care about `Pattern.Name` because they won't appear in `specialize`. */
+  /** We don't care about `Pattern.Var` because they won't appear in `specialize`. */
   extension (lhs: Pattern)
     /** Checks if two patterns are the same. */
     def =:=(rhs: Pattern): Bool = (lhs, rhs) match
@@ -49,13 +49,8 @@ class Normalization(tl: TraceLogger)(using raise: Raise):
       case (Pattern.Lit(l1), Pattern.Lit(l2)) => l1 === l2
       case (Pattern.Tuple(n1, b1), Pattern.Tuple(n2, b2)) => n1 == n2 && b1 == b2
       case (_, _) => false
-    /** Checks if `self` can be subsumed under `rhs`. */
-    def <:<(rhs: Pattern): Bool =
-      def mk(pattern: Pattern): Option[Literal | ClassSymbol | ModuleSymbol] = lhs match
-        case c: Pattern.ClassLike => S(c.sym)
-        case Pattern.Lit(l) => S(l)
-        case _ => N
-      compareCasePattern(mk(lhs), mk(rhs))
+    /** Checks if `lhs` can be subsumed under `rhs`. */
+    def <:<(rhs: Pattern): Bool = compareCasePattern(lhs, rhs)
     /**
       * If two class-like patterns has different `refined` flag. Report the
       * inconsistency as a warning.
@@ -195,31 +190,21 @@ class Normalization(tl: TraceLogger)(using raise: Raise):
 end Normalization
 
 object Normalization:
-  /**
-    * Hard-coded subtyping relations used in normalization and coverage checking.
-    */
-  def compareCasePattern(
-      lhs: Opt[Literal | ClassSymbol | ModuleSymbol],
-      rhs: Opt[Literal | ClassSymbol | ModuleSymbol]
-  ): Bool = (lhs, rhs) match
-    case (S(lhs), S(rhs)) => compareCasePattern(lhs, rhs)
-    case (_, _) => false
   /**
     * Hard-coded subtyping relations used in normalization and coverage checking.
     * TODO use base classes and also handle modules
     */
-  def compareCasePattern(
-      lhs: Literal | ClassSymbol | ModuleSymbol,
-      rhs: Literal | ClassSymbol | ModuleSymbol
-  ): Bool = (lhs, rhs) match
-    case (_, s: ClassSymbol) if s.nme === "Object" => true
-    case (s1: ClassSymbol, s2: ClassSymbol) if s1.nme === "Int" && s2.nme === "Num" => true
+  def compareCasePattern(lhs: Pattern, rhs: Pattern): Bool = (lhs, rhs) match
+    case (_, Pattern.ClassLike(s: ClassSymbol, _, _, _)) if s.nme === "Object" => true
+    case (Pattern.Tuple(n1, false), Pattern.Tuple(n2, false)) if n1 == n2 => true
+    case (Pattern.Tuple(n1, _), Pattern.Tuple(n2, true)) if n2 <= n1 => true
+    case (Pattern.ClassLike(s1: ClassSymbol, _, _, _), Pattern.ClassLike(s2: ClassSymbol, _, _, _)) if s1.nme === "Int" && s2.nme === "Num" => true
     // case (s1: ClassSymbol, s2: ClassSymbol) => s1 <:< s2 // TODO: find a way to check inheritance
-    case (Tree.IntLit(_), s: ClassSymbol) if s.nme === "Int" || s.nme === "Num" => true
-    case (Tree.StrLit(_), s: ClassSymbol) if s.nme === "Str" => true
-    case (Tree.DecLit(_), s: ClassSymbol) if s.nme === "Num" => true
-    case (Tree.BoolLit(_), s: ClassSymbol) if s.nme === "Bool" => true
-    case (Tree.UnitLit(true), s: ClassSymbol) if s.nme === "Unit" => true // TODO: how about undefined?
+    case (Pattern.Lit(Tree.IntLit(_)), Pattern.ClassLike(s: ClassSymbol, _, _, _)) if s.nme === "Int" || s.nme === "Num" => true
+    case (Pattern.Lit(Tree.StrLit(_)), Pattern.ClassLike(s: ClassSymbol, _, _, _)) if s.nme === "Str" => true
+    case (Pattern.Lit(Tree.DecLit(_)), Pattern.ClassLike(s: ClassSymbol, _, _, _)) if s.nme === "Num" => true
+    case (Pattern.Lit(Tree.BoolLit(_)), Pattern.ClassLike(s: ClassSymbol, _, _, _)) if s.nme === "Bool" => true
+    case (Pattern.Lit(Tree.UnitLit(true)), Pattern.ClassLike(s: ClassSymbol, _, _, _)) if s.nme === "Unit" => true // TODO: how about undefined?
     case (_, _) => false
 
   final case class VarSet(declared: Set[BlockLocalSymbol]):
diff --git a/hkmc2/shared/src/test/mlscript/ucs/normalization/UnifyTupleElements.mls b/hkmc2/shared/src/test/mlscript/ucs/normalization/UnifyTupleElements.mls
index 3b0b3d54b..b6f565ac0 100644
--- a/hkmc2/shared/src/test/mlscript/ucs/normalization/UnifyTupleElements.mls
+++ b/hkmc2/shared/src/test/mlscript/ucs/normalization/UnifyTupleElements.mls
@@ -4,7 +4,11 @@
 :import ../Prelude/Option.mls
 //│ Imported 3 member(s)
 
-fun add_6(x, y) =
+:import ../Prelude/Tuple.mls
+//│ Imported 2 member(s)
+
+// Normalization should unify fixed-length tuple patterns.
+fun sum_options(x, y) =
   if [x, y] is
     [Some(xv), Some(yv)] then xv + yv
     [Some(xv), None]     then xv
@@ -12,46 +16,153 @@ fun add_6(x, y) =
     [None,     None]     then 0
 //│ Desugared:
 //│ >  if
-//│ >    let $scrut@34 = [x@32#666, y@33#666]
-//│ >    $scrut@34 is []=2 and
-//│ >      let $first0@36 = $scrut@34#10.0
-//│ >      let $first1@35 = $scrut@34#11.1
-//│ >      $first0@36 is Some($param0@39) and
-//│ >        let xv@41 = $param0@39#1
-//│ >        $first1@35 is Some($param0@37) and
-//│ >          let yv@42 = $param0@37#1
-//│ >          else globalThis:import#Prelude#666.+‹member:+›(xv@41#666, yv@42#666)
-//│ >    $scrut@34 is []=2 and
-//│ >      let $first0@36 = $scrut@34#7.0
-//│ >      let $first1@35 = $scrut@34#8.1
-//│ >      $first0@36 is Some($param0@39) and
-//│ >        let xv@40 = $param0@39#0
-//│ >        $first1@35 is None then xv@40#666
-//│ >    $scrut@34 is []=2 and
-//│ >      let $first0@36 = $scrut@34#4.0
-//│ >      let $first1@35 = $scrut@34#5.1
-//│ >      $first0@36 is None and $first1@35 is Some($param0@37) and
-//│ >        let yv@38 = $param0@37#0
-//│ >        else yv@38#666
-//│ >    $scrut@34 is []=2 and
-//│ >      let $first0@36 = $scrut@34#1.0
-//│ >      let $first1@35 = $scrut@34#2.1
-//│ >      $first0@36 is None $first1@35 is None then 0
+//│ >    let $scrut@49 = [x@47#666, y@48#666]
+//│ >    $scrut@49 is []=2 and
+//│ >      let $first0@51 = $scrut@49#10.0
+//│ >      let $first1@50 = $scrut@49#11.1
+//│ >      $first0@51 is Some($param0@54) and
+//│ >        let xv@56 = $param0@54#1
+//│ >        $first1@50 is Some($param0@52) and
+//│ >          let yv@57 = $param0@52#1
+//│ >          else globalThis:import#Prelude#666.+‹member:+›(xv@56#666, yv@57#666)
+//│ >    $scrut@49 is []=2 and
+//│ >      let $first0@51 = $scrut@49#7.0
+//│ >      let $first1@50 = $scrut@49#8.1
+//│ >      $first0@51 is Some($param0@54) and
+//│ >        let xv@55 = $param0@54#0
+//│ >        $first1@50 is None then xv@55#666
+//│ >    $scrut@49 is []=2 and
+//│ >      let $first0@51 = $scrut@49#4.0
+//│ >      let $first1@50 = $scrut@49#5.1
+//│ >      $first0@51 is None and $first1@50 is Some($param0@52) and
+//│ >        let yv@53 = $param0@52#0
+//│ >        else yv@53#666
+//│ >    $scrut@49 is []=2 and
+//│ >      let $first0@51 = $scrut@49#1.0
+//│ >      let $first1@50 = $scrut@49#2.1
+//│ >      $first0@51 is None $first1@50 is None then 0
+//│ Normalized:
+//│ >  if
+//│ >    let $scrut@49 = [x@47#666, y@48#666]
+//│ >    $scrut@49 is []=2 and
+//│ >      let $first0@51 = $scrut@49#10.0
+//│ >      let $first1@50 = $scrut@49#11.1
+//│ >      $first0@51 is Some($param0@54) and
+//│ >        let xv@56 = $param0@54#1
+//│ >        $first1@50 is Some($param0@52) and
+//│ >          let yv@57 = $param0@52#1
+//│ >          else globalThis:import#Prelude#666.+‹member:+›(xv@56#666, yv@57#666)
+//│ >        let xv@55 = $param0@54#0
+//│ >        $first1@50 is None then xv@55#666
+//│ >      $first0@51 is None and
+//│ >        $first1@50 is Some($param0@52) and
+//│ >          let yv@53 = $param0@52#0
+//│ >          else yv@53#666
+//│ >        $first1@50 is None then 0
+
+
+
+
+// ========================================================================== //
+
+
+// Normalization should also unify the sub-scrutinees at the same position of
+// tuple patterns of different lengths.
+
+
+fun foo(xs) = if xs is
+  [Some(x)] then x
+  [Some(y), ..rest] then y
+//│ Desugared:
+//│ >  if
+//│ >    xs@62 is []=1 and
+//│ >      let $first0@64 = xs@62#4.0
+//│ >      $first0@64 is Some($param0@65) and
+//│ >        let x@68 = $param0@65#1
+//│ >        else x@68#666
+//│ >    xs@62 is []>=1 and
+//│ >      let $first0@64 = xs@62#1.0
+//│ >      let $rest@63 = globalThis:import#Tuple#666.tupleSlice‹member:tupleSlice›(xs@62#2, 1, 0)
+//│ >      $first0@64 is Some($param0@65) and
+//│ >        let y@66 = $param0@65#0
+//│ >        let rest@67 = $rest@63#0
+//│ >        else y@66#666
 //│ Normalized:
 //│ >  if
-//│ >    let $scrut@34 = [x@32#666, y@33#666]
-//│ >    $scrut@34 is []=2 and
-//│ >      let $first0@36 = $scrut@34#10.0
-//│ >      let $first1@35 = $scrut@34#11.1
-//│ >      $first0@36 is Some($param0@39) and
-//│ >        let xv@41 = $param0@39#1
-//│ >        $first1@35 is Some($param0@37) and
-//│ >          let yv@42 = $param0@37#1
-//│ >          else globalThis:import#Prelude#666.+‹member:+›(xv@41#666, yv@42#666)
-//│ >        let xv@40 = $param0@39#0
-//│ >        $first1@35 is None then xv@40#666
-//│ >      $first0@36 is None and
-//│ >        $first1@35 is Some($param0@37) and
-//│ >          let yv@38 = $param0@37#0
-//│ >          else yv@38#666
-//│ >        $first1@35 is None then 0
+//│ >    xs@62 is []=1 and
+//│ >      let $first0@64 = xs@62#4.0
+//│ >      $first0@64 is Some($param0@65) and
+//│ >        let x@68 = $param0@65#1
+//│ >        else x@68#666
+//│ >      let $rest@63 = globalThis:import#Tuple#666.tupleSlice‹member:tupleSlice›(xs@62#2, 1, 0)
+//│ >    xs@62 is []>=1 and
+//│ >      let $first0@64 = xs@62#1.0
+//│ >      let $rest@63 = globalThis:import#Tuple#666.tupleSlice‹member:tupleSlice›(xs@62#2, 1, 0)
+//│ >      $first0@64 is Some($param0@65) and
+//│ >        let y@66 = $param0@65#0
+//│ >        let rest@67 = $rest@63#0
+//│ >        else y@66#666
+
+fun do_something(x) = "done"
+
+
+fun foo(zs) = if zs is
+  [Some(x), Some(y)] then x + y
+  [None, ..rest] then do_something(rest)
+//│ Desugared:
+//│ >  if
+//│ >    zs@76 is []=2 and
+//│ >      let $first0@78 = zs@76#4.0
+//│ >      let $first1@81 = zs@76#5.1
+//│ >      $first0@78 is Some($param0@82) and
+//│ >        let x@83 = $param0@82#0
+//│ >        $first1@81 is Some($param0@84) and
+//│ >          let y@85 = $param0@84#0
+//│ >          else globalThis:import#Prelude#666.+‹member:+›(x@83#666, y@85#666)
+//│ >    zs@76 is []>=1 and
+//│ >      let $first0@78 = zs@76#1.0
+//│ >      let $rest@77 = globalThis:import#Tuple#666.tupleSlice‹member:tupleSlice›(zs@76#2, 1, 0)
+//│ >      $first0@78 is None and
+//│ >        let rest@79 = $rest@77#0
+//│ >        else globalThis:block#3#666.do_something‹member:do_something›(rest@79#666)
+//│ Normalized:
+//│ >  if
+//│ >    zs@76 is []=2 and
+//│ >      let $first0@78 = zs@76#4.0
+//│ >      let $first1@81 = zs@76#5.1
+//│ >      $first0@78 is Some($param0@82) and
+//│ >        let x@83 = $param0@82#0
+//│ >        $first1@81 is Some($param0@84) and
+//│ >          let y@85 = $param0@84#0
+//│ >          else globalThis:import#Prelude#666.+‹member:+›(x@83#666, y@85#666)
+//│ >        let $rest@77 = globalThis:import#Tuple#666.tupleSlice‹member:tupleSlice›(zs@76#2, 1, 0)
+//│ >      let $rest@77 = globalThis:import#Tuple#666.tupleSlice‹member:tupleSlice›(zs@76#2, 1, 0)
+//│ >      $first0@78 is None and
+//│ >        let rest@79 = $rest@77#0
+//│ >        else globalThis:block#3#666.do_something‹member:do_something›(rest@79#666)
+//│ >    zs@76 is []>=1 and
+//│ >      let $first0@78 = zs@76#1.0
+//│ >      let $rest@77 = globalThis:import#Tuple#666.tupleSlice‹member:tupleSlice›(zs@76#2, 1, 0)
+//│ >      $first0@78 is None and
+//│ >        let rest@79 = $rest@77#0
+//│ >        else globalThis:block#3#666.do_something‹member:do_something›(rest@79#666)
+
+:expect 4
+foo([Some(1), Some(3)])
+//│ = 4
+
+:expect 'done'
+foo([None, Some(1), Some(2)])
+//│ = 'done'
+
+:re
+foo([Some(0)])
+//│ ═══[RUNTIME ERROR] Error: match error
+
+:re
+foo([Some(0), Some(1), Some(2)])
+//│ ═══[RUNTIME ERROR] Error: match error
+
+:re
+foo([])
+//│ ═══[RUNTIME ERROR] Error: match error
diff --git a/hkmc2/shared/src/test/mlscript/ucs/patterns/RestTuple.mls b/hkmc2/shared/src/test/mlscript/ucs/patterns/RestTuple.mls
index 5a865cccc..6dbe70535 100644
--- a/hkmc2/shared/src/test/mlscript/ucs/patterns/RestTuple.mls
+++ b/hkmc2/shared/src/test/mlscript/ucs/patterns/RestTuple.mls
@@ -35,11 +35,7 @@ fun stupid(xs) = if xs is
 //│     ys = rest;
 //│     return ys
 //│   } else {
-//│     if (Array.isArray(xs) && xs.length === 0) {
-//│       return "empty"
-//│     } else {
-//│       throw new globalThis.Error("match error")
-//│     }
+//│     throw new globalThis.Error("match error")
 //│   }
 //│ };
 //│ undefined