From 8bd7cc4cec30fde0b4674b2fc9e1c5e8ef306513 Mon Sep 17 00:00:00 2001
From: Oszkar Semerath <semerath@mit.bme.hu>
Date: Fri, 30 Aug 2019 17:07:28 +0200
Subject: Type Interpretation for Alloy with Inheritance+Horizontal mapping

---
 ...peInterpretation_InheritanceAndHorizontal.xtend | 63 ++++++++++++++++++++--
 1 file changed, 58 insertions(+), 5 deletions(-)

diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend
index 8019c6b5..ac75b2a1 100644
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend
+++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend
@@ -1,20 +1,73 @@
 package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
 
 import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar
-import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution
-import java.util.Map
 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.logiclanguage.DefinedElement
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
+import java.util.ArrayList
 import java.util.List
-import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
+import java.util.Map
+
+import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
 
 class AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal 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) {
-		throw new UnsupportedOperationException("TODO: auto-generated method stub")
+	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_InheritanceAndHorizontal
+		
+		// 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)
+			}
+		}
 	}
 	
 }
\ No newline at end of file
-- 
cgit v1.2.3-54-g00ecf