Skip to content

Commit

Permalink
Recognize overlapping tuple patterns
Browse files Browse the repository at this point in the history
  • Loading branch information
@chengluyu
chengluyu committed Nov 13, 2024
1 parent b0a4d41 commit 63885f9
Show file tree
Hide file tree
Showing 3 changed files with 167 additions and 75 deletions.
41 changes: 13 additions & 28 deletions hkmc2/shared/src/main/scala/hkmc2/semantics/ucs/Normalization.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,21 +41,16 @@ 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
case (c1: Pattern.ClassLike, c2: Pattern.ClassLike) => c1.sym === c2.sym
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.
Expand Down Expand Up @@ -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]):
Expand Down
195 changes: 153 additions & 42 deletions hkmc2/shared/src/test/mlscript/ucs/normalization/UnifyTupleElements.mls
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,54 +4,165 @@
: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
[None, Some(yv)] then yv
[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
6 changes: 1 addition & 5 deletions hkmc2/shared/src/test/mlscript/ucs/patterns/RestTuple.mls
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 63885f9

Please sign in to comment.