aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/patterns/hu/bme/mit/inf/dslreasoner/viatrasolver
diff options
context:
space:
mode:
authorLibravatar OszkarSemerath <oszka@152.66.252.189>2017-06-10 19:05:05 +0200
committerLibravatar OszkarSemerath <oszka@152.66.252.189>2017-06-10 19:05:05 +0200
commit60f01f46ba232ed6416054f0a6115cb2a9b70b4e (patch)
tree5edf8aeb07abc51f3fec63bbd15c926e1de09552 /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/patterns/hu/bme/mit/inf/dslreasoner/viatrasolver
parentInitial commit, migrating from SVN (diff)
downloadVIATRA-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')
-rw-r--r--Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/patterns/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/queries/TypeAnalysis.vql223
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 @@
1package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.queries
2
3import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language"
4import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem"
5import epackage "http://www.bme.hu/mit/inf/dslreasoner/viatrasolver/partialinterpretationlanguage"
6
7/**
8 * Direct supertypes of a type.
9 */
10private pattern supertypeDirect(subtype : Type, supertype : Type) {
11 Type.supertypes(subtype, supertype);
12}
13
14/**
15 * All supertypes of a type.
16 */
17
18private pattern supertypePlus(subtype: Type, supertype: Type) {
19 find supertypeDirect+(subtype,supertype);
20}
21
22private pattern supertypeStar(subtype: Type, supertype: Type) {
23 subtype == supertype;
24} or {
25 find supertypePlus(subtype,supertype);
26}
27
28pattern hasDefinedSupertype(type:Type) {
29 find supertypeStar(type,superType);
30 TypeDefinition(superType);
31}
32
33pattern 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 */
47private 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 */
63pattern 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
74pattern newElementTypeRefinementTarget(refined: TypeDeclaration) {
75 find possibleNewElementDynamicType(refined);
76}
77
78private pattern incompatibleType(type:TypeDeclaration, incompatible:TypeDeclaration) {
79 LogicProblem.types(problem,type);
80 LogicProblem.types(problem,incompatible);
81 neg find supertypeStar(type, incompatible);
82}
83
84pattern incompatibleSuperType(type:TypeDeclaration, incompatibleType1:TypeDeclaration, incompatibleType2:TypeDeclaration) {
85 find incompatibleType(type, incompatibleType1);
86 find incompatibleType(type, incompatibleType2);
87 find supertypePlus(incompatibleType1, incompatibleType2);
88}
89
90pattern incompatibleTopType(type:TypeDeclaration, incompatible:TypeDeclaration) {
91 find incompatibleType(type, incompatible);
92 neg find incompatibleSuperType(type, incompatible, _);
93}
94
95pattern newElementTypeRefinementNegativeConstraint(refined:TypeDeclaration, inhibitor:TypeDeclaration) {
96 find incompatibleTopType(refined, inhibitor);
97} or {
98 find possibleNewElementDynamicType(refined);
99 refined == inhibitor;
100}
101
102pattern 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//}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-06-29 08:39:12 +0000