Parse theorems inside Theory using parameter types in local symbol ta…

…ble.
viklauverk · Jul 12, 2024 · 36f9fd8 · 36f9fd8
1 parent 2864bf3
commit 36f9fd8
Show file tree

Hide file tree

Showing 11 changed files with 183 additions and 50 deletions.
diff --git a/models/SimpleTheoryTest/Fishes.bpo b/models/SimpleTheoryTest/Fishes.bpo
@@ -3,4 +3,11 @@
     <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.poStamp="0">
         <org.eventb.core.poIdentifier name="T" org.eventb.core.type="ℙ(T)"/>
     </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poSequent name="thm1/S-THM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Therorem Soundness" org.eventb.core.poStamp="0">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/SimpleTheoryTest/Fishes.bpo|org.eventb.core.poFile#Fishes|org.eventb.core.poPredicateSet#ABSHYP"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="1∈ℕ" org.eventb.core.source="/SimpleTheoryTest/Fishes.tuf|org.eventb.theory.core.theoryRoot#Fishes|org.eventb.theory.core.theorem#*"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/SimpleTheoryTest/Fishes.tcf|org.eventb.theory.core.scTheoryRoot#Fishes|org.eventb.theory.core.scTheorem#Salmoo"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/SimpleTheoryTest/Fishes.tuf|org.eventb.theory.core.theoryRoot#Fishes|org.eventb.theory.core.theorem#*"/>
+        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/SimpleTheoryTest/Fishes.bpo|org.eventb.core.poFile#Fishes|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/SimpleTheoryTest/Fishes.bpo|org.eventb.core.poFile#Fishes|org.eventb.core.poSequent#thm1\/S-THM|org.eventb.core.poPredicateSet#SEQHYP"/>
+    </org.eventb.core.poSequent>
 </org.eventb.core.poFile>
diff --git a/models/SimpleTheoryTest/Fishes.bpr b/models/SimpleTheoryTest/Fishes.bpr
@@ -54,4 +54,35 @@
         <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL5:0"/>
         <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
     </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="thm1/S-THM" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
+        <org.eventb.core.lang name="L">
+            <org.eventb.theory.core.scDatatypeDefinition name="Crustean">
+                <org.eventb.theory.core.scTypeArgument name="T" org.eventb.theory.core.givenType="T"/>
+                <org.eventb.theory.core.scDatatypeConstructor name="nilfish"/>
+                <org.eventb.theory.core.scDatatypeConstructor name="conshel">
+                    <org.eventb.theory.core.scConstructorArgument name="head" org.eventb.core.type="T"/>
+                    <org.eventb.theory.core.scConstructorArgument name="tail" org.eventb.core.type="Crustean"/>
+                </org.eventb.theory.core.scDatatypeConstructor>
+            </org.eventb.theory.core.scDatatypeDefinition>
+            <org.eventb.theory.core.scNewOperatorDefinition name="compo" org.eventb.core.label="compo" org.eventb.core.predicate="⊤" org.eventb.core.source="/SimpleTheoryTest/Crabs.tuf|org.eventb.theory.core.theoryRoot#Crabs|org.eventb.theory.core.newOperatorDefinition#)" org.eventb.theory.core.associative="false" org.eventb.theory.core.commutative="false" org.eventb.theory.core.formulaType="false" org.eventb.theory.core.groupID="org.eventb.core.ast.relOp" org.eventb.theory.core.hasError="false" org.eventb.theory.core.notationType="INFIX" org.eventb.theory.core.wd="⊤">
+                <org.eventb.theory.core.scOperatorArgument name="left" org.eventb.core.source="/SimpleTheoryTest/Crabs.tuf|org.eventb.theory.core.theoryRoot#Crabs|org.eventb.theory.core.newOperatorDefinition#)|org.eventb.theory.core.operatorArgument#'" org.eventb.core.type="ℤ"/>
+                <org.eventb.theory.core.scOperatorArgument name="right" org.eventb.core.source="/SimpleTheoryTest/Crabs.tuf|org.eventb.theory.core.theoryRoot#Crabs|org.eventb.theory.core.newOperatorDefinition#)|org.eventb.theory.core.operatorArgument#(" org.eventb.core.type="ℤ"/>
+                <org.eventb.theory.core.scDirectOperatorDefinition name=")" org.eventb.core.source="/SimpleTheoryTest/Crabs.tuf|org.eventb.theory.core.theoryRoot#Crabs|org.eventb.theory.core.newOperatorDefinition#)|org.eventb.theory.core.directOperatorDefinition#)" org.eventb.theory.core.formula="⊤"/>
+            </org.eventb.theory.core.scNewOperatorDefinition>
+            <org.eventb.theory.core.scDatatypeDefinition name="Salmon">
+                <org.eventb.theory.core.scTypeArgument name="T" org.eventb.theory.core.givenType="T"/>
+                <org.eventb.theory.core.scDatatypeConstructor name="LeBigFish"/>
+                <org.eventb.theory.core.scDatatypeConstructor name="LeSmallFish"/>
+            </org.eventb.theory.core.scDatatypeDefinition>
+        </org.eventb.core.lang>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p1">
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="1∈ℕ"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL5:0"/>
+    </org.eventb.core.prProof>
 </org.eventb.core.prFile>
