[add] except keyword

p-org · Oct 8, 2024 · 08aa8bc · 08aa8bc
1 parent 7317620
commit 08aa8bc
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 2 deletions.
diff --git a/Src/PCompiler/CompilerCore/Parser/PLexer.g4 b/Src/PCompiler/CompilerCore/Parser/PLexer.g4
@@ -75,6 +75,7 @@ PROVE      : 'prove';
 USING      : 'using';
 LEMMA      : 'Lemma';
 THEOREM    : 'Theorem';
+EXCEPT     : 'except';
 
 // module-system-specific keywords
 

diff --git a/Src/PCompiler/CompilerCore/Parser/PParser.g4 b/Src/PCompiler/CompilerCore/Parser/PParser.g4
@@ -74,7 +74,7 @@ invariantGroupDecl : LEMMA name=iden LBRACE invariantDecl* RBRACE
 
 proofBlockDecl : PROOF LBRACE proofBody RBRACE ;
 proofBody : proofItem* ;
-proofItem : PROVE (targets+=expr (COMMA targets+=expr)* | goalsAll=MUL) (USING ((premises+=expr (COMMA premises+=expr)*) | premisesAll=MUL))? SEMI # ProveUsingCmd ; 
+proofItem : PROVE (targets+=expr (COMMA targets+=expr)* | goalsAll=MUL) (USING ((premises+=expr (COMMA premises+=expr)*) | premisesAll=MUL))? (EXCEPT excludes+=expr (COMMA excludes+=expr)*)? SEMI # ProveUsingCmd ; 
 
 typeDefDecl : TYPE name=iden SEMI # ForeignTypeDef
             | TYPE name=iden ASSIGN type SEMI # PTypeDef

diff --git a/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/ProofCommand.cs b/Src/PCompiler/CompilerCore/TypeChecker/AST/Declarations/ProofCommand.cs
@@ -15,6 +15,7 @@ public ProofCommand(string name, ParserRuleContext sourceNode)
 
         public List<Invariant> Goals { get; set; }
         public List<Invariant> Premises { get; set; }
+        public List<Invariant> Excepts { get; set; }
         public ParserRuleContext SourceLocation { get; }
         public string Name { get; set; }
     }

diff --git a/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs b/Src/PCompiler/CompilerCore/TypeChecker/DeclarationVisitor.cs
@@ -723,6 +723,7 @@ public override object VisitProveUsingCmd(PParser.ProveUsingCmdContext context)
             var exprVisitor = new ExprVisitor(temporaryFunction, Handler);
             List<IPExpr> premises = [];
             List<IPExpr> goals = [];
+            List<IPExpr> excepts = context._excludes.Select(exprVisitor.Visit).ToList();
             if (context.premisesAll == null)
             {
                 premises = context._premises.Select(exprVisitor.Visit).ToList();
@@ -755,8 +756,10 @@ public override object VisitProveUsingCmd(PParser.ProveUsingCmdContext context)
             {
                 proofCmd.Goals = goals.SelectMany(x => ToInvariant(x, context)).ToList();
             }
+            proofCmd.Excepts = excepts.Zip(context._excludes, (x, y) => ToInvariant(x, y)).SelectMany(x => x).ToList();
             // exclude things appear in `goals` from `premises`
-            proofCmd.Premises = proofCmd.Premises.Except(proofCmd.Goals).ToList();
+            proofCmd.Premises = proofCmd.Premises.Except(proofCmd.Goals).Except(proofCmd.Excepts).ToList();
+            proofCmd.Goals = proofCmd.Goals.Except(proofCmd.Excepts).ToList();
             return proofCmd;
         }