Merge branch 'master' into refresh-by-default

dafny-lang · Jul 30, 2024 · d701a33 · d701a33
2 parents 4979a6e + d8868e5
commit d701a33
Show file tree

Hide file tree

Showing 93 changed files with 2,627 additions and 968 deletions.
diff --git a/Source/DafnyCore/AST/Expressions/StmtExpr.cs b/Source/DafnyCore/AST/Expressions/StmtExpr.cs
@@ -61,7 +61,7 @@ public Expression GetSConclusion() {
     } else if (S is CalcStmt) {
       var s = (CalcStmt)S;
       return s.Result;
-    } else if (S is RevealStmt) {
+    } else if (S is HideRevealStmt) {
       return CreateBoolLiteral(tok, true);  // one could use the definition axiom or the referenced labeled assertions, but "true" is conservative and much simpler :)
     } else if (S is UpdateStmt) {
       return CreateBoolLiteral(tok, true);  // one could use the postcondition of the method, suitably instantiated, but "true" is conservative and much simpler :)

diff --git a/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs b/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs
@@ -25,6 +25,8 @@ public Parser(DafnyOptions options, Scanner/*!*/ scanner, Errors/*!*/ errors, Ca
     theModule = new FileModuleDefinition(scanner.FirstToken);
   }
 
+  bool IsReveal(IToken nextToken) => la.kind == _reveal || (la.kind == _hide && nextToken.kind is _star or _ident);
+
   bool IsIdentifier(int kind) {
     return kind == _ident || kind == _least || kind == _greatest || kind == _older || kind == _opaque;
   }
@@ -156,7 +158,12 @@ bool IsWitness() {
   }
 
   bool IsFunctionDecl() {
-    switch (la.kind) {
+    var kind = la.kind;
+    return IsFunctionDecl(kind);
+  }
+
+  private bool IsFunctionDecl(int kind) {
+    switch (kind) {
       case _function:
       case _predicate:
       case _copredicate:
@@ -620,7 +627,6 @@ class DeclModifierData {
     public bool IsOpaque;
     public IToken OpaqueToken;
     public IToken FirstToken;
-
   }
 
   private ModuleKindEnum GetModuleKind(DeclModifierData mods) {

diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs
@@ -29,7 +29,7 @@ public partial class Printer {
     public void PrintStatement(Statement stmt, int indent) {
       Contract.Requires(stmt != null);
 
-      if (stmt.IsGhost && printMode == PrintModes.NoGhost) { return; }
+      if (stmt.IsGhost && printMode == PrintModes.NoGhostOrIncludes) { return; }
       for (LList<Label> label = stmt.Labels; label != null; label = label.Next) {
         if (label.Data.Name != null) {
           wr.WriteLine("label {0}:", label.Data.Name);
@@ -38,7 +38,7 @@ public void PrintStatement(Statement stmt, int indent) {
       }
 
       if (stmt is PredicateStmt) {
-        if (printMode == PrintModes.NoGhost) { return; }
+        if (printMode == PrintModes.NoGhostOrIncludes) { return; }
         Expression expr = ((PredicateStmt)stmt).Expr;
         var assertStmt = stmt as AssertStmt;
         var expectStmt = stmt as ExpectStmt;
@@ -70,8 +70,8 @@ public void PrintStatement(Statement stmt, int indent) {
         PrintAttributeArgs(s.Args, true);
         wr.Write(";");
 
-      } else if (stmt is RevealStmt revealStmt) {
-        PrintRevealStmt(revealStmt);
+      } else if (stmt is HideRevealStmt revealStmt) {
+        PrintHideReveal(revealStmt);
       } else if (stmt is BreakStmt) {
         var s = (BreakStmt)stmt;
         if (s.TargetLabel != null) {
@@ -220,7 +220,7 @@ public void PrintStatement(Statement stmt, int indent) {
 
       } else if (stmt is CalcStmt) {
         CalcStmt s = (CalcStmt)stmt;
-        if (printMode == PrintModes.NoGhost) { return; }   // Calcs don't get a "ghost" attribute, but they are.
+        if (printMode == PrintModes.NoGhostOrIncludes) { return; }   // Calcs don't get a "ghost" attribute, but they are.
         wr.Write("calc");
         PrintAttributes(stmt.Attributes);
         wr.Write(" ");
@@ -374,7 +374,7 @@ public void PrintStatement(Statement stmt, int indent) {
 
       } else if (stmt is VarDeclStmt) {
         var s = (VarDeclStmt)stmt;
-        if (s.Locals.Exists(v => v.IsGhost) && printMode == PrintModes.NoGhost) { return; }
+        if (s.Locals.Exists(v => v.IsGhost) && printMode == PrintModes.NoGhostOrIncludes) { return; }
         if (s.Locals.TrueForAll((v => v.IsGhost))) {
           // Emit the "ghost" modifier if all of the variables are ghost. If some are ghost, but not others,
           // then some of these ghosts are auto-converted to ghost, so we should not emit the "ghost" keyword.
@@ -457,17 +457,21 @@ public void PrintStatement(Statement stmt, int indent) {
       }
     }
 
-    private void PrintRevealStmt(RevealStmt revealStmt) {
-      wr.Write("reveal ");
-      var sep = "";
-      foreach (var e in revealStmt.Exprs) {
-        wr.Write(sep);
-        sep = ", ";
-        if (RevealStmt.SingleName(e) != null) {
-          // this will do the printing correctly for labels (or label-lookalikes) like 00_023 (which by PrintExpression below would be printed as 23)
-          wr.Write(RevealStmt.SingleName(e));
-        } else {
-          PrintExpression(e, true);
+    private void PrintHideReveal(HideRevealStmt revealStmt) {
+      wr.Write(revealStmt.Mode == Bpl.HideRevealCmd.Modes.Hide ? "hide " : "reveal ");
+      if (revealStmt.Wildcard) {
+        wr.Write("*");
+      } else {
+        var sep = "";
+        foreach (var e in revealStmt.Exprs) {
+          wr.Write(sep);
+          sep = ", ";
+          if (HideRevealStmt.SingleName(e) != null) {
+            // this will do the printing correctly for labels (or label-lookalikes) like 00_023 (which by PrintExpression below would be printed as 23)
+            wr.Write(HideRevealStmt.SingleName(e));
+          } else {
+            PrintExpression(e, true);
+          }
         }
       }
       wr.Write(";");