Parse constructors/destructors with arguments.

viklauverk · Jul 12, 2024 · 2a939d8 · 2a939d8
1 parent 833949f
commit 2a939d8
Show file tree

Hide file tree

Showing 5 changed files with 47 additions and 3 deletions.
diff --git a/src/main/antlr4/com/viklauverk/eventbtools/core/EvBFormula.g4 b/src/main/antlr4/com/viklauverk/eventbtools/core/EvBFormula.g4
@@ -280,10 +280,16 @@ expression
    | { symbol_table.isNumberSymbol(_input.LT(1).getText()) }?     sym=SYMBOL meta? # NumberSymbol
    | { symbol_table.isNonFreeVariableSymbol(_input.LT(1).getText()) }?   variable=SYMBOL meta? # NonFreeExpressionVariable
    | { symbol_table.isVariableSymbol(_input.LT(1).getText()) }?   variable=SYMBOL  PRIM? meta? # ExpressionVariable
-   | { symbol_table.isConstructorSymbol(_input.LT(1).getText()) }? constructor=SYMBOL meta? # Constructor
-   | { symbol_table.isDestructorSymbol(_input.LT(1).getText()) }? destructor=SYMBOL meta? # Destructor
+
+   | { symbol_table.isConstructorSymbol(_input.LT(1).getText()) }? constructor=SYMBOL
+        meta? ( '(' parameters=listOfExpressions ')' )? # Constructor
+
+   | { symbol_table.isDestructorSymbol(_input.LT(1).getText()) }? destructor=SYMBOL
+        meta? ( '(' parameters=listOfExpressions ')' )? # Destructor
+
    | { symbol_table.isOperatorSymbol(OperatorNotationType.PREFIX, OperatorType.EXPRESSION, _input.LT(1).getText()) }? operator=SYMBOL
       meta? ( '(' parameters=listOfExpressions ')' )? # OperatorPrefixExpression
+
    | { symbol_table.isConstantSymbol(_input.LT(1).getText()) }?   constant=SYMBOL meta?        # ExpressionConstant
    // Should we be able to talk about all functions such that their applications give such and such result? For the moment, we can't.
    | { symbol_table.isVariableSymbol(_input.LT(1).getText()) }?   variable=SYMBOL PRIM? INV? meta? '(' inner=expression ')' # VariableFunctionApplication

diff --git a/src/main/java/com/viklauverk/eventbtools/core/Operator.java b/src/main/java/com/viklauverk/eventbtools/core/Operator.java
@@ -27,6 +27,7 @@ public class Operator extends Typed
     private Formula definition_;
     private OperatorNotationType notation_type_;
     private OperatorType operator_type_;
+    private String predicate_; // Used by axiomatic operator definitions.
     private Theory theory_;
 
     public Operator(String n, Theory t, OperatorNotationType nt, OperatorType ot)
@@ -73,6 +74,11 @@ public void addComment(String c)
         comment_ = c;
     }
 
+    public void setPredicate(String p)
+    {
+        predicate_ = p;
+    }
+
     public void setDefinition(Formula f)
     {
         definition_ = f;

diff --git a/src/main/java/com/viklauverk/eventbtools/core/PolymorphicDataType.java b/src/main/java/com/viklauverk/eventbtools/core/PolymorphicDataType.java
@@ -49,6 +49,7 @@ public PolymorphicDataType(String bn, Theory t)
     {
         base_name_ = bn;
         long_name_ = bn;
+        hr_long_name_ = bn;
 
         type_parameters_ = new ArrayList<>();
 

diff --git a/src/main/java/com/viklauverk/eventbtools/core/Theory.java b/src/main/java/com/viklauverk/eventbtools/core/Theory.java
@@ -415,7 +415,7 @@ public void loadDeployedDTF() throws Exception
             }
         }
 
-        // Load the operators.
+        // Load the operator definitions.
         list = document.selectNodes("//org.eventb.theory.core.scNewOperatorDefinition");
         for (Node n : list)
         {
@@ -441,6 +441,33 @@ public void loadDeployedDTF() throws Exception
             addOperator(o);
         }
 
+        // Load the axiomatic operator definitions.
+        list = document.selectNodes("//org.eventb.theory.core.scAxiomaticOperatorDefinition");
+        for (Node n : list)
+        {
+            String name = n.valueOf("@org.eventb.core.label");
+            String predicate = n.valueOf("@org.eventb.core.predicate");
+            String is_assocs = n.valueOf("@org.eventb.theory.core.associative");
+            String is_commus = n.valueOf("@org.eventb.theory.core.commutative");
+            String comment = n.valueOf("@org.eventb.core.comment");
+            String onts = n.valueOf("@org.eventb.theory.core.notationType");
+            OperatorNotationType ont = OperatorNotationType.valueOf(onts);
+            String ots = n.valueOf("@org.eventb.theory.core.formulaType");
+            OperatorType ot = null;
+            if (ots.equals("true")) ot = OperatorType.EXPRESSION;
+            else if (ots.equals("false")) ot = OperatorType.PREDICATE;
+            else LogModule.usageErrorStatic("Invalid formulaType %s for axiomatic operator %s in theory %s in file %s",
+                                            ots,
+                                            name,
+                                            name(),
+                                            dtf_);
+
+            Operator o = new Operator(name, this, ont, ot);
+            o.addComment(comment);
+            o.setPredicate(predicate);
+            addOperator(o);
+        }
+
         list = document.selectNodes("//org.eventb.theory.core.scTheorem");
         for (Node n : list)
         {

diff --git a/src/main/java/com/viklauverk/eventbtools/core/Util.java b/src/main/java/com/viklauverk/eventbtools/core/Util.java
@@ -294,6 +294,8 @@ public static int widthFromString(String s)
     public static
     String texSafe(String s)
     {
+        if (s == null) return "null";
+
         assert s.indexOf("\n") == -1 : "Internal error: string should not contain newline \""+s+"\"";
 
         StringBuilder sb = new StringBuilder();
@@ -335,6 +337,8 @@ String texSafe(String s)
     public static
     String htmqSafe(String s)
     {
+        if (s == null) return "null";
+
         assert s.indexOf("\n") == -1 : "Internal error: string should not contain newline \""+s+"\"";
         return "'"+s+"'";
     }