diff --git a/models/SimpleTheoryTest/Fishes.bpo b/models/SimpleTheoryTest/Fishes.bpo
index 6301595..32c0aef 100644
--- a/models/SimpleTheoryTest/Fishes.bpo
+++ b/models/SimpleTheoryTest/Fishes.bpo
@@ -3,4 +3,11 @@
+
+
+
+
+
+
+
diff --git a/models/SimpleTheoryTest/Fishes.bpr b/models/SimpleTheoryTest/Fishes.bpr
index e727bed..10f3254 100644
--- a/models/SimpleTheoryTest/Fishes.bpr
+++ b/models/SimpleTheoryTest/Fishes.bpr
@@ -54,4 +54,35 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/models/SimpleTheoryTest/Fishes.bps b/models/SimpleTheoryTest/Fishes.bps
index ced513e..51ea5a4 100644
--- a/models/SimpleTheoryTest/Fishes.bps
+++ b/models/SimpleTheoryTest/Fishes.bps
@@ -1,2 +1,4 @@
-
-
\ No newline at end of file
+
+
+
+
diff --git a/models/SimpleTheoryTest/Fishes.dtf b/models/SimpleTheoryTest/Fishes.dtf
index ec033af..944d2ff 100644
--- a/models/SimpleTheoryTest/Fishes.dtf
+++ b/models/SimpleTheoryTest/Fishes.dtf
@@ -1,9 +1,13 @@
-
+
+
+
+
+
diff --git a/models/SimpleTheoryTest/Fishes.tcf b/models/SimpleTheoryTest/Fishes.tcf
index 2d64af3..733ebca 100644
--- a/models/SimpleTheoryTest/Fishes.tcf
+++ b/models/SimpleTheoryTest/Fishes.tcf
@@ -7,5 +7,9 @@
+
+
+
+
diff --git a/models/SimpleTheoryTest/Fishes.tuf b/models/SimpleTheoryTest/Fishes.tuf
index af9aafa..41df772 100644
--- a/models/SimpleTheoryTest/Fishes.tuf
+++ b/models/SimpleTheoryTest/Fishes.tuf
@@ -7,5 +7,9 @@
+
+
+
+
diff --git a/models/SimpleTheoryTest/LePond.bpo b/models/SimpleTheoryTest/LePond.bpo
index 116adad..85c235c 100644
--- a/models/SimpleTheoryTest/LePond.bpo
+++ b/models/SimpleTheoryTest/LePond.bpo
@@ -1,7 +1,7 @@
-
+
-
+
@@ -10,7 +10,7 @@
-
+
diff --git a/src/main/java/com/viklauverk/eventbtools/core/IsAFormula.java b/src/main/java/com/viklauverk/eventbtools/core/IsAFormula.java
index 9945c80..971f433 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/IsAFormula.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/IsAFormula.java
@@ -1,6 +1,6 @@
/*
Copyright (C) 2021 Viklauverk AB
-
+
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU Affero General Public License as published by
the Free Software Foundation, either version 3 of the License, or
@@ -64,6 +64,11 @@ public Formula formula()
return formula_;
}
+ public String formulaString()
+ {
+ return formula_s_;
+ }
+
public String comment()
{
return comment_;
diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderTheoryUnicode.java b/src/main/java/com/viklauverk/eventbtools/core/RenderTheoryUnicode.java
index 067c8cd..fa5be68 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/RenderTheoryUnicode.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/RenderTheoryUnicode.java
@@ -131,6 +131,33 @@ public void renderProofSummary(Theory thr)
cnvs().stopAlignments();
}
+ @Override public void visit_AxiomsStart(Theory thr)
+ {
+ cnvs().startLine();
+ cnvs().keyword("theorems");
+ cnvs().endLine();
+
+ cnvs().startAlignments(Canvas.align_3col);
+ }
+
+ @Override public void visit_Axiom(Theory thr, Axiom axiom)
+ {
+ cnvs().startAlignedLine();
+ cnvs().label(axiom.name());
+ cnvs().align();
+ cnvs().startMath();
+ axiom.writeFormulaStringToCanvas(cnvs());
+ cnvs().stopMath();
+
+ stopAlignedLineAndHandlePotentialComment(axiom.comment(), cnvs(), axiom);
+
+ }
+
+ @Override public void visit_AxiomsEnd(Theory thr)
+ {
+ cnvs().stopAlignments();
+ }
+
@Override public void visit_TheoryEnd(Theory thr)
{
cnvs().startLine();
diff --git a/src/main/java/com/viklauverk/eventbtools/core/Theory.java b/src/main/java/com/viklauverk/eventbtools/core/Theory.java
index 01e183b..08295e6 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/Theory.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/Theory.java
@@ -37,19 +37,23 @@ public class Theory
private String name_;
private String comment_;
- private List imports_theories_;
+ private List imports_theories_ = new ArrayList<>();
- private Map polymorphic_data_types_;
- private List polymorphic_data_type_ordering_;
- private List polymorphic_data_type_names_;
+ private Map parameter_types_ = new HashMap<>();
+ private List parameter_type_ordering_ = new ArrayList<>();
+ private List parameter_type_names_ = new ArrayList<>();
- private Map operators_;
- private List operator_ordering_;
- private List operator_names_;
+ private Map polymorphic_data_types_ = new HashMap<>();
+ private List polymorphic_data_type_ordering_ = new ArrayList<>();
+ private List polymorphic_data_type_names_ = new ArrayList<>();
- private Map axioms_;
- private List axiom_ordering_;
- private List axiom_names_;
+ private Map operators_ = new HashMap<>();
+ private List operator_ordering_ = new ArrayList<>();
+ private List operator_names_ = new ArrayList<>();
+
+ private Map axioms_ = new HashMap<>();
+ private List axiom_ordering_ = new ArrayList<>();
+ private List axiom_names_ = new ArrayList<>();
private Map proof_obligations_ = new HashMap<>();
private List proof_obligation_ordering_ = new ArrayList<>();
@@ -66,7 +70,8 @@ public class Theory
private File theory_root_dir_; // Where to look for imported theories.
private Sys sys_;
- private SymbolTable symbol_table_;
+ private SymbolTable global_symbol_table_; // Inserted as parent to root symbol table in systen.
+ private SymbolTable local_symbol_table_; // Contains type parameters to be able to parse theorems etc.
private EDKTheory edk_theory_; // Points to the proper EVBT supported EDK information.
@@ -74,19 +79,6 @@ public Theory(String n, Sys s, File f, File trd)
{
name_ = n;
comment_ = "";
- imports_theories_ = new ArrayList<>();
-
- polymorphic_data_types_ = new HashMap<>();
- polymorphic_data_type_ordering_ = new ArrayList<>();
- polymorphic_data_type_names_ = new ArrayList<>();
-
- operators_ = new HashMap<>();
- operator_ordering_ = new ArrayList<>();
- operator_names_ = new ArrayList<>();
-
- axioms_ = new HashMap<>();
- axiom_ordering_ = new ArrayList<>();
- axiom_names_ = new ArrayList<>();
loaded_ = false;
theory_root_dir_ = trd;
@@ -107,7 +99,8 @@ public Theory(String n, Sys s, File f, File trd)
sys_ = s;
- symbol_table_ = null;
+ global_symbol_table_ = null;
+
}
public Sys sys()
@@ -145,9 +138,14 @@ List importsTheories()
return imports_theories_;
}
- SymbolTable symbolTable()
+ SymbolTable globalSymbolTable()
+ {
+ return global_symbol_table_;
+ }
+
+ SymbolTable localSymbolTable()
{
- return symbol_table_;
+ return local_symbol_table_;
}
public boolean hasPolymorphicDataTypes()
@@ -368,6 +366,14 @@ public void loadDeployedDTF() throws Exception
comment_ = m.valueOf("@org.eventb.core.comment");
}
+ List pts = document.selectNodes("//org.eventb.theory.core.scTypeParameter");
+ for (Node pt : pts)
+ {
+ String name = pt.valueOf("@name");
+ String core_type = pt.valueOf("@org.eventb.core.type"); // 'ℙ(T)')
+ addParameterType(name);
+ }
+
// Does this theory import other theories?
List its = document.selectNodes("//org.eventb.theory.core.useTheory");
for (Node it : its)
@@ -435,17 +441,14 @@ public void loadDeployedDTF() throws Exception
addOperator(o);
}
- // Load the axioms and theorems.
- list = document.selectNodes("//org.eventb.core.axiom");
+ list = document.selectNodes("//org.eventb.theory.core.scTheorem");
for (Node n : list)
{
String name = n.valueOf("@org.eventb.core.label");
String pred = n.valueOf("@org.eventb.core.predicate");
String comment = n.valueOf("@org.eventb.core.comment");
- String is_theorem = n.valueOf("@org.eventb.core.theorem");
- boolean it = is_theorem.equals("true");
- Axiom a = new Axiom(name, pred, comment, it);
+ Axiom a = new Axiom(name, pred, comment, true);
addAxiom(a);
}
@@ -615,33 +618,41 @@ public void loadCheckedTypes() throws Exception
void buildSymbolTable()
{
- if (symbol_table_ != null) return;
+ if (global_symbol_table_ != null) return;
log.debug("building symbol table for theory: %s", name_);
- symbol_table_ = sys_.newTheorySymbolTable(name_);
+ global_symbol_table_ = sys_.newTheorySymbolTable(name_);
for (PolymorphicDataType pdt : polymorphicDataTypeOrdering())
{
sys().addPolymorphicDataType(pdt);
- log.debug("added polymorphic data type %s to symbol table %s", pdt.longName(), symbol_table_.name());
- symbol_table_.addPolymorphicDataType(pdt);
+ log.debug("added polymorphic data type %s to symbol table %s", pdt.longName(), global_symbol_table_.name());
+ global_symbol_table_.addPolymorphicDataType(pdt);
for (Constructor cnstr : pdt.constructorOrdering())
{
log.debug(" constructor %s", cnstr.name());
- symbol_table_.addConstructor(cnstr);
+ global_symbol_table_.addConstructor(cnstr);
for (Destructor dstr : cnstr.destructorOrdering())
{
log.debug(" destructor %s", dstr.name());
- symbol_table_.addDestructor(dstr);
+ global_symbol_table_.addDestructor(dstr);
}
}
}
for (Operator c : operatorOrdering())
{
- log.debug("added operator %s to symbol table %s", c, symbol_table_.name());
- symbol_table_.addOperator(c);
+ log.debug("added operator %s to symbol table %s", c, global_symbol_table_.name());
+ global_symbol_table_.addOperator(c);
}
+
+ local_symbol_table_ = sys_.newSymbolTable("ParameterTypes_"+name_);
+ for (String p : parameterTypeOrdering())
+ {
+ log.debug("added parameter type %s to symbol table >%s<", p, local_symbol_table_.name());
+ local_symbol_table_.addSetSymbol(p);
+ }
+
}
public void parse()
@@ -658,13 +669,13 @@ public void parse()
}
for (Operator o : operatorOrdering())
{
- o.parseCheckedType(symbol_table_);
+ o.parseCheckedType(local_symbol_table_);
log.debug("parsed checked type %s for operator %s", o.checkedType(), o.name());
}
for (Axiom a : axiomOrdering())
{
- a.parse(symbol_table_);
- sys().typing().extractInfoFromAxiom(a.formula(), symbol_table_);
+ a.parse(local_symbol_table_);
+ sys().typing().extractInfoFromAxiom(a.formula(), local_symbol_table_);
}
}
@@ -698,4 +709,26 @@ public boolean isLoaded()
return loaded_;
}
+ public void addParameterType(String a)
+ {
+ parameter_types_.put(a, a);
+ parameter_type_ordering_.add(a);
+ parameter_type_names_ = parameter_types_.keySet().stream().sorted().collect(Collectors.toList());
+ }
+
+ public String getParameterType(String name)
+ {
+ return parameter_types_.get(name);
+ }
+
+ public List parameterTypeOrdering()
+ {
+ return parameter_type_ordering_;
+ }
+
+ public List parameterTypeNames()
+ {
+ return parameter_type_names_;
+ }
+
}
diff --git a/src/main/java/com/viklauverk/eventbtools/core/VisitTheory.java b/src/main/java/com/viklauverk/eventbtools/core/VisitTheory.java
index 7ecd295..0b5b462 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/VisitTheory.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/VisitTheory.java
@@ -71,6 +71,22 @@ public static void walk(RenderTheory rt, Theory thr, String pattern)
if (s) rt.visit_OperatorsEnd(thr);
}
+ if (thr.hasAxioms())
+ {
+ boolean s = Util.match(RenderTheory.buildAxiomPartName(thr, null), pattern);
+
+ if (s) rt.visit_AxiomsStart(thr);
+ for (Axiom axm : thr.axiomOrdering())
+ {
+ boolean ss = Util.match(RenderTheory.buildAxiomPartName(thr, axm), pattern);
+ if (ss)
+ {
+ rt.visit_Axiom(thr, axm);
+ }
+ }
+ if (s) rt.visit_AxiomsEnd(thr);
+ }
+
if (m) rt.visit_TheoryEnd(thr);
}
}