aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java')
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java183
1 files changed, 175 insertions, 8 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
index c55e2421..d3dddcfc 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
@@ -2,24 +2,191 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder;
2 2
3import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; 3import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper;
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; 4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace;
5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation_TypeInterpretation; 5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support;
6import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote;
7import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent;
8import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula;
9import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction;
6import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; 10import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
11import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUnaryNegation;
12import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;
13import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;
14import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;
15import com.google.common.base.Objects;
16import com.google.common.collect.Iterables;
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; 17import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement;
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; 18import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
19import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition;
20import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage;
21import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;
22import java.util.ArrayList;
9import java.util.Collection; 23import java.util.Collection;
10import java.util.List; 24import java.util.List;
25import org.eclipse.emf.common.util.EList;
26import org.eclipse.xtext.xbase.lib.CollectionLiterals;
27import org.eclipse.xtext.xbase.lib.Extension;
28import org.eclipse.xtext.xbase.lib.Functions.Function1;
29import org.eclipse.xtext.xbase.lib.IterableExtensions;
30import org.eclipse.xtext.xbase.lib.ObjectExtensions;
31import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
11 32
12@SuppressWarnings("all") 33@SuppressWarnings("all")
13public interface Logic2VampireLanguageMapper_TypeMapper { 34public class Logic2VampireLanguageMapper_TypeMapper {
14 public abstract void transformTypes(final Collection<Type> types, final Collection<DefinedElement> elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace); 35 @Extension
36 private final VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE;
15 37
16 public abstract List<VLSTerm> transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace); 38 private final Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support();
17 39
18 public abstract VLSTerm getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace); 40 private final Logic2VampireLanguageMapper base;
19 41
20 public abstract int getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace); 42 public Logic2VampireLanguageMapper_TypeMapper(final Logic2VampireLanguageMapper base) {
43 LogicproblemPackage.eINSTANCE.getClass();
44 this.base = base;
45 }
21 46
22 public abstract VLSTerm transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace); 47 protected boolean transformTypes(final Collection<Type> types, final Collection<DefinedElement> elements, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) {
48 boolean _xblockexpression = false;
49 {
50 VLSVariable _createVLSVariable = this.factory.createVLSVariable();
51 final Procedure1<VLSVariable> _function = (VLSVariable it) -> {
52 it.setName("A");
53 };
54 final VLSVariable variable = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);
55 for (final Type type : types) {
56 {
57 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
58 final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> {
59 it.setConstant(this.support.toIDMultiple("t", type.getName().split(" ")[0]));
60 EList<VLSTerm> _terms = it.getTerms();
61 VLSVariable _duplicate = this.support.duplicate(variable);
62 _terms.add(_duplicate);
63 };
64 final VLSFunction typePred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);
65 trace.type2Predicate.put(type, typePred);
66 }
67 }
68 Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class);
69 for (final TypeDefinition type_1 : _filter) {
70 {
71 final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList();
72 EList<DefinedElement> _elements = type_1.getElements();
73 for (final DefinedElement e : _elements) {
74 {
75 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
76 final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> {
77 it.setConstant(this.support.toIDMultiple("e", e.getName().split(" ")[0], e.getName().split(" ")[2]));
78 EList<VLSTerm> _terms = it.getTerms();
79 VLSVariable _duplicate = this.support.duplicate(variable);
80 _terms.add(_duplicate);
81 };
82 final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1);
83 trace.element2Predicate.put(e, enumElemPred);
84 orElems.add(enumElemPred);
85 }
86 }
87 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
88 final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> {
89 it.setName(this.support.toIDMultiple("typeDef", type_1.getName().split(" ")[0]));
90 it.setFofRole("axiom");
91 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
92 final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> {
93 EList<VLSVariable> _variables = it_1.getVariables();
94 VLSVariable _duplicate = this.support.duplicate(variable);
95 _variables.add(_duplicate);
96 VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
97 final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> {
98 it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate));
99 it_2.setRight(this.support.unfoldOr(orElems));
100 };
101 VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3);
102 it_1.setOperand(_doubleArrow);
103 };
104 VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2);
105 it.setFofFormula(_doubleArrow);
106 };
107 final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1);
108 EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
109 _formulas.add(res);
110 }
111 }
112 final Function1<Type, Boolean> _function_1 = (Type it) -> {
113 boolean _isIsAbstract = it.isIsAbstract();
114 return Boolean.valueOf((!_isIsAbstract));
115 };
116 Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_1);
117 for (final Type t1 : _filter_1) {
118 {
119 for (final Type t2 : types) {
120 if ((Objects.equal(t1, t2) || this.support.dfsSupertypeCheck(t1, t2))) {
121 trace.type2PossibleNot.put(t2, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate)));
122 } else {
123 VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();
124 final Procedure1<VLSUnaryNegation> _function_2 = (VLSUnaryNegation it) -> {
125 it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate)));
126 };
127 VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2);
128 trace.type2PossibleNot.put(t2, _doubleArrow);
129 }
130 }
131 Collection<VLSTerm> _values = trace.type2PossibleNot.values();
132 ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values);
133 trace.type2And.put(t1, this.support.unfoldAnd(_arrayList));
134 trace.type2PossibleNot.clear();
135 }
136 }
137 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
138 final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> {
139 it.setName("hierarchyHandler");
140 it.setFofRole("axiom");
141 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
142 final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> {
143 EList<VLSVariable> _variables = it_1.getVariables();
144 VLSVariable _duplicate = this.support.duplicate(variable);
145 _variables.add(_duplicate);
146 VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
147 final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> {
148 it_2.setLeft(this.support.topLevelTypeFunc());
149 Collection<VLSTerm> _values = trace.type2And.values();
150 ArrayList<VLSTerm> _arrayList = new ArrayList<VLSTerm>(_values);
151 it_2.setRight(this.support.unfoldOr(_arrayList));
152 };
153 VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4);
154 it_1.setOperand(_doubleArrow);
155 };
156 VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_3);
157 it.setFofFormula(_doubleArrow);
158 };
159 final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2);
160 EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
161 _xblockexpression = _formulas.add(hierarch);
162 }
163 return _xblockexpression;
164 }
23 165
24 public abstract VampireModelInterpretation_TypeInterpretation getTypeInterpreter(); 166 protected void transformTypeReference(final Type referred, final Logic2VampireLanguageMapper mapper, final Logic2VampireLanguageMapperTrace trace) {
167 throw new UnsupportedOperationException("TODO: auto-generated method stub");
168 }
169
170 protected void getUndefinedSupertype(final Logic2VampireLanguageMapperTrace trace) {
171 throw new UnsupportedOperationException("TODO: auto-generated method stub");
172 }
173
174 protected void getUndefinedSupertypeScope(final int undefinedScope, final Logic2VampireLanguageMapperTrace trace) {
175 throw new UnsupportedOperationException("TODO: auto-generated method stub");
176 }
177
178 protected VLSDoubleQuote transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) {
179 VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote();
180 final Procedure1<VLSDoubleQuote> _function = (VLSDoubleQuote it) -> {
181 String _name = referred.getName();
182 String _plus = ("\"a" + _name);
183 String _plus_1 = (_plus + "\"");
184 it.setValue(_plus_1);
185 };
186 return ObjectExtensions.<VLSDoubleQuote>operator_doubleArrow(_createVLSDoubleQuote, _function);
187 }
188
189 protected void getTypeInterpreter() {
190 throw new UnsupportedOperationException("TODO: auto-generated method stub");
191 }
25} 192}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-29 10:18:01 +0000