From 9643b7b7a735afc408ca6a172e2719653553627a Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Mon, 4 Mar 2019 17:31:16 -0500 Subject: Begin handing of scope and fix type definitions. --- ...ireLanguageMapper_TypeMapper_FilteredTypes.java | 95 +++++++--------------- 1 file changed, 28 insertions(+), 67 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java') diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java index 0f5e4e7a..71e98871 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper_FilteredTypes.java @@ -7,7 +7,6 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguage import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation_TypeInterpretation; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; -import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; @@ -27,10 +26,10 @@ import java.util.ArrayList; import java.util.Collection; import java.util.List; 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.IterableExtensions; -import org.eclipse.xtext.xbase.lib.ListExtensions; import org.eclipse.xtext.xbase.lib.ObjectExtensions; import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; @@ -58,14 +57,10 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log { VLSFunction _createVLSFunction = this.factory.createVLSFunction(); final Procedure1 _function_1 = (VLSFunction it) -> { - it.setConstant(this.support.toIDMultiple("type", type.getName())); + it.setConstant(this.support.toIDMultiple("t", type.getName())); EList _terms = it.getTerms(); - VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); - final Procedure1 _function_2 = (VLSVariable it_1) -> { - it_1.setName(variable.getName()); - }; - VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_2); - _terms.add(_doubleArrow); + VLSVariable _duplicate = this.support.duplicate(variable); + _terms.add(_duplicate); }; final VLSFunction typePred = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); typeTrace.type2Predicate.put(type, typePred); @@ -74,6 +69,22 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log Iterable _filter = Iterables.filter(types, TypeDefinition.class); for (final TypeDefinition type_1 : _filter) { { + final List orElems = CollectionLiterals.newArrayList(); + EList _elements = type_1.getElements(); + for (final DefinedElement e : _elements) { + { + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function_1 = (VLSFunction it) -> { + it.setConstant(this.support.toIDMultiple("e", e.getName(), type_1.getName())); + EList _terms = it.getTerms(); + VLSVariable _duplicate = this.support.duplicate(variable); + _terms.add(_duplicate); + }; + final VLSFunction enumElemPred = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_1); + typeTrace.element2Predicate.put(e, enumElemPred); + orElems.add(enumElemPred); + } + } VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); final Procedure1 _function_1 = (VLSFofFormula it) -> { it.setName(this.support.toIDMultiple("typeDef", type_1.getName())); @@ -81,53 +92,15 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); final Procedure1 _function_2 = (VLSUniversalQuantifier it_1) -> { EList _variables = it_1.getVariables(); - VLSVariable _createVLSVariable_1 = this.factory.createVLSVariable(); - final Procedure1 _function_3 = (VLSVariable it_2) -> { - it_2.setName(variable.getName()); - }; - VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable_1, _function_3); - _variables.add(_doubleArrow); + VLSVariable _duplicate = this.support.duplicate(variable); + _variables.add(_duplicate); VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); - final Procedure1 _function_4 = (VLSEquivalent it_2) -> { - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function_5 = (VLSFunction it_3) -> { - it_3.setConstant(CollectionsUtil.lookup(type_1, typeTrace.type2Predicate).getConstant()); - EList _terms = it_3.getTerms(); - VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable(); - final Procedure1 _function_6 = (VLSVariable it_4) -> { - it_4.setName("A"); - }; - VLSVariable _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSVariable_2, _function_6); - _terms.add(_doubleArrow_1); - }; - VLSFunction _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_5); - it_2.setLeft(_doubleArrow_1); - CollectionsUtil.lookup(type_1, typeTrace.type2Predicate); - final Function1 _function_6 = (DefinedElement e) -> { - VLSEquality _createVLSEquality = this.factory.createVLSEquality(); - final Procedure1 _function_7 = (VLSEquality it_3) -> { - VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable(); - final Procedure1 _function_8 = (VLSVariable it_4) -> { - it_4.setName(variable.getName()); - }; - VLSVariable _doubleArrow_2 = ObjectExtensions.operator_doubleArrow(_createVLSVariable_2, _function_8); - it_3.setLeft(_doubleArrow_2); - VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote(); - final Procedure1 _function_9 = (VLSDoubleQuote it_4) -> { - String _name = e.getName(); - String _plus = ("\"a" + _name); - String _plus_1 = (_plus + "\""); - it_4.setValue(_plus_1); - }; - VLSDoubleQuote _doubleArrow_3 = ObjectExtensions.operator_doubleArrow(_createVLSDoubleQuote, _function_9); - it_3.setRight(_doubleArrow_3); - }; - return ObjectExtensions.operator_doubleArrow(_createVLSEquality, _function_7); - }; - it_2.setRight(this.support.unfoldOr(ListExtensions.map(type_1.getElements(), _function_6))); + final Procedure1 _function_3 = (VLSEquivalent it_2) -> { + it_2.setLeft(CollectionsUtil.lookup(type_1, typeTrace.type2Predicate)); + it_2.setRight(this.support.unfoldOr(orElems)); }; - VLSEquivalent _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_4); - it_1.setOperand(_doubleArrow_1); + VLSEquivalent _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSEquivalent, _function_3); + it_1.setOperand(_doubleArrow); }; VLSUniversalQuantifier _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); it.setFofFormula(_doubleArrow); @@ -201,19 +174,7 @@ public class Logic2VampireLanguageMapper_TypeMapper_FilteredTypes implements Log _variables.add(_doubleArrow); VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); final Procedure1 _function_5 = (VLSEquivalent it_2) -> { - VLSFunction _createVLSFunction = this.factory.createVLSFunction(); - final Procedure1 _function_6 = (VLSFunction it_3) -> { - it_3.setConstant("object"); - EList _terms = it_3.getTerms(); - VLSVariable _createVLSVariable_2 = this.factory.createVLSVariable(); - final Procedure1 _function_7 = (VLSVariable it_4) -> { - it_4.setName("A"); - }; - VLSVariable _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSVariable_2, _function_7); - _terms.add(_doubleArrow_1); - }; - VLSFunction _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function_6); - it_2.setLeft(_doubleArrow_1); + it_2.setLeft(this.support.topLevelTypeFunc()); Collection _values = typeTrace.type2And.values(); ArrayList _arrayList = new ArrayList(_values); it_2.setRight(this.support.unfoldOr(_arrayList)); -- cgit v1.2.3-54-g00ecf