1 % (c) 2009-2026 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(typing_tools,[
6 is_infinite_type/1, % check if a type is infinite for animation purposes
7 is_provably_finite_type/1, % check if a type is provably finite (not just for animation)
8 is_finite_type_in_context/2, % check if a type is finite, either in animation or proving context
9
10 type_has_at_least_two_elements/1,
11 non_empty_type/1,
12
13 valid_ground_type/1, % check if a type is a valid ground type
14 contains_infinite_type/1,
15 any_value_for_type/2,
16 normalize_type/2,
17 create_maximal_type_set/2, % converts sequences to cartesian product
18 create_type_set/2, % keeps sequence types
19 create_type_set/3, % with flag for keeping sequences types or not
20 lift_type_parameters/3,
21 check_type_of_value/2
22 ]).
23 :- use_module(module_information,[module_info/2]).
24 :- module_info(group,typechecker).
25 :- module_info(description,'This module provides utilities for B types.').
26
27 %:- use_module(bsyntaxtree, [get_texpr_types/2, syntaxtraversion/6, find_typed_identifier_uses/3]).
28 :- use_module(library(lists), [maplist/2, maplist/3]).
29
30 :- use_module(kernel_freetypes,[is_infinite_freetype/1, freetype_has_at_least_two_elements/1]).
31 :- use_module(probsrc(translate), [pretty_type/2]).
32 :- use_module(probsrc(tools_strings),[ajoin/2]).
33 :- use_module(avl_tools,[check_is_non_empty_avl/1, avl_fetch_root/2]).
34
35 % check if a type is infinite for ProB animation; deferred sets are not counted as infinite here!
36 is_infinite_type(X) :- var(X),!, add_internal_error('Variable as type:',is_infinite_type(X)),fail.
37 is_infinite_type(integer).
38 is_infinite_type(real).
39 is_infinite_type(string).
40 is_infinite_type(freetype(Id)) :- is_infinite_freetype(Id). % will call back is_infinite_type
41 is_infinite_type(global(G)) :- infinite_global_set(G).
42 is_infinite_type(set(X)) :- is_infinite_type(X).
43 is_infinite_type(seq(_)).
44 is_infinite_type(couple(X,Y)) :- (is_infinite_type(X) -> true ; is_infinite_type(Y)).
45 is_infinite_type(record(Fields)) :-
46 ? ((member(field(_,Type),Fields), is_infinite_type(Type)) -> true).
47
48 contains_infinite_type([H|T]) :-
49 (is_infinite_type(H) -> true ; contains_infinite_type(T)).
50
51 :- use_module(b_global_sets,[provably_finite_global_set/1, b_empty_global_set/1, infinite_global_set/1]).
52
53 % this a finite type for the prover, not just for animation
54 % e.g., deferred sets in Event-B are not finite; in classical B they are in principle finite
55 is_provably_finite_type(X) :-
56 var(X),!,fail. % e.g., in tests 402, 403 this predicate can be called with variables in the type
57 is_provably_finite_type(boolean).
58 is_provably_finite_type(set(X)) :- is_provably_finite_type(X).
59 is_provably_finite_type(couple(X,Y)) :- is_provably_finite_type(X),is_provably_finite_type(Y).
60 is_provably_finite_type(global(G)) :-
61 provably_finite_global_set(G). % Note: in Classical B in principle all SETS are finite !
62 % note that scope_ DEFINITIONS make the set G finite here: TODO : investigate what we want/need
63 is_provably_finite_type(record(Fields)) :- maplist(finite_field,Fields).
64 is_provably_finite_type(constant([_])).
65 % TODO: freetype
66
67 finite_field(field(_,Type)) :- is_provably_finite_type(Type).
68
69
70
71 is_finite_type_in_context(animation,Type) :-
72 !, \+ is_infinite_type(Type). % all deferred sets counted as finite here; assumes record_construction already ran
73 is_finite_type_in_context(proving,Type) :-
74 is_provably_finite_type(Type). % here deferred sets can be in principle infinite; see Classical B comment above
75
76 % -------------------
77
78 type_has_at_least_two_elements(X) :- var(X),!,fail.
79 type_has_at_least_two_elements(boolean).
80 type_has_at_least_two_elements(string).
81 type_has_at_least_two_elements(integer).
82 type_has_at_least_two_elements(real).
83 type_has_at_least_two_elements(couple(A,B)) :-
84 ( type_has_at_least_two_elements(A) -> non_empty_type(B)
85 ; type_has_at_least_two_elements(B), non_empty_type(A)).
86 type_has_at_least_two_elements(set(A)) :- non_empty_type(A).
87 type_has_at_least_two_elements(seq(A)) :- non_empty_type(A).
88 type_has_at_least_two_elements(record([field(_,Type)|TF])) :-
89 (type_has_at_least_two_elements(Type) -> true
90 ; type_has_at_least_two_elements(record(TF))).
91 type_has_at_least_two_elements(freetype(Id)) :-
92 freetype_has_at_least_two_elements(Id).
93 type_has_at_least_two_elements(constant([_,_|_])). % type occurs in freetype, but always with one constant
94
95
96 % normally all types are non-empty!
97 non_empty_type(X) :- var(X),!,fail.
98 non_empty_type(boolean).
99 non_empty_type(string).
100 non_empty_type(integer).
101 non_empty_type(real).
102 non_empty_type(global(G)) :- \+ b_empty_global_set(G).
103 non_empty_type(set(_)). % always empty set as element of the type
104 non_empty_type(seq(_)).
105 non_empty_type(couple(A,B)) :- non_empty_type(A), non_empty_type(B).
106 non_empty_type(freetype(_)).
107 non_empty_type(record(Fields)) :- maplist(non_empty_field,Fields).
108 non_empty_type(constant([_|_])). % type used in kernel_freetypes
109
110 non_empty_field(field(_,Type)) :- non_empty_type(Type).
111
112 % --------------------
113
114 :- use_module(error_manager).
115
116 valid_ground_type(X) :- var(X),!, add_error(valid_ground_type,'Variable as type: ',X),fail.
117 valid_ground_type(X) :- valid_ground_type_aux(X),!.
118 valid_ground_type(X) :- add_error(valid_ground_type,'Illegal type term: ',X),fail.
119
120 %:- use_module(b_global_sets,[b_global_set/1]).
121
122 valid_ground_type_aux(any) :-
123 format(user_error,'! Type contains *any*~n',[]).
124 % can happen, e.g., for test 949 due to assertion prj1({{}},BOOL)({}|->TRUE) = {} or test 292 for {}<->{}={}
125 valid_ground_type_aux(integer).
126 valid_ground_type_aux(real).
127 valid_ground_type_aux(string).
128 valid_ground_type_aux(boolean).
129 valid_ground_type_aux(global(G)) :- atom(G).
130 %bmachine:b_get_machine_set(G).
131 %b_global_sets:b_global_set(G).
132 valid_ground_type_aux(freetype(FT)) :- ground(FT).
133 valid_ground_type_aux(set(X)) :- valid_ground_type(X).
134 valid_ground_type_aux(seq(X)) :- valid_ground_type(X).
135 valid_ground_type_aux(couple(X,Y)) :- valid_ground_type(X), valid_ground_type(Y).
136 valid_ground_type_aux(record(Fields)) :- valid_fields(Fields,'$prev_field_name').
137 valid_ground_type_aux(constant([X])) :- ground(X). % appears in Z freetype cases, test 738
138
139 valid_fields([],_).
140 valid_fields([field(Name,_)|_],_) :- \+ atom(Name),!,
141 add_error(valid_ground_type,'Illegal record field name: ',Name),fail.
142 valid_fields([field(Name,_)|_],PrevName) :- Name @=< PrevName,!,
143 add_error(valid_ground_type,'Record field names not sorted: ',PrevName:Name),fail.
144 valid_fields([field(Name,Type)|T],_) :-
145 valid_ground_type(Type),
146 valid_fields(T,Name).
147
148
149 % --------------
150
151 :- use_module(kernel_freetypes,[get_freeval_type/3]).
152 :- use_module(b_global_sets,[b_get_fd_type_bounds/3,get_global_type_value/3]).
153 any_value_for_type(T,V) :- if(inst2(T,V),true, (nl,print('*** instantiate_to_any_value failed: '), print(T:V),nl,nl %,trace,inst2(T,V)
154 )).
155 %inst2(_,V) :- ground(V),!.
156 inst2(boolean,V) :- !, inst3(V,pred_true).
157 inst2(pred,V) :- !, inst3(V,pred_true).
158 inst2(integer,V) :- !, V=int(X),inst_fd(X,0).
159 inst2(set(_),V) :- !, inst3(V,[]). % TO DO: what if V already partially instantiated
160 inst2(seq(_),V) :- !, inst3(V,[]). % TO DO: what if V already partially instantiated
161 inst2(couple(TA,TB),V) :- !, V=(A,B), inst2(TA,A), inst2(TB,B).
162 %inst2(real,V) :- !, V=... % TO DO
163 inst2(string,V) :- !, V=string(X), inst3(X,'').
164 inst2(real,V) :- !, V=term(X), (var(X) -> X=floating(0.0) ; X=floating(Y), inst3(Y,0.0)).
165 inst2(global(T),V) :- !, get_global_type_value(V,T,X),
166 b_get_fd_type_bounds(T,LowBnd,_UpBnd),
167 inst_fd(X,LowBnd).
168 inst2(record(Fields),rec(Vals)) :- !, instantiate_fields(Fields,Vals).
169 inst2(constant([A]),V) :- !, V=term(A).
170 inst2(freetype(FT),V) :- !, V=freeval(FT,CASE,Val),
171 (nonvar(CASE) -> (get_freeval_type(FT,CASE,Type) -> any_value_for_type(Type,Val)) % ensure no backtracking
172 ; nonvar(Val) -> print((nonvar_value(V))),nl, get_freeval_type(FT,CASE,Type), any_value_for_type(Type,Val)
173 ? ; (get_freeval_type(FT,C,Type) -> CASE=C, any_value_for_type(Type,Val))
174 ).
175 inst2(X,V) :- print(cannot_inst2(X,V)),nl.
176
177 inst3(X,V) :- (var(X) -> X=V ; true).
178
179 :- use_module(probsrc(clpfd_interface), [clpfd_some_element_in_domain/2]).
180 inst_fd(X,_) :- nonvar(X),!.
181 inst_fd(X,_Default) :- clpfd_some_element_in_domain(X,El),!, X=El.
182 inst_fd(X,X).
183
184 instantiate_fields([],[]).
185 instantiate_fields([field(Name,Type)|T],[field(Name,Val)|TV]) :-
186 any_value_for_type(Type,Val),
187 instantiate_fields(T,TV).
188
189 % ----------------------
190
191 % replace seq(X) by set(couple(integer,X))
192
193 normalize_type(X,Y) :-
194 (normalize_type_aux(X,Y) -> true ; add_internal_error('Illegal type: ',normalize_type(X,Y)),Y=X).
195
196 normalize_type_aux(V,R) :- var(V),!,R=V.
197 normalize_type_aux(any,any).
198 normalize_type_aux(pred,pred).
199 normalize_type_aux(subst,subst).
200 normalize_type_aux(boolean,boolean).
201 normalize_type_aux(integer,integer).
202 normalize_type_aux(string,string).
203 normalize_type_aux(real,real).
204 normalize_type_aux(constant(C),constant(C)).
205 normalize_type_aux(global(F),global(F)).
206 normalize_type_aux(freetype(F),freetype(F)).
207 normalize_type_aux(set(X),set(N)) :- normalize_type_aux(X,N).
208 normalize_type_aux(seq(X),set(couple(integer,N))) :- normalize_type_aux(X,N).
209 normalize_type_aux(couple(X,Y),couple(NX,NY)) :- normalize_type_aux(X,NX),normalize_type_aux(Y,NY).
210 normalize_type_aux(record(F),record(NF)) :- normalize_type_fields(F,NF).
211 normalize_type_aux(op(A,B),op(NA,NB)) :- maplist(normalize_type_aux,A,NA), maplist(normalize_type_aux,B,NB).
212
213 normalize_type_fields(V,R) :- var(V),!,R=V.
214 normalize_type_fields([],[]).
215 normalize_type_fields([field(N,T)|R],[field(N,NT)|RN]) :- normalize_type_aux(T,NT),normalize_type_fields(R,RN).
216
217 % -------------------------
218
219 % usage: lift_type_parameters(couple(t1,t1),[t1],R) --> R=couple(T,T)
220 lift_type_parameters(GroundType,[],LiftedType) :- !, LiftedType=GroundType.
221 lift_type_parameters(Type,TypeParameters,LiftedType) :-
222 sort(TypeParameters,STP),
223 maplist(gen_var,STP,Env),
224 lift_aux(Type,Env,LT),
225 LT=LiftedType.
226
227 gen_var(ID,ID-_).
228
229 lift_aux([],_,R) :- !, R=[].
230 lift_aux([H|T],Env,[LH|LT]) :- !, lift_aux(H,Env,LH), lift_aux(T,Env,LT).
231 lift_aux(Type,Env,Res) :- member(Type-Var,Env),!, Res=Var.
232 lift_aux(set(X),Env,set(LX)) :- !, lift_aux(X,Env,LX).
233 lift_aux(seq(X),Env,seq(LX)) :- !, lift_aux(X,Env,LX).
234 lift_aux(record(X),Env,record(LX)) :- !, lift_aux(X,Env,LX).
235 lift_aux(field(Name,X),Env,field(Name,LX)) :- lift_aux(X,Env,LX).
236 lift_aux(couple(X,Y),Env,couple(NX,NY)) :- !, lift_aux(X,Env,NX), lift_aux(Y,Env,NY).
237 lift_aux(Type,_,Type).
238
239 % -------------------------
240
241 :- use_module(bsyntaxtree, [create_texpr/4]).
242
243 % translate a ProB type into a B expression so that we can write x:TSet
244 % translate_type:
245 create_type_set(Type,TSet) :- create_type_set(Type,true,TSet).
246 create_type_set(Type,KeepSeq,TSet) :-
247 ( var(Type) -> add_error_and_fail(translate,'type_set Type is variable: ',Type)
248 ;
249 type_set2(Type,KeepSeq,Set,Infos),
250 create_texpr(Set,set(Type),Infos,TSet)).
251 type_set2(set(T),KeepSeq,pow_subset(Set),[]) :-
252 create_type_set(T,KeepSeq,Set).
253 type_set2(seq(T),KeepSeq,Res,Info) :-
254 (KeepSeq = true
255 -> Res=seq(Set), Info=[], create_type_set(T,KeepSeq,Set) % keep sequence types as is
256 ; type_set2(set(couple(integer,T)),KeepSeq,Res,Info)). % write as POW(INTEGER*T)
257 type_set2(couple(TA,TB),KeepSeq,cartesian_product(SetA,SetB),[]) :-
258 create_type_set(TA,KeepSeq,SetA), create_type_set(TB,KeepSeq,SetB).
259 %type_set2(global(G),_,identifier(G),[given_set]).
260 type_set2(global(G),_,value(global_set(G)),[given_set]). % avoids variable capture/clash
261 type_set2(integer,_,integer_set('INTEGER'),[]).
262 type_set2(string,_,string_set,[]).
263 type_set2(real,_,real_set,[]).
264 type_set2(boolean,_,bool_set,[]).
265 type_set2(record(TFields), KeepSeq, struct(Rec),[]) :-
266 create_texpr(rec(SFields),record(TFields),[],Rec),
267 type_set_fields(TFields,KeepSeq,SFields).
268 %type_set2(freetype(Id),identifier(Id),[given_set]).
269 % Missing: no case for constant([C]) term
270 type_set2(freetype(Id),_,freetype_set(Id),[]).
271 type_set2(constant(L),_,value(Terms),[]) :- % these types occur in Event-B for Theory plugin inductive datatypes
272 (var(L) -> add_internal_error('Illegal var constant list: ',type_set2(constant(L),_,value(Terms),[])) ; true),
273 maplist(create_term,L,Terms).
274 create_term(T,term(T)).
275 type_set_fields([],_,[]).
276 type_set_fields([field(Id,Type)|TFrest],KeepSeq,[field(Id,TSet)|EFrest]) :-
277 create_type_set(Type,KeepSeq,TSet),
278 type_set_fields(TFrest,KeepSeq,EFrest).
279
280 % translate a ProB type to a typed expression representing the maximal type
281 % set_type_to_maximal_texpr
282 create_maximal_type_set(ProBType,TExpr) :- create_type_set(ProBType,false,TExpr).
283 %replace_seq(ProBType,MType),create_type_set(MType,TExpr).
284
285 % translate a ProB type into a B value of all values of the type is done in b_type2_set
286
287
288 % ------------------------
289 % check whether a value matches an expected type
290 % does not traverse the entire value, e.g., for sets only one element is inspected
291 % see check_type in spec_file for CSP conversion
292 % see adapt_value_according_to_type in translate
293
294 :- use_module(b_global_sets,[b_global_set/1,b_get_fd_type_bounds/3,global_type/2]).
295
296 check_type_of_value(_,Var) :- var(Var),!.
297 check_type_of_value(T,V) :- var(T),!,
298 add_internal_error('Variable type: ',check_type_of_value(T,V)),fail.
299 check_type_of_value(any,_Value) :- !.
300 check_type_of_value(integer,int(_)) :- !.
301 check_type_of_value(string,string(_)) :- !.
302 check_type_of_value(real,term(_)) :- !.
303 check_type_of_value(boolean,V) :- (V=pred_true ; V=pred_false), !.
304 check_type_of_value(global(GlobalSet),fd(Nr,GlobalSet)) :- !,
305 (\+ b_global_set(GlobalSet)
306 -> add_error(check_type_of_value,'Unknown reference to global set in value:',GlobalSet),fail
307 ; var(Nr) -> true
308 ; global_type(fd(Nr,GlobalSet),GlobalSet) -> true
309 ; b_get_fd_type_bounds(GlobalSet,Min,Max),
310 ajoin(['Index for element of global set ',GlobalSet,' is not in range ',Min,'..',Max,':'],Msg),
311 add_error(check_type_of_value,Msg,Nr),fail
312 ).
313 check_type_of_value(couple(TA,TB),(VA,VB)) :- !,
314 (check_type_of_value(TA,VA) -> check_type_of_value(TB,VB)).
315 check_type_of_value(set(Type),Set) :- !, check_type_of_set(Set,Type).
316 check_type_of_value(seq(Type),Set) :- !, check_type_of_set(Set,couple(integer,Type)).
317 check_type_of_value(record(Fields),rec(Values)) :- !,
318 % fields and values should be in the same (alphabetical) order
319 maplist(check_type_of_record_field,Fields,Values).
320 check_type_of_value(freetype(_),Value) :-
321 Value = freeval(ID,_,Term),
322 nonvar(Term), Term=term(ID), % not a constructor, just a value
323 !.
324 check_type_of_value(freetype(_),freeval(ID,Case,SubValue)) :- nonvar(Case),
325 !,
326 (kernel_freetypes:get_freeval_type(ID,Case,SubType)
327 -> check_type_of_value(SubType,SubValue)
328 ; ajoin(['Could not get freevalue case ',Case,' for freevalue type:'],Msg),
329 add_error(check_type_of_value,Msg,ID),
330 fail
331 ).
332 check_type_of_value(freetype(_),_Value) :- !. % TODO
333 check_type_of_value(pred,V) :- (V=pred_true ; V=pred_false), !.
334 check_type_of_value(_,term(_V)) :-
335 !. % appears for unknown values (no_value_for) when ALLOW_INCOMPLETE_SETUP_CONSTANTS is true
336 check_type_of_value(Type,Value) :-
337 pretty_type(Type,TS),
338 ajoin(['Value does not match expected type ',TS,':'],Msg),
339 add_error(check_type_of_value,Msg,Value),fail.
340
341 check_type_of_set([],_).
342 check_type_of_set(avl_set(A),Type) :- check_is_non_empty_avl(A),
343 avl_fetch_root(A,Root), % just check type of root value
344 % TODO: maybe check a few more, e.g., in case Root has by chance an empty set as sub-value
345 check_type_of_value(Type,Root).
346 check_type_of_set([H|_],Type) :-
347 check_type_of_value(Type,H).
348
349
350 check_type_of_record_field(field(Name,HTy),field(Name2,H)) :-
351 (Name=Name2 -> check_type_of_value(HTy,H)
352 ; ajoin(['Record field ',Name,' does not match expected name from type:'],Msg),
353 add_error(check_type_of_value,Msg,Name2),fail
354 ).
355
356
357
358