diff options
author | 2017-06-10 19:05:05 +0200 | |
---|---|---|
committer | 2017-06-10 19:05:05 +0200 | |
commit | 60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch) | |
tree | 5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/patterns/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/queries | |
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/patterns/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/queries')
-rw-r--r-- | Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/patterns/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/queries/TypeAnalysis.vql | 223 |
1 files changed, 223 insertions, 0 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/patterns/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/queries/TypeAnalysis.vql b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/patterns/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/queries/TypeAnalysis.vql new file mode 100644 index 00000000..ebab542c --- /dev/null +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/patterns/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/queries/TypeAnalysis.vql | |||
@@ -0,0 +1,223 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries | ||
2 | |||
3 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language" | ||
4 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" | ||
5 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage" | ||
6 | |||
7 | /** | ||
8 | * Direct supertypes of a type. | ||
9 | */ | ||
10 | private pattern supertypeDirect(subtype : Type, supertype : Type) { | ||
11 | Type.supertypes(subtype, supertype); | ||
12 | } | ||
13 | |||
14 | /** | ||
15 | * All supertypes of a type. | ||
16 | */ | ||
17 | |||
18 | private pattern supertypePlus(subtype: Type, supertype: Type) { | ||
19 | find supertypeDirect+(subtype,supertype); | ||
20 | } | ||
21 | |||
22 | private pattern supertypeStar(subtype: Type, supertype: Type) { | ||
23 | subtype == supertype; | ||
24 | } or { | ||
25 | find supertypePlus(subtype,supertype); | ||
26 | } | ||
27 | |||
28 | pattern hasDefinedSupertype(type:Type) { | ||
29 | find supertypeStar(type,superType); | ||
30 | TypeDefinition(superType); | ||
31 | } | ||
32 | |||
33 | pattern dontHaveDefinedSupertype(type:TypeDeclaration) { | ||
34 | neg find hasDefinedSupertype(type); | ||
35 | } | ||
36 | |||
37 | /////////////////////// | ||
38 | // New element types | ||
39 | /////////////////////// | ||
40 | |||
41 | /** | ||
42 | * A new element can has 'type' as a dynamic type iff | ||
43 | * (1) 'type' is concrete and | ||
44 | * (2) 'type' does not have defined supertype | ||
45 | * (including the case when 'type' itself is defined). | ||
46 | */ | ||
47 | private pattern possibleNewElementDynamicType(type:TypeDeclaration) { | ||
48 | Type.isAbstract(type,false); | ||
49 | find dontHaveDefinedSupertype(type); | ||
50 | } | ||
51 | ///** | ||
52 | // * The type of a new element can be refined from 'previous' to 'refined'. | ||
53 | // */ | ||
54 | //private pattern newElementTypeRefinementPath(previous:TypeDeclaration, refined:TypeDeclaration) { | ||
55 | // find possibleNewElementDynamicType(previous); | ||
56 | // find possibleNewElementDynamicType(refined); | ||
57 | // find supertypePlus(refined,previous); | ||
58 | //} | ||
59 | |||
60 | /** | ||
61 | * New element can be created with type 'type' iff it can has 'type' as a dynamic type. | ||
62 | */ | ||
63 | pattern newElementTypeConstructor(type:TypeDeclaration) { | ||
64 | find possibleNewElementDynamicType(type); | ||
65 | } | ||
66 | |||
67 | /** | ||
68 | * New element can be refined to type 'refined' iff | ||
69 | * (1) type is concrete | ||
70 | * (2) the new type cover each existing type of the previous state, i.e. | ||
71 | * (2') it does not have type that: | ||
72 | */ | ||
73 | |||
74 | pattern newElementTypeRefinementTarget(refined: TypeDeclaration) { | ||
75 | find possibleNewElementDynamicType(refined); | ||
76 | } | ||
77 | |||
78 | private pattern incompatibleType(type:TypeDeclaration, incompatible:TypeDeclaration) { | ||
79 | LogicProblem.types(problem,type); | ||
80 | LogicProblem.types(problem,incompatible); | ||
81 | neg find supertypeStar(type, incompatible); | ||
82 | } | ||
83 | |||
84 | pattern incompatibleSuperType(type:TypeDeclaration, incompatibleType1:TypeDeclaration, incompatibleType2:TypeDeclaration) { | ||
85 | find incompatibleType(type, incompatibleType1); | ||
86 | find incompatibleType(type, incompatibleType2); | ||
87 | find supertypePlus(incompatibleType1, incompatibleType2); | ||
88 | } | ||
89 | |||
90 | pattern incompatibleTopType(type:TypeDeclaration, incompatible:TypeDeclaration) { | ||
91 | find incompatibleType(type, incompatible); | ||
92 | neg find incompatibleSuperType(type, incompatible, _); | ||
93 | } | ||
94 | |||
95 | pattern newElementTypeRefinementNegativeConstraint(refined:TypeDeclaration, inhibitor:TypeDeclaration) { | ||
96 | find incompatibleTopType(refined, inhibitor); | ||
97 | } or { | ||
98 | find possibleNewElementDynamicType(refined); | ||
99 | refined == inhibitor; | ||
100 | } | ||
101 | |||
102 | pattern newElementMayTypeNegativeConstraint(mayType: TypeDeclaration, inhibitor: TypeDeclaration) { | ||
103 | find incompatibleTopType(mayType, inhibitor); | ||
104 | } | ||
105 | |||
106 | /////////////////////// | ||
107 | // Old element types | ||
108 | /////////////////////// | ||
109 | |||
110 | //TODO old element types | ||
111 | |||
112 | //private pattern typeInterpretation(problem:LogicProblem, interpetation:PartialInterpretation, type:TypeDeclaration, typeInterpretation:PartialTypeInterpratation) { | ||
113 | // find interpretation(problem,interpetation); | ||
114 | // LogicProblem.types(problem,type); | ||
115 | // PartialInterpretation.partialtypeinterpratation(interpetation,typeInterpretation); | ||
116 | // PartialTypeInterpratation.interpretationOf(typeInterpretation,type); | ||
117 | //} | ||
118 | // | ||
119 | //pattern directInstanceOf(problem:LogicProblem, interpetation:PartialInterpretation, element:DefinedElement, type:Type) { | ||
120 | // find interpretation(problem,interpetation); | ||
121 | // find mustExist(problem,interpetation,element); | ||
122 | // LogicProblem.types(problem,type); | ||
123 | // TypeDefinition.elements(type,element); | ||
124 | //} or { | ||
125 | // find mustExist(problem,interpetation,element); | ||
126 | // find typeInterpretation(problem,interpetation,type,typeInterpretation); | ||
127 | // PartialTypeInterpratation.elements(typeInterpretation,element); | ||
128 | //} | ||
129 | // | ||
130 | // | ||
131 | // | ||
132 | ///// Complex type reasoning patterns /// | ||
133 | //// | ||
134 | //// In a valid type system, for each element e there is exactly one type T where | ||
135 | //// 1: T(e) - but we dont know this for type declaration | ||
136 | //// 2: For the dynamic type D and another type T, where D(e) && D-->T, T(e) is true. | ||
137 | //// 2e: A type hierarchy is invalid, if there is a supertype T for a dynamic type D which does no contains e: | ||
138 | //// D(e) && D-->T && !T(e) | ||
139 | //// 3: There is no T' that T'->T and T'(e) | ||
140 | //// 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: | ||
141 | //// D(e) && ![T--->D] && T(e) | ||
142 | //// 4: T is not abstract | ||
143 | //// Such type T is called Dynamic type of e, while other types are called static types. | ||
144 | //// | ||
145 | //// The following patterns checks the possible dynamic types for an element | ||
146 | // | ||
147 | //pattern wellformedType(problem: LogicProblem, interpretation:PartialInterpretation, dynamic:Type, element:DefinedElement) { | ||
148 | // // 1: T(e) | ||
149 | // find directInstanceOf(problem,interpretation,element,dynamic); | ||
150 | // // 2e is not true: D(e) && D-->T && !T(e) | ||
151 | // neg find dynamicTypeNotSubtypeOfADefinition(problem,interpretation,element,dynamic); | ||
152 | // // 3e is not true: D(e) && ![T--->D] && T(e) | ||
153 | // neg find dynamicTypeIsSubtypeOfANonDefinition(problem,interpretation,element,dynamic); | ||
154 | // // 4: T is not abstract | ||
155 | // Type.isAbstract(dynamic,false); | ||
156 | //} | ||
157 | // | ||
158 | //pattern possibleDynamicType(problem: LogicProblem, interpretation:PartialInterpretation, dynamic:Type, element:DefinedElement) | ||
159 | //// case 1: element is defined at least once | ||
160 | //{ | ||
161 | // LogicProblem.types(problem,dynamic); | ||
162 | // // select a random definition 'randomType' | ||
163 | // find directInstanceOf(problem,interpretation,element,randomType); | ||
164 | // // dynamic is a subtype of 'randomType' | ||
165 | // find supertypeStar(dynamic,randomType); | ||
166 | // // 2e is not true: D(e) && D-->T && !T(e) | ||
167 | // neg find dynamicTypeNotSubtypeOfADefinition(problem,interpretation,element,dynamic); | ||
168 | // // 3e is not true: D(e) && ![T--->D] && T(e) | ||
169 | // neg find dynamicTypeIsSubtypeOfANonDefinition(problem,interpretation,element,dynamic); | ||
170 | // // 4: T is not abstract | ||
171 | // Type.isAbstract(dynamic,false); | ||
172 | //} or | ||
173 | //// case 2: element is not defined anywhere | ||
174 | //{ | ||
175 | // find mayExist(problem,interpretation,element); | ||
176 | // // there is no definition | ||
177 | // neg find directInstanceOf(problem,interpretation,element,_); | ||
178 | // // 2e is not true: D(e) && D-->T && !T(e) | ||
179 | // // because non of the definition contains element, the type cannot have defined supertype | ||
180 | // LogicProblem.types(problem,dynamic); | ||
181 | // PartialInterpretation.problem(interpretation,problem); | ||
182 | // neg find typeWithDefinedSupertype(dynamic); | ||
183 | // // 3e is not true: D(e) && ![T--->D] && T(e) | ||
184 | // // because there is no definition, dynamic covers all definition | ||
185 | // // 4: T is not abstract | ||
186 | // Type.isAbstract(dynamic,false); | ||
187 | //} | ||
188 | // | ||
189 | ///** | ||
190 | // * supertype -------> element <------- otherSupertype | ||
191 | // * A A | ||
192 | // * | | | ||
193 | // * wrongDynamic -----------------------------X | ||
194 | // */ | ||
195 | //private pattern dynamicTypeNotSubtypeOfADefinition(problem:LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, wrongDynamic : Type) { | ||
196 | // find directInstanceOf(problem,interpretation,element,supertype); | ||
197 | // find directInstanceOf(problem,interpretation,element,otherSupertype); | ||
198 | // find supertypeStar(wrongDynamic,supertype); | ||
199 | // neg find supertypeStar(wrongDynamic,otherSupertype); | ||
200 | //} | ||
201 | // | ||
202 | // | ||
203 | ///** | ||
204 | // * supertype -------> element <---X--- otherSupertype | ||
205 | // * A A | ||
206 | // * | | | ||
207 | // * wrongDynamic -----------------------------+ | ||
208 | // */ | ||
209 | //private pattern dynamicTypeIsSubtypeOfANonDefinition(problem: LogicProblem, interpretation:PartialInterpretation, element:DefinedElement, wrongDynamic:Type) { | ||
210 | // find directInstanceOf(problem,interpretation,element,supertype); | ||
211 | // neg find elementInTypeDefinition(element,otherSupertype); | ||
212 | // find supertypeStar(wrongDynamic, supertype); | ||
213 | // find supertypeStar(wrongDynamic, otherSupertype); | ||
214 | //} | ||
215 | // | ||
216 | //private pattern elementInTypeDefinition(element:DefinedElement, definition:TypeDefinition) { | ||
217 | // TypeDefinition.elements(definition,element); | ||
218 | //} | ||
219 | // | ||
220 | //private pattern typeWithDefinedSupertype(type:TypeDeclaration) { | ||
221 | // find supertypeStar(type,definedSupertype); | ||
222 | // TypeDefinition(definedSupertype); | ||
223 | //} | ||