Refactoring of Alloy type mapping and interpretation.

4 files changed, 12 insertions, 135 deletions

diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
index 53674ca3..abedf9e4 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation.xtend
@@ -1,6 +1,7 @@
 package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder

 

 import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar

+import edu.mit.csail.sdg.alloy4compiler.ast.Sig

 import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field

 import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution

 import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation

@@ -20,123 +21,6 @@ import java.util.Map
 import java.util.Set

 

 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*

-import edu.mit.csail.sdg.alloy4compiler.ast.Sig

-import java.util.ArrayList

-

-interface AlloyModelInterpretation_TypeInterpretation {

-        def void resolveUnknownAtoms(

-                Iterable<ExprVar> objectAtoms, 

-                A4Solution solution,

-                Logic2AlloyLanguageMapperTrace forwardTrace,

-                Map<String, Sig> name2AlloySig,

-                Map<String, Field> name2AlloyField,

-                Map<String,DefinedElement> expression2DefinedElement,

-                Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType)

-}

-

-class AlloyModelInterpretation_TypeInterpretation_FilteredTypes implements AlloyModelInterpretation_TypeInterpretation{

-        protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE

-        

-        override resolveUnknownAtoms(

-                Iterable<ExprVar> objectAtoms, 

-                A4Solution solution,

-                Logic2AlloyLanguageMapperTrace forwardTrace,

-                Map<String, Sig> name2AlloySig,

-                Map<String, Field> name2AlloyField,

-                Map<String,DefinedElement> expression2DefinedElement,

-                Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType)

-        {

-                /*val Map<String,DefinedElement> expression2DefinedElement = new HashMap()

-                val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap;*/

-                

-                val typeTrace = forwardTrace.typeMapperTrace as Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes

-                

-                // 1. Evaluate the defined elements

-                for(definedElementMappingEntry : typeTrace.definedElement2Declaration.entrySet) {

-                        val name = definedElementMappingEntry.value.name

-                        val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig)

-                        val elementsOfSingletonSignature = solution.eval(matchingSig)

-                        if(elementsOfSingletonSignature.size != 1) {

-                                throw new IllegalArgumentException('''Defined element is unambigous: "«name»", possible values: «elementsOfSingletonSignature»!''')

-                        } else {

-                                val expressionOfDefinedElement  = elementsOfSingletonSignature.head.atom(0)// as ExprVar

-                                expression2DefinedElement.put(expressionOfDefinedElement, definedElementMappingEntry.key)

-                        }

-                }

-                

-                // 2. evaluate the signatures and create new elements if necessary

-                for(type2SingatureEntry : typeTrace.type2ALSType.entrySet) {

-                        val type = type2SingatureEntry.key

-                        if(type instanceof TypeDeclaration) {

-                                val name = type2SingatureEntry.value.name

-                                val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig)

-                                val elementsOfSignature = solution.eval(matchingSig)

-                                val elementList = new ArrayList(elementsOfSignature.size)

-                                var newVariableIndex = 1;

-                                for(elementOfSignature : elementsOfSignature) {

-                                        val expressionOfDefinedElement  = elementOfSignature.atom(0)

-                                        if(expression2DefinedElement.containsKey(expressionOfDefinedElement)) {

-                                                elementList += expressionOfDefinedElement.lookup(expression2DefinedElement)

-                                        } else {

-                                                val newElementName = '''newObject «newVariableIndex.toString»'''

-                                                val newRepresentation = createDefinedElement => [

-                                                        it.name = newElementName

-                                                ]

-                                                elementList += newRepresentation

-                                                expression2DefinedElement.put(expressionOfDefinedElement,newRepresentation)

-                                        }

-                                }

-                                interpretationOfUndefinedType.put(type,elementList)

-                        }

-                }

-        }

-}

