From ed8082e833438536865afc73df2d033dae643ae1 Mon Sep 17 00:00:00 2001 From: Sidonie Bouthors Date: Sun, 5 Jan 2025 00:17:21 +0100 Subject: [PATCH] Add error messages for Coq and GenC not supporting pattern alternatives Co-authored-by: SidonieBouthors Co-authored-by: Mai-LinhC --- core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala | 3 +++ core/src/main/scala/stainless/verification/CoqEncoder.scala | 2 ++ 2 files changed, 5 insertions(+) diff --git a/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala b/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala index 6256b8fb0..e9b644ca1 100644 --- 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 index 972391b4e..04997599b 100644 --- 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.") }