Add error messages for Coq and GenC not supporting pattern alternatives

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

Hide file tree

Showing 2 changed files with 5 additions and 0 deletions.
diff --git a/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala b/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala
@@ -465,6 +465,9 @@ private class S2IRImpl(override val s: tt.type,
         update(b, scrutinee)
         buildBinOp(scrutinee, O.Equals, lit)(pat.getPos)
 
+      case AlternativePattern(_, _) =>
+        reporter.fatalError(pat.getPos, s"Alternative Pattern, a.k.a pattern disjunction, is not yet supported by GenC")
+
       case UnapplyPattern(_, _, _, _, _) =>
         reporter.fatalError(pat.getPos, s"Unapply Pattern, a.k.a. Extractor Objects, is not supported by GenC")
     }

diff --git a/core/src/main/scala/stainless/verification/CoqEncoder.scala b/core/src/main/scala/stainless/verification/CoqEncoder.scala
@@ -225,6 +225,8 @@ trait CoqEncoder {
       ctx.reporter.warning(s"Ignoring type $tpe in the wildcard pattern $p.")
       //TODO not tested
       CoqTuplePatternVd(ps.map(transformPattern), VariablePattern(Some(makeFresh(id))))
+    case AlternativePattern(_, _) =>
+      ctx.reporter.fatalError(s"The translation to Coq does not support disjunctive patterns such as `$p` (${p.getClass}) yet.")
     case _ => ctx.reporter.fatalError(s"Coq does not support patterns such as `$p` (${p.getClass}) yet.")
   }