diff --git a/models/SimpleTheoryTest/Fishes.bps b/models/SimpleTheoryTest/Fishes.bps
@@ -1,2 +1,4 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<org.eventb.core.psFile/>
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<org.eventb.core.psFile>
+    <org.eventb.core.psStatus name="thm1/S-THM" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+</org.eventb.core.psFile>
diff --git a/models/SimpleTheoryTest/Fishes.dtf b/models/SimpleTheoryTest/Fishes.dtf
@@ -1,9 +1,13 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.theory.core.deployedTheoryRoot org.eventb.core.accurate="true" org.eventb.core.comment="GENERATED THEORY FILE: !DO NOT CHANGE!" org.eventb.theory.core.modificationHashValue="4c1601ee259e8450e4c3a8dc0a2df763" org.eventb.theory.core.outdated="false">
+<org.eventb.theory.core.deployedTheoryRoot org.eventb.core.accurate="true" org.eventb.core.comment="GENERATED THEORY FILE: !DO NOT CHANGE!" org.eventb.theory.core.modificationHashValue="3a6e0e8a9b2e2ce08a4e89f9b2a407e1" org.eventb.theory.core.outdated="false">
     <org.eventb.theory.core.useTheory name="Crabs" org.eventb.core.scTarget="/SimpleTheoryTest/Crabs.dtf|org.eventb.theory.core.deployedTheoryRoot#Crabs"/>
     <org.eventb.theory.core.scTypeParameter name="T" org.eventb.core.source="/SimpleTheoryTest/Fishes.tuf|org.eventb.theory.core.theoryRoot#Fishes|org.eventb.theory.core.typeParameter#(" org.eventb.core.type="ℙ(T)"/>
     <org.eventb.theory.core.scDatatypeDefinition name="Salmon" org.eventb.core.source="/SimpleTheoryTest/Fishes.tuf|org.eventb.theory.core.theoryRoot#Fishes|org.eventb.theory.core.datatypeDefinition#)" org.eventb.theory.core.hasError="false">
         <org.eventb.theory.core.scTypeArgument name="T" org.eventb.core.source="/SimpleTheoryTest/Fishes.tuf|org.eventb.theory.core.theoryRoot#Fishes|org.eventb.theory.core.datatypeDefinition#)|org.eventb.theory.core.typeArgument#'" org.eventb.theory.core.givenType="T"/>
         <org.eventb.theory.core.scDatatypeConstructor name="LeBigFish" org.eventb.core.source="/SimpleTheoryTest/Fishes.tuf|org.eventb.theory.core.theoryRoot#Fishes|org.eventb.theory.core.datatypeDefinition#)|org.eventb.theory.core.datatypeConstructor#("/>
