diff options
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.logic.model/patterns/hu/bme/mit')
-rw-r--r-- | Framework/hu.bme.mit.inf.dslreasoner.logic.model/patterns/hu/bme/mit/inf/dslreasoner/logic/model/patterns/typeUtil.vql | 167 |
1 files changed, 167 insertions, 0 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/patterns/hu/bme/mit/inf/dslreasoner/logic/model/patterns/typeUtil.vql b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/patterns/hu/bme/mit/inf/dslreasoner/logic/model/patterns/typeUtil.vql new file mode 100644 index 00000000..5b38189f --- /dev/null +++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/patterns/hu/bme/mit/inf/dslreasoner/logic/model/patterns/typeUtil.vql | |||
@@ -0,0 +1,167 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.logic.model.patterns | ||
2 | |||
3 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/problem" | ||
4 | import epackage "http://www.bme.hu/mit/inf/dslreasoner/logic/model/language" | ||
5 | |||
6 | /// Basic util patterns /// | ||
7 | |||
8 | /** | ||
9 | * Direct supertypes of a type. | ||
10 | */ | ||
11 | private pattern supertypeDirect(subtype : Type, supertype : Type) { | ||
12 | Type.supertypes(subtype, supertype); | ||
13 | } | ||
14 | |||
15 | /** | ||
16 | * All supertypes of a type. | ||
17 | */ | ||
18 | pattern supertypeStar(subtype: Type, supertype: Type) { | ||
19 | subtype == supertype; | ||
20 | } or { | ||
21 | find supertypeDirect+(subtype,supertype); | ||
22 | } | ||
23 | |||
24 | /** | ||
25 | * Direct element of a type | ||
26 | */ | ||
27 | pattern typeDirectElements(type: TypeDefinition, element: DefinedElement) { | ||
28 | TypeDefinition.elements(type,element); | ||
29 | } | ||
30 | |||
31 | /// Complex type reasoning patterns /// | ||
32 | // | ||
33 | // In a valid type system, for each element e there is exactly one type T where | ||
34 | // 1: T(e) - but we dont know this for type declaration | ||
35 | // 2: For the dynamic type D and another type T, where D(e) && D-->T, T(e) is true. | ||
36 | // 2e: A type hierarchy is invalid, if there is a supertype T for a dynamic type D which does no contains e: | ||
37 | // D(e) && D-->T && !T(e) | ||
38 | // 3: There is no T' that T'->T and T'(e) | ||
39 | // 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: | ||
40 | // D(e) && ![T--->D] && T(e) | ||
41 | // 4: T is not abstract | ||
42 | // Such type T is called Dynamic type of e, while other types are called static types. | ||
43 | // | ||
44 | // The following patterns checks the possible dynamic types for an element | ||
45 | |||
46 | pattern possibleDynamicType(problem: LogicProblem, dynamic:Type, element:DefinedElement) | ||
47 | // case 1: element is defined in at least once | ||
48 | { | ||
49 | LogicProblem.types(problem,dynamic); | ||
50 | // select a random definition | ||
51 | find typeDirectElements(definition,element); | ||
52 | // 2e is not true: D(e) && D-->T && !T(e) | ||
53 | find supertypeStar(dynamic,definition); | ||
54 | neg find dynamicTypeNotSubtypeOfADefinition(problem,element,dynamic); | ||
55 | // 3e is not true: D(e) && ![T--->D] && T(e) | ||
56 | neg find dynamicTypeIsSubtypeOfANonDefinition(problem,element,dynamic); | ||
57 | // 4: T is not abstract | ||
58 | Type.isAbstract(dynamic,false); | ||
59 | } or | ||
60 | // case 2: element is defined is not defined | ||
61 | { | ||
62 | LogicProblem.types(problem,dynamic); | ||
63 | // there is no definition | ||
64 | neg find typeDirectElements(_,element); | ||
65 | // 2e is not true: D(e) && D-->T && !T(e) | ||
66 | // because non of the definition contains element, the type cannot have defined supertype | ||
67 | neg find typesWithDefinedSupertype(problem,dynamic); | ||
68 | // 3e is not true: D(e) && ![T--->D] && T(e) | ||
69 | // because there is no definition, dynamic covers all definition | ||
70 | } | ||
71 | |||
72 | /** | ||
73 | * supertype -------> element <------- otherSupertype | ||
74 | * A A | ||
75 | * | | | ||
76 | * wrongDynamic -----------------------------X | ||
77 | */ | ||
78 | private pattern dynamicTypeNotSubtypeOfADefinition(problem:LogicProblem, element:DefinedElement, wrongDynamic : Type) { | ||
79 | LogicProblem.types(problem,wrongDynamic); | ||
80 | find typeDirectElements(supertype,element); | ||
81 | find supertypeStar(wrongDynamic,supertype); | ||
82 | find typeDirectElements(otherSupertype,element); | ||
83 | neg find supertypeStar(wrongDynamic,otherSupertype); | ||
84 | //otherSupertype != wrongDynamic; | ||
85 | } | ||
86 | |||
87 | |||
88 | /** | ||
89 | * supertype -------> element <---X--- otherSupertype | ||
90 | * A A | ||
91 | * | | | ||
92 | * wrongDynamic -----------------------------+ | ||
93 | */ | ||
94 | private pattern dynamicTypeIsSubtypeOfANonDefinition(problem: LogicProblem, element:DefinedElement, wrongDynamic:Type) { | ||
95 | LogicProblem.types(problem,wrongDynamic); | ||
96 | find typeDirectElements(supertype, element); | ||
97 | find supertypeStar(wrongDynamic, supertype); | ||
98 | find supertypeStar(wrongDynamic, otherSupertype); | ||
99 | TypeDefinition(otherSupertype); | ||
100 | neg find typeDirectElements(otherSupertype, element); | ||
101 | } | ||
102 | |||
103 | private pattern typesWithDefinedSupertype(problem: LogicProblem, type:TypeDeclaration) { | ||
104 | LogicProblem.types(problem,type); | ||
105 | find supertypeStar(type,definedSupertype); | ||
106 | TypeDefinition(definedSupertype); | ||
107 | } | ||
108 | |||
109 | /** | ||
110 | * Types that | ||
111 | */ | ||
112 | pattern mustTypeElement(problem: LogicProblem, type:Type, element:DefinedElement) { | ||
113 | LogicProblem.types(problem,type); | ||
114 | TypeDefinition.elements(type,element); | ||
115 | } or { | ||
116 | TypeDeclaration(type); | ||
117 | LogicProblem.types(problem,type); | ||
118 | LogicProblem.types(problem,subtype); | ||
119 | TypeDefinition.elements(subtype,element); | ||
120 | find supertypeStar(subtype,type); | ||
121 | } | ||
122 | |||
123 | |||
124 | /// Validation patterns /// | ||
125 | |||
126 | @Constraint(severity = "warning",key = {problem}, | ||
127 | message="Type system is inconsistent." | ||
128 | ) | ||
129 | pattern typeSystemIsInconsistent(problem:LogicProblem) { | ||
130 | find elementWithNoPossibleDynamicType(problem,_); | ||
131 | } or { | ||
132 | find elementNotDefinedInSupertype(problem,_,_,_); | ||
133 | } | ||
134 | |||
135 | /** | ||
136 | * An element is defined in a type, but not defined in a supertype | ||
137 | */ | ||
138 | @Constraint(severity = "warning",key = {element}, | ||
139 | message="An element is defined in a type, but not defined in a supertype." | ||
140 | ) | ||
141 | pattern elementNotDefinedInSupertype(problem: LogicProblem, | ||
142 | element: DefinedElement, | ||
143 | directType:TypeDefinition, | ||
144 | notDefinedIn: TypeDefinition) | ||
145 | { | ||
146 | LogicProblem.elements(problem,element); | ||
147 | find typeDirectElements(directType,element); | ||
148 | find supertypeStar(directType,notDefinedIn); | ||
149 | neg find typeDirectElements(notDefinedIn,element); | ||
150 | } | ||
151 | |||
152 | @Constraint(severity = "warning",key = {element}, | ||
153 | message="There is no possible dynamic type for an element." | ||
154 | ) | ||
155 | pattern elementWithNoPossibleDynamicType(problem:LogicProblem, element:DefinedElement) { | ||
156 | LogicProblem.elements(problem,element); | ||
157 | neg find possibleDynamicType(problem,_,element); | ||
158 | } | ||
159 | |||
160 | |||
161 | |||
162 | @Constraint(severity = "error",key = {t}, | ||
163 | message="Circle in the type hierarchy" | ||
164 | ) | ||
165 | pattern cyclicTypeHierarchy(t: Type) { | ||
166 | find supertypeDirect+(t,t); | ||
167 | } | ||