diff options
author | OszkarSemerath <oszka@152.66.252.189> | 2017-06-10 19:05:05 +0200 |
---|---|---|
committer | OszkarSemerath <oszka@152.66.252.189> | 2017-06-10 19:05:05 +0200 |
commit | 60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch) | |
tree | 5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend | |
parent | Initial commit, migrating from SVN (diff) | |
download | VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.gz VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.tar.zst VIATRA-Generator-60f01f46ba232ed6416054f0a6115cb2a9b70b4e.zip |
Migrating Additional projects
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend | 194 |
1 files changed, 194 insertions, 0 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend new file mode 100644 index 00000000..fbbd9fb5 --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/GenericTypeIndexer.xtend | |||
@@ -0,0 +1,194 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.patterns | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
5 | import org.eclipse.emf.ecore.EClass | ||
6 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.Modality | ||
7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
8 | import hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.TypeAnalysisResult | ||
9 | |||
10 | class GenericTypeIndexer implements TypeIndexer { | ||
11 | val PatternGenerator base; | ||
12 | |||
13 | new(PatternGenerator base) { | ||
14 | this.base = base | ||
15 | } | ||
16 | override requiresTypeAnalysis() { false } | ||
17 | |||
18 | public override getRequiredQueries() ''' | ||
19 | private pattern newELement(interpretation: PartialInterpretation, element: DefinedElement) { | ||
20 | PartialInterpretation.newElements(interpretation,element); | ||
21 | } | ||
22 | |||
23 | private pattern typeInterpretation(problem:LogicProblem, interpetation:PartialInterpretation, type:TypeDeclaration, typeInterpretation:PartialTypeInterpratation) { | ||
24 | find interpretation(problem,interpetation); | ||
25 | LogicProblem.types(problem,type); | ||
26 | PartialInterpretation.partialtypeinterpratation(interpetation,typeInterpretation); | ||
27 | PartialTypeInterpratation.interpretationOf(typeInterpretation,type); | ||
28 | } | ||
29 | |||
30 | private pattern directInstanceOf(problem:LogicProblem, interpetation:PartialInterpretation, element:DefinedElement, type:Type) { | ||
31 | find interpretation(problem,interpetation); | ||
32 | find mustExist(problem,interpetation,element); | ||
33 | LogicProblem.types(problem,type); | ||
34 | TypeDefinition.elements(type,element); | ||
35 | } or { | ||
36 | find mustExist(problem,interpetation,element); | ||
37 | find typeInterpretation(problem,interpetation,type,typeInterpretation); | ||
38 | PartialTypeInterpratation.elements(typeInterpretation,element); | ||
39 | } | ||
40 | |||
41 | /** | ||
42 | * Direct supertypes of a type. | ||
43 | */ | ||
44 | private pattern supertypeDirect(subtype : Type, supertype : Type) { | ||
45 | Type.supertypes(subtype, supertype); | ||
46 | } | ||
47 | |||
48 | /** | ||
49 | * All supertypes of a type. | ||
50 | */ | ||
51 | private pattern supertypeStar(subtype: Type, supertype: Type) { | ||
52 | subtype == supertype; | ||
53 | } or { | ||
54 | find supertypeDirect+(subtype,supertype); | ||
55 | } | ||
56 | |||
57 | /// Complex type reasoning patterns /// | ||
58 | // | ||
59 | // In a valid type system, for each element e there is exactly one type T where | ||
60 | // 1: T(e) - but we dont know this for type declaration | ||
61 | // 2: For the dynamic type D and another type T, where D(e) && D-->T, T(e) is true. | ||
62 | // 2e: A type hierarchy is invalid, if there is a supertype T for a dynamic type D which does no contains e: | ||
63 | // D(e) && D-->T && !T(e) | ||
64 | // 3: There is no T' that T'->T and T'(e) | ||
65 | // 3e: A type hierarcy is invalid, if there is a type T for a dynamic type D, which contains e, but not subtype of T: | ||
66 | // D(e) && ![T--->D] && T(e) | ||
67 | // 4: T is not abstract | ||
68 | // Such type T is called Dynamic type of e, while other types are called static types. | ||
69 | // | ||
70 | // The following patterns checks the possible dynamic types for an element | ||
71 | |||
72 | private pattern wellformedType(problem: LogicProblem, interpretation:PartialInterpretation, dynamic:Type, element:DefinedElement) { | ||
73 | // 1: T(e) | ||
74 | find directInstanceOf(problem,interpretation,element,dynamic); | ||
75 | // 2e is not true: D(e) && D-->T && !T(e) | ||
76 | neg find dynamicTypeNotSubtypeOfADefinition(problem,interpretation,element,dynamic); | ||
77 | // 3e is not true: D(e) && ![T--->D] && T(e) | ||
78 | neg find dynamicTypeIsSubtypeOfANonDefinition(problem,interpretation,element,dynamic); | ||
79 | // 4: T is not abstract | ||
80 | Type.isAbstract(dynamic,false); | ||
81 | } | ||
82 | |||
83 | private pattern possibleDynamicType(problem: LogicProblem, interpretation:PartialInterpretation, dynamic:Type, element:DefinedElement) | ||
84 | // case 1: element is defined at least once | ||
85 | { | ||
86 | LogicProblem.types(problem,dynamic); | ||
87 | // select a random definition 'randomType' | ||
88 | find directInstanceOf(problem,interpretation,element,randomType); | ||
89 | // dynamic is a subtype of 'randomType' | ||
90 | find supertypeStar(dynamic,randomType); | ||
91 | // 2e is not true: D(e) && D-->T && !T(e) | ||
92 | neg find dynamicTypeNotSubtypeOfADefinition(problem,interpretation,element,dynamic); | ||
93 | // 3e is not true: D(e) && ![T--->D] && T(e) | ||
94 | neg find dynamicTypeIsSubtypeOfANonDefinition(problem,interpretation,element,dynamic); | ||
95 | // 4: T is not abstract | ||
96 | Type.isAbstract(dynamic,false); | ||
97 | } or | ||
98 | // case 2: element is not defined anywhere | ||
99 | { | ||
100 | find mayExist(problem,interpretation,element); | ||
101 | // there is no definition | ||
102 | neg find directInstanceOf(problem,interpretation,element,_); | ||
103 | // 2e is not true: D(e) && D-->T && !T(e) | ||
104 | // because non of the definition contains element, the type cannot have defined supertype | ||
105 | LogicProblem.types(problem,dynamic); | ||
106 | PartialInterpretation.problem(interpretation,problem); | ||
107 | neg find typeWithDefinedSupertype(dynamic); | ||
108 | // 3e is not true: D(e) && ![T--->D] && T(e) | ||
109 | // because there is no definition, dynamic covers all definition | ||
110 | // 4: T is not abstract | ||
111 | Type.isAbstract(dynamic,false); | ||
112 | } | ||
113 | |||
114 | /** | ||
115 | * supertype -------> element <------- otherSupertype | ||
116 | * A A | ||
117 | * | | | ||
118 | * wrongDynamic -----------------------------X | ||
119 | */ | ||
120 | private pattern dynamicTypeNotSubtypeOfADefinition(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, wrongDynamic : Type) { | ||
121 | find directInstanceOf(problem,interpretation,element,supertype); | ||
122 | find directInstanceOf(problem,interpretation,element,otherSupertype); | ||
123 | find supertypeStar(wrongDynamic,supertype); | ||
124 | neg find supertypeStar(wrongDynamic,otherSupertype); | ||
125 | } | ||
126 | |||
127 | /** | ||
128 | * supertype -------> element <---X--- otherSupertype | ||
129 | * A A | ||
130 | * | | | ||
131 | * wrongDynamic -----------------------------+ | ||
132 | */ | ||
133 | private pattern dynamicTypeIsSubtypeOfANonDefinition(problem: LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, wrongDynamic:Type) { | ||
134 | find directInstanceOf(problem,interpretation,element,supertype); | ||
135 | neg find elementInTypeDefinition(element,otherSupertype); | ||
136 | TypeDefinition(otherSupertype); | ||
137 | find supertypeStar(wrongDynamic, supertype); | ||
138 | find supertypeStar(wrongDynamic, otherSupertype); | ||
139 | } | ||
140 | |||
141 | private pattern elementInTypeDefinition(element:DefinedElement, definition:TypeDefinition) { | ||
142 | TypeDefinition.elements(definition,element); | ||
143 | } | ||
144 | |||
145 | private pattern typeWithDefinedSupertype(type:Type) { | ||
146 | find supertypeStar(type,definedSupertype); | ||
147 | TypeDefinition(definedSupertype); | ||
148 | } | ||
149 | ''' | ||
150 | |||
151 | public override generateInstanceOfQueries(LogicProblem problem, PartialInterpretation emptySolution,TypeAnalysisResult typeAnalysisResult) { | ||
152 | ''' | ||
153 | «FOR type:problem.types» | ||
154 | «problem.generateMustInstenceOf(type)» | ||
155 | «problem.generateMayInstanceOf(type)» | ||
156 | «ENDFOR» | ||
157 | ''' | ||
158 | } | ||
159 | |||
160 | private def patternName(Type type, Modality modality) | ||
161 | '''«modality.toString.toLowerCase»InstanceOf«base.canonizeName(type.name)»''' | ||
162 | |||
163 | private def generateMustInstenceOf(LogicProblem problem, Type type) { | ||
164 | ''' | ||
165 | /** | ||
166 | * An element must be an instance of type "«type.name»". | ||
167 | */ | ||
168 | private pattern «patternName(type,Modality.MUST)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { | ||
169 | Type.name(type,"«type.name»"); | ||
170 | find directInstanceOf(problem,interpretation,element,type); | ||
171 | } | ||
172 | ''' | ||
173 | } | ||
174 | |||
175 | private def generateMayInstanceOf(LogicProblem problem, Type type) { | ||
176 | ''' | ||
177 | /** | ||
178 | * An element may be an instance of type "«type.name»". | ||
179 | */ | ||
180 | private pattern «patternName(type,Modality.MAY)»(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement) { | ||
181 | Type.name(type,"«type.name»"); | ||
182 | find possibleDynamicType(problem,interpretation,dynamic,element); | ||
183 | find supertypeStar(dynamic,type); | ||
184 | } | ||
185 | ''' | ||
186 | } | ||
187 | |||
188 | public override referInstanceOf(Type type, Modality modality, String variableName) { | ||
189 | '''find «patternName(type,modality)»(problem,interpretation,«variableName»);''' | ||
190 | } | ||
191 | public override referInstanceOf(EClass type, Modality modality, String variableName) { | ||
192 | '''find «modality.toString.toLowerCase»InstanceOf«base.canonizeName('''class «type.name»''')»(problem,interpretation,«variableName»);''' | ||
193 | } | ||
194 | } \ No newline at end of file | ||