Skip to content

Commit

Permalink
Added defi to operators.
Browse files Browse the repository at this point in the history
  • Loading branch information
@weetmuts
weetmuts committed Jul 17, 2024
1 parent bbc0c0c commit ca739c7
Show file tree
Hide file tree
Showing 6 changed files with 86 additions and 46 deletions.
8 changes: 4 additions & 4 deletions models/SimpleTheoryTest/Fishes.tuf
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,9 +19,9 @@
<org.eventb.theory.core.constructorArgument name="(" org.eventb.core.identifier="nos" org.eventb.theory.core.type="Bass"/>
</org.eventb.theory.core.datatypeConstructor>
</org.eventb.theory.core.datatypeDefinition>
<org.eventb.theory.core.newOperatorDefinition name="." org.eventb.core.label="addo" org.eventb.theory.core.associative="false" org.eventb.theory.core.commutative="false" org.eventb.theory.core.formulaType="true" org.eventb.theory.core.notationType="INFIX">
<org.eventb.theory.core.operatorArgument name="'" org.eventb.core.expression="Salmon(T)" org.eventb.core.identifier="a"/>
<org.eventb.theory.core.directOperatorDefinition name="(" org.eventb.theory.core.formula="17"/>
<org.eventb.theory.core.operatorArgument name=")" org.eventb.core.expression="Bass" org.eventb.core.identifier="b"/>
<org.eventb.theory.core.newOperatorDefinition name="." org.eventb.core.comment="This is an adding operator" org.eventb.core.label="addo" org.eventb.theory.core.associative="false" org.eventb.theory.core.commutative="false" org.eventb.theory.core.formulaType="true" org.eventb.theory.core.notationType="INFIX">
<org.eventb.theory.core.operatorArgument name="'" org.eventb.core.comment="The first argument comment." org.eventb.core.expression="Salmon(T)" org.eventb.core.identifier="a"/>
<org.eventb.theory.core.directOperatorDefinition name="(" org.eventb.core.comment="A direct definition." org.eventb.theory.core.formula="17"/>
<org.eventb.theory.core.operatorArgument name=")" org.eventb.core.comment="The second argument comment." org.eventb.core.expression="Bass" org.eventb.core.identifier="b"/>
</org.eventb.theory.core.newOperatorDefinition>
</org.eventb.theory.core.theoryRoot>
47 changes: 46 additions & 1 deletion src/main/java/com/viklauverk/eventbtools/core/Canvas.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -953,9 +953,54 @@ public void align()
num_aligns_++;
}

public void indent(int n)
{
n *= 4;
while (n > 0)
{
space();
n--;
}
}

public void definedAs()
{
switch (render_target_)
{
case PLAIN:
append("≙");
return;
case TERMINAL:
append("≙");
return;
case TEX:
append("\\defi ");
return;
case HTML:
append("≙");
return;
}
assert (false) : "Unknown encoding "+render_target_;
}

public void space()
{
append(" ");
switch (render_target_)
{
case PLAIN:
append(" ");
return;
case TERMINAL:
append(" ");
return;
case TEX:
append("\\ ");
return;
case HTML:
append("&nbsp;");
return;
}
assert (false) : "Unknown encoding "+render_target_;
}

public void id(String s)
Expand Down
36 changes: 21 additions & 15 deletions src/main/java/com/viklauverk/eventbtools/core/Constructor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@

import java.util.ArrayList;
import java.util.List;
import java.util.LinkedList;
import java.util.Map;
import java.util.HashMap;
import java.util.Set;
Expand All @@ -29,13 +30,16 @@ public class Constructor extends Typed
{
private String name_;
private String comment_;
private Formula definition_;
private PolymorphicDataType polymorphic_datatype_;

private List<OperatorArgument> arguments_ = new LinkedList<>();

private Map<String,Destructor> destructors_ = new HashMap<>();
private List<Destructor> destructor_ordering_ = new ArrayList<>();
private List<String> destructor_names_ = new ArrayList<>();

private SymbolTable constructor_symbol_table_;

public Constructor(String n, PolymorphicDataType pdt)
{
name_ = n;
Expand All @@ -53,6 +57,16 @@ public String name()
return name_;
}

public void toString(Canvas cnvs)
{
cnvs.constructor(name_);
if (destructor_ordering_.size() > 0)
{
cnvs.append("(");
cnvs.append(")");
}
}

public String comment()
{
return comment_;
Expand All @@ -68,20 +82,6 @@ public void addComment(String c)
comment_ = c;
}

public void setDefinition(Formula f)
{
definition_ = f;
}

public Formula definition()
{
return definition_;
}

public boolean hasDefinition()
{
return definition_ != null;
}

public void addDestructor(Destructor o)
{
Expand All @@ -105,4 +105,10 @@ public List<String> destructorNames()
return destructor_names_;
}

public void addArgument(String name, String type)
{
constructor_symbol_table_.addVariableSymbol(name);
arguments_.add(new OperatorArgument(name, type, null));
}

}
4 changes: 2 additions & 2 deletions src/main/java/com/viklauverk/eventbtools/core/RenderTheoryTeX.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -92,8 +92,8 @@ public void visit_PolymorphicDataType(Theory thr, PolymorphicDataType pdt)
{
for (Constructor c: pdt.constructorOrdering())
{
cnvs().append(" ");
cnvs().constructor(c.name());
cnvs().space();
c.toString(cnvs());
}
}
cnvs().stopMath();
Expand Down
28 changes: 4 additions & 24 deletions src/main/java/com/viklauverk/eventbtools/core/RenderTheoryUnicode.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -94,8 +94,8 @@ public void renderProofSummary(Theory thr)
for (Constructor c : pdt.constructorOrdering())
{
cnvs().startAlignedLine();
cnvs().indent(1);
cnvs().startMath();
cnvs().append("\\ \\ ");
cnvs().constructor(c.name());
cnvs().stopMath();
cnvs().align();
Expand All @@ -119,6 +119,8 @@ public void renderProofSummary(Theory thr)
cnvs().keyword("operator ");
cnvs().startMath();
oprt.formula().toString(cnvs());
cnvs().space();
cnvs().definedAs();
cnvs().stopMath();
cnvs().endLine();

Expand All @@ -136,6 +138,7 @@ public void renderProofSummary(Theory thr)

if (oprt.hasDefinition())
{
cnvs().indent(1);
cnvs().startMath();
oprt.definition().toString(cnvs());
cnvs().stopMath();
Expand All @@ -147,29 +150,6 @@ public void renderProofSummary(Theory thr)

cnvs().stopAlignedLine();

/*
String id = buildOperatorPartName(oprt);
cnvs().marker(id);
cnvs().startLine();
if (oprt.notation() == OperatorNotationType.PREFIX)
{
cnvs().keywordLeft("prefix ");
}
if (oprt.notation() == OperatorNotationType.INFIX)
{
cnvs().keywordLeft("infix ");
}
cnvs().keywordLeft("operator ");
cnvs().id(oprt.name());
cnvs().endLine();
if (oprt.hasComment())
{
cnvs().acomment(oprt.comment());
}
*/
cnvs().stopAlignments();
}

Expand Down
9 changes: 9 additions & 0 deletions src/main/java/com/viklauverk/eventbtools/core/Theory.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -439,6 +439,15 @@ public void loadDeployedDTF() throws Exception
Constructor co = new Constructor(name, pdt);
co.addComment(comment);
pdt.addConstructor(co);

List<Node> args = c.selectNodes("org.eventb.theory.core.scConstructorArgument");
for (Node a : args)
{
name = a.valueOf("@name");
String type = a.valueOf("@org.eventb.core.type");
OperatorArgument oa = new OperatorArgument(name, type, null);
//co.addArgument(oa);
}
}
}

Expand Down

0 comments on commit ca739c7

Please sign in to comment.