refactor BAstCreator again

- replace duplicate AST auxiliary methods by those of the ASTBuilder of probparsers
- create external function definitions directly in UsedExternalFunctions
- further minor simplifications

src/main/java/de/tla2b/analysis/BOperation.java

@@ -58,7 +58,7 @@ public class BOperation extends BuiltInOPs {
 		List<PExpression> lhsAssignment = new ArrayList<>();
 		List<PExpression> rhsAssignment = new ArrayList<>();
 		assignments.forEach((id, assignExpr) -> {
-			lhsAssignment.add(bASTCreator.createIdentifierNode(id));
+			lhsAssignment.add(bASTCreator.createIdentifierFromNode(id));
 			rhsAssignment.add(bASTCreator.visitExprOrOpArgNodeExpression(assignExpr));
 		});
 
@@ -70,7 +70,7 @@ public class BOperation extends BuiltInOPs {
 				AIdentifierExpression nextName = createIdentifier(var.getName().toString() + "_n");
 				anyParams.add(nextName);
 				whereList.add(new AMemberPredicate(nextName.clone(), TypeChecker.getType(var).getBNode()));
-				lhsAssignment.add(bASTCreator.createIdentifierNode(var));
+				lhsAssignment.add(bASTCreator.createIdentifierFromNode(var));
 				rhsAssignment.add(nextName.clone());
 			}
 			whereList.addAll(createBeforeAfterPredicates(bASTCreator));
@@ -94,7 +94,7 @@ public class BOperation extends BuiltInOPs {
 
 		return new AOperation(new LinkedList<>(),
 				bASTCreator.createPositionedTIdentifierLiteral(name, getNode()),
-				this.getFormalParams().stream().map(bASTCreator::createIdentifierNode).collect(Collectors.toList()),
+				this.getFormalParams().stream().map(bASTCreator::createIdentifierFromNode).collect(Collectors.toList()),
 				operationBody
 		);
 	}

src/main/java/de/tla2b/analysis/UsedExternalFunctions.java

 package de.tla2b.analysis;
 
+import de.be4.classicalb.core.parser.Definitions;
+import de.be4.classicalb.core.parser.IDefinitions;
 import de.tla2b.global.BBuildIns;
 import de.tla2b.global.BBuiltInOPs;
 import tla2sany.semantic.*;
@@ -7,22 +9,26 @@ import tla2sany.semantic.*;
 import java.util.HashSet;
 import java.util.Set;
 
-public class UsedExternalFunctions extends AbstractASTVisitor implements BBuildIns {
+import static de.be4.classicalb.core.parser.util.ASTBuilder.*;
 
-	public enum EXTERNAL_FUNCTIONS {
-		CHOOSE, ASSERT
-	}
+public class UsedExternalFunctions extends AbstractASTVisitor implements BBuildIns {
 
-	private final Set<EXTERNAL_FUNCTIONS> usedExternalFunctions;
+	private final Set<String> usedExternalFunctions = new HashSet<>();
 
-	public Set<EXTERNAL_FUNCTIONS> getUsedExternalFunctions() {
-		return usedExternalFunctions;
+	public static IDefinitions createDefinitions(SpecAnalyser specAnalyser) {
+		UsedExternalFunctions externalFunctions = new UsedExternalFunctions(specAnalyser);
+		IDefinitions definitions = new Definitions();
+		if (externalFunctions.usedExternalFunctions.contains(CHOOSE)) {
+			addChooseDefinition(definitions);
+		}
+		if (externalFunctions.usedExternalFunctions.contains(ASSERT_TRUE)) {
+			addAssertTrueDefinition(definitions);
+		}
+		return definitions;
 	}
 
-	public UsedExternalFunctions(ModuleNode moduleNode, SpecAnalyser specAnalyser) {
-		usedExternalFunctions = new HashSet<>();
-		visitAssumptions(moduleNode.getAssumptions());
-
+	private UsedExternalFunctions(SpecAnalyser specAnalyser) {
+		visitAssumptions(specAnalyser.getModuleNode().getAssumptions());
 		for (OpDefNode def : specAnalyser.getUsedDefinitions()) {
 			visitDefinition(def);
 		}
@@ -34,7 +40,7 @@ public class UsedExternalFunctions extends AbstractASTVisitor implements BBuildI
 			case OPCODE_case:
 			case OPCODE_uc:
 			case OPCODE_bc: {
-				usedExternalFunctions.add(EXTERNAL_FUNCTIONS.CHOOSE);
+				usedExternalFunctions.add(CHOOSE);
 			}
 			default:
 		}
@@ -56,7 +62,7 @@ public class UsedExternalFunctions extends AbstractASTVisitor implements BBuildI
 	@Override
 	public void visitBBuiltinsNode(OpApplNode n) {
 		if (BBuiltInOPs.getOpcode(n.getOperator().getName()) == B_OPCODE_assert) {
-			usedExternalFunctions.add(EXTERNAL_FUNCTIONS.ASSERT);
+			usedExternalFunctions.add(ASSERT_TRUE);
 		}
 
 		for (ExprNode exprNode : n.getBdedQuantBounds()) {

src/main/java/de/tla2bAst/Translator.java

 package de.tla2bAst;
 
 import de.be4.classicalb.core.parser.BParser;
-import de.be4.classicalb.core.parser.Definitions;
+import de.be4.classicalb.core.parser.IDefinitions;
 import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader;
 import de.be4.classicalb.core.parser.exceptions.BCompoundException;
 import de.be4.classicalb.core.parser.exceptions.PreParseException;
@@ -277,7 +277,7 @@ public class Translator {
 		return translateExpressionWithoutModel(tlaExpression);
 	}
 
-	public Definitions getBDefinitions() {
+	public IDefinitions getBDefinitions() {
 		return bAstCreator.getBDefinitions();
 	}