1 | | % (c) 2009-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, |
2 | | % Heinrich Heine Universitaet Duesseldorf |
3 | | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) |
4 | | |
5 | | :- module(kernel_freetypes, |
6 | | [registered_freetype/2 |
7 | | ,freetype_case_db/3 |
8 | | ,reset_freetypes/0 |
9 | | ,create_freetype_typeid/3 |
10 | | ,add_freetype/2 |
11 | | ,freetype_with_single_case/2 |
12 | | ,enumerate_freetype_wf/4 |
13 | | ,max_freetype_enum_depth/1 |
14 | | ,max_cardinality_freetype/2 |
15 | | ,set_freetype_depth/1 |
16 | | ,is_a_freetype_wf/3 |
17 | | ,freetype_cardinality/2 |
18 | | ,is_recursive_freetype/1 |
19 | | ,is_infinite_freetype/1 |
20 | | ,get_freetype_type_parameters/3 |
21 | | ,is_maximal_freetype/1 |
22 | | ,is_empty_freetype/1 |
23 | | ,is_non_empty_freetype/1 |
24 | | ,test_empty_freetype/2 |
25 | | ,get_freeval_type/3 |
26 | | ,registered_freetype_case_value/3 |
27 | | ,get_freetype_id/2]). |
28 | | |
29 | | /* This module contains predicates for the support for free types as they are used in Z specifications */ |
30 | | |
31 | | :- use_module(module_information,[module_info/2]). |
32 | | :- module_info(group,proz). |
33 | | :- module_info(description,'This module contains predicates that cope with the internal freetype. This is currently only used by the Z extension.'). |
34 | | |
35 | | :- use_module(library(lists)). |
36 | | |
37 | | :- use_module(error_manager,[add_internal_error/2]). |
38 | | :- use_module(debug,[debug_format/3]). |
39 | | :- use_module(self_check). |
40 | | :- use_module(preferences,[get_preference/2]). |
41 | | :- use_module(kernel_objects,[basic_type/2, |
42 | | enumerate_type_wf/4, |
43 | | max_cardinality/2,safe_add/3]). |
44 | | :- use_module(typing_tools,[is_infinite_type/1]). |
45 | | |
46 | | |
47 | | :- dynamic freetype_register_db/2, freetype_with_single_case/2, freetype_case_db/3, |
48 | | max_iteration_depth/1, marked_cases/3, max_cardinality_db/3. |
49 | | |
50 | | /* freetype_register queries the database of registered free types for the list of cases */ |
51 | ? | registered_freetype(Id, Cases) :- freetype_register_db(Id,Cases). |
52 | | |
53 | | /* the extended register contains for each case a mark if it is recursive or not, |
54 | | for internal use only (regarding the module) */ |
55 | | extended_register(Id, ECases, ERec) :- |
56 | ? | marked_cases(Id,Cs,Rec),!,ECases = Cs, ERec=Rec. |
57 | | extended_register(Id, ECases, Rec) :- |
58 | | registered_freetype(Id,Cases), |
59 | | mark_recursive_cases(Cases,Id,ECases), |
60 | | (memberchk( case(_,_,recursive), ECases ) -> Rec=recursive ; Rec=non_recursive), |
61 | | assertz(marked_cases(Id,ECases,Rec)). |
62 | | |
63 | | /* reset_freetypes clears the database of registered free types */ |
64 | | reset_freetypes :- |
65 | | retractall(freetype_register_db(_,_)), |
66 | | retractall(freetype_case_db(_,_,_)), |
67 | | retractall(freetype_with_single_case(_,_)), |
68 | | retractall(marked_cases(_,_,_)), |
69 | | retractall(max_iteration_depth(_)), |
70 | | retractall(max_cardinality_db(_,_,_)). |
71 | | |
72 | | portray_freetypes :- freetype_register_db(Id,Cases), format('Freetype ~w~n cases:~w~n',[Id,Cases]),fail. |
73 | | portray_freetypes. |
74 | | |
75 | | % can be used to deconstruct or construct a freetype(.) argument term |
76 | | % the freetype does not yet need to be registered |
77 | | get_freetype_type_parameters(Id,Functor,TypeParas) :- var(Id),!, |
78 | | Id =.. [Functor|TypeParas]. |
79 | | %(freetype_register_db(Id,_) -> true ; add_internal_error('Illegal freetype: ',get_freetype_type_parameters(Id,Functor,TypeParas))). |
80 | | get_freetype_type_parameters(Id,Functor,TypeParas) :- |
81 | | %freetype_register_db(Id,_), |
82 | | (atom(Id) -> TypeParas=[], Functor=Id |
83 | | ; Id =.. [Functor|TypeParas]). |
84 | | |
85 | | /* with set_freetype_depth it is possible to set the maximum recursion depth of |
86 | | free types when enumerating them. If the depth is not set manually the |
87 | | depth is taken from the preference globalsets_fdrange. Mainly for testing */ |
88 | | set_freetype_depth(Depth) :- |
89 | | retractall(max_iteration_depth(_)),assertz(max_iteration_depth(Depth)). |
90 | | |
91 | | |
92 | | % encode type parameters into freetype id: |
93 | | % Type parameters are Prolog variables, or for B types (e.g., integer) for freetype uses |
94 | | create_freetype_typeid(Id,TypeParameters,FreetypeId) :- |
95 | | FreetypeId =.. [Id|TypeParameters]. |
96 | | |
97 | | |
98 | | /* add_freetypes appends a new free type to the database of free types */ |
99 | | % example (test 1304): |
100 | | % add_freetype('List'(T),[case(nil,constant([nil])),case(cons,couple(T,freetype(List(T))))]). |
101 | | add_freetype(Id, Cases) :- |
102 | | debug_format(19,'Add freetype ~w with cases ~w~n',[Id,Cases]), |
103 | | ( is_caselist(Cases,Id) -> |
104 | | ( registered_freetype(Id,OldCases) -> |
105 | | add_internal_error('freetype already registered: ', add_freetype(Id, Cases)), |
106 | | OldCases=Cases |
107 | ? | ; member(case(C,_),Cases),freetype_case_db(C,OId,_) -> |
108 | | add_internal_error('freetype case registered twice: ', (C,OId,Id)),fail |
109 | | ; |
110 | | assertz(freetype_register_db(Id,Cases)), |
111 | | (Cases = [case(Name,_)] -> assertz(freetype_with_single_case(Id,Name)) ; true), |
112 | | maplist(register_case(Id),Cases) |
113 | | ) |
114 | | ; |
115 | | add_internal_error('list of cases invalid', add_freetype(Id, Cases)),fail). |
116 | | |
117 | | register_case(FreetypeId,case(CaseId,CaseType)) :- |
118 | | assertz(freetype_case_db(CaseId,FreetypeId,CaseType)). |
119 | | |
120 | | % compute a value representing a freetype case identifier; for use in REPL, VisB, JSON trace replay, ... |
121 | | % it requires the type of the ID in context to instantiate polymorphic Freetype IDs |
122 | | registered_freetype_case_value(ID,Type,Value) :- |
123 | | freetype_case_db(ID,FreeTypeId,ArgType), |
124 | | get_freetype_id(Type,FreeTypeId), |
125 | | convert_case_type(ArgType,FreeTypeId,ID,Value). |
126 | | |
127 | | get_freetype_id(freetype(FID),FID). % a constructor without args |
128 | | get_freetype_id(set(couple(_,freetype(FID))),FID). % a constructor with args |
129 | | |
130 | | convert_case_type(Var,FreeTypeId,ConstId,Val) :- var(Var), |
131 | | add_internal_error('Variable freetype case: ',convert_case_type(Var,FreeTypeId,ConstId,Val)), |
132 | | fail. |
133 | | convert_case_type(constant(_),FreeTypeId,ConstId,Val) :- !, |
134 | | Val=freeval(FreeTypeId,ConstId,term(ConstId)). |
135 | | convert_case_type(Type,FreeTypeId,CaseId, |
136 | | closure(['_zzzz_unary','_zzzz_binary'],[Type,freetype(FreeTypeId)],EQ)) :- % could be pre-compiled |
137 | | % {x,y| y = CaseId(x)} -> a lambda function constructing free values |
138 | | ARG = b(identifier('_zzzz_unary'),Type,[]), |
139 | | LHS = b(identifier('_zzzz_binary'),freetype(FreeTypeId),[]), |
140 | | RHS = b(freetype_constructor(FreeTypeId,CaseId,ARG),freetype(FreeTypeId),[]), |
141 | | EQ = b(equal(LHS,RHS),pred,[prob_annotation('SYMBOLIC')]). |
142 | | |
143 | | |
144 | | /* enumerates a free type with regard to the maximum recursive iteration of free types. |
145 | | The first argument is "basic" or "tight", depending on wich enumeration method |
146 | | should be used for the value of the included types. */ |
147 | | enumerate_freetype_wf(EType,freeval(Id,C,Value),freetype(Id),WF) :- |
148 | | max_freetype_enum_depth(MaxDepth), |
149 | ? | enumerate_freetype_wf(EType,freeval(Id,C,Value),freetype_lim_depth(Id,MaxDepth),WF). |
150 | | enumerate_freetype_wf(EType,freeval(Id,C,Value),freetype_lim_depth(Id,Depth),WF) :- |
151 | | Depth > 0, |
152 | | extended_register(Id,Cases,_), |
153 | ? | member(case(C,CT,Mark),Cases), |
154 | | /* If the case is recursive we have to append information about the |
155 | | maximum recursion depth to limit the size of the data structure. |
156 | | In the non-recursive case we leave the type untouched */ |
157 | | (Mark = recursive -> |
158 | | NewDepth is Depth - 1, insert_recursion_depth(CT,NewDepth,NewCT) |
159 | | ; NewCT = CT), |
160 | ? | enumerate_type_wf(Value, NewCT, EType,WF). |
161 | | |
162 | | |
163 | | /* gives the maximumm cardinality of the free type with regard to the maximum |
164 | | recursive iteration of free types */ |
165 | | max_cardinality_freetype(freetype(Id),Card) :- |
166 | | max_freetype_enum_depth(MaxDepth), |
167 | | max_cardinality_freetype(freetype_lim_depth(Id,MaxDepth),Card). |
168 | | max_cardinality_freetype(freetype_lim_depth(Id,Depth),Card) :- |
169 | | (Depth > 0 -> |
170 | | /* we save the computed cardinality for a certain maximum depth to |
171 | | prevent exponential computation steps */ |
172 | | (max_cardinality_db(Id,Depth,Card) -> true; |
173 | | (NewDepth is Depth - 1, |
174 | | extended_register(Id,Cases,_), |
175 | | sum_cases_cardinalities(Cases,NewDepth,Card), |
176 | | assertz(max_cardinality_db(Id,Depth,Card)))); |
177 | | Card = 0). |
178 | | |
179 | | sum_cases_cardinalities([],_,0). |
180 | | sum_cases_cardinalities([case(_,Type,Mark)|Rest],Depth,Card) :- |
181 | | sum_cases_cardinalities(Rest,Depth,CRest), |
182 | | /* like in enumerate_freetype we distinguish between recursive and |
183 | | non-recursive cases and add information about the maximum recursion |
184 | | depth in the former case. */ |
185 | | (Mark = recursive -> |
186 | | insert_recursion_depth(Type,Depth,NewType); |
187 | | NewType = Type), |
188 | | max_cardinality(NewType,C), |
189 | | add_with_inf(CRest,C,Card). |
190 | | |
191 | | add_with_inf(inf,_,R) :- !,R=inf. |
192 | | add_with_inf(_,inf,R) :- !,R=inf. |
193 | | add_with_inf(A,B,R) :- R is A+B. |
194 | | |
195 | | max_freetype_enum_depth(Depth) :- |
196 | | max_iteration_depth(Depth) -> true; get_preference(globalsets_fdrange,Depth). |
197 | | |
198 | | :- use_module(typing_tools,[valid_ground_type/1]). |
199 | | /* Is the list a valid list of cases? */ |
200 | | is_caselist([],_). |
201 | | is_caselist([case(Case,CaseType)|Rest],Id) :- |
202 | | atom(Case), |
203 | | (ground(Id) -> valid_ground_type(CaseType) |
204 | | ; true % TODO: we could check if variables are subset of variables of Id |
205 | | ), |
206 | | is_caselist(Rest,Id). |
207 | | |
208 | | |
209 | | /* Appends to all freetype references a maximum depth */ |
210 | | insert_recursion_depth(freetype(Id),Depth,freetype_lim_depth(Id,Depth)) :- !. |
211 | | insert_recursion_depth(set(A),Depth,set(B)) :- !,insert_recursion_depth(A,Depth,B). |
212 | | insert_recursion_depth(seq(A),Depth,seq(B)) :- !,insert_recursion_depth(A,Depth,B). |
213 | | insert_recursion_depth(couple(A,B),Depth,couple(C,D)) :- !, |
214 | | insert_recursion_depth(A,Depth,C),insert_recursion_depth(B,Depth,D). |
215 | | insert_recursion_depth(record(Fields),Depth,record(RFields)) :- !,insert_recursion_depth_fields(Fields,Depth,RFields). |
216 | | insert_recursion_depth(X,_,X). |
217 | | |
218 | | insert_recursion_depth_fields([],_,[]). |
219 | | insert_recursion_depth_fields([field(Name,Type)|Rest],Depth,[field(Name,RType)|RRest]) :- |
220 | | insert_recursion_depth(Type,Depth,RType), |
221 | | insert_recursion_depth_fields(Rest,Depth,RRest). |
222 | | |
223 | | |
224 | | :- assert_must_succeed((kernel_freetypes:find_references([case(a,integer), |
225 | | case(b,set(freetype(aa))), |
226 | | case(c,couple(boolean,seq(freetype(bb)))), |
227 | | case(d,record([field(f1,constant), |
228 | | field(f2,freetype(cc)), |
229 | | field(f3,freetype(aa)), |
230 | | field(f4,integer)]))],[cc,bb,aa]))). |
231 | | /* finds all references to other free types */ |
232 | | find_references(Cases,Ids) :- find_references(Cases,[],Ids). |
233 | | find_references([],Refs,Refs). |
234 | | find_references([case(_,Type)|Rest],Acc,Refs) :- find_references_type(Type,Acc,TRefs),find_references(Rest,TRefs,Refs). |
235 | | find_references_type(Type,Refs) :- find_references_type(Type,[],Refs). |
236 | | find_references_type(freetype(Id),Acc,Res) :- !,(member(Id,Acc) -> Res=Acc ; Res=[Id|Acc]). |
237 | | find_references_type(set(X),Acc,Refs) :- !, find_references_type(X,Acc,Refs). |
238 | | find_references_type(seq(X),Acc,Refs) :- !, find_references_type(X,Acc,Refs). |
239 | | find_references_type(couple(X,Y),Acc,Refs) :- !, find_references_type(X,Acc,XRefs),find_references_type(Y,XRefs,Refs). |
240 | | find_references_type(record(Fields),Acc,Refs) :- !, find_references_fields(Fields,Acc,Refs). |
241 | | find_references_type(_,Refs,Refs). |
242 | | find_references_fields([],Refs,Refs). |
243 | | find_references_fields([field(_,Type)|Rest],Acc,Refs) :- |
244 | | find_references_type(Type,Acc,TRefs), |
245 | | find_references_fields(Rest,TRefs,Refs). |
246 | | |
247 | | /* find all references of a type (also indirect references) by breadth first search */ |
248 | | find_transitive_references(Type,Refs) :- |
249 | | find_references_type(Type,Refs1), |
250 | | find_transitive_references(Refs1,[],Refs). |
251 | | find_transitive_references([],Refs,Refs). |
252 | | find_transitive_references([Id|Rest],VisitedRefs,AllRefs) :- |
253 | | registered_freetype(Id,Cases), |
254 | | find_references(Cases,Refs), |
255 | | append([Id|Rest],VisitedRefs,FoundRefs), |
256 | | find_new_ids(Refs,FoundRefs,NewRefs), |
257 | | append(Rest,NewRefs,UnvisitedRefs), |
258 | | find_transitive_references(UnvisitedRefs,[Id|VisitedRefs],AllRefs). |
259 | | |
260 | | find_new_ids([],_,[]). |
261 | | find_new_ids([Id|Rest],Old,New) :- |
262 | | member(Id,Old),!, |
263 | | find_new_ids(Rest,Old,New). |
264 | | find_new_ids([Id|Rest],Old,[Id|New]) :- |
265 | | find_new_ids(Rest,Old,New). |
266 | | |
267 | | /* translate each case/2 into a case/3 where the third argument is "recursive" or "plain" */ |
268 | | mark_recursive_cases([],_,[]). |
269 | | mark_recursive_cases([case(C,Type)|Rest],Id,[case(C,Type,Mark)|MRest]) :- |
270 | ? | (recursive_case(Id,Type) -> |
271 | | Mark = recursive; |
272 | | Mark = plain), |
273 | | mark_recursive_cases(Rest,Id,MRest). |
274 | | |
275 | | recursive_case(Id,Type) :- |
276 | | find_transitive_references(Type,Refs), |
277 | ? | member(Id,Refs). |
278 | | |
279 | | /* used by kernel_objects:check_element_of */ |
280 | | % TODO: we could enumerate cases, maybe only if non-recursive |
281 | | is_a_freetype_wf(freeval(Id,Case,Value),Id,_WF) :- |
282 | | registered_freetype(Id,Cases), |
283 | | (freetype_with_single_case(Id,SC) -> Case=SC ; true), |
284 | | is_a_freetype_wf2(Case,Cases,Value). |
285 | | :- block is_a_freetype_wf2(-,?,?). |
286 | | is_a_freetype_wf2(Case,Cases,Value) :- |
287 | | member(case(Case,CT),Cases),!, |
288 | | basic_type(Value,CT). |
289 | | |
290 | | |
291 | | is_recursive_freetype(Id) :- |
292 | | extended_register(Id,_,recursive). |
293 | | |
294 | | freetype_cardinality(Id,Card) :- |
295 | | extended_register(Id,Cases,Rec), |
296 | | % if there is a recursive case, the cardinality is infinite |
297 | | ( Rec=recursive -> |
298 | | Card = inf |
299 | | ; |
300 | | sum_case_cardinality(Cases,0,Card)). |
301 | | sum_case_cardinality([],Card,Card). |
302 | | sum_case_cardinality([case(_Name,Type,_)|Crest],In,Out) :- |
303 | | max_cardinality(Type,TypeCard), |
304 | | safe_add(In,TypeCard,NewCard), |
305 | | sum_case_cardinality(Crest,NewCard,Out). |
306 | | |
307 | | is_infinite_freetype(Id) :- |
308 | | extended_register(Id,Cases,Rec), |
309 | | (Rec=recursive -> true ; has_infinite_case(Cases)). |
310 | | has_infinite_case([case(_Name,Type,Mark)|_]) :- |
311 | | is_infinite_case(Type,Mark),!. |
312 | | has_infinite_case([_|Crest]) :- |
313 | | has_infinite_case(Crest). |
314 | | is_infinite_case(_Type,recursive) :- !. % recursive types are always infinite [unless no base-case !?!?] |
315 | | is_infinite_case(Type,_) :- |
316 | | is_infinite_type(Type). |
317 | | |
318 | | is_maximal_freetype(_). |
319 | | % we assume a freetype is always maximal (i.e., covers all possible values with its basic type) |
320 | | % TO DO: Daniel check this ! |
321 | | |
322 | | is_empty_freetype(_) :- fail. |
323 | | is_non_empty_freetype(_). |
324 | | test_empty_freetype(_,pred_false). |
325 | | % we assume all freetypes are not empty; TO DO: DANIEL please check |
326 | | |
327 | | % get the basic type of a freeval(Id,Case,Val) for Val |
328 | | get_freeval_type(Id,Case,CaseType) :- |
329 | | registered_freetype(Id,_), |
330 | | freetype_case_db(Case,Id,CaseType). |