Revert changes to add asserting/assuming expressions. This is now imp…

…lemented in #1277.

.git-blame-ignore-revs

@@ -2,9 +2,3 @@
 # Date: Tue May 28 19:06:33 2024 +0200
 # reformat scala sources
 7a81a51d7791bc2e407fcfc6aef24bc1d1a52850
-
-# Bob Rubbens: wanted to merge some stuff in after reformatting
-fecd37bf5922332cc449f0ef95f79b09f370aa8e
-
-# (I think the same happened to Philip Tasche)
-97fb61d23cf04a909145ecb28946d1297d947ef4

src/col/vct/col/ast/Node.scala

@@ -2175,14 +2175,6 @@ final case class ActionPerm[G](loc: Expr[G], perm: Expr[G])(
     implicit val o: Origin
 ) extends Expr[G] with ActionPermImpl[G]
 
-final case class Assuming[G](assn: Expr[G], inner: Expr[G])(
-    implicit val o: Origin
-) extends Expr[G] with AssumingImpl[G]
-final case class Asserting[G](assn: Expr[G], inner: Expr[G])(
-    val blame: Blame[AssertFailed]
-)(implicit val o: Origin)
-    extends Expr[G] with AssertingImpl[G]
-
 sealed trait SmtlibType[G] extends Type[G]
 case class TSmtlibArray[G](index: Seq[Type[G]], value: Type[G])(
     implicit val o: Origin = DiagnosticOrigin

src/col/vct/col/origin/Blame.scala

@@ -183,9 +183,7 @@ case class CopyClassFailedBeforeCall(
     s"Insufficient permission for call `$source`."
 }
 
-// Type of `node` here is `Node`, but only to easily allow using this failure for both
-// assert statements and assert expressions.
-case class AssertFailed(failure: ContractFailure, node: Node[_])
+case class AssertFailed(failure: ContractFailure, node: Assert[_])
     extends WithContractFailure {
   override def baseCode: String = "assertFailed"
   override def descInContext: String = "Assertion may not hold, since"
@@ -1527,9 +1525,6 @@ object NonNullPointerNull
 object UnsafeDontCare {
   case class Satisfiability(reason: String)
       extends UnsafeDontCare[NontrivialUnsatisfiable]
-  case class Contract(reason: String) extends UnsafeDontCare[ContractedFailure]
-  case class Invocation(reason: String)
-      extends UnsafeDontCare[InvocationFailure]
 }
 
 trait UnsafeDontCare[T <: VerificationFailure]

src/col/vct/col/typerules/CoercingRewriter.scala

@@ -2144,8 +2144,6 @@ abstract class CoercingRewriter[Pre <: Generation]()
       case PVLEndpointExpr(endpoint, expr) => e
       case EndpointExpr(ref, expr) => e
       case ChorExpr(expr) => ChorExpr(bool(expr))
-      case e @ Asserting(assn, inner) => Asserting(bool(assn), inner)(e.blame)
-      case Assuming(assn, inner) => Assuming(bool(assn), inner)
       case CtExpr(inner) => e
       case EndpointFamilyExpr(ref) => e
     }

src/hre/hre/io/ChecksumReadableFile.scala

@@ -18,7 +18,7 @@ case class ChecksumReadableFile(
     checksumKind: String,
 ) extends InMemoryCachedReadable {
   override def underlyingPath: Option[Path] = Some(file)
-  override def fileName: String = file.getFileName.toString
+  override def fileName: String = file.toString
   override def isRereadable: Boolean = true
   private var checksumCache: Option[String] = None
 

src/hre/hre/io/RWFile.scala

@@ -7,7 +7,7 @@ import java.nio.file.{Files, Path}
 case class RWFile(file: Path, doWatch: Boolean = true)
     extends InMemoryCachedReadable with Writeable {
   override def underlyingPath: Option[Path] = Some(file)
-  override def fileName: String = file.getFileName.toString
+  override def fileName: String = file.toString
   override def isRereadable: Boolean = true
 
   override protected def getWriter: Writer = {

src/main/vct/main/stages/Transformation.scala

@@ -118,9 +118,9 @@ object Transformation extends LazyLogging {
     Of course, this all while still retaining the functionality of making it possible to pass more simplification rules
     using command line flags.
      */
-    Progress.hiddenStage(s"Loading PVL library file ${readable.fileName}") {
-      Util.loadPVLLibraryFile(readable, debugOptions)
-    }
+    Progress.hiddenStage(
+      s"Loading PVL library file ${readable.underlyingPath.getOrElse("<unknown>")}"
+    ) { Util.loadPVLLibraryFile(readable, debugOptions) }
   }
 
   def simplifierFor(path: PathOrStd, options: Options): RewriterBuilder =
@@ -418,7 +418,6 @@ case class SilverTransformation(
         RefuteToInvertedAssert,
         ExplicitResourceValues,
         EncodeResourceValues,
-        EncodeAssertingAssuming,
 
         // Encode parallel blocks
         EncodeSendRecv,

src/main/vct/options/types/PathOrStd.scala

@@ -15,7 +15,7 @@ sealed trait PathOrStd extends InMemoryCachedReadable with Writeable {
 
   override def fileName: String =
     this match {
-      case PathOrStd.Path(path) => path.getFileName.toString
+      case PathOrStd.Path(path) => path.toString
       case PathOrStd.StdInOrOut => "<stdio>"
     }
 

src/parsers/antlr4/LangPVLLexer.g4

@@ -105,8 +105,6 @@ UNFOLDING_ESC: '\\unfolding';
 UNFOLDING: 'unfolding';
 IN_ESC: '\\in';
 IN: 'in';
-ASSERTING: 'asserting';
-ASSUMING: 'assuming';
 NEW: 'new';
 ID: 'id';
 

src/parsers/antlr4/LangPVLParser.g4

@@ -158,10 +158,6 @@ unit
  | '(' '\\' '[' identifier ']' expr ')' # pvlShortEndpointExpr
  | '(' '\\chor' expr ')' # pvlLongChorExpr
  | '(' '\\' '[' ']' expr ')' # pvlShortChorExpr
- | '(' 'asserting' expr ')' # pvlBoolAsserting
- | '(' 'asserting' expr ';' expr ')' # pvlAsserting
- | '(' 'assuming' expr ')' # pvlBoolAssuming
- | '(' 'assuming' expr ';' expr ')' # pvlAssuming
  | 'this' # pvlThis
  | 'null' # pvlNull
  | '\\sender' # pvlSender

src/parsers/antlr4/SpecLexer.g4

@@ -148,8 +148,6 @@ CHOOSE: '\\choose';
 CHOOSE_FRESH: '\\choose_fresh';
 LENGTH: '\\length';
 OLD: '\\old';
-ASSERT_EXPR: '\\asserting';
-ASSUME_EXPR: '\\assuming';
 TYPEOF: '\\typeof';
 TYPEVALUE: '\\type';
 MATRIX: '\\matrix';

src/parsers/antlr4/SpecParser.g4

@@ -298,10 +298,6 @@ valPrimary
  | '\\is_int' '(' langExpr ')' # valIsInt
  | '\\choose' '(' langExpr ')' # valChoose
  | '\\choose_fresh' '(' langExpr ')' # valChooseFresh
- | '(' '\\assuming' langExpr ')' # valBoolAssuming
- | '(' '\\assuming' langExpr ';' langExpr ')' # valAssuming
- | '(' '\\asserting' langExpr ')' # valBoolAsserting
- | '(' '\\asserting' langExpr ';' langExpr ')' # valAsserting
  ;
 
 // Out spec: defined meaning: a language local

src/parsers/vct/parsers/transform/CToCol.scala

@@ -2002,13 +2002,6 @@ case class CToCol[G](
       case ValIsInt(_, _, arg, _) => SmtlibIsInt(convert(arg))
       case ValChoose(_, _, xs, _) => Choose(convert(xs))(blame(e))
       case ValChooseFresh(_, _, xs, _) => ChooseFresh(convert(xs))(blame(e))
-      case ValBoolAssuming(_, _, assn, _) => Assuming(convert(assn), tt)
-      case ValAssuming(_, _, assn, _, inner, _) =>
-        Assuming(convert(assn), convert(inner))
-      case ValBoolAsserting(_, _, assn, _) =>
-        Asserting(convert(assn), tt)(blame(e))
-      case ValAsserting(_, _, assn, _, inner, _) =>
-        Asserting(convert(assn), convert(inner))(blame(e))
     }
 
   def convert(implicit e: ValExprPairContext): (Expr[G], Expr[G]) =

src/parsers/vct/parsers/transform/JavaToCol.scala

@@ -2532,13 +2532,6 @@ case class JavaToCol[G](
       case ValNdLength(_, _, dims, _) => NdLength(convert(dims))
       case ValChoose(_, _, xs, _) => Choose(convert(xs))(blame(e))
       case ValChooseFresh(_, _, xs, _) => ChooseFresh(convert(xs))(blame(e))
-      case ValBoolAssuming(_, _, assn, _) => Assuming(convert(assn), tt)
-      case ValAssuming(_, _, assn, _, inner, _) =>
-        Assuming(convert(assn), convert(inner))
-      case ValBoolAsserting(_, _, assn, _) =>
-        Asserting(convert(assn), tt)(blame(e))
-      case ValAsserting(_, _, assn, _, inner, _) =>
-        Asserting(convert(assn), convert(inner))(blame(e))
     }
 
   def convert(implicit e: ValExprPairContext): (Expr[G], Expr[G]) =

src/parsers/vct/parsers/transform/PVLToCol.scala

@@ -504,13 +504,6 @@ case class PVLToCol[G](
         )
       case PvlLongChorExpr(_, _, inner, _) => ChorExpr(convert(inner))
       case PvlShortChorExpr(_, _, _, _, inner, _) => ChorExpr(convert(inner))
-      case PvlBoolAsserting(_, _, assn, _) =>
-        Asserting(convert(assn), tt)(blame(expr))
-      case PvlAsserting(_, _, assn, _, inner, _) =>
-        Asserting(convert(assn), convert(inner))(blame(expr))
-      case PvlBoolAssuming(_, _, assn, _) => Assuming(convert(assn), tt)
-      case PvlAssuming(_, _, assn, _, inner, _) =>
-        Assuming(convert(assn), convert(inner))
       case PvlSender(_) => PVLSender()
       case PvlReceiver(_) => PVLReceiver()
       case PvlMessage(_) => PVLMessage()
@@ -1993,13 +1986,6 @@ case class PVLToCol[G](
       case ValNdLength(_, _, dims, _) => NdLength(convert(dims))
       case ValChoose(_, _, xs, _) => Choose(convert(xs))(blame(e))
       case ValChooseFresh(_, _, xs, _) => ChooseFresh(convert(xs))(blame(e))
-      case ValBoolAssuming(_, _, assn, _) => Assuming(convert(assn), tt)
-      case ValAssuming(_, _, assn, _, inner, _) =>
-        Assuming(convert(assn), convert(inner))
-      case ValBoolAsserting(_, _, assn, _) =>
-        Asserting(convert(assn), tt)(blame(e))
-      case ValAsserting(_, _, assn, _, inner, _) =>
-        Asserting(convert(assn), convert(inner))(blame(e))
     }
 
   def convert(implicit e: ValExprPairContext): (Expr[G], Expr[G]) =