1		% (c) 2009-2019 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		,reset_freetypes/0
8		,add_freetype/2
9		,enumerate_freetype/3
10		,max_cardinality_freetype/2
11		,set_freetype_depth/1
12		,is_a_freetype_wf/3
13		,freetype_cardinality/2
14		,is_infinite_freetype/1
15		,is_maximal_freetype/1
16		,is_empty_freetype/1
17		,is_non_empty_freetype/1
18		,test_empty_freetype/2
19		,get_freeval_type/3]).
20
21		/* This module contains predicates for the support for free types as they are used in Z specifications */
22
23		:- use_module(module_information,[module_info/2]).
24		:- module_info(group,proz).
25		:- module_info(description,'This module contains predicates that cope with the internal freetype. This is currently only used by the Z extension.').
26
27		:- use_module(library(lists)).
28
29		:- use_module(error_manager,[add_internal_error/2]).
30		:- use_module(self_check).
31		:- use_module(preferences,[get_preference/2]).
32		:- use_module(kernel_objects,[basic_type/2,
33		enumerate_type/3,
34		max_cardinality/2,safe_add/3]).
35		:- use_module(typing_tools,[is_infinite_type/1]).
36
37
38		:- dynamic freetype_register_db/2, max_iteration_depth/1, marked_cases/2, max_cardinality_db/3.
39
40		/* freetype_register queries the database of registered free types for the list of cases */
41		registered_freetype(Id, Cases) :- freetype_register_db(Id,Cases).
42
43		/* the extended register contains for each case a mark if it is recursive or not,
44		for internal use only (regarding the module) */
45		extended_register(Id, ECases) :- marked_cases(Id,Cs),!,ECases = Cs.
46		extended_register(Id, ECases) :-
47		registered_freetype(Id,Cases),mark_recursive_cases(Cases,Id,ECases),
48		assert(marked_cases(Id,ECases)).
49
50		/* reset_freetypes clears the database of registered free types */
51		reset_freetypes :-
52		retractall(freetype_register_db(_,_)),
53		retractall(marked_cases(_,_)),
54		retractall(max_iteration_depth(_)),
55		retractall(max_cardinality_db(_,_,_)).
56
57		/* with set_freetype_depth it is possible to set the maximum recursion depth of
58		free types when enumerating them. If the depth is not set manually the
59		depth is taken from the preference globalsets_fdrange. Mainly for testing */
60		set_freetype_depth(Depth) :-
61		retractall(max_iteration_depth(_)),assert(max_iteration_depth(Depth)).
62
63		/* add_freetypes appends a new free type to the database of free types */
64		add_freetype(Id, Cases) :-
65		( is_caselist(Cases) ->
66		( registered_freetype(Id,_) ->
67		add_internal_error('freetype already registered: ', add_freetype(Id, Cases)),fail
68		; registered_freetype(OId,Cs),member(case(C,_),Cs),member(case(C,_),Cases) ->
69		add_internal_error('freetype case registered twice: ', (C,OId,Id)),fail
70		; otherwise ->
71		assert(freetype_register_db(Id,Cases))
72		)
73		; otherwise ->
74		add_internal_error('list of cases invalid', add_freetype(Id, Cases)),fail).
75
76		/* enumerates a free type with regard to the maximum recursive iteration of free types.
77		The first argument is "basic" or "tight", depending on wich enumeration method
78		should be used for the value of the included types. */
79		enumerate_freetype(EType,freeval(Id,C,Value),freetype(Id)) :-
80		max_freetype_depth(MaxDepth),
81		enumerate_freetype(EType,freeval(Id,C,Value),freetype(Id,MaxDepth)).
82		enumerate_freetype(EType,freeval(Id,C,Value),freetype(Id,Depth)) :-
83		Depth > 0,
84		extended_register(Id,Cases),
85		member(case(C,CT,Mark),Cases),
86		/* If the case is recursive we have to append information about the
87		maximum recursion depth to limit the size of the data structure.
88		In the non-recursive case we leave the type untouched */
89		(Mark = recursive ->
90		(NewDepth is Depth - 1, insert_recursion_depth(CT,NewDepth,NewCT));
91		NewCT = CT),
92		enumerate_type(Value, NewCT, EType).
93
94
95		/* gives the maximumm cardinality of the free type with regard to the maximum
96		recursive iteration of free types */
97		max_cardinality_freetype(freetype(Id),Card) :-
98		max_freetype_depth(MaxDepth),
99		max_cardinality_freetype(freetype(Id,MaxDepth),Card).
100		max_cardinality_freetype(freetype(Id,Depth),Card) :-
101		(Depth > 0 ->
102		/* we save the computed cardinality for a certain maximum depth to
103		prevent exponential computation steps */
104		(max_cardinality_db(Id,Depth,Card) -> true;
105		(NewDepth is Depth - 1,
106		extended_register(Id,Cases),
107		sum_cases_cardinalities(Cases,NewDepth,Card),
108		assert(max_cardinality_db(Id,Depth,Card))));
109		Card = 0).
110
111		sum_cases_cardinalities([],_,0).
112		sum_cases_cardinalities([case(_,Type,Mark)|Rest],Depth,Card) :-
113		sum_cases_cardinalities(Rest,Depth,CRest),
114		/* like in enumerate_freetype we distinguish between recursive and
115		non-recursive cases and add information about the maximum recursion
116		depth in the former case. */
117		(Mark = recursive ->
118		insert_recursion_depth(Type,Depth,NewType);
119		NewType = Type),
120		max_cardinality(NewType,C),
121		add_with_inf(CRest,C,Card).
122
123		add_with_inf(inf,_,R) :- !,R=inf.
124		add_with_inf(_,inf,R) :- !,R=inf.
125		add_with_inf(A,B,R) :- R is A+B.
126
127		max_freetype_depth(Depth) :-
128		max_iteration_depth(Depth) -> true; get_preference(globalsets_fdrange,Depth).
129
130		/* Is the list a valid list of cases? */
131		is_caselist([]).
132		is_caselist([case(_,_)|Rest]) :- is_caselist(Rest).
133
134
135		/* Appends to all freetype references a maximum depth */
136		insert_recursion_depth(freetype(Id),Depth,freetype(Id,Depth)) :- !.
137		insert_recursion_depth(set(A),Depth,set(B)) :- !,insert_recursion_depth(A,Depth,B).
138		insert_recursion_depth(seq(A),Depth,seq(B)) :- !,insert_recursion_depth(A,Depth,B).
139		insert_recursion_depth(couple(A,B),Depth,couple(C,D)) :- !,
140		insert_recursion_depth(A,Depth,C),insert_recursion_depth(B,Depth,D).
141		insert_recursion_depth(record(Fields),Depth,record(RFields)) :- !,insert_recursion_depth_fields(Fields,Depth,RFields).
142		insert_recursion_depth(X,_,X).
143
144		insert_recursion_depth_fields([],_,[]).
145		insert_recursion_depth_fields([field(Name,Type)|Rest],Depth,[field(Name,RType)|RRest]) :-
146		insert_recursion_depth(Type,Depth,RType),
147		insert_recursion_depth_fields(Rest,Depth,RRest).
148
149
150		:- assert_must_succeed((kernel_freetypes:find_references([case(a,integer),
151		case(b,set(freetype(aa))),
152		case(c,couple(boolean,seq(freetype(bb)))),
153		case(d,record([field(f1,constant),
154		field(f2,freetype(cc)),
155		field(f3,freetype(aa)),
156		field(f4,integer)]))],[cc,bb,aa]))).
157		/* finds all references to other free types */
158		find_references(Cases,Ids) :- find_references(Cases,[],Ids).
159		find_references([],Refs,Refs).
160		find_references([case(_,Type)|Rest],Acc,Refs) :- find_references_type(Type,Acc,TRefs),find_references(Rest,TRefs,Refs).
161		find_references_type(Type,Refs) :- find_references_type(Type,[],Refs).
162		find_references_type(freetype(Id),Acc,Res) :- !,(member(Id,Acc) -> Res=Acc ; Res=[Id|Acc]).
163		find_references_type(set(X),Acc,Refs) :- !, find_references_type(X,Acc,Refs).
164		find_references_type(seq(X),Acc,Refs) :- !, find_references_type(X,Acc,Refs).
165		find_references_type(couple(X,Y),Acc,Refs) :- !, find_references_type(X,Acc,XRefs),find_references_type(Y,XRefs,Refs).
166		find_references_type(record(Fields),Acc,Refs) :- !, find_references_fields(Fields,Acc,Refs).
167		find_references_type(_,Refs,Refs).
168		find_references_fields([],Refs,Refs).
169		find_references_fields([field(_,Type)|Rest],Acc,Refs) :-
170		find_references_type(Type,Acc,TRefs),
171		find_references_fields(Rest,TRefs,Refs).
172
173		/* find all references of a type (also indirect references) by breadth first search */
174		find_transitive_references(Type,Refs) :-
175		find_references_type(Type,Refs1),
176		find_transitive_references(Refs1,[],Refs).
177		find_transitive_references([],Refs,Refs).
178		find_transitive_references([Id|Rest],VisitedRefs,AllRefs) :-
179		registered_freetype(Id,Cases),
180		find_references(Cases,Refs),
181		append([Id|Rest],VisitedRefs,FoundRefs),
182		find_new_ids(Refs,FoundRefs,NewRefs),
183		append(Rest,NewRefs,UnvisitedRefs),
184		find_transitive_references(UnvisitedRefs,[Id|VisitedRefs],AllRefs).
185
186		find_new_ids([],_,[]).
187		find_new_ids([Id|Rest],Old,New) :-
188		member(Id,Old),!,
189		find_new_ids(Rest,Old,New).
190		find_new_ids([Id|Rest],Old,[Id|New]) :-
191		find_new_ids(Rest,Old,New).
192
193		/* translate each case/2 into a case/3 where the third argument is "recursive" or "plain" */
194		mark_recursive_cases([],_,[]).
195		mark_recursive_cases([case(C,Type)|Rest],Id,[case(C,Type,Mark)|MRest]) :-
196		(recursive_case(Id,Type) ->
197		Mark = recursive;
198		Mark = plain),
199		mark_recursive_cases(Rest,Id,MRest).
200
201		recursive_case(Id,Type) :-
202		mnf(kernel_freetypes:find_transitive_references(Type,Refs)),
203		member(Id,Refs).
204
205		/* used by kernel_objects:check_element_of */
206		is_a_freetype_wf(freeval(Id,Case,Value),Id,_WF) :-
207		registered_freetype(Id,Cases),
208		is_a_freetype_wf2(Case,Cases,Value).
209		:- block is_a_freetype_wf2(-,?,?).
210		is_a_freetype_wf2(Case,Cases,Value) :-
211		member(case(Case,CT),Cases),!,
212		basic_type(Value,CT).
213
214		freetype_cardinality(Id,Card) :-
215		extended_register(Id,Cases),
216		% if there is a recursive case, the cardinality is infinite
217		( memberchk( case(_,_,recursive), Cases ) ->
218		Card = inf
219		; otherwise ->
220		sum_case_cardinality(Cases,0,Card)).
221		sum_case_cardinality([],Card,Card).
222		sum_case_cardinality([case(_Name,Type,_)|Crest],In,Out) :-
223		max_cardinality(Type,TypeCard),
224		safe_add(In,TypeCard,NewCard),
225		sum_case_cardinality(Crest,NewCard,Out).
226
227		is_infinite_freetype(Id) :-
228		extended_register(Id,Cases),
229		has_infinite_case(Cases).
230		has_infinite_case([case(_Name,Type,Mark)|_]) :-
231		is_infinite_case(Type,Mark),!.
232		has_infinite_case([_|Crest]) :-
233		has_infinite_case(Crest).
234		is_infinite_case(_Type,recursive) :- !. % recursive types are always infinite
235		is_infinite_case(Type,_) :-
236		is_infinite_type(Type).
237
238		is_maximal_freetype(_).
239		% we assume a freetype is always maximal (i.e., covers all possible values with its basic type)
240		% TO DO: Daniel check this !
241
242		is_empty_freetype(_) :- fail.
243		is_non_empty_freetype(_).
244		test_empty_freetype(_,pred_false).
245		% we assume all freetypes are not empty; TO DO: DANIEL please check
246
247		% get the basic type of a freeval(Id,Case,Val) for Val
248		get_freeval_type(Id,Case,CaseType):-
249		registered_freetype(Id,Cases),
250		member(case(Case,CaseType),Cases).