-/*

-class AlloyModelInterpretation_TypeInterpretation_Horizontal implements AlloyModelInterpretation_TypeInterpretation{

-        protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE

-        

-        override resolveUnknownAtoms(Iterable<ExprVar> objectAtoms, Logic2AlloyLanguageMapperTrace forwardTrace, Map<String,DefinedElement> alloyAtom2LogicElement) {

-                val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap;

-                

-                //TMP sig maps to identify alloy signatures by their names

-                val Map<String,Type> sigName2LogicType =

-                        forwardTrace.type2ALSType.keySet.toMap[x|forwardTrace.type2ALSType.get(x).name]

-                //val Map<String,DefinedElement> elementNameNamel2DefinedElement = 

-                //      forwardTrace.definedElement2Declaration.keySet.toMap[x|forwardTrace.definedElement2Declaration.get(x).name]

-                        

-                // Fill the interpretation map with empty lists

-                forwardTrace.type2ALSType.keySet.filter(TypeDeclaration).forEach[x|interpretationOfUndefinedType.put(x,new LinkedList)]

-                

-                // exporing individuals

-                for(atom: objectAtoms) {

-                        val typeName = getName(atom.type)

-                        //val atomName = atom.name

-                        

-                        if(sigName2LogicType.containsKey(typeName)) {

-                                val type = sigName2LogicType.get(typeName)

-                                val elementsOfType = interpretationOfUndefinedType.get(type)

-                                val element = createDefinedElement => [

-                                        it.name += type.name

-                                        it.name += (elementsOfType.size+1).toString

-                                ]

-                                alloyAtom2LogicElement.put(atom.label,element)

-                                elementsOfType+=element

-                        }

-                        else throw new UnsupportedOperationException('''Unknown atom: «atom»''')

-                }

-                

-                return interpretationOfUndefinedType

-        }

-        

-        def private getName(edu.mit.csail.sdg.alloy4compiler.ast.Type type) {

-                val name = type.toString

-                if(name.startsWith("{this/") && name.endsWith("}")) {

-                        return type.toString.replaceFirst("\\{this\\/","").replace("}","")

-                }

-                else throw new IllegalArgumentException('''Unknown type format: "«name»"!''')

-        }

-        //def private getName(ExprVar atom) { atom.toString.split("\\$") }

-}*/

 

 class AlloyModelInterpretation implements LogicModelInterpretation{

         

diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend
index 9927f1cc..49268b42 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper.xtend
@@ -13,4 +13,6 @@ interface Logic2AlloyLanguageMapper_TypeMapper {
         def ALSSignatureDeclaration getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace)

         def int getUndefinedSupertypeScope(int undefinedScope,Logic2AlloyLanguageMapperTrace trace)

         def ALSTerm transformReference(DefinedElement referred,Logic2AlloyLanguageMapperTrace trace)

+        

+        def AlloyModelInterpretation_TypeInterpretation getTypeInterpreter()

 }

diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend
index ade9860b..3b2e3390 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend
@@ -18,13 +18,7 @@ import java.util.Map
 

 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*

 

-class Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes

-        implements Logic2AlloyLanguageMapper_TypeMapperTrace

-{

-        public var ALSSignatureDeclaration objectSupperClass;

-        public val Map<Type, ALSSignatureDeclaration> type2ALSType = new HashMap;

-        public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = new HashMap

-}

+

 /**

  * Each object is an element of an Object set, and types are subsets of the objects.

  */

@@ -265,4 +259,7 @@ class Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes implements Logic2AlloyL
                 return undefinedScope + trace.typeTrace.definedElement2Declaration.size

         }

         

+        override getTypeInterpreter() {

+                return new AlloyModelInterpretation_TypeInterpretation_FilteredTypes

+        }

 }
\ No newline at end of file
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend
index 92ac27df..be840e30 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend
@@ -2,24 +2,13 @@ package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
 

 import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity

 import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody

-import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration

 import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition

 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage

 import java.util.Collection

-import java.util.HashMap

 import java.util.LinkedList

-import java.util.List

-import java.util.Map

-

-class Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapperTrace {

-        public var ALSSignatureDeclaration objectSupperClass;

-        public val Map<Type, ALSSignatureDeclaration> type2ALSType = new HashMap;

-        public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = new HashMap

-        public val Map<Type, List<ALSSignatureDeclaration>> typeSelection = new HashMap 

-}

 

 class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapper{

         private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE

@@ -125,4 +114,9 @@ class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements L
         override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) {

                 return undefinedScope + trace.typeTrace.definedElement2Declaration.size

         }

+        

+        override getTypeInterpreter() {

+                return new AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal

+        }

+        

 }
\ No newline at end of file