aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend
blob: 4d7b50e8d2dc2fe6df103da28c1fb6e728b53cad (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
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
	private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
	
	new() {
		LogicproblemPackage.eINSTANCE.class
	}
	
	override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
		if(types.exists[hasDefinedSupertype]) {
			throw new UnsupportedOperationException('''Defined supertype is not supported by this type mapping!''')
		} else {
			
			val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal
			trace.typeMapperTrace = typeTrace
			
			// 1. A global type for Objects is created
			val objectSig = createALSSignatureDeclaration => [it.name = support.toID(#["util","Object"])]
			val objectBody = createALSSignatureBody => [
				it.declarations += objectSig
				it.abstract = true
			]
			typeTrace.objectSupperClass = objectSig
			trace.specification.signatureBodies += objectBody
			
			// 2. Each type is mapped to a unique sig
			for(type : types) {
				val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple("type",type.name)]
				val body = createALSSignatureBody => [it.declarations += sig]
				body.abstract = type.isIsAbstract || (type instanceof TypeDefinition)
				
				trace.specification.signatureBodies += body
				typeTrace.type2ALSType.put(type,sig)
				
				if(type instanceof TypeDefinition) {
					val elementContainer = createALSSignatureBody => [it.multiplicity = ALSMultiplicity::ONE it.supertype = sig]
					for(element : type.elements) {
						val signature = createALSSignatureDeclaration => [it.name = support.toIDMultiple("element",element.name)]
						elementContainer.declarations += signature
						
					}
					trace.specification.signatureBodies += elementContainer
				}
				
				typeTrace.typeSelection.put(type,new LinkedList()=>[add(sig)])
			}
			
			// 6. Each inheritance is modeled by extend keyword
			for(type : types) {
				if(type.supertypes.size == 1) {
					val alsType = typeTrace.type2ALSType.get(type.supertypes.head)
					(type.eContainer as ALSSignatureBody).supertype = alsType
				} else if(type.supertypes.size > 1){
					val alsMainType = typeTrace.type2ALSType.get(type.supertypes.head)
					(type.eContainer as ALSSignatureBody).supertype = alsMainType
					for(otherType : type.supertypes.filter[it != alsMainType]) {
						typeTrace.typeSelection.get(otherType).add(typeTrace.type2ALSType.get(otherType))
					}
				}
			}
				
		}
	}
	
	private def boolean hasDefinedSupertype(Type type) {
		if(type instanceof TypeDefinition) {
			return true
		} else {
			if(type.supertypes.empty) return false
			else return type.supertypes.exists[it.hasDefinedSupertype]
		}
	}
	
	def getTypeTrace(Logic2AlloyLanguageMapperTrace trace) {
		val res = trace.typeMapperTrace
		if(res instanceof Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal) {
			return res
		} else {
			throw new IllegalArgumentException('''
			Expected type mapping trace: «Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.name»,
			but found «res.class.name»''')
		}
	}
	
	override transformTypeReference(Type referred, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
		trace.typeTrace.typeSelection.get(referred)
	}
	
	override getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) {
		trace.typeTrace.objectSupperClass
	}
	
	override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) {
		createALSReference => [it.referred = trace.typeTrace.definedElement2Declaration.get(referred)]
	}
	
	override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) {
		return undefinedScope + trace.typeTrace.definedElement2Declaration.size
	}
}