Skip to content

Commit

Permalink
Merge pull request #616 from utwente-fmt/some-printer-improvements
Browse files Browse the repository at this point in the history 
changes to PVLPrinter, JavaPrinter and PVLSyntax
  • Loading branch information
@petravandenbos-utwente
petravandenbos-utwente authored Mar 24, 2021
2 parents c3b6754 + b554aa7 commit 07d831b
Show file tree
Hide file tree
Showing 4 changed files with 121 additions and 170 deletions.
94 changes: 94 additions & 0 deletions col/src/main/java/vct/col/ast/print/AbstractPrinter.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,12 +10,19 @@
import vct.col.ast.generic.ASTNode;
import vct.col.ast.stmt.composite.Hole;
import vct.col.ast.stmt.decl.ASTSpecial;
import vct.col.ast.stmt.decl.Contract;
import vct.col.ast.stmt.decl.DeclarationStatement;
import vct.col.ast.stmt.decl.SignalsClause;
import vct.col.ast.type.ASTReserved;
import vct.col.ast.type.PrimitiveType;
import vct.col.ast.type.TypeExpression;
import vct.col.ast.util.ASTUtils;
import vct.col.ast.util.AbstractVisitor;
import vct.col.ast.syntax.Syntax;

import java.util.ArrayList;
import java.util.List;

/**
* This class contains the generic code for pretty printing expressions
* based on a given syntax.
Expand Down Expand Up @@ -251,5 +258,92 @@ public void visit(ASTSpecial s){
break;
}
}

@Override
public void visit(Contract contract) {
if (contract!=null) {
for (DeclarationStatement d : contract.given) {
out.printf("given ");
d.accept(this);
out.lnprintf("");
}
for (ASTNode e : ASTUtils.conjuncts(contract.invariant, StandardOperator.Star)) {
out.printf("loop_invariant ");
nextExpr();
e.accept(this);
out.lnprintf(";");
}
List<ASTNode> contextElems = new ArrayList<>();
for (ASTNode pre : ASTUtils.conjuncts(contract.pre_condition, StandardOperator.Star)) {
boolean added = false;
for (ASTNode post : ASTUtils.conjuncts(contract.post_condition, StandardOperator.Star)) {
if (pre.equals(post)) {
contextElems.add(pre);
added = true;
}
}
if (!added) {
printContractElement(pre, "requires");
}
}
for (ASTNode con : contextElems) {
printContractElement(con, "context");
}
for (ASTNode post : ASTUtils.conjuncts(contract.post_condition, StandardOperator.Star)) {
if (!contextElems.contains(post)) {
printContractElement(post, "ensures");
}
}
for (DeclarationStatement d : contract.yields) {
out.printf("yields ");
d.accept(this);
out.lnprintf("");
}
for (SignalsClause sc : contract.signals) {
sc.accept(this);
}
if (contract.modifies != null) {
out.printf("modifies ");
if (contract.modifies.length == 0) {
out.lnprintf("\\nothing;");
} else {
nextExpr();
contract.modifies[0].accept(this);
for (int i = 1; i < contract.modifies.length; i++) {
out.printf(", ");
nextExpr();
contract.modifies[i].accept(this);
}
out.lnprintf(";");
}
}
if (contract.accesses != null) {
out.printf("accessible ");
if (contract.accesses.length == 0) {
out.lnprintf("\\nothing;");
} else {
nextExpr();
contract.accesses[0].accept(this);
for (int i = 1; i < contract.accesses.length; i++) {
out.printf(", ");
nextExpr();
contract.accesses[i].accept(this);
}
out.lnprintf(";");
}
}
}
}

protected void printContractElement(ASTNode expr, String contractHead) {
out.printf(contractHead + " ");
nextExpr();
if(expr instanceof MethodInvokation)
out.print("(");
expr.accept(this);
if(expr instanceof MethodInvokation)
out.print(")");
out.lnprintf(";");
}
}

69 changes: 4 additions & 65 deletions col/src/main/java/vct/col/ast/print/JavaPrinter.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,6 @@
import vct.col.ast.type.*;
import vct.col.ast.syntax.JavaDialect;
import vct.col.ast.syntax.JavaSyntax;
import vct.col.ast.util.ASTUtils;
import vct.col.ast.util.ClassName;
import hre.util.LambdaHelper;

Expand Down Expand Up @@ -632,67 +631,7 @@ public void visit(Contract contract) {
if (contract!=null){
out.lnprintf("/*@");
out.incrIndent();
for (DeclarationStatement d:contract.given){
out.printf("given ");
d.accept(this);
out.lnprintf("");
}
for(ASTNode e:ASTUtils.conjuncts(contract.invariant,StandardOperator.Star)){
out.printf("loop_invariant ");
nextExpr();
e.accept(this);
out.lnprintf(";");
}
for(ASTNode e:ASTUtils.conjuncts(contract.pre_condition,StandardOperator.Star)){
out.printf("requires ");
nextExpr();
e.accept(this);
out.lnprintf(";");
}
for (DeclarationStatement d:contract.yields){
out.printf("yields ");
d.accept(this);
out.lnprintf("");
}
for(ASTNode e:ASTUtils.conjuncts(contract.post_condition,StandardOperator.Star)){
out.printf("ensures ");
nextExpr();
e.accept(this);
out.lnprintf(";");
}
for (SignalsClause sc : contract.signals){
sc.accept(this);
}
if (contract.modifies!=null){
out.printf("modifies ");
if (contract.modifies.length==0){
out.lnprintf("\\nothing;");
} else {
nextExpr();
contract.modifies[0].accept(this);
for(int i=1;i<contract.modifies.length;i++){
out.printf(", ");
nextExpr();
contract.modifies[i].accept(this);
}
out.lnprintf(";");
}
}
if (contract.accesses!=null){
out.printf("accessible ");
if (contract.accesses.length==0){
out.lnprintf("\\nothing;");
} else {
nextExpr();
contract.accesses[0].accept(this);
for(int i=1;i<contract.accesses.length;i++){
out.printf(", ");
nextExpr();
contract.accesses[i].accept(this);
}
out.lnprintf(";");
}
}
super.visit(contract);
out.decrIndent();
out.lnprintf("@*/");
}
Expand Down Expand Up @@ -1439,17 +1378,17 @@ public void visit(VariableDeclaration decl){
sep=",";
if (dd instanceof DeclarationStatement){
DeclarationStatement d = (DeclarationStatement)dd;
d.getType().accept(this);
out.print(d.name());
ASTNode init = d.initJava();
if (init!=null){
out.print("=");
out.print(" = ");
setExpr();
init.accept(this);
}
} else {
out.print("TODO");
}
}
out.println(";");
}

@Override
Expand Down
Loading

0 comments on commit 07d831b

Please sign in to comment.