Fixes related to added pattern alternative support

Co-authored-by: SidonieBouthors <sidonie.bouthors@epfl.ch> Co-authored-by: Mai-LinhC <mai-linh.cordonnier@epfl.ch>
epfl-lara · Jan 10, 2025 · af9dce3 · af9dce3
1 parent 4b0cf5d
commit af9dce3
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 12 deletions.
diff --git a/core/src/main/scala/stainless/ast/ExprOps.scala b/core/src/main/scala/stainless/ast/ExprOps.scala
@@ -460,12 +460,10 @@ class ExprOps(override val trees: Trees) extends inox.ast.ExprOps(trees) { self
 
       case AlternativePattern(vdOpt, subPatterns) =>
         val freshVdOpt = vdOpt.map(vd => transform(vd.freshen, env))
-        val newPatterns = subPatterns.map(transformAndGetEnv(_, env))
+        // We don't need to freshen the subPatterns here, as they are not bound
         (
-          AlternativePattern(freshVdOpt, newPatterns.map(_._1)),
-          newPatterns.map(_._2).fold
-            (env ++ freshVdOpt.map(freshVd => vdOpt.get.id -> freshVd.id))
-            (_ ++ _)
+          AlternativePattern(freshVdOpt, subPatterns),
+          env ++ freshVdOpt.map(freshVd => vdOpt.get.id -> freshVd.id)
         )
 
       case LiteralPattern(vdOpt, lit) =>

diff --git a/core/src/main/scala/stainless/transformers/lattices/Core.scala b/core/src/main/scala/stainless/transformers/lattices/Core.scala
@@ -3295,14 +3295,14 @@ trait Core extends Definitions { ocbsl =>
         PatBdgsAndConds(newCtxs, subscruts ++ recBdgs, recPatConds)
 
       case LabelledPattern.Alternative(sub) => 
-        val PatBdgsAndConds(newCtxs, subBdgs, subPatConds) = 
+        val PatBdgsAndConds(newCtxs, _, subPatConds) = 
           sub.foldLeft(PatBdgsAndConds(ctxs, Seq.empty, Seq.empty)) {
-            case (PatBdgsAndConds(ctxs, bdgsAcc, condsAcc), subpat) =>
-              val PatBdgsAndConds(ctxs2, bdgs2, conds2) = addPatternBindingsAndConds(ctxs, scrut, subpat)
-              PatBdgsAndConds(ctxs2, bdgsAcc ++ bdgs2, condsAcc ++ conds2)
+            case (PatBdgsAndConds(ctxs, _, condsAcc), subpat) =>
+              val PatBdgsAndConds(ctxs2, _, conds2) = addPatternBindingsAndConds(ctxs, scrut, subpat)
+              PatBdgsAndConds(ctxs2, Seq.empty, condsAcc ++ conds2)
           }
-        // At least one of the subpatterns must match
         val cond = codeOfSig(mkOr(subPatConds), BoolTy)
+        assert(ctxs.isPrefixOf(newCtxs))
         PatBdgsAndConds(newCtxs.withCond(cond), Seq.empty, Seq(cond))
 
       case LabelledPattern.Unapply(recs, id, tps, subps) =>

diff --git a/frontends/dotty/src/main/scala/stainless/frontends/dotc/CodeExtraction.scala b/frontends/dotty/src/main/scala/stainless/frontends/dotc/CodeExtraction.scala
@@ -919,8 +919,8 @@ class CodeExtraction(inoxCtx: inox.Context,
   private def extractPattern(p: tpd.Tree, expectedTpe: Option[xt.Type], binder: Option[xt.ValDef] = None)(using dctx: DefContext): (xt.Pattern, DefContext) = p match {
 
     case a @ Alternative(subpatterns) =>
-      val (patterns, nctx) = subpatterns.map(extractPattern(_, expectedTpe, None)).unzip
-      (xt.AlternativePattern(binder, patterns), nctx.foldLeft(dctx)(_ `union` _))
+      val (patterns, nctx) = subpatterns.map(extractPattern(_, expectedTpe)).unzip
+      (xt.AlternativePattern(binder, patterns), dctx)
 
     case b @ Bind(name, t @ Typed(pat, tpt)) =>
       val vd = xt.ValDef(FreshIdentifier(name.toString), extractType(tpt), annotationsOf(b.symbol, ignoreOwner = true)).setPos(b.sourcePos)