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(bsyntaxtree,
6 [is_texpr/1, % checks if the given argument is a typed expression
7
8 get_texpr_expr/2, % get the expression part of a typed expression
9 get_texpr_type/2, % get the type of a typed expression
10 get_texpr_info/2, % get the list of information of a typed expression
11 get_texpr_id/2, % get the id of a typed identifier, fails if it's not an identifier
12 def_get_texpr_id/2, % same as above, but raises error if arg1 is not an identifier
13 def_get_texpr_ids/2, % maplist of the above, i.e., translate a typed id list into a plain list of id names
14 create_typed_id/3, % create a typed identifier
15 create_typed_ids/3, % create a list of typed identifiers from list of names and types
16 same_id/3, % true if two typed identifiers have the same id
17 same_ids/2, % true if two lists of typed identifiers have the same ids
18 same_ids_and_types/2, % also check types
19 split_names_and_types/3, % split list of typed ids into ids and types
20 get_texpr_exprs/2, % list variant of the above
21 get_texpr_types/2, % list variant of the above
22 get_texpr_infos/2, % list variant of the above
23 get_texpr_ids/2, % list variant of the above
24 get_texpr_pos/2, % get the position of a typed expression
25 get_texpr_pos_infos/2, % the a list containing the position infos, sublist of get_texpr_infos
26 extract_pos_infos/2, % get the position info sub list of an info list
27 copy_pos_infos/3, % copy position infos from one typed expression to another
28 delete_pos_info/2, % delete position info from an info list
29 propagate_pos_info_if_useful/3, % propagate position info from second list if useful
30 merge_info/3, % merge two information lists as well as possible
31 update_infos/3, % provide updates to an existing info list
32 get_info_pos/2, % get the position directly from info field
33 contains_info_pos/1, % true if info field contains position infos
34
35 same_texpr/2, % check if two typed expressions are equal modulo Info fields
36 different_texpr_values/2, % check if two type expressions are WD and definitely denote different values
37
38 create_texpr/4, % creates a typed expression by giving expression, type and infos
39 add_texpr_infos/3, % adds some more information to a typed expression at front
40 add_texpr_info_if_new/3, % adds one info field to typed B expression info list at front if it is new
41 add_texpr_infos_if_new/3, % ditto but list of infos can be added
42 add_info_if_new/3, % adds to info list
43 add_infos_if_new/3, % same for list of info items
44 safe_create_texpr/3, % a version of create_texpr which extracts wd-info from sub-expressionssafe_create_texpr
45 safe_create_texpr/4,
46 texpr_contains_wd_condition/1,
47 sub_expression_contains_wd_condition/1, % utility to check if sub-expression contains wd condition
48
49 get_rodin_name/2, get_precise_rodin_name/2,
50 get_rodin_model_name/2,
51 is_rodin_label_info/1,
52 get_texpr_label/2, get_texpr_labels/2,
53 get_info_labels/2, select_info_labels/3,
54 add_labels_to_texpr/3,
55 get_texpr_description/2, % get @desc pragma for typed expression
56 add_texpr_description/3, % add an additional description by hand
57 info_has_ignore_pragma/1, % check if an info list has an ignore pragma
58 predicate_has_ignore_pragma/1, % ditto for the info list of a predicate
59 always_well_defined/1, always_well_defined_or_disprover_mode/1,
60 always_well_defined_or_wd_reorderings_allowed/1,
61 always_well_defined_or_wd_improvements_allowed/1,
62 finite_wd_set_value/1, finite_set_or_disprover_mode/1,
63 is_truth/1, is_falsity/1,
64 conjunct_predicates/2,
65 conjunct_predicates_with_pos_info/3, conjunct_predicates_with_pos_info/2,
66 is_a_conjunct/3, is_a_conjunct_without_label/3, decompose_conjunct/3,
67 is_a_disjunct/3, is_an_implication/3, is_an_equivalence/3, is_a_negation/2,
68 conjunction_to_list/2,
69 conjunction_to_list_with_rodin_labels/2, % a variation which propagates labels down to conjuncts
70 member_in_conjunction/2, select_member_in_conjunction/3,
71 flatten_conjunctions/2,
72 size_of_conjunction/2,
73 member_in_conjunction_cse/3,
74 disjunct_predicates/2,
75 disjunct_predicates_with_pos_info/3,
76 disjunction_to_list/2,
77 is_a_disjunct_or_implication/4,
78 is_a_conjunct_or_neg_disj/3,
79
80 predicate_components/2, % split a predicate into components which use distinct identifiers
81 predicate_components_in_scope/3, % ditto with an optional list of local variables
82 predicate_components_with_restriction/4,
83 predicate_identifiers/2, predicate_identifiers_in_scope/3,
84
85 project_predicate_on_identifiers/5,
86
87 find_identifier_uses_top_level/2, % not including global sets and constants
88 find_identifier_uses/3, find_identifier_uses_if_necessary/3,
89 find_identifier_uses_l/3,
90 find_typed_identifier_uses/3,
91 find_typed_identifier_uses/2, % not including global sets and constants
92 find_typed_identifier_uses_l/3,
93 find_identifier_uses_for_quantifier_body/3,
94 get_global_identifiers/1, get_global_identifiers/2,
95 occurs_in_expr/2, some_id_occurs_in_expr/2,
96 single_usage_identifier/3,
97 update_used_ids/3,
98 check_computed_used_ids/2,
99
100 create_exists/3, create_or_merge_exists/3,
101 create_exists_or_let_predicate/3,
102 create_exists_opt_liftable/3,
103 create_exists_opt/3, create_exists_opt/4, create_exists_opt/5,
104 not_generated_exists_paras/1,
105 create_forall/3,
106 infer_seq_types_for_tids/3,
107 create_negation/2, is_negation_of/2, get_negated_operator_expr/2,
108 create_implication/3,
109 create_equivalence/3,
110 is_equality/3,
111 create_equality/3, split_equality/3, get_texpr_couple/3,
112 create_couple/3, create_couple/2, nested_couple_to_list/2,
113 create_cartesian_product/3,
114 create_comprehension_set/4,
115 is_eventb_comprehension_set/4, is_eventb_comprehension_set/6,
116 singleton_set_extension/2,
117 is_membership/3, is_membership_or_equality/3,
118 get_lambda_equality/4,
119 is_succ_compset/2, is_pred_compset/2,
120 is_pow_subset/2, is_pow1_subset/2,
121
122 detect_global_predicates/4,
123
124 definitely_not_empty_set/1, definitely_empty_set/1, definitely_not_empty_finite_value/1,
125 get_integer/2,
126 get_interval/3,
127
128 replace_id_by_expr/4,
129 replace_id_by_expr_with_count/5, % also count number of replacements
130 replace_ids_by_exprs/4,
131 remove_used_id_from_info/3, % remove an id from used_id info field if it exists
132 remove_used_ids_from_info/3, % remove list of ids (order of args different !)
133
134 rename_bt/3, % a simplified version of replace_ids_by_exprs, which assumes target of renamings are variables
135 rename_bt_l/3,
136 remove_bt/4,
137 syntaxtransformation/5,
138 syntaxtransformation_det/5, % faster, non-backtracking version
139 syntaxtransformation_for_renaming/5,
140 remove_renamings/3,
141
142 map_over_bexpr/2, map_over_typed_bexpr/2, map_over_typed_bexpr/3,
143 map_over_typed_bexpr_with_names/2,
144 map_over_bexpr_top_down_acc/3, map_over_typed_bexpr_top_down_acc/3,
145 reduce_over_bexpr/4,
146 transform_bexpr/3, % transform a typed B expression bottom-up
147 transform_bexpr_with_scoping/3, % ditto, but we also provide info about local ids
148 transform_bexpr_td_with_scoping/3, % top-down with scoping
149 transform_bexpr_with_bup_accs/5, transform_bexpr_with_acc/5,
150 non_det_transform_bexpr_with_acc/5, % can be used to generate several transformed expressions
151 uses_implementable_integers/1,
152 min_max_integer_value_used/3, min_max_integer_value_used/5,
153 syntaxtraversion/6,
154 safe_syntaxelement/5,
155 safe_syntaxelement_det/5, % a deterministic, non-backtracking version
156 is_subst_syntaxelement/1,
157 is_syntax_constant/1,
158
159 expand_all_lets/2,
160
161 remove_all_infos/2, extract_info/2, extract_info/3, extract_info_wo_used_ids/2,
162 bsyntax_pattern/2,
163
164 remove_all_infos_and_ground/2,
165
166 check_if_typed_predicate/1,
167 check_if_typed_expression/1,
168 check_if_typed_substitution/1,
169
170 strip_and_norm_ast/2,
171 same_norm_texpr/2,
172 get_texpr_functor/3,
173
174 is_set_type/2, get_set_type/2, get_texpr_set_type/2,
175 is_just_type/1, is_just_type/2,
176 get_texpr_boolean/2,
177
178 create_recursive_compset/6,
179 unique_typed_id/3,
180 mark_bexpr_as_symbolic/2,
181
182 identifier_sub_ast/3, exchange_ast_position/5,
183
184 has_declared_identifier/2, add_declaration_for_identifier/3,
185 check_ast/1, check_ast/2,
186 repair_used_ids/3,
187 print_ast/1,
188 rewrite_if_then_else_expr_to_b/2,
189 normalise_bexpr_for_ml/2
190 ]).
191
192 % meta_predicate annotations should appear before loading any code:
193
194 :- meta_predicate map_over_full_bexpr_no_fail(1,?).
195
196 :- meta_predicate map_over_bexpr(1,?).
197 :- meta_predicate map_over_typed_bexpr(1,?).
198 :- meta_predicate map_over_typed_bexpr(2,?,?).
199 :- meta_predicate map_over_bexpr_top_down_acc(3,?,?).
200 :- meta_predicate map_over_typed_bexpr_top_down_acc(3,?,?).
201
202 :- meta_predicate reduce_over_bexpr(3,?,?,?).
203 :- meta_predicate transform_bexpr(2,?,?).
204 :- meta_predicate l_transform_bexpr(?,2,?).
205 :- meta_predicate transform_bexpr_with_scoping(3,?,?).
206 :- meta_predicate transform_bexpr_td_with_scoping(3,?,?).
207 :- meta_predicate transform_bexpr_with_scoping2(3,?,?,?).
208 :- meta_predicate l_transform_bexpr_with_scoping(?,3,?,?).
209 :- meta_predicate transform_bexpr_with_bup_accs(4,?,?,?,?).
210 :- meta_predicate l_transform_bexpr_with_bup_accs(?,4,?,?,?).
211 :- meta_predicate transform_bexpr_with_acc(4,?,?,?,?).
212 :- meta_predicate l_transform_bexpr_with_acc(?,4,?,?,?).
213 :- meta_predicate non_det_transform_bexpr_with_acc(4,?,?,?,?).
214 :- meta_predicate l_nd_transform_bexpr_with_acc(?,4,?,?,?).
215
216 % -----------
217
218
219 :- use_module(tools).
220
221 :- use_module(module_information,[module_info/2]).
222 :- module_info(group,typechecker).
223 :- module_info(description,'This module provides operations on the type-checked AST.').
224
225 :- use_module(library(lists)).
226 :- use_module(library(ordsets)).
227 :- use_module(library(avl)).
228 :- use_module(library(terms)).
229
230 :- use_module(self_check).
231 :- use_module(error_manager).
232 :- use_module(translate,[print_bexpr/1,translate_bexpression/2]).
233 :- use_module(gensym,[gensym/2]).
234 :- use_module(preferences,[get_preference/2,preference/2]).
235 :- use_module(debug,[debug_mode/1,debug_format/3]).
236
237 :- use_module(typing_tools,[is_finite_type_in_context/2,normalize_type/2]).
238 :- use_module(tools_lists,[convlist_max/4]).
239
240 :- set_prolog_flag(double_quotes, codes).
241
242 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
243 % basic access to enriched syntax tree
244
245 is_texpr(b(_,_,_)).
246
247 get_texpr_expr(b(Name,_,_),R) :- !,R=Name.
248 get_texpr_expr(E,_) :- add_error_fail(get_texpr_expr,'B Expression not properly wrapped: ',E).
249
250 get_texpr_type(b(_,Type,_),R) :- !, R=Type.
251 get_texpr_type(E,_) :- add_error_fail(get_texpr_type,'B Expression not properly wrapped: ',E).
252 get_texpr_info(b(_,_,Info),R) :- !, R=Info.
253 get_texpr_info(E,_) :- add_error_fail(get_texpr_info,'B Expression not properly wrapped: ',E).
254
255 %! get_texpr_id(+Texpr,-Id)
256 get_texpr_id(b(N,_,_),Id) :- !, N=identifier(Id).
257 get_texpr_id(E,_) :- add_error_fail(get_texpr_id,'B Expression not properly wrapped: ',E).
258 /* same as above: but must succeed */
259 def_get_texpr_id(b(identifier(Id),_,_),R) :- !,R=Id.
260 def_get_texpr_id(b(E,_,_),_) :- !,
261 add_error_fail(def_get_texpr_id,'Could not extract identifier from typed expression: ',E).
262 def_get_texpr_id(ID,_) :- add_error_fail(def_get_texpr_id,'Could not extract identifier, not properly wrapped: ',ID).
263
264 % translate a list of ids with the b/3 wrapper into a plain id list; throw error if not an identifier
265 % used to also be called get_texpr_id_names
266 def_get_texpr_ids(L,Ids) :- maplist(def_get_texpr_id,L,Ids).
267
268 create_typed_id(IDName,Type,b(identifier(IDName),Type,[])).
269
270 % inverse of split_names_and_types; merge atomic ids and types into typed identifiers
271 create_typed_ids([],[],[]).
272 create_typed_ids([ID|TI],[Type|TT],[TID| TRes]) :-
273 create_typed_id(ID,Type,TID),
274 create_typed_ids(TI,TT,TRes).
275
276 same_id(X,Y,ID) :- get_texpr_id(X,ID), get_texpr_id(Y,ID).
277
278 same_ids([],[]).
279 same_ids([X|Xs],[Y|Ys]) :- same_id(X,Y,_), same_ids(Xs,Ys).
280
281 % check if two lists of identifiers have the same name and types
282 same_ids_and_types([],[]).
283 same_ids_and_types([b(identifier(Id),T1,_)|Xs],[b(identifier(Id),T2,_)|Ys]) :- unify_types_strict(T1,T2),
284 same_ids_and_types(Xs,Ys).
285
286 % split a list of typed identifiers into atomic ids and types, inverse of create_typed_ids
287 split_names_and_types([],N,T) :- !, N=[], T=[].
288 split_names_and_types([Identifier|IdRest],[Name|NRest],[Type|TRest]) :- !,
289 def_get_texpr_id(Identifier,Name),
290 get_texpr_type(Identifier,Type),
291 split_names_and_types(IdRest,NRest,TRest).
292 split_names_and_types(TIDS,N,R) :-
293 add_internal_error('Illegal call to:',split_names_and_types(TIDS,N,R)),fail.
294
295
296
297 % check if two wrapped expressions are equal (modulo associated Info, e.g. source loc info)
298 same_texpr(b(E1,Type1,_),b(E2,Type2,_)) :-
299 % should we do a == check first? probably not as it may traverse entire term (see emails with SICStus 28.1.2015)
300 same_texpr4(E1,Type1,E2,Type2).
301
302 same_texpr4(empty_set,Type1,E2,Type2) :- !, is_empty_set_aux(E2), unify_types_strict(Type1,Type2).
303 same_texpr4(empty_sequence,Type1,E2,Type2) :- !, is_empty_set_aux(E2), unify_types_strict(Type1,Type2).
304 same_texpr4(value(V),Type1,E2,Type2) :- V==[], !, is_empty_set_aux(E2), unify_types_strict(Type1,Type2).
305 same_texpr4(E1,Type1,E2,Type2) :-
306 same_functor(E1,E2),
307 unify_types_strict(Type1,Type2), % can be relevant for test 1544, last assertion to detect if_then_else
308 safe_syntaxelement_det(E1,Subs1,_Names1,_List1,Constant),
309 safe_syntaxelement_det(E2,Subs2,_Names2,_List2,Constant2),
310 Constant==Constant2, % in case we have values with variables inside !
311 same_sub_expressions(Subs1,Subs2).
312
313 same_sub_expressions([],[]).
314 same_sub_expressions([H1|T1],[H2|T2]) :- same_texpr(H1,H2), same_sub_expressions(T1,T2).
315
316 % check if two wrapped expressions definitely denote a different value (and are well-defined)
317 % only detects certain cases !
318 different_texpr_values(b(E1,Type1,I1),b(E2,Type2,I2)) :-
319 different_value(E1,E2,CheckWD),
320 unify_types_strict(Type1,Type2),
321 (CheckWD=false -> true
322 ; always_well_defined_or_wd_improvements_allowed(b(E1,Type1,I1)),
323 always_well_defined_or_wd_improvements_allowed(b(E2,Type2,I2))).
324 different_value(boolean_false,boolean_true,false) :- !.
325 different_value(boolean_true,boolean_false,false) :- !.
326 different_value(integer(X),IY,false) :- get_integer_aux(IY,Y),!, X\=Y.
327 different_value(string(X),string(Y),false) :- !, X\=Y.
328 different_value(value(VX),Y,false) :- !, different_val_from(VX,Y).
329 different_value(empty_set,S,check_wd) :- !, non_empty_set(S).
330 different_value(empty_sequence,S,check_wd) :- !, non_empty_set(S).
331 different_value(S,empty_set,check_wd) :- !, non_empty_set(S).
332 different_value(S,empty_sequence,check_wd) :- !, non_empty_set(S).
333 % should we compare two set_extensions ? couples ? records ? reals/floats?
334
335 different_val_from(Var,_) :- var(Var),!,fail.
336 different_val_from(int(X),IY) :- integer(X), get_integer_aux(IY,Y), X\=Y.
337 different_val_from(fd(X,Gs),value(FY)) :- nonvar(X), nonvar(FY), FY=fd(Y,Gs), nonvar(Y), X\=Y.
338 different_val_from(pred_false,boolean_true).
339 different_val_from(pred_false,value(BY)) :- BY==pred_true.
340 different_val_from(pred_true,boolean_false).
341 different_val_from(pred_true,value(BY)) :- BY==pred_false.
342 different_val_from(string(X),string(Y)) :- !, X\=Y.
343 different_val_from(string(X),value(VY)) :- nonvar(VY), VY=string(Y), nonvar(Y), !, X\=Y.
344 different_val_from(avl_set(node(_,_,_,_,_)),empty_set).
345
346 non_empty_set(set_extension([_|_])).
347 non_empty_set(sequence_extension([_|_])).
348
349
350 get_texpr_exprs([],[]).
351 get_texpr_exprs([E|Rest],[N|NRest]) :- get_texpr_expr(E,N),get_texpr_exprs(Rest,NRest).
352 get_texpr_exprs(b(E,_,_),Res) :- add_internal_error('Illegal call:',get_texpr_infos(b(E,_,_),Res)), Res=[E].
353 get_texpr_types([],[]).
354 get_texpr_types([E|Rest],[T|TRest]) :- get_texpr_type(E,T),get_texpr_types(Rest,TRest).
355 get_texpr_types(b(_,T,_),Res) :- add_internal_error('Illegal call:',get_texpr_infos(b(_,T,_),Res)), Res=[T].
356 get_texpr_infos([],[]).
357 get_texpr_infos([E|Rest],[I|IRest]) :- get_texpr_info(E,I),get_texpr_infos(Rest,IRest).
358 get_texpr_infos(b(_,_,I),Res) :- add_internal_error('Illegal call:',get_texpr_infos(b(_,_,I),Res)), Res=[I].
359 get_texpr_ids([],[]).
360 ?get_texpr_ids([E|Rest],[I|IRest]) :- get_texpr_id(E,I),get_texpr_ids(Rest,IRest).
361
362 get_texpr_pos(TExpr,Pos) :-
363 get_texpr_info(TExpr,Infos),
364 ? ( member(nodeid(Pos1),Infos) -> !,Pos=Pos1
365 ; Pos = none).
366
367 get_texpr_pos_infos(b(_,_,Infos),PosInfos) :- extract_pos_infos(Infos,PosInfos).
368
369 % similar to get_texpr_pos, but returns sub-list of infos relating to position
370 extract_pos_infos(Infos,InfoRes) :-
371 ? ( member(nodeid(Pos1),Infos) -> !,InfoRes=[nodeid(Pos1)]
372 ; InfoRes = []).
373
374 % copy position info from first arg to second argument
375 copy_pos_infos(b(_,_,Infos1),Arg2,Res) :-
376 ? member(nodeid(Pos1),Infos1),!,
377 Arg2 = b(E,T,Infos2), Res = b(E,T,Infos3),
378 delete_pos_info(Infos2,Infos2d),
379 Infos3 = [nodeid(Pos1)|Infos2d].
380 copy_pos_infos(_,TE,TE).
381
382 delete_pos_info(Infos1,Infos2) :-
383 ? select(nodeid(_),Infos1,D),!, Infos2=D.
384 %delete(Infos1,nodeid(_),Infos2).
385 delete_pos_info(I,I).
386
387 % propagate position info from second list to first one if it has better position info
388 propagate_pos_info_if_useful(Infos,AuxInfos,NewInfos) :-
389 ? member(nodeid(Pos2),AuxInfos),
390 \+ derived_pos(Pos2),!, % potentially useful position info to propagate
391 ? (select(nodeid(Pos1),Infos,Infos2)
392 -> (derived_pos(Pos1)
393 -> NewInfos = [nodeid(Pos2)|Infos2] % we have better position info now
394 ; NewInfos = Infos % we already have a position info
395 )
396 ; NewInfos = [nodeid(Pos2)|Infos]
397 ).
398 propagate_pos_info_if_useful(Infos,_,Infos).
399
400 % derived position; not precise instrinsic label at top-level
401 derived_pos(rodin_derived_context_pos(_,_,_)).
402
403
404 ?get_info_pos(Infos,Pos) :- (member(nodeid(Pos1),Infos) -> Pos=Pos1 ; Pos=none).
405 contains_info_pos(Infos) :- (member(nodeid(NI),Infos) -> NI \= none).
406
407 create_texpr(Expr,Type,Info,b(Expr,Type,Info)).
408
409 add_texpr_infos(b(Expr,Type,Old),Infos,b(Expr,Type,New)) :- !,
410 append(Infos,Old,New).
411 add_texpr_infos(Other,Infos,Res) :-
412 add_internal_error('Illegal call, not BExpr:',add_texpr_infos(Other,Infos,Res)),fail.
413
414 add_texpr_info_if_new(b(Expr,Type,Old),Info,b(Expr,Type,New)) :- !,
415 add_info_if_new(Old,Info,New).
416 add_texpr_info_if_new(Other,Infos,Res) :-
417 add_internal_error('Illegal call, not BExpr:',add_texpr_info_if_new(Other,Infos,Res)),fail.
418 % add multiple infos:
419 add_texpr_infos_if_new(b(Expr,Type,Old),Infos,b(Expr,Type,New)) :-
420 add_infos_if_new(Infos,Old,New).
421
422 % add to info list:
423 add_info_if_new(Old,Info,New) :-
424 ? (member(Info,Old) -> New=Old ; New = [Info|Old]).
425
426 add_infos_if_new([]) --> [].
427 add_infos_if_new([Info|T]) --> add_info(Info), add_infos_if_new(T).
428 add_info(Info,Old,New) :-
429 ? (member(Info,Old) -> New=Old ; New = [Info|Old]).
430
431
432 % try and extract the Rodin name of a predicate or expression
433 get_rodin_name(Expression,LabelName) :-
434 get_texpr_pos(Expression,Pos),
435 (Pos = rodinpos(LabelName,_) -> LabelName \= []
436 ; Pos = rodinpos(_Model,LabelName,_) -> LabelName \= [] % new rodinpos
437 ; Pos = rodin_derived_context_pos(_Model,_ContextTerm,Label) % ContextTerm can be e.g. event(isqrt,guard)
438 -> atom_concat(Label,' (part)',LabelName) % happens when a guard/predicate is split by ProB
439 ).
440
441 get_precise_rodin_name(Expression,LabelName) :-
442 get_texpr_pos(Expression,Pos),
443 (Pos = rodinpos(LabelName,_) -> LabelName \= []
444 ; Pos = rodinpos(_Model,LabelName,_) -> LabelName \= [] % new rodinpos
445 ).
446
447 get_rodin_model_name(Expression,Model) :-
448 get_texpr_pos(Expression,rodinpos(Model,Name,_)), Name \= []. % new rodinpos
449 % Note: only precise position label, not rodin_derived_context_pos
450
451 % try and extract the Rodin name or label pragma of a predicate or expression
452 get_texpr_labels(TExpr,LabelList) :-
453 get_texpr_info(TExpr,Infos),
454 ? member(I,Infos), info_label_list(I,LabelList).
455 get_info_labels(Infos,LabelList) :-
456 ? member(I,Infos), info_label_list(I,LabelList).
457 select_info_labels(LabelList,Infos,Rest) :-
458 ? select(I,Infos,Rest), info_label_list(I,LabelList).
459 info_label_list(nodeid(NodeID),[Name]) :- nodeid_info_label(NodeID,Name).
460 info_label_list(label(LabelList),LabelList).
461
462 nodeid_info_label(rodinpos(Name,_),Name) :- Name \= [].
463 nodeid_info_label(rodinpos(Model,Name,_),FullName) :- Name \= [], % new rodinpos
464 ajoin([Model,':',Name], FullName). % TO DO: if only one level; don't do this
465 % TODO: provide separate way to access this derived information:
466 %nodeid_info_label(rodin_derived_context_pos(Model,Context,Label),FullName) :-
467 % ajoin([Model,'.',Context,':',Label], FullName).
468
469
470 add_labels_to_texpr(E,[],R) :- !, R=E. % no labels to add
471 add_labels_to_texpr(b(E,T,I),Labels,b(E,T,NewI)) :-
472 (select(label(OldList),I,Rest)
473 -> append(Labels,OldList,NewList), NewI=[label(NewList)|Rest]
474 % TO DO: what if we have Rodin labels
475 ; NewI = [label(Labels)|I]
476 ).
477
478 ?get_texpr_label(TExpr,Label) :- get_texpr_labels(TExpr,Labels), member(Label,Labels).
479
480 get_texpr_description(TExpr,Description) :-
481 get_texpr_info(TExpr,Infos),
482 memberchk(description(Description),Infos).
483
484 add_texpr_description(b(E,T,I),Description,b(E,T,[description(Description)|I])) :-
485 (atom(Description) -> true ;
486 add_error(add_texpr_description,'Non-atomic description:',Description)).
487
488 % check if an info list has an ignore pragma
489 info_has_ignore_pragma(Infos) :-
490 ? member(description('prob-ignore'),Infos).
491 % detect_prob_ignore ast_cleanup rule also generates this description annotation
492 % if use_ignore_pragmas is true and label starts with prob-ignore
493
494 predicate_has_ignore_pragma(b(_E,pred,I)) :-
495 %add_message(check_prob_ignore,'Pred: ',b(_E,pred,I),I),
496 ? info_has_ignore_pragma(I).
497
498 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
499
500 :- assert_must_succeed( (E = "1/2",
501 bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err),
502 Type==integer, Err==none, always_well_defined(ET) ) ).
503 :- assert_must_succeed( (E = "3 mod 2",
504 bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err),
505 Type==integer, Err==none, always_well_defined(ET) ) ).
506 :- assert_must_succeed( (E = "1/0",
507 bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err),
508 Type==integer, Err==none, \+ always_well_defined(ET) ) ).
509 :- assert_must_succeed( (E = "2*(3 mod card({}))",
510 bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err),
511 Type==integer, Err==none, \+ always_well_defined(ET) ) ).
512 :- assert_must_succeed( (E = "1/(2+1-3)",
513 bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err),
514 Type==integer, Err==none, \+ always_well_defined(ET) ) ).
515 :- assert_must_succeed( (E = "max({1,2,3,0})",
516 bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err),
517 Type==integer, Err==none, always_well_defined(ET) ) ).
518 :- assert_must_succeed( (E = "min({1,2,3,0})",
519 bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err),
520 Type==integer, Err==none, always_well_defined(ET) ) ).
521 :- assert_must_succeed( (E = "min({1,2,3,0}-(0..4))",
522 bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err),
523 Type==integer, Err==none, \+ always_well_defined(ET) ) ).
524 :- assert_must_succeed( (E = "2+max({1,2,3, 1/0})",
525 bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err),
526 Type==integer, Err==none,\+ always_well_defined(ET) ) ).
527 :- assert_must_succeed( (E = "2-card({1,2,3})",
528 bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err),
529 Type==integer, Err==none, always_well_defined(ET) ) ).
530 :- assert_must_succeed( (E = "2-card({1,2,3, 1/0})",
531 bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err),
532 Type==integer, Err==none,\+ always_well_defined(ET) ) ).
533 :- assert_must_succeed( (E = "bool(2-size([1,2,3, 1/0])=3)",
534 bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err),
535 Type==boolean, Err==none, \+ always_well_defined(ET) ) ).
536 :- assert_must_succeed( (E = "bool(2-size([1,2,3, 1/2, 3 mod 2, 3**2])=size([]))",
537 bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err),
538 Type==boolean, Err==none, always_well_defined(ET) ) ).
539
540 always_well_defined_or_wd_reorderings_allowed(BE) :- % allow re-ordering to improve Left-to-right WD
541 (preferences:preference(disprover_mode,true) -> true % we can assume all calls are well-defined
542 ; preferences:preference(allow_improving_wd_mode,true) -> true
543 ; preferences:preference(data_validation_mode,true) -> true
544 ; always_well_defined_or_discharged(BE)).
545 always_well_defined_or_wd_improvements_allowed(BE) :- % allow to remove useless calls which could be non-WD
546 % example #x(x = f(...)) -> btrue or f[{}] --> {}
547 always_well_defined_or_wd_reorderings_allowed(BE). % we currently use the same definition
548 always_well_defined_or_disprover_mode(BE) :-
549 (preferences:preference(disprover_mode,true) -> true % we can assume all calls are well-defined
550 ; always_well_defined_or_discharged(BE)).
551
552 always_well_defined_or_discharged(b(E,_,Infos)) :- !,
553 (nonmember(contains_wd_condition,Infos) -> true
554 ; always_wd(E) -> true % some special rules
555 ? ; member(discharged_wd_po,Infos) -> true
556 %; nl, functor(E,F,N), F \= function, print(non_wd(F,N)),nl,nl,fail
557 ).
558 always_well_defined_or_discharged(E) :-
559 add_error_fail(always_well_defined,'Illegal call: ',always_well_defined_or_discharged(E)).
560
561 % should ensure that there is no failure and no error raised
562 always_well_defined(b(E,_,Infos)) :- !,
563 (nonmember(contains_wd_condition,Infos) -> true
564 ; always_wd(E) -> true % some special rules
565 %; nl, functor(E,F,N), F \= function, print(non_wd(F,N)),nl,nl,fail
566 ).
567 always_well_defined(E) :- add_error_fail(always_well_defined,'Illegal call: ',always_well_defined(E)).
568
569
570 :- assert_must_succeed( always_wd(div( b(integer(2),integer,[]), b(integer(2),integer,[]) )) ).
571 :- assert_must_fail( always_wd(div( b(integer(2),integer,[]), b(integer(0),integer,[]) )) ).
572 :- assert_must_succeed( always_wd(modulo( b(integer(2),integer,[]), b(integer(2),integer,[]) )) ).
573 :- assert_must_fail( always_wd(modulo( b(integer(2),integer,[]), b(integer(0),integer,[]) )) ).
574 :- assert_must_fail( always_wd(modulo( b(integer(2),integer,[]), b(integer(-2),integer,[]) )) ).
575 :- assert_must_fail( always_wd(modulo( b(integer(-1),integer,[]), b(integer(2),integer,[]) )) ).
576 :- assert_must_succeed( always_wd(power_of( b(integer(2),integer,[]), b(integer(3),integer,[]) )) ).
577 :- assert_must_succeed( always_wd(power_of( b(integer(2),integer,[]), b(integer(0),integer,[]) )) ).
578 :- assert_must_fail( always_wd(power_of( b(integer(2),integer,[]), b(integer(-1),integer,[]) )) ).
579
580 % catch cases where the construct is currently so instantiated that we can determine that it is well-defined
581 % can happen e.g. during closure compilation
582 :- use_module(custom_explicit_sets,[check_unique_in_domain_of_avlset/2]).
583 :- use_module(kernel_tools,[ground_value/1]).
584 always_wd(power_of(X,Y)) :- get_integer(Y,Val), Val>=0,
585 (eventb_mode -> get_integer(X,ValX), ValX >=0
586 ; always_well_defined(X)).
587 always_wd(div(X,Y)) :- get_integer(Y,Val), Val\=0, always_well_defined(X).
588 always_wd(modulo(X,Y)) :- get_integer(Y,Val), Val>0, % Z Live allows negative numbers here it seems, cf modulo2
589 (z_or_tla_minor_mode -> true % in Z, TLA we can have negative numbers here
590 ; get_integer(X,ValX), ValX>=0).
591 always_wd(function(X,Y)) :- nonvar(X),
592 X= b(value(AVLSET),_,_), nonvar(AVLSET), AVLSET=avl_set(AVL),
593 always_wd_avl_function(AVL,Y).
594 always_wd(min(X)) :- non_empty_finite_wd_set_value(X).
595 always_wd(max(X)) :- non_empty_finite_wd_set_value(X).
596 always_wd(card(X)) :- finite_wd_set_value(X).
597 always_wd(size(X)) :- finite_wd_seq_value(X).
598 always_wd(first(X)) :- non_empty_wd_seq_value(X).
599 always_wd(front(X)) :- non_empty_wd_seq_value(X).
600 always_wd(last(X)) :- non_empty_wd_seq_value(X).
601 always_wd(tail(X)) :- non_empty_wd_seq_value(X). % TO DO: add restrict_front, restrict_tail ?
602 always_wd(rev(X)) :- finite_wd_seq_value(X).
603 always_wd(concat(X,Y)) :- finite_wd_seq_value(X), finite_wd_seq_value(Y).
604 always_wd(insert_front(_,Y)) :- finite_wd_seq_value(Y).
605 always_wd(insert_tail(X,_)) :- finite_wd_seq_value(X).
606
607 always_wd(general_intersection(X)) :- non_empty_finite_wd_set_value(X).
608 always_wd(value(_)). % we have already computed the value and will raise WD error; to be 100 % safe we could restrict this to ground values
609 % other candidates: size(_), first(_) last(_) tail(_) front(_) restrict_front(_,_) restrict_tail(_,_) rel_iterate(_,_)
610 always_wd(typeset).
611 % operators that are always wd on their own:
612 always_wd(record_field(RecEx,FieldName)) :- ground(FieldName),
613 always_well_defined(RecEx).
614 always_wd(unary_minus(A)) :- always_well_defined(A).
615 always_wd(unary_minus_real(A)) :- always_well_defined(A).
616 always_wd(first_of_pair(A)) :- always_well_defined(A).
617 always_wd(add(A,B)) :- always_well_defined(A),always_well_defined(B).
618 always_wd(add_real(A,B)) :- always_well_defined(A),always_well_defined(B).
619 always_wd(minus(A,B)) :- always_well_defined(A),always_well_defined(B).
620 always_wd(minus_real(A,B)) :- always_well_defined(A),always_well_defined(B).
621 always_wd(multiplication(A,B)) :- always_well_defined(A),always_well_defined(B).
622 always_wd(multiplication_real(A,B)) :- always_well_defined(A),always_well_defined(B).
623 always_wd(equal(A,B)) :- always_well_defined(A),always_well_defined(B).
624 always_wd(not_equal(A,B)) :- always_well_defined(A),always_well_defined(B).
625 always_wd(less_equal(A,B)) :- always_well_defined(A),always_well_defined(B).
626 always_wd(less_equal_real(A,B)) :- always_well_defined(A),always_well_defined(B).
627 always_wd(greater_equal(A,B)) :- always_well_defined(A),always_well_defined(B).
628 always_wd(less(A,B)) :- always_well_defined(A),always_well_defined(B).
629 always_wd(less_real(A,B)) :- always_well_defined(A),always_well_defined(B).
630 always_wd(greater(A,B)) :- always_well_defined(A),always_well_defined(B).
631 always_wd(couple(A,B)) :- always_well_defined(A),always_well_defined(B).
632 % TO DO: add more/all other operators ?
633
634 always_wd_avl_function(AVL,Y) :- nonvar(Y), Y= b(value(Val),_,_),
635 ground_value(Val), !,
636 % Warning: this does not check that the whole AVL is a function; just this particular lookup is ok
637 check_unique_in_domain_of_avlset(Val,AVL). % ,print(ok),nl.
638 always_wd_avl_function(AVL,Y) :- always_well_defined(Y),
639 custom_explicit_sets:quick_definitely_maximal_total_function_avl(AVL).
640
641 % non empty set with WD elements
642 non_empty_finite_wd_set_value(b(E,_,_)) :- non_empty_fin_wd_set2(E).
643 non_empty_fin_wd_set2(bool_set).
644 non_empty_fin_wd_set2(value(X)) :- definitely_not_empty_finite_value(X).
645 non_empty_fin_wd_set2(set_extension(S)) :- l_always_well_defined(S). % the set_extension could contain wd_errors !!
646 non_empty_fin_wd_set2(sequence_extension(S)) :- l_always_well_defined(S). % ditto
647 non_empty_fin_wd_set2(interval(A,B)) :- get_integer(A,IA), get_integer(B,IB), IA =< IB.
648 % see not_empty_set_aux
649 definitely_not_empty_finite_value(X) :- var(X),!,fail.
650 definitely_not_empty_finite_value(avl_set(_)).
651 definitely_not_empty_finite_value([_|_]).
652 definitely_not_empty_finite_value(closure(P,T,B)) :-
653 custom_explicit_sets:is_interval_closure(P,T,B,LOW,UP), integer(LOW),integer(UP), LOW =< UP.
654 % TODO: pow_subset of finite values
655
656 non_empty_wd_seq_value(b(E,_,_)) :- non_empty_seq2(E).
657 non_empty_seq2(value(X)) :- definitely_not_empty_seq(X).
658 non_empty_seq2(sequence_extension(S)) :- l_always_well_defined(S), S=[_|_].
659
660 definitely_not_empty_seq(X) :- var(X),!,fail.
661 definitely_not_empty_seq(avl_set(A)) :- custom_explicit_sets:is_avl_sequence(A).
662 definitely_not_empty_seq([El1|T]) :- T==[],nonvar(El1), El1=(IDX,_), IDX==int(1). % TO DO: add more cases ?
663
664
665 finite_set_or_disprover_mode(Set) :-
666 (preferences:preference(disprover_mode,true) -> true % we can assume all calls are well-defined
667 ; finite_wd_set_value(Set)).
668
669 :- use_module(typing_tools,[is_provably_finite_type/1]).
670 % we could also use is_finite_type_in_context to allow deferred sets to be counted as finite
671 finite_wd_set_value(b(E,T,_)) :- !, (finite_set2(E) -> true ; is_provably_finite_type(T)).
672 finite_wd_set_value(E) :- add_internal_error('Not a BExpr: ',E),fail.
673 finite_set2(empty_set).
674 finite_set2(empty_sequence).
675 finite_set2(value(X)) :- X==[] -> true ; definitely_not_empty_finite_value(X).
676 finite_set2(set_extension(S)) :- l_always_well_defined(S). % the set_extension could contain wd_errors !!
677 finite_set2(sequence_extension(S)) :- l_always_well_defined(S). % ditto
678
679 finite_wd_seq_value(b(E,_,_)) :- finite_seq2(E).
680 finite_seq2(empty_set).
681 finite_seq2(empty_sequence).
682 finite_seq2(value(X)) :- finite_seq_value(X).
683 finite_seq2(sequence_extension(S)) :- l_always_well_defined(S).
684
685 finite_seq_value(X) :- var(X),!,fail.
686 finite_seq_value([]).
687 finite_seq_value(avl_set(A)) :- custom_explicit_sets:is_avl_sequence(A).
688 % it could be expensive to check if non empty list is a B sequence ??
689
690 l_always_well_defined([]).
691 l_always_well_defined([H|T]) :- always_well_defined(H), l_always_well_defined(T).
692
693 ?is_truth(b(F,pred,_)) :- is_truth_aux(F).
694 is_truth_aux(truth).
695 is_truth_aux(value(V)) :- V==pred_true. % can occur in CSE mode
696
697 is_falsity(b(F,pred,_)) :- is_falsity_aux(F).
698 is_falsity_aux(falsity).
699 is_falsity_aux(value(V)) :- V==pred_false. % can occur in CSE mode
700
701 % conjunction of a list of predicates
702 % NOTE: bsyntaxtree:conjunct_predicates([P1,P2,P3],R). --> generates R = b(conjunct(b(conjunct(P1,P2),pred,[]),P3),pred,[])
703 conjunct_predicates(V,R) :- var(V),!, add_internal_error('Variable conjunction list: ',conjunct_predicates(V,R)),fail.
704 conjunct_predicates([],b(truth,pred,[])).
705 conjunct_predicates([P|Rest],Result) :- conjunct2(Rest,P,Result).
706 conjunct2([],P,P).
707 conjunct2([Q|Rest],P,Result) :- conjunct3(P,Q,R), conjunct2(Rest,R,Result).
708 conjunct3(b(truth,_,_),P,P) :- !.
709 conjunct3(P,b(truth,_,_),P) :- !.
710 conjunct3(A,B,b(conjunct(A,B),pred,NewInfo)) :- extract_info(A,B,NewInfo).
711
712 % disjunction of a list of predicates
713 disjunct_predicates([],b(falsity,pred,[])).
714 disjunct_predicates([P|Rest],Result) :- disjunct2(Rest,P,Result).
715 disjunct2([],P,P).
716 disjunct2([Q|Rest],P,Result) :- disjunct3(P,Q,R), disjunct2(Rest,R,Result).
717 disjunct3(b(falsity,_,_),P,R) :- !, R=P.
718 disjunct3(b(truth,T,I),_,R) :- !, R=b(truth,T,I).
719 disjunct3(P,b(falsity,_,_),R) :- !, R=P.
720 disjunct3(_,b(truth,T,I),R) :- !, R=b(truth,T,I).
721 disjunct3(A,B,b(disjunct(A,B),pred,NewInfo)) :- extract_info(A,B,NewInfo).
722
723 % conjunct two predicates and try and construct position information
724 conjunct_predicates_with_pos_info(A,B,AB) :- is_truth(B),!, AB=A.
725 conjunct_predicates_with_pos_info(A,B,AB) :- is_truth(A),!, AB=B.
726 conjunct_predicates_with_pos_info(A,B,AB) :-
727 conjunct_predicates([A,B],AB0), % this may contain position info if B is truth; hence we do check above
728 (try_get_merged_position_info(A,B,ABI)
729 -> add_texpr_infos(AB0,[ABI],AB) %,print(abi(ABI)),nl
730 ; AB=AB0).
731
732 % disjunct two predicates and try and construct position information
733 disjunct_predicates_with_pos_info(A,B,AB) :-
734 disjunct_predicates([A,B],AB0),
735 (try_get_merged_position_info(A,B,ABI)
736 -> add_texpr_infos(AB0,[ABI],AB) %,print(abi(ABI)),nl
737 ; AB=AB0).
738
739 try_get_merged_position_info(b(_,_,I1),b(_,_,I2),PosInfo) :-
740 (try_get_merged_position_info_aux(I1,I2,MergedInfo) -> PosInfo = MergedInfo
741 ? ; get_non_label_posinfo(Pos1,I1) -> PosInfo=nodeid(Pos1)
742 ? ; get_non_label_posinfo(Pos2,I2) -> PosInfo=nodeid(Pos2)
743 ).
744 try_get_merged_position_info_aux(I1,I2,nodeid(pos(C,Filenumber,Srow,Scol,Erow,Ecol))) :-
745 ? member(nodeid(pos(C1,Filenumber,Srow1,Scol1,Erow1,Ecol1)),I1),
746 (number(C1),number(Srow1),number(Scol1),number(Erow1),number(Ecol1)
747 -> true ; add_internal_error('Info field 1 not yet instantiated: ',try_get_merged_position_info(I1)),fail),
748 !,
749 ? member(nodeid(pos(C2,Filenumber,Srow2,Scol2,Erow2,Ecol2)),I2),
750 (number(C2),number(Srow2),number(Scol2),number(Erow2),number(Ecol2)
751 -> true ; add_internal_error('Info field 2 not yet instantiated: ',try_get_merged_position_info(I2)),fail),
752 !,
753 % merge position info if in same file
754 (C1 =< C2 -> C=C1, Srow=Srow1,Scol=Scol1 ; C=C2, Srow=Srow2,Scol=Scol2),
755 ((Erow1 > Erow2 ; Erow1=Erow2, Ecol1 >= Ecol2)
756 -> Erow =Erow1, Ecol=Ecol1
757 ; Erow =Erow2, Ecol=Ecol2).
758
759 % get position info which is not a label; label info should not be propagated to outer conjuncts/disjuncts/...
760 ?get_non_label_posinfo(Pos,Infos) :- member(nodeid(Pos),Infos),
761 \+ functor(Pos,rodinpos,_).
762
763 ?get_texpr_non_label_posinfo(b(_,_,Infos),nodeid(Pos)) :- get_non_label_posinfo(Pos,Infos).
764
765 % conjunct list of predicates and try and construct position information
766 conjunct_predicates_with_pos_info([H|T],Res) :- is_truth(H),!,
767 (T=[] -> Res = H ; conjunct_predicates_with_pos_info(T,Res)).
768 conjunct_predicates_with_pos_info([H|T],Res) :-
769 last_non_truth(T,none,Last), % the truth elements will be removed and are not relevant; get last relevant predicate
770 Last \= none,
771 try_get_merged_position_info(H,Last,MergedPosInfo), % try and merge position of first and last element
772 !,
773 conjunct_predicates([H|T],Res0),
774 add_texpr_infos(Res0,[MergedPosInfo],Res). % Res0 should have no nodeid field
775 conjunct_predicates_with_pos_info(L,Res) :- conjunct_predicates(L,Res).
776
777 :- assert_must_succeed((bsyntaxtree:last_non_truth([a,b,c],none,L),L==c)).
778 :- assert_must_succeed((bsyntaxtree:last_non_truth([a,b,c,b(truth,pred,[])],none,L),L==c)).
779
780 % get last non-truth element and filter out all truth elements
781 last_non_truth([],Acc,Acc).
782 last_non_truth([H|T],NonTruth,Last) :- is_truth(H),!, last_non_truth(T,NonTruth,Last).
783 last_non_truth([H|T],_,Last) :- last_non_truth(T,H,Last).
784
785
786 texpr_contains_wd_condition(b(_,_,Info)) :- !, memberchk(contains_wd_condition,Info).
787 texpr_contains_wd_condition(E) :- add_internal_error('Not a texpr: ',texpr_contains_wd_condition(E)).
788
789 % a version of create_texpr which collects automatically important infos from sub-expressions
790 safe_create_texpr(Expr,Type,b(Expr,Type,Info)) :- %
791 ? (sub_expression_contains_wd_condition(Expr) -> Info = [contains_wd_condition] ; Info=[]).
792
793 safe_create_texpr(Expr,Type,Info,b(Expr,Type,FullInfo)) :- %
794 ? ((sub_expression_contains_wd_condition(Expr), nonmember(contains_wd_condition, Info)) -> FullInfo = [contains_wd_condition|Info] ; FullInfo=Info).
795
796 ?sub_expression_contains_wd_condition(Expr) :- sub_expression_contains_wd_condition(Expr,_).
797 sub_expression_contains_wd_condition(Expr,Sub) :-
798 safe_syntaxelement_det(Expr,Subs,_Names,_L,_C),
799 ? member(b(Sub,_,Infos),Subs),
800 (var(Infos)
801 -> add_internal_error('Typed expression not sufficiently instantiated (variable Infos): ',sub_expression_contains_wd_condition(Expr)),
802 fail
803 ; memberchk(contains_wd_condition,Infos)).
804
805 % provide updated infos (e.g., reads(...)) and remove any old info fields with same functor
806 update_infos([],Infos,Infos).
807 update_infos([Update|T],OldInfos,NewInfos) :-
808 functor(Update,F,N),
809 functor(Old,F,N),
810 delete(OldInfos,Old,OldInfos1),
811 update_infos(T,[Update|OldInfos1],NewInfos).
812
813 % merge two info lists and try to reconcile position information:
814 merge_info(Info1,Info2,Res) :-
815 merge_imp_info2(Info2,Info1,NewInfo),
816 (try_get_merged_position_info_aux(Info1,Info2,NewPos)
817 -> delete_pos_info(NewInfo,NI2),
818 Res = [NewPos|NI2]
819 ; Res = NewInfo).
820
821 % extract important info but without used_ids:
822 extract_info_wo_used_ids(b(_,_,Info1),Info) :-
823 extract_pos_infos(Info1,PosInfos),
824 extract_just_important_info_aux(Info1,[],I1),
825 append(PosInfos,I1,Info).
826 extract_info_wo_used_ids_and_pos(b(_,_,Info1),b(_,_,Info2),Info) :-
827 extract_just_important_info_aux(Info1,[],I1),
828 extract_just_important_info_aux(Info2,I1,Info).
829
830 % extract important info from one sub-expression:
831 extract_info(b(_,_,Info1),NewInfo) :-
832 extract_imp_info1(Info1,I1),!, NewInfo = I1.
833 extract_info(A,R) :-
834 add_internal_error('Could not extract info: ',extract_info(A,R)),
835 R=[].
836 % extract imortant info fields from two (sub-)expressions
837 extract_info(b(_,_,Info1),b(_,_,Info2),NewInfo) :-
838 ? merge_imp_info2(Info1,Info2,II),!, NewInfo = II.
839 %:- use_module(library(ordsets),[ord_intersection/3]).
840 % ord_intersection(Info1,Info2,NewInfo),!.
841 % TO DO: should we merge nodeid position information !?
842 extract_info(A,B,R) :- add_internal_error('Could not extract info: ',extract_info(A,B,R)),
843 R=[].
844
845 % extract important info and used_ids
846 extract_imp_info1([],[]).
847 extract_imp_info1([H|T],Res) :-
848 ((important_info(H); H=used_ids(_)) -> Res=[H|ET], extract_imp_info1(T,ET)
849 ; extract_imp_info1(T,Res)
850 ).
851
852 % extract and merge important info and try to merge used_ids from two info lists
853 merge_imp_info2(Info1,Info2,ResInfos) :-
854 extract_imp_info1(Info1,I1),
855 ? extract_imp_info1(Info2,I2),
856 merge_aux(I1,I2,ResInfos).
857
858 merge_aux([],I2,Res) :- !, delete(I2,used_ids(_),Res). % used_ids not valid for new construct
859 merge_aux(I1,[],Res) :- !, delete(I1,used_ids(_),Res). % ditto
860 merge_aux(I1,I2,ResInfos) :-
861 ? (select(used_ids(Ids1),I1,II1)
862 ? -> (select(used_ids(Ids2),I2,II2)
863 -> ord_union(Ids1,Ids2,Ids3),
864 append(II1,[used_ids(Ids3)|II2],II)
865 ; append(II1,I2,II)
866 )
867 ; delete(I2,used_ids(_),II2),
868 append(I1,II2,II)
869 ),
870 sort(II,ResInfos). % TO DO: sort sublists ? and use ord_union?
871
872 important_info(contains_wd_condition).
873 important_info(prob_annotation(_)).
874 important_info(allow_to_lift_exists).
875 important_info(removed_typing).
876 %important_info(lambda_result(_)). % should probably not be copied
877
878 % variation of above which does not extract and merge used_ids:
879 extract_just_important_info_aux([],Acc,Acc).
880 extract_just_important_info_aux([H|T],Acc,Res) :-
881 ? (important_info(H), \+ member(H,Acc) -> extract_just_important_info_aux(T,[H|Acc],Res)
882 ; extract_just_important_info_aux(T,Acc,Res)).
883
884
885 is_a_conjunct(b(conjunct(A,B),pred,_),A,B).
886 % use is_a_conjunct_without_label if you want to avoid decomposing conjunction associated with a single label
887 is_a_conjunct_without_label(b(conjunct(A,B),pred,I),A,B) :- \+ get_info_labels(I,_).
888 % use decompose conjunct if you want to propagate labels down to the conjuncts
889 decompose_conjunct(b(conjunct(A,B),pred,I),ResA,ResB) :-
890 ? (get_info_labels(I,Labels)
891 -> add_labels_to_texpr(A,Labels,ResA), add_labels_to_texpr(B,Labels,ResB)
892 ; ResA=A, ResB=B).
893
894 size_of_conjunction(C,Size) :- size_of_conjunction(C,0,Size).
895 size_of_conjunction(C,Acc,Res) :- is_a_conjunct(C,A,B),!,
896 size_of_conjunction(B,Acc,A1),
897 size_of_conjunction(A,A1,Res).
898 size_of_conjunction(_,Acc,Size) :- Size is Acc+1.
899
900 conjunction_to_list(C,L) :- var(C),!,
901 add_error_fail(conjunction_to_list,'Internal error: var :',conjunction_to_list(C,L)).
902 conjunction_to_list(C,List) :-
903 conjunction_to_list2(C,List,[]).
904 conjunction_to_list2(X,I,O) :- X=b(E,_,_),
905 (E=conjunct(LHS,RHS) -> conjunction_to_list2(LHS,I,Inter),
906 conjunction_to_list2(RHS,Inter,O)
907 ; E = truth -> I=O
908 ; I = [X|O]).
909
910 % a variation of conjunction_to_list which propagates Rodin and pragma label infos down
911 % important for proof info; maybe we should only propagate Rodin labels ?
912 conjunction_to_list_with_rodin_labels(C,L) :- var(C),!,
913 add_error_fail(conjunction_to_list,'Internal error: var :',conjunction_to_list_with_rodin_labels(C,L)).
914 conjunction_to_list_with_rodin_labels(C,List) :-
915 conjunction_to_list_with_labels2(C,List,[]).
916 conjunction_to_list_with_labels2(b(conjunct(A,B),pred,Infos),I,O) :- !,
917 copy_rodin_label(Infos,A,B,LHS,RHS),
918 conjunction_to_list_with_labels2(LHS,I,Inter),
919 conjunction_to_list_with_labels2(RHS,Inter,O).
920 conjunction_to_list_with_labels2(X,I,O) :- X=b(E,_,_),
921 ( E = truth -> I=O
922 ; I = [X|O]).
923
924
925 ?copy_rodin_label(Infos,A,B,NewA,NewB) :- member(Pos,Infos), is_rodin_label_info(Pos),!,
926 add_rodin_label_info(A,Pos,NewA),
927 add_rodin_label_info(B,Pos,NewB).
928 copy_rodin_label(_,A,B,A,B).
929
930 add_rodin_label_info(b(E,T,I),Pos,b(E,T,I2)) :-
931 (member(Pos,I), is_rodin_label_info(Pos) -> I2=I
932 ; I2 = [Pos|I]).
933
934 is_rodin_label_info(nodeid(Pos)) :- functor(Pos,rodinpos,_).
935
936
937 flatten_conjunctions(List,FlattenedList) :- flatten_conj_aux(List,FlattenedList,[]).
938 flatten_conj_aux([]) --> !, [].
939 flatten_conj_aux([H|T]) --> !, flatten_conj_aux(H),flatten_conj_aux(T).
940 flatten_conj_aux(C) --> {is_a_conjunct(C,LHS,RHS)},
941 !,
942 flatten_conj_aux(LHS), flatten_conj_aux(RHS).
943 flatten_conj_aux(Truth) --> {is_truth(Truth)},!,[].
944 flatten_conj_aux(C) --> [C].
945
946 member_in_conjunction(M,Conj) :- is_a_conjunct(Conj,LHS,RHS),!,
947 ? (member_in_conjunction(M,LHS) ; member_in_conjunction(M,RHS)).
948 member_in_conjunction(M,M).
949
950 % a version of member_in_conjunction which can deal with lazy_let_pred :
951 % member_in_conjunction_cse(FullConjunctWithLets,InnerConjunctNotALet, Conjunction)
952 member_in_conjunction_cse(M,InnerConj,Conj) :- is_a_conjunct(Conj,LHS,RHS),!,
953 (member_in_conjunction_cse(M,InnerConj,LHS) ; member_in_conjunction_cse(M,InnerConj,RHS)).
954 member_in_conjunction_cse(Conj,InnerConj,b(lazy_let_pred(ID,Share,Body),pred,Info)) :-
955 Conj = b(lazy_let_pred(ID,Share,BConj),pred,Info),!,
956 member_in_conjunction_cse(BConj,InnerConj,Body).
957 member_in_conjunction_cse(M,M,M).
958
959 % not terribly efficient way to select and remove a conjunct from a predicate
960 select_member_in_conjunction(M,Conj,Rest) :- is_a_conjunct(Conj,LHS,RHS),!,
961 ? (select_member_in_conjunction(M,LHS,RL), conjunct_predicates([RL,RHS],Rest)
962 ; select_member_in_conjunction(M,RHS,RR), conjunct_predicates([LHS,RR],Rest)).
963 select_member_in_conjunction(M,M,b(truth,pred,[])).
964
965 is_a_disjunct(b(disjunct(A,B),pred,_),A,B).
966 is_a_negation(b(negation(A),pred,_),A).
967
968 disjunction_to_list(C,L) :- var(C),!,
969 add_error_fail(disjunction_to_list,'Internal error: var :',disjunction_to_list(C,L)).
970 disjunction_to_list(C,List) :-
971 disjunction_to_list2(C,List,[]).
972 disjunction_to_list2(C,I,O) :- is_a_disjunct(C,LHS,RHS),!,
973 disjunction_to_list2(LHS,I,Inter),
974 disjunction_to_list2(RHS,Inter,O).
975 disjunction_to_list2(X,[X|R],R).
976
977 is_an_implication(b(implication(A,B),pred,_),A,B).
978
979 is_an_equivalence(b(equivalence(A,B),pred,_),A,B).
980
981
982 is_a_disjunct_or_implication(b(DI,pred,_),Type,A,B) :- is_a_disj_or_impl_aux(DI,Type,A,B).
983 is_a_disj_or_impl_aux(disjunct(A,B),'disjunction',A,B).
984 is_a_disj_or_impl_aux(implication(A,B),'implication',NA,B) :-
985 create_negation(A,NA).
986 is_a_disj_or_impl_aux(negation(b(conjunct(A,B),pred,_)),'negated conjunction',NA,NB) :-
987 create_negation(A,NA),create_negation(B,NB).
988
989 % a more liberal version of is_a_conjunct/2 which also detects negated disjunctions/implications
990 is_a_conjunct_or_neg_disj(b(DI,pred,I),A,B) :- is_conjunct_aux(DI,I,A,B).
991
992 is_conjunct_aux(conjunct(LHS,RHS),_,LHS,RHS).
993 is_conjunct_aux(negation(DISJ),_,NegLHS,NegRHS) :-
994 is_a_disjunct_or_implication(DISJ,_Type,LHS,RHS),
995 create_negation(LHS,NegLHS),
996 create_negation(RHS,NegRHS).
997 is_conjunct_aux(equal(TA,TB),I,b(equal(TA1,TB1),pred,I),b(equal(TA2,TB2),pred,I)) :-
998 % split TA1|->TA2 = TB1|->TB2, cf, split_equality/3; useful for enumeration order analysis
999 get_texpr_couple(TA,TA1,TA2),
1000 get_texpr_couple(TB,TB1,TB2).
1001 % print('Splitting equality in is_a_conjunct_or_neg_disj: '), translate:print_bexpr(b(equal(TA,TB),pred,I)),nl.
1002
1003 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1004 % remove all info fields by fresh variables
1005 % typically the result will be unified with AST terms which contain full info fields
1006 remove_all_infos(TExpr,TNExpr) :-
1007 var(TExpr),!,TExpr=TNExpr.
1008 % in contrast to remove_all_infos_and_ground we provide no special treatment of values with closures here;
1009 % there could be a problem if we unify with a free variable as value
1010 remove_all_infos(TExpr,TNExpr) :-
1011 get_texpr_expr(TExpr,Expr),
1012 get_texpr_type(TExpr,Type),
1013 ? syntaxtransformation(Expr,Subs,_,NSubs,NExpr),
1014 create_texpr(NExpr,Type,_,TNExpr),
1015 ? maplist(remove_all_infos,Subs,NSubs).
1016
1017 % replace all info fields
1018 remove_all_infos_and_ground(TExpr,TNExpr) :-
1019 var(TExpr),!,TExpr=TNExpr.
1020 remove_all_infos_and_ground(b(value(Value),Type,_),TNExpr) :-
1021 % special case for closure(_,_,_) since it is not covered by syntraxtransformation/5
1022 % most useful for intervals
1023 !,
1024 remove_all_infos_from_bvalue(Value,NValue),
1025 TNExpr = b(value(NValue),Type,[]).
1026 remove_all_infos_and_ground(TExpr,TNExpr) :-
1027 get_texpr_expr(TExpr,Expr),
1028 get_texpr_type(TExpr,Type),
1029 syntaxtransformation(Expr,Subs,_,NSubs,NExpr),
1030 create_texpr(NExpr,Type,[],TNExpr),
1031 maplist(remove_all_infos_and_ground,Subs,NSubs).
1032
1033 remove_all_infos_from_bvalue(Var,Res) :- var(Var),!, Res=Var.
1034 remove_all_infos_from_bvalue((A,B),(RA,RB)) :- !,
1035 remove_all_infos_from_bvalue(A,RA),
1036 remove_all_infos_from_bvalue(B,RB).
1037 remove_all_infos_from_bvalue(closure(P,T,Body),Res) :- !,
1038 remove_all_infos_and_ground(Body,RBody),
1039 Res = closure(P,T,RBody).
1040 % TODO: we could provide more cases like records, sets as lists, freetype values
1041 remove_all_infos_from_bvalue(Val,Val).
1042
1043 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1044
1045 % a version of create_exists_opt which also detects top-level disjunctions
1046 % and marks the exists as generated and as allow_to_lift_exists
1047 create_exists_opt_liftable(Ids,b(disjunct(A,B),pred,Info1),NewPred) :- !,
1048 create_exists_opt_liftable(Ids,A,PA),
1049 create_exists_opt_liftable(Ids,B,PB),
1050 disjunct_predicates_with_pos_info(PA,PB,b(NP,pred,Info2)),
1051 NewPred=b(NP,pred,NewInfo),
1052 extract_just_important_info_aux(Info1,Info2,NewInfo). % copy symbolic or other relevant info
1053 create_exists_opt_liftable(Ids,Pred,NewPred) :- conjunction_to_list(Pred,L),
1054 create_exists_opt(Ids,L,[allow_to_lift_exists],NewPred,_Modified).
1055
1056 % create_exists_opt(TIds,Preds,NewPred)
1057 % creating an existential quantification with some optimisations.
1058 % TIds: The typed identifiers that are quantified
1059 % Preds: A list of predicates
1060 % NewPred: The (optimised) quantified expression
1061 % Basically two optimisations are performed:
1062 % - identifiers that are not used at all are removed from the quantifier
1063 % - predicates that do not use one of the quantified identifiers are moved
1064 % outside the quantification, resulting in a predicate of the form "P & #x.Q(x)"
1065
1066 create_exists_opt(TIds,Preds,NewPred) :-
1067 create_exists_opt(TIds,Preds,[],NewPred,_).
1068
1069 create_exists_opt(TIds,Preds,NewPred,Modified) :-
1070 create_exists_opt(TIds,Preds,[],NewPred,Modified).
1071
1072 create_exists_opt([],Preds,_,NewPred,Modified) :- !, Modified = false,
1073 conjunct_predicates(Preds,NewPred).
1074 create_exists_opt(TIds,Preds,AdditionalInfos,Res,Mod) :-
1075 get_texpr_ids(TIds,UnsortedIds), sort(UnsortedIds,Ids),
1076 (create_exists_opt1(TIds,Ids,Preds,AdditionalInfos,NewPred2,Modified) -> Res = NewPred2, Mod=Modified
1077 ; add_internal_error('Call failed:',create_exists_opt(TIds,Preds,AdditionalInfos,_,_)),fail).
1078 %create_exists_opt1(TIds,_,Preds,AdditionalInfos,NewPred,Modified) :- preference(data_validation_mode,true),
1079 % % do not lift predicates outside of existential quantifiers and change order; see rule_avec_DV.mch ClearSy example (N_ITERa_avec_DV_sans_DV) and test 1945
1080 create_exists_opt1(TIds,Ids,Preds,AdditionalInfos,NewPred2,Modified) :-
1081 create_exists_opt2(Preds,first,Ids,[],Inner,Outer,UsedIds),
1082 % Inner: quantified part, Outer: part which does not have to be quantified
1083 ( Inner = [] -> AllPreds=Outer % no exists needed
1084 ; % Inner = [_|_] ->
1085 create_filtered_exists(TIds,UsedIds,Inner,AdditionalInfos,Exists,IModified),
1086 append(Outer,[Exists],AllPreds)
1087 ),
1088 (Outer=[_|_] -> Modified=true % TO DO: check if TIds=UsedTIds
1089 ; IModified==true -> Modified=true
1090 ; UsedIds == Ids -> Modified= false
1091 ; Modified=true),
1092 conjunct_predicates(AllPreds,NewPred2).
1093
1094 % create an exists for the used Ids only
1095 create_filtered_exists(TIds,UsedIds,Inner,AdditionalInfos,Exists,_) :-
1096 ceo_filter_used_ids(TIds,UsedIds,UsedTIds), % filter out unused variables
1097 conjunct_predicates_with_pos_info(Inner,I), % we could store used_ids info
1098 create_exists_detect_tautology_aux(UsedTIds,I,AdditionalInfos,Exists).
1099 % remove_typing also added in create_exists_detect_tautology_aux
1100
1101
1102 % return Inner: predicates inside quantifier and Outer: predicates that can be moved out of the quantifier
1103 create_exists_opt2([],_,_Ids,UsedIds,[],[],UsedIds) :- !.
1104 create_exists_opt2([Pred|Prest],First,Ids,UsedIdsIn,Inner,Outer,UsedIdsOut) :- !,
1105 find_identifier_uses_if_necessary(Pred, [], LocalUses), % TODO: add used_ids(LocalUses) to Pred
1106 ord_intersection(Ids,LocalUses,ExistsIdsUsed),
1107 ( ExistsIdsUsed = [], % Pred uses none of the quantified ids: we can move it out
1108 (First==first -> true
1109 ; preference(data_validation_mode,false), % see test 1945; step 39 in trace replay
1110 always_well_defined_or_disprover_mode(Pred) % TODO: we should probably also check this !
1111 )
1112 ->
1113 Inner = Irest,
1114 Outer = [Pred|Orest], % move Pred out of existential quantifier as it does not depend on quantified variables
1115 % format('MOVED out of #(~w): ',[Ids]),translate:print_bexpr(Pred), format(' Uses ~w [~w]~n',[LocalUses,ExistsIdsUsed]),
1116 create_exists_opt2(Prest,first,Ids,UsedIdsIn,Irest,Orest,UsedIdsOut)
1117 ;
1118 update_used_ids(Pred,LocalUses,Pred2),
1119 Inner = [Pred2|Irest],
1120 Outer = Orest,
1121 ord_union(UsedIdsIn,ExistsIdsUsed,Urest),
1122 create_exists_opt2(Prest,not_first_anymore,Ids,Urest,Irest,Orest,UsedIdsOut)
1123 ).
1124 create_exists_opt2(Pred,First,Ids,UsedIdsIn,Inner,Outer,UsedIdsOut) :-
1125 add_error(create_exists_opt,'Expecting predicate list: ',Pred),
1126 create_exists_opt2([Pred],First,Ids,UsedIdsIn,Inner,Outer,UsedIdsOut).
1127
1128 % construct exists optimized: keep only used TIds
1129 ceo_filter_used_ids([],_UsedIds,[]).
1130 ceo_filter_used_ids([TId|Irest],UsedIds,Filtered) :-
1131 get_texpr_id(TId,Id),
1132 ( ord_member(Id,UsedIds) -> Filtered = [TId|Frest] % id used: keep it
1133 ; Filtered = Frest),
1134 ceo_filter_used_ids(Irest,UsedIds,Frest).
1135
1136 % a version of create_exists which also detects x=E and x:E, x>E, not(x>E) tautologies
1137 % we could replace this by a more generic prover
1138 create_exists_detect_tautology_aux([TID],b(member(LHS,RHS),pred,_),_,Truth) :-
1139 get_texpr_id(LHS,ID), get_texpr_id(TID,ID),
1140 definitely_not_empty_set(RHS),
1141 always_well_defined_or_disprover_mode(RHS),
1142 !, % replace #x.(x:RHS) by TRUTH
1143 debug_format(19,'Detected tautology exists membership over ~w~n',[ID]),
1144 Truth=b(truth,pred,[]).
1145 create_exists_detect_tautology_aux([TID],b(Pred,_,_),_,Truth) :-
1146 ? is_comparison(Pred,pos_neg(pos,TID),L,R), get_texpr_id(TID,ID),
1147 ((LHS,RHS)=(L,R) ; (LHS,RHS)=(R,L)),
1148 get_texpr_id(LHS,ID),
1149 \+ occurs_in_expr(ID,RHS),
1150 always_well_defined_or_disprover_mode(RHS),
1151 !, % replace #x.(x COMP E) by TRUTH
1152 debug_format(19,'Detected tautology comparison over ~w~n',[ID]),
1153 Truth=b(truth,pred,[]).
1154 %create_exists_detect_tautology_aux(Ids,b(disjunct(A,B),pred,Info1),AdditionalInfos,NewPred) :- !,
1155 % create_exists(Ids,A,PA), create_exists(Ids,B,PB),
1156 % disjunct_predicates_with_pos_info(PA,PB,b(NP,pred,Info2)),
1157 % NewPred=b(NP,pred,NewInfo),
1158 % extract_just_important_info_aux(Info1,Info2,NewInfo). % copy symbolic or other relevant info
1159 create_exists_detect_tautology_aux(Ids,Pred,AdditionalInfos,NewPred2) :-
1160 create_exists_or_let_predicate(Ids,Pred,NewPred),
1161 add_texpr_infos_if_new(NewPred,[removed_typing|AdditionalInfos],NewPred2).
1162 % removed_typing to avoid spurious exists_body_warning, see test 1681, 625
1163
1164
1165 is_eventb_comprehension_set(b(comprehension_set(TopIds,Body),_,Info),Ids,PRED,EXPR) :-
1166 ? is_eventb_comprehension_set(TopIds,Body,Info,Ids,PRED,EXPR).
1167 is_eventb_comprehension_set([TID1],Body,Info,Ids,PRED,EXPR) :-
1168 Body = b(exists(Ids,InnerBody),pred,_),
1169 conjunction_to_list(InnerBody,Inner),
1170 append(Inner1,[b(equal(TID2,EXPR),pred,EqInfo)],Inner),
1171 ? (member(was(event_b_comprehension_set),Info) -> true ;
1172 ? member(prob_annotation('LAMBDA-EQUALITY'),EqInfo) % relevant for TLA2B
1173 ),
1174 same_id(TID1,TID2,_),
1175 conjunct_predicates(Inner1,PRED),
1176 % we check that TID1 is not being used in P1 and not just rely on was(event_b_comprehension_set)
1177 not_occurs_in_expr(PRED,TID1).
1178
1179 % -------------------
1180
1181 is_equal(b(equal(LHS,RHS),pred,_),A,B) :-
1182 ((A,B)=(LHS,RHS) ; (A,B)=(RHS,LHS)).
1183
1184 :- use_module(typing_tools,[type_has_at_least_two_elements/1]).
1185 is_comparison(greater(A,B),_,A,B).
1186 is_comparison(less(A,B),_,A,B).
1187 is_comparison(greater_equal(A,B),_,A,B).
1188 is_comparison(less_equal(A,B),_,A,B).
1189 is_comparison(equal(A,B),pos_neg(P,TID),A,B) :-
1190 % for neg: we need to make sure there is more than one value in the type (otherwise we cannot make equal false)
1191 % for pos: assuming the RHS expression above is well-defined there must be at least one element; no need to check non_empty_type(Type)
1192 (P=pos -> true ; get_texpr_type(TID,Type),type_has_at_least_two_elements(Type)).
1193 is_comparison(not_equal(A,B),pos_neg(P,TID),A,B) :- % ditto but with pos and neg reversed
1194 (P=neg -> true ; get_texpr_type(TID,Type),type_has_at_least_two_elements(Type)).
1195 ?is_comparison(negation(b(Comp,pred,_)),PosNeg,A,B) :- negate(PosNeg,P2),
1196 is_comparison(Comp,P2,A,B).
1197 negate(pos_neg(pos,T),pos_neg(neg,T)).
1198 negate(pos_neg(neg,T),pos_neg(pos,T)).
1199
1200
1201
1202 % is true if a predicate Pred can be split into two parts:
1203 % Outer which does not depend on LocalIds (can be lifted out) and Inner which does
1204 detect_global_predicates(LocalIds,Pred,Outer,Inner) :-
1205 get_texpr_ids(LocalIds,UnsortedIds), sort(UnsortedIds,Ids),
1206 conjunction_to_list(Pred,Preds),
1207 split_predicate_local_global(Preds,Ids,OuterL,InnerL),
1208 OuterL \= [],
1209 conjunct_predicates(OuterL,Outer),
1210 conjunct_predicates(InnerL,Inner).
1211 split_predicate_local_global([],_Ids,[],[]).
1212 split_predicate_local_global([P|Ps],Ids,Outer,Inner) :-
1213 (is_local_predicate(Ids,P)
1214 -> Inner = [P|Is], split_predicate_local_global(Ps,Ids,Outer,Is)
1215 ; Outer = [P|Os], split_predicate_local_global(Ps,Ids,Os,Inner)).
1216 is_local_predicate(Ids,Pred) :-
1217 find_identifier_uses_if_necessary(Pred, [], LocalUses),
1218 ord_intersect(Ids,LocalUses).
1219
1220 %:- use_module(b_global_sets,[b_global_set/1]).
1221 definitely_not_empty_set(b(SET,T,_)) :- not_empty_set_aux(SET,T).
1222 not_empty_set_aux(bool_set,_).
1223 not_empty_set_aux(integer_set(_),_).
1224 not_empty_set_aux(float_set,_).
1225 not_empty_set_aux(real_set,_).
1226 not_empty_set_aux(string_set,_).
1227 not_empty_set_aux(set_extension(X),_) :- dif(X,[]).
1228 not_empty_set_aux(sequence_extension(X),_) :- dif(X,[]).
1229 not_empty_set_aux(pow_subset(_),_). % always contains at least the empty set
1230 not_empty_set_aux(fin_subset(_),_). % ditto
1231 not_empty_set_aux(seq(_),_). % ditto
1232 not_empty_set_aux(iseq(_),_). % ditto
1233 not_empty_set_aux(pow1_subset(A),_) :- definitely_not_empty_set(A).
1234 not_empty_set_aux(fin1_subset(A),_) :- definitely_not_empty_set(A).
1235 not_empty_set_aux(seq1(A),_) :- definitely_not_empty_set(A).
1236 not_empty_set_aux(iseq1(A),_) :- definitely_not_empty_set(A).
1237 not_empty_set_aux(cartesian_product(A,B),_) :- definitely_not_empty_set(A), definitely_not_empty_set(B).
1238 not_empty_set_aux(partial_function(_A,_B),_). % always contains at least the empty set
1239 not_empty_set_aux(partial_injection(_A,_B),_). % ditto
1240 not_empty_set_aux(relations(_A,_B),_). % ditto
1241 not_empty_set_aux(total_function(A,B),_) :-
1242 (definitely_not_empty_set(B) -> true
1243 ; definitely_empty_set(A)). % if A is empty, then the set of total functions is {{}}
1244 not_empty_set_aux(union(A,B),_) :- (definitely_not_empty_set(A) -> true ; definitely_not_empty_set(B)).
1245 not_empty_set_aux(overwrite(A,B),_) :- (definitely_not_empty_set(A) -> true ; definitely_not_empty_set(B)).
1246 % TODO: add a few more function rules
1247 not_empty_set_aux(value(S),_) :- not_empty_value(S).
1248 %not_empty_set_aux(identifier(X),set(global(X))) :- bmachine:b_get_machine_set(X). % what if we have a local variable ? ENSURE THAT WE DO NOT ALLOW identifier X to stand for global set X; see ExistentialGlobalSetIDTest in Tester % also: b_global_set not yet computed when ast_cleanup runs on startup !
1249 % TO DO: determine which identifier(X) refer to global set names
1250 not_empty_set_aux(interval(A,B),_) :- get_integer(A,IA), get_integer(B,IB), IA =< IB.
1251
1252 :- use_module(b_global_sets,[b_non_empty_global_set/1]).
1253 :- use_module(kernel_freetypes,[is_non_empty_freetype/1]).
1254 not_empty_value(S) :- var(S),!,fail.
1255 not_empty_value(avl_set(_)).
1256 not_empty_value([_|_]).
1257 not_empty_value(global_set(G)) :- b_non_empty_global_set(G). % always true
1258 not_empty_value(freetype(G)) :- is_non_empty_freetype(G). % always true
1259 not_empty_value(closure(P,T,B)) :-
1260 custom_explicit_sets:is_interval_closure(P,T,B,LOW,UP), integer(LOW),integer(UP), LOW =< UP.
1261 %TODO: more closures; see also definitely_not_empty_finite_value
1262
1263 definitely_empty_set(b(ES,_,_)) :- is_empty_set_aux(ES).
1264 is_empty_set_aux(empty_set).
1265 is_empty_set_aux(empty_sequence).
1266 is_empty_set_aux(domain(D)) :- definitely_empty_set(D).
1267 is_empty_set_aux(range(D)) :- definitely_empty_set(D).
1268 is_empty_set_aux(domain_subtraction(_,Rel)) :- definitely_empty_set(Rel).
1269 is_empty_set_aux(domain_restriction(Dom,Rel)) :- (definitely_empty_set(Dom) -> true ; definitely_empty_set(Rel)).
1270 is_empty_set_aux(range_restriction(Rel,Ran)) :- (definitely_empty_set(Ran) -> true ; definitely_empty_set(Rel)).
1271 is_empty_set_aux(range_subtraction(Rel,_)) :- definitely_empty_set(Rel).
1272 is_empty_set_aux(interval(A,B)) :- get_integer(A,IA), get_integer(B,IB), IA > IB.
1273 is_empty_set_aux(intersection(A,B)) :- (definitely_empty_set(A) -> true ; definitely_empty_set(B)).
1274 is_empty_set_aux(set_subtraction(A,_)) :- definitely_empty_set(A).
1275 is_empty_set_aux(union(A,B)) :- definitely_empty_set(A), definitely_empty_set(B).
1276 is_empty_set_aux(overwrite(A,B)) :- definitely_empty_set(A), definitely_empty_set(B).
1277 is_empty_set_aux(value(V)) :- V==[].
1278
1279
1280 get_integer(b(B,_,_),I) :- get_integer_aux(B,I).
1281 get_integer_aux(integer(I),I).
1282 get_integer_aux(value(V),I) :- get_integer_value(V,I).
1283 get_integer_value(V,I) :- nonvar(V),V=int(I), integer(I).
1284
1285
1286
1287 :- use_module(probsrc(custom_explicit_sets),[avl_is_interval/3]).
1288 get_interval(b(I,set(integer),_),Low,Up) :-
1289 is_interval_aux(I,Low,Up).
1290 is_interval_aux(interval(Low,Up),Low,Up).
1291 is_interval_aux(value(CS),Low,Up) :- nonvar(CS), CS=avl_set(AVL), % occurs in Leftpad_i.imp
1292 Low = b(integer(LI),integer,[]), Up = b(integer(UI),integer,[]),
1293 avl_is_interval(AVL,LI,UI).
1294 is_interval_aux(set_extension(List),Low,Up) :- print(l(List)),nl,
1295 sort(List,SList),
1296 SList = [Low|Rest], get_integer(Low,LI),
1297 last(SList,Up), get_integer(Up,UI),
1298 length(List,Len),
1299 Len is UI-LI+1,
1300 maplist(get_integer,Rest,_).
1301
1302 % a simple let-detection
1303 create_exists_or_let_predicate([H|T],b(conjunct(LHS,RHS),pred,I),NewPred) :- get_texpr_id(H,ID),
1304 ? is_equal(LHS,TID,IDEXPR), % TO DO: should we do a more complicated check here ? exist technique useful for SLOT-24 codespeed test
1305 get_texpr_id(TID,ID), \+ occurs_in_expr(ID,IDEXPR),
1306 maplist(not_occurs_in_expr(IDEXPR),T),
1307 !,
1308 NewPred = b(let_predicate([TID],[IDEXPR],Body),pred,I),
1309 %print('LET: '),translate:print_bexpr(NewPred),nl,
1310 create_exists_or_let_predicate(T,RHS,Body).
1311 create_exists_or_let_predicate(Ids,Pred,NewPred) :- create_exists(Ids,Pred,NewPred).
1312
1313 not_occurs_in_expr(IDEXPR,TID) :- get_texpr_id(TID,ID), \+ occurs_in_expr(ID,IDEXPR).
1314
1315 create_exists([],Pred,NewPred) :- !,Pred=NewPred.
1316 create_exists(Ids,Pred,NewPred) :-
1317 find_identifier_uses_for_quantifier_body(Ids,Pred, Used),
1318 extract_info_wo_used_ids(Pred,NewImportantInfo),
1319 create_texpr(exists(Ids,Pred),pred,[used_ids(Used)|NewImportantInfo],NewPred).
1320
1321 % try and infer seq(.) types for identifiers
1322 % at the moment this is a light-weight inference just using membership predicates
1323 infer_seq_types_for_tids([],_Pred,NewIds) :- !, NewIds=[].
1324 infer_seq_types_for_tids(Ids,Pred,NewIds) :-
1325 conjunction_to_list(Pred,LP),
1326 infer_seq_types_for_preds(LP,Ids,NewIds).
1327
1328 infer_seq_types_for_preds([],TIds,TIds).
1329 infer_seq_types_for_preds([H|T],TIds,NewTIds) :-
1330 infer_seq_type_for_id(H,Id,NewType),
1331 debug_println(19,sequence_type_inferred_for(Id,NewType)),
1332 TID = b(identifier(Id),_OldType,Info),
1333 ? nth1(Pos,TIds,TID,Rest),
1334 get_texpr_id(TID,Id),!,
1335 nth1(Pos,NewTIds1,b(identifier(Id),NewType,Info),Rest),
1336 infer_seq_types_for_preds(T,NewTIds1,NewTIds).
1337 infer_seq_types_for_preds([b(LetPred,pred,_)|T],TIds,NewTIds) :- % see test 1377
1338 is_let_pred(LetPred,LetTIds,MainPred),
1339 % there should be no conflict between lazy let id @Nr and quantified variables; but we check nonetheless
1340 \+ clash(LetTIds,TIds),
1341 !,
1342 conjunction_to_list(MainPred,MainLP),
1343 infer_seq_types_for_preds(MainLP,TIds,TIds2), % TODO: store value of LazyLetID?
1344 infer_seq_types_for_preds(T,TIds2,NewTIds).
1345 infer_seq_types_for_preds([_|T],TIds,NewTIds) :- infer_seq_types_for_preds(T,TIds,NewTIds).
1346
1347 ?clash(TIds1,TIds2) :- member(TLazyID,TIds1),
1348 get_texpr_id(TLazyID,LazyID),
1349 % there should be no conflict between lazy let id @Nr and quantified variables; but we check nonetheless
1350 member(b(identifier(LazyID),_,_),TIds2).
1351 is_let_pred(lazy_let_pred(TLazyID,_SharedExpr,MainPred),[TLazyID],MainPred).
1352 is_let_pred(let_predicate(TIDs,_SharedExpr,MainPred),TIDs,MainPred).
1353
1354
1355 infer_seq_type_for_id(b(member(LHS,RHS),_,_),Id,Type) :-
1356 get_texpr_id(LHS,Id),
1357 is_seq_type_rhs(RHS,Type).
1358
1359 is_seq_type_rhs(b(E,T,_),seq(ResType)) :-
1360 ? T = set(SEQT), is_seq_type(SEQT,SType),
1361 is_seq_type_rhs2(E,SType,ResType).
1362 is_seq_type_rhs2(seq(Set),FullType,SeqType) :-
1363 (is_seq_type_rhs(Set,IS) -> SeqType=IS ; SeqType=FullType). % TODO: check if arguments also contain seq types
1364 is_seq_type_rhs2(iseq1(Set),FullType,S) :- is_seq_type_rhs2(seq(Set),FullType,S).
1365 is_seq_type_rhs2(iseq(Set),FullType,S) :- is_seq_type_rhs2(seq(Set),FullType,S).
1366 is_seq_type_rhs2(seq1(Set),FullType,S) :- is_seq_type_rhs2(seq(Set),FullType,S).
1367 is_seq_type_rhs2(perm(Set),FullType,S) :- is_seq_type_rhs2(seq(Set),FullType,S).
1368 is_seq_type_rhs2(value(V),_FullType,S) :- nonvar(V), V=closure([_],[seq(S)],_). % TODO: more than one arg
1369 % TODO: relations/functions/cartesian product with seq types
1370 % TODO: {x|x : seq((0 .. 1)) & card(x) > 5}, ...
1371
1372 is_seq_type(seq(S),S).
1373 is_seq_type(set(couple(integer,S)),S).
1374
1375 % a version of create_exists which can merge with an already present exists if possible
1376 % possibly more expensive as identfiers used are recomputed for the moment (TODO: reuse used_ids and subtract)
1377 create_or_merge_exists(IDs, Condition, Exists):-
1378 get_texpr_expr(Condition,exists(InnerVars,InnerCond)),!,
1379 % fuse two exists together
1380 append(IDs,InnerVars,Vars),
1381 create_or_merge_exists(Vars,InnerCond,Exists).
1382 create_or_merge_exists(IDs, Condition, Exists):-
1383 create_exists(IDs,Condition,Exists).
1384
1385 % see create_unsimplified_exists
1386 not_generated_exists_paras([b(_,_,Infos)|_]) :- nonmember(generated_exists_parameter,Infos).
1387
1388
1389 create_forall([],Pred,NewPred) :- !,Pred=NewPred.
1390 create_forall(Ids,Pred,NewPred) :-
1391 find_identifier_uses_for_quantifier_body(Ids,Pred, Used),
1392 split_forall_body(Pred,LHS,RHS),
1393 extract_info_wo_used_ids_and_pos(LHS,RHS,NewImportantInfo),
1394 infer_seq_types_for_tids(Ids,LHS,Ids2),
1395 create_texpr(forall(Ids2,LHS,RHS),pred,[used_ids(Used)|NewImportantInfo],NewPred).
1396 split_forall_body(b(implication(LHS,RHS),_,_),LHS,RHS) :- !.
1397 split_forall_body(RHS,b(truth,pred,[]),RHS).
1398
1399 create_implication(b(truth,pred,_),P,Res) :- !, Res=P.
1400 create_implication(b(falsity,pred,_),P,Res) :- !, create_negation(P,Res).
1401 create_implication(Lhs,Rhs,b(implication(Lhs,Rhs),pred,NewInfo)) :-
1402 extract_info(Lhs,Rhs,NewInfo).
1403
1404 create_equivalence(Lhs,Rhs, b(equivalence(Lhs,Rhs),pred,NewInfo)) :-
1405 extract_info(Lhs,Rhs,NewInfo).
1406
1407 create_negation(b(P,pred,I),Res) :- create_negation_aux(P,I,R),!,Res=R.
1408 create_negation(Pred,b(negation(Pred),pred,NewInfo)) :-
1409 extract_info(Pred,Infos),
1410 ? (get_texpr_non_label_posinfo(Pred,Pos) -> NewInfo = [Pos|Infos] ; NewInfo=Infos).
1411
1412 create_negation_aux(truth,I,R) :- !, R=b(falsity,pred,I).
1413 create_negation_aux(falsity,I,R) :- !, R=b(truth,pred,I).
1414 create_negation_aux(negation(Pred),_,R) :- R=Pred. % not(not(P)) = P
1415 %create_negation_aux(equal(A,B),I,R) :- !, R=b(not_equal(A,B),pred,I).
1416 %create_negation_aux(not_equal(A,B),I,R) :- !, R=b(equal(A,B),pred,I).
1417 % we could add some rules about negating member <-> not_member, ... but be careful with effects on is_negation_of
1418
1419 % check if something is the negation of something else (quite stupid at the moment)
1420 % used, e.g., to detect IF-THEN-ELSE constructs in b_ast_cleanup
1421 is_negation_of(P,NP) :-
1422 create_negation(P,NotP), % works both with not(A),A or A,not(A)
1423 same_texpr(NotP,NP).
1424 ?is_negation_of(b(P,pred,_),b(NP,pred,_)) :- is_negation_aux(P,NP).
1425
1426 ?is_negation_aux(equal(A,B),NP) :- is_negation_of_equality(NP,A,B).
1427 is_negation_aux(not_equal(A,B),NP) :- is_negation_of_disequality(NP,A,B).
1428 is_negation_aux(subset(XA,SA),not_subset(XB,SB)) :- same_texpr(XA,XB), same_texpr(SA,SB).
1429 is_negation_aux(not_subset(XA,SA),subset(XB,SB)) :- same_texpr(XA,XB), same_texpr(SA,SB).
1430 is_negation_aux(subset_strict(XA,SA),not_subset_strict(XB,SB)) :- same_texpr(XA,XB), same_texpr(SA,SB).
1431 is_negation_aux(not_subset_strict(XA,SA),subset_strict(XB,SB)) :- same_texpr(XA,XB), same_texpr(SA,SB).
1432 is_negation_aux(member(XA,SA),not_member(XB,SB)) :- same_texpr(XA,XB), same_texpr(SA,SB).
1433 is_negation_aux(not_member(XA,SA),member(XB,SB)) :- same_texpr(XA,XB), same_texpr(SA,SB).
1434 is_negation_aux(less(A,B),greater_equal(AA,BB)) :- same_texpr(A,AA), same_texpr(B,BB).
1435 is_negation_aux(less(A,B),less_equal(BB,AA)) :- same_texpr(A,AA), same_texpr(B,BB).
1436 is_negation_aux(less_equal(B,A),less(AA,BB)) :- same_texpr(A,AA), same_texpr(B,BB).
1437 is_negation_aux(less_equal(A,B),greater(AA,BB)) :- same_texpr(A,AA), same_texpr(B,BB).
1438 ?is_negation_aux(greater_equal(A,B),NP) :- is_negation_aux(less_equal(B,A),NP).
1439 is_negation_aux(greater(A,B),NP) :- is_negation_aux(less(B,A),NP).
1440 is_negation_aux(less_equal_real(B,A),less_real(AA,BB)) :- same_texpr(A,AA), same_texpr(B,BB).
1441 is_negation_aux(less_real(B,A),less_equal_real(AA,BB)) :- same_texpr(A,AA), same_texpr(B,BB).
1442 is_negation_aux(negation(A),negation(B)) :- is_negation_of(A,B).
1443 is_negation_aux(truth,falsity).
1444 is_negation_aux(falsity,truth).
1445 % TO DO: detect more ?? x < y <=> not ( x > y-1 )
1446
1447 is_negation_of_equality(not_equal(AA,BB),A,B) :- same_texpr(A,AA), same_texpr(B,BB).
1448 ?is_negation_of_equality(equal(AA,BB),A,B) :- same_texpr(A,AA), neg_value(BB,B).
1449
1450 neg_value(b(boolean_true,_,_),b(boolean_false,_,_)).
1451 neg_value(b(boolean_false,_,_),b(boolean_true,_,_)).
1452
1453 is_negation_of_disequality(equal(AA,BB),A,B) :- same_texpr(A,AA), same_texpr(B,BB).
1454 is_negation_of_disequality(not_equal(AA,BB),A,B) :- same_texpr(A,AA), neg_value(BB,B).
1455
1456
1457 % another version which is simpler can can be used to get the negation of some operators
1458
1459 get_negated_operator_expr(b(E,pred,_),Res) :- negate_expr_aux(E,Res).
1460 negate_expr_aux(falsity,truth).
1461 negate_expr_aux(truth,falsity).
1462 negate_expr_aux(member(X,S),not_member(X,S)).
1463 negate_expr_aux(not_member(X,S),member(X,S)).
1464 negate_expr_aux(subset(X,S),not_subset(X,S)).
1465 negate_expr_aux(not_subset(X,S),subset(X,S)).
1466 negate_expr_aux(subset_strict(X,S),not_subset_strict(X,S)).
1467 negate_expr_aux(not_subset_strict(X,S),subset_strict(X,S)).
1468 negate_expr_aux(equal(X,S),not_equal(X,S)).
1469 negate_expr_aux(not_equal(X,S),equal(X,S)).
1470 negate_expr_aux(less(X,S),greater_equal(X,S)).
1471 negate_expr_aux(greater_equal(X,S),less(X,S)).
1472 negate_expr_aux(less_equal(X,S),greater(X,S)).
1473 negate_expr_aux(greater(X,S),less_equal(X,S)).
1474 negate_expr_aux(less_equal_real(X,S),less_real(S,X)).
1475 negate_expr_aux(less_real(X,S),less_equal_real(S,X)).
1476 % TO DO: negation()
1477
1478
1479 % a liberal version for finding equalities
1480 is_equality(TP,TA,TB) :- get_texpr_expr(TP,P), is_equality_aux(P,TA,TB).
1481
1482 is_equality_aux(Var,TA,TB) :- var(Var),!, add_internal_error('Illegal call: ', is_equality_aux(Var,TA,TB)),fail.
1483 is_equality_aux(equal(TA,TB),TA,TB).
1484 is_equality_aux(not_equal(TA,TB),NTA,NTB) :-
1485 (negate_boolean_value(TB,NTB) -> NTA=TA
1486 ; NTB=TB, negate_boolean_value(TA,NTA)). % TA /= TRUE ---> TA = FALSE
1487 is_equality_aux(partition(TA,[TB]),TA,TB).
1488 is_equality_aux(member(TA,TSet),TA,TB) :- singleton_set_extension(TSet,TB). % TA:{TB}
1489 is_equality_aux(negation(TExpr),TA,TB) :- get_negated_operator_expr(TExpr,NT), is_equality_aux(NT,TA,TB).
1490
1491 negate_boolean_value(b(B,T,I),b(NB,T,I)) :- neg_bool_aux(B,NB).
1492 neg_bool_aux(boolean_true,boolean_false).
1493 neg_bool_aux(boolean_false,boolean_true).
1494 % TODO: should we also detect value(pred_true), ....
1495
1496 singleton_set_extension(b(SONE,Type,_),El) :- singleton_set_extension_aux(SONE,Type,El).
1497 singleton_set_extension_aux(set_extension([El]),_,El).
1498 singleton_set_extension_aux(value(Set),SType,b(value(El),Type,[])) :-
1499 is_set_type(SType,Type),custom_explicit_sets:singleton_set(Set,El).
1500 singleton_set_extension_aux(sequence_extension([El]),_,Couple) :-
1501 ONE = b(integer(1),integer,[]),
1502 create_couple(ONE,El,Couple).
1503
1504
1505 % detect various forms of membership:
1506 is_membership(b(Expr,pred,_),TID,Set) :- is_membership_aux(Expr,TID,Set).
1507 is_membership_aux(member(TID,Set),TID,Set).
1508 is_membership_aux(subset(SONE,Set),TID,Set) :- singleton_set_extension(SONE,TID). % {TID} <: Set
1509
1510 % detect even more forms of membership:
1511 is_membership_or_equality(b(Expr,pred,_),TID,Set) :-
1512 ? (is_membership_aux(Expr,TID,Set) -> true ; is_mem_eq_aux(Expr,TID,Set)).
1513
1514 is_mem_eq_aux(equal(TID,VAL),TID,Set) :- % x=VAL <==> x:{VAL}
1515 get_texpr_type(VAL,Type),
1516 safe_create_texpr(set_extension([VAL]),set(Type),Set).
1517
1518 % extract a lambda equality from a body; we suppose the equality is the last conjunct
1519 get_lambda_equality(b(equal(TID,ResultExpr),pred,_),ID,[],ResultExpr) :- get_texpr_id(TID,ID).
1520 get_lambda_equality(b(conjunct(LHS,RHS),pred,_),ID,[LHS|T],ResultExpr) :-
1521 ? get_lambda_equality(RHS,ID,T,ResultExpr).
1522
1523 % see pred_succ_compset in ast_cleanup which constructs these terms
1524 is_succ_compset(Paras,Body) :-
1525 Paras = [b(identifier('_succ_'),integer,_),
1526 b(identifier(LAMBDARES),integer,_)],
1527 Body = b(equal(LR,T),pred,_),
1528 LR = b(identifier(LAMBDARES),integer,_),
1529 T = b(add(ARG,One),integer,_),
1530 get_integer(One,1), ARG = b(identifier('_succ_'),integer,_).
1531 is_pred_compset(Paras,Body) :-
1532 Paras = [b(identifier('_pred_'),integer,_),
1533 b(identifier(LAMBDARES),integer,_)],
1534 Body = b(equal(LR,T),pred,_),
1535 LR = b(identifier(LAMBDARES),integer,_),
1536 T = b(minus(ARG,One),integer,_),
1537 get_integer(One,1), ARG = b(identifier('_pred_'),integer,_).
1538
1539 % ---------------------------------
1540
1541 is_pow_subset(B,Set) :-
1542 ( B = b(pow_subset(Set),_,_)
1543 ; B = b(fin_subset(Set),_,_),
1544 finite_wd_set_value(Set)
1545 ).
1546 is_pow1_subset(B,Set) :-
1547 ( B = b(pow1_subset(Set),_,_)
1548 ; B = b(fin1_subset(Set),_,_),
1549 finite_wd_set_value(Set)
1550 ).
1551
1552 % ---------------------------------
1553
1554 get_texpr_couple(b(couple(TA1,TA2),_,_),TA1,TA2).
1555
1556 % detect TA1|->TA2 = TB1|->TB2 and split into two
1557 split_equality(b(equal(TA,TB),pred,I),b(equal(TA1,TB1),pred,I),b(equal(TA2,TB2),pred,I)) :-
1558 get_texpr_couple(TA,TA1,TA2),
1559 get_texpr_couple(TB,TB1,TB2).
1560
1561 create_equality(b(_,TA,_),b(_,TB,_),_) :- TA \= TB, \+ unify_types_strict(TA,TB),!,
1562 add_internal_error('Creating equality with incompatible types:',equal(TA,TB)),fail.
1563 create_equality(A,B,Equality) :-
1564 safe_create_texpr(equal(A,B),pred,Equality).
1565
1566 create_couple(A,B,b(couple(A,B),couple(TA,TB),Infos)) :-
1567 get_texpr_type(A,TA), get_texpr_type(B,TB),
1568 extract_info(A,B,Infos).
1569
1570 % couplise_list for typed expression list
1571 create_couple([A],Couple) :- !,A=Couple.
1572 create_couple([A,B|Rest],Couple) :-
1573 create_couple(A,B,Couple1),
1574 create_couple([Couple1|Rest],Couple).
1575
1576 create_cartesian_product(A,B,CartAB) :-
1577 get_texpr_types([A,B],[STA,STB]),
1578 is_set_type(STA,TypeA), is_set_type(STB,TypeB),
1579 safe_create_texpr(cartesian_product(A,B),set(couple(TypeA,TypeB)),CartAB).
1580
1581 % derive typing from Ids
1582 create_comprehension_set(Ids,Pred,Info,CompSet) :-
1583 get_texpr_types(Ids,Types),
1584 couplise_list(Types,ElementType),
1585 create_texpr(comprehension_set(Ids,Pred),set(ElementType),Info,CompSet).
1586
1587
1588 :- assert_must_succeed(bsyntaxtree:nested_couple_to_list(b(couple(b(couple(a,b),x,[]),c),xx,[]),[a,b,c])).
1589 :- assert_must_succeed(bsyntaxtree:nested_couple_to_list(b(couple(a,c),x,[]),[a,c])).
1590 :- assert_must_succeed(bsyntaxtree:nested_couple_to_list(b(couple(a,b(couple(b,c),x,[])),xx,[]),[a,b(couple(b,c),x,[])])).
1591 nested_couple_to_list(NC,L) :- nested_couple_to_list_dcg(NC,L,[]).
1592 nested_couple_to_list_dcg(b(couple(A,B),_,_)) --> !,
1593 nested_couple_to_list_dcg(A), [B].
1594 nested_couple_to_list_dcg(E) --> [E].
1595
1596 % --------------------------------------
1597
1598
1599 % check if identifier(s) occur in typed expressions
1600
1601 occurs_in_expr(ID,TExpr) :- var(ID),!,
1602 add_internal_error('Variable id: ',occurs_in_expr(ID,TExpr)),fail.
1603 occurs_in_expr(ID,TExpr) :- ID=b(_,_,_),!, add_internal_error('Non-atomic identifier: ',occurs_in_expr(ID,TExpr)),fail.
1604 occurs_in_expr(ID,TExpr) :- ID=[_|_],!,
1605 add_internal_error('List instead of identifier: ',occurs_in_expr(ID,TExpr)),fail.
1606 occurs_in_expr(ID,TExpr) :- occurs_in_expr1(TExpr,ID).
1607
1608 % treat a few common operators here; possibly avoid traversing whole term if we find ID in a sub-tree
1609 occurs_in_expr1(TExpr,ID) :- TExpr = b(Expr,_,_),!,
1610 occurs_in_expr2(Expr,TExpr,ID).
1611 occurs_in_expr1(TExpr,ID) :- add_internal_error('Illegal typed expression:',occurs_in_expr1(TExpr,ID)).
1612
1613 occurs_in_expr2(add(A,B),_,ID) :- !,
1614 (occurs_in_expr1(A,ID) -> true ; occurs_in_expr1(B,ID)).
1615 occurs_in_expr2(conjunct(A,B),_,ID) :- !,
1616 (occurs_in_expr1(A,ID) -> true ; occurs_in_expr1(B,ID)).
1617 occurs_in_expr2(couple(A,B),_,ID) :- !,
1618 (occurs_in_expr1(A,ID) -> true ; occurs_in_expr1(B,ID)).
1619 occurs_in_expr2(member(A,B),_,ID) :- !,
1620 (occurs_in_expr1(A,ID) -> true ; occurs_in_expr1(B,ID)).
1621 occurs_in_expr2(equal(A,B),_,ID) :- !,
1622 (occurs_in_expr1(A,ID) -> true ; occurs_in_expr1(B,ID)).
1623 occurs_in_expr2(function(A,B),_,ID) :- !,
1624 (occurs_in_expr1(A,ID) -> true ; occurs_in_expr1(B,ID)).
1625 occurs_in_expr2(image(A,B),_,ID) :- !,
1626 (occurs_in_expr1(A,ID) -> true ; occurs_in_expr1(B,ID)).
1627 occurs_in_expr2(intersection(A,B),_,ID) :- !,
1628 (occurs_in_expr1(A,ID) -> true ; occurs_in_expr1(B,ID)).
1629 occurs_in_expr2(interval(A,B),_,ID) :- !,
1630 (occurs_in_expr1(A,ID) -> true ; occurs_in_expr1(B,ID)).
1631 occurs_in_expr2(not_equal(A,B),_,ID) :- !,
1632 (occurs_in_expr1(A,ID) -> true ; occurs_in_expr1(B,ID)).
1633 occurs_in_expr2(assertion_expression(A,_Msg,B),_,ID) :- !,
1634 (occurs_in_expr1(A,ID) -> true ; occurs_in_expr1(B,ID)).
1635 occurs_in_expr2(domain(A),_,ID) :- !, occurs_in_expr1(A,ID).
1636 occurs_in_expr2(range(A),_,ID) :- !, occurs_in_expr1(A,ID).
1637 occurs_in_expr2(record_field(A,_FieldName),_,ID) :- !, occurs_in_expr1(A,ID).
1638 occurs_in_expr2(identifier(ID1),_,ID) :- !,
1639 ID1 = ID.
1640 occurs_in_expr2(integer(_),_,_ID) :- !,fail.
1641 occurs_in_expr2(string(_),_,_ID) :- !,fail.
1642 occurs_in_expr2(value(_),_,_ID) :- !,fail.
1643 occurs_in_expr2(truth,_,_ID) :- !,fail.
1644 occurs_in_expr2(if_then_else(A,B,C),_,ID) :- !,
1645 (occurs_in_expr1(A,ID) -> true ; occurs_in_expr1(B,ID) -> true ; occurs_in_expr1(C,ID)).
1646 occurs_in_expr2(rec(Fields),_,ID) :- !,
1647 l_field_occurs_in_expr1(Fields,ID).
1648 occurs_in_expr2(set_extension(Elements),_,ID) :- !,
1649 l_occurs_in_expr1(Elements,ID).
1650 occurs_in_expr2(sequence_extension(Elements),_,ID) :- !,
1651 l_occurs_in_expr1(Elements,ID).
1652 occurs_in_expr2(Expr,_,ID) :-
1653 syntaxelement(Expr,List,[], [], [], _), % no bound quantifiers; TO DO: treat bound quantifiers
1654 !,
1655 l_occurs_in_expr1(List,ID).
1656 occurs_in_expr2(_E,TExpr,ID) :-
1657 %functor(_E,F,N), print(occurs_in_expr2(F,N,ID)),nl,
1658 (find_identifier_uses_if_necessary(TExpr,[],Used)
1659 -> %check_sorted(Used),
1660 %add_message(bsyntaxtree,'Occurs check: ',ID:Used,TExpr), translate:nested_print_bexpr(TExpr),nl,
1661 ord_member(ID,Used)
1662 ; add_failed_call_error(find_identifier_uses(TExpr,[],_)),fail).
1663 % TO DO: optimize so that we only look for ID; we don't have to keep track of other IDs
1664
1665 l_occurs_in_expr1([H|T],ID) :- !,
1666 (occurs_in_expr1(H,ID) -> true ; l_occurs_in_expr1(T,ID)).
1667 l_occurs_in_expr1(L,ID) :- L \= [],
1668 add_internal_error('Illegal typed expression list:',l_occurs_in_expr1(L,ID)).
1669 l_field_occurs_in_expr1([field(_,H)|T],ID) :- !,
1670 (occurs_in_expr1(H,ID) -> true ; l_field_occurs_in_expr1(T,ID)).
1671 l_field_occurs_in_expr1(L,ID) :- L \= [],
1672 add_internal_error('Illegal record field list:',l_field_occurs_in_expr1(L,ID)).
1673
1674 %check_sorted(List) :- sort(List,SL), (SL \= List -> add_internal_error('Not sorted:',List) ; true).
1675
1676 some_id_occurs_in_expr([H|T],TExpr) :- (var(H) ; \+ atomic(H) ; var(T) ; T=[H2|_], H2 @< H),
1677 add_internal_error('Must be (sorted) atomic identifiers: ',some_id_occurs_in_expr([H|T],TExpr)),
1678 fail.
1679 some_id_occurs_in_expr([Id],TExpr) :- !, % use version without complete find_identifier_uses
1680 occurs_in_expr(Id,TExpr).
1681 some_id_occurs_in_expr(SortedIDs,TExpr) :-
1682 find_identifier_uses_if_necessary(TExpr,[],Used),
1683 list_to_ord_set(Used,UsedSorted),
1684 ord_intersect(UsedSorted,SortedIDs).
1685
1686 % -----------------------------
1687
1688 % find used identifiers in typed expressions
1689
1690 % a special version for quantifier bodies, attempting to reuse used_ids info
1691 find_identifier_uses_for_quantifier_body(TIds,Body,Res) :-
1692 get_texpr_ids(TIds,Ids),
1693 list_to_ord_set(Ids,Ignore),
1694 find_identifier_uses_if_necessary(Body,Ignore,Res).
1695
1696 % only run find_identifier_uses if necessary because no used_ids Info field present
1697 % TO DO: we could consider using used_ids within find_typed_identifier_uses: drawback: we would need to store types
1698 find_identifier_uses_if_necessary(Expr,Ignore,Res) :-
1699 get_texpr_info(Expr,I),
1700 ? member(used_ids(UIds),I),!, %print('+'),nl,
1701 find_with_reuse(Expr,UIds,Ignore,Res).
1702 find_identifier_uses_if_necessary(Expr,Ignore,Res) :- find_identifier_uses(Expr,Ignore,Res).
1703
1704 find_with_reuse(Expr,UIds,Ignore,Res) :- preference(prob_safe_mode,true),
1705 !,
1706 (is_ordset(Ignore) -> true ; add_internal_error('Not ordset: ',Ignore)),
1707 (is_ordset(UIds) -> true ; add_internal_error('Not ordset: ',UIds)),
1708 ord_subtract(UIds,Ignore,Res0),
1709 find_identifier_uses(Expr,Ignore,Res1),
1710 (Res1=Res0 -> true
1711 ; ord_subtract(Res1,Res0,Miss), % missing
1712 ord_subtract(Res0,Res1,Res01), % too much
1713 (Miss=[] -> add_message(find_identifier_uses_if_necessary,'Suboptimal used_ids: ',Res01,Expr)
1714 ; add_internal_error('Incorrect used_ids:',used_ids(missing(Miss),toomuch(Res01),usedids(UIds),
1715 ignore(Ignore),real(Res1))),
1716 translate:print_bexpr(Expr),nl
1717 )
1718 ),
1719 Res=Res1.
1720 find_with_reuse(_,UIds,Ignore,Res) :-
1721 %(is_ordset(Ignore) -> true ; add_internal_error('Not ordset: ',Ignore)),
1722 ord_subtract(UIds,Ignore,Res).
1723
1724
1725 find_identifier_uses_top_level(TExpr,Ids) :-
1726 % get_global_identifiers(Ignored), % ignore all global sets and global constants;
1727 % hence find_identifier_uses_top_level/2 usually should only be called for top level expressions
1728 Ignored = [], % much more efficient to exclude afterwards for long lists of Ignored ids
1729 find_identifier_uses(TExpr,Ignored,Ids0),
1730 exclude_global_identifiers(Ids0,Ids).
1731
1732 :- use_module(tools,[safe_sort/3]).
1733 find_identifier_uses(TExpr,Ignored,Ids) :-
1734 %tools_printing:print_term_summary(find_identifier_uses(TExpr,Ignored,Ids)),nl,
1735 check_is_texpr(TExpr,find_identifier_uses),
1736 (find_typed_identifier_uses(TExpr,Ignored,TIds)
1737 -> get_texpr_ids(TIds,RIds),
1738 % in case of type errors, or when type checking is not yet complete, we can have multiple entries of the same identifier with different types !
1739 sort(RIds,Ids) % was remove_dups, but remove_dups just calls sort; TODO: implement get_sorted_texpr_ids
1740 ; add_internal_error('Call failed:',find_typed_identifier_uses(TExpr,Ignored,_)),
1741 Ids=[]
1742 ).
1743 find_identifier_uses_l(TExprs,Ignored,Ids) :-
1744 find_typed_identifier_uses_l(TExprs,Ignored,TIds),
1745 get_texpr_ids(TIds,RIds),
1746 sort(RIds,Ids). % see above
1747
1748 check_is_texpr(X,Context) :-
1749 (get_texpr_expr(X,_) -> true ; add_internal_error('Expected TExpr: ', check_is_texpr(X,Context))).
1750
1751 find_typed_identifier_uses(TExpr,Ids) :-
1752 % get_global_identifiers(Ignored), % ignore all global sets and global constants; hence find_typed_identifier_uses/2 usually should only be called for top level expressions
1753 Ignored = [],
1754 find_typed_identifier_uses(TExpr,Ignored,Ids0),
1755 exclude_global_identifiers(Ids0,Ids).
1756
1757 find_typed_identifier_uses(TExpr,Ignored,Ids) :- var(TExpr),!,
1758 add_internal_error('Variable typed expression: ', find_typed_identifier_uses(TExpr,Ignored,Ids)),
1759 Ids = [].
1760 find_typed_identifier_uses(TExpr,Ignored,Ids) :-
1761 find_typed_identifier_uses_l([TExpr],Ignored,Ids).
1762
1763 find_typed_identifier_uses2(TExpr,Ignored,Ids,Rest) :-
1764 get_texpr_expr(TExpr,Expr),
1765 safe_syntaxelement_det(Expr,Subs,TNames,_,_), % QSubs=[],
1766 ( uses_an_identifier(Expr,Id,TExpr,Ignored) ->
1767 ( ord_member(Id,Ignored) -> Ids=Rest
1768 ;
1769 get_texpr_type(TExpr,Type),
1770 normalize_type(Type,NType), % replace seq by set;
1771 % warning: when type-check not yet complete we have variables here
1772 create_texpr(identifier(Id),NType,[],TId),
1773 %print(adding(Id,NType,Ignored)),nl,
1774 Ids = [TId|Rest]
1775 )
1776 % ; (Expr = becomes_such(TIds,_)), nl,print(uses_primes(Expr)),nl,fail
1777 ; indirectly_uses_identifiers(Expr,Ignored,IndirectIds) ->
1778 add_typed_ids(IndirectIds,Ids,Rest2),
1779 find_typed_identifier_uses2_l(Subs,Ignored,Rest2,Rest)
1780 ; TNames = [] -> find_typed_identifier_uses2_l(Subs,Ignored,Ids,Rest)
1781 ;
1782 %find_typed_identifier_uses2_l(QSubs,Ignored,Ids,Ids2), % useless here as QSubs=[]
1783 get_texpr_ids(TNames,Names),
1784 list_to_ord_set(Names,SNames), ord_union(SNames,Ignored,Ignored2),
1785 find_typed_identifier_uses2_l(Subs,Ignored2,Ids,Rest)).
1786 find_typed_identifier_uses2_l([],_) --> !, [].
1787 find_typed_identifier_uses2_l([Expr|Rest],Ignored) --> !,
1788 find_typed_identifier_uses2(Expr,Ignored),
1789 find_typed_identifier_uses2_l(Rest,Ignored).
1790 find_typed_identifier_uses2_l(E,Ignored) -->
1791 {add_internal_error('Illegal arguments (not a list):',find_typed_identifier_uses2_l(E,Ignored)),fail}.
1792
1793 %Note: above we do not remap uses of Id$0 to Id in becomes_such;
1794 % this is done in find_read_vars_for_becomes_such in b_read_write_info
1795
1796
1797 uses_an_identifier(Expr,Id) :- uses_an_identifier(Expr,Id,none,[]).
1798
1799 uses_an_identifier(identifier(Id),Id,_,_).
1800 uses_an_identifier(lazy_lookup_pred(Id),Id,_,_).
1801 uses_an_identifier(lazy_lookup_expr(Id),Id,_,_).
1802 uses_an_identifier(value(_),Id,b(_,_,Info),Ignored) :- Ignored \= [],
1803 ? member(was_identifier(Id),Info),
1804 member('$examine_value_was_identifier_info',Ignored),!.
1805
1806 % uses multiple ids and we also need to inspect subs (operation call arguments)
1807 indirectly_uses_identifiers(operation_call_in_expr(Operation,_),Ignored,IndirectIds) :-
1808 get_texpr_info(Operation,Info),
1809 (memberchk(reads(Vars),Info)
1810 -> (var(Vars) % can happen during initial computation of read_write info for recursive operation calls in expr
1811 -> add_message(bsyntaxtree,'Operation reads info not yet computed (probably recursive call): ',Operation,Info),
1812 fail % Assume this is a direct recursive call which adds no used ids,
1813 % case happens in test 1960 for recursive call to Fact; TODO: more robust solution or disallow recursion
1814 ; true)
1815 ; add_warning(bsyntaxtree,'Operation call contains no read infos:',Operation,Info),fail),
1816 ord_subtract(Vars,Ignored,IndirectIds),
1817 IndirectIds \= [].
1818 %indirectly_uses_identifiers(external_pred_call(FunName,_),Ignored,IndirectIds) :-
1819 % expects_state(FunName), TODO: check for which external functions/predicates we need to add ids
1820
1821
1822 % this is to convert untyped ids in operation call reads infos to typed ids
1823 add_typed_ids([]) --> [].
1824 add_typed_ids([Id|T]) --> {var_cst_type(Id,Type)},!,
1825 {create_texpr(identifier(Id),Type,[],TId)}, [TId], add_typed_ids(T).
1826 add_typed_ids([Id|T]) --> {debug_println(19,ignoring_used_id(Id))}, add_typed_ids(T).
1827
1828 :- use_module(bmachine,[bmachine_is_precompiled/0, b_is_variable/2,b_is_constant/2]).
1829 var_cst_type(Name,Type) :- bmachine_is_precompiled,!,
1830 (b_is_variable(Name,Type) ; b_is_constant(Name,Type)),!.
1831 var_cst_type(_,any). % TODO: provide a better solution; maybe only allow untyped find_identifier_uses ??
1832
1833 % -------------
1834
1835 find_typed_identifier_uses_l(TExprs,Ignored,Ids) :-
1836 check_atomic_ids(Ignored),
1837 list_to_ord_set(Ignored,SIgnored),
1838 find_typed_identifier_uses2_l(TExprs,SIgnored,Unsorted,[]),!,
1839 safe_sort(find_typed_identifier_uses,Unsorted,Ids),
1840 (preference(prob_safe_mode,true) -> check_typed_ids(Ids) ; true).
1841 find_typed_identifier_uses_l(TExprs,Ignored,Ids) :-
1842 add_internal_error('Call failed:',find_typed_identifier_uses_l(TExprs,Ignored,Ids)),
1843 fail.
1844
1845 check_typed_ids([]) :- !.
1846 check_typed_ids([b(identifier(ID),T,_)|Tail]) :- !, check_ids3(Tail,ID,T).
1847 check_typed_ids(Other) :- add_internal_error('Unexpected typed id list:',check_typed_ids(Other)).
1848
1849
1850 check_atomic_ids([]) :- !.
1851 check_atomic_ids([Id|_]) :- atomic(Id),!.
1852 check_atomic_ids(Other) :- add_internal_error('Expected atomic id list:',check_atomic_ids(Other)).
1853
1854
1855 check_ids3([],_,_) :- !.
1856 check_ids3([b(identifier(ID),T,_)|Tail],ID1,T1) :- !,
1857 (ID=ID1 -> add_internal_error('Identifier appears multiple times with types:',id(ID,T1,T)) ; true),
1858 check_ids3(Tail,ID,T).
1859 check_ids3(Other,ID1,T1) :- add_internal_error('Unexpected typed id list:',check_ids3(Other,ID1,T1)).
1860
1861
1862 update_used_ids(b(Pred,T,OInfo),UsedIds,b(Pred,T,[used_ids(UsedIds)|NInfo])) :-
1863 delete(OInfo,used_ids(_),NInfo).
1864
1865 % check if some pre-computed used ids are valid wrt find_typed_identifier_uses
1866 check_computed_used_ids(TExpr,CompUsedIds) :-
1867 find_identifier_uses(TExpr,[],RealUsedIds),
1868 (RealUsedIds=CompUsedIds -> print(ok(CompUsedIds)),nl
1869 ; add_error(range,'Unexpected used ids:',CompUsedIds,TExpr),
1870 format('Real: ~w~nComp: ~w~n',[RealUsedIds,CompUsedIds]),trace
1871 ).
1872
1873 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1874 % break predicate into components with disjunct identifiers
1875 % Pred: a predicate
1876 % Components: a list of terms component/2 where the first argument
1877 % is a predicate, the second is the set of used identifiers
1878 predicate_components(Pred,Res) :- predicate_components_in_scope(Pred,[],Res).
1879 predicate_components_in_scope(Pred,LocalVars,Res) :-
1880 predicate_components_with_restriction(Pred,LocalVars,all,Res).
1881
1882 predicate_components_with_restriction(Pred,LocalVars,RestrictionList,Res) :-
1883 conjunction_to_list(Pred,Preds),
1884 l_predicate_identifiers(Preds,LocalVars,PredIds),
1885 (RestrictionList=all -> R=all ; list_to_ord_set(RestrictionList,R)),
1886 try_find_and_remove_equalities(PredIds,PredIds2),
1887 % print(find_components(R)),nl,nl,
1888 %%(member(pred(P,Ids,X),PredIds2), nl,print(pred(Ids,X)),nl,translate:print_bexpr(P),nl,fail ; true),
1889 find_components(PredIds2,R,Components),
1890 !,
1891 %maplist(print_component,Components),
1892 Components=Res.
1893 predicate_components_with_restriction(Pred,_,_,[component(Pred,[])]) :-
1894 add_internal_error('predicate_components failed: ',predicate_components_with_restriction(Pred,_,_,_)).
1895
1896 % print_component(component(Pred,Ids)) :- format('Component over ~w :~n',[Ids]), translate:print_bexpr(Pred),nl.
1897
1898 % get the list of used identifiers for each predicate
1899 l_predicate_identifiers([],_LocalVars,[]).
1900 l_predicate_identifiers([Pred|PRest],LocalVars,[pred(Pred,Ids,_Selected)|IRest]) :-
1901 predicate_identifiers_in_scope(Pred,LocalVars,Ids), % Do not ignore local variables; used instead of enumerate set elements
1902 l_predicate_identifiers(PRest,LocalVars,IRest).
1903
1904
1905 try_find_and_remove_equalities(PredAndIds,PredAndIds2) :-
1906 preferences:get_preference(partition_predicates_inline_equalities,true),
1907 \+ preferences:get_preference(use_solver_on_load,kodkod),
1908 ? find_and_remove_equalities(PredAndIds,RR),
1909 !, PredAndIds2=RR.
1910 try_find_and_remove_equalities(Ps,Ps).
1911
1912 :- use_module(debug,[debug_println/2]).
1913 % find and apply obvious equalities so that they do not interfere with partitioning into components
1914 % example: c = 1 & f: 1..c --> A & g: 1..c --> B
1915 % TO DO: preprocess and do one pass to detect potential equalities
1916 find_and_remove_equalities([],[]).
1917 find_and_remove_equalities(List,[pred(P,PIds,Sel)|FT]) :-
1918 ? select(pred(P,PIds,Sel),List,Rest),
1919 %PIds = [Id],
1920 identifier_equality(P,Id,Value),
1921 %(value_which_can_be_replaced(Value) -> true ; nl,print('Not replaced: '),translate:print_bexpr(Value),nl,fail),
1922 (get_texpr_id(Value,Id2)
1923 -> Id2 \= Id %,print(inline_id(Id,Id2)),nl
1924 % Note: this inlining does *not* help with partitioning; but does help ProB detect common predicates/expressions
1925 ; PIds=[Id],value_which_can_be_replaced(Value)),
1926 debug_println(9,replace_simple_equality(Id,PIds)),
1927 ? maplist(apply_to_pred(Id,Value),Rest,RT),
1928 !,
1929 ? find_and_remove_equalities(RT,FT).
1930 % TO DO: detect equalityes x = EXPR, where EXPR does not contain x and where x occurs in no other predicate
1931 % we can then annotate x as not to enumerate
1932 find_and_remove_equalities(R,R).
1933
1934 identifier_equality(b(equal(LHS,RHS),_,_),Id,EqTerm) :-
1935 (get_texpr_id(LHS,Id) -> EqTerm = RHS
1936 ; get_texpr_id(RHS,Id) -> EqTerm = LHS).
1937 % TO DO: should we detect other equalities?
1938
1939 value_which_can_be_replaced(b(E,T,_)) :- value_which_can_be_replaced2(E,T).
1940 %(value_which_can_be_replaced2(E,T) -> true ; print(not_val(E)),nl,fail).
1941 value_which_can_be_replaced2(value(_),_).
1942 value_which_can_be_replaced2(integer(_),_).
1943 %value_which_can_be_replaced2(identifier(I),global(G)) :- b_global_constant(G), id_not_used_anywhere(I).
1944 value_which_can_be_replaced2(integer_set(_),_).
1945 value_which_can_be_replaced2(unary_minus(A),_) :- value_which_can_be_replaced(A).
1946 value_which_can_be_replaced2(add(A,B),_) :- value_which_can_be_replaced(A), value_which_can_be_replaced(B).
1947 % we could compute the value
1948 value_which_can_be_replaced2(minus(A,B),_) :- value_which_can_be_replaced(A), value_which_can_be_replaced(B).
1949 value_which_can_be_replaced2(multiplication(A,B),_) :- value_which_can_be_replaced(A), value_which_can_be_replaced(B).
1950 value_which_can_be_replaced2(div(A,B),_) :-
1951 get_integer(B,IB), IB \= 0,
1952 value_which_can_be_replaced(A).
1953 value_which_can_be_replaced2(floored_div(A,B),T) :- value_which_can_be_replaced2(div(A,B),T).
1954 % should we add: with WD check: division, modulo, .... ? see also simple2 in b_ast_cleanup
1955 value_which_can_be_replaced2(max_int,_).
1956 value_which_can_be_replaced2(min_int,_).
1957 value_which_can_be_replaced2(float_set,_).
1958 value_which_can_be_replaced2(real(_),_).
1959 value_which_can_be_replaced2(real_set,_).
1960 value_which_can_be_replaced2(string(_),_).
1961 value_which_can_be_replaced2(string_set,_).
1962 value_which_can_be_replaced2(boolean_true,_).
1963 value_which_can_be_replaced2(boolean_false,_).
1964 value_which_can_be_replaced2(bool_set,_).
1965 value_which_can_be_replaced2(empty_set,_).
1966 value_which_can_be_replaced2(empty_sequence,_).
1967 value_which_can_be_replaced2(couple(A,B),_) :- value_which_can_be_replaced(A), value_which_can_be_replaced(B).
1968 value_which_can_be_replaced2(interval(A,B),_) :- value_which_can_be_replaced(A), value_which_can_be_replaced(B).
1969 value_which_can_be_replaced2(set_extension(L),_) :- maplist(value_which_can_be_replaced,L).
1970 value_which_can_be_replaced2(sequence_extension(L),_) :- maplist(value_which_can_be_replaced,L).
1971 value_which_can_be_replaced2(cartesian_product(A,B),_) :- % typing equations, like t_float = INTEGER*NATURAL1
1972 simple_value_set(A), simple_value_set(B).
1973 value_which_can_be_replaced2(pow_subset(A),_) :- simple_value_set(A).
1974 %value_which_can_be_replaced2(identifier(_),_). % TO DO: check that this is not the LHS identifier which we replace !!
1975 % identifiers can also be replaced: we check above that the only identifier in the predicate is the equality identifier
1976 % TO DO: enable this but then we need to fix replace_id_by_expr2 to updated the used_ids info ! + we can have scoping issues !?; see test 1358
1977
1978 % TO DO: also allow inlining of prj1/prj2 of simple_value_set:
1979 % not_val(comprehension_set([b(identifier(_zzzz_unary),integer,[generated(first)]),b(identifier(_zzzz_binary),integer,[generated(first)]),b(identifier(_lambda_result_),integer,[lambda_result])],b(equal(b(identifier(_lambda_result_),integer,[lambda_result]),b(identifier(_zzzz_unary),integer,[generated(first)])),pred,[prob_annotation(LAMBDA),lambda_result])))
1980 % not_val(comprehension_set([b(identifier(_zzzz_unary),integer,[generated(second)]),b(identifier(_zzzz_binary),integer,[generated(second)]),b(identifier(_lambda_result_),integer,[lambda_result])],b(equal(b(identifier(_lambda_result_),integer,[lambda_result]),b(identifier(_zzzz_binary),integer,[generated(second)])),pred,[prob_annotation(LAMBDA),lambda_result])))
1981
1982 % TO DO: maybe check if it is an infinite type which cannot be evaluated anyway
1983 simple_value_set(b(E,_,_)) :- simple_value_set2(E).
1984 %simple_value_set2(bool_set). % Warning: we could have a finite construct which gets evaluated multiple times
1985 simple_value_set2(string_set).
1986 simple_value_set2(integer_set(_)).
1987 simple_value_set2(float_set).
1988 simple_value_set2(real_set).
1989 simple_value_set2(cartesian_product(A,B)) :- simple_value_set(A), simple_value_set(B).
1990 simple_value_set2(pow_subset(A)) :- simple_value_set(A).
1991 % POW, records struct(_) set ?
1992
1993 % apply a substiution of ID/Expr on a pred(EXPR,VarList,X) term
1994 % Expr must either be a variable or contain no variables at all
1995 apply_to_pred(ID,Expr,pred(E1,PIds1,X),pred(E2,PIds3,X)) :-
1996 ? (select(ID,PIds1,PIds2)
1997 ? -> replace_id_by_expr(E1,ID,Expr,E2), %,print(applied(ID)),nl,translate:print_bexpr(E2),nl
1998 % TO DO: replace_id_by_expr does not seem to update used_ids info !! check_used_ids_info fails for test 1358 if we allow identifiers inside Expr
1999 (get_texpr_id(Expr,NewID)
2000 -> ord_add_element(PIds2,NewID,PIds3)
2001 ; PIds3 = PIds2)
2002 %, format('Apply ~w -> ~w : ',[ID,NewID]),translate:print_bexpr(E2),nl
2003 ; E1=E2,PIds1=PIds3).
2004
2005
2006 % project a predicate : keep only those Predicates that are directly or
2007 % indirectly relevant for Ids; FullIds are all identifiers used by ProjectedPredicate
2008 project_predicate_on_identifiers(Pred,Ids,ProjectedPredicate,FullIds, RestList) :-
2009 (debug_mode(on)
2010 -> print('project: '),print_bexpr(Pred),nl, print(' on : '), print(Ids),nl
2011 ; true),
2012 conjunction_to_list(Pred,Preds),
2013 l_predicate_identifiers(Preds,[],PredIds), % TO DO: allow LocalVariables to be passed
2014 % print(predids(PredIds)),nl,
2015 try_find_and_remove_equalities(PredIds,PredIds2),
2016 extract_all_predicates(Ids,all,Ids,PredIds2,ProjectedPredicates, RestList,FullIds),
2017 conjunct_predicates(ProjectedPredicates,ProjectedPredicate),
2018 (debug_mode(on)
2019 -> print('*result: '),print_bexpr(ProjectedPredicate),nl,
2020 print(' on : '), print(FullIds),nl
2021 ; true).
2022
2023 %print_preds([]).
2024 %print_preds([pred(P,_IDs,_)|T]) :- translate:print_bexpr(P), nl, print(' '), print_preds(T).
2025
2026 :- use_module(b_global_sets,[b_get_global_constants/1, b_get_enumerated_set_constants/1,
2027 b_get_global_sets/1, exclude_global_identifiers/2, exclude_global_identifiers/3]).
2028 predicate_identifiers(Pred,Ids) :- predicate_identifiers_in_scope(Pred,[],Ids).
2029 predicate_identifiers_in_scope(Pred,LocalVariables,Ids) :-
2030 %get_global_identifiers(IS),
2031 list_to_ord_set(LocalVariables,LV),
2032 %ord_subtract(IS,LV,Ignore2), % Do not ignore any local variable; it will be used instead of enumerate set element
2033 find_identifier_uses_if_necessary(Pred,[],Ids1), % Ignore enumerated set names
2034 exclude_global_identifiers(Ids1,LV,Ids2),
2035 list_to_ord_set(Ids2,Ids).
2036
2037 % see also b_global_constant_or_set_identifier and exclude_global_identifiers
2038 get_global_identifiers(IDs) :- get_global_identifiers(IDs,all).
2039 % get global set and constant identifiers which you usually want to exclude for find_identifier_uses
2040 get_global_identifiers(IDs,Option) :-
2041 (Option=ignore_promoted_constants
2042 % do not include those constants that have been automatically promoted as enumerated set elements
2043 -> b_get_enumerated_set_constants(EnumeratedSetCsts)
2044 ; b_get_global_constants(EnumeratedSetCsts)
2045 ),
2046 % b_global_sets:b_get_global_enumerated_sets(GSets), % is there a reason to exclude deferred sets ??; cardinality inference,... are all done before partitioning ?
2047 b_get_global_sets(GSets),
2048 append(GSets,EnumeratedSetCsts,GE),
2049 list_to_ord_set(GE,IDs).
2050
2051 % find_components(ListOf_pred, Restrict, Out:ListOfComponents)
2052 % role of Restrict: all if we do normal partition or List of VariableIDs on which we restrict our attention to (for Existential quantifier construction)
2053 find_components([],_,[]).
2054 find_components([pred(P,PIds,true)|PRest],Restrict,[component(Pred,Ids)|CRest]) :-
2055 % find all predicates which are using identifiers occuring in PIds
2056 % (and additionally those which use common identifiers )
2057 ord_restrict(Restrict,PIds,InterIDs),
2058 %format('Treating predicate with ids ~w; restr. intersect = ~w~n',[PIds,InterIDs]),
2059 ( InterIDs =[] ->
2060 % we simply copy this predicate into a single component; not with the scope of Restricted IDs
2061 % print(skip(PIds,P)),nl, %
2062 Pred=P, Ids=PIds, PRest=Rest
2063 ;
2064 extract_all_predicates(InterIDs,Restrict,PIds,PRest,Preds,Rest,Ids),
2065 %length([P|Preds],Len), format('Detected component with ~w conjuncts over ~w~n',[Len,Ids]),
2066 conjunct_predicates_with_pos_info([P|Preds],Pred)
2067 ),
2068 find_components(Rest,Restrict,CRest).
2069 extract_all_predicates([],_,_,Preds,Found,Rest,[]) :- !, % selecting done at end: keep same order of conjuncts
2070 select_predicates(Preds,Found,Rest).
2071 extract_all_predicates(Ids,Restrict,OldIds,Preds,Found,Rest,ResultIds) :-
2072 % search for all predicates that directly use one of the
2073 % identifiers in "Ids"
2074 select_all_using_preds(Preds,Ids,FoundIds),
2075 ord_subtract(FoundIds,OldIds,NewIds),
2076 ord_restrict(Restrict,NewIds,NewIdsToExtract),
2077 ord_union(OldIds,FoundIds,OldIds2),
2078 % now recursively do this which the new identifiers that we have found
2079 extract_all_predicates(NewIdsToExtract,Restrict,OldIds2,Preds,Found,Rest,RestIds),
2080 ord_union([Ids,NewIds,RestIds],ResultIds).
2081
2082 % mark all predicates which intersect with ComponentIds and compute new ids to be added to the component
2083 select_all_using_preds([],_,[]).
2084 select_all_using_preds([pred(_P,PIds,Selected)|PRest],ComponentIds,NewFoundIds) :-
2085 ( (Selected==true ; ord_disjoint(PIds,ComponentIds)) ->
2086 NewFoundIds1 = []
2087 ; % we select the predicate for the component
2088 ord_subtract(PIds,ComponentIds,NewFoundIds1),
2089 Selected=true
2090 ),
2091 select_all_using_preds(PRest,ComponentIds,NewFoundIds2),
2092 ord_union(NewFoundIds1,NewFoundIds2,NewFoundIds).
2093
2094 % ord_intersection with special case for all term
2095 ord_restrict(all,Ids,Res) :- !, Res=Ids.
2096 ord_restrict(Restrict,Ids,Res) :- ord_intersection(Ids,Restrict,Res).
2097
2098 select_predicates(Predicates,FoundPreds,OtherPreds) :-
2099 split_list(is_selected_predicate,Predicates,FoundPredIds,OtherPreds),
2100 maplist(extract_found_predicate,FoundPredIds,FoundPreds).
2101 is_selected_predicate(pred(_P,_PIds,Selected)) :- ground(Selected).
2102 extract_found_predicate(pred(P,_PIds,_Selected),P).
2103
2104 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2105 % replace (simultaneously) multiple identifiers by expressions
2106 % this could be used to replace the predicate replace_id_by_expr by mapping everything in a
2107 % singleton list. however, that would involve list operations instead of unifications
2108 parse_pred(Codes,TExpr) :- %format('Parsing ~s~n',[Codes]),
2109 bmachine:b_parse_machine_predicate_from_codes_open(no_quantifier,Codes,[],[],TExpr).
2110 parse_expr(Codes,TExpr) :- bmachine:b_parse_machine_expression_from_codes(Codes,[],TExpr,_Type,true,_Error).
2111 test_result(1,b(equal(b(comprehension_set([b(identifier(__FRESH____),integer,_)],
2112 b(greater(b(identifier(__FRESH____2),integer,_),b(identifier(x),integer,_)),pred,_)),set(integer),_),
2113 b(empty_set,set(integer),_)),pred,_)).
2114
2115 :- assert_must_succeed((bsyntaxtree:parse_pred("{x|x:INTEGER & x>y}={}",T1), replace_ids_by_exprs(T1,[],[],T1))).
2116 :- assert_must_succeed((bsyntaxtree:parse_pred("{x|x:INTEGER & x>y}={}",T1), bsyntaxtree:parse_expr("100",T2),
2117 replace_ids_by_exprs(T1,[y],[T2],R),bsyntaxtree:parse_pred("{x|x>100}={}",T3),same_texpr(R,T3) )).
2118 :- assert_must_succeed((bsyntaxtree:parse_pred("{x|x:INTEGER & x>y}={}",T1),
2119 replace_ids_by_exprs(T1,[y],[b(identifier(x),integer,[])],R),
2120 bsyntaxtree:test_result(1,R),bsyntaxtree:parse_pred("{x|x:INTEGER & x>x}={}",T3),\+ same_texpr(R,T3) )).
2121 :- assert_must_succeed((bsyntaxtree:parse_pred("{x,y|x:INTEGER & y:INTEGER & x>v & y>w}={}",T1),
2122 replace_ids_by_exprs(T1,[v,w],[b(identifier(w),integer,[]),b(identifier(v),integer,[])],R),
2123 bsyntaxtree:parse_pred("{x,y|x:INTEGER & y:INTEGER & x>w & y>v}={}",T3), same_texpr(R,T3) )).
2124 :- assert_must_succeed((gensym:reset_gensym, bsyntaxtree:parse_pred("{x,y|x:INTEGER & y:INTEGER & x>v & y>w}={}",T1),
2125 replace_ids_by_exprs(T1,[v,w],[b(identifier(w),integer,[]),b(identifier(x),integer,[])],R),
2126 translate:translate_bexpression(R,TR),
2127 TR = '{`__FRESH____1`,y|`__FRESH____1` > w & y > x} = {}')). %'{__FRESH____1,y|(__FRESH____1 : INTEGER & y : INTEGER) & (__FRESH____1 > w & y > x)} = {}' )).
2128
2129 replace_ids_by_exprs(TExpr,[TId],[Inserted],Replaced) :- !, % better, more robust and efficient version
2130 check_ids([TId],[Id]),
2131 ? replace_id_by_expr(TExpr,Id,Inserted,Replaced).
2132 replace_ids_by_exprs(TExpr,[],[],Replaced) :- !, Replaced=TExpr. % Nothing to do
2133 replace_ids_by_exprs(TExpr,Ids,Exprs,Replaced) :-
2134 check_ids(Ids,Ids2), % convert to atomic identifiers
2135 find_identifier_uses_l(Exprs,[],ExprsUsedIds),
2136 sort(ExprsUsedIds,SExprsUsedIds),
2137 generate_rename_list(Ids2,Exprs,RenameList),
2138 %print(replace(RenameList,SExprsUsedIds)),nl,
2139 replace_ids_by_exprs2(RenameList,SExprsUsedIds,TExpr,Replaced,_). %, nl,print(done),nl.
2140 % a version of replace_ids_by_exprs2 for maplist:
2141 %replace_ids_by_exprs1(RenameList,SExprsUsedIds,TExpr,Replaced) :-
2142 % replace_ids_by_exprs2(RenameList,SExprsUsedIds,TExpr,Replaced,_). %, print('Rep: '), translate:print_bexpr(Replaced),nl.
2143
2144 generate_rename_list([],[],[]).
2145 generate_rename_list([ID1|T],[Expr1|TE],[rename(ID1,Expr1)|RT]) :- generate_rename_list(T,TE,RT).
2146
2147 check_ids([],[]).
2148 check_ids([H|T],[ID|IT]) :- (atomic(H) -> ID=H ; def_get_texpr_id(H,ID)), check_ids(T,IT).
2149 replace_ids_by_exprs2(RenameList,ExprsUsedIds,TExpr,Replaced,WDC) :-
2150 remove_bt(TExpr,Expr,NewExpr,TNewExpr),
2151 ? ( Expr = identifier(Id), member(rename(Id,Inserted),RenameList) ->
2152 Replaced = Inserted,
2153 get_texpr_info(Inserted,Infos),
2154 (memberchk(contains_wd_condition,Infos)
2155 -> WDC = true ; WDC = false) % WDC = true means we have added a wd-condition where previously there was none
2156 ; contains_no_ids(Expr) -> Replaced=TExpr, WDC=false
2157 ;
2158 syntaxtransformation_det(Expr,Subs1,Names,NSubs,NewExpr),
2159 find_variable_clashes(Names,ExprsUsedIds,RenameNames), % check for variable caputure
2160 (RenameNames = []
2161 -> Subs = Subs1 % no variable capture occured
2162 ; %format('*** VARIABLE CAPTURE : ~w~n~n',[RenameNames]),
2163 rename_bt_l(Subs1,RenameNames,Subs) % replace affected names by fresh ids in sub arguments (will also change list of quantified variables itself)
2164 ),
2165 %l_replace_ids_by_exprs2(QSubs,RenameList,ExprsUsedIds,NQSubs,WDC1), % QSubs are like RHS of let expression, where Names are not in scope
2166 remove_hidden_names(Names,RenameList,UpdatedRenameList),
2167 ( UpdatedRenameList = [] -> % all Ids are now hidden for the inner expressions
2168 NSubs=Subs, WDC=false
2169 ;
2170 l_replace_ids_by_exprs2(Subs,UpdatedRenameList,ExprsUsedIds,NSubs,WDC)
2171 ),
2172 TNewExpr = b(E1,T1,Info1),
2173 rename_update_used_ids_info(RenameList,Info1,Info2),
2174 add_wd_if_needed(WDC,b(E1,T1,Info2),Replaced)
2175 ).
2176
2177 contains_no_ids(integer(_)).
2178 contains_no_ids(string(_)).
2179 contains_no_ids(value(_)).
2180
2181
2182 % check if we have to rename any quantified variable to avoid variable capture of RHS of renamings
2183 % example, suppose we rename x/y+1 and we enter {y|y>x} we have to generate {fresh|fresh>y+1} and *not* {y|y>y+1}
2184 find_variable_clashes([],_,[]).
2185 find_variable_clashes([Name|Names],ExprsUsedIds,[rename(ID,FRESHID)|Renaming] ) :-
2186 def_get_texpr_id(Name,ID),
2187 ord_member(ID,ExprsUsedIds), % the quantified name is also introduced by the renaming
2188 !,
2189 gensym('__FRESH__',FRESHID),
2190 find_variable_clashes(Names,ExprsUsedIds,Renaming).
2191 find_variable_clashes([_|Names],ExprsUsedIds,Renaming) :-
2192 find_variable_clashes(Names,ExprsUsedIds,Renaming).
2193
2194
2195 l_replace_ids_by_exprs2([],_,_,[],false).
2196 l_replace_ids_by_exprs2([H|T],UpdatedRenameList,ExprsUsedIds,[IH|IT],WDC) :-
2197 replace_ids_by_exprs2(UpdatedRenameList,ExprsUsedIds,H,IH,WDC1),
2198 l_replace_ids_by_exprs2(T,UpdatedRenameList,ExprsUsedIds,IT,WDC2),
2199 and_wdc(WDC1,WDC2,WDC).
2200
2201 % remove any identifiers that are now "invisible" because they are masked by quantified names
2202 % e.g., when we enter #x.(P) then a renaming of x will be "hidden" inside P
2203 remove_hidden_names([],RenameList,RenameList).
2204 remove_hidden_names([Name|Names],RenameList,NewRenameList) :-
2205 def_get_texpr_id(Name,ID),
2206 delete(RenameList,rename(ID,_),RenameList1),
2207 !, % only one rename should exist
2208 %print(del(ID,RenameList1)),nl,
2209 remove_hidden_names(Names,RenameList1,NewRenameList).
2210
2211 find_rhs_ids(rename(Id,TExpr),rename_ids(Id,InsUsedIds)) :- find_identifier_uses(TExpr,[],InsUsedIds).
2212
2213 % apply a rename list to the used_ids,... information fields
2214 % this is more tricky than applying a single identifier, as we first have to deleted all ids
2215 % and remember which ones were deleted, and only then insert the corresponding ids
2216 % e.g., we could have a RenameList = [rename(p,q),rename(q,p)] ; see test 1776 M1_Internal_v3.mch
2217 rename_update_used_ids_info(RenameList,IIn,IOut) :-
2218 l_find_rhs_ids(RenameList,RenameList2),
2219 %maplist(apply_rename_list(RenameList2),IIn,IOut).
2220 l_apply_rename_list(IIn,RenameList2,IOut).
2221
2222 l_find_rhs_ids([],[]).
2223 l_find_rhs_ids([R1|T],[NR1|NTR]) :-
2224 find_rhs_ids(R1,NR1),
2225 l_find_rhs_ids(T,NTR).
2226
2227 l_apply_rename_list([],_,[]).
2228 l_apply_rename_list([Info1|T],RenameList2,[NewInfo1|NTI]) :-
2229 apply_rename_list(RenameList2,Info1,NewInfo1),
2230 l_apply_rename_list(T,RenameList2,NTI).
2231
2232 apply_rename_list(RenameList,I,NI) :-
2233 apply_rename_list2(I,RenameList,NI).
2234 apply_rename_list2(used_ids(IDS),RenameList,used_ids(NewIDS)) :- !, apply_rename_list_to_ids(RenameList,IDS,[],NewIDS).
2235 apply_rename_list2(reads(IDS),RenameList,reads(NewIDS)) :- !, apply_rename_list_to_ids(RenameList,IDS,[],NewIDS).
2236 apply_rename_list2(modifies(IDS),RenameList,modifies(NewIDS)) :- !, apply_rename_list_to_ids(RenameList,IDS,[],NewIDS).
2237 apply_rename_list2(Info,_,Info).
2238
2239 % apply a rename list to a sorted list of ids
2240 apply_rename_list_to_ids([],Acc,ToInsert,Res) :- ord_union(Acc,ToInsert,Res).
2241 apply_rename_list_to_ids([rename_ids(Id,NewIds)|T],Acc,ToInsert,Res) :-
2242 (ord_delete_existing_element(Acc,Id,Acc2) % the Id occurs and is deleted
2243 -> ord_union(NewIds,ToInsert,ToInsert2),
2244 apply_rename_list_to_ids(T,Acc2,ToInsert2,Res)
2245 ; apply_rename_list_to_ids(T,Acc,ToInsert,Res)).
2246
2247 ord_delete_existing_element(List,El,ResList) :- % ord_del_element also succeeds if El is not in the list !
2248 ord_intersection([El],List,[El],ResList).
2249 % -----------------------
2250 % remove an Identifier from used_ids Info field if it exists
2251 remove_used_id_from_info(I,ID_to_remove,NI) :-
2252 update_used_ids_info(I,ID_to_remove,[],NI).
2253
2254 remove_used_ids_from_info([],I,I).
2255 remove_used_ids_from_info([ID_to_remove|T],I,NI) :- remove_used_id_from_info(I,ID_to_remove,I2),
2256 remove_used_ids_from_info(T,I2,NI).
2257
2258 % remove a single Identifier from used_ids Info field if it exists and insert sorted list of ids instead
2259 % a simpler version of rename_update_used_ids_info for a single identifier
2260 update_used_ids_info([],_,_,[]).
2261 update_used_ids_info([InfoField|T],ID_to_remove,IDsInserted,[NewInfoField|NT]) :-
2262 (update_id_from_info_field(ID_to_remove,IDsInserted,InfoField,R)
2263 -> NewInfoField=R
2264 ; NewInfoField=InfoField),
2265 update_used_ids_info(T,ID_to_remove,IDsInserted,NT).
2266
2267 update_id_from_info_field(ID_to_remove,IDsInserted,I,NI) :-
2268 update_id_from_info_field2(I,ID_to_remove,IDsInserted,NI).
2269 update_id_from_info_field2(used_ids(IDS),ID,IDsInserted,used_ids(NewIDS)) :- update_id(IDS,ID,IDsInserted,NewIDS).
2270 update_id_from_info_field2(reads(IDS),ID,IDsInserted,reads(NewIDS)) :- update_id(IDS,ID,IDsInserted,NewIDS).
2271 update_id_from_info_field2(modifies(IDS),ID,IDsInserted,modifies(NewIDS)) :- update_id(IDS,ID,IDsInserted,NewIDS).
2272
2273 update_id(IDS,ID_to_remove,IDsInserted,NewIDS) :-
2274 ord_delete_existing_element(IDS,ID_to_remove,IDS2), % the Id occurs and is deleted
2275 ord_union(IDsInserted,IDS2,NewIDS).
2276 %if ord_del_element fails we do not add IDsInserted: we assume the used_ids info is correct and ID_to_remove does not occur !
2277 % We could use this info to avoid traversing subtree !
2278 % print(projecting_away_unknown_id(ID_to_remove,IDS)),nl,
2279
2280 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2281
2282 :- assert_must_succeed((gensym:reset_gensym, bsyntaxtree:exists_ast(A), replace_id_by_expr(A,y,b(identifier(x),integer,[]),RA),translate:translate_bexpression(RA,TR),
2283 TR = 'r = {`__FRESH____1`|`__FRESH____1` : 1 .. x & `__FRESH____1` mod 2 = 1}' )).
2284 :- assert_must_succeed((bsyntaxtree:parse_pred("{x|x:INTEGER & x>y}={}",T1),
2285 replace_id_by_expr(T1,y,b(identifier(x),integer,[]),R),
2286 bsyntaxtree:test_result(1,R),bsyntaxtree:parse_pred("{x|x:INTEGER & x>x}={}",T3),
2287 \+ same_texpr(R,T3) )).
2288 :- assert_must_succeed((bsyntaxtree:parse_pred("{x|x:INTEGER & x>y}={}",T1), bsyntaxtree:parse_expr("100",T2),
2289 replace_id_by_expr(T1,y,T2,R),bsyntaxtree:parse_pred("{x|x>100}={}",T3),same_texpr(R,T3) )).
2290
2291 % replace an identifier Id by an expression Inserted
2292 replace_id_by_expr(TExpr,Id,Inserted,Replaced) :-
2293 ? replace_id_by_expr_with_count(TExpr,Id,Inserted,Replaced,_).
2294
2295 replace_id_by_expr_with_count(TExpr,Id,Inserted,Replaced,NrReplacements) :- \+ atomic(Id),!,
2296 add_internal_error('Id not atomic: ',replace_id_by_expr(TExpr,Id,Inserted,Replaced)),
2297 Replaced = TExpr, NrReplacements=0.
2298 replace_id_by_expr_with_count(TExpr,Id,Inserted,Replaced,NrReplacements) :-
2299 %find_all_relevant_quantified_vars(Id,TExpr,QVars),
2300 find_identifier_uses(Inserted,[],SInsUsedIds), % SInsUsedIds is sorted
2301 ? replace_id_by_expr2(Id,Inserted,SInsUsedIds,TExpr,Replaced,_WDC,0,NrReplacements).
2302
2303 replace_id_by_expr2(Id,Inserted,InsUsedIds,TExpr,Replaced,WDC,InR,OutR) :-
2304 remove_bt(TExpr,Expr,NewExpr,TNewExpr),
2305 ( Expr = identifier(Id) -> % TODO: count number of replacements
2306 Replaced = Inserted,
2307 OutR is InR+1,
2308 get_texpr_info(Inserted,Infos),
2309 (memberchk(contains_wd_condition,Infos)
2310 -> WDC = true ; WDC = false) % WDC = true means we have added a wd-condition where previously there was none
2311 ; contains_no_ids(Expr) -> Replaced=TExpr, WDC=false, OutR=InR
2312 ;
2313 ? syntaxtransformation_det(Expr,Subs,Names,NSubs,NewExpr),
2314 get_texpr_id(TId,Id),
2315 ( memberchk(TId,Names) -> % the Id is now hidden for the inner expressions
2316 NSubs=Subs, WDC=false, OutR = InR
2317 ; (InsUsedIds \= [],
2318 get_texpr_ids(Names,Ns),sort(Ns,SNs),
2319 ord_intersection(SNs,InsUsedIds,Captured),
2320 Captured \= [] %, print(inter(SNs,InsUsedIds,Captured)),nl
2321 )
2322 % The Names introduced clash with variables used in the Inserted expression
2323 -> findall(rename(X,FRESHID),(member(X,Captured),gensym:gensym('__FRESH__',FRESHID)),RenameList),
2324 %print(rename(RenameList)),nl,
2325 rename_bt_l(Subs,RenameList,RenSubs),
2326 l_replace_id_by_expr2(RenSubs,Id,Inserted,InsUsedIds,NSubs,WDC,InR,OutR)
2327 ;
2328 ? l_replace_id_by_expr2(Subs,Id,Inserted,InsUsedIds,NSubs,WDC,InR,OutR)
2329 ),
2330 TNewExpr = b(E1,T1,Info1),
2331 update_used_ids_info(Info1,Id,InsUsedIds,Info2),
2332 %(E1 = exists(P,_) -> print(exists(P,Id,Info1,Info2)),nl ; true),
2333 add_wd_if_needed(WDC,b(E1,T1,Info2),Replaced)
2334 ).
2335
2336 l_replace_id_by_expr2([],_,_,_,[],false,R,R).
2337 l_replace_id_by_expr2([H|T],Id,Inserted,InsUsedIds,[IH|IT],WDC,InR,OutR) :-
2338 ? replace_id_by_expr2(Id,Inserted,InsUsedIds,H,IH,WDC1,InR,InR2),
2339 ? l_replace_id_by_expr2(T,Id,Inserted,InsUsedIds,IT,WDC2,InR2,OutR),
2340 and_wdc(WDC1,WDC2,WDC).
2341
2342 % conjunct wd condition added flag
2343 and_wdc(true,_,R) :- !,R=true.
2344 and_wdc(_,true,R) :- !, R=true.
2345 and_wdc(_,_,false).
2346
2347 % add contains_wd_condition if a change occured during replacement of id by expression
2348 add_wd_if_needed(true,b(E,T,Infos),Replaced) :-
2349 nonmember(contains_wd_condition,Infos),
2350 !,
2351 Replaced = b(E,T,[contains_wd_condition|Infos]).
2352 add_wd_if_needed(_,T,T).
2353
2354
2355
2356 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2357
2358
2359 % syntaxtransformation_fixed/7 is the same as syntaxtransformation/5 with the exception
2360 % that we distinguish between subexpressions that have the newly introduced identifiers (Names)
2361 % in scope (OSubs) and those who don't (OExprs). The only expressions where the latter case is relevant
2362 % are let_expression and let_predicate.
2363 % TODO: This is a quick'n dirty fix for only some cases.
2364 % NO LONGER REQUIRED: let_expression and let_predicate now obey another semantic, not the Z semantics anymore
2365 %syntaxtransformation_fixed(OExpr,OExprs,OSubs,Names,NExprs,NSubs,NExpr) :-
2366 %syntaxtransformation_fixed(Expr,[],Subs,Names,[],NSubs,NExpr) :-
2367 % syntaxtransformation_det(Expr,Subs,Names,NSubs,NExpr).
2368
2369
2370 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2371 % rename identifier
2372
2373 % r = {x|x : 1..y & x mod 2 = 1}
2374 exists_ast(AST) :- AST =
2375 b(equal(b(identifier(r),set(integer),[nodeid(none)]),
2376 b(comprehension_set([b(identifier(x),integer,[nodeid(none)])],
2377 b(conjunct(b(member(b(identifier(x),integer,[nodeid(none)]),
2378 b(interval(b(integer(1),integer,[nodeid(none)]),b(identifier(y),integer,[nodeid(none)])),
2379 set(integer),[nodeid(none)])),pred,[nodeid(none)]),
2380 b(equal(b(modulo(b(identifier(x),integer,[nodeid(none)]),
2381 b(integer(2),integer,[nodeid(none)])),integer,[contains_wd_condition,nodeid(none)]),
2382 b(integer(1),integer,[nodeid(none)])),pred,
2383 [contains_wd_condition,nodeid(none)])),pred,[contains_wd_condition,nodeid(none)])),
2384 set(integer),[contains_wd_condition,nodeid(none)])),
2385 pred,[contains_wd_condition,nodeid(none)]).
2386
2387 :- assert_must_succeed((bsyntaxtree:exists_ast(A), rename_bt(A,[rename(x,xx)],RA), RA==A )).
2388 :- assert_must_succeed((bsyntaxtree:exists_ast(A), rename_bt(A,[rename(r,v)],RA),
2389 translate:translate_bexpression(RA,TR), TR='v = {x|x : 1 .. y & x mod 2 = 1}' )).
2390 :- assert_must_succeed((gensym:reset_gensym, bsyntaxtree:exists_ast(A), rename_bt(A,[rename(y,x)],RA), RA \= A,
2391 translate:translate_bexpression(RA,TR),
2392 TR = 'r = {`__FRESH____1`|`__FRESH____1` : 1 .. x & `__FRESH____1` mod 2 = 1}' )).
2393
2394 % a simplified version of replace_ids_by_exprs, which assumes target of renamings are variables
2395 rename_bt(Expr,[],Res) :- !,Res=Expr.
2396 rename_bt(OExpr,Renamings,NExpr) :-
2397 create_texpr(Old,Type,OInfo,OExpr),
2398 create_texpr(New,Type,NInfo,NExpr),
2399 ? rename_in_infos(OInfo,Renamings,NInfo),
2400 ? rename_bt2(Old,Renamings,New).
2401 rename_bt2(identifier(Old),Renamings,identifier(New)) :-
2402 !, rename_id(Old,Renamings,New).
2403 rename_bt2(lazy_lookup_expr(Old),Renamings,lazy_lookup_expr(New)) :-
2404 !, rename_id(Old,Renamings,New).
2405 rename_bt2(lazy_lookup_pred(Old),Renamings,lazy_lookup_pred(New)) :-
2406 !, rename_id(Old,Renamings,New).
2407 rename_bt2(OExpr,Renamings,NExpr) :-
2408 ? syntaxtransformation_for_renaming(OExpr,Subs,TNames,NSubs,NExpr),
2409 get_texpr_exprs(TNames,Names),
2410 remove_renamings(Names,Renamings,NRenamings),
2411 ? rename_bt_l(Subs,NRenamings,NSubs).
2412 rename_bt_l([],_,[]).
2413 rename_bt_l([Old|ORest],Renamings,[New|NRest]) :-
2414 ? rename_bt(Old,Renamings,New),
2415 ? rename_bt_l(ORest,Renamings,NRest).
2416
2417 % syntaxtransformation rule for operation_call_in_expr does not show Id field in sub expressions
2418 % (to avoid issues with find_identifier_uses, see below)
2419 % so here we explicitly also rename the operation name if required, relevant for bmachine_construction, test 2504
2420 % TODO: avoid this special case and fix find_identifier_uses instead
2421 syntaxtransformation_for_renaming(operation_call_in_expr(ID,Subs1),Subs,TNames,NSubs,NExpr) :- !,
2422 NExpr = operation_call_in_expr(NID,NSubs1),
2423 Subs = [ID|Subs1],
2424 NSubs = [NID|NSubs1], TNames = [].
2425 syntaxtransformation_for_renaming(OExpr,Subs,TNames,NSubs,NExpr) :-
2426 ? syntaxtransformation(OExpr,Subs,TNames,NSubs,NExpr).
2427
2428 remove_renamings([],Renamings,Renamings).
2429 remove_renamings([identifier(Name)|Rest],Old,New) :-
2430 ? ( select(rename(Name,_),Old,Inter1) -> true % Name no longer visible to renaming
2431 ; Old = Inter1),
2432 ? (member(rename(_OldName,Name),Inter1) ->
2433 % rename the local identifier Name, to avoid clash with the outer Name
2434 % (in case _OldName is used inside)
2435 gensym('__FRESH__',FRESHID),
2436 %print(variable_capture_in_rename(Name,from(OldName),FRESHID)),nl,
2437 Inter2 = [rename(Name,FRESHID)|Inter1]
2438 ; Inter2 = Inter1),
2439 remove_renamings(Rest,Inter2,New).
2440
2441 rename_in_infos(Old,Renamings,New) :-
2442 ( has_info_to_rename(Old) ->
2443 ? maplist(rename_in_infos2(Renamings),Old,New)
2444 ;
2445 Old = New).
2446 rename_in_infos2(Renamings,OInfo,NInfo) :-
2447 ( infos_to_rename(OInfo,OIds,SortedNIds,NInfo) ->
2448 ? rename_ids(OIds,Renamings,NIds),
2449 sort(NIds,SortedNIds)
2450 ;
2451 OInfo = NInfo).
2452
2453 rename_ids([],_,[]).
2454 rename_ids([OId|Orest],Renamings,[NId|Nrest]) :-
2455 rename_id(OId,Renamings,NId),
2456 rename_ids(Orest,Renamings,Nrest).
2457 rename_id(Old,Renamings,New) :-
2458 ( memberchk(rename(Old,New),Renamings) -> true % we could use ord_member if we sort !
2459 ; Old=New).
2460
2461 has_info_to_rename(Infos) :-
2462 ? member(I,Infos),infos_to_rename(I,_,_,_),!.
2463
2464 infos_to_rename(modifies(O),O,N,modifies(N)).
2465 infos_to_rename(reads(O),O,N,reads(N)).
2466 infos_to_rename(non_det_modifies(O),O,N,non_det_modifies(N)).
2467 infos_to_rename(modifies_locals(O),O,N,modifies_locals(N)).
2468 infos_to_rename(reads_locals(O),O,N,reads_locals(N)).
2469 infos_to_rename(used_ids(O),O,N,used_ids(N)).
2470 %infos_to_rename(lambda_result(O),[O],[N],lambda_result(N)). % whould we no longer assume that we have lambda result, as predicate has possibly changed!?
2471
2472
2473 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2474 % remove type information for transformations
2475
2476 remove_bt(b(Expr,Type,Infos),Expr,NExpr,b(NExpr,Type,Infos)).
2477
2478 remove_bt_and_used_ids(b(OldExpr,T,Infos),OldExpr,NewExpr,b(NewExpr,T,NewInfos)) :-
2479 delete(Infos,used_ids(_),NewInfos). % invalidate used_ids info
2480
2481 %remove_bt_l([],[],[],[]).
2482 %remove_bt_l([OT|OTRest],[O|ORest],[N|NRest],[NT|NTRest]) :-
2483 % remove_bt(OT,O,N,NT),
2484 % remove_bt_l(OTRest,ORest,NRest,NTRest).
2485
2486 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2487 % traversations
2488 % Takes a predicate or expression or substitution and extracts:
2489 % the expression itself Expr, its type Type, the syntaxnode information Infos
2490 % + the subexpressions as a list Subs and the local identifiers declared
2491 syntaxtraversion(b(Expr,Type,Infos),Expr,Type,Infos,Subs,Names) :- !,
2492 safe_syntaxelement(Expr,Subs,Names,_,_).
2493 syntaxtraversion(IExpr,Expr,Type,Infos,Subs,Names) :-
2494 add_internal_error('Not properly wrapped', syntaxtraversion(IExpr,Expr,Type,Infos,Subs,Names)),
2495 fail.
2496
2497
2498 map_over_full_bexpr_no_fail(P,BExpr) :-
2499 syntaxtraversion(BExpr,Expr,_,_,Subs,_TNames),
2500 call(P,Expr), % the predicate should not fail
2501 (Subs=[] -> true ; maplist(map_over_full_bexpr_no_fail(P),Subs)).
2502
2503 map_over_bexpr(P,BExpr) :-
2504 syntaxtraversion(BExpr,Expr,_,_,Subs,_TNames),
2505 ? (call(P,Expr) % should probably fail so that by backtrack we recurse
2506 ;
2507 ? member(Sub,Subs), map_over_bexpr(P,Sub)
2508 ).
2509 % same as above but gets typed expressions:
2510 map_over_typed_bexpr(P,BExpr) :-
2511 syntaxtraversion(BExpr,_Expr,_,_,Subs,_TNames),
2512 ? (call(P,BExpr)
2513 ;
2514 ? member(Sub,Subs), map_over_typed_bexpr(P,Sub)
2515 ).
2516 % same as above but returns value:
2517 map_over_typed_bexpr(P,BExpr,Result) :-
2518 syntaxtraversion(BExpr,_Expr,_,_,Subs,_TNames),
2519 ? (call(P,BExpr,Result)
2520 ;
2521 ? member(Sub,Subs), map_over_typed_bexpr(P,Sub,Result)
2522 ).
2523 % this one gets TNames (locally introduced variables as parameter)
2524 map_over_typed_bexpr_with_names(P,BExpr) :-
2525 syntaxtraversion(BExpr,_Expr,_,_,Subs,TNames),
2526 (call(P,BExpr,TNames)
2527 ;
2528 ? member(Sub,Subs), map_over_typed_bexpr_with_names(P,Sub)
2529 ).
2530
2531 % same as map_over_expr but provides an accumulator passed top-down to children; needs to be used by failure driven loop
2532
2533 map_over_bexpr_top_down_acc(P,BExpr,TDAcc) :-
2534 syntaxtraversion(BExpr,Expr,_,_,Subs,_TNames),
2535 (call(P,Expr,TDAcc,NewAcc)
2536 -> member(Sub,Subs), map_over_bexpr_top_down_acc(P,Sub,NewAcc)
2537 ; member(Sub,Subs), map_over_bexpr_top_down_acc(P,Sub,TDAcc)
2538 ).
2539 % now a version which gets the typed predicate as argument
2540
2541 map_over_typed_bexpr_top_down_acc(P,BExpr,TDAcc) :-
2542 syntaxtraversion(BExpr,_Expr,_,_,Subs,_TNames),
2543 (call(P,BExpr,TDAcc,NewAcc)
2544 -> member(Sub,Subs), map_over_typed_bexpr_top_down_acc(P,Sub,NewAcc)
2545 ; member(Sub,Subs), map_over_typed_bexpr_top_down_acc(P,Sub,TDAcc)
2546 ).
2547
2548 % predicate P has 3 arguments: (Expr,ValueSoFar,NewValue)
2549 reduce_over_bexpr(P,BExpr,InitialValue,ResultValue) :-
2550 syntaxtraversion(BExpr,Expr,_,_,Subs,_TNames),
2551 ? call(P,Expr,InitialValue,I1), % print(reduce(P,Expr,InitialValue,I1)),nl,
2552 ? scanlist(reduce_over_bexpr(P),Subs,I1,ResultValue).
2553
2554 % apply a predicate over a syntax tree (bottom-up)
2555
2556 transform_bexpr(Pred,b(Expr,Type,Info),NewBExpr) :- !,
2557 ? syntaxtransformation(Expr,Subs,_Names,NSubs,NewExpr1),
2558 ? l_transform_bexpr(Subs,Pred,NSubs),
2559 ? (call(Pred,b(NewExpr1,Type,Info),NewBExpr) -> true ; NewBExpr = b(NewExpr1,Type,Info)).
2560 transform_bexpr(Pred,Expr,NewBExpr) :-
2561 add_internal_error('Expression not properly wrapped:',transform_bexpr(Pred,Expr,NewBExpr)),
2562 fail.
2563
2564 l_transform_bexpr([],_,[]).
2565 l_transform_bexpr([SubH|T],Pred,[TSubH|TT]) :-
2566 ? transform_bexpr(Pred,SubH,TSubH),
2567 ? l_transform_bexpr(T,Pred,TT).
2568
2569 % apply a predicate over a syntax tree (bottom-up), and provide scoping info about local ids
2570
2571 transform_bexpr_with_scoping(Pred,BExpr,NewBExpr) :-
2572 transform_bexpr_with_scoping2(Pred,BExpr,NewBExpr,[]).
2573 transform_bexpr_with_scoping2(Pred,b(Expr,Type,Info),NewBExpr,LocalIds) :-
2574 syntaxtransformation(Expr,Subs,Names,NSubs,NewExpr1),
2575 get_texpr_ids(Names,QuantifiedNewIds), list_to_ord_set(QuantifiedNewIds,SQuantifiedNewIds),
2576 ord_union(LocalIds,SQuantifiedNewIds,NewLocalIds),
2577 l_transform_bexpr_with_scoping(Subs,Pred,NSubs,NewLocalIds),
2578 (call(Pred,b(NewExpr1,Type,Info),NewBExpr,LocalIds) -> true ; NewBExpr = b(NewExpr1,Type,Info)).
2579
2580 l_transform_bexpr_with_scoping([],_,[],_).
2581 l_transform_bexpr_with_scoping([SubH|T],Pred,[TSubH|TT],LocalIds) :-
2582 transform_bexpr_with_scoping2(Pred,SubH,TSubH,LocalIds),
2583 l_transform_bexpr_with_scoping(T,Pred,TT,LocalIds).
2584
2585 % transform a predicate top-down with scoping infos
2586 % if Pred succeeds the top-down traversal stops
2587 transform_bexpr_td_with_scoping(Pred,BExpr,NewBExpr) :-
2588 ? transform_bexpr_td_with_scoping2(Pred,BExpr,NewBExpr,[]).
2589 transform_bexpr_td_with_scoping2(Pred,b(Expr,Type,Info),b(NewExpr1,Type,Info),LocalIds) :-
2590 ? (call(Pred,Expr,NewExpr1,LocalIds)
2591 -> true
2592 ? ; syntaxtransformation(Expr,Subs,Names,NSubs,NewExpr1),
2593 get_texpr_ids(Names,QuantifiedNewIds), list_to_ord_set(QuantifiedNewIds,SQuantifiedNewIds),
2594 ord_union(LocalIds,SQuantifiedNewIds,NewLocalIds),
2595 ? l_transform_bexpr_td_with_scoping(Subs,Pred,NSubs,NewLocalIds)
2596 ).
2597
2598 l_transform_bexpr_td_with_scoping([],_,[],_).
2599 l_transform_bexpr_td_with_scoping([SubH|T],Pred,[TSubH|TT],LocalIds) :-
2600 ? transform_bexpr_td_with_scoping2(Pred,SubH,TSubH,LocalIds),
2601 ? l_transform_bexpr_td_with_scoping(T,Pred,TT,LocalIds).
2602
2603
2604 % apply a predicate over a syntax tree (bottom-up) with Accumulator result
2605 % Accumulator is constructed bottom up; Pred receives *all* accumulators of sub expressions
2606
2607 transform_bexpr_with_bup_accs(Pred,b(Expr,Type,Info),NewBExpr,EmptyAcc,Acc) :-
2608 syntaxtransformation(Expr,Subs,_Names,NSubs,NewExpr1),
2609 l_transform_bexpr_with_bup_accs(Subs,Pred,NSubs,EmptyAcc,SubAccs),
2610 (call(Pred,b(NewExpr1,Type,Info),NewBExpr,SubAccs,Acc) -> true
2611 ; NewBExpr = b(NewExpr1,Type,Info), Acc = EmptyAcc).
2612
2613 l_transform_bexpr_with_bup_accs([],_,[],_,[]).
2614 l_transform_bexpr_with_bup_accs([SubH|T],Pred,[TSubH|TT],EmptyAcc,[Acc1|RestAcc]) :-
2615 transform_bexpr_with_bup_accs(Pred,SubH,TSubH,EmptyAcc,Acc1),
2616 l_transform_bexpr_with_bup_accs(T,Pred,TT,EmptyAcc,RestAcc).
2617
2618 % apply a predicate over a syntax tree (bottom-up) with Accumulator result
2619 % a single Accumulator is passed along
2620
2621 transform_bexpr_with_acc(_Pred,E,NewBExpr,InAcc,Acc) :- var(E),!,
2622 NewBExpr=E, Acc=InAcc.
2623 transform_bexpr_with_acc(Pred,b(Expr,Type,Info),NewBExpr,InAcc,Acc) :-
2624 syntaxtransformation(Expr,Subs,_Names,NSubs,NewExpr1),
2625 l_transform_bexpr_with_acc(Subs,Pred,NSubs,InAcc,SubAcc),
2626 (call(Pred,b(NewExpr1,Type,Info),NewBExpr,SubAcc,Acc) -> true
2627 ; NewBExpr = b(NewExpr1,Type,Info), Acc = SubAcc).
2628
2629 l_transform_bexpr_with_acc([],_,[],Acc,Acc).
2630 l_transform_bexpr_with_acc([SubH|T],Pred,[TSubH|TT],InAcc,ResAcc) :-
2631 transform_bexpr_with_acc(Pred,SubH,TSubH,InAcc,Acc1),
2632 l_transform_bexpr_with_acc(T,Pred,TT,Acc1,ResAcc).
2633
2634 % a non-deterministic version of this
2635 non_det_transform_bexpr_with_acc(_Pred,E,NewBExpr,InAcc,Acc) :- var(E),!,
2636 NewBExpr=E, Acc=InAcc.
2637 non_det_transform_bexpr_with_acc(Pred,b(Expr,Type,Info),NewBExpr,InAcc,Acc) :-
2638 syntaxtransformation(Expr,Subs,_Names,NSubs,NewExpr1),
2639 l_nd_transform_bexpr_with_acc(Subs,Pred,NSubs,InAcc,SubAcc),
2640 if(call(Pred,b(NewExpr1,Type,Info),NewBExpr,SubAcc,Acc),
2641 true,
2642 (NewBExpr = b(NewExpr1,Type,Info), Acc = SubAcc)).
2643
2644 l_nd_transform_bexpr_with_acc([],_,[],Acc,Acc).
2645 l_nd_transform_bexpr_with_acc([SubH|T],Pred,[TSubH|TT],InAcc,ResAcc) :-
2646 non_det_transform_bexpr_with_acc(Pred,SubH,TSubH,InAcc,Acc1),
2647 l_nd_transform_bexpr_with_acc(T,Pred,TT,Acc1,ResAcc).
2648
2649
2650 % -------------------------
2651
2652 min_max_integer_value_used(BExpr,Min,Max) :-
2653 min_max_integer_value_used(BExpr,none,none,Min,Max).
2654 min_max_integer_value_used(BExpr,IMin,IMax,Min,Max) :-
2655 reduce_over_bexpr(min_max_aux,BExpr,minmax(IMin,IMax),minmax(Min,Max)).
2656
2657 min_max_aux(sequence_extension(L),minmax(Min,Max),minmax(NMin,NMax)) :- !,
2658 length(L,Len), % we use implicitly numbers from 1..Len
2659 (number(Min),1>Min -> NMin=Min ; NMin=1),
2660 (number(Max),Len<Max -> NMax=Max ; NMax=Len).
2661 min_max_aux(integer(N),minmax(Min,Max),minmax(NMin,NMax)) :- !,
2662 (number(Min),N>Min -> NMin=Min ; NMin=N),
2663 (number(Max),N<Max -> NMax=Max ; NMax=N).
2664 min_max_aux(_,V,V).
2665
2666 % check if a B expression uses something like NAT,NAT1,INT, MAXINT or MININT.
2667 uses_implementable_integers(BExpr) :-
2668 map_over_bexpr(uses_implementable_integers_aux,BExpr).
2669
2670 uses_implementable_integers_aux(maxint).
2671 uses_implementable_integers_aux(minint).
2672 uses_implementable_integers_aux(integer_set(X)) :-
2673 (X='NAT1' ; X='NAT' ; X='INT').
2674
2675 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2676 % some checks
2677 check_if_typed_predicate(b(Pred,X,_)) :- ground(X), X=pred, % at runtime there can be value(X) with variables inside !
2678 syntaxelement(Pred,_,_,_,_,TypePred), (TypePred=pred -> true ; TypePred = pred/only_typecheck).
2679 check_if_typed_expression(b(Expr,Type,_)) :-
2680 syntaxelement(Expr,_,_,_,_,TypeExpr),
2681 (TypeExpr=expr -> true ; TypeExpr = expr/only_typecheck),
2682 Type \== pred, Type \== subst, ground(Type).
2683 check_if_typed_substitution(b(Subst,X,_)) :- ground(X), X=subst,
2684 syntaxelement(Subst,_,_,_,_,subst).
2685
2686 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2687 % transformations
2688
2689 syntaxtransformation(Expr,Subs,Names,NSubs,NExpr) :-
2690 functor(Expr,F,Arity),
2691 functor(NExpr,F,Arity),
2692 safe_syntaxelement(Expr,Subs,Names,Lists,Constant),
2693 all_same_length(Lists,NLists),
2694 ? syntaxelement(NExpr,NSubs,_,NLists,Constant,_).
2695 % a faster non-backtracking version:
2696 syntaxtransformation_det(Expr,Subs,Names,NSubs,NExpr) :-
2697 functor(Expr,F,Arity),
2698 functor(NExpr,F,Arity),
2699 safe_syntaxelement_det(Expr,Subs,Names,Lists,Constant),
2700 all_same_length(Lists,NLists),
2701 ? syntaxelement(NExpr,NSubs,_,NLists,Constant,_).
2702
2703
2704 safe_syntaxelement(Expr,Subs,Names,Lists,Constant) :-
2705 ( syntaxelement(Expr,SubsX,NamesX,Lists,ConstantX,_) ->
2706 Subs=SubsX, Names=NamesX, Constant=ConstantX
2707 %(Subs,Names,Constant)=(SubsX,NamesX,ConstantX)
2708 ;
2709 functor(Expr,F,Arity),
2710 add_error_fail(bsyntaxtree,'Uncovered syntax element: ', F/Arity)
2711 ).
2712 % a faster non-backtracking version of safe_syntaxelement, assuming Subs, Names, ... are fresh vars
2713 safe_syntaxelement_det(Expr,Subs,Names,Lists,Constant) :-
2714 (syntaxelement(Expr,Subs,Names,Lists,Constant,_) -> true
2715 ; functor(Expr,F,Arity),
2716 add_error_fail(bsyntaxtree,'Uncovered syntax element: ', F/Arity)).
2717
2718 is_subst_syntaxelement(Subst) :-
2719 syntaxelement(Subst,_,_,_,_,subst).
2720
2721 % check if we have a syntax node without parameters
2722 is_syntax_constant(Expr) :- atom(Expr), syntaxelement(Expr,_,_,_,_,_).
2723
2724 % syntaxelement(Expr,SubExprs,Identifiers,Lists,Constant,Type):
2725 % Expr: the expression itself
2726 % SubExprs: a list of sub-expressions
2727 % Identifiers: a list of identifiers that are newly introduced (e.g. by a quantifier)
2728 % Lists: A list of lists in the expression, to prevent infinite loops when having variable parts
2729 % Constant: A part of the expression that is not a sub-expression (e.g. the number in integer(...))
2730 % Type: Fundamental type of the element (predicate, expression, etc)
2731
2732 % predicates
2733 syntaxelement(truth, [], [], [], [], pred).
2734 syntaxelement(falsity, [], [], [], [], pred).
2735 syntaxelement(unknown_truth_value(Msg),[], [], [], Msg, pred). % artificial, e.g., created by well_def_analyser
2736 syntaxelement(conjunct(A,B), [A,B],[], [], [], pred).
2737 %syntaxelement(conjunct(As), As, [], [], [], pred). % TO DO: support associative version of conjunct
2738 syntaxelement(negation(A), [A], [], [], [], pred).
2739 syntaxelement(disjunct(A,B), [A,B],[], [], [], pred).
2740 syntaxelement(implication(A,B), [A,B],[], [], [], pred).
2741 syntaxelement(equivalence(A,B), [A,B],[], [], [], pred).
2742 syntaxelement(equal(A,B), [A,B],[], [], [], pred).
2743 syntaxelement(not_equal(A,B), [A,B],[], [], [], pred).
2744 syntaxelement(member(A,B), [A,B],[], [], [], pred).
2745 syntaxelement(not_member(A,B), [A,B],[], [], [], pred).
2746 syntaxelement(subset(A,B), [A,B],[], [], [], pred).
2747 syntaxelement(subset_strict(A,B), [A,B],[], [], [], pred).
2748 syntaxelement(not_subset(A,B), [A,B],[], [], [], pred).
2749 syntaxelement(not_subset_strict(A,B),[A,B],[], [], [], pred).
2750 syntaxelement(less_equal(A,B), [A,B],[], [], [], pred).
2751 syntaxelement(less(A,B), [A,B],[], [], [], pred).
2752 syntaxelement(less_equal_real(A,B), [A,B],[], [], [], pred).
2753 syntaxelement(less_real(A,B), [A,B],[], [], [], pred).
2754 syntaxelement(greater_equal(A,B), [A,B],[], [], [], pred).
2755 syntaxelement(greater(A,B), [A,B],[], [], [], pred).
2756 syntaxelement(forall(Ids,D,P), [D,P|Ids],Ids,[Ids], [], pred).
2757 syntaxelement(exists(Ids,P), [P|Ids], Ids,[Ids], [], pred).
2758 syntaxelement(finite(A), [A], [], [], [], pred/only_typecheck).
2759 syntaxelement(partition(S,Es), [S|Es],[],[Es],[],pred).
2760 syntaxelement(kodkod(PId,Ids), Ids,[],[Ids],PId, pred).
2761 syntaxelement(external_pred_call(F,Args),Args,[],[Args],F,pred).
2762
2763 % expressions
2764 syntaxelement(value(V), [], [], [], V, expr).
2765 syntaxelement(operation_call_in_expr(Id,As), As, [], [As], Id, expr). % Do not treat Id as a sub-expression for find_identifier_uses, ...
2766 %syntaxelement(operation_call_in_expr(Id,As), [Id|As], [], [As], [], expr). % was like this, but changed to avoid op(.) ids in find_identifier_uses
2767 syntaxelement(boolean_true, [], [], [], [], expr).
2768 syntaxelement(boolean_false, [], [], [], [], expr).
2769 syntaxelement(max_int, [], [], [], [], expr).
2770 syntaxelement(min_int, [], [], [], [], expr).
2771 syntaxelement(empty_set, [], [], [], [], expr).
2772 syntaxelement(bool_set, [], [], [], [], expr).
2773 syntaxelement(float_set, [], [], [], [], expr).
2774 syntaxelement(real(I), [], [], [], I, expr).
2775 syntaxelement(real_set, [], [], [], [], expr).
2776 syntaxelement(string_set, [], [], [], [], expr).
2777 syntaxelement(convert_bool(A), [A], [], [], [], expr).
2778 syntaxelement(convert_real(A), [A], [], [], [], expr).
2779 syntaxelement(convert_int_floor(A), [A], [], [], [], expr).
2780 syntaxelement(convert_int_ceiling(A), [A], [], [], [], expr).
2781 syntaxelement(add(A,B), [A,B],[], [], [], expr).
2782 syntaxelement(add_real(A,B), [A,B],[], [], [], expr).
2783 syntaxelement(minus(A,B), [A,B],[], [], [], expr).
2784 syntaxelement(minus_real(A,B), [A,B],[], [], [], expr).
2785 syntaxelement(minus_or_set_subtract(A,B),[A,B],[], [], [], expr/only_typecheck).
2786 syntaxelement(unary_minus(A), [A], [], [], [], expr).
2787 syntaxelement(unary_minus_real(A), [A], [], [], [], expr).
2788 syntaxelement(multiplication(A,B), [A,B],[], [], [], expr).
2789 syntaxelement(multiplication_real(A,B),[A,B],[], [], [], expr).
2790 syntaxelement(mult_or_cart(A,B), [A,B],[], [], [], expr/only_typecheck).
2791 syntaxelement(cartesian_product(A,B), [A,B],[], [], [], expr).
2792 syntaxelement(div(A,B), [A,B],[], [], [], expr).
2793 syntaxelement(div_real(A,B), [A,B],[], [], [], expr).
2794 syntaxelement(floored_div(A,B), [A,B],[], [], [], expr).
2795 syntaxelement(modulo(A,B), [A,B],[], [], [], expr).
2796 syntaxelement(power_of(A,B), [A,B],[], [], [], expr).
2797 syntaxelement(power_of_real(A,B), [A,B],[], [], [], expr).
2798 syntaxelement(successor, [], [], [], [], expr).
2799 syntaxelement(predecessor, [], [], [], [], expr).
2800 syntaxelement(max(A), [A], [], [], [], expr).
2801 syntaxelement(max_real(A), [A], [], [], [], expr).
2802 syntaxelement(min(A), [A], [], [], [], expr).
2803 syntaxelement(min_real(A), [A], [], [], [], expr).
2804 syntaxelement(card(A), [A], [], [], [], expr).
2805 syntaxelement(couple(A,B), [A,B],[], [], [], expr).
2806 syntaxelement(pow_subset(A), [A], [], [], [], expr).
2807 syntaxelement(pow1_subset(A), [A], [], [], [], expr).
2808 syntaxelement(fin_subset(A), [A], [], [], [], expr).
2809 syntaxelement(fin1_subset(A), [A], [], [], [], expr).
2810 syntaxelement(interval(A,B), [A,B],[], [], [], expr).
2811 syntaxelement(union(A,B), [A,B],[], [], [], expr).
2812 syntaxelement(intersection(A,B), [A,B],[], [], [], expr).
2813 syntaxelement(set_subtraction(A,B), [A,B],[], [], [], expr).
2814 syntaxelement(general_union(A), [A], [], [], [], expr).
2815 syntaxelement(general_intersection(A), [A] , [], [], [], expr).
2816 syntaxelement(relations(A,B), [A,B],[], [], [], expr).
2817 syntaxelement(identity(A), [A], [], [], [], expr).
2818 syntaxelement(event_b_identity, [], [], [], [], expr). % for Rodin 1.0, TO DO: Daniel please check
2819 syntaxelement(reverse(A), [A], [], [], [], expr).
2820 syntaxelement(first_projection(A,B), [A,B],[], [], [], expr/only_typecheck).
2821 syntaxelement(first_of_pair(A), [A], [], [], [], expr).
2822 syntaxelement(event_b_first_projection(A),[A], [], [], [], expr/only_typecheck).
2823 syntaxelement(event_b_first_projection_v2,[], [], [], [], expr/only_typecheck). % for Rodin 1.0, TO DO: Daniel please check
2824 syntaxelement(second_projection(A,B), [A,B],[], [], [], expr/only_typecheck).
2825 syntaxelement(event_b_second_projection_v2,[], [], [], [], expr/only_typecheck). % for Rodin 1.0, TO DO: Daniel please check
2826 syntaxelement(second_of_pair(A), [A], [], [], [], expr).
2827 syntaxelement(event_b_second_projection(A),[A], [], [], [], expr/only_typecheck).
2828 syntaxelement(composition(A,B), [A,B],[], [], [], expr).
2829 syntaxelement(ring(A,B), [A,B],[], [], [], expr/only_typecheck).
2830 syntaxelement(direct_product(A,B), [A,B],[], [], [], expr).
2831 syntaxelement(parallel_product(A,B), [A,B],[], [], [], expr).
2832 syntaxelement(trans_function(A), [A], [], [], [], expr).
2833 syntaxelement(trans_relation(A), [A], [], [], [], expr).
2834 syntaxelement(iteration(A,B), [A,B],[], [], [], expr).
2835 syntaxelement(reflexive_closure(A), [A], [], [], [], expr).
2836 syntaxelement(closure(A), [A], [], [], [], expr).
2837 syntaxelement(domain(A), [A], [], [], [], expr).
2838 syntaxelement(range(A), [A], [], [], [], expr).
2839 syntaxelement(image(A,B), [A,B],[], [], [], expr).
2840 syntaxelement(domain_restriction(A,B), [A,B],[], [], [], expr).
2841 syntaxelement(domain_subtraction(A,B), [A,B],[], [], [], expr).
2842 syntaxelement(range_restriction(A,B), [A,B],[], [], [], expr).
2843 syntaxelement(range_subtraction(A,B), [A,B],[], [], [], expr).
2844 syntaxelement(overwrite(A,B), [A,B],[], [], [], expr).
2845 syntaxelement(partial_function(A,B), [A,B],[], [], [], expr).
2846 syntaxelement(total_function(A,B), [A,B],[], [], [], expr).
2847 syntaxelement(partial_injection(A,B), [A,B],[], [], [], expr).
2848 syntaxelement(total_injection(A,B), [A,B],[], [], [], expr).
2849 syntaxelement(partial_surjection(A,B), [A,B],[], [], [], expr).
2850 syntaxelement(total_surjection(A,B), [A,B],[], [], [], expr).
2851 syntaxelement(total_bijection(A,B), [A,B],[], [], [], expr).
2852 syntaxelement(partial_bijection(A,B), [A,B],[], [], [], expr).
2853 syntaxelement(total_relation(A,B), [A,B],[], [], [], expr).
2854 syntaxelement(surjection_relation(A,B),[A,B],[], [], [], expr).
2855 syntaxelement(total_surjection_relation(A,B),[A,B],[], [], [], expr).
2856 syntaxelement(seq(A), [A], [], [], [], expr).
2857 syntaxelement(seq1(A), [A], [], [], [], expr).
2858 syntaxelement(iseq(A), [A], [], [], [], expr).
2859 syntaxelement(iseq1(A), [A], [], [], [], expr).
2860 syntaxelement(perm(A), [A], [], [], [], expr).
2861 syntaxelement(empty_sequence, [], [], [], [], expr).
2862 syntaxelement(size(A), [A], [], [], [], expr).
2863 syntaxelement(first(A), [A], [], [], [], expr).
2864 syntaxelement(last(A), [A], [], [], [], expr).
2865 syntaxelement(front(A), [A], [], [], [], expr).
2866 syntaxelement(tail(A), [A], [], [], [], expr).
2867 syntaxelement(rev(A), [A], [], [], [], expr).
2868 syntaxelement(concat(A,B), [A,B],[], [], [], expr).
2869 syntaxelement(insert_front(A,B), [A,B],[], [], [], expr).
2870 syntaxelement(insert_tail(A,B), [A,B],[], [], [], expr).
2871 syntaxelement(restrict_front(A,B), [A,B],[], [], [], expr).
2872 syntaxelement(restrict_tail(A,B), [A,B],[], [], [], expr).
2873 syntaxelement(general_concat(A), [A], [], [], [], expr).
2874 syntaxelement(function(A,B), [A,B],[], [], [], expr).
2875 syntaxelement(external_function_call(F,Args),Args,[],[Args],F,expr).
2876 syntaxelement(identifier(I), [], [], [], I, expr).
2877 syntaxelement(lazy_lookup_expr(I), [], [], [], I, expr).
2878 syntaxelement(lazy_lookup_pred(I), [], [], [], I, pred).
2879 syntaxelement(integer(I), [], [], [], I, expr).
2880 syntaxelement(integer_set(T), [], [], [], T, expr).
2881 syntaxelement(string(S), [], [], [], S, expr).
2882 syntaxelement(set_extension(L), L, [], [L], [], expr).
2883 syntaxelement(sequence_extension(L), L, [], [L], [], expr).
2884 syntaxelement(comprehension_set(Ids,P),[P|Ids], Ids,[Ids], [], expr).
2885 syntaxelement(event_b_comprehension_set(Ids,E,P),[E,P|Ids], Ids,[Ids], [], expr/only_typecheck).
2886 syntaxelement(lambda(Ids,P,E), [P,E|Ids],Ids,[Ids], [], expr).
2887 syntaxelement(general_sum(Ids,P,E), [P,E|Ids],Ids,[Ids], [], expr).
2888 syntaxelement(general_product(Ids,P,E), [P,E|Ids],Ids,[Ids], [], expr).
2889 syntaxelement(quantified_union(Ids,P,E), [P,E|Ids],Ids,[Ids], [], expr).
2890 syntaxelement(quantified_intersection(Ids,P,E), [P,E|Ids],Ids,[Ids], [], expr).
2891 syntaxelement(struct(Rec), [Rec], [], [], [], expr).
2892 ?syntaxelement(rec(Fields), FContent, [], [FContent], FNames, expr) :- syntaxfields(Fields,FContent, FNames).
2893 syntaxelement(record_field(R,I), [R], [], [], I, expr).
2894 syntaxelement(assertion_expression(Cond,ErrMsg,Expr), [Cond,Expr], [], [], ErrMsg, expr).
2895 syntaxelement(typeset, [], [], [], [], expr/only_typecheck).
2896
2897 syntaxelement(tree(A), [A], [], [], [], expr).
2898 syntaxelement(btree(A), [A], [], [], [], expr).
2899 syntaxelement(const(A,B), [A,B],[], [], [], expr).
2900 syntaxelement(top(A), [A], [], [], [], expr).
2901 syntaxelement(sons(A), [A], [], [], [], expr).
2902 syntaxelement(prefix(A), [A], [], [], [], expr).
2903 syntaxelement(postfix(A), [A], [], [], [], expr).
2904 syntaxelement(sizet(A), [A], [], [], [], expr).
2905 syntaxelement(mirror(A), [A], [], [], [], expr).
2906 syntaxelement(rank(A,B), [A,B],[], [], [], expr).
2907 syntaxelement(father(A,B), [A,B],[], [], [], expr).
2908 syntaxelement(son(A,B,C), [A,B,C],[], [], [], expr).
2909 syntaxelement(subtree(A,B), [A,B],[], [], [], expr).
2910 syntaxelement(arity(A,B), [A,B],[], [], [], expr).
2911 syntaxelement(bin(A), [A],[], [], [], expr).
2912 syntaxelement(bin(A,B,C), [A,B,C],[], [], [], expr).
2913 syntaxelement(infix(A), [A], [], [], [], expr).
2914 syntaxelement(left(A), [A], [], [], [], expr).
2915 syntaxelement(right(A), [A], [], [], [], expr).
2916
2917 % substitutions
2918 syntaxelement(skip, [], [], [], [], subst).
2919 syntaxelement(precondition(A,B), [A,B],[], [], [], subst).
2920 syntaxelement(assertion(A,B), [A,B],[], [], [], subst).
2921 syntaxelement(witness_then(A,B), [A,B],[], [], [], subst).
2922 syntaxelement(if_elsif(A,B), [A,B],[], [], [], subst/elsif).
2923 syntaxelement(while(A,B,C,D), [A,B,C,D],[], [], [], subst).
2924 % used only internally in the interpreter, contains last value of variant:
2925 syntaxelement(while1(A,B,C,D,E), [A,B,C,D],[], [], E, subst).
2926 syntaxelement(select_when(A,B), [A,B],[], [], [], subst/when).
2927 syntaxelement(block(S),[S],[],[],[], subst/only_typecheck).
2928 syntaxelement(assign(Lhs,Rhs),Exprs,[],[Lhs,Rhs], [], subst) :- append(Lhs,Rhs,Exprs).
2929 syntaxelement(assign_single_id(Id,Rhs),[Id,Rhs],[],[], [], subst).
2930 syntaxelement(any(Ids,P,S),[P,S|Ids],Ids,[Ids], [], subst).
2931 syntaxelement(var(Ids,S), [S|Ids], Ids,[Ids], [], subst).
2932 syntaxelement(if(Ifs), Ifs, [], [Ifs], [], subst).
2933 syntaxelement(parallel(Ss), Ss, [], [Ss], [], subst).
2934 syntaxelement(sequence(Ss), Ss, [], [Ss], [], subst).
2935 syntaxelement(becomes_element_of(Ids,E), [E|Ids], [], [Ids], [], subst).
2936 syntaxelement(becomes_such(Ids,P), [P|Ids], [], [Ids], [], subst). % Ids are new value, Ids$0 is old value
2937 syntaxelement(evb2_becomes_such(Ids,P), [P|Ids], [], [Ids], [], subst/only_typecheck).
2938 syntaxelement(let(Ids,P,S), [P,S|Ids], Ids, [Ids], [], subst).
2939 syntaxelement(operation_call(Id,Rs,As), [Id|Exprs], [], [Rs,As], [], subst) :- append(Rs,As,Exprs).
2940 syntaxelement(case(E,Eithers,Else), [E,Else|Eithers], [], [Eithers], [], subst).
2941 syntaxelement(case_or(Es,S), [S|Es], [], [Es], [], subst/caseor).
2942 syntaxelement(choice(Ss), Ss, [], [Ss], [], subst).
2943 syntaxelement(select(Whens), Whens, [], [Whens], [], subst).
2944 syntaxelement(select(Whens,Else), [Else|Whens], [], [Whens], [], subst).
2945 syntaxelement(operation(I,Rs,As,B), [I,B|Ids], Ids, [Rs,As], [], subst) :- append(Rs,As,Ids).
2946 syntaxelement(external_subst_call(F,Args),Args,[],[Args],F,subst).
2947
2948 % elements of a VALUES clause
2949 syntaxelement(values_entry(I,E),[I,E],[],[],[],values_entry).
2950
2951 % syntax for Event-B events
2952 syntaxelement(rlevent(I,Sec,St,Ps,G,Ts,As,VWs,PWs,Ums,Rs), Subs, [], [Ps,Ts,As,VWs,PWs,Ums,Rs], [I,Sec], subst) :-
2953 append([[St],Ps,[G],Ts,As,VWs,PWs,Ums,Rs],Subs).
2954 syntaxelement(witness(I,P), [I,P], [], [], [], witness).
2955
2956 % extended syntax for Z
2957 syntaxelement(let_predicate(Ids,As,Pred), Exprs, Ids, [Ids,As], [], pred) :- append([Ids,As,[Pred]],Exprs).
2958 syntaxelement(let_expression(Ids,As,Expr), Exprs, Ids, [Ids,As], [], expr) :- append([Ids,As,[Expr]],Exprs).
2959 syntaxelement(let_expression_global(Ids,As,Expr), Exprs, Ids, [Ids,As], [], expr) :- % version used by b_compiler
2960 append([Ids,As,[Expr]],Exprs).
2961 syntaxelement(lazy_let_expr(TID,A,Expr), [TID, A, Expr], [TID], [[TID],[A]], [], expr).
2962 syntaxelement(lazy_let_pred(TID,A,Expr), [TID, A, Expr], [TID], [[TID],[A]], [], pred).
2963 syntaxelement(lazy_let_subst(TID,A,Expr), [TID, A, Expr], [TID], [[TID],[A]], [], subst).
2964 syntaxelement(if_then_else(If,Then,Else),[If,Then,Else], [], [], [], expr).
2965 syntaxelement(compaction(A), [A], [], [], [], expr).
2966 syntaxelement(mu(A), [A], [], [], [], expr).
2967 syntaxelement(bag_items(A), [A], [], [], [], expr).
2968
2969 syntaxelement(freetype_set(Id), [], [], [], Id, expr).
2970 syntaxelement(freetype_case(Type,Case,Expr), [Expr], [], [], [Type,Case], pred).
2971 syntaxelement(freetype_constructor(Type,Case,Expr), [Expr], [], [], [Type,Case], expr).
2972 syntaxelement(freetype_destructor(Type,Case,Expr), [Expr], [], [], [Type,Case], expr).
2973
2974 syntaxelement(ordinary, [], [], [], [], status).
2975 syntaxelement(anticipated(Variant), [Variant], [], [], [], status).
2976 syntaxelement(convergent(Variant), [Variant], [], [], [], status).
2977
2978 % Just one ID expected
2979 syntaxelement(recursive_let(Id,C),[Id,C],[Id],[],[], expr). % Note: Id is not really introduced !
2980
2981
2982 % fields of records
2983 %syntaxfields(Fields,C,_) :- var(Fields),var(C),var(N),!, add_internal_error('Illegal call: ',syntaxfields(Fields,C,N)),fail.
2984 syntaxfields([],[],[]).
2985 ?syntaxfields([field(N,C)|Rest],[C|CRest],[N|NRest]) :- syntaxfields(Rest,CRest,NRest).
2986
2987 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2988 % helper for declaration of quantified identifiers
2989
2990 % has_declared_identifier/2 returns a list of identifiers which are declared in
2991 % this AST node. The main difference to the Names variable when doing a
2992 % syntaxtraversion/6 or similiar is that the identifiers are described by
2993 % predicates.
2994 has_declared_identifier(TExpr,Ids) :-
2995 get_texpr_expr(TExpr,Expr),
2996 ( default_declaration(Expr,_,Ids,_)
2997 ; non_default_declaration(Expr,Ids)).
2998
2999 add_declaration_for_identifier(b(Expr,Type,Infos),Decl,b(NExpr,Type,NewInfos)) :-
3000 %delete(Infos,used_ids(_),NewInfos), % we cannot
3001 ( default_declaration(Expr,Predicate,Ids,Constant) ->
3002 same_functor(Expr,NExpr),
3003 conjunct_predicates([Decl,Predicate],NPredicate),
3004 default_declaration(NExpr,NPredicate,Ids,Constant)
3005 ; non_default_declaration(Expr,Ids) ->
3006 add_non_default_declaration(Expr,Decl,NExpr)
3007 ),
3008 add_used_ids(Infos,Ids,Decl,NewInfos).
3009
3010 % add used ids of a predicate within quantification of Ids to current used_ids info; if it is there
3011 add_used_ids(Infos,Ids,Pred,NewInfos) :- update_used_ids(Infos,OldUsed,NewInfos,NewUsed),
3012 !, % a field needs updating
3013 find_identifier_uses(Pred,[],NewIds), get_texpr_ids(Ids,UnsortedIds),sort(UnsortedIds,SIds),
3014 ord_subtract(NewIds,SIds,NewIds2),
3015 ord_union(NewIds2,OldUsed,NewUsed).
3016 add_used_ids(I,_,_,I).
3017
3018 % just update used_ids field (e.g., when just computed to store it for later)
3019 ?update_used_ids(Infos,OldUsed,NewInfos,NewUsed) :- select(OldInfo,Infos,I1),
3020 used_ids_like_info(OldInfo,F,OldUsed),!,
3021 used_ids_like_info(NewInfo,F,NewUsed),NewInfos = [NewInfo|I1].
3022
3023 % info fields which contain used_ids information
3024 used_ids_like_info(used_ids(UsedIds),used_ids,UsedIds).
3025 used_ids_like_info(reads(UsedIds),reads,UsedIds).
3026
3027 :- use_module(probsrc(btypechecker), [prime_identifiers/2]).
3028
3029 % default_declaration(Expr,Predicate,Ids,Constant)
3030 default_declaration(forall(Ids,D,P),D,Ids,P).
3031 default_declaration(exists(Ids,P),P,Ids,[]).
3032 default_declaration(comprehension_set(Ids,P),P,Ids,[]).
3033 default_declaration(event_b_comprehension_set(Ids,E,P),P,Ids,E). % translated !?
3034 default_declaration(lambda(Ids,P,E),P,Ids,E).
3035 default_declaration(general_sum(Ids,P,E),P,Ids,E).
3036 default_declaration(general_product(Ids,P,E),P,Ids,E).
3037 default_declaration(quantified_union(Ids,P,E),P,Ids,E).
3038 default_declaration(quantified_intersection(Ids,P,E),P,Ids,E).
3039 default_declaration(any(Ids,P,S),P,Ids,S).
3040 default_declaration(becomes_such(Ids,P),P,Ids,[]).
3041 default_declaration(evb2_becomes_such(Ids,P),P,Primed,[]) :-
3042 nl,print(evb2(Ids,Primed)),nl,nl, % no longer used, as it is translated to becomes_such
3043 prime_identifiers(Ids,Primed).
3044 default_declaration(rlevent(I,Sec,St,Ps,G,Ts,As,VWs,PWs,Ums,Rs),G,Ps,
3045 [I,Sec,St,Ps,Ts,As,VWs,PWs,Ums,Rs]).
3046 default_declaration(let_predicate(Ids,Ps,Body),Ps,Ids,Body) :- print(let(Ids)),nl. % TODO: check format of Ps
3047 default_declaration(let_expression(Ids,Ps,Body),Ps,Ids,Body) :- print(let(Ids)),nl. % TODO: check format of Ps
3048 default_declaration(let_expression_global(Ids,Ps,Body),Ps,Ids,Body) :- print(let(Ids)),nl. % TODO: check format of Ps
3049 % TODO: lazy let ?
3050
3051 non_default_declaration(operation(_I,Rs,As,_TBody),Ids) :-
3052 append(Rs,As,Ids).
3053
3054 add_non_default_declaration(operation(I,Rs,As,TBody),Decl,operation(I,Rs,As,NTBody)) :-
3055 ( get_guard_and_copy(TBody,P,NP,NTBody) ->
3056 conjunct_predicates([Decl,P],NP)
3057 ; create_texpr(precondition(Decl,TBody),subst,[],NTBody)).
3058
3059 get_guard_and_copy(TBody,P,NP,NTBody) :- remove_bt(TBody,Body,NBody,NTBody),
3060 get_guard_copy2(Body,P,NP,NBody).
3061
3062 get_guard_copy2(precondition(P,S),P,NP,precondition(NP,S)).
3063 get_guard_copy2(rlevent(I,Sec,St,Ps, G,Ts,As,VWs,PWs,Ums,Rs), G, NG,
3064 rlevent(I,Sec,St,Ps,NG,Ts,As,VWs,PWs,Ums,Rs)).
3065
3066 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3067 % pattern definitions (not yet finished)
3068
3069 bsyntax_pattern(Expr,TExpr) :-
3070 var(Expr),!,Expr=TExpr.
3071 bsyntax_pattern(-Expr,TExpr) :-
3072 !,remove_all_infos(Expr,TExpr).
3073 bsyntax_pattern(Expr,TExpr) :-
3074 functor(Expr,b,3),!,Expr=TExpr.
3075 bsyntax_pattern(Expr:Type/Info,TExpr) :-
3076 !,bsyntax_pattern2(Expr,Type,Info,TExpr).
3077 bsyntax_pattern(Expr:Type,TExpr) :-
3078 !,bsyntax_pattern2(Expr,Type,_Info,TExpr).
3079 bsyntax_pattern(Expr/Info,TExpr) :-
3080 !,bsyntax_pattern2(Expr,_Type,Info,TExpr).
3081 bsyntax_pattern(Expr,TExpr) :-
3082 !,bsyntax_pattern2(Expr,_Type,_Info,TExpr).
3083
3084 bsyntax_pattern2(Pattern,Type,Info,TExpr) :-
3085 functor(Pattern,Functor,Arity),
3086 functor(R,Functor,Arity),
3087 create_texpr(R,Type,Info,TExpr),
3088 syntaxelement(Pattern,PSubs,_,PLists,Const,EType),
3089 syntaxelement(R,RSubs,_,RLists,Const,EType),
3090 ( EType==pred -> Type=pred
3091 ; EType==subst -> Type=subst
3092 ; true),
3093 all_same_length(PLists,RLists),
3094 maplist(bsyntax_pattern,PSubs,RSubs).
3095
3096 all_same_length([],[]).
3097 all_same_length([A|Arest],[B|Brest]) :-
3098 ( var(A),var(B) ->
3099 add_error_fail(bsyntaxtree,'At least one list should contain nonvar elements for all_same_length',[A,B])
3100 ;
3101 same_length(A,B)),
3102 all_same_length(Arest,Brest).
3103
3104 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3105 % strip an AST into a more compact form (without b/3 terms)
3106
3107 strip_and_norm_ast(TExpr,SNExpr) :-
3108 get_texpr_expr(TExpr,Expr),
3109 ? strip_and_norm_ast_aux(Expr,SNExpr).
3110
3111 :- use_module(tools,[safe_univ_no_cutoff/2]).
3112 strip_and_norm_ast_aux(Expr,Res) :-
3113 comm_assoc_subs(Expr,Op,Subs,[]), !, % associative & commutative operator detected
3114 ? maplist(strip_and_norm_ast_aux,Subs,NSubs), % Subs are already unwrapped
3115 sort(NSubs,Sorted), % in case there are associative operators that are not commutative: insert is_commutative check
3116 safe_univ_no_cutoff(Res,[Op|Sorted]).
3117 strip_and_norm_ast_aux(Expr,Res) :-
3118 assoc_subs(Expr,Op,Subs,[]), !, % associative operator detected
3119 maplist(strip_and_norm_ast_aux,Subs,NSubs), % Subs are already unwrapped
3120 safe_univ_no_cutoff(Res,[Op|NSubs]).
3121 strip_and_norm_ast_aux(Expr,SNExpr) :-
3122 ? syntaxtransformation(Expr,Subs,_,NSubs,SExpr),
3123 ? strip_and_norm_ast_l(Subs,NSubs),
3124 norm_strip(SExpr,SNExpr).
3125
3126 strip_and_norm_ast_l([],[]).
3127 strip_and_norm_ast_l([TExpr|Trest],[NExpr|Nrest]) :-
3128 ? strip_and_norm_ast(TExpr,NExpr),
3129 ? strip_and_norm_ast_l(Trest,Nrest).
3130
3131 norm_strip(greater_equal(A,B),less_equal(B,A)) :- !.
3132 norm_strip(greater(A,B),less(B,A)) :- !.
3133 norm_strip(set_extension(NL),set_extension(SNL)) :- !,
3134 sort(NL,SNL).
3135 norm_strip(Old,New) :-
3136 functor(Old,Functor,2),
3137 is_commutative(Functor),!,
3138 arg(1,Old,OA),
3139 arg(2,Old,OB),
3140 ( OA @> OB -> New =.. [Functor,OB,OA]
3141 ; New=Old).
3142 norm_strip(Old,Old).
3143 % TO DO: flatten associative operators into lists !
3144
3145 comm_assoc_subs(conjunct(TA,TB),conjunct) --> !,
3146 {get_texpr_expr(TA,A), get_texpr_expr(TB,B)},
3147 comm_assoc_subs(A,conjunct), comm_assoc_subs(B,conjunct).
3148 comm_assoc_subs(disjunct(TA,TB),disjunct) --> !,
3149 {get_texpr_expr(TA,A), get_texpr_expr(TB,B)},
3150 comm_assoc_subs(A,disjunct), comm_assoc_subs(B,disjunct).
3151 comm_assoc_subs(add(TA,TB),add) --> !,
3152 {get_texpr_expr(TA,A), get_texpr_expr(TB,B)},
3153 comm_assoc_subs(A,add), comm_assoc_subs(B,add).
3154 comm_assoc_subs(multiplication(TA,TB),multiplication) --> !,
3155 {get_texpr_expr(TA,A), get_texpr_expr(TB,B)},
3156 comm_assoc_subs(A,multiplication), comm_assoc_subs(B,multiplication).
3157 comm_assoc_subs(union(TA,TB),union) --> !,
3158 {get_texpr_expr(TA,A), get_texpr_expr(TB,B)},
3159 comm_assoc_subs(A,union), comm_assoc_subs(B,union).
3160 comm_assoc_subs(intersection(TA,TB),intersection) --> !,
3161 {get_texpr_expr(TA,A), get_texpr_expr(TB,B)},
3162 comm_assoc_subs(A,intersection), comm_assoc_subs(B,intersection).
3163 comm_assoc_subs(Expr,Op) --> {nonvar(Op)},[Expr]. % base case for other operators
3164
3165 % detect just associative operators
3166 assoc_subs(concat(TA,TB),concat) --> !,
3167 {get_texpr_expr(TA,A), get_texpr_expr(TB,B)},
3168 assoc_subs(A,concat), assoc_subs(B,concat).
3169 assoc_subs(composition(TA,TB),composition) --> !,
3170 {get_texpr_expr(TA,A), get_texpr_expr(TB,B)},
3171 assoc_subs(A,composition), assoc_subs(B,composition).
3172 assoc_subs(Expr,Op) --> {nonvar(Op)},[Expr]. % base case for other operators
3173
3174 is_commutative(conjunct).
3175 is_commutative(disjunct).
3176 is_commutative(equivalence).
3177 is_commutative(equal).
3178 is_commutative(not_equal).
3179 is_commutative(add).
3180 is_commutative(multiplication).
3181 is_commutative(union).
3182 is_commutative(intersection).
3183
3184 % check if two type expressions are same modulo info fields and reordering of commutative operators
3185 % same_texpr does not reorder wrt commutativity.
3186 same_norm_texpr(TExpr1,TExpr2) :-
3187 ? strip_and_norm_ast(TExpr1,N1),
3188 strip_and_norm_ast(TExpr2,N1).
3189
3190
3191 % small utility to get functor of texpr:
3192 get_texpr_functor(b(E,_,_),F,N) :- !, functor(E,F,N).
3193 get_texpr_functor(E,_,+) :- add_error_fail(get_texpr_functor,'Not a typed expression: ',E).
3194
3195 % -------------------------
3196
3197 % check if a ProB type is a set type:
3198 is_set_type(set(Type),Type).
3199 is_set_type(seq(Type),couple(integer,Type)).
3200 % should we have a rule for any ?? : in all cases using is_set_type any seems not possible; better that we generate error message in get_set_type or get_texpr_set_type
3201 % is_set_type(any,any).
3202
3203 get_set_type(TypeX,Res) :-
3204 ? (is_set_type(TypeX,SetType) -> Res=SetType ; add_error_fail(get_set_type,'Not a set type: ',TypeX)).
3205
3206 get_texpr_set_type(X,Res) :- get_texpr_type(X,TypeX),
3207 get_set_type(TypeX,Res).
3208
3209
3210 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3211 % check if a set contains all elements of a type, i.e., maximal type
3212 is_just_type(Expr) :- is_just_type(Expr,[]).
3213 % is_just_type(+Expr,+RTT):
3214 % like is_just_type/1 but RTT is a list of identifiers (without type information)
3215 % of variables or constants that are known to be types, too.
3216 % E.g. is_just_type(a ** INTEGER) would fail but is_just_type(a ** INTEGER,[a]) would
3217 % succeed.
3218 is_just_type(b(E,T,I),RTT) :- is_just_type3(E,T,I,RTT).
3219
3220
3221 is_just_type3(identifier(G),SType,Infos,RefsToTypes) :-
3222 nonvar(SType), SType = set(Type), nonvar(Type),
3223 ( Type = global(G),
3224 memberchk(given_set,Infos) % no accidental local variable G that hides global G
3225 ; memberchk(G,RefsToTypes) -> true
3226 %; Type = freetype(G),
3227 % memberchk(given_set,Infos) % no accidental local variable G that hides global G
3228 % TODO: we do not know if the Freetype has restrictions (which are encoded in the PROPERTIES)
3229 ),!.
3230 is_just_type3(freetype_set(_),_,_,_).
3231 is_just_type3(pow_subset(E),_,_,RTT) :- is_just_type(E,RTT).
3232 is_just_type3(fin_subset(E),T,_,RTT) :-
3233 is_finite_type_in_context(proving,T), % animation or proving
3234 is_just_type(E,RTT).
3235 is_just_type3(integer_set('INTEGER'),set(integer),_,_).
3236 is_just_type3(bool_set,set(boolean),_,_).
3237 is_just_type3(real_set,set(real),_,_).
3238 is_just_type3(string_set,set(string),_,_).
3239 is_just_type3(cartesian_product(A,B),_,_,RTT) :-
3240 is_just_type(A,RTT),is_just_type(B,RTT).
3241 is_just_type3(mult_or_cart(A,B),_,_,RTT) :- % is_just_type/1 could be called before the cleanup
3242 is_just_type(A,RTT),is_just_type(B,RTT). % of an expression has finished
3243 is_just_type3(relations(A,B),_,_,RTT) :-
3244 is_just_type(A,RTT),is_just_type(B,RTT).
3245 is_just_type3(struct(b(rec(Fields),_,_)),_,_,RTT) :-
3246 maplist(field_is_just_type(RTT),Fields).
3247 is_just_type3(typeset,_,_,_).
3248 is_just_type3(comprehension_set(_,b(truth,_,_)),_,_,_).
3249 is_just_type3(set_extension([V1,V2]),_,_,_) :- get_texpr_boolean(V1,B1), % TODO: also deal with enumerated set elems
3250 (B1=boolean_true -> get_texpr_boolean(V2,boolean_false) ; B1=boolean_false -> get_texpr_boolean(V2,boolean_true)).
3251 is_just_type3(value(Val),ST,_,_) :- % e.g., {TRUE,FALSE} would usually get translated into this
3252 is_set_type(ST,Type), is_maximal_value(Val,Type). % also see: quick_is_definitely_maximal_set(Val).
3253
3254 field_is_just_type(RTT,field(_,Set)) :- is_just_type(Set,RTT).
3255
3256
3257 get_texpr_boolean(b(X,_,_),Res) :- is_boolan_expr(X,Res).
3258 is_boolan_expr(boolean_true,boolean_true).
3259 is_boolan_expr(boolean_false,boolean_false).
3260 is_boolan_expr(value(X),Res) :- nonvar(X), conv_bool_val(X,Res).
3261 conv_bool_val(pred_true,boolean_true).
3262 conv_bool_val(pred_false,boolean_false).
3263
3264 :- use_module(probsrc(custom_explicit_sets),[quick_definitely_maximal_set_avl/1]).
3265 is_maximal_value(V,_) :- var(V),!,fail.
3266 is_maximal_value(global_set(GS),Type) :- (GS=='INTEGER' -> true ; Type==global(GS)).
3267 % we could call is_maximal_global_set(GS) or b_global_set (but requires compiled)
3268 is_maximal_value(avl_set(A),Type) :-
3269 type_finite_and_pre_compiled(Type),
3270 quick_definitely_maximal_set_avl(A). % note: affects test 2392
3271
3272 :- use_module(probsrc(b_global_sets),[b_global_sets_precompiled/0, enumerated_sets_precompiled/0, enumerated_set/1]).
3273 type_finite_and_pre_compiled(boolean).
3274 type_finite_and_pre_compiled(global(GS)) :-
3275 (enumerated_set(GS) -> true % at least added with pre_register_enumerated_set_with_elems
3276 ; b_global_sets_precompiled).
3277 type_finite_and_pre_compiled(couple(A,B)) :- type_finite_and_pre_compiled(A), type_finite_and_pre_compiled(B).
3278 type_finite_and_pre_compiled(set(A)) :- type_finite_and_pre_compiled(A).
3279 % TODO: records?? less-likely we have an exhaustive list
3280
3281 % Generate a custom matching / visitor predicate
3282 % bsyntaxtree:gen_visitor(bexpr_variables_aux,bexpr_variables)
3283 /*
3284 gen_visitor(Pred, BodyPred) :- syntaxelement(Expr,SubsX,_NamesX,_Lists,_ConstantX,_),
3285 print_clause(Pred,BodyPred,Expr,SubsX),
3286 fail.
3287 gen_visitor(Pred, BodyPred) :- nl.
3288
3289 print_clause(Pred,BodyPred,Expr,SubsX) :- E=..[Op|SubsX], format('~w(~w) :- ',[Pred,Expr]).
3290 */
3291
3292 /*
3293 * create_recursive_compset(+Ids,+Cond,+Type,+Infos,-RecId,-TCompSet)
3294 * creates a recursive comprehension set:
3295 * Ids is the list of the introduced typed identifiers
3296 * Cond is the condition (a typed predicate)
3297 * Infos are additional informations for the comprehension set syntax element
3298 * RecId is the identifier (untyped, an atom) that can be used in Cond to refer to the
3299 * comprehension set recursively. Usually RecId is used in Cond as a variable
3300 * TCompSet is the generated recursive comprehension set, the recursion parameter is introduced
3301 * by a recusive(Id,CompSet) syntax element
3302 */
3303 create_recursive_compset(Ids,Cond,Type,Infos,RecId,TCompSet) :-
3304 unique_id("recursive.",RecId),
3305 add_symbolic_annotation(Infos,RInfos),
3306 create_texpr(comprehension_set(Ids,Cond),Type,RInfos,TCompSet1),
3307 create_typed_id(RecId,Type,TRecId),
3308 create_texpr(recursive_let(TRecId,TCompSet1),Type,[],TCompSet).
3309
3310 unique_typed_id(Prefix,Type,TId) :-
3311 unique_id(Prefix,Id),
3312 create_typed_id(Id,Type,TId).
3313
3314
3315 mark_bexpr_as_symbolic(b(E,T,I),b(E2,T,RI)) :-
3316 add_symbolic_annotation(I,RI),
3317 mark_aux(E,E2).
3318 mark_aux(union(A,B),R) :- !, R=union(SA,SB),
3319 mark_bexpr_as_symbolic(A,SA), mark_bexpr_as_symbolic(B,SB).
3320 % union is currently the only operator that is kept symbolically
3321 mark_aux(A,A).
3322
3323 add_symbolic_annotation([H|I],R) :- H == prob_annotation('SYMBOLIC'),!, R=[H|I].
3324 add_symbolic_annotation(I,R) :- !, R=[prob_annotation('SYMBOLIC')|I].
3325
3326 % identifier_sub_ast(+TExpr,+Identifier,-SubPosition):
3327 % Find occurences of an identifier "Identifier" in an expression "TExpr"
3328 % Returns a list of positions (beginning with 0) that describes the position of a sub-expression
3329 % that contains all occurrences of Identifier in TExpr.
3330 % E.g. [1,0,1] means "second sub-expression of TExpr, then the first sub-expression of that,
3331 % then the second sub-expression of that".
3332 % When an identifier has multiple occurences, the position of the sub-expression is returned
3333 % where all occurences of it are located.
3334 % If the identifier is not found, the call fails.
3335 % Sub-expressions are meant like the ones syntaxtraversion or syntaxtransformation return.
3336 identifier_sub_ast(TExpr,Identifier,SubPosition) :-
3337 syntaxtraversion(TExpr,Expr,_Type,_Infos,AllSubs,Names),
3338 identifier_sub_ast_aux(Expr,AllSubs,Names,Identifier,SubPosition).
3339 identifier_sub_ast_aux(identifier(Identifier),[],[],Identifier,[]) :- !.
3340 identifier_sub_ast_aux(_Expr,AllSubs,Names,Identifier,SubPosition) :-
3341 get_texpr_id(TId,Identifier),nonmember(TId,Names),
3342 % For each sub-expression E in the list AllSubs create a term Pos-E
3343 % where Pos is E's position (starting with 0) in AllSubs
3344 foldl(annotate_pos,AllSubs,AllAnnotatedSubs,0,_),
3345 % Introduced identifiers occur alsa as sub-expressions, remove those
3346 foldl(select_sub,Names,AllAnnotatedSubs,RealAnnSubs),
3347 convlist_max(identifier_sub_ast_aux2(Identifier),2,RealAnnSubs,SubPositions), % find at most 2 sols
3348 ( SubPositions = [SubPosition] -> true
3349 ; SubPositions = [_,_|_] -> % More then one occurrences - make this the found node
3350 SubPosition = []).
3351 identifier_sub_ast_aux2(Identifier,Pos-TExpr,[Pos|SubPosition]) :-
3352 identifier_sub_ast(TExpr,Identifier,SubPosition).
3353 annotate_pos(TExpr,I-TExpr,I,I2) :- I2 is I+1.
3354 select_sub(Name,AnnotatedSubs,Result) :-
3355 selectchk(_Pos-Name,AnnotatedSubs,Result).
3356
3357
3358
3359 % exchange_ast_position(+SubPosition,+OldTExpr,-OldInner,+NewInner,-NewTExpr):
3360 % exchanges a sub-expression in the expression "OldTExpr".
3361 % SubPosition is a list of positions like identifier_sub_ast/3 returns it.
3362 % OldInner is the sub-expression found in OldTExpr.
3363 % NewInner is the new sub-expression.
3364 % NewTExpr is the new expression that originates from replacing OldInner by NewInner.
3365 exchange_ast_position([],Old,Old,New,New).
3366 exchange_ast_position([Pos|RestPos],OldTExpr,OldInner,NewInner,NewTExpr) :-
3367 remove_bt_and_used_ids(OldTExpr,OldExpr,NewExpr,NewTExpr), % also invalidates used_ids info
3368 ? syntaxtransformation(OldExpr,Subs,_Names,NSubs,NewExpr),
3369 nth0(Pos,Subs, OldSelected,Rest),
3370 nth0(Pos,NSubs,NewSelected,Rest),
3371 ? exchange_ast_position(RestPos,OldSelected,OldInner,NewInner,NewSelected).
3372
3373
3374 % -----------------------
3375 % utility to expand / inline all let expressions and let predicates:
3376 % useful for tools that cannot handle the lets
3377
3378 expand_all_lets(Expr,NewExpr) :-
3379 transform_bexpr(tl_expand_lets,Expr,NewExpr).
3380
3381 tl_expand_lets(b(E,_,_),Res) :- tl_expand_lets2(E,Res).
3382 tl_expand_lets2(let_expression(Ids,Exprs,Body),NewBody) :- % expand LET expression
3383 replace_ids_by_exprs(Body,Ids,Exprs,NewBody).
3384 tl_expand_lets2(let_predicate(Ids,Exprs,Body),NewBody) :- % expand LET predicate
3385 replace_ids_by_exprs(Body,Ids,Exprs,NewBody).
3386
3387 % -----------------------
3388
3389 :- public check_used_ids/2.
3390 % a simple checker, only checks used_ids info fields for entire typed expression:
3391 check_used_ids(TExpr,PP) :- %format('CHECK AST for ~w~n',[PP]),
3392 map_over_typed_bexpr(check_used_ids_texpr_fail(PP),TExpr).
3393 check_used_ids(_,_).
3394 check_used_ids_texpr_fail(PP,E) :- check_used_ids_texpr(PP,E),!,fail.
3395 check_used_ids_texpr(PP,b(P,T,I)) :- member(used_ids(UIds1),I),!,
3396 (find_identifier_uses(b(P,T,I),[],UIds2) -> true
3397 ; add_internal_error('find_identifier_uses failed',PP),fail),
3398 (UIds1==UIds2 -> true
3399 ; format('*** Wrong used_ids Info (~w)!!~n Used_ids: ~w~n Comp_ids: ~w~n',[PP,UIds1,UIds2]),
3400 translate:print_bexpr(b(P,T,I)),nl,
3401 add_error(check_used_ids,'Wrong used_ids: ',PP,I)
3402 ).
3403 check_used_ids_texpr(_,_).
3404
3405 % repair any broken used_ids info in typed expression TExpr and re-compute used_ids if necessary
3406 % PP is a program point, will be reported in case of an error
3407 repair_used_ids(PP,TExpr,Res) :-
3408 (transform_bexpr(bsyntaxtree:repair_used_ids_info(PP),TExpr,NewTExpr) -> Res=NewTExpr
3409 ; add_internal_error('Repairing used_ids failed:',PP),
3410 Res=TExpr).
3411
3412 % we could also simply call recompute_used_ids_inf; but it would not generate any messages
3413 repair_used_ids_info(PP,b(P,T,I),b(P,T,NI)) :- %functor(P,FF,_), print(repair(FF)),nl,
3414 ? select(used_ids(OldUsed),I,I2),!,
3415 (find_identifier_uses(b(P,T,I),[],NewUsed)
3416 -> (NewUsed=OldUsed -> NI=I
3417 ; NI = [used_ids(NewUsed)|I2],
3418 add_message(repair_used_ids,'Updating used_ids for: ',b(P,T,I),I2)
3419 )
3420 ; add_internal_error('find_identifier_uses failed',PP),
3421 NI=I
3422 ).
3423 repair_used_ids_info(PP,b(P,T,I),b(P,T,NI)) :-
3424 requires_used_ids(P),
3425 (find_identifier_uses(b(P,T,I),[],NewUsed) -> true
3426 ; add_internal_error('find_identifier_uses failed',PP),fail
3427 ),
3428 !,
3429 NI=[used_ids(NewUsed)|I].
3430 repair_used_ids_info(_,B,B).
3431
3432 requires_used_ids(exists(_,_)).
3433 requires_used_ids(forall(_,_,_)).
3434
3435 % a simple checker to see if an AST is well-formed:
3436 % can be tested e.g. as follows: b_get_invariant_from_machine(I), check_ast(I).
3437 % called in prob_safe_mode by clean_up_section
3438
3439 check_ast(TE) :- check_ast(false,TE).
3440 check_ast(AllowVars,TExpr) :- %nl,print('CHECK AST'),nl,
3441 map_over_typed_bexpr(check_ast_texpr(AllowVars),TExpr).
3442 check_ast(_,_).
3443
3444 :- use_module(typing_tools,[valid_ground_type/1]).
3445 %check_ast_texpr(X) :- print(check(X)),nl,fail.
3446 check_ast_texpr(AllowVars,AST) :- AST = b(E,Type,Infos),
3447 (debug:debug_level_active_for(9) -> write(' check_ast: '),print_bexpr(AST), write(' :: '), write(Type), nl ; true),
3448 (check_expr(E,Type,Infos) -> true
3449 ; add_error(check_ast_texpr,'Invalid Expr: ', AST) %, trace, check_expr(E,Type,Infos)
3450 ),
3451 (check_type(Type,AllowVars) -> true
3452 ; add_error(check_ast_texpr,'Invalid Type for: ',AST,Infos)),
3453 safe_functor(E,F),
3454 check_ast_typing(E,Type,Infos),
3455 (check_infos(Infos,F) -> true ; add_error(check_ast_texpr,'Invalid Infos: ',AST)),
3456 check_special_rules(E,Type,Infos),
3457 fail. % to force backtracking in map_over_typed_bexpr
3458
3459
3460 check_special_rules(operation_call_in_expr(Operation,_),_,OInfos) :- !,
3461 get_texpr_info(Operation,Info), % reads info important for used_ids computation
3462 (memberchk(reads(_V),Info) -> true
3463 ; add_error(check_ast_texpr,'Missing reads info: ',Operation,OInfos)).
3464
3465
3466 safe_functor(V,R) :- var(V),!,R='$VAR'.
3467 safe_functor(E,F/N) :- functor(E,F,N).
3468
3469 % check whether the type term is ok
3470 check_type(X,AllowVars) :- var(X),!,
3471 (AllowVars==true -> true ; add_error(check_type,'Variable type: ',X),fail).
3472 check_type(pred,_) :- !.
3473 check_type(subst,_) :- !.
3474 check_type(op(Paras,Returns),AllowVars) :- !,
3475 maplist(check_normal_type(AllowVars),Paras),
3476 maplist(check_normal_type(AllowVars),Returns).
3477 check_type(T,AllowVars) :- check_normal_type(AllowVars,T).
3478
3479 check_normal_type(AllowVars,T) :-
3480 (AllowVars \== true -> valid_ground_type(T)
3481 ; ground(T) -> valid_ground_type(T)
3482 ; true). % TO DO: call valid_ground_type but pass AllowVars
3483
3484 :- use_module(probsrc(btypechecker), [lookup_type_for_expr/2, unify_types_werrors/4]).
3485 % check whether type is compatible with operators
3486 check_ast_typing(member(A,B),Type,Pos) :- !,
3487 get_texpr_type(B,TB), check_set_type(TB,member,Pos),
3488 check_type(Type,pred,member),
3489 get_texpr_type(A,TA),
3490 unify_types_werrors(set(TA),TB,Pos,member).
3491 check_ast_typing(not_equal(A,B),Type,Pos) :- !, check_ast_typing(equal(A,B),Type,Pos).
3492 check_ast_typing(equal(A,B),Type,Pos) :- !,
3493 get_texpr_type(B,TB),
3494 get_texpr_type(A,TA),
3495 unify_types_werrors(TA,TB,Pos,'='),
3496 (non_value_type(TA)
3497 -> add_error(check_ast_typing,'Binary predicate has to have values as arguments:',TA,Pos)
3498 ; Type=pred -> true
3499 ; add_error(check_ast_typing,'Illegal type for binary predicate:',Type,Pos)
3500 ).
3501 check_ast_typing(greater_equal(A,B),Type,_) :- !,
3502 get_texpr_type(A,TA),check_type(TA,integer,greater_equal),
3503 get_texpr_type(B,TB),check_type(TB,integer,greater_equal), check_type(Type,pred,member).
3504 check_ast_typing(Expr,Type,Pos) :-
3505 syntaxtransformation(Expr,Subs,Names,NSubs,NewExpr),
3506 check_names(Names,Pos),
3507 (lookup_type(NewExpr,T) -> true
3508 ; add_warning(check_ast_typing,'Unable to lookup type for: ',NewExpr),
3509 fail
3510 ),
3511 !,
3512 (unify_types_werrors(Type,T,Pos,'check_ast')
3513 -> maplist(check_sub_type(Expr,Pos),Subs,NSubs)
3514 ; add_error(check_ast_typing,'Type mismatch for expression:',Expr,Pos)
3515 ).
3516 check_ast_typing(_,subst,_) :- !. % ignore subst for the moment
3517 check_ast_typing(operation(_TName,_Res,_Params,_TBody),_,_) :- !. % ignore operations for the moment
3518 check_ast_typing(Expr,_,Pos) :-
3519 syntaxtransformation(Expr,_,_Names,_,_NewExpr),!,
3520 add_message(check_ast_typing,'Cannot lookup type for expression: ',Expr,Pos).
3521 check_ast_typing(Expr,_,Pos) :-
3522 add_message(check_ast_typing,'No applicable type rule for expression: ',Expr,Pos).
3523
3524 non_value_type(X) :- var(X),!,fail.
3525 non_value_type(pred).
3526 non_value_type(subst).
3527 non_value_type(op(_)).
3528
3529
3530 check_names([],_).
3531 check_names([H|T],Pos) :-
3532 (member(H,T) -> add_error(check_ast_name,'Duplicate name:',H,Pos) ; check_names(T,Pos)).
3533
3534 check_sub_type(OuterExpr,Pos,Arg,Type) :- get_texpr_type(Arg,T),!,
3535 (unify_types_werrors(Type,T,Pos,'check_sub_type') -> true
3536 ; add_error(check_ast_typing,'Type mismatch for sub-expression:',Arg,Pos),
3537 write('Outer expression: '),translate:print_bexpr(OuterExpr),nl,
3538 write('Outer type: '),write(Type),nl,
3539 write('Arg type: '),write(T),nl,print(type(T)),nl, tools_printing:print_term_summary(Arg),nl,trace
3540 ).
3541 check_sub_type(_,Pos,Arg,_) :-
3542 add_error(check_ast_typing,'Cannot extract type: ',Arg,Pos).
3543
3544 lookup_type(identifier(_),_) :- !. % ignore typing issues for identifiers
3545 lookup_type(Expr,Type) :- lookup_type_for_expr(Expr,Type).
3546
3547 check_set_type(Var,_,_) :- var(Var),!.
3548 check_set_type(set(_),_,_) :- !.
3549 check_set_type(seq(_),_,_) :- !.
3550 check_set_type(Type,Func,Pos) :- add_error(check_ast_typing,'Invalid type for operator: ',Func:Type,Pos).
3551
3552 check_type(Type,Type,_) :- !.
3553 check_type(Type,_,Func) :- add_error(check_ast_typing,'Unexpected type for operator: ',Func:Type).
3554
3555 check_infos(X,F) :- var(X),!, add_error(check_infos,'Info field list not terminated: ',F:X),fail.
3556 check_infos([],_).
3557 check_infos([H|_],F) :- \+ ground(H),!, add_error(check_infos,'Info field not ground: ',F:H),fail.
3558 check_infos([[H|T]|_],F) :- !, add_error(check_infos,'Info field contains nested list: ',F:[H|T]),fail.
3559 check_infos([cse_used_ids(H)|T],F) :- member(cse_used_ids(H2),T),!,
3560 add_error(check_infos,'Multiple cse_used_ids entries: ',F:[H,H2]),fail.
3561 check_infos([used_ids(H)|T],F) :- member(used_ids(H2),T),!,
3562 add_error(check_infos,'Multiple used_ids entries: ',F:[H,H2]),fail.
3563 check_infos([nodeid(N1)|T],F) :- member(nodeid(N2),T),!,
3564 add_error(check_infos,'Multiple nodeid entries: ',F:[N1,N2],[nodeid(N1)]),fail.
3565 check_infos([removed_typing|T],F) :- member(removed_typing,T),!,
3566 add_error(check_infos,'Multiple removed_typing entries: ',F,T),fail.
3567 check_infos([_|T],F) :- check_infos(T,F).
3568
3569 check_expr(Expr,Type,Infos) :- nonmember(contains_wd_condition,Infos),
3570 sub_expression_contains_wd_condition(Expr,Sub),
3571 TE = b(Expr,Type,Infos),
3572 (Type = subst
3573 -> fail % AST cleanup is not called for substitutions; WD-info not available for substitutions at the moment
3574 ; translate_bexpression(TE,PS)),
3575 functor(Expr,Functor,_),
3576 functor(Sub,SubFunctor,_),
3577 tools:ajoin(['Node for AST node ',Functor,' does not contain WD info from Subexpression ',SubFunctor,' :'],Msg),
3578 add_warning(check_expr,Msg,PS,TE).
3579 % well_def_analyser:nested_print_wd_bexpr(TE),nl.
3580 % TODO: check when we have an unnecessary WD condition
3581 check_expr(Expr,Type,Infos) :- nonmember(contains_wd_condition,Infos),
3582 always_not_wd_top(Expr),
3583 add_warning(check_expr,'AST is not well-defined but does not contain WD info: ',b(Expr,Type,Infos),Infos).
3584 check_expr(member(LHS,RHS),Type,Infos) :- is_just_type(RHS),
3585 get_preference(optimize_ast,true),
3586 !,
3587 TE = b(member(LHS,RHS),Type,Infos),
3588 translate:translate_bexpression(TE,PS),
3589 add_warning(check_expr,'AST contains redundant typing predicate: ',PS,TE).
3590 check_expr(identifier(ID),_,_) :- illegal_id(ID),!,
3591 add_error(check_infos,'Illegal identifier: ', identifier(ID)).
3592 check_expr(lazy_lookup_expr(ID),_,_) :- illegal_id(ID),!,
3593 add_error(check_infos,'Illegal identifier: ', lazy_lookup_expr(ID)).
3594 check_expr(lazy_lookup_pred(ID),_,_) :- illegal_id(ID),!,
3595 add_error(check_infos,'Illegal identifier: ', lazy_lookup_pred(ID)).
3596 check_expr(exists(Parameters,Condition),pred,Infos) :- !,
3597 check_used_ids(exists,Parameters,Condition,Infos,_Used).
3598 check_expr(forall(Parameters,LHS,RHS),pred,Infos) :- !,
3599 create_implication(LHS,RHS,Condition),
3600 check_used_ids(forall,Parameters,Condition,Infos,_Used). %
3601 check_expr(value(V),Type,_) :- !, check_bvalue(V,Type).
3602 check_expr(_,_,_).
3603
3604 % will check all used_ids fields (not just for exists and forall)
3605 :- public check_used_ids_in_ast/1.
3606 check_used_ids_in_ast(closure(_,_,TExpr)) :- !, (map_over_typed_bexpr(check_used_ids_aux,TExpr) ; true).
3607 check_used_ids_in_ast(TExpr) :- map_over_typed_bexpr(check_used_ids_aux,TExpr).
3608 check_used_ids_in_ast(_).
3609
3610 check_used_ids_aux(AST) :- AST = b(_,_,Infos),
3611 ? member(used_ids(_),Infos),!,
3612 find_identifier_uses_if_necessary(AST,[],_), % will perform check
3613 fail.
3614
3615 % --------------------
3616
3617 :- use_module(specfile,[eventb_mode/0, z_or_tla_minor_mode/0]).
3618 % check if an expression is definitely not WD; looking at the top-level operator only
3619 always_not_wd_top(function(X,_)) :- definitely_empty_set(X). % TODO: detect a few more cases, e.g., arg not in dom
3620 always_not_wd_top(power_of(X,Y)) :- (get_integer(Y,VY), VY < 0 -> true
3621 ; eventb_mode, get_integer(X,VX), VX < 0).
3622 always_not_wd_top(div(_,Val)) :- get_integer(Val,VV), VV==0.
3623 always_not_wd_top(modulo(X,Y)) :-
3624 (get_integer(Y,VY), VY=<0
3625 -> true % there seems to be a def for Z in Z Live, cf modulo2
3626 ; get_integer(X,VX), VX<0, \+ z_or_tla_minor_mode).
3627 always_not_wd_top(min(X)) :- definitely_empty_set(X).
3628 always_not_wd_top(max(X)) :- definitely_empty_set(X).
3629 always_not_wd_top(size(X)) :- definitely_not_sequence(X). % TODO: detect infinite sets; also for card(_)
3630 always_not_wd_top(first(X)) :- definitely_not_non_empty_sequence(X).
3631 always_not_wd_top(front(X)) :- definitely_not_non_empty_sequence(X).
3632 always_not_wd_top(last(X)) :- definitely_not_non_empty_sequence(X).
3633 always_not_wd_top(tail(X)) :- definitely_not_non_empty_sequence(X).
3634 always_not_wd_top(general_intersection(X)) :- definitely_empty_set(X).
3635
3636 definitely_not_non_empty_sequence(X) :-
3637 (definitely_empty_set(X) -> true ; definitely_not_sequence(X)).
3638
3639 :- use_module(avl_tools,[avl_min_pair/3]).
3640 definitely_not_sequence(b(value(A),_,_)) :- nonvar(A), A=avl_set(AVL),
3641 avl_min_pair(AVL,int(StartIndex),_), StartIndex \= 1.
3642 % TODO: treat set_extension
3643
3644 :- use_module(b_ast_cleanup,[check_used_ids_info/4]).
3645 check_used_ids(Quantifier,Parameters,Condition,Infos,Used) :-
3646 ? select(used_ids(Used),Infos,Rest)
3647 -> check_used_ids_info(Parameters,Condition,Used,Quantifier), %% comment in to check used_ids field
3648 (member(used_ids(_),Rest)
3649 -> add_internal_error('Multiple used_ids info fields:',Parameters:Infos) ; true)
3650 ;
3651 add_internal_error(
3652 'Expected information of used identifiers information',Quantifier:Parameters:Infos).
3653
3654 illegal_id(ID) :- var(ID),!.
3655 illegal_id(op(ID)) :- !, \+ atom(ID).
3656 illegal_id(ID) :- \+ atom(ID).
3657
3658 :- use_module(btypechecker, [unify_types_strict/2, couplise_list/2]).
3659 :- use_module(avl_tools,[check_is_non_empty_avl/1]).
3660 % TO DO: we could check type more
3661 check_bvalue(V,_) :- var(V),!.
3662 check_bvalue(avl_set(A),Type) :- !, unify_types_strict(Type,set(_)),
3663 check_is_non_empty_avl(A).
3664 check_bvalue(closure(_,T,B),Type) :- !,
3665 couplise_list(T,CT), unify_types_strict(set(CT),Type),
3666 check_ast(B).
3667 check_bvalue(_,_).
3668
3669 % -----------------------
3670
3671
3672 indent_ws(X) :- X<1,!.
3673 indent_ws(X) :- print(' '), X1 is X-1, indent_ws(X1).
3674
3675 print_ast_td(b(E,T,I),Level,L1) :-
3676 indent_ws(Level),
3677 (E=identifier(_)
3678 -> format('~w (~w) -> ~w~n',[E,T,I])
3679 ; functor(E,F,N),
3680 format('~w/~w (~w) -> ~w~n',[F,N,T,I])
3681 ),
3682 L1 is Level+1.
3683 print_ast(TExpr) :-
3684 (map_over_typed_bexpr_top_down_acc(print_ast_td,TExpr,0),fail ; true).
3685
3686 % ---------------------
3687
3688 :- dynamic count_id_usage/2.
3689 single_usage_id_count(Expr) :- uses_an_identifier(Expr,Id),
3690 retract(count_id_usage(Id,Count)),
3691 !,
3692 Count=0,
3693 C1 is Count+1,
3694 assertz(count_id_usage(Id,C1)).
3695 single_usage_id_count(_).
3696
3697 % check if an identifier is used at most once
3698 single_usage_identifier(ID,ExprOrPredicates,Count) :-
3699 retractall(count_id_usage(_,_)),
3700 assertz(count_id_usage(ID,0)),
3701 % TO DO: take care of naming; do not count occurences when we enter scope defining ID
3702 maplist(single_usage_cnt,ExprOrPredicates),
3703 retract(count_id_usage(ID,Count)).
3704
3705 single_usage_cnt(ExprOrPredicate) :- map_over_full_bexpr_no_fail(single_usage_id_count,ExprOrPredicate).
3706
3707 gen_fresh_id_if_necessary(Default,Expr,FreshID) :-
3708 occurs_in_expr(Default,Expr),!,
3709 gensym('__FRESH_ID__',FreshID). % assumes _Fresh_XXX not used
3710 gen_fresh_id_if_necessary(Default,_,Default).
3711
3712 %% rewrite_if_then_else_expr_to_b(IfThenElseExpr, NExpr).
3713 % Rewrite if-then-else expr to B as understood by Atelier-B.
3714 % {d,x| d:BOOL & If => x=Then & not(if) => x=Else}(TRUE)
3715 rewrite_if_then_else_expr_to_b(if_then_else(If,Then,Else), NExpr) :-
3716 get_texpr_type(Then,Type),
3717 ARG = b(boolean_true,boolean,[]), AT=boolean, % we could use unit type or BOOL here
3718 gen_fresh_id_if_necessary('_zzzz_unary',b(if_then_else(If,Then,Else),Type,[]),AID1),
3719 gen_fresh_id_if_necessary('_zzzz_binary',b(if_then_else(If,Then,Else),Type,[]),AID2),
3720 safe_create_texpr(identifier(AID1), AT, [], Id1), % a dummy argument
3721 safe_create_texpr(identifier(AID2), Type, [], Id2), % The result
3722 safe_create_texpr(equal(Id2,Then), pred, [], Eq1),
3723 safe_create_texpr(equal(Id2,Else), pred, [], Eq2),
3724 safe_create_texpr(implication(If,Eq1), pred, [], Pred1),
3725 safe_create_texpr(negation(If), pred, [], NIf),
3726 safe_create_texpr(implication(NIf,Eq2), pred, [], Pred2),
3727 safe_create_texpr(conjunct(Pred1,Pred2), pred, [], Pred),
3728 safe_create_texpr(comprehension_set([Id1,Id2],Pred), set(couple(AT,Type)), [], FUN),
3729 NExpr = function(FUN,ARG).
3730
3731
3732 % --------------------
3733
3734 % apply normalisation rules from Atlier-B PP/ML provers
3735 % see chapter 3 of Atelier-B prover manual
3736
3737 normalise_bexpr_for_ml(TExpr,Res) :-
3738 transform_bexpr(normalise_bexpr,TExpr,Res).
3739
3740 normalise_bexpr(b(E,T,I),b(E2,T,I)) :- norm2(E,E2),!.
3741
3742 norm2(equivalence(A,B),conjunct(TIMP1,TIMP2)) :- !,
3743 safe_create_texpr(implication(A,B),pred,TIMP1),
3744 safe_create_texpr(implication(B,A),pred,TIMP2).
3745 norm2(subset_strict(A,B),conjunct(TMEM,TNEQ)) :- !,
3746 norm2(subset(A,B),MEM), safe_create_texpr(MEM,pred,TMEM),
3747 safe_create_not_equal(A,B,TNEQ).
3748 norm2(subset(A,B),member(A,PowB)) :- !, % A <: B <===> A:POW(B)
3749 get_texpr_type(A,TA),
3750 safe_create_texpr(pow_subset(B),TA,PowB).
3751 norm2(not_equal(A,B),negation(TEQ)) :- !,
3752 safe_create_texpr(equal(A,B),pred,TEQ).
3753 norm2(not_member(A,B),negation(TMEM)) :- !,
3754 safe_create_texpr(member(A,B),pred,TMEM).
3755 norm2(not_subset(A,B),negation(TMEM)) :- !,
3756 norm2(subset(A,B),MEM),safe_create_texpr(MEM,pred,TMEM).
3757 norm2(not_subset_strict(A,B),implication(TMEM,TEQ)) :- !, % A /<< : B <===> A:POW(B) => A=B
3758 norm2(subset(A,B),MEM),safe_create_texpr(MEM,pred,TMEM),
3759 safe_create_texpr(equal(A,B),pred,TEQ).
3760 norm2(POW1,set_subtraction(TPOW,TSEMPTY)) :- not_empty_pow(POW1,A,POW), !,
3761 % POW1(A) <===> POW(A) - {{}}, FIN1(A) <===> FIN(A) - {{}}, ...
3762 safe_create_texpr(POW,pred,TPOW),
3763 get_texpr_type(A,TA), TEMPTY = b(empty_set,TA,[]),
3764 safe_create_texpr(set_extension([TEMPTY]),set(TA),TSEMPTY).
3765 norm2(member(A,b(integer_set('NATURAL'),_,_)),conjunct(TMEM,TLEQ)) :- !, % A <: NATURAL <===> A:INTEGER & 0 <= A
3766 INTEGER = b(integer_set('INTEGER'),set(integer),[]),
3767 safe_create_texpr(member(A,INTEGER),pred,TMEM),
3768 Zero = b(integer(0),integer,[]),
3769 safe_create_texpr(less_equal(Zero,A),pred,TLEQ).
3770 norm2(set_extension(List),Union) :- List = [H|T], T=[_|_], !, % {A,B} <===> {A} \/ {B}
3771 get_texpr_type(H,Type),
3772 set_extension_to_union(H,T,set(Type),b(Union,_,_)).
3773 norm2(greater_equal(A,B),less_equal(B,A)) :- !.
3774 norm2(greater(A,B),less_equal(B1,A)) :- !, plus1(B,B1).
3775 norm2(less(A,B),less_equal(A,B1)) :- !, minus1(B,B1). % the normalisation rule in chapter 3 is actually false
3776 norm2(integer_set(NAT1),set_subtraction(TNAT,TSZero)) :- nat1(NAT1,NAT), !, % NATURAL1 <===> NATURAL - {0}
3777 TNAT = b(integer_set(NAT),set(integer),[]),
3778 set_with_zero(TSZero).
3779 norm2(empty_sequence,empty_set) :- !.
3780 norm2(perm(A),intersection(ISEQ,PSURJ)) :- !, % perm(A) <===> iseq(A) /\ (NATURAL-{0} +->> A)
3781 get_texpr_type(A,TA),
3782 safe_create_texpr(iseq(A),set(seq(TA)),ISEQ),
3783 set_with_zero(TSZero),
3784 NATURAL = b(integer_set('NATURAL'),set(integer),[]),
3785 safe_create_texpr(set_subtraction(NATURAL,TSZero),set(integer),DOM),
3786 safe_create_texpr(partial_surjection(DOM,A),set(seq(TA)),PSURJ).
3787 % TODO: total_relation, if_then_else, ...?
3788
3789 set_with_zero(TSZero) :- % {0}
3790 TZero = b(integer(0),TA,[]),
3791 safe_create_texpr(set_extension([TZero]),set(TA),TSZero).
3792
3793 % TODO: more intelligent versions like x-1 ==> x ...
3794 plus1(A,Plus1) :- One = b(integer(1),integer,[]),
3795 safe_create_texpr(add(A,One),integer,Plus1).
3796 minus1(A,Plus1) :- One = b(integer(1),integer,[]),
3797 safe_create_texpr(minus(A,One),integer,Plus1).
3798
3799 not_empty_pow(pow1_subset(A),A,pow_subset(A)).
3800 not_empty_pow(fin1_subset(A),A,fin_subset(A)).
3801 not_empty_pow(seq1(A),A,seq(A)).
3802 not_empty_pow(iseq1(A),A,iseq(A)).
3803
3804 nat1('NATURAL1','NATURAL').
3805 nat1('NAT1','NAT').
3806
3807 safe_create_not_equal(A,B,TNEQ) :-
3808 safe_create_texpr(equal(A,B),pred,TEQ),
3809 safe_create_texpr(negation(TEQ),pred,TNEQ).
3810
3811 set_extension_to_union(H,[],Type,Res) :- !,
3812 safe_create_texpr(set_extension([H]),Type,Res).
3813 set_extension_to_union(H,[H2|T],Type,Res) :-
3814 safe_create_texpr(set_extension([H]),Type,TH),
3815 set_extension_to_union(H2,T,Type,TUnion),
3816 safe_create_texpr(union(TH,TUnion),Type,Res).