diff options
author | OszkarSemerath <oszkar.semerath@gmail.com> | 2018-08-10 21:27:34 +0200 |
---|---|---|
committer | OszkarSemerath <oszkar.semerath@gmail.com> | 2018-08-10 21:27:34 +0200 |
commit | b4734ce5b92f00026351748932fb4158617f0da7 (patch) | |
tree | 2631d6d6ebb960835b60ea452c112cbcd32d713e | |
parent | Lowered documentation level requirement for initial partial models (diff) | |
download | VIATRA-Generator-b4734ce5b92f00026351748932fb4158617f0da7.tar.gz VIATRA-Generator-b4734ce5b92f00026351748932fb4158617f0da7.tar.zst VIATRA-Generator-b4734ce5b92f00026351748932fb4158617f0da7.zip |
Updated type provider to support java native types
2 files changed, 238 insertions, 85 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF index 9f2acd2e..1fda4212 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF | |||
@@ -16,7 +16,8 @@ Require-Bundle: com.google.guava, | |||
16 | org.eclipse.core.runtime, | 16 | org.eclipse.core.runtime, |
17 | org.eclipse.emf.ecore;visibility:=reexport, | 17 | org.eclipse.emf.ecore;visibility:=reexport, |
18 | hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0";visibility:=reexport, | 18 | hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0";visibility:=reexport, |
19 | org.eclipse.viatra.query.runtime.base.itc;bundle-version="1.5.0" | 19 | org.eclipse.viatra.query.runtime.base.itc;bundle-version="1.5.0", |
20 | org.eclipse.viatra.query.patternlanguage.emf;bundle-version="2.0.0" | ||
20 | Bundle-ActivationPolicy: lazy | 21 | Bundle-ActivationPolicy: lazy |
21 | Export-Package: hu.bme.mit.inf.dslreasoner.viatra2logic, | 22 | Export-Package: hu.bme.mit.inf.dslreasoner.viatra2logic, |
22 | hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations, | 23 | hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations, |
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2Logic.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2Logic.xtend index 95ba9219..ce902353 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2Logic.xtend +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2Logic.xtend | |||
@@ -4,20 +4,23 @@ import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | |||
4 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace | 4 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace |
5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | 9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDescriptor | 10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | 12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable |
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 13 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
11 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery | 14 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery |
12 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsFactory | 15 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsFactory |
13 | import java.util.ArrayList | 16 | import java.util.ArrayList |
14 | import java.util.HashMap | 17 | import java.util.HashMap |
18 | import java.util.HashSet | ||
15 | import java.util.LinkedList | 19 | import java.util.LinkedList |
16 | import java.util.List | 20 | import java.util.List |
17 | import java.util.Map | 21 | import java.util.Map |
18 | import java.util.Set | 22 | import java.util.Set |
19 | import org.eclipse.emf.ecore.EAttribute | 23 | import org.eclipse.emf.ecore.EAttribute |
20 | import org.eclipse.emf.ecore.EClass | ||
21 | import org.eclipse.emf.ecore.EClassifier | 24 | import org.eclipse.emf.ecore.EClassifier |
22 | import org.eclipse.emf.ecore.EEnum | 25 | import org.eclipse.emf.ecore.EEnum |
23 | import org.eclipse.emf.ecore.EReference | 26 | import org.eclipse.emf.ecore.EReference |
@@ -28,6 +31,9 @@ import org.eclipse.viatra.query.runtime.emf.EMFQueryMetaContext | |||
28 | import org.eclipse.viatra.query.runtime.emf.types.BaseEMFTypeKey | 31 | import org.eclipse.viatra.query.runtime.emf.types.BaseEMFTypeKey |
29 | import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey | 32 | import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey |
30 | import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey | 33 | import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey |
34 | import org.eclipse.viatra.query.runtime.matchers.context.IInputKey | ||
35 | import org.eclipse.viatra.query.runtime.matchers.context.common.JavaTransitiveInstancesKey | ||
36 | import org.eclipse.viatra.query.runtime.matchers.planning.helpers.TypeHelper | ||
31 | import org.eclipse.viatra.query.runtime.matchers.psystem.PBody | 37 | import org.eclipse.viatra.query.runtime.matchers.psystem.PBody |
32 | import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable | 38 | import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable |
33 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall | 39 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall |
@@ -37,7 +43,9 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.rewriters.PBodyNormaliz | |||
37 | import org.eclipse.xtend.lib.annotations.Data | 43 | import org.eclipse.xtend.lib.annotations.Data |
38 | 44 | ||
39 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 45 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
40 | import org.eclipse.viatra.query.runtime.matchers.psystem.TypeJudgement | 46 | import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction |
47 | import org.eclipse.emf.ecore.util.EcoreUtil | ||
48 | import org.eclipse.viatra.query.runtime.emf.types.EClassUnscopedTransitiveInstancesKey | ||
41 | 49 | ||
42 | @Data class ViatraQuerySetDescriptor { | 50 | @Data class ViatraQuerySetDescriptor { |
43 | val List<? extends IQuerySpecification<?>> patterns | 51 | val List<? extends IQuerySpecification<?>> patterns |
@@ -45,6 +53,7 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.TypeJudgement | |||
45 | val Map<IQuerySpecification<?>,EStructuralFeature> derivedFeatures | 53 | val Map<IQuerySpecification<?>,EStructuralFeature> derivedFeatures |
46 | } | 54 | } |
47 | class Viatra2LogicTrace { | 55 | class Viatra2LogicTrace { |
56 | public val Map<PQuery, PDisjunction> query2Disjunction = new HashMap | ||
48 | public val Map<PQuery, RelationDefinition> query2Relation = new HashMap | 57 | public val Map<PQuery, RelationDefinition> query2Relation = new HashMap |
49 | public val Map<PQuery, TransfomedViatraQuery> query2Annotation = new HashMap | 58 | public val Map<PQuery, TransfomedViatraQuery> query2Annotation = new HashMap |
50 | public val Map<Pair<PQuery,PParameter>, Variable> parameter2Variable = new HashMap | 59 | public val Map<Pair<PQuery,PParameter>, Variable> parameter2Variable = new HashMap |
@@ -58,6 +67,8 @@ class Viatra2LogicConfiguration { | |||
58 | class Viatra2Logic { | 67 | class Viatra2Logic { |
59 | val extension LogicProblemBuilder builder = new LogicProblemBuilder | 68 | val extension LogicProblemBuilder builder = new LogicProblemBuilder |
60 | val extension Viatra2LogicAnnotationsFactory factory = Viatra2LogicAnnotationsFactory.eINSTANCE | 69 | val extension Viatra2LogicAnnotationsFactory factory = Viatra2LogicAnnotationsFactory.eINSTANCE |
70 | val normalizer = new PBodyNormalizer(EMFQueryMetaContext.DEFAULT) | ||
71 | |||
61 | val Ecore2Logic ecore2Logic | 72 | val Ecore2Logic ecore2Logic |
62 | Constraint2Logic constraint2Logic | 73 | Constraint2Logic constraint2Logic |
63 | 74 | ||
@@ -72,18 +83,44 @@ class Viatra2Logic { | |||
72 | Viatra2LogicConfiguration config) | 83 | Viatra2LogicConfiguration config) |
73 | { | 84 | { |
74 | val viatra2LogicTrace = new Viatra2LogicTrace | 85 | val viatra2LogicTrace = new Viatra2LogicTrace |
75 | for(query: queries.patterns) { | 86 | val typeAlanysis = new HashMap |
87 | val pQueries = queries.patterns.map[it.internalQueryRepresentation] | ||
88 | |||
89 | for(query: pQueries) { | ||
90 | val disjunction = normalizer.rewrite(query) | ||
91 | viatra2LogicTrace.query2Disjunction.put(query,disjunction) | ||
92 | } | ||
93 | |||
94 | for(query: pQueries) { | ||
95 | val types = query.lookup(viatra2LogicTrace.query2Disjunction).bodies.toInvertedMap[ | ||
96 | TypeHelper::inferUnaryTypesFor(it.uniqueVariables,it.constraints,EMFQueryMetaContext.DEFAULT) | ||
97 | ] | ||
98 | // for(m : types.values) { | ||
99 | // for(n: m.entrySet) { | ||
100 | // val variable = n.key | ||
101 | // println(''' - «variable.name»''') | ||
102 | // for(type : n.value) { | ||
103 | // println('''«variable.name» - «type»''') | ||
104 | // } | ||
105 | // } | ||
106 | // | ||
107 | // } | ||
108 | |||
109 | typeAlanysis.put(query,types) | ||
110 | } | ||
111 | |||
112 | for(query: pQueries) { | ||
76 | try { | 113 | try { |
77 | this.transformQueryHeader(query,ecore2LogicTrace,viatra2LogicTrace,config) | 114 | this.transformQueryHeader(query,query.lookup(typeAlanysis),ecore2LogicTrace,viatra2LogicTrace,config) |
78 | } catch(IllegalArgumentException e) { | 115 | } catch(IllegalArgumentException e) { |
79 | throw new IllegalArgumentException(''' | 116 | throw new IllegalArgumentException(''' |
80 | Unable to translate query "«query.fullyQualifiedName»". | 117 | Unable to translate query "«query.fullyQualifiedName»". |
81 | Reason: «e.class.simpleName», «e.message»''',e) | 118 | Reason: «e.class.simpleName», «e.message»''',e) |
82 | } | 119 | } |
83 | } | 120 | } |
84 | for(query: queries.patterns) { | 121 | for(query: pQueries) { |
85 | try { | 122 | try { |
86 | this.transformQuerySpecification(query,ecore2LogicTrace,viatra2LogicTrace,config) | 123 | this.transformQuerySpecification(query,query.lookup(typeAlanysis),ecore2LogicTrace,viatra2LogicTrace,config) |
87 | } catch (IllegalArgumentException e){ | 124 | } catch (IllegalArgumentException e){ |
88 | throw new IllegalArgumentException(''' | 125 | throw new IllegalArgumentException(''' |
89 | Unable to translate query "«query.fullyQualifiedName»". | 126 | Unable to translate query "«query.fullyQualifiedName»". |
@@ -95,31 +132,27 @@ class Viatra2Logic { | |||
95 | }*/ | 132 | }*/ |
96 | 133 | ||
97 | transformQueryConstraints( | 134 | transformQueryConstraints( |
98 | queries.validationPatterns, | 135 | queries.validationPatterns.map[internalQueryRepresentation], |
99 | queries.derivedFeatures, | 136 | queries.derivedFeatures, |
100 | ecore2LogicTrace,viatra2LogicTrace) | 137 | ecore2LogicTrace,viatra2LogicTrace) |
101 | return new TracedOutput(ecore2LogicTrace.output,viatra2LogicTrace) | 138 | return new TracedOutput(ecore2LogicTrace.output,viatra2LogicTrace) |
102 | } | 139 | } |
103 | 140 | ||
104 | def protected transformQueryHeader(IQuerySpecification<?> squery, | 141 | def protected transformQueryHeader( |
142 | PQuery pquery, | ||
143 | Map<PBody, Map<PVariable, Set<IInputKey>>> types, | ||
105 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | 144 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, |
106 | Viatra2LogicTrace viatra2LogicTrace, | 145 | Viatra2LogicTrace viatra2LogicTrace, |
107 | Viatra2LogicConfiguration config) | 146 | Viatra2LogicConfiguration config) |
108 | { | 147 | { |
109 | val pquery = squery.internalQueryRepresentation | 148 | val relationName = '''pattern «pquery.fullyQualifiedName.replace('.',' ')»''' |
110 | val relationName = '''pattern «pquery.fullyQualifiedName.replace('.',' ')»''' | ||
111 | val parameters = new ArrayList<Variable>(pquery.parameters.size) | 149 | val parameters = new ArrayList<Variable>(pquery.parameters.size) |
112 | for(vParam: pquery.parameters) { | 150 | for(vParam: pquery.parameters) { |
113 | //println(">" + vParam.declaredUnaryType) | ||
114 | val type = vParam.declaredUnaryType as BaseEMFTypeKey<? extends EClassifier> | ||
115 | val parameterType = transformTypeReference( | ||
116 | type, | ||
117 | ecore2LogicTrace | ||
118 | ) | ||
119 | // if(parameterType == null) { | ||
120 | // println(parameterType) | ||
121 | // } | ||
122 | val parameterName = '''parameter «vParam.name»''' | 151 | val parameterName = '''parameter «vParam.name»''' |
152 | val parameterType = getType(vParam,types,ecore2LogicTrace) | ||
153 | if(parameterType === null) { | ||
154 | throw new AssertionError('''null type for parameter «vParam.name»''') | ||
155 | } | ||
123 | val lParam = createVar(parameterName,parameterType) | 156 | val lParam = createVar(parameterName,parameterType) |
124 | viatra2LogicTrace.parameter2Variable.put(pquery->vParam,lParam) | 157 | viatra2LogicTrace.parameter2Variable.put(pquery->vParam,lParam) |
125 | parameters+=lParam | 158 | parameters+=lParam |
@@ -141,42 +174,37 @@ class Viatra2Logic { | |||
141 | } | 174 | } |
142 | 175 | ||
143 | def protected transformQuerySpecification( | 176 | def protected transformQuerySpecification( |
144 | IQuerySpecification<?> squery, | 177 | PQuery pquery, |
178 | Map<PBody, Map<PVariable, Set<IInputKey>>> types, | ||
145 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | 179 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, |
146 | Viatra2LogicTrace viatra2LogicTrace, | 180 | Viatra2LogicTrace viatra2LogicTrace, |
147 | Viatra2LogicConfiguration config) | 181 | Viatra2LogicConfiguration config) |
148 | { | 182 | { |
149 | val pquery = squery.internalQueryRepresentation | 183 | val disjunction = pquery.lookup(viatra2LogicTrace.query2Disjunction) |
150 | val disjunction = if(config.normalize) { | 184 | |
151 | val normalizer = new PBodyNormalizer(EMFQueryMetaContext.DEFAULT) | ||
152 | normalizer.rewrite(pquery) | ||
153 | } else { | ||
154 | pquery.disjunctBodies | ||
155 | } | ||
156 | val translatedBodies = new ArrayList(disjunction.bodies.size) | 185 | val translatedBodies = new ArrayList(disjunction.bodies.size) |
157 | for(body : disjunction.bodies) { | 186 | for(body : disjunction.bodies) { |
158 | translatedBodies+=body.transformBody(ecore2LogicTrace,viatra2LogicTrace,config) | 187 | translatedBodies+=body.transformBody(types,ecore2LogicTrace,viatra2LogicTrace,config) |
159 | } | 188 | } |
160 | val relation = pquery.lookup(viatra2LogicTrace.query2Relation) | 189 | val relation = pquery.lookup(viatra2LogicTrace.query2Relation) |
161 | relation.value = Or(translatedBodies) | 190 | relation.value = Or(translatedBodies) |
162 | } | 191 | } |
163 | 192 | ||
164 | def transformQueryConstraints( | 193 | def transformQueryConstraints( |
165 | Set<? extends IQuerySpecification<?>> validationPatterns, | 194 | Iterable<PQuery> validationPatterns, |
166 | Map<IQuerySpecification<?>,EStructuralFeature> derivedFeatures, | 195 | Map<IQuerySpecification<?>,EStructuralFeature> derivedFeatures, |
167 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | 196 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, |
168 | Viatra2LogicTrace viatra2LogicTrace) | 197 | Viatra2LogicTrace viatra2LogicTrace) |
169 | { | 198 | { |
170 | for(validationPattern : validationPatterns) { | 199 | for(pquery : validationPatterns) { |
171 | val pquery = validationPattern.internalQueryRepresentation | 200 | val targetRelation = pquery.lookup(viatra2LogicTrace.query2Relation) |
172 | val constraint = Assertion('''errorpattern «pquery.fullyQualifiedName.replace('.',' ')»''', | 201 | val constraint = Assertion('''errorpattern «pquery.fullyQualifiedName.replace('.',' ')»''', |
173 | Forall[ | 202 | Forall[ |
174 | for(param: pquery.parameters) { | 203 | for(param: targetRelation.parameters) { |
175 | addVar(param.name,transformTypeReference( | 204 | addVar('''p«targetRelation.parameters.indexOf(param)»''', |
176 | param.declaredUnaryType as BaseEMFTypeKey<? extends EClassifier>, | 205 | EcoreUtil::copy(param)) |
177 | ecore2LogicTrace)) | ||
178 | } | 206 | } |
179 | Not(pquery.lookup(viatra2LogicTrace.query2Relation).call(it.variables)) | 207 | Not(targetRelation.call(it.variables)) |
180 | ] | 208 | ] |
181 | ) | 209 | ) |
182 | val annotation = createTransformedViatraWellformednessConstraint => [ | 210 | val annotation = createTransformedViatraWellformednessConstraint => [ |
@@ -205,6 +233,7 @@ class Viatra2Logic { | |||
205 | } | 233 | } |
206 | 234 | ||
207 | def transformBody(PBody body, | 235 | def transformBody(PBody body, |
236 | Map<PBody, Map<PVariable, Set<IInputKey>>> types, | ||
208 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, | 237 | TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, |
209 | Viatra2LogicTrace viatra2LogicTrace, | 238 | Viatra2LogicTrace viatra2LogicTrace, |
210 | Viatra2LogicConfiguration config) | 239 | Viatra2LogicConfiguration config) |
@@ -220,10 +249,11 @@ class Viatra2Logic { | |||
220 | val innerPositiveVariables = new LinkedList | 249 | val innerPositiveVariables = new LinkedList |
221 | val innerNegativeVariables = new LinkedList | 250 | val innerNegativeVariables = new LinkedList |
222 | for(innerVariable : body.uniqueVariables) { | 251 | for(innerVariable : body.uniqueVariables) { |
252 | |||
223 | if(!variable2Variable.containsKey(innerVariable)) { | 253 | if(!variable2Variable.containsKey(innerVariable)) { |
224 | val name = '''variable «innerVariable.name.normalizeName»''' | 254 | val name = '''variable «innerVariable.name.normalizeName»''' |
225 | //println(body.pattern.fullyQualifiedName + "-") | 255 | //println(body.pattern.fullyQualifiedName + "-") |
226 | val logicType = getType(innerVariable,body,ecore2LogicTrace) | 256 | val logicType = getType(innerVariable,types,ecore2LogicTrace) |
227 | val logicVariable = createVar(name,logicType) | 257 | val logicVariable = createVar(name,logicType) |
228 | if(innerVariable.isPositiveVariable) { | 258 | if(innerVariable.isPositiveVariable) { |
229 | innerPositiveVariables += logicVariable | 259 | innerPositiveVariables += logicVariable |
@@ -252,38 +282,47 @@ class Viatra2Logic { | |||
252 | 282 | ||
253 | return allVariablesAreExisting | 283 | return allVariablesAreExisting |
254 | } | 284 | } |
285 | // def toTypeJudgement(PVariable v, IInputKey key) { | ||
286 | // new TypeJudgement(key,new Tuple1) | ||
287 | // } | ||
255 | 288 | ||
256 | def private normalizeName(String variableName) { | 289 | def private normalizeName(String variableName) { |
257 | return variableName.replaceAll("[\\W]|_", "") | 290 | return variableName.replaceAll("[\\W]|_", "") |
258 | } | 291 | } |
259 | 292 | ||
260 | def TypeDescriptor getType(PVariable v, PBody body, TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { | 293 | /** |
261 | var Map<PVariable, Set<TypeJudgement>> unaryTypeRestrictions = null; | 294 | * Translates the type of a parameter variable in a pattern |
262 | if (v.isPositiveVariable) { | 295 | */ |
263 | unaryTypeRestrictions = body.getAllUnaryTypeRestrictions(EMFQueryMetaContext.DEFAULT) | 296 | def TypeReference getType(PParameter v, Map<PBody, Map<PVariable, Set<IInputKey>>> types, TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { |
264 | if (!unaryTypeRestrictions.containsKey(v)) { | 297 | // If parameter type is specified then the specified type is used |
265 | throw new IllegalArgumentException('''No positive constraints on variable: «v.name»''') | 298 | if(v.declaredUnaryType !== null) { |
266 | } | 299 | return transformTypeReference(v.declaredUnaryType,ecore2LogicTrace) |
267 | val allTypes = v.lookup(unaryTypeRestrictions) | 300 | } |
268 | 301 | // Otherwise, calculate the type based on the type of the variable in the bodies | |
269 | val types = allTypes.filter[it.inputKey instanceof BaseEMFTypeKey<?>].toSet | 302 | else { |
270 | 303 | val bodies = types.keySet | |
271 | if (types.size == 0) { | 304 | val typesFromBodies = new ArrayList(bodies.size) |
272 | throw new AssertionError(''' | 305 | for(body : bodies) { |
273 | No EMF type for «v.name». | 306 | // collect the variable in the body |
274 | Non-EMF types: [«FOR t : allTypes.filter[!types.contains(it)].map[inputKey.prettyPrintableName] SEPARATOR ','»«t»«ENDFOR»]''') | 307 | val exported = body.symbolicParameters.filter[it.patternParameter === v] |
275 | } else if (types.size == 1) { | 308 | if(exported.size !== 1) { |
276 | return (types.head.inputKey as BaseEMFTypeKey<? extends EClassifier>). | 309 | throw new AssertionError('''Parameter «v.name» has no reference in body!''') |
277 | transformTypeReference(ecore2LogicTrace) | 310 | } |
278 | } else { | 311 | val variable = exported.head.parameterVariable |
279 | // println(''' | 312 | typesFromBodies+=variable.getType(types,ecore2LogicTrace) |
280 | // Type Judgements of «v.name» | ||
281 | // «types.map[inputKey.prettyPrintableName]» | ||
282 | // ''') | ||
283 | return this.ecore2Logic.TypeofEClass(ecore2LogicTrace.trace, calculateCommonSubtype(types.map [ | ||
284 | (it.inputKey as BaseEMFTypeKey<EClass>).emfKey as EClass | ||
285 | ], ecore2LogicTrace)) | ||
286 | } | 313 | } |
314 | return typesFromBodies.calculateCommonSupertype | ||
315 | } | ||
316 | } | ||
317 | |||
318 | /** | ||
319 | * Translates the type of a variable in a pattern body | ||
320 | */ | ||
321 | def TypeReference getType(PVariable v, Map<PBody, Map<PVariable, Set<IInputKey>>> types ,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { | ||
322 | if (v.isPositiveVariable) { | ||
323 | val keys = getTypesFromCollection(v,types) | ||
324 | val logicTypes = keys.map[transformTypeReference(it,ecore2LogicTrace)].filterNull | ||
325 | return logicTypes.calculateCommonSubtype | ||
287 | } else { | 326 | } else { |
288 | val onlyConstraint = v.referringConstraints.head as NegativePatternCall | 327 | val onlyConstraint = v.referringConstraints.head as NegativePatternCall |
289 | val indexOfVariable = v.lookup(onlyConstraint.actualParametersTuple.invertIndex) | 328 | val indexOfVariable = v.lookup(onlyConstraint.actualParametersTuple.invertIndex) |
@@ -295,42 +334,155 @@ class Viatra2Logic { | |||
295 | } else | 334 | } else |
296 | return declaredUnaryType.transformTypeReference(ecore2LogicTrace) | 335 | return declaredUnaryType.transformTypeReference(ecore2LogicTrace) |
297 | } | 336 | } |
298 | |||
299 | } | 337 | } |
300 | 338 | ||
301 | def calculateCommonSubtype(Iterable<EClass> allsuperClasses,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { | 339 | def getTypesFromCollection(PVariable v, Map<PBody, Map<PVariable, Set<IInputKey>>> types) { |
302 | val superClasses = allsuperClasses.filter[it!=EcorePackage.eINSTANCE.EObject] | 340 | for(entry : types.entrySet) { |
303 | val head = superClasses.head | 341 | if(entry.key.uniqueVariables.contains(v)) { |
304 | if(superClasses.forall[it.isSuperTypeOf(head)]) return head | 342 | return v.lookup(entry.value) |
305 | else { | 343 | } |
306 | val allClasses = this.ecore2Logic.allClassesInScope(ecore2LogicTrace.trace) | 344 | } |
307 | //println(allClasses.toList) | 345 | throw new IllegalArgumentException('''Variable «v.name» is not present in neither of the bodies!''') |
308 | val commonSubclasses = allClasses.filter[sub | superClasses.forall[sup | sup.isSuperTypeOf(sub)]] | 346 | } |
309 | //println(commonSubclasses.toList) | 347 | |
310 | val mostGenericSubclasses = commonSubclasses.filter[generic | ! commonSubclasses.exists[moreGeneric | moreGeneric!=generic && moreGeneric.isSuperTypeOf(generic)]] | 348 | |
311 | //println(mostGenericSubclasses.toList) | 349 | def TypeReference calculateCommonSubtype(Iterable<TypeReference> types) { |
312 | if(mostGenericSubclasses.isEmpty) throw new AssertionError('''No common supertype: | 350 | val primitiveTypeReferences = types.filter(PrimitiveTypeReference) |
313 | «FOR s : superClasses SEPARATOR ", "»«s.name»«ENDFOR»''') | 351 | val complexTypeReferences = types.filter(ComplexTypeReference) |
314 | else return mostGenericSubclasses.head | 352 | if(complexTypeReferences.isEmpty) { |
353 | val head = primitiveTypeReferences.head | ||
354 | if(primitiveTypeReferences.exists[it.eClass !== head.eClass]) { | ||
355 | throw new IllegalArgumentException('''Inconsistent types: «primitiveTypeReferences.map[eClass.name].toSet.toList»''') | ||
356 | } | ||
357 | return head | ||
358 | } else if(primitiveTypeReferences.isEmpty) { | ||
359 | val complexTypes = complexTypeReferences.map[it.referred].toSet | ||
360 | if(complexTypes.size === 1) { | ||
361 | return builder.toTypeReference(complexTypes.head) | ||
362 | } | ||
363 | // Collect possible subtypes | ||
364 | val subtypeSets = complexTypes.map[it.transitiveClosureStar[it.subtypes].toSet] | ||
365 | val commonTypeSet = new HashSet(subtypeSets.head) | ||
366 | val otherSets = subtypeSets.tail | ||
367 | for(otherSet : otherSets) { | ||
368 | commonTypeSet.retainAll(otherSet) | ||
369 | } | ||
370 | if(commonTypeSet.empty) { | ||
371 | throw new IllegalArgumentException('''Inconsistent types: «complexTypes.map[name].toList»''') | ||
372 | } | ||
373 | |||
374 | return calculateCommonComplexSupertype(commonTypeSet) | ||
375 | |||
376 | } else { | ||
377 | throw new IllegalArgumentException(''' | ||
378 | Inconsistent types, mixing primitive and complex types: | ||
379 | «primitiveTypeReferences.map[eClass.name].toSet.toList» | ||
380 | and | ||
381 | «complexTypeReferences.map[it.referred].toSet.map[name].toList»''') | ||
382 | |||
383 | } | ||
384 | } | ||
385 | def TypeReference calculateCommonSupertype(Iterable<TypeReference> types) { | ||
386 | val primitiveTypeReferences = types.filter(PrimitiveTypeReference) | ||
387 | val complexTypeReferences = types.filter(ComplexTypeReference) | ||
388 | if(complexTypeReferences.isEmpty) { | ||
389 | val head = primitiveTypeReferences.head | ||
390 | if(primitiveTypeReferences.exists[it.eClass !== head.eClass]) { | ||
391 | throw new IllegalArgumentException('''Inconsistent types: «primitiveTypeReferences.map[eClass.name].toSet.toList»''') | ||
392 | } | ||
393 | return head | ||
394 | } else if(primitiveTypeReferences.isEmpty) { | ||
395 | val complexTypes = complexTypeReferences.map[it.referred].toSet | ||
396 | return calculateCommonComplexSupertype(complexTypes) | ||
397 | |||
398 | } else { | ||
399 | throw new IllegalArgumentException(''' | ||
400 | Inconsistent types, mixing primitive and complex types: | ||
401 | «primitiveTypeReferences.map[eClass.name].toSet.toList» | ||
402 | and | ||
403 | «complexTypeReferences.map[it.referred].toSet.map[name].toList»''') | ||
315 | 404 | ||
316 | } | 405 | } |
317 | } | 406 | } |
407 | def TypeReference calculateCommonComplexSupertype(Set<Type> complexTypes) { | ||
408 | if(complexTypes.size === 1) { | ||
409 | return builder.toTypeReference(complexTypes.head) | ||
410 | } | ||
411 | // Collect possible supertypes | ||
412 | val supertypeSets = complexTypes.map[it.transitiveClosureStar[it.supertypes].toSet] | ||
413 | val commonTypeSet = new HashSet(supertypeSets.head) | ||
414 | val otherSets = supertypeSets.tail | ||
415 | for(otherSet : otherSets) { | ||
416 | commonTypeSet.retainAll(otherSet) | ||
417 | } | ||
418 | if(commonTypeSet.empty) { | ||
419 | throw new IllegalArgumentException('''Inconsistent types: «complexTypes.map[name].toList»''') | ||
420 | } | ||
421 | // Remove type that already have covered | ||
422 | val coveredTypes = commonTypeSet.map[it.supertypes].flatten | ||
423 | commonTypeSet.removeAll(coveredTypes) | ||
424 | return builder.toTypeReference(commonTypeSet.head) | ||
425 | } | ||
318 | 426 | ||
319 | def dispatch transformTypeReference(EDataTypeInSlotsKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { | 427 | /** |
428 | * Transforms a Viatra type reference to a logic type. | ||
429 | */ | ||
430 | def dispatch TypeReference transformTypeReference(EDataTypeInSlotsKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { | ||
320 | val w = k.wrappedKey | 431 | val w = k.wrappedKey |
321 | if(w == EcorePackage.Literals.EINT) { | 432 | if(w == EcorePackage.Literals.EINT || w == EcorePackage.Literals.ESHORT || w == EcorePackage.Literals.ELONG) { |
322 | return builder.LogicInt | 433 | return builder.LogicInt |
323 | } else if(w == EcorePackage.Literals.EDOUBLE || w == EcorePackage.Literals.EFLOAT) { | 434 | } else if(w == EcorePackage.Literals.EDOUBLE || w == EcorePackage.Literals.EFLOAT) { |
324 | return builder.LogicReal | 435 | return builder.LogicReal |
325 | } else if(w == EcorePackage.Literals.EBOOLEAN) { | 436 | } else if(w == EcorePackage.Literals.EBOOLEAN) { |
326 | return builder.LogicBool | 437 | return builder.LogicBool |
438 | } else if(w == EcorePackage.Literals.ESTRING) { | ||
439 | return builder.LogicString | ||
327 | } else if(w instanceof EEnum) { | 440 | } else if(w instanceof EEnum) { |
328 | this.ecore2Logic.TypeofEEnum(ecore2LogicTrace.trace,w); | 441 | val c = this.ecore2Logic.TypeofEEnum(ecore2LogicTrace.trace,w) |
442 | return builder.toTypeReference(c); | ||
329 | } else throw new UnsupportedOperationException('''Unknown reference type «w.class.name»''') | 443 | } else throw new UnsupportedOperationException('''Unknown reference type «w.class.name»''') |
330 | } | 444 | } |
445 | def dispatch TypeReference transformTypeReference(JavaTransitiveInstancesKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { | ||
446 | val c = k.wrapperInstanceClass | ||
447 | if(c == Integer || c == Long || c == Short) { | ||
448 | return LogicInt | ||
449 | } else if(c == Float || c == Double) { | ||
450 | return LogicReal | ||
451 | } else if(c == Boolean) { | ||
452 | return LogicBool | ||
453 | } else if(c.superclass == java.lang.Enum){ | ||
454 | val enums = ecore2Logic.allEnumsInScope(ecore2LogicTrace.trace) | ||
455 | for(enum : enums) { | ||
456 | if(c == enum.instanceClass) { | ||
457 | return builder.toTypeReference(ecore2Logic.TypeofEEnum(ecore2LogicTrace.trace,enum)) | ||
458 | } | ||
459 | } | ||
460 | throw new IllegalArgumentException('''Enum type «c.simpleName» is not mapped to logic!''') | ||
461 | } | ||
462 | return null | ||
463 | } | ||
464 | def dispatch TypeReference transformTypeReference(EClassTransitiveInstancesKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { | ||
465 | val c = k.wrappedKey | ||
466 | |||
467 | if(this.ecore2Logic.allClassesInScope(ecore2LogicTrace.trace).toList.contains(c)) { | ||
468 | return builder.toTypeReference(this.ecore2Logic.TypeofEClass(ecore2LogicTrace.trace,k.wrappedKey)) | ||
469 | } else { | ||
470 | return null | ||
471 | } | ||
472 | } | ||
473 | def dispatch TypeReference transformTypeReference(EClassUnscopedTransitiveInstancesKey k, TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { | ||
474 | val c = k.wrappedKey | ||
475 | |||
476 | if(this.ecore2Logic.allClassesInScope(ecore2LogicTrace.trace).toList.contains(c)) { | ||
477 | return builder.toTypeReference(this.ecore2Logic.TypeofEClass(ecore2LogicTrace.trace,k.wrappedKey)) | ||
478 | } else { | ||
479 | return null | ||
480 | } | ||
481 | } | ||
331 | 482 | ||
332 | def dispatch transformTypeReference(EClassTransitiveInstancesKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { | 483 | def dispatch TypeReference transformTypeReference(IInputKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) { |
333 | this.ecore2Logic.TypeofEClass(ecore2LogicTrace.trace,k.wrappedKey) | 484 | println(k) |
485 | throw new IllegalArgumentException('''Unsupported type: «k.class.simpleName»''') | ||
334 | } | 486 | } |
335 | 487 | ||
336 | def boolean isPositiveVariable(PVariable v) { | 488 | def boolean isPositiveVariable(PVariable v) { |