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).