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