aboutsummaryrefslogtreecommitdiffstats
path: root/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu
diff options
context:
space:
mode:
authorLibravatar Oszkar Semerath <semerath@mit.bme.hu>2019-07-15 17:31:00 +0200
committerLibravatar Oszkar Semerath <semerath@mit.bme.hu>2019-07-15 17:31:00 +0200
commit539618ccaedfe05d5d62971c8fd0578f5ff3d040 (patch)
tree43d07de9773db3bc6ab71021c530b205680315c4 /Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu
parentaggregated partial substitution + builder (diff)
downloadVIATRA-Generator-539618ccaedfe05d5d62971c8fd0578f5ff3d040.tar.gz
VIATRA-Generator-539618ccaedfe05d5d62971c8fd0578f5ff3d040.tar.zst
VIATRA-Generator-539618ccaedfe05d5d62971c8fd0578f5ff3d040.zip
parsing count, min, max, check and eval v1
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu')
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Constraint2Logic.xtend69
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend132
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2Logic.xtend328
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeInferer.xtend392
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeResult.xtend47
-rw-r--r--Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/XExpressionExtractor.xtend24
6 files changed, 727 insertions, 265 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Constraint2Logic.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Constraint2Logic.xtend
index 3e8b3366..ffbca0af 100644
--- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Constraint2Logic.xtend
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Constraint2Logic.xtend
@@ -30,10 +30,20 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeCo
30 30
31import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 31import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
32import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint 32import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.TypeFilterConstraint
33import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.AggregatorConstraint
34import org.eclipse.viatra.query.runtime.matchers.aggregators.DoubleSumOperator
35import org.eclipse.viatra.query.runtime.matchers.aggregators.IntegerSumOperator
36import org.eclipse.viatra.query.runtime.matchers.aggregators.LongSumOperator
37import org.eclipse.viatra.query.runtime.matchers.aggregators.ExtremumOperator
38import org.eclipse.viatra.query.runtime.matchers.aggregators.ExtremumOperator.Extreme
39import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.PatternMatchCounter
40import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
33 41
34class Constraint2Logic { 42class Constraint2Logic {
35 val extension LogicProblemBuilder builder = new LogicProblemBuilder 43 val extension LogicProblemBuilder builder = new LogicProblemBuilder
36 val Ecore2Logic ecore2Logic 44 val Ecore2Logic ecore2Logic
45 val ExpressionEvaluation2Logic expressionEvaliation2Logic = new ExpressionEvaluation2Logic
46 val expressionExtractor = new XExpressionExtractor
37 47
38 new(Ecore2Logic ecore2Logic) { 48 new(Ecore2Logic ecore2Logic) {
39 this.ecore2Logic = ecore2Logic 49 this.ecore2Logic = ecore2Logic
@@ -269,6 +279,65 @@ class Constraint2Logic {
269 } else throw new IllegalArgumentException('''unknown tuple: «tuple»''') 279 } else throw new IllegalArgumentException('''unknown tuple: «tuple»''')
270 } 280 }
271 281
282 def dispatch Term transformConstraint(AggregatorConstraint constraint,
283 TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace,
284 Viatra2LogicTrace viatra2LogicTrace,
285 Map<PVariable, Variable> variable2Variable,
286 Viatra2LogicConfiguration config)
287 {
288 val logicReferred = constraint.referredQuery.lookup(viatra2LogicTrace.query2Relation)
289 val parameterSubstitution = new LinkedList
290 for(index : 0..<constraint.actualParametersTuple.size) {
291 val term = (constraint.actualParametersTuple.get(index) as PVariable).lookup(variable2Variable)
292 parameterSubstitution += term
293 }
294 val aggregatorIndex = constraint.aggregatedColumn
295 val logicResultVariable = constraint.resultVariable.lookup(variable2Variable)
296 val type = constraint.aggregator.operator
297 if(type === null) {
298 return Count(logicReferred,parameterSubstitution,logicResultVariable)
299 } else if(type instanceof IntegerSumOperator || type instanceof DoubleSumOperator || type instanceof LongSumOperator){
300 return Sum(logicReferred,parameterSubstitution,aggregatorIndex,logicResultVariable)
301 } else if(type instanceof ExtremumOperator) {
302 if(type.name == Extreme.MIN.name.toLowerCase) {
303 return Min(logicReferred,parameterSubstitution,aggregatorIndex,logicResultVariable)
304 } else if(type.name == Extreme.MAX.name.toLowerCase){
305 return Max(logicReferred,parameterSubstitution,aggregatorIndex,logicResultVariable)
306 } else {
307 throw new UnsupportedOperationException('''Unkown Extremum aggregator type: «type.name»''')
308 }
309 } else {
310 throw new UnsupportedOperationException('''Unkown aggregator type: «type.name»''')
311 }
312 }
313
314 def dispatch Term transformConstraint(PatternMatchCounter constraint,
315 TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace,
316 Viatra2LogicTrace viatra2LogicTrace,
317 Map<PVariable, Variable> variable2Variable,
318 Viatra2LogicConfiguration config)
319 {
320 val logicReferred = constraint.referredQuery.lookup(viatra2LogicTrace.query2Relation)
321 val parameterSubstitution = new LinkedList
322 for(index : 0..<constraint.actualParametersTuple.size) {
323 val term = (constraint.actualParametersTuple.get(index) as PVariable).lookup(variable2Variable)
324 parameterSubstitution += term
325 }
326 val logicResultVariable = constraint.resultVariable.lookup(variable2Variable)
327 return Count(logicReferred,parameterSubstitution,logicResultVariable)
328 }
329
330 def dispatch Term transformConstraint(ExpressionEvaluation constraint,
331 TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace,
332 Viatra2LogicTrace viatra2LogicTrace,
333 Map<PVariable, Variable> variable2Variable,
334 Viatra2LogicConfiguration config)
335 {
336 val outputVariable = constraint.outputVariable
337 val expression = expressionExtractor.extractExpression(constraint.evaluator)
338 return expressionEvaliation2Logic.transformEval(outputVariable,expression,variable2Variable)
339 }
340
272 def dispatch Term transformConstraint(PConstraint constraint, 341 def dispatch Term transformConstraint(PConstraint constraint,
273 TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, 342 TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace,
274 Viatra2LogicTrace viatra2LogicTrace, 343 Viatra2LogicTrace viatra2LogicTrace,
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend
new file mode 100644
index 00000000..f474ded4
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend
@@ -0,0 +1,132 @@
1package hu.bme.mit.inf.dslreasoner.viatra2logic
2
3import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
4import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
5import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
6import java.util.Map
7import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
8import org.eclipse.xtext.xbase.XBinaryOperation
9import org.eclipse.xtext.xbase.XExpression
10import org.eclipse.xtext.xbase.XFeatureCall
11import org.eclipse.xtext.xbase.XMemberFeatureCall
12import org.eclipse.xtext.xbase.XNumberLiteral
13import org.eclipse.xtext.xbase.XUnaryOperation
14
15import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
16
17class ExpressionEvaluation2Logic {
18 val extension LogicProblemBuilder builder = new LogicProblemBuilder
19
20 def Term transformCheck(XExpression expression, Map<PVariable, Variable> variable2Variable) {
21 return expression.transform(variable2Variable)
22 }
23 def Term transformEval(PVariable target, XExpression expression, Map<PVariable, Variable> variable2Variable) {
24 return target.lookup(variable2Variable) == expression.transform(variable2Variable)
25 }
26
27 static val N_Base = "org.eclipse.xtext.xbase.lib."
28
29 static val N_PLUS1 = "operator_plus"
30 static val N_MINUS1 = "operator_minus"
31
32 static val N_MINUS2 = "operator_minus"
33 static val N_PLUS2 = "operator_plus"
34 static val N_POWER = "operator_power"
35 static val N_MULTIPLY = "operator_multiply"
36 static val N_DIVIDE = "operator_divide"
37 static val N_MODULO = "operator_modulo"
38 static val N_LESSTHAN = "operator_lessThan"
39 static val N_LESSEQUALSTHAN = "operator_lessEqualsThan"
40 static val N_GREATERTHAN = "operator_greaterThan"
41 static val N_GREATEREQUALTHAN = "operator_greaterEqualsThan"
42 static val N_EQUALS = "operator_equals"
43 static val N_NOTEQUALS = "operator_notEquals"
44 static val N_EQUALS3 = "operator_tripleEquals"
45 static val N_NOTEQUALS3 = "operator_tripleNotEquals"
46
47
48
49 protected def isN(String name, String s) {
50 val res = name.startsWith(N_Base) && name.endsWith(s)
51 //println('''[«res»] «name» ?= «N_Base»*«s»''')
52 return res
53 }
54
55 static val N_POWER2 = "java.lang.Math.pow"
56
57 def protected dispatch Term transform(XBinaryOperation e, Map<PVariable, Variable> variable2Variable) {
58 val left = e.leftOperand.transform(variable2Variable)
59 val right = e.rightOperand.transform(variable2Variable)
60 val feature = e.feature.qualifiedName
61 if(feature.isN(N_MINUS2)) { return Minus(left,right) }
62 else if(feature.isN(N_PLUS2)) { return Plus(left,right) }
63 else if(feature.isN(N_POWER)) { return Pow(left,right) }
64 else if(feature.isN(N_MULTIPLY)) { return Multiply(left,right) }
65 else if(feature.isN(N_DIVIDE)) { return Divide(left,right) }
66 else if(feature.isN(N_MODULO)) { return Modulo(left,right) }
67 else if(feature.isN(N_LESSTHAN)) { return LessThan(left,right) }
68 else if(feature.isN(N_LESSEQUALSTHAN)) { return LessOrEqual(left,right) }
69 else if(feature.isN(N_GREATERTHAN)) { return MoreThan(left,right) }
70 else if(feature.isN(N_GREATEREQUALTHAN)) { return MoreOrEqual(left,right) }
71 else if(feature.isN(N_EQUALS)) { return Equals(left,right) }
72 else if(feature.isN(N_NOTEQUALS)) { return Distinct(left,right) }
73 else if(feature.isN(N_EQUALS3)) { return Equals(left,right) }
74 else if(feature.isN(N_NOTEQUALS3)) { return Distinct(left,right) }
75 else {
76 println("-> " + e.feature+","+e.class)
77 println("-> " + e.leftOperand)
78 println("-> " + e.rightOperand)
79 println("-> " + e.feature.qualifiedName)
80 throw new UnsupportedOperationException('''Unsupported binary operator feature: "«e.feature.class.simpleName»" - «e»''')
81 }
82 }
83
84 def protected dispatch Term transform(XUnaryOperation e, Map<PVariable, Variable> variable2Variable) {
85 val operand = e.operand.transform(variable2Variable)
86 val feature = e.feature.qualifiedName
87 if(feature.isN(N_MINUS1)) { return Minus(0.asTerm,operand)}
88 else if(feature.isN(N_PLUS1)) { return operand}
89 else{
90 println("-> " + e.feature+","+e.class)
91 println("-> " + e.operand)
92 println("-> " + e.feature.qualifiedName)
93 throw new UnsupportedOperationException('''Unsupported unary operator feature: "«e.feature.class.simpleName»" - «e»''')
94 }
95 }
96
97 def protected dispatch Term transform(XMemberFeatureCall e, Map<PVariable, Variable> variable2Variable) {
98 val transformedArguments = e.actualArguments.map[transform(variable2Variable)]
99 val feature = e.feature.qualifiedName
100 if(feature == N_POWER2) {
101 return Pow(transformedArguments.get(0),transformedArguments.get(1))
102 }else {
103 println(e.feature+","+e.class)
104 println(e.actualArguments.join(", "))
105 println(e.feature.qualifiedName)
106 throw new UnsupportedOperationException('''Unsupported feature call: "«e.feature.qualifiedName»" - «e»''')
107 }
108 }
109
110 def protected dispatch Term transform(XFeatureCall e, Map<PVariable,Variable> variable2Variable) {
111 val featureName = e.feature.qualifiedName
112 val entryWithName = variable2Variable.entrySet.filter[it.key.name == featureName].head
113 if(entryWithName !== null) {
114 return entryWithName.value.toTerm
115 } else {
116 throw new IllegalArgumentException('''Feature call reference to unavailable variable "«featureName»"''')
117 }
118 }
119
120 def protected dispatch Term transform(XNumberLiteral l, Map<PVariable, Variable> variable2Variable) {
121 val s = l.value
122 try{ return Integer.parseInt(s).asTerm } catch(NumberFormatException e){}
123 try{ return Short.parseShort(s).asTerm } catch(NumberFormatException e){}
124 try{ return Double.parseDouble(s).asTerm } catch(NumberFormatException e){}
125 try{ return Float.parseFloat(s).asTerm } catch(NumberFormatException e){}
126 throw new UnsupportedOperationException('''Unsupported numeric type: "«s»"''')
127 }
128
129 def protected dispatch Term transform(XExpression e, Map<PVariable, Variable> variable2Variable) {
130 throw new UnsupportedOperationException('''Unsupported expression: "«e.class.simpleName»" - «e»''')
131 }
132} \ No newline at end of file
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 3b828170..0f97d3fe 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,48 +4,36 @@ import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
4import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace 4import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
5import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder 5import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
6import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput 6import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition 7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition
10import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable 8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
13import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem 9import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
14import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery 10import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.TransfomedViatraQuery
15import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsFactory 11import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsFactory
16import java.util.ArrayList 12import java.util.ArrayList
17import java.util.HashMap 13import java.util.HashMap
18import java.util.HashSet
19import java.util.LinkedList 14import java.util.LinkedList
20import java.util.List 15import java.util.List
21import java.util.Map 16import java.util.Map
22import java.util.Set 17import java.util.Set
23import org.eclipse.emf.ecore.EAttribute 18import org.eclipse.emf.ecore.EAttribute
24import org.eclipse.emf.ecore.EClassifier
25import org.eclipse.emf.ecore.EEnum
26import org.eclipse.emf.ecore.EReference 19import org.eclipse.emf.ecore.EReference
27import org.eclipse.emf.ecore.EStructuralFeature 20import org.eclipse.emf.ecore.EStructuralFeature
28import org.eclipse.emf.ecore.EcorePackage 21import org.eclipse.emf.ecore.util.EcoreUtil
29import org.eclipse.viatra.query.runtime.api.IQuerySpecification 22import org.eclipse.viatra.query.runtime.api.IQuerySpecification
30import org.eclipse.viatra.query.runtime.emf.EMFQueryMetaContext 23import org.eclipse.viatra.query.runtime.emf.EMFQueryMetaContext
31import org.eclipse.viatra.query.runtime.emf.types.BaseEMFTypeKey
32import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey
33import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey
34import org.eclipse.viatra.query.runtime.matchers.context.IInputKey
35import org.eclipse.viatra.query.runtime.matchers.context.common.JavaTransitiveInstancesKey
36import org.eclipse.viatra.query.runtime.matchers.planning.helpers.TypeHelper
37import org.eclipse.viatra.query.runtime.matchers.psystem.PBody 24import org.eclipse.viatra.query.runtime.matchers.psystem.PBody
25import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint
38import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable 26import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
27import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.AggregatorConstraint
39import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall 28import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.NegativePatternCall
29import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.PatternMatchCounter
30import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction
40import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter 31import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter
41import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery 32import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
42import org.eclipse.viatra.query.runtime.matchers.psystem.rewriters.PBodyNormalizer 33import org.eclipse.viatra.query.runtime.matchers.psystem.rewriters.PBodyNormalizer
43import org.eclipse.xtend.lib.annotations.Data 34import org.eclipse.xtend.lib.annotations.Data
44 35
45import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 36import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
46import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PDisjunction
47import org.eclipse.emf.ecore.util.EcoreUtil
48import org.eclipse.viatra.query.runtime.emf.types.EClassUnscopedTransitiveInstancesKey
49 37
50@Data class ViatraQuerySetDescriptor { 38@Data class ViatraQuerySetDescriptor {
51 val List<? extends IQuerySpecification<?>> patterns 39 val List<? extends IQuerySpecification<?>> patterns
@@ -57,24 +45,24 @@ class Viatra2LogicTrace {
57 public val Map<PQuery, RelationDefinition> query2Relation = new HashMap 45 public val Map<PQuery, RelationDefinition> query2Relation = new HashMap
58 public val Map<PQuery, TransfomedViatraQuery> query2Annotation = new HashMap 46 public val Map<PQuery, TransfomedViatraQuery> query2Annotation = new HashMap
59 public val Map<Pair<PQuery,PParameter>, Variable> parameter2Variable = new HashMap 47 public val Map<Pair<PQuery,PParameter>, Variable> parameter2Variable = new HashMap
60 //public val Map<PVariable, Variable> variable2Variable = new HashMap
61} 48}
62class Viatra2LogicConfiguration { 49class Viatra2LogicConfiguration {
63 public var normalize = true 50 public var normalize = true
64 public var transitiveClosureDepth = 3
65} 51}
66 52
67class Viatra2Logic { 53class Viatra2Logic {
68 val extension LogicProblemBuilder builder = new LogicProblemBuilder 54 val extension LogicProblemBuilder builder = new LogicProblemBuilder
69 val extension Viatra2LogicAnnotationsFactory factory = Viatra2LogicAnnotationsFactory.eINSTANCE 55 val extension Viatra2LogicAnnotationsFactory factory = Viatra2LogicAnnotationsFactory.eINSTANCE
70 val normalizer = new PBodyNormalizer(EMFQueryMetaContext.DEFAULT) 56 val normalizer = new PBodyNormalizer(EMFQueryMetaContext.DEFAULT)
57 val Viatra2LogicTypeInferer typeInferer
71 58
72 val Ecore2Logic ecore2Logic 59 val Ecore2Logic ecore2Logic
73 Constraint2Logic constraint2Logic 60 Constraint2Logic constraint2Logic
74 61
75 new(Ecore2Logic ecore2Logic) { 62 new(Ecore2Logic ecore2Logic) {
76 this.ecore2Logic = ecore2Logic 63 this.ecore2Logic = ecore2Logic
77 constraint2Logic = new Constraint2Logic(ecore2Logic) 64 this.typeInferer = new Viatra2LogicTypeInferer(ecore2Logic)
65 this.constraint2Logic = new Constraint2Logic(ecore2Logic)
78 } 66 }
79 67
80 def TracedOutput<LogicProblem,Viatra2LogicTrace> transformQueries( 68 def TracedOutput<LogicProblem,Viatra2LogicTrace> transformQueries(
@@ -82,65 +70,55 @@ class Viatra2Logic {
82 TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, 70 TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace,
83 Viatra2LogicConfiguration config) 71 Viatra2LogicConfiguration config)
84 { 72 {
73 // Create trace
85 val viatra2LogicTrace = new Viatra2LogicTrace 74 val viatra2LogicTrace = new Viatra2LogicTrace
86 val typeAlanysis = new HashMap 75
76 // Translation works on PQueries. QuerySpecification -> PQuery.
87 val pQueries = queries.patterns.map[it.internalQueryRepresentation] 77 val pQueries = queries.patterns.map[it.internalQueryRepresentation]
88 78
89 for(query: pQueries) { 79 // If requested, the queries are normalized
90 val disjunction = normalizer.rewrite(query) 80 for(query: pQueries) {
81 val disjunction = normalizer.rewrite(query)
91 viatra2LogicTrace.query2Disjunction.put(query,disjunction) 82 viatra2LogicTrace.query2Disjunction.put(query,disjunction)
92 } 83 }
93 84
94 for(query: pQueries) { 85 // The types are calculated
95 val types = query.lookup(viatra2LogicTrace.query2Disjunction).bodies.toInvertedMap[ 86 val types = typeInferer.inferTypes(pQueries,ecore2LogicTrace,viatra2LogicTrace)
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 87
88 // First, the signature of the queries are translated, ...
112 for(query: pQueries) { 89 for(query: pQueries) {
113 try { 90 try {
114 this.transformQueryHeader(query,query.lookup(typeAlanysis),ecore2LogicTrace,viatra2LogicTrace,config) 91 this.transformQueryHeader(query,types,ecore2LogicTrace,viatra2LogicTrace,config)
115 } catch(IllegalArgumentException e) { 92 } catch(IllegalArgumentException e) {
116 throw new IllegalArgumentException(''' 93 throw new IllegalArgumentException('''
117 Unable to translate query "«query.fullyQualifiedName»". 94 Unable to translate query "«query.fullyQualifiedName»".
118 Reason: «e.class.simpleName», «e.message»''',e) 95 Reason: «e.class.simpleName», «e.message»''',e)
119 } 96 }
120 } 97 }
98
99 // ...then the bodies, ...
121 for(query: pQueries) { 100 for(query: pQueries) {
122 try { 101 try {
123 this.transformQuerySpecification(query,query.lookup(typeAlanysis),ecore2LogicTrace,viatra2LogicTrace,config) 102 this.transformQuerySpecification(query,types,ecore2LogicTrace,viatra2LogicTrace,config)
124 } catch (IllegalArgumentException e){ 103 } catch (IllegalArgumentException e){
125 throw new IllegalArgumentException(''' 104 throw new IllegalArgumentException('''
126 Unable to translate query "«query.fullyQualifiedName»". 105 Unable to translate query "«query.fullyQualifiedName»".
127 Reason: «e.class.simpleName», «e.message»''',e) 106 Reason: «e.class.simpleName», «e.message»''',e)
128 } 107 }
129 } 108 }
130 /*for(d : viatra2LogicTrace.query2Relation.values) {
131 checkDefinition(d)
132 }*/
133 109
110 // ... and finally, the annotations.
134 transformQueryConstraints( 111 transformQueryConstraints(
135 queries.validationPatterns.map[internalQueryRepresentation], 112 queries.validationPatterns.map[internalQueryRepresentation],
136 queries.derivedFeatures, 113 queries.derivedFeatures,
137 ecore2LogicTrace,viatra2LogicTrace) 114 ecore2LogicTrace,viatra2LogicTrace)
115
138 return new TracedOutput(ecore2LogicTrace.output,viatra2LogicTrace) 116 return new TracedOutput(ecore2LogicTrace.output,viatra2LogicTrace)
139 } 117 }
140 118
141 def protected transformQueryHeader( 119 def protected transformQueryHeader(
142 PQuery pquery, 120 PQuery pquery,
143 Map<PBody, Map<PVariable, Set<IInputKey>>> types, 121 Viatra2LogicTypeResult types,
144 TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, 122 TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace,
145 Viatra2LogicTrace viatra2LogicTrace, 123 Viatra2LogicTrace viatra2LogicTrace,
146 Viatra2LogicConfiguration config) 124 Viatra2LogicConfiguration config)
@@ -149,7 +127,7 @@ class Viatra2Logic {
149 val parameters = new ArrayList<Variable>(pquery.parameters.size) 127 val parameters = new ArrayList<Variable>(pquery.parameters.size)
150 for(vParam: pquery.parameters) { 128 for(vParam: pquery.parameters) {
151 val parameterName = '''parameter «vParam.name»''' 129 val parameterName = '''parameter «vParam.name»'''
152 val parameterType = getType(vParam,types,ecore2LogicTrace) 130 val parameterType = types.getType(pquery,vParam)
153 if(parameterType === null) { 131 if(parameterType === null) {
154 throw new AssertionError('''null type for parameter «vParam.name» in pattern «pquery.fullyQualifiedName»''') 132 throw new AssertionError('''null type for parameter «vParam.name» in pattern «pquery.fullyQualifiedName»''')
155 } 133 }
@@ -175,7 +153,7 @@ class Viatra2Logic {
175 153
176 def protected transformQuerySpecification( 154 def protected transformQuerySpecification(
177 PQuery pquery, 155 PQuery pquery,
178 Map<PBody, Map<PVariable, Set<IInputKey>>> types, 156 Viatra2LogicTypeResult types,
179 TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, 157 TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace,
180 Viatra2LogicTrace viatra2LogicTrace, 158 Viatra2LogicTrace viatra2LogicTrace,
181 Viatra2LogicConfiguration config) 159 Viatra2LogicConfiguration config)
@@ -233,7 +211,7 @@ class Viatra2Logic {
233 } 211 }
234 212
235 def transformBody(PBody body, 213 def transformBody(PBody body,
236 Map<PBody, Map<PVariable, Set<IInputKey>>> types, 214 Viatra2LogicTypeResult types,
237 TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, 215 TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace,
238 Viatra2LogicTrace viatra2LogicTrace, 216 Viatra2LogicTrace viatra2LogicTrace,
239 Viatra2LogicConfiguration config) 217 Viatra2LogicConfiguration config)
@@ -248,19 +226,29 @@ class Viatra2Logic {
248 // Inner Variables 226 // Inner Variables
249 val innerPositiveVariables = new LinkedList 227 val innerPositiveVariables = new LinkedList
250 val innerNegativeVariables = new LinkedList 228 val innerNegativeVariables = new LinkedList
229 val innerAggreatedVariables = new LinkedList
230 //println(body.uniqueVariables)
251 for(innerVariable : body.uniqueVariables) { 231 for(innerVariable : body.uniqueVariables) {
252 232
253 if(!variable2Variable.containsKey(innerVariable)) { 233 if(!variable2Variable.containsKey(innerVariable)) {
254 val name = '''variable «innerVariable.name.normalizeName»''' 234 if(innerVariable.aggregateOnly) {
255 //println(body.pattern.fullyQualifiedName + "-") 235 // do not create variable
256 val logicType = getType(innerVariable,types,ecore2LogicTrace) 236 innerAggreatedVariables.add(innerVariable)
257 val logicVariable = createVar(name,logicType) 237 variable2Variable.put(innerVariable,null)
258 if(innerVariable.isPositiveVariable) {
259 innerPositiveVariables += logicVariable
260 } else { 238 } else {
261 innerNegativeVariables += logicVariable 239 val name = '''variable «innerVariable.name.normalizeName»'''
240 val logicType = types.getType(body,innerVariable)
241 if(logicType === null) {
242 throw new IllegalArgumentException('''Variable «innerVariable.name.normalizeName» has no type!''')
243 }
244 val logicVariable = createVar(name,logicType)
245 if(innerVariable.negativeOnly) {
246 innerNegativeVariables += logicVariable
247 } else {
248 innerPositiveVariables += logicVariable
249 }
250 variable2Variable.put(innerVariable,logicVariable)
262 } 251 }
263 variable2Variable.put(innerVariable,logicVariable)
264 } 252 }
265 } 253 }
266 254
@@ -282,226 +270,36 @@ class Viatra2Logic {
282 270
283 return allVariablesAreExisting 271 return allVariablesAreExisting
284 } 272 }
285// def toTypeJudgement(PVariable v, IInputKey key) {
286// new TypeJudgement(key,new Tuple1)
287// }
288 273
289 def private normalizeName(String variableName) { 274 def private normalizeName(String variableName) {
290 return variableName.replaceAll("[\\W]|_", "") 275 return variableName.replaceAll("[\\W]|_", "")
291 } 276 }
292
293 /**
294 * Translates the type of a parameter variable in a pattern
295 */
296 def TypeReference getType(PParameter v, Map<PBody, Map<PVariable, Set<IInputKey>>> types, TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) {
297 // If parameter type is specified then the specified type is used
298 if(v.declaredUnaryType !== null) {
299 val res = transformTypeReference(v.declaredUnaryType,ecore2LogicTrace)
300 if(res === null) {
301 throw new AssertionError('''
302 Unable to translate declared type «v.declaredUnaryType».
303 ''')
304 } else {
305 return res
306 }
307 }
308 // Otherwise, calculate the type based on the type of the variable in the bodies
309 else {
310 val bodies = types.keySet
311 val typesFromBodies = new ArrayList(bodies.size)
312 for(body : bodies) {
313 // collect the variable in the body
314 val exported = body.symbolicParameters.filter[it.patternParameter === v]
315 if(exported.size !== 1) {
316 throw new AssertionError('''Parameter «v.name» has no reference in body!''')
317 }
318 val variable = exported.head.parameterVariable
319 typesFromBodies+=variable.getType(types,ecore2LogicTrace)
320 }
321 return typesFromBodies.calculateCommonSupertype
322 }
323 }
324
325 /**
326 * Translates the type of a variable in a pattern body
327 */
328 def TypeReference getType(PVariable v, Map<PBody, Map<PVariable, Set<IInputKey>>> types ,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) {
329 if (v.isPositiveVariable) {
330 val keys = getTypesFromCollection(v,types)
331 val logicTypes = keys.map[transformTypeReference(it,ecore2LogicTrace)].filterNull
332 return logicTypes.calculateCommonSubtype
333 } else {
334 val onlyConstraint = v.referringConstraints.head as NegativePatternCall
335 val indexOfVariable = v.lookup(onlyConstraint.actualParametersTuple.invertIndex)
336 val parameter = onlyConstraint.referredQuery.parameters.get(indexOfVariable)
337 val declaredUnaryType = parameter.declaredUnaryType as BaseEMFTypeKey<? extends EClassifier>
338 if (declaredUnaryType === null) {
339 throw new UnsupportedOperationException(
340 '''parameter «parameter.name» in pattern «onlyConstraint.referredQuery.fullyQualifiedName» does not have type!''')
341 } else
342 return declaredUnaryType.transformTypeReference(ecore2LogicTrace)
343 }
344 }
345
346 def getTypesFromCollection(PVariable v, Map<PBody, Map<PVariable, Set<IInputKey>>> types) {
347 for(entry : types.entrySet) {
348 if(entry.key.uniqueVariables.contains(v)) {
349 return v.lookup(entry.value)
350 }
351 }
352 throw new IllegalArgumentException('''Variable «v.name» is not present in neither of the bodies!''')
353 }
354
355 277
356 def TypeReference calculateCommonSubtype(Iterable<TypeReference> types) { 278 def isNegativeOnly(PVariable variable) {
357 val primitiveTypeReferences = types.filter(PrimitiveTypeReference) 279 if(variable.referringConstraints.size == 1) {
358 val complexTypeReferences = types.filter(ComplexTypeReference) 280 val PConstraint onlyConstraint = variable.referringConstraints.head
359 if(complexTypeReferences.isEmpty) { 281 if(onlyConstraint instanceof NegativePatternCall) {
360 val head = primitiveTypeReferences.head 282 return true
361 if(primitiveTypeReferences.exists[it.eClass !== head.eClass]) { 283 } else {
362 throw new IllegalArgumentException('''Inconsistent types: «primitiveTypeReferences.map[eClass.name].toSet.toList»''') 284 return false
363 }
364 return head
365 } else if(primitiveTypeReferences.isEmpty) {
366 val complexTypes = complexTypeReferences.map[it.referred].toSet
367 if(complexTypes.size === 1) {
368 return builder.toTypeReference(complexTypes.head)
369 }
370 // Collect possible subtypes
371 val subtypeSets = complexTypes.map[it.transitiveClosureStar[it.subtypes].toSet]
372 val commonTypeSet = new HashSet(subtypeSets.head)
373 val otherSets = subtypeSets.tail
374 for(otherSet : otherSets) {
375 commonTypeSet.retainAll(otherSet)
376 }
377 if(commonTypeSet.empty) {
378 throw new IllegalArgumentException('''Inconsistent types: «complexTypes.map[name].toList»''')
379 }
380
381 return calculateCommonComplexSupertype(commonTypeSet)
382
383 } else {
384 throw new IllegalArgumentException('''
385 Inconsistent types, mixing primitive and complex types:
386 «primitiveTypeReferences.map[eClass.name].toSet.toList»
387 and
388 «complexTypeReferences.map[it.referred].toSet.map[name].toList»''')
389
390 }
391 }
392 def TypeReference calculateCommonSupertype(Iterable<TypeReference> types) {
393 val primitiveTypeReferences = types.filter(PrimitiveTypeReference)
394 val complexTypeReferences = types.filter(ComplexTypeReference)
395 if(complexTypeReferences.isEmpty) {
396 val head = primitiveTypeReferences.head
397 if(primitiveTypeReferences.exists[it.eClass !== head.eClass]) {
398 throw new IllegalArgumentException('''Inconsistent types: «primitiveTypeReferences.map[eClass.name].toSet.toList»''')
399 }
400 return head
401 } else if(primitiveTypeReferences.isEmpty) {
402 val complexTypes = complexTypeReferences.map[it.referred].toSet
403 return calculateCommonComplexSupertype(complexTypes)
404
405 } else {
406 throw new IllegalArgumentException('''
407 Inconsistent types, mixing primitive and complex types:
408 «primitiveTypeReferences.map[eClass.name].toSet.toList»
409 and
410 «complexTypeReferences.map[it.referred].toSet.map[name].toList»''')
411
412 }
413 }
414 def TypeReference calculateCommonComplexSupertype(Set<Type> complexTypes) {
415 if(complexTypes.size === 1) {
416 return builder.toTypeReference(complexTypes.head)
417 }
418 // Collect possible supertypes
419 val supertypeSets = complexTypes.map[it.transitiveClosureStar[it.supertypes].toSet]
420 val commonTypeSet = new HashSet(supertypeSets.head)
421 val otherSets = supertypeSets.tail
422 for(otherSet : otherSets) {
423 commonTypeSet.retainAll(otherSet)
424 }
425 if(commonTypeSet.empty) {
426 throw new IllegalArgumentException('''Inconsistent types: «complexTypes.map[name].toList»''')
427 }
428 // Remove type that already have covered
429 val coveredTypes = commonTypeSet.map[it.supertypes].flatten
430 commonTypeSet.removeAll(coveredTypes)
431 return builder.toTypeReference(commonTypeSet.head)
432 }
433
434 /**
435 * Transforms a Viatra type reference to a logic type.
436 */
437 def dispatch TypeReference transformTypeReference(EDataTypeInSlotsKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) {
438 val w = k.wrappedKey
439 if(w == EcorePackage.Literals.EINT || w == EcorePackage.Literals.ESHORT || w == EcorePackage.Literals.ELONG) {
440 return builder.LogicInt
441 } else if(w == EcorePackage.Literals.EDOUBLE || w == EcorePackage.Literals.EFLOAT) {
442 return builder.LogicReal
443 } else if(w == EcorePackage.Literals.EBOOLEAN) {
444 return builder.LogicBool
445 } else if(w == EcorePackage.Literals.ESTRING) {
446 return builder.LogicString
447 } else if(w instanceof EEnum) {
448 val c = this.ecore2Logic.TypeofEEnum(ecore2LogicTrace.trace,w)
449 return builder.toTypeReference(c);
450 } else throw new UnsupportedOperationException('''Unknown reference type «w.class.name»''')
451 }
452 def dispatch TypeReference transformTypeReference(JavaTransitiveInstancesKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) {
453 val c = k.wrapperInstanceClass
454 if(c == Integer || c == Long || c == Short) {
455 return LogicInt
456 } else if(c == Float || c == Double) {
457 return LogicReal
458 } else if(c == Boolean) {
459 return LogicBool
460 } else if(c == String) {
461 return LogicString
462 } else if(c.superclass == java.lang.Enum){
463 val enums = ecore2Logic.allEnumsInScope(ecore2LogicTrace.trace)
464 for(enum : enums) {
465 if(c == enum.instanceClass) {
466 return builder.toTypeReference(ecore2Logic.TypeofEEnum(ecore2LogicTrace.trace,enum))
467 }
468 } 285 }
469 throw new IllegalArgumentException('''Enum type «c.simpleName» is not mapped to logic!''')
470 }
471 return null
472 }
473 def dispatch TypeReference transformTypeReference(EClassTransitiveInstancesKey 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 { 286 } else {
479 return null 287 return false
480 } 288 }
481 } 289 }
482 def dispatch TypeReference transformTypeReference(EClassUnscopedTransitiveInstancesKey k, TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) {
483 val c = k.wrappedKey
484
485 if(this.ecore2Logic.allClassesInScope(ecore2LogicTrace.trace).toList.contains(c)) {
486 return builder.toTypeReference(this.ecore2Logic.TypeofEClass(ecore2LogicTrace.trace,k.wrappedKey))
487 } else {
488 return null
489 }
490 }
491
492 def dispatch TypeReference transformTypeReference(IInputKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) {
493 //println(k)
494 throw new IllegalArgumentException('''Unsupported type: «k.class.simpleName»''')
495 }
496 290
497 def boolean isPositiveVariable(PVariable v) { 291 def isAggregateOnly(PVariable variable) {
498 val constraints = v.referringConstraints 292 if(variable.referringConstraints.size == 1) {
499 if(constraints.size == 1) { 293 val PConstraint onlyConstraint = variable.referringConstraints.head
500 val onlyConstraint = constraints.head 294 if(onlyConstraint instanceof AggregatorConstraint) {
501 if(onlyConstraint instanceof NegativePatternCall) { 295 return true
296 } else if(onlyConstraint instanceof PatternMatchCounter) {
297 return true
298 } else {
502 return false 299 return false
503 } 300 }
301 } else {
302 return false
504 } 303 }
505 return true
506 } 304 }
507} \ No newline at end of file 305} \ No newline at end of file
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeInferer.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeInferer.xtend
new file mode 100644
index 00000000..b8a6b9c1
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeInferer.xtend
@@ -0,0 +1,392 @@
1package hu.bme.mit.inf.dslreasoner.viatra2logic
2
3import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic
4import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace
5import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder
6import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference
9import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference
10import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference
11import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
13import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
14import java.util.HashMap
15import java.util.HashSet
16import java.util.List
17import java.util.Set
18import org.eclipse.emf.ecore.EEnum
19import org.eclipse.emf.ecore.EcorePackage
20import org.eclipse.viatra.query.patternlanguage.emf.EMFPatternLanguageStandaloneSetup
21import org.eclipse.viatra.query.patternlanguage.emf.specification.XBaseEvaluator
22import org.eclipse.viatra.query.runtime.emf.EMFQueryMetaContext
23import org.eclipse.viatra.query.runtime.emf.types.EClassTransitiveInstancesKey
24import org.eclipse.viatra.query.runtime.emf.types.EClassUnscopedTransitiveInstancesKey
25import org.eclipse.viatra.query.runtime.emf.types.EDataTypeInSlotsKey
26import org.eclipse.viatra.query.runtime.matchers.context.IInputKey
27import org.eclipse.viatra.query.runtime.matchers.context.common.JavaTransitiveInstancesKey
28import org.eclipse.viatra.query.runtime.matchers.planning.helpers.TypeHelper
29import org.eclipse.viatra.query.runtime.matchers.psystem.IExpressionEvaluator
30import org.eclipse.viatra.query.runtime.matchers.psystem.PBody
31import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
32import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.AggregatorConstraint
33import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation
34import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.PatternCallBasedDeferred
35import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.PatternMatchCounter
36import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter
37import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
38import org.eclipse.xtext.xbase.XExpression
39import org.eclipse.xtext.xbase.typesystem.IBatchTypeResolver
40import org.eclipse.xtext.xbase.typesystem.references.UnknownTypeReference
41
42import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
43import org.eclipse.xtext.xbase.typesystem.references.InnerTypeReference
44
45class Viatra2LogicTypeInferer{
46 val Ecore2Logic ecore2Logic
47 val extension LogicProblemBuilder builder = new LogicProblemBuilder
48 /**Typeresolver uses the same resolver as EMFPatternLanguageStandaloneSetup.*/
49 val IBatchTypeResolver typeResolver =
50 (new EMFPatternLanguageStandaloneSetup).createInjector.getInstance(IBatchTypeResolver)
51 val expressionExtractor = new XExpressionExtractor
52
53 new(Ecore2Logic ecore2Logic) {
54 this.ecore2Logic = ecore2Logic
55 }
56
57 def Viatra2LogicTypeResult inferTypes(List<PQuery> pQueries, TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace, Viatra2LogicTrace viatra2LogicTrace) {
58 val Viatra2LogicTypeResult result = new Viatra2LogicTypeResult(new HashMap,new HashMap);
59 for(query : pQueries) {
60 for(body: query.lookup(viatra2LogicTrace.query2Disjunction).bodies) {
61 for(variable : body.uniqueVariables) {
62 getOrMakeTypeDecision(result,variable,body,ecore2LogicTrace,viatra2LogicTrace,emptySet)
63 }
64 }
65 for(parameter: query.parameters) {
66 getOrMakeTypeDecision(result,query,parameter,ecore2LogicTrace,viatra2LogicTrace,emptySet)
67 }
68 }
69 return result
70 }
71
72 private def TypeReference getOrMakeTypeDecision(
73 Viatra2LogicTypeResult result,
74 PVariable variable, PBody body,
75 TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace,
76 Viatra2LogicTrace viatra2LogicTrace,
77 Set<? extends PParameter> checkedInDecisionMaking)
78 {
79 if(result.containsSolution(body,variable)) {
80 return result.getType(body,variable)
81 } else {
82 val inferredTypesByViatra = TypeHelper::inferUnaryTypesFor(body.uniqueVariables, body.constraints, EMFQueryMetaContext.DEFAULT)
83 val constraintsForVariable = variable.lookup(inferredTypesByViatra)
84
85 val typeConstraintsDerivedByTypeHelper = constraintsForVariable.map[transformTypeReference(ecore2LogicTrace)]
86 val typesFromEval = variable.getTypesFromEval(typeResolver)
87 val typesFromAggregatorResult = variable.getTypeFromPassivePatternCallConstraintResult(
88 result,
89 ecore2LogicTrace,
90 viatra2LogicTrace,
91 checkedInDecisionMaking)
92
93 val typesFromPositiveReasoning = (typeConstraintsDerivedByTypeHelper + typesFromEval + typesFromAggregatorResult).filterNull
94
95 val types = if(!typesFromPositiveReasoning.empty) {
96 typesFromPositiveReasoning
97 } else {
98 variable.getTypeFromPassivePatternCallConstraints(
99 result,
100 ecore2LogicTrace,
101 viatra2LogicTrace,
102 checkedInDecisionMaking)
103 }
104
105 val commonSubtype = this.calculateCommonSubtype(types)
106
107 result.addType(body,variable,commonSubtype)
108 return commonSubtype
109 }
110 }
111
112 private def TypeReference getOrMakeTypeDecision(
113 Viatra2LogicTypeResult result,
114 PQuery query,
115 PParameter parameter,
116 TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace,
117 Viatra2LogicTrace viatra2LogicTrace,
118 Set<? extends PParameter> checkedInDecisionMaking)
119 {
120 if(checkedInDecisionMaking.contains(parameter)) {
121 return null
122 }
123 if(result.containsSolution(parameter)) {
124 return result.getType(query, parameter)
125 }
126
127 var TypeReference typeReference;
128
129 if(parameter.declaredUnaryType !== null) {
130 val key = parameter.declaredUnaryType
131 typeReference = key.transformTypeReference(ecore2LogicTrace)
132 } else {
133 val bodies = query.lookup(viatra2LogicTrace.query2Disjunction).bodies
134 val newChecked = new HashSet(checkedInDecisionMaking) => [add(parameter)]
135 val Iterable<TypeReference> variableTypes = bodies.map[body|
136 val symbolicParameter = body.symbolicParameters.filter[patternParameter === parameter].head
137 val variable = symbolicParameter.parameterVariable
138 getOrMakeTypeDecision(result,variable,body,ecore2LogicTrace,viatra2LogicTrace,newChecked)
139 ]
140 typeReference = calculateCommonSupertype(variableTypes)
141 }
142 result.addType(query,parameter,typeReference)
143 return typeReference
144 }
145
146 private def Iterable<? extends TypeReference> getTypesFromEval(PVariable v, IBatchTypeResolver typeResolver) {
147 val constraints = v.getReferringConstraintsOfType(
148 typeof(ExpressionEvaluation)
149 ).filter[
150 it.outputVariable === v
151 ]
152 val res = constraints.map[getTypeFromEval]
153 return res
154 }
155
156 def TypeReference getTypeFromEval(ExpressionEvaluation evaluation) {
157 val XExpression expression = expressionExtractor.extractExpression(evaluation.evaluator)
158 val returnType = typeResolver.resolveTypes(expression).getReturnType(expression);
159 if(returnType === null || returnType instanceof UnknownTypeReference) {
160 return null
161 } else {
162 val javaIdentifier = returnType.wrapperTypeIfPrimitive.javaIdentifier
163 if(javaIdentifier == Boolean.name) {
164 return LogicBool
165 } else if(javaIdentifier == Integer.name || javaIdentifier == Short.name) {
166 return LogicInt
167 } else if(javaIdentifier == Double.name || javaIdentifier == Float.name){
168 return LogicReal
169 } else if(javaIdentifier == String.name) {
170 return LogicString
171 } else {
172 throw new UnsupportedOperationException('''Unsupported eval type: "«javaIdentifier»"!''')
173 }
174 }
175 }
176
177 private def getTypeFromPassivePatternCallConstraintResult(
178 PVariable v,
179 Viatra2LogicTypeResult result,
180 TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace,
181 Viatra2LogicTrace viatra2LogicTrace,
182 Set<? extends PParameter> checkedInDecisionMaking
183 ) {
184 val referringConstraints = v.referringConstraints
185
186 val referringCountMatcherTargeting = referringConstraints
187 .filter(PatternMatchCounter)
188 .filter[it.resultVariable === v]
189 .map[builder.LogicInt]
190 val referringAggregatorConstraintsTargeting = referringConstraints
191 .filter(AggregatorConstraint)
192 .filter[it.resultVariable === v]
193 .map[ // get the type of the referred column
194 getOrMakeTypeDecision(
195 result,
196 it.referredQuery,
197 it.referredQuery.parameters.get(aggregatedColumn),
198 ecore2LogicTrace,
199 viatra2LogicTrace,
200 checkedInDecisionMaking)]
201
202 return referringCountMatcherTargeting + referringAggregatorConstraintsTargeting
203 }
204
205 private def getTypeFromPassivePatternCallConstraints(
206 PVariable v,
207 Viatra2LogicTypeResult result,
208 TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace,
209 Viatra2LogicTrace viatra2LogicTrace,
210 Set<? extends PParameter> checkedInDecisionMaking
211 ) {
212 val referringConstraints = v.referringConstraints
213 if(referringConstraints.size === 1) {
214 val onlyConstraint = referringConstraints.head
215
216 if(onlyConstraint instanceof PatternCallBasedDeferred) {
217 val indexOfVariable = v.lookup(onlyConstraint.actualParametersTuple.invertIndex)
218 val parameter = onlyConstraint.referredQuery.parameters.get(indexOfVariable)
219 val res = getOrMakeTypeDecision(result, onlyConstraint.referredQuery, parameter, ecore2LogicTrace,viatra2LogicTrace,checkedInDecisionMaking)
220 return #[res]
221 } else {
222 throw new IllegalArgumentException('''A non-PatternCallBasedDeferred type constraint is referring to the variable "«v.name»"!''')
223 }
224 } else {
225 throw new IllegalArgumentException('''Multiple («referringConstraints.size», «FOR c:referringConstraints SEPARATOR ", "»«c»«ENDFOR») constraints are referring to variable "«v.name»", but no type is inferred!''')
226 }
227 }
228
229 def TypeReference calculateCommonSubtype(Iterable<TypeReference> types) {
230 val primitiveTypeReferences = types.filter(PrimitiveTypeReference)
231 val complexTypeReferences = types.filter(ComplexTypeReference)
232 if(complexTypeReferences.isEmpty) {
233 // If there is an int type, ...
234 if(primitiveTypeReferences.exists[it instanceof IntTypeReference]) {
235 // ... and all types are either real or int, then return int!
236 if(primitiveTypeReferences.forall[it instanceof RealTypeReference || it instanceof IntTypeReference]) {
237 return primitiveTypeReferences.filter(IntTypeReference).head
238 }
239 // Otherwise, the types are inconsistent, because they mixing numeric and non-numeric types.
240 else throw new IllegalArgumentException('''Inconsistent types: «primitiveTypeReferences.map[eClass.name].toSet.toList»''')
241 }
242 // If there is no Real, then the types should be homogenious
243 val head = primitiveTypeReferences.head
244 if(primitiveTypeReferences.exists[it.eClass !== head.eClass]) {
245 throw new IllegalArgumentException('''Inconsistent types: «primitiveTypeReferences.map[eClass.name].toSet.toList»''')
246 }
247 return head
248 } else if(primitiveTypeReferences.isEmpty) {
249 val complexTypes = complexTypeReferences.map[it.referred].toSet
250 if(complexTypes.size === 1) {
251 return builder.toTypeReference(complexTypes.head)
252 }
253 // Collect possible subtypes
254 val subtypeSets = complexTypes.map[it.transitiveClosureStar[it.subtypes].toSet]
255 val commonTypeSet = new HashSet(subtypeSets.head)
256 val otherSets = subtypeSets.tail
257 for(otherSet : otherSets) {
258 commonTypeSet.retainAll(otherSet)
259 }
260 if(commonTypeSet.empty) {
261 throw new IllegalArgumentException('''Inconsistent types: «complexTypes.map[name].toList»''')
262 }
263
264
265 return calculateCommonComplexSupertype(commonTypeSet)
266
267 } else {
268 throw new IllegalArgumentException('''
269 Inconsistent types, mixing primitive and complex types:
270 «primitiveTypeReferences.map[eClass.name].toSet.toList»
271 and
272 «complexTypeReferences.map[it.referred].toSet.map[name].toList»''')
273
274 }
275 }
276
277
278 def TypeReference calculateCommonSupertype(Iterable<TypeReference> types) {
279 val primitiveTypeReferences = types.filter(PrimitiveTypeReference)
280 val complexTypeReferences = types.filter(ComplexTypeReference)
281 if(complexTypeReferences.isEmpty) {
282 // If there is a real type, ...
283 if(primitiveTypeReferences.exists[it instanceof RealTypeReference]) {
284 // ... and all types are either real or int, then return real!
285 if(primitiveTypeReferences.forall[it instanceof RealTypeReference || it instanceof IntTypeReference]) {
286 return primitiveTypeReferences.filter(RealTypeReference).head
287 }
288 // Otherwise, the types are inconsistent, because they mixing numeric and non-numeric types.
289 else throw new IllegalArgumentException('''Inconsistent types: «primitiveTypeReferences.map[eClass.name].toSet.toList»''')
290 }
291 // If there is no Real, then the types should be homogenious
292 val head = primitiveTypeReferences.head
293 if(primitiveTypeReferences.exists[it.eClass !== head.eClass]) {
294 throw new IllegalArgumentException('''Inconsistent types: «primitiveTypeReferences.map[eClass.name].toSet.toList»''')
295 }
296 return head
297 } else if(primitiveTypeReferences.isEmpty) {
298 val complexTypes = complexTypeReferences.map[it.referred].toSet
299 return calculateCommonComplexSupertype(complexTypes)
300
301 } else {
302 throw new IllegalArgumentException('''
303 Inconsistent types, mixing primitive and complex types:
304 «primitiveTypeReferences.map[eClass.name].toSet.toList»
305 and
306 «complexTypeReferences.map[it.referred].toSet.map[name].toList»''')
307
308 }
309 }
310 def TypeReference calculateCommonComplexSupertype(Set<Type> complexTypes) {
311 if(complexTypes.size === 1) {
312 return builder.toTypeReference(complexTypes.head)
313 }
314 // Collect possible supertypes
315 val supertypeSets = complexTypes.map[it.transitiveClosureStar[it.supertypes].toSet]
316 val commonTypeSet = new HashSet(supertypeSets.head)
317 val otherSets = supertypeSets.tail
318 for(otherSet : otherSets) {
319 commonTypeSet.retainAll(otherSet)
320 }
321 if(commonTypeSet.empty) {
322 throw new IllegalArgumentException('''Inconsistent types: «complexTypes.map[name].toList»''')
323 }
324 // Remove type that already have covered
325 val coveredTypes = commonTypeSet.map[it.supertypes].flatten
326 commonTypeSet.removeAll(coveredTypes)
327 return builder.toTypeReference(commonTypeSet.head)
328 }
329
330 /**
331 * Transforms a Viatra type reference to a logic type.
332 */
333 def dispatch TypeReference transformTypeReference(EDataTypeInSlotsKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) {
334 val w = k.wrappedKey
335 if(w == EcorePackage.Literals.EINT || w == EcorePackage.Literals.ESHORT || w == EcorePackage.Literals.ELONG) {
336 return builder.LogicInt
337 } else if(w == EcorePackage.Literals.EDOUBLE || w == EcorePackage.Literals.EFLOAT) {
338 return builder.LogicReal
339 } else if(w == EcorePackage.Literals.EBOOLEAN) {
340 return builder.LogicBool
341 } else if(w == EcorePackage.Literals.ESTRING) {
342 return builder.LogicString
343 } else if(w instanceof EEnum) {
344 val c = this.ecore2Logic.TypeofEEnum(ecore2LogicTrace.trace,w)
345 return builder.toTypeReference(c);
346 } else throw new UnsupportedOperationException('''Unknown reference type «w.class.name»''')
347 }
348 def dispatch TypeReference transformTypeReference(JavaTransitiveInstancesKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) {
349 val c = k.wrapperInstanceClass
350 if(c == Integer || c == Long || c == Short) {
351 return LogicInt
352 } else if(c == Float || c == Double) {
353 return LogicReal
354 } else if(c == Boolean) {
355 return LogicBool
356 } else if(c == String) {
357 return LogicString
358 } else if(c.superclass == Enum){
359 val enums = ecore2Logic.allEnumsInScope(ecore2LogicTrace.trace)
360 for(enum : enums) {
361 if(c == enum.instanceClass) {
362 return builder.toTypeReference(ecore2Logic.TypeofEEnum(ecore2LogicTrace.trace,enum))
363 }
364 }
365 throw new IllegalArgumentException('''Enum type «c.simpleName» is not mapped to logic!''')
366 } else {
367 return null
368 }
369 }
370 def dispatch TypeReference transformTypeReference(EClassTransitiveInstancesKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) {
371 val c = k.wrappedKey
372
373 if(this.ecore2Logic.allClassesInScope(ecore2LogicTrace.trace).toList.contains(c)) {
374 return builder.toTypeReference(this.ecore2Logic.TypeofEClass(ecore2LogicTrace.trace,k.wrappedKey))
375 } else {
376 return null
377 }
378 }
379 def dispatch TypeReference transformTypeReference(EClassUnscopedTransitiveInstancesKey k, TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) {
380 val c = k.wrappedKey
381
382 if(this.ecore2Logic.allClassesInScope(ecore2LogicTrace.trace).toList.contains(c)) {
383 return builder.toTypeReference(this.ecore2Logic.TypeofEClass(ecore2LogicTrace.trace,k.wrappedKey))
384 } else {
385 return null
386 }
387 }
388
389 def dispatch TypeReference transformTypeReference(IInputKey k,TracedOutput<LogicProblem, Ecore2Logic_Trace> ecore2LogicTrace) {
390 throw new IllegalArgumentException('''Unsupported type: «k.class.simpleName»''')
391 }
392} \ No newline at end of file
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeResult.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeResult.xtend
new file mode 100644
index 00000000..7ba90724
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2LogicTypeResult.xtend
@@ -0,0 +1,47 @@
1package hu.bme.mit.inf.dslreasoner.viatra2logic
2
3import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference
4import java.util.Map
5import org.eclipse.viatra.query.runtime.matchers.psystem.PBody
6import org.eclipse.viatra.query.runtime.matchers.psystem.PVariable
7import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter
8import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery
9import org.eclipse.xtend.lib.annotations.Data
10import org.eclipse.xtext.xbase.lib.Functions.Function0
11import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
12import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference
13import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory
14import org.eclipse.emf.ecore.util.EcoreUtil
15import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.PrimitiveTypeReference
16
17@Data class Viatra2LogicTypeResult{
18 Map<Pair<PQuery,PParameter>,Function0<TypeReference>> typesInParameters
19 Map<Pair<PBody,PVariable>,Function0<TypeReference>> typesInBodies;
20
21 def addType(PBody body, PVariable variable, TypeReference typeConstructor) {
22 typesInBodies.put(body->variable,typeConstructor.createTypeConstructor)
23 }
24 def addType(PQuery query, PParameter variable, TypeReference typeConstructor) {
25 typesInParameters.put(query->variable,typeConstructor.createTypeConstructor)
26 }
27 def getType(PBody body, PVariable variable) {
28 return (body->variable).lookup(typesInBodies).apply
29 }
30 def getType(PQuery query, PParameter variable) {
31 return (query->variable).lookup(typesInParameters).apply
32 }
33
34 def containsSolution(PBody body, PVariable variable) {
35 return typesInBodies.containsKey(body->variable)
36 }
37 def containsSolution(PParameter variable) {
38 return typesInParameters.containsKey(variable)
39 }
40
41 def dispatch Function0<TypeReference> createTypeConstructor(ComplexTypeReference ref) {
42 return [LogiclanguageFactory.eINSTANCE.createComplexTypeReference=>[it.referred = ref.referred]]
43 }
44 def dispatch Function0<TypeReference> createTypeConstructor(PrimitiveTypeReference ref) {
45 return [EcoreUtil.copy(ref)]
46 }
47} \ No newline at end of file
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/XExpressionExtractor.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/XExpressionExtractor.xtend
new file mode 100644
index 00000000..ea8d0b23
--- /dev/null
+++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/XExpressionExtractor.xtend
@@ -0,0 +1,24 @@
1package hu.bme.mit.inf.dslreasoner.viatra2logic
2
3import org.eclipse.viatra.query.patternlanguage.emf.specification.XBaseEvaluator
4import org.eclipse.viatra.query.runtime.matchers.psystem.IExpressionEvaluator
5import org.eclipse.xtext.xbase.XExpression
6
7class XExpressionExtractor {
8 def dispatch XExpression extractExpression(XBaseEvaluator evaluator) { evaluator.expression }
9 def dispatch XExpression extractExpression(IExpressionEvaluator evaluator) {
10 val clazz = evaluator.class
11 if(clazz.name == "org.eclipse.viatra.query.runtime.matchers.psystem.rewriters.VariableMappingExpressionEvaluatorWrapper") {
12 val field = clazz.declaredFields.filter[it.name == "wrapped"].head
13 if(field === null) {
14 throw new IllegalArgumentException('''Class «clazz.simpleName» has no field "wrapped"!''')
15 } else {
16 field.setAccessible(true);
17 val wrappedEvaluator = field.get(evaluator) as XBaseEvaluator
18 return wrappedEvaluator.extractExpression
19 }
20 } else {
21 throw new IllegalArgumentException('''Unsupported expression evaluation form: «clazz.simpleName»!''')
22 }
23 }
24} \ No newline at end of file
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-30 22:27:20 +0000