1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
|
package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;
import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;
import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support;
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant;
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality;
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies;
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;
import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;
import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration;
import java.util.ArrayList;
import org.eclipse.emf.common.util.EList;
import org.eclipse.xtext.xbase.lib.CollectionLiterals;
import org.eclipse.xtext.xbase.lib.Extension;
import org.eclipse.xtext.xbase.lib.Functions.Function1;
import org.eclipse.xtext.xbase.lib.ListExtensions;
import org.eclipse.xtext.xbase.lib.ObjectExtensions;
import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
@SuppressWarnings("all")
public class Logic2VampireLanguageMapper_ScopeMapper {
@Extension
private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;
private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();
private final Logic2VampireLanguageMapper base;
public Logic2VampireLanguageMapper_ScopeMapper(final Logic2VampireLanguageMapper base) {
this.base = base;
}
public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {
VLSVariable _createVLSVariable = this.factory.createVLSVariable();
final Procedure1<VLSVariable> _function = (VLSVariable it) -> {
it.setName("A");
};
final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);
final ArrayList<VLSTerm> localInstances = CollectionLiterals.<VLSTerm>newArrayList();
for (int i = 0; (i < config.typeScopes.minNewElements); i++) {
{
final int num = (i + 1);
VLSConstant _createVLSConstant = this.factory.createVLSConstant();
final Procedure1<VLSConstant> _function_1 = (VLSConstant it) -> {
it.setName(("o" + Integer.valueOf(num)));
};
final VLSConstant cst = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_1);
trace.uniqueInstances.add(cst);
localInstances.add(cst);
}
}
if ((config.typeScopes.minNewElements != 0)) {
VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> {
it.setName("typeScope");
it.setFofRole("axiom");
VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> {
EList<VLSVariable> _variables = it_1.getVariables();
VLSVariable _duplicate = this.support.duplicate(variable);
_variables.add(_duplicate);
VLSImplies _createVLSImplies = this.factory.createVLSImplies();
final Procedure1<VLSImplies> _function_3 = (VLSImplies it_2) -> {
final Function1<VLSTerm, VLSEquality> _function_4 = (VLSTerm i) -> {
VLSEquality _createVLSEquality = this.factory.createVLSEquality();
final Procedure1<VLSEquality> _function_5 = (VLSEquality it_3) -> {
VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable();
final Procedure1<VLSVariable> _function_6 = (VLSVariable it_4) -> {
it_4.setName(variable.getName());
};
VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_1, _function_6);
it_3.setLeft(_doubleArrow);
it_3.setRight(i);
};
return ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_5);
};
it_2.setLeft(this.support.unfoldOr(ListExtensions.<VLSTerm, VLSEquality>map(localInstances, _function_4)));
it_2.setRight(this.support.topLevelTypeFunc());
};
VLSImplies _doubleArrow = ObjectExtensions.<VLSImplies>operator_doubleArrow(_createVLSImplies, _function_3);
it_1.setOperand(_doubleArrow);
};
VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2);
it.setFofFormula(_doubleArrow);
};
final VLSFofFormula cstDec = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1);
EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
_formulas.add(cstDec);
VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> {
it.setName("typeUniqueness");
it.setFofRole("axiom");
it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances));
};
final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_2);
EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas();
_formulas_1.add(uniqueness);
}
}
public void transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {
_transformScope(config, trace);
return;
}
}
|