+        <org.eventb.theory.core.scDatatypeConstructor name="LeSmallFish" org.eventb.core.source="/SimpleTheoryTest/Fishes.tuf|org.eventb.theory.core.theoryRoot#Fishes|org.eventb.theory.core.datatypeDefinition#)|org.eventb.theory.core.datatypeConstructor#)"/>
     </org.eventb.theory.core.scDatatypeDefinition>
+    <org.eventb.theory.core.scTheorem name="Salmoo" org.eventb.core.label="thm1" org.eventb.core.predicate="1∈ℕ" org.eventb.core.source="/SimpleTheoryTest/Fishes.tuf|org.eventb.theory.core.theoryRoot#Fishes|org.eventb.theory.core.theorem#*" org.eventb.theory.core.order="0"/>
+    <org.eventb.theory.core.scTheorem name="Salmop" org.eventb.core.label="thm2" org.eventb.core.predicate="(LeBigFish ⦂ Salmon(T))∈Salmon(T)" org.eventb.core.source="/SimpleTheoryTest/Fishes.tuf|org.eventb.theory.core.theoryRoot#Fishes|org.eventb.theory.core.theorem#+" org.eventb.theory.core.order="1"/>
+    <org.eventb.theory.core.scTheorem name="Salmoq" org.eventb.core.label="thm3" org.eventb.core.predicate="⊤" org.eventb.core.source="/SimpleTheoryTest/Fishes.tuf|org.eventb.theory.core.theoryRoot#Fishes|org.eventb.theory.core.theorem#," org.eventb.theory.core.order="2"/>
 </org.eventb.theory.core.deployedTheoryRoot>
diff --git a/models/SimpleTheoryTest/Fishes.tcf b/models/SimpleTheoryTest/Fishes.tcf
@@ -7,5 +7,9 @@
     <org.eventb.theory.core.scDatatypeDefinition name="Salmon" org.eventb.core.source="/SimpleTheoryTest/Fishes.tuf|org.eventb.theory.core.theoryRoot#Fishes|org.eventb.theory.core.datatypeDefinition#)" org.eventb.theory.core.hasError="false">
         <org.eventb.theory.core.scTypeArgument name="T" org.eventb.core.source="/SimpleTheoryTest/Fishes.tuf|org.eventb.theory.core.theoryRoot#Fishes|org.eventb.theory.core.datatypeDefinition#)|org.eventb.theory.core.typeArgument#'" org.eventb.theory.core.givenType="T"/>
         <org.eventb.theory.core.scDatatypeConstructor name="LeBigFish" org.eventb.core.source="/SimpleTheoryTest/Fishes.tuf|org.eventb.theory.core.theoryRoot#Fishes|org.eventb.theory.core.datatypeDefinition#)|org.eventb.theory.core.datatypeConstructor#("/>
+        <org.eventb.theory.core.scDatatypeConstructor name="LeSmallFish" org.eventb.core.source="/SimpleTheoryTest/Fishes.tuf|org.eventb.theory.core.theoryRoot#Fishes|org.eventb.theory.core.datatypeDefinition#)|org.eventb.theory.core.datatypeConstructor#)"/>
     </org.eventb.theory.core.scDatatypeDefinition>
+    <org.eventb.theory.core.scTheorem name="Salmoo" org.eventb.core.label="thm1" org.eventb.core.predicate="1∈ℕ" org.eventb.core.source="/SimpleTheoryTest/Fishes.tuf|org.eventb.theory.core.theoryRoot#Fishes|org.eventb.theory.core.theorem#*" org.eventb.theory.core.order="0"/>
+    <org.eventb.theory.core.scTheorem name="Salmop" org.eventb.core.label="thm2" org.eventb.core.predicate="(LeBigFish ⦂ Salmon(T))∈Salmon(T)" org.eventb.core.source="/SimpleTheoryTest/Fishes.tuf|org.eventb.theory.core.theoryRoot#Fishes|org.eventb.theory.core.theorem#+" org.eventb.theory.core.order="1"/>
+    <org.eventb.theory.core.scTheorem name="Salmoq" org.eventb.core.label="thm3" org.eventb.core.predicate="⊤" org.eventb.core.source="/SimpleTheoryTest/Fishes.tuf|org.eventb.theory.core.theoryRoot#Fishes|org.eventb.theory.core.theorem#," org.eventb.theory.core.order="2"/>
 </org.eventb.theory.core.scTheoryRoot>
diff --git a/models/SimpleTheoryTest/Fishes.tuf b/models/SimpleTheoryTest/Fishes.tuf
@@ -7,5 +7,9 @@
     <org.eventb.theory.core.datatypeDefinition name=")" org.eventb.core.comment="A fishy fish." org.eventb.core.identifier="Salmon">
         <org.eventb.theory.core.typeArgument name="'" org.eventb.theory.core.givenType="T"/>
         <org.eventb.theory.core.datatypeConstructor name="(" org.eventb.core.comment="A big constructor." org.eventb.core.identifier="LeBigFish"/>
+        <org.eventb.theory.core.datatypeConstructor name=")" org.eventb.core.comment="Another constructor" org.eventb.core.identifier="LeSmallFish"/>
     </org.eventb.theory.core.datatypeDefinition>
+    <org.eventb.theory.core.theorem name="*" org.eventb.core.comment="Another comment another day." org.eventb.core.label="thm1" org.eventb.core.predicate="1∈ℕ"/>
+    <org.eventb.theory.core.theorem name="+" org.eventb.core.comment="Complicated proven theorem." org.eventb.core.label="thm2" org.eventb.core.predicate="LeBigFish ∈ Salmon(T) "/>
+    <org.eventb.theory.core.theorem name="," org.eventb.core.label="thm3" org.eventb.core.predicate="⊤"/>
 </org.eventb.theory.core.theoryRoot>
diff --git a/models/SimpleTheoryTest/LePond.bpo b/models/SimpleTheoryTest/LePond.bpo
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.poFile org.eventb.core.poStamp="2">
+<org.eventb.core.poFile org.eventb.core.poStamp="0">
     <org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="0"/>
-    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/SimpleTheoryTest/LePond.bpo|org.eventb.core.poFile#LePond|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="2">
+    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/SimpleTheoryTest/LePond.bpo|org.eventb.core.poFile#LePond|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="0">
         <org.eventb.core.poIdentifier name="fush" org.eventb.core.type="Salmon(Crustean(BOOL))"/>
         <org.eventb.core.poIdentifier name="fish" org.eventb.core.type="Salmon(ℤ)"/>
     </org.eventb.core.poPredicateSet>
@@ -10,7 +10,7 @@
         <org.eventb.core.poIdentifier name="fish'" org.eventb.core.type="Salmon(ℤ)"/>
     </org.eventb.core.poPredicateSet>
     <org.eventb.core.poPredicateSet name="EVTALLHYPfusi" org.eventb.core.parentSet="/SimpleTheoryTest/LePond.bpo|org.eventb.core.poFile#LePond|org.eventb.core.poPredicateSet#EVTIDENTfusi" org.eventb.core.poStamp="0"/>
-    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/SimpleTheoryTest/LePond.bpo|org.eventb.core.poFile#LePond|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="2">
+    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/SimpleTheoryTest/LePond.bpo|org.eventb.core.poFile#LePond|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="0">
         <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="fish∈Salmon(ℤ)" org.eventb.core.source="/SimpleTheoryTest/LePond.bum|org.eventb.core.machineFile#LePond|org.eventb.core.invariant#_mDTKIT-9Ee-sh8HVMshK-g"/>
         <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="fush∈Salmon(Crustean(BOOL))" org.eventb.core.source="/SimpleTheoryTest/LePond.bum|org.eventb.core.machineFile#LePond|org.eventb.core.invariant#_mDTKIj-9Ee-sh8HVMshK-g"/>
     </org.eventb.core.poPredicateSet>

diff --git 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
@@ -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();