From a3dd33359f41c250a5b35c0813004e4daedc70a2 Mon Sep 17 00:00:00 2001 From: Jan Gruteser <jan.gruteser@hhu.de> Date: Thu, 2 Jan 2025 16:01:18 +0100 Subject: [PATCH] minor layouting --- .../analysis/InstanceTransformation.java | 1 + .../java/de/tla2b/analysis/SymbolRenamer.java | 6 +- .../translation/UsedDefinitionsFinder.java | 10 +-- src/main/java/de/tla2bAst/BAstCreator.java | 74 +++++++++---------- 4 files changed, 45 insertions(+), 46 deletions(-) diff --git a/src/main/java/de/tla2b/analysis/InstanceTransformation.java b/src/main/java/de/tla2b/analysis/InstanceTransformation.java index 018576f..2204e8e 100644 --- a/src/main/java/de/tla2b/analysis/InstanceTransformation.java +++ b/src/main/java/de/tla2b/analysis/InstanceTransformation.java @@ -35,6 +35,7 @@ public class InstanceTransformation extends BuiltInOPs implements ASTConstants { /** * replace all definitions M1!Op1 by the real Op1 and add included definitions from instances + * -> SubstInNode should never occur after InstanceTransformation */ private void start() { for (OpDefNode def : defs.values()) { diff --git a/src/main/java/de/tla2b/analysis/SymbolRenamer.java b/src/main/java/de/tla2b/analysis/SymbolRenamer.java index 122284b..92bd5ce 100644 --- a/src/main/java/de/tla2b/analysis/SymbolRenamer.java +++ b/src/main/java/de/tla2b/analysis/SymbolRenamer.java @@ -142,20 +142,20 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals { } // constants - for(OpDeclNode node : moduleNode.getConstantDecls()) { + for (OpDeclNode node : moduleNode.getConstantDecls()) { String newName = incName(node.getName().toString()); globalNames.add(newName); node.setToolObject(NEW_NAME, newName); } - for(OpDefNode node : moduleNode.getOpDefs()) { + for (OpDefNode node : moduleNode.getOpDefs()) { String newName = getOperatorName(node); globalNames.add(newName); node.setToolObject(NEW_NAME, newName); usedNamesTable.put(node, new HashSet<>()); } - for(AssumeNode node : moduleNode.getAssumptions()) { + for (AssumeNode node : moduleNode.getAssumptions()) { visitNode(node.getAssume(), new HashSet<>()); } diff --git a/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java b/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java index 39b964b..67b06eb 100644 --- a/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java +++ b/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java @@ -22,7 +22,7 @@ public class UsedDefinitionsFinder extends AbstractASTVisitor { public UsedDefinitionsFinder(SpecAnalyser specAnalyser) { DebugUtils.printMsg("Finding used definitions"); - // some definition are not yet supported, like recursive definitions + // some definitions are not yet supported, like recursive definitions // hence it is important not to try and translate all of them and only the used ones if (specAnalyser.getConfigFileEvaluator() != null) { @@ -82,13 +82,11 @@ public class UsedDefinitionsFinder extends AbstractASTVisitor { OpDefNode def = (OpDefNode) n.getOperator(); ModuleNode moduleNode = def.getSource().getOriginallyDefinedInModuleNode(); - if (moduleNode.getName().toString().equals("TLA2B")) { + if (moduleNode.getName().toString().equals("TLA2B")) return; - } - if (BBuiltInOPs.contains(def.getName()) - && STANDARD_MODULES.contains(def.getSource().getOriginallyDefinedInModuleNode().getName().toString())) { + if (BBuiltInOPs.contains(def.getName()) && STANDARD_MODULES.contains(moduleNode.getName().toString())) return; - } + if (usedDefinitions.add(def)) { visitExprNode(def.getBody()); } diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java index 7f144c7..ef40219 100644 --- a/src/main/java/de/tla2bAst/BAstCreator.java +++ b/src/main/java/de/tla2bAst/BAstCreator.java @@ -121,8 +121,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuil return; List<EnumType> printed = new ArrayList<>(); - OpDeclNode[] cons = moduleNode.getConstantDecls(); - for (OpDeclNode con : cons) { + for (OpDeclNode con : moduleNode.getConstantDecls()) { TLAType type = (TLAType) con.getToolObject(TYPE_ID); EnumType e = null; @@ -1306,14 +1305,17 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuil return new ADomainExpression(visitExprOrOpArgNodeExpression(n.getArgs()[0])); case OPCODE_sof: // [ A -> B] - return new ATotalFunctionExpression(visitExprOrOpArgNodeExpression(n.getArgs()[0]), - visitExprOrOpArgNodeExpression(n.getArgs()[1])); + return new ATotalFunctionExpression( + visitExprOrOpArgNodeExpression(n.getArgs()[0]), + visitExprOrOpArgNodeExpression(n.getArgs()[1]) + ); case OPCODE_tup: { // $Tuple List<PExpression> list = new ArrayList<>(); for (int i = 0; i < n.getArgs().length; i++) { list.add(visitExprOrOpArgNodeExpression(n.getArgs()[i])); } + TLAType t = (TLAType) n.getToolObject(TYPE_ID); if (t instanceof TupleType) { return new ACoupleExpression(list); @@ -1748,34 +1750,28 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuil AConjunctPredicate conj = new AConjunctPredicate(); if (pair.getArgs()[0] == null) { - ANegationPredicate neg = new ANegationPredicate(); - neg.setPredicate(createDisjunction(conditions)); - conj.setLeft(neg); + conj.setLeft(new ANegationPredicate(createDisjunction(conditions))); } else { conditions.add(visitExprOrOpArgNodePredicate(pair.getArgs()[0])); conj.setLeft(visitExprOrOpArgNodePredicate(pair.getArgs()[0])); } - AEqualPredicate equals = new AEqualPredicate(); - equals.setLeft(createIdentifierNode("t_")); - equals.setRight(visitExprOrOpArgNodeExpression(pair.getArgs()[1])); - conj.setRight(equals); + conj.setRight(new AEqualPredicate( + createIdentifierNode("t_"), + visitExprOrOpArgNodeExpression(pair.getArgs()[1]) + )); disjunctionList.add(conj); } - AComprehensionSetExpression comprehension = new AComprehensionSetExpression(); - comprehension.setIdentifiers(createIdentifierList("t_")); - comprehension.setPredicates(createDisjunction(disjunctionList)); - ADefinitionExpression defCall = new ADefinitionExpression(); - defCall.setDefLiteral(new TIdentifierLiteral("CHOOSE")); - List<PExpression> params = new ArrayList<>(); - params.add(comprehension); - defCall.setParameters(params); - return defCall; + return new ADefinitionExpression( + new TIdentifierLiteral("CHOOSE"), + Collections.singletonList(new AComprehensionSetExpression( + createIdentifierList("t_"), + createDisjunction(disjunctionList) + )) + ); } private List<PExpression> createIdentifierList(String name) { - ArrayList<PExpression> list = new ArrayList<>(); - list.add(createIdentifierNode(name)); - return list; + return Collections.singletonList(createIdentifierNode(name)); } private PPredicate visitBuiltInKindPredicate(OpApplNode n) { @@ -1783,10 +1779,10 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuil switch (getOpCode(n.getOperator().getName())) { case OPCODE_land: // \land { - AConjunctPredicate conjunction = new AConjunctPredicate(); - conjunction.setLeft(visitExprOrOpArgNodePredicate(n.getArgs()[0])); - conjunction.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[1])); - returnNode = conjunction; + returnNode = new AConjunctPredicate( + visitExprOrOpArgNodePredicate(n.getArgs()[0]), + visitExprOrOpArgNodePredicate(n.getArgs()[1]) + ); break; } case OPCODE_cl: // $ConjList @@ -1800,10 +1796,10 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuil } case OPCODE_lor: // \/ { - ADisjunctPredicate disjunction = new ADisjunctPredicate(); - disjunction.setLeft(visitExprOrOpArgNodePredicate(n.getArgs()[0])); - disjunction.setRight(visitExprOrOpArgNodePredicate(n.getArgs()[1])); - returnNode = disjunction; + returnNode = new ADisjunctPredicate( + visitExprOrOpArgNodePredicate(n.getArgs()[0]), + visitExprOrOpArgNodePredicate(n.getArgs()[1]) + ); break; } case OPCODE_dl: // $DisjList @@ -1819,13 +1815,17 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuil returnNode = new ANegationPredicate(visitExprOrOpArgNodePredicate(n.getArgs()[0])); break; case OPCODE_equiv: // \equiv - returnNode = new AEquivalencePredicate(visitExprOrOpArgNodePredicate(n.getArgs()[0]), - visitExprOrOpArgNodePredicate(n.getArgs()[1])); + returnNode = new AEquivalencePredicate( + visitExprOrOpArgNodePredicate(n.getArgs()[0]), + visitExprOrOpArgNodePredicate(n.getArgs()[1]) + ); break; case OPCODE_implies: // => - returnNode = new AImplicationPredicate(visitExprOrOpArgNodePredicate(n.getArgs()[0]), - visitExprOrOpArgNodePredicate(n.getArgs()[1])); + returnNode = new AImplicationPredicate( + visitExprOrOpArgNodePredicate(n.getArgs()[0]), + visitExprOrOpArgNodePredicate(n.getArgs()[1]) + ); break; case OPCODE_be: { // \E x \in S : P @@ -2090,7 +2090,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuil if (n instanceof ExprNode) { return visitExprNodePredicate((ExprNode) n); } else { - throw new RuntimeException("OpArgNode not implemented jet"); + throw new RuntimeException("OpArgNode not implemented yet"); } } @@ -2098,7 +2098,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuil if (n instanceof ExprNode) { return visitExprNodeExpression((ExprNode) n); } else { - throw new RuntimeException("OpArgNode not implemented jet"); + throw new RuntimeException("OpArgNode not implemented yet"); } } -- GitLab