diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-05 13:37:02 -0500 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-03-05 13:37:02 -0500 |
commit | df12163128073296c4d811fa67b02e37ceb20179 (patch) | |
tree | 7509fdd478d6ff3d908d0ab5aa39ed9a8260f0b0 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java | |
parent | Begin handing of scope and fix type definitions. (diff) | |
download | VIATRA-Generator-df12163128073296c4d811fa67b02e37ceb20179.tar.gz VIATRA-Generator-df12163128073296c4d811fa67b02e37ceb20179.tar.zst VIATRA-Generator-df12163128073296c4d811fa67b02e37ceb20179.zip |
Implement type scope handling
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java | 36 |
1 files changed, 34 insertions, 2 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java index b111732f..dfe624be 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java | |||
@@ -3,6 +3,7 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | 3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; |
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; | 5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; |
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | ||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; |
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; |
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | 9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; |
@@ -25,6 +26,7 @@ import java.util.List; | |||
25 | import java.util.Map; | 26 | import java.util.Map; |
26 | import org.eclipse.emf.common.util.EList; | 27 | import org.eclipse.emf.common.util.EList; |
27 | import org.eclipse.xtend2.lib.StringConcatenation; | 28 | import org.eclipse.xtend2.lib.StringConcatenation; |
29 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
28 | import org.eclipse.xtext.xbase.lib.Conversions; | 30 | import org.eclipse.xtext.xbase.lib.Conversions; |
29 | import org.eclipse.xtext.xbase.lib.ExclusiveRange; | 31 | import org.eclipse.xtext.xbase.lib.ExclusiveRange; |
30 | import org.eclipse.xtext.xbase.lib.Extension; | 32 | import org.eclipse.xtext.xbase.lib.Extension; |
@@ -73,6 +75,36 @@ public class Logic2VampireLanguageMapper_Support { | |||
73 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | 75 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); |
74 | } | 76 | } |
75 | 77 | ||
78 | public VLSTerm establishUniqueness(final List<VLSConstant> terms) { | ||
79 | final List<VLSInequality> eqs = CollectionLiterals.<VLSInequality>newArrayList(); | ||
80 | List<VLSConstant> _subList = terms.subList(1, ((Object[])Conversions.unwrapArray(terms, Object.class)).length); | ||
81 | for (final VLSConstant t1 : _subList) { | ||
82 | List<VLSConstant> _subList_1 = terms.subList(0, terms.indexOf(t1)); | ||
83 | for (final VLSConstant t2 : _subList_1) { | ||
84 | { | ||
85 | VLSInequality _createVLSInequality = this.factory.createVLSInequality(); | ||
86 | final Procedure1<VLSInequality> _function = (VLSInequality it) -> { | ||
87 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
88 | final Procedure1<VLSConstant> _function_1 = (VLSConstant it_1) -> { | ||
89 | it_1.setName(t2.getName()); | ||
90 | }; | ||
91 | VLSConstant _doubleArrow = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function_1); | ||
92 | it.setLeft(_doubleArrow); | ||
93 | VLSConstant _createVLSConstant_1 = this.factory.createVLSConstant(); | ||
94 | final Procedure1<VLSConstant> _function_2 = (VLSConstant it_1) -> { | ||
95 | it_1.setName(t1.getName()); | ||
96 | }; | ||
97 | VLSConstant _doubleArrow_1 = ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant_1, _function_2); | ||
98 | it.setRight(_doubleArrow_1); | ||
99 | }; | ||
100 | final VLSInequality eq = ObjectExtensions.<VLSInequality>operator_doubleArrow(_createVLSInequality, _function); | ||
101 | eqs.add(eq); | ||
102 | } | ||
103 | } | ||
104 | } | ||
105 | return this.unfoldAnd(eqs); | ||
106 | } | ||
107 | |||
76 | protected VLSTerm unfoldAnd(final List<? extends VLSTerm> operands) { | 108 | protected VLSTerm unfoldAnd(final List<? extends VLSTerm> operands) { |
77 | int _size = operands.size(); | 109 | int _size = operands.size(); |
78 | boolean _equals = (_size == 1); | 110 | boolean _equals = (_size == 1); |
@@ -180,7 +212,7 @@ public class Logic2VampireLanguageMapper_Support { | |||
180 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 212 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
181 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | 213 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { |
182 | TypeReference _range = variable.getRange(); | 214 | TypeReference _range = variable.getRange(); |
183 | it.setConstant(this.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); | 215 | it.setConstant(this.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); |
184 | EList<VLSTerm> _terms = it.getTerms(); | 216 | EList<VLSTerm> _terms = it.getTerms(); |
185 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 217 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); |
186 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { | 218 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { |
@@ -229,7 +261,7 @@ public class Logic2VampireLanguageMapper_Support { | |||
229 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 261 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
230 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { | 262 | final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { |
231 | TypeReference _range = variable.getRange(); | 263 | TypeReference _range = variable.getRange(); |
232 | it.setConstant(this.toIDMultiple("type", ((ComplexTypeReference) _range).getReferred().getName())); | 264 | it.setConstant(this.toIDMultiple("t", ((ComplexTypeReference) _range).getReferred().getName())); |
233 | EList<VLSTerm> _terms = it.getTerms(); | 265 | EList<VLSTerm> _terms = it.getTerms(); |
234 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); | 266 | VLSVariable _createVLSVariable = this.factory.createVLSVariable(); |
235 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { | 267 | final Procedure1<VLSVariable> _function_2 = (VLSVariable it_1) -> { |