parsing-related changes

viperproject · Sep 22, 2024 · 5040a93 · 5040a93
1 parent 2707ddb
commit 5040a93
Show file tree

Hide file tree

Showing 6 changed files with 3,677 additions and 3,604 deletions.
diff --git a/src/main/antlr4/GobraLexer.g4 b/src/main/antlr4/GobraLexer.g4
@@ -85,8 +85,9 @@ WRITEPERM   : 'writePerm' -> mode(NLSEMI);
 NOPERM      : 'noPerm' -> mode(NLSEMI);
 TRUSTED     : 'trusted' -> mode(NLSEMI);
 OUTLINE     : 'outline';
-DUPLICABLE  : 'duplicable';
+DUPLICABLE  : 'dup';
 PKG_INV     : 'pkgInvariant';
+OPEN_DUP_SINV : 'openDupPkgInv';
 INIT_POST   : 'initEnsures';
 IMPORT_PRE  : 'importRequires';
 PROOF       : 'proof';

diff --git a/src/main/antlr4/GobraParser.g4 b/src/main/antlr4/GobraParser.g4
@@ -33,13 +33,13 @@ maybeAddressableIdentifier: IDENTIFIER ADDR_MOD?;
 
 // Ghost members
 sourceFile:
-  ((initPost eos) | (pkgInvariant eos))* packageClause eos (importDecl eos)* (
+   (pkgInvariant eos)* (initPost eos)* packageClause eos (importDecl eos)* (
     (specMember | declaration | ghostMember) eos
   )* EOF;
 
 // `preamble` is a second entry point allowing us to parse only the top of a source.
 // That's also why we don not enforce EOF at the end.
-preamble: (initPost eos)* packageClause eos (importDecl eos)*;
+preamble: (pkgInvariant eos)* (initPost eos)* packageClause eos (importDecl eos)*;
 
 initPost: INIT_POST expression;
 
@@ -63,6 +63,7 @@ ghostStatement:
   | fold_stmt=(FOLD | UNFOLD) predicateAccess #foldStatement
   | kind=(ASSUME | ASSERT | REFUTE | INHALE | EXHALE) expression #proofStatement
   | matchStmt #matchStmt_
+  | OPEN_DUP_SINV (IDENTIFIER) #pkgInvStatement
   ;
 
 // Auxiliary statements