aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers
diff options
context:
space:
mode:
authorLibravatar OszkarSemerath <oszka@192.168.122.1>2017-08-21 00:38:15 +0200
committerLibravatar OszkarSemerath <oszka@192.168.122.1>2017-08-21 00:38:15 +0200
commita119a0edd2883f64bab54fe552c40bd46c4a8885 (patch)
treea0f761b30ba0320f7341f71b29e4af13a3b25a80 /Solvers
parentAlloy Examples (diff)
downloadVIATRA-Generator-a119a0edd2883f64bab54fe552c40bd46c4a8885.tar.gz
VIATRA-Generator-a119a0edd2883f64bab54fe552c40bd46c4a8885.tar.zst
VIATRA-Generator-a119a0edd2883f64bab54fe552c40bd46c4a8885.zip
simple typemapper for alloy
Diffstat (limited to 'Solvers')
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_Horizontal.xtend_old428
-rw-r--r--Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal.xtend99
2 files changed, 86 insertions, 441 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_Horizontal.xtend_old b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_Horizontal.xtend_old
deleted file mode 100644
index 7383904d..00000000
--- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_Horizontal.xtend_old
+++ /dev/null
@@ -1,428 +0,0 @@
1package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
2
3import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSIntersection
4import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity
5import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration
6import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm
7import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
10import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
13import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
14import hu.bme.mit.inf.dslreasoner.logic.model.patterns.SupertypeStarMatcher
15import java.util.HashMap
16import java.util.LinkedHashSet
17import java.util.LinkedList
18import java.util.List
19import java.util.Map
20import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
21import org.eclipse.viatra.query.runtime.emf.EMFScope
22import org.eclipse.xtend.lib.annotations.Data
23
24import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
25
26class Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal
27 implements Logic2AlloyLanguageMapper_TypeMapperTrace {
28 public var ALSSignatureDeclaration declaredSupertype
29 public var ALSSignatureDeclaration definedSupertype
30 public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = new HashMap
31
32 public val Map<TypeDefinition, ALSSignatureDeclaration> definition2definition = new HashMap
33 public val Map<TypeDeclaration, ALSSignatureDeclaration> declaration2definition = new HashMap
34 public val Map<TypeDeclaration, ALSSignatureDeclaration> undefined2definition = new HashMap
35 public val Map<TypeDeclaration, ALSSignatureDeclaration> new2declaration = new HashMap
36
37 def getAllDefinedTypes() {
38 return (definition2definition.values) +
39 (declaration2definition.values) +
40 (undefined2definition.values)
41 }
42 def getAllDeclaredTypes() {
43 return new2declaration.values
44 }
45
46 public val Map<Type,List<ALSSignatureDeclaration>> type2AllSignatures = new HashMap;
47}
48
49@Data
50class DynamicTypeConstraints {
51 List<List<Type>> positiveCNF
52 LinkedHashSet<Type> negative
53 public new() {
54 this.positiveCNF = new LinkedList
55 this.negative = new LinkedHashSet
56 }
57 def public void addPositiveTypeOptions(List<Type> typeDisjunction) {
58 this.positiveCNF.add(typeDisjunction)
59 }
60 def public void addNegativeTypes(Iterable<Type> negativeTypes) {
61 this.negative.addAll(negativeTypes)
62 }
63}
64
65/**
66 * Dynamic types are represented by disjoint sets, and
67 * static types are represented by the union of the dynamic type sets.
68 *
69 * Definition Declaration
70 * | / \
71 * | W/DefinedSuper Wo/DefinedSuper
72 * | | / \
73 * | | undefined2declaration new2declaration
74 * definition2definition definition2declaration
75 * +----------------------------------------------------+ +-------------+
76 * Defined Declared
77 */
78class Logic2AlloyLanguageMapper_TypeMapper_Horizontal implements Logic2AlloyLanguageMapper_TypeMapper{
79 private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
80 private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
81
82 override transformTypes(LogicProblem problem, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
83 // 0. Creating the traces
84 val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal
85 trace.typeMapperTrace = typeTrace
86 /**
87 * Static type -> list of possible dynamic type map
88 */
89 val typeToConcreteSubtypes = problem.typeToConcreteSubtypes(trace)
90
91
92
93 // 1. Transforming the types
94
95 // There are two kind of types:
96 // A: one with defined supertypes (including itself), that only has defined elements
97 // Those types can have instances only from the defined elements, ie they are subset of problem.elements
98 // B: one without defined supertypes
99 // Those types can have instances from two sources
100 // B.1 from elements that dont have definitions
101 // B.2 from newly created elements
102 val allConcreteTypes = problem.types.filter[!it.isAbstract]
103 val definitions = allConcreteTypes.filter(TypeDefinition).toList
104 val declarationsWithDefinedSupertype = allConcreteTypes.filter(TypeDeclaration).filter[it.hasDefinedSupertype].toList
105 val declarationsWithoutDefinedSupertype = allConcreteTypes.filter(TypeDeclaration).filter[!it.hasDefinedSupertype].toList
106
107 // 2. If there are defined elements
108 if(trace.typeTrace.definedSupertype != null) {
109 // 3 mapping the elements
110 problem.elements.transformDefinedSupertype(trace)
111 // 4. if there are elements that are added to types, then it have to be mapped to defined parts
112 if(problem.elements.exists[!it.definedInType.empty]) {
113 definitions.forEach[it.transformDefinition2Definition(trace)]
114 declarationsWithDefinedSupertype.forEach[it.transformDeclaration2Definition(trace)]
115 }
116 // 5. if there are elements that are not added to types, then it have to be mapped to declarations without definitions
117 if(problem.elements.exists[it.definedInType.empty]) {
118 declarationsWithoutDefinedSupertype.forEach[it.transformUndefined2Definition(trace)]
119 }
120
121 definedConcreteTypesAreFull(trace)
122 definedConcreteTypesAreDisjoint(trace)
123 problem.definedConcreteTypesAreSatisfyingDefinitions(typeToConcreteSubtypes,trace)
124 }
125
126 // Transforming the declared and defined concrete types
127 problem.elements.transformDefinedSupertype(trace)
128 if(trace.typeTrace.definedSupertype != null) {
129 problem.elements.transformDefinedElements(trace)
130 declarationsWithoutDefinedSupertype.forEach[it.transformNew2Declaration(trace)]
131 }
132
133 // 2: Caching the types by filling type2AllSignatures
134 for(typeToConcreteSubtypesEntry : typeToConcreteSubtypes.entrySet) {
135 val type = typeToConcreteSubtypesEntry.key
136 val List<ALSSignatureDeclaration> signatures = new LinkedList
137
138 }
139 }
140
141 def getTypeTrace(Logic2AlloyLanguageMapperTrace trace) {
142 val res = trace.typeMapperTrace
143 if(res instanceof Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal) {
144 return res
145 } else {
146 throw new IllegalArgumentException('''
147 Expected type mapping trace: «Logic2AlloyLanguageMapper_TypeMapperTrace_Horizontal.name»,
148 but found «res.class.name»''')
149 }
150 }
151
152 private def boolean hasDefinedSupertype(Type type) {
153 if(type instanceof TypeDefinition) {
154 return true
155 } else {
156 if(type.supertypes.empty) return false
157 else return type.supertypes.exists[it.hasDefinedSupertype]
158 }
159 }
160
161 private def transformDefinedSupertype(List<DefinedElement> elements, Logic2AlloyLanguageMapperTrace trace) {
162 trace.typeTrace.definedSupertype = createALSSignatureDeclaration => [
163 it.name = support.toID(#["util","defined","Object"])
164 ]
165 trace.specification.signatureBodies += createALSSignatureBody => [
166 it.abstract = true
167 it.declarations += trace.typeTrace.definedSupertype
168 ]
169 }
170
171 private def transformDefinedElements(List<DefinedElement> elements,
172 Logic2AlloyLanguageMapperTrace trace){
173 if(trace.typeTrace.definedSupertype != null) {
174 // 2. Create elements as singleton signatures subtype of definedSupertype
175 val elementBodies = createALSSignatureBody => [
176 it.multiplicity = ALSMultiplicity::ONE
177 it.supertype = trace.typeTrace.definedSupertype
178 ]
179 trace.specification.signatureBodies += elementBodies
180 for(element : elements) {
181 val elementDeclaration = createALSSignatureDeclaration => [
182 it.name = support.toIDMultiple(#["element"],element.name)
183 ]
184 elementBodies.declarations += elementDeclaration
185 trace.typeTrace.definedElement2Declaration.put(element,elementDeclaration)
186 }
187 // 3. Specify that definedSupertype is equal to the union of specified
188 /*trace.specification.factDeclarations += createALSFactDeclaration => [
189 it.name = support.toID(#["util","typehierarchy","definitionOfElements"])
190 it.term = createALSEquals => [
191 it.leftOperand = createALSReference => [it.referred = trace.typeTrace.definedSupertype]
192 it.rightOperand = support.unfoldPlus(elements.map[element|createALSReference=>[
193 it.referred = element.lookup(trace.typeTrace.definedElement2Declaration)
194 ]])
195 ]
196 ]*/
197 }
198 }
199
200 ///// Type definitions
201
202 protected def void transformDefinition2Definition(TypeDefinition type, Logic2AlloyLanguageMapperTrace trace) {
203 val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["definition2definition"],type.name)]
204 val body = createALSSignatureBody => [
205 it.declarations += sig
206 it.superset += trace.typeTrace.definedSupertype
207 ]
208 trace.specification.signatureBodies += body
209 trace.typeTrace.definition2definition.put(type,sig)
210 }
211 protected def void transformDeclaration2Definition(TypeDeclaration type, Logic2AlloyLanguageMapperTrace trace) {
212 val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["declaration2definition"],type.name)]
213 val body = createALSSignatureBody => [
214 it.declarations += sig
215 it.superset += trace.typeTrace.definedSupertype
216 ]
217 trace.specification.signatureBodies += body
218 trace.typeTrace.declaration2definition.put(type,sig)
219 }
220 protected def void transformUndefined2Definition(TypeDeclaration type, Logic2AlloyLanguageMapperTrace trace) {
221 val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["undefined2definition"],type.name)]
222 val body = createALSSignatureBody => [
223 it.declarations += sig
224 it.supertype = trace.typeTrace.definedSupertype
225 ]
226 trace.specification.signatureBodies += body
227 trace.typeTrace.undefined2definition.put(type,sig)
228 }
229 protected def void transformNew2Declaration(TypeDeclaration type, Logic2AlloyLanguageMapperTrace trace) {
230 val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple(#["declaredPartOfDeclaration"],type.name)]
231 val body = createALSSignatureBody => [
232 it.declarations += sig
233 it.supertype = trace.typeTrace.declaredSupertype
234 ]
235 trace.specification.signatureBodies += body
236 trace.typeTrace.new2declaration.put(type,sig)
237 }
238
239 /**
240 * The dynamic types cover each concrete types
241 */
242 protected def definedConcreteTypesAreFull(Logic2AlloyLanguageMapperTrace trace) {
243 trace.specification.factDeclarations += createALSFactDeclaration => [
244 it.name = support.toID(#["util","typehierarchy","elementFull"])
245 it.term = createALSEquals => [
246 it.leftOperand = createALSReference => [it.referred = trace.typeTrace.definedSupertype]
247 it.rightOperand = support.unfoldPlus(
248 trace.typeTrace.allDefinedTypes.map[type|
249 createALSReference=>[referred = type]
250 ].toList
251 )
252 ]
253 ]
254
255 }
256 /**
257 * The dynamic types are disjoint
258 */
259 protected def definedConcreteTypesAreDisjoint(Logic2AlloyLanguageMapperTrace trace) {
260 val types = trace.getTypeTrace.allDefinedTypes.toList
261 if (types.size >= 2) {
262 trace.specification.factDeclarations += createALSFactDeclaration => [
263 it.name = support.toID(#["util", "typehierarchy", "elementFull"])
264 it.term = types.disjointSets
265 ]
266 }
267 }
268 /**
269 * The dynamic types are subtypes of the types where it is defined, but not subtypes where it is not
270 */
271 protected def definedConcreteTypesAreSatisfyingDefinitions(LogicProblem problem, Map<Type,List<Type>> typeToConcreteSubtypes, Logic2AlloyLanguageMapperTrace trace) {
272 val constraintOnElements = problem.elements.typeConstraints(typeToConcreteSubtypes)
273 for(constraintOnElement : constraintOnElements.entrySet) {
274 val element = constraintOnElement.key
275 val elementSignature = element.lookup(trace.typeTrace.definedElement2Declaration)
276 val constraint = constraintOnElement.value
277
278 var ALSTerm negativeConstraints;
279 if(constraint.negative.isEmpty) {
280 negativeConstraints = null
281 } else {
282 negativeConstraints = support.unfoldAnd(constraint.negative.map[type|
283 createALSNot=> [ elementInDefinedType(elementSignature, type, trace) ]
284 ].toList)
285 }
286
287 var ALSTerm positiveTypeConstraints
288 if(constraint.positiveCNF.isEmpty) {
289 positiveTypeConstraints = null
290 } else {
291 positiveTypeConstraints = support.unfoldAnd(constraint.positiveCNF.map[ typeConstraintFromDefinition |
292 support.unfoldOr(typeConstraintFromDefinition.map[type |
293 elementInDefinedType(elementSignature,type,trace)
294 ].toList,trace)
295 ])
296 }
297
298 var ALSTerm typeConstraint
299 if(negativeConstraints != null && positiveTypeConstraints == null) {
300 typeConstraint = negativeConstraints
301 } else if (negativeConstraints == null && positiveTypeConstraints != null) {
302 typeConstraint = positiveTypeConstraints
303 } else if (negativeConstraints != null && positiveTypeConstraints != null) {
304 val and = createALSAnd
305 and.leftOperand = positiveTypeConstraints
306 and.rightOperand = negativeConstraints
307 typeConstraint = and
308 } else {
309 typeConstraint = null
310 }
311
312 if(typeConstraint != null) {
313 val fact = createALSFactDeclaration => [
314 name = support.toIDMultiple(#["util","typehierarchy","definition"],element.name)
315 ]
316 fact.term = typeConstraint
317 trace.specification.factDeclarations +=fact
318 }
319 // otherwise there is no type constraint on element
320 }
321 }
322
323 private def elementInDefinedType(
324 ALSSignatureDeclaration elementSignature,
325 Type type,
326 Logic2AlloyLanguageMapperTrace trace)
327 {
328 var ALSSignatureDeclaration signature
329 if(type instanceof TypeDeclaration) {
330 if(trace.typeTrace.declaration2definition.containsKey(type)) {
331 signature = type.lookup(trace.typeTrace.declaration2definition)
332 } else if(trace.typeTrace.undefined2definition.containsKey(type)) {
333 signature = type.lookup(trace.typeTrace.undefined2definition)
334 } else {
335 return null
336 }
337 } else if(type instanceof TypeDefinition) {
338 if(trace.typeTrace.definition2definition.containsKey(type)) {
339 signature = type.lookup(trace.typeTrace.definition2definition)
340 } else {
341 return null
342 }
343 } else throw new IllegalArgumentException('''Unknownt type «type.class.name»''')
344
345 val finalSignature = signature
346 return createALSSubset => [
347 leftOperand = createALSReference => [
348 referred = elementSignature
349 ]
350 rightOperand = createALSReference => [
351 referred = finalSignature
352 ]
353 ]
354 }
355
356 def private typeToConcreteSubtypes(LogicProblem problem, Logic2AlloyLanguageMapperTrace trace) {
357 if(trace.incqueryEngine == null) {
358 trace.incqueryEngine = ViatraQueryEngine.on(new EMFScope(problem))
359 }
360 val matcher = SupertypeStarMatcher.on(trace.incqueryEngine)
361 val Map<Type,List<Type>> typeToConcreteSubtypes = new HashMap
362 for(supertype : problem.types) {
363 typeToConcreteSubtypes.put(
364 supertype,
365 matcher.getAllValuesOfsubtype(supertype)
366 .filter[!it.isIsAbstract].toList)
367 }
368 return typeToConcreteSubtypes
369 }
370
371 /**
372 * Gives type constraints in a form of CNF
373 */
374 def private Map<DefinedElement,DynamicTypeConstraints> typeConstraints(List<DefinedElement> elements, Map<Type,List<Type>> typeToConcreteSubtypes) {
375 val Map<DefinedElement,DynamicTypeConstraints> constraints = new HashMap
376 elements.forEach[constraints.put(it,new DynamicTypeConstraints)]
377
378 for(type : typeToConcreteSubtypes.keySet.filter(TypeDefinition)) {
379 val subtypes = type.lookup(typeToConcreteSubtypes)
380 for(elementInType:type.elements) {
381 elementInType.lookup(constraints).addPositiveTypeOptions(subtypes)
382 }
383 for(elementNotInType:elements.filter[!type.elements.contains(it)]) {
384 elementNotInType.lookup(constraints).addNegativeTypes(subtypes)
385 }
386 }
387
388 return constraints
389 }
390
391 private def ALSTerm disjointSets(List<ALSSignatureDeclaration> signatures) {
392 if(signatures.size >= 2){
393 val top = createALSEquals => [
394 it.leftOperand = signatures.intersectionOfTypes
395 it.rightOperand = createALSNone
396 ]
397 if(signatures.size > 2) {
398 return createALSAnd => [
399 it.leftOperand = top
400 it.rightOperand = signatures.subList(1,signatures.size).disjointSets
401 ]
402 } else{
403 return top
404 }
405 } else {
406 throw new UnsupportedOperationException()
407 }
408 }
409
410 private def ALSIntersection intersectionOfTypes(List<ALSSignatureDeclaration> signatures) {
411 if(signatures.size == 2) {
412 return createALSIntersection => [
413 leftOperand = createALSReference => [it.referred = signatures.get(0)]
414 rightOperand = createALSReference => [it.referred = signatures.get(1)]
415 ]
416 } else if(signatures.size > 2) {
417 return createALSIntersection => [
418 leftOperand = createALSReference => [it.referred = signatures.get(0)]
419 rightOperand = signatures.subList(1,signatures.size).intersectionOfTypes
420 ]
421 } else throw new UnsupportedOperationException()
422 }
423
424
425 override transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
426 //trace.typeTrace.
427 }
428} \ 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 6533ad36..4d7b50e8 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
@@ -1,26 +1,88 @@
1package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder 1package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder
2 2
3import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity
4import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureBody
3import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration 5import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration
6import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement 7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type 8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
6import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition 9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
8import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem 10import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage
11import java.util.Collection
9import java.util.HashMap 12import java.util.HashMap
13import java.util.LinkedList
14import java.util.List
10import java.util.Map 15import java.util.Map
11import java.util.Collection
12 16
13class Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapperTrace { 17class Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapperTrace {
14 val Map<TypeDeclaration,ALSSignatureDeclaration> newElementTypes = new HashMap 18 public var ALSSignatureDeclaration objectSupperClass;
15 val Map<Type,ALSSignatureDeclaration> definedElementTypes = new HashMap 19 public val Map<Type, ALSSignatureDeclaration> type2ALSType = new HashMap;
16 var ALSSignatureDeclaration undefinedSupertype 20 public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = new HashMap
17 var ALSSignatureDeclaration definedSupertype 21 public val Map<Type, List<ALSSignatureDeclaration>> typeSelection = new HashMap
18} 22}
19 23
20class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapper{ 24class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapper{
25 private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE
26 private val Logic2AlloyLanguageMapper_Support support = new Logic2AlloyLanguageMapper_Support;
27
28 new() {
29 LogicproblemPackage.eINSTANCE.class
30 }
21 31
22 override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { 32 override transformTypes(Collection<Type> types, Collection<DefinedElement> elements, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
23 throw new UnsupportedOperationException("TODO: auto-generated method stub") 33 if(types.exists[hasDefinedSupertype]) {
34 throw new UnsupportedOperationException('''Defined supertype is not supported by this type mapping!''')
35 } else {
36
37 val typeTrace = new Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal
38 trace.typeMapperTrace = typeTrace
39
40 // 1. A global type for Objects is created
41 val objectSig = createALSSignatureDeclaration => [it.name = support.toID(#["util","Object"])]
42 val objectBody = createALSSignatureBody => [
43 it.declarations += objectSig
44 it.abstract = true
45 ]
46 typeTrace.objectSupperClass = objectSig
47 trace.specification.signatureBodies += objectBody
48
49 // 2. Each type is mapped to a unique sig
50 for(type : types) {
51 val sig = createALSSignatureDeclaration => [it.name = support.toIDMultiple("type",type.name)]
52 val body = createALSSignatureBody => [it.declarations += sig]
53 body.abstract = type.isIsAbstract || (type instanceof TypeDefinition)
54
55 trace.specification.signatureBodies += body
56 typeTrace.type2ALSType.put(type,sig)
57
58 if(type instanceof TypeDefinition) {
59 val elementContainer = createALSSignatureBody => [it.multiplicity = ALSMultiplicity::ONE it.supertype = sig]
60 for(element : type.elements) {
61 val signature = createALSSignatureDeclaration => [it.name = support.toIDMultiple("element",element.name)]
62 elementContainer.declarations += signature
63
64 }
65 trace.specification.signatureBodies += elementContainer
66 }
67
68 typeTrace.typeSelection.put(type,new LinkedList()=>[add(sig)])
69 }
70
71 // 6. Each inheritance is modeled by extend keyword
72 for(type : types) {
73 if(type.supertypes.size == 1) {
74 val alsType = typeTrace.type2ALSType.get(type.supertypes.head)
75 (type.eContainer as ALSSignatureBody).supertype = alsType
76 } else if(type.supertypes.size > 1){
77 val alsMainType = typeTrace.type2ALSType.get(type.supertypes.head)
78 (type.eContainer as ALSSignatureBody).supertype = alsMainType
79 for(otherType : type.supertypes.filter[it != alsMainType]) {
80 typeTrace.typeSelection.get(otherType).add(typeTrace.type2ALSType.get(otherType))
81 }
82 }
83 }
84
85 }
24 } 86 }
25 87
26 private def boolean hasDefinedSupertype(Type type) { 88 private def boolean hasDefinedSupertype(Type type) {
@@ -30,21 +92,32 @@ class Logic2AlloyLanguageMapper_TypeMapper_InheritanceAndHorizontal implements L
30 if(type.supertypes.empty) return false 92 if(type.supertypes.empty) return false
31 else return type.supertypes.exists[it.hasDefinedSupertype] 93 else return type.supertypes.exists[it.hasDefinedSupertype]
32 } 94 }
33 } 95 }
96
97 def getTypeTrace(Logic2AlloyLanguageMapperTrace trace) {
98 val res = trace.typeMapperTrace
99 if(res instanceof Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal) {
100 return res
101 } else {
102 throw new IllegalArgumentException('''
103 Expected type mapping trace: «Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.name»,
104 but found «res.class.name»''')
105 }
106 }
34 107
35 override transformTypeReference(Type referred, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) { 108 override transformTypeReference(Type referred, Logic2AlloyLanguageMapper mapper, Logic2AlloyLanguageMapperTrace trace) {
36 throw new UnsupportedOperationException("TODO: auto-generated method stub") 109 trace.typeTrace.typeSelection.get(referred)
37 } 110 }
38 111
39 override getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) { 112 override getUndefinedSupertype(Logic2AlloyLanguageMapperTrace trace) {
40 throw new UnsupportedOperationException("TODO: auto-generated method stub") 113 trace.typeTrace.objectSupperClass
41 } 114 }
42 115
43 override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) { 116 override transformReference(DefinedElement referred, Logic2AlloyLanguageMapperTrace trace) {
44 throw new UnsupportedOperationException("TODO: auto-generated method stub") 117 createALSReference => [it.referred = trace.typeTrace.definedElement2Declaration.get(referred)]
45 } 118 }
46 119
47 override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) { 120 override getUndefinedSupertypeScope(int undefinedScope, Logic2AlloyLanguageMapperTrace trace) {
48 throw new UnsupportedOperationException("TODO: auto-generated method stub") 121 return undefinedScope + trace.typeTrace.definedElement2Declaration.size
49 } 122 }
50} \ No newline at end of file 123} \ No newline at end of file
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-29 00:43:14 +0000