| 1 | | % (c) 2009-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, |
| 2 | | % Heinrich Heine Universitaet Duesseldorf |
| 3 | | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) |
| 4 | | |
| 5 | | :- module(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 | | same_id/3, % true if two typed identifiers have the same id |
| 16 | | get_texpr_exprs/2, % list variant of the above |
| 17 | | get_texpr_types/2, % list variant of the above |
| 18 | | get_texpr_infos/2, % list variant of the above |
| 19 | | get_texpr_ids/2, % list variant of the above |
| 20 | | get_texpr_pos/2, % get the position of a typed expression |
| 21 | | extract_pos_infos/2, % get the position info sub list of an info list |
| 22 | | copy_pos_infos/3, % copy position infos from one typed expression to another |
| 23 | | merge_info/3, % merge two information lists as well as possible |
| 24 | | update_infos/3, % provide updates to an existing info list |
| 25 | | get_info_pos/2, % get the position directly from info field |
| 26 | | contains_info_pos/1, % true if info field contains position infos |
| 27 | | |
| 28 | | same_texpr/2, % check if two typed expressions are equal modulo Info fields |
| 29 | | different_texpr_values/2, % check if two type expressions are WD and definitely denote different values |
| 30 | | |
| 31 | | create_texpr/4, % creates a typed expression by giving expression, type and infos |
| 32 | | add_texpr_infos/3, % adds some more information to a typed expression at front |
| 33 | | add_texpr_info_if_new/3, % adds one info field to typed B expression info list at front if it is new |
| 34 | | add_texpr_infos_if_new/3, % ditto but list of infos can be added |
| 35 | | add_info_if_new/3, % adds to info list |
| 36 | | safe_create_texpr/3, % a version of create_texpr which extracts wd-info from sub-expressionssafe_create_texpr |
| 37 | | safe_create_texpr/4, |
| 38 | | sub_expression_contains_wd_condition/1, % utility to check if sub-expression contains wd condition |
| 39 | | |
| 40 | | get_rodin_name/2, get_rodin_model_name/2, get_texpr_label/2, get_texpr_labels/2, |
| 41 | | get_texpr_description/2, % get @desc pragma for typed expression |
| 42 | | info_has_ignore_pragma/1, % check if an info list has an ignore pragma |
| 43 | | always_well_defined/1, always_well_defined_or_disprover_mode/1, |
| 44 | | is_truth/1, is_falsity/1, |
| 45 | | conjunct_predicates/2, |
| 46 | | conjunct_predicates_with_pos_info/3, |
| 47 | | is_a_conjunct/3, is_a_conjunct_without_label/3, decompose_conjunct/3, |
| 48 | | is_a_disjunct/3, is_an_implication/3, is_an_equivalence/3, is_a_negation/2, |
| 49 | | conjunction_to_list/2, member_in_conjunction/2, select_member_in_conjunction/3, |
| 50 | | member_in_conjunction_cse/3, |
| 51 | | disjunct_predicates/2, |
| 52 | | disjunction_to_list/2, |
| 53 | | is_a_disjunct_or_implication/4, |
| 54 | | |
| 55 | | predicate_components/2, % split a predicate into components which use distinct identifiers |
| 56 | | predicate_components_in_scope/3, % ditto with an optional list of local variables |
| 57 | | predicate_components_with_restriction/4, |
| 58 | | predicate_identifiers/2, predicate_identifiers_in_scope/3, |
| 59 | | |
| 60 | | project_predicate_on_identifiers/5, |
| 61 | | |
| 62 | | find_identifier_uses/3, find_identifier_uses_l/3, |
| 63 | | find_typed_identifier_uses/3, find_typed_identifier_uses/2, |
| 64 | | find_typed_identifier_uses_l/3, |
| 65 | | get_global_identifiers/1, |
| 66 | | occurs_in_expr/2, some_id_occurs_in_expr/2, |
| 67 | | single_usage_identifier/3, |
| 68 | | |
| 69 | | create_exists/3, create_exists_or_let_predicate/3, |
| 70 | | create_exists_opt/3, create_exists_opt/4, create_exists_opt/5, |
| 71 | | create_forall/3, |
| 72 | | create_negation/2, is_negation_of/2, |
| 73 | | create_implication/3, |
| 74 | | create_equivalence/3, |
| 75 | | create_couple/3, create_couple/2, |
| 76 | | |
| 77 | | detect_global_predicates/4, |
| 78 | | |
| 79 | | definitely_not_empty_set/1, |
| 80 | | |
| 81 | | replace_id_by_expr/4, |
| 82 | | replace_ids_by_exprs/4, |
| 83 | | remove_used_id_from_info/3, % remove an id from used_id info field if it exists |
| 84 | | remove_used_ids_from_info/3, % remove list of ids (order of args different !) |
| 85 | | |
| 86 | | rename_bt/3, % a simplified version of replace_ids_by_exprs, which assumes target of renamings are variables |
| 87 | | rename_bt_l/3, |
| 88 | | remove_bt/4, |
| 89 | | syntaxtransformation/5, |
| 90 | | |
| 91 | | map_over_bexpr/2, map_over_typed_bexpr/2, map_over_typed_bexpr/3, |
| 92 | | map_over_bexpr_top_down_acc/3, map_over_type_bexpr_top_down_acc/3, |
| 93 | | reduce_over_bexpr/4, |
| 94 | | transform_bexpr/3, transform_bexpr_with_bup_accs/5, transform_bexpr_with_acc/5, |
| 95 | | uses_implementable_integers/1, |
| 96 | | min_max_integer_value_used/3, min_max_integer_value_used/5, |
| 97 | | syntaxtraversion/6, |
| 98 | | safe_syntaxelement/5, |
| 99 | | |
| 100 | | remove_all_infos/2, extract_info/2, extract_info/3, |
| 101 | | bsyntax_pattern/2, |
| 102 | | |
| 103 | | remove_all_infos_and_ground/2, |
| 104 | | |
| 105 | | check_if_typed_predicate/1, |
| 106 | | check_if_typed_expression/1, |
| 107 | | check_if_typed_substitution/1, |
| 108 | | |
| 109 | | strip_and_norm_ast/2, |
| 110 | | same_norm_texpr/2, |
| 111 | | |
| 112 | | is_set_type/2, get_set_type/2, get_texpr_set_type/2, |
| 113 | | is_just_type/1, is_just_type/2, |
| 114 | | |
| 115 | | create_recursive_compset/6, |
| 116 | | unique_typed_id/3, |
| 117 | | mark_bexpr_as_symbolic/2, |
| 118 | | |
| 119 | | identifier_sub_ast/3, exchange_ast_position/5, |
| 120 | | |
| 121 | | has_declared_identifier/2, add_declaration_for_identifier/3, |
| 122 | | check_ast/1, check_ast/2, |
| 123 | | print_ast/1 |
| 124 | | ]). |
| 125 | | |
| 126 | | % meta_predicate annotations should appear before loading any code: |
| 127 | | |
| 128 | | :- meta_predicate map_over_full_bexpr_no_fail(1,?). |
| 129 | | |
| 130 | | :- meta_predicate map_over_bexpr(1,?). |
| 131 | | :- meta_predicate map_over_typed_bexpr(1,?). |
| 132 | | :- meta_predicate map_over_typed_bexpr(2,?,?). |
| 133 | | :- meta_predicate map_over_bexpr_top_down_acc(3,?,?). |
| 134 | | :- meta_predicate map_over_type_bexpr_top_down_acc(3,?,?). |
| 135 | | |
| 136 | | :- meta_predicate reduce_over_bexpr(3,?,?,?). |
| 137 | | :- meta_predicate transform_bexpr(2,?,?). |
| 138 | | :- meta_predicate l_transform_bexpr(?,2,?). |
| 139 | | :- meta_predicate transform_bexpr_with_bup_accs(4,?,?,?,?). |
| 140 | | :- meta_predicate l_transform_bexpr_with_bup_accs(?,4,?,?,?). |
| 141 | | :- meta_predicate transform_bexpr_with_acc(4,?,?,?,?). |
| 142 | | :- meta_predicate l_transform_bexpr_with_acc(?,4,?,?,?). |
| 143 | | |
| 144 | | % ----------- |
| 145 | | |
| 146 | | |
| 147 | | :- use_module(tools). |
| 148 | | |
| 149 | | :- use_module(module_information,[module_info/2]). |
| 150 | | :- module_info(group,typechecker). |
| 151 | | :- module_info(description,'This module provides operations on the type-checked AST.'). |
| 152 | | |
| 153 | | :- use_module(library(lists)). |
| 154 | | :- use_module(library(ordsets)). |
| 155 | | :- use_module(library(avl)). |
| 156 | | :- use_module(library(terms)). |
| 157 | | |
| 158 | | :- use_module(self_check). |
| 159 | | :- use_module(error_manager). |
| 160 | | :- use_module(translate,[print_bexpr/1,translate_bexpression/2]). |
| 161 | | :- use_module(gensym,[gensym/2,reset_gensym/0]). |
| 162 | | :- use_module(preferences,[get_preference/2,preference/2]). |
| 163 | | :- use_module(debug,[debug_format/3]). |
| 164 | | |
| 165 | | :- use_module(typing_tools,[is_infinite_type/1,normalize_type/2]). |
| 166 | | |
| 167 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 168 | | % basic access to enriched syntax tree |
| 169 | | |
| 170 | | is_texpr(b(_,_,_)). |
| 171 | | |
| 172 | | get_texpr_expr(b(Name,_,_),R) :- !,R=Name. |
| 173 | | get_texpr_expr(E,_) :- add_error_fail(get_texpr_expr,'B Expression not properly wrapped: ',E). |
| 174 | | |
| 175 | | get_texpr_type(b(_,Type,_),R) :- !, R=Type. |
| 176 | | get_texpr_type(E,_) :- add_error_fail(get_texpr_type,'B Expression not properly wrapped: ',E). |
| 177 | | get_texpr_info(b(_,_,Info),R) :- !, R=Info. |
| 178 | | get_texpr_info(E,_) :- add_error_fail(get_texpr_info,'B Expression not properly wrapped: ',E). |
| 179 | | |
| 180 | | get_texpr_id(b(N,_,_),Id) :- !, N=identifier(Id). |
| 181 | | get_texpr_id(E,_) :- add_error_fail(get_texpr_id,'B Expression not properly wrapped: ',E). |
| 182 | | /* same as above: but must succeed */ |
| 183 | | def_get_texpr_id(b(identifier(Id),_,_),R) :- !,R=Id. |
| 184 | | def_get_texpr_id(ID,_) :- add_error(def_get_texpr_id,'Could not extract identifier: ',ID,ID),fail. |
| 185 | | |
| 186 | | % translate a list of ids with the b/3 wrapper into a plain id list; throw error if not an identifier |
| 187 | | % used to also be called get_texpr_id_names |
| 188 | | def_get_texpr_ids(L,Ids) :- maplist(def_get_texpr_id,L,Ids). |
| 189 | | |
| 190 | | create_typed_id(IDName,Type,b(identifier(IDName),Type,[])). |
| 191 | | |
| 192 | | same_id(X,Y,ID) :- get_texpr_id(X,ID), get_texpr_id(Y,ID). |
| 193 | | |
| 194 | | |
| 195 | | % check if two wrapped expressions are equal (modulo associated Info, e.g. source loc info) |
| 196 | | 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) |
| 197 | | same_functor(E1,E2), |
| 198 | | safe_syntaxelement(E1,Subs1,_Names1,_List1,Constant), |
| 199 | | safe_syntaxelement(E2,Subs2,_Names2,_List2,Constant2), |
| 200 | | Constant==Constant2, % in case we have values with variables inside ! |
| 201 | | same_sub_expressions(Subs1,Subs2). |
| 202 | | |
| 203 | | same_sub_expressions([],[]). |
| 204 | | same_sub_expressions([H1|T1],[H2|T2]) :- same_texpr(H1,H2), same_sub_expressions(T1,T2). |
| 205 | | |
| 206 | | % check if two wrapped expressions definitely denote a different value (and are well-defined) |
| 207 | | % only detects certain cases ! |
| 208 | | different_texpr_values(b(E1,Type,I1),b(E2,Type,I2)) :- |
| 209 | | different_value(E1,E2,CheckWD), |
| 210 | | (CheckWD=false -> true |
| 211 | | ; always_well_defined_or_disprover_mode(b(E1,Type,I1)), |
| 212 | | always_well_defined_or_disprover_mode(b(E2,Type,I2))). |
| 213 | | different_value(boolean_false,boolean_true,false) :- !. |
| 214 | | different_value(boolean_true,boolean_false,false) :- !. |
| 215 | | different_value(integer(X),integer(Y),false) :- !, X\=Y. |
| 216 | | different_value(string(X),string(Y),false) :- !, X\=Y. |
| 217 | | different_value(empty_set,S,check_wd) :- !, non_empty_set(S). |
| 218 | | different_value(S,empty_set,check_wd) :- !, non_empty_set(S). |
| 219 | | % should we compare two set_extensions ? couples ? records ? |
| 220 | | |
| 221 | | non_empty_set(set_extension([_|_])). |
| 222 | | non_empty_set(sequence_extension([_|_])). |
| 223 | | %non_empty_set(value(avl_set(node.... |
| 224 | | |
| 225 | | |
| 226 | | get_texpr_exprs([],[]). |
| 227 | | get_texpr_exprs([E|Rest],[N|NRest]) :- get_texpr_expr(E,N),get_texpr_exprs(Rest,NRest). |
| 228 | | get_texpr_types([],[]). |
| 229 | | get_texpr_types([E|Rest],[T|TRest]) :- get_texpr_type(E,T),get_texpr_types(Rest,TRest). |
| 230 | | get_texpr_infos([],[]). |
| 231 | | get_texpr_infos([E|Rest],[I|IRest]) :- get_texpr_info(E,I),get_texpr_infos(Rest,IRest). |
| 232 | | get_texpr_ids([],[]). |
| 233 | | get_texpr_ids([E|Rest],[I|IRest]) :- get_texpr_id(E,I),get_texpr_ids(Rest,IRest). |
| 234 | | |
| 235 | | get_texpr_pos(TExpr,Pos) :- |
| 236 | | get_texpr_info(TExpr,Infos), |
| 237 | ? | ( member(nodeid(Pos1),Infos) -> !,Pos=Pos1 |
| 238 | | ; Pos = none). |
| 239 | | |
| 240 | | % similar to get_texpr_pos, but returns sub-list of infos relating to position |
| 241 | | extract_pos_infos(Infos,InfoRes) :- |
| 242 | ? | ( member(nodeid(Pos1),Infos) -> !,InfoRes=[nodeid(Pos1)] |
| 243 | | ; InfoRes = []). |
| 244 | | |
| 245 | | % copy position info from first arg to second argument |
| 246 | | copy_pos_infos(b(_,_,Infos1),b(E,T,Infos2),b(E,T,Infos3)) :- |
| 247 | ? | member(nodeid(Pos1),Infos1),!, |
| 248 | | delete_pos_info(Infos2,Infos2d), |
| 249 | | Infos3 = [nodeid(Pos1)|Infos2d]. |
| 250 | | copy_pos_infos(_,TE,TE). |
| 251 | | |
| 252 | | delete_pos_info(Infos1,Infos2) :- delete(Infos1,nodeid(_),Infos2). |
| 253 | | |
| 254 | | get_info_pos(Infos,Pos) :- (member(nodeid(Pos1),Infos) -> Pos=Pos1 ; Pos=none). |
| 255 | | contains_info_pos(Infos) :- (member(nodeid(_),Infos) -> true). |
| 256 | | |
| 257 | | create_texpr(Expr,Type,Info,b(Expr,Type,Info)). |
| 258 | | |
| 259 | | add_texpr_infos(b(Expr,Type,Old),Infos,b(Expr,Type,New)) :- !, |
| 260 | | append(Infos,Old,New). |
| 261 | | add_texpr_infos(Other,Infos,Res) :- |
| 262 | | add_internal_error('Illegal call, not BExpr:',add_texpr_infos(Other,Infos,Res)),fail. |
| 263 | | |
| 264 | | add_texpr_info_if_new(b(Expr,Type,Old),Info,b(Expr,Type,New)) :- !, |
| 265 | | add_info_if_new(Old,Info,New). |
| 266 | | add_texpr_info_if_new(Other,Infos,Res) :- |
| 267 | | add_internal_error('Illegal call, not BExpr:',add_texpr_info_if_new(Other,Infos,Res)),fail. |
| 268 | | % add multiple infos: |
| 269 | | add_texpr_infos_if_new(b(Expr,Type,Old),Infos,b(Expr,Type,New)) :- |
| 270 | | add_infos(Infos,Old,New). |
| 271 | | |
| 272 | | % add to info list: |
| 273 | | add_info_if_new(Old,Info,New) :- |
| 274 | | (member(Info,Old) -> New=Old ; New = [Info|Old]). |
| 275 | | |
| 276 | | add_infos([]) --> []. |
| 277 | | add_infos([Info|T]) --> add_info(Info), add_infos(T). |
| 278 | | add_info(Info,Old,New) :- |
| 279 | ? | (member(Info,Old) -> New=Old ; New = [Info|Old]). |
| 280 | | |
| 281 | | |
| 282 | | % try and extract the Rodin name of a predicate or expression |
| 283 | | get_rodin_name(Expression,Name) :- get_texpr_pos(Expression,rodinpos(Name,_)), Name \= []. |
| 284 | | get_rodin_name(Expression,Name) :- get_texpr_pos(Expression,rodinpos(_Model,Name,_)), Name \= []. % new rodinpos |
| 285 | | |
| 286 | | get_rodin_model_name(Expression,Model) :- |
| 287 | | get_texpr_pos(Expression,rodinpos(Model,Name,_)), Name \= []. % new rodinpos |
| 288 | | |
| 289 | | % try and extract the Rodin name or label pragma of a predicate or expression |
| 290 | | get_texpr_labels(TExpr,Label) :- |
| 291 | | get_texpr_info(TExpr,Infos), |
| 292 | ? | member(I,Infos), info_label(I,Label). |
| 293 | | get_info_labels(Infos,Label) :- |
| 294 | ? | member(I,Infos), info_label(I,Label). |
| 295 | | info_label(nodeid(rodinpos(Name,_)),[Name]) :- Name \= []. |
| 296 | | info_label(nodeid(rodinpos(Model,Name,_)),[FullName]) :- Name \= [], % new rodinpos |
| 297 | | ajoin([Model,':',Name], FullName). % TO DO: if only one level; don't do this |
| 298 | | info_label(label(LabelList),LabelList). |
| 299 | | |
| 300 | | add_labels_to_texpr(b(E,T,I),Labels,b(E,T,NewI)) :- |
| 301 | | (select(label(OldList),I,Rest) |
| 302 | | -> append(Labels,OldList,NewList), NewI=[label(NewList)|Rest] |
| 303 | | % TO DO: what if we have Rodin labels |
| 304 | | ; NewI = [label(Labels)|I] |
| 305 | | ). |
| 306 | | |
| 307 | | get_texpr_label(TExpr,Label) :- get_texpr_labels(TExpr,Labels), member(Label,Labels). |
| 308 | | |
| 309 | | get_texpr_description(TExpr,Description) :- |
| 310 | | get_texpr_info(TExpr,Infos), |
| 311 | | memberchk(description(Description),Infos). |
| 312 | | |
| 313 | | % check if an info list has an ignore pragma |
| 314 | | info_has_ignore_pragma(Infos) :- |
| 315 | | member(description(D),Infos), D='prob-ignore'. |
| 316 | | |
| 317 | | |
| 318 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 319 | | |
| 320 | | :- assert_must_succeed( (E = "1/2", |
| 321 | | bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err), |
| 322 | | Type==integer, Err==none, always_well_defined(ET) ) ). |
| 323 | | :- assert_must_succeed( (E = "3 mod 2", |
| 324 | | bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err), |
| 325 | | Type==integer, Err==none, always_well_defined(ET) ) ). |
| 326 | | :- assert_must_succeed( (E = "1/0", |
| 327 | | bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err), |
| 328 | | Type==integer, Err==none, \+ always_well_defined(ET) ) ). |
| 329 | | :- assert_must_succeed( (E = "2*(3 mod card({}))", |
| 330 | | bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err), |
| 331 | | Type==integer, Err==none, \+ always_well_defined(ET) ) ). |
| 332 | | :- assert_must_succeed( (E = "1/(2+1-3)", |
| 333 | | bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err), |
| 334 | | Type==integer, Err==none, \+ always_well_defined(ET) ) ). |
| 335 | | :- assert_must_succeed( (E = "max({1,2,3,0})", |
| 336 | | bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err), |
| 337 | | Type==integer, Err==none, always_well_defined(ET) ) ). |
| 338 | | :- assert_must_succeed( (E = "min({1,2,3,0})", |
| 339 | | bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err), |
| 340 | | Type==integer, Err==none, always_well_defined(ET) ) ). |
| 341 | | :- assert_must_succeed( (E = "min({1,2,3,0}-(0..4))", |
| 342 | | bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err), |
| 343 | | Type==integer, Err==none, \+ always_well_defined(ET) ) ). |
| 344 | | :- assert_must_succeed( (E = "2+max({1,2,3, 1/0})", |
| 345 | | bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err), |
| 346 | | Type==integer, Err==none,\+ always_well_defined(ET) ) ). |
| 347 | | :- assert_must_succeed( (E = "2-card({1,2,3})", |
| 348 | | bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err), |
| 349 | | Type==integer, Err==none, always_well_defined(ET) ) ). |
| 350 | | :- assert_must_succeed( (E = "2-card({1,2,3, 1/0})", |
| 351 | | bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err), |
| 352 | | Type==integer, Err==none,\+ always_well_defined(ET) ) ). |
| 353 | | :- assert_must_succeed( (E = "bool(2-size([1,2,3, 1/0])=3)", |
| 354 | | bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err), |
| 355 | | Type==boolean, Err==none, \+ always_well_defined(ET) ) ). |
| 356 | | :- assert_must_succeed( (E = "bool(2-size([1,2,3, 1/2, 3 mod 2, 3**2])=size([]))", |
| 357 | | bmachine:b_parse_machine_expression_from_codes(E,ET,Type,false,Err), |
| 358 | | Type==boolean, Err==none, always_well_defined(ET) ) ). |
| 359 | | |
| 360 | | always_well_defined_or_disprover_mode(BE) :- |
| 361 | | (preferences:preference(disprover_mode,true) -> true % we can assume all calls are well-defined |
| 362 | | ; always_well_defined(BE)). |
| 363 | | |
| 364 | | always_well_defined(b(E,_,Infos)) :- !, |
| 365 | | (nonmember(contains_wd_condition,Infos) -> true |
| 366 | | ; always_wd(E) -> true % some special rules |
| 367 | | %; nl, functor(E,F,N), F \= function, print(non_wd(F,N)),nl,nl,fail |
| 368 | | ). |
| 369 | | always_well_defined(E) :- add_error_fail(always_well_defined,'Illegal call: ',always_well_defined(E)). |
| 370 | | |
| 371 | | |
| 372 | | :- assert_must_succeed( always_wd(div( b(integer(2),integer,[]), b(integer(2),integer,[]) )) ). |
| 373 | | :- assert_must_fail( always_wd(div( b(integer(2),integer,[]), b(integer(0),integer,[]) )) ). |
| 374 | | :- assert_must_succeed( always_wd(modulo( b(integer(2),integer,[]), b(integer(2),integer,[]) )) ). |
| 375 | | :- assert_must_fail( always_wd(modulo( b(integer(2),integer,[]), b(integer(0),integer,[]) )) ). |
| 376 | | :- assert_must_fail( always_wd(modulo( b(integer(2),integer,[]), b(integer(-2),integer,[]) )) ). |
| 377 | | :- assert_must_fail( always_wd(modulo( b(integer(-1),integer,[]), b(integer(2),integer,[]) )) ). |
| 378 | | :- assert_must_succeed( always_wd(power_of( b(integer(2),integer,[]), b(integer(3),integer,[]) )) ). |
| 379 | | :- assert_must_succeed( always_wd(power_of( b(integer(2),integer,[]), b(integer(0),integer,[]) )) ). |
| 380 | | :- assert_must_fail( always_wd(power_of( b(integer(2),integer,[]), b(integer(-1),integer,[]) )) ). |
| 381 | | |
| 382 | | % catch cases where the construct is currently so instantiated that we can determine that it is well-defined |
| 383 | | % can happen e.g. during closure compilation |
| 384 | | :- use_module(custom_explicit_sets,[check_in_domain_of_avlset/2]). |
| 385 | | :- use_module(kernel_tools,[ground_value/1]). |
| 386 | | always_wd(power_of(X,Y)) :- integer_value(Y,Val), number(Val),Val>=0, always_well_defined(X). |
| 387 | | always_wd(div(X,Y)) :- integer_value(Y,Val), number(Val),Val\=0, always_well_defined(X). |
| 388 | | always_wd(modulo(X,Y)) :- integer_value(Y,Val), number(Val),Val>0, |
| 389 | | integer_value(X,ValX), number(ValX), ValX>=0. % TO DO: maybe treat this differently in TLA / Event-B minor mode ? |
| 390 | | always_wd(function(X,Y)) :- nonvar(X), |
| 391 | | X= b(value(AVLSET),_,_), nonvar(AVLSET), AVLSET=avl_set(AVL), |
| 392 | | always_wd_avl_function(AVL,Y). |
| 393 | | always_wd(min(X)) :- non_empty_wd_set_value(X). |
| 394 | | always_wd(max(X)) :- non_empty_wd_set_value(X). |
| 395 | | always_wd(card(X)) :- finite_wd_set_value(X). |
| 396 | | always_wd(size(X)) :- finite_wd_seq_value(X). |
| 397 | | always_wd(first(X)) :- non_empty_wd_seq_value(X). |
| 398 | | always_wd(front(X)) :- non_empty_wd_seq_value(X). |
| 399 | | always_wd(last(X)) :- non_empty_wd_seq_value(X). |
| 400 | | always_wd(tail(X)) :- non_empty_wd_seq_value(X). % TO DO: add restrict_front, restrict_tail ? |
| 401 | | always_wd(general_intersection(X)) :- non_empty_wd_set_value(X). |
| 402 | | 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 |
| 403 | | % other candidates: size(_), first(_) last(_) tail(_) front(_) restrict_front(_,_) restrict_tail(_,_) rel_iterate(_,_) |
| 404 | | always_wd(typeset). |
| 405 | | % operators that are always wd on their own: |
| 406 | | always_wd(record_field(RecEx,FieldName)) :- ground(FieldName), |
| 407 | | always_well_defined(RecEx). |
| 408 | | always_wd(unary_minus(A)) :- always_well_defined(A). |
| 409 | | always_wd(first_of_pair(A)) :- always_well_defined(A). |
| 410 | | always_wd(add(A,B)) :- always_well_defined(A),always_well_defined(B). |
| 411 | | always_wd(minus(A,B)) :- always_well_defined(A),always_well_defined(B). |
| 412 | | always_wd(equal(A,B)) :- always_well_defined(A),always_well_defined(B). |
| 413 | | always_wd(not_equal(A,B)) :- always_well_defined(A),always_well_defined(B). |
| 414 | | always_wd(less_equal(A,B)) :- always_well_defined(A),always_well_defined(B). |
| 415 | | always_wd(greater_equal(A,B)) :- always_well_defined(A),always_well_defined(B). |
| 416 | | always_wd(less(A,B)) :- always_well_defined(A),always_well_defined(B). |
| 417 | | always_wd(greater(A,B)) :- always_well_defined(A),always_well_defined(B). |
| 418 | | always_wd(couple(A,B)) :- always_well_defined(A),always_well_defined(B). |
| 419 | | % TO DO: add more/all other operators ? |
| 420 | | |
| 421 | | always_wd_avl_function(AVL,Y) :- nonvar(Y), Y= b(value(Val),_,_), |
| 422 | | ground_value(Val), !, |
| 423 | | check_in_domain_of_avlset(Val,AVL). % ,print(ok),nl. |
| 424 | | always_wd_avl_function(AVL,Y) :- always_well_defined(Y), |
| 425 | | custom_explicit_sets:quick_definitely_maximal_total_function_avl(AVL). |
| 426 | | |
| 427 | | integer_value(b(E,integer,_),Val) :- integer_value2(E,Val). |
| 428 | | integer_value2(integer(X),R) :- !, R=X. |
| 429 | | integer_value2(value(int(X)),R) :- !, R=X. |
| 430 | | %integer_value2(X,_) :- print(not_integer_value2(X)),nl,fail. |
| 431 | | |
| 432 | | non_empty_wd_set_value(b(E,_,_)) :- non_empty_set2(E). |
| 433 | | non_empty_set2(value(X)) :- definitely_not_empty(X). |
| 434 | | non_empty_set2(set_extension(S)) :- l_always_well_defined(S). % the set_extension could contain wd_errors !! |
| 435 | | non_empty_set2(sequence_extension(S)) :- l_always_well_defined(S). % ditto |
| 436 | | definitely_not_empty(X) :- var(X),!,fail. |
| 437 | | definitely_not_empty(avl_set(_)). |
| 438 | | definitely_not_empty([_|_]). |
| 439 | | |
| 440 | | non_empty_wd_seq_value(b(E,_,_)) :- non_empty_seq2(E). |
| 441 | | non_empty_seq2(value(X)) :- definitely_not_empty_seq(X). |
| 442 | | non_empty_seq2(sequence_extension(S)) :- l_always_well_defined(S), S=[_|_]. |
| 443 | | |
| 444 | | definitely_not_empty_seq(X) :- var(X),!,fail. |
| 445 | | definitely_not_empty_seq(avl_set(A)) :- custom_explicit_sets:is_avl_sequence(A). |
| 446 | | definitely_not_empty_seq([El1|T]) :- T==[],nonvar(El1), El1=(IDX,_), IDX==int(1). % TO DO: add more cases ? |
| 447 | | |
| 448 | | |
| 449 | | finite_wd_set_value(b(E,_,_)) :- finite_set2(E). |
| 450 | | finite_set2(empty_set). |
| 451 | | finite_set2(empty_sequence). |
| 452 | | finite_set2(value(X)) :- X==[] -> true ; definitely_not_empty(X). |
| 453 | | finite_set2(set_extension(S)) :- l_always_well_defined(S). % the set_extension could contain wd_errors !! |
| 454 | | finite_set2(sequence_extension(S)) :- l_always_well_defined(S). % ditto |
| 455 | | |
| 456 | | finite_wd_seq_value(b(E,_,_)) :- finite_seq2(E). |
| 457 | | finite_seq2(empty_set). |
| 458 | | finite_seq2(empty_sequence). |
| 459 | | finite_seq2(value(X)) :- finite_seq_value(X). |
| 460 | | finite_seq2(sequence_extension(S)) :- l_always_well_defined(S). |
| 461 | | |
| 462 | | finite_seq_value(X) :- var(X),!,fail. |
| 463 | | finite_seq_value([]). |
| 464 | | finite_seq_value(avl_set(A)) :- custom_explicit_sets:is_avl_sequence(A). |
| 465 | | % it could be expensive to check if non empty list is a B sequence ?? |
| 466 | | |
| 467 | | l_always_well_defined([]). |
| 468 | | l_always_well_defined([H|T]) :- always_well_defined(H), l_always_well_defined(T). |
| 469 | | |
| 470 | | is_truth(b(F,pred,_)) :- is_truth_aux(F). |
| 471 | | is_truth_aux(truth). |
| 472 | | is_truth_aux(value(V)) :- V==pred_true. % can occur in CSE mode |
| 473 | | |
| 474 | | is_falsity(b(F,pred,_)) :- is_falsity_aux(F). |
| 475 | | is_falsity_aux(falsity). |
| 476 | | is_falsity_aux(value(V)) :- V==pred_false. % can occur in CSE mode |
| 477 | | |
| 478 | | % conjunction of a list of predicates |
| 479 | | % NOTE: bsyntaxtree:conjunct_predicates([P1,P2,P3],R). --> generates R = b(conjunct(b(conjunct(P1,P2),pred,[]),P3),pred,[]) |
| 480 | | conjunct_predicates(V,R) :- var(V),!, add_internal_error('Variable conjunction list: ',conjunct_predicates(V,R)),fail. |
| 481 | | conjunct_predicates([],b(truth,pred,[])). |
| 482 | | conjunct_predicates([P|Rest],Result) :- conjunct2(Rest,P,Result). |
| 483 | | conjunct2([],P,P). |
| 484 | | conjunct2([Q|Rest],P,Result) :- conjunct3(P,Q,R), conjunct2(Rest,R,Result). |
| 485 | | conjunct3(b(truth,_,_),P,P) :- !. |
| 486 | | conjunct3(P,b(truth,_,_),P) :- !. |
| 487 | | conjunct3(A,B,b(conjunct(A,B),pred,NewInfo)) :- extract_info(A,B,NewInfo). |
| 488 | | |
| 489 | | % disjunction of a list of predicates |
| 490 | | disjunct_predicates([],b(falsity,pred,[])). |
| 491 | | disjunct_predicates([P|Rest],Result) :- disjunct2(Rest,P,Result). |
| 492 | | disjunct2([],P,P). |
| 493 | | disjunct2([Q|Rest],P,Result) :- disjunct3(P,Q,R), disjunct2(Rest,R,Result). |
| 494 | | disjunct3(b(falsity,_,_),P,R) :- !, R=P. |
| 495 | | disjunct3(b(truth,T,I),_,R) :- !, R=b(truth,T,I). |
| 496 | | disjunct3(P,b(falsity,_,_),R) :- !, R=P. |
| 497 | | disjunct3(_,b(truth,T,I),R) :- !, R=b(truth,T,I). |
| 498 | | disjunct3(A,B,b(disjunct(A,B),pred,NewInfo)) :- extract_info(A,B,NewInfo). |
| 499 | | |
| 500 | | % conjunct two predicates and try and construct position information |
| 501 | | conjunct_predicates_with_pos_info(A,B,AB) :- |
| 502 | | conjunct_predicates([A,B],AB0), |
| 503 | | (try_get_merged_position_info(A,B,ABI) |
| 504 | | -> add_texpr_infos(AB0,[ABI],AB) %,print(abi(ABI)),nl |
| 505 | | ; AB=AB0). |
| 506 | | |
| 507 | | try_get_merged_position_info(b(_,_,I1),b(_,_,I2),PosInfo) :- |
| 508 | | try_get_merged_position_info_aux(I1,I2,PosInfo). |
| 509 | | try_get_merged_position_info_aux(I1,I2,nodeid(pos(C,Filenumber,Srow,Scol,Erow,Ecol))) :- |
| 510 | ? | member(nodeid(pos(C1,Filenumber,Srow1,Scol1,Erow1,Ecol1)),I1),!, |
| 511 | ? | member(nodeid(pos(C2,Filenumber,Srow2,Scol2,Erow2,Ecol2)),I2),!, |
| 512 | | % merge position info if in same file |
| 513 | | (C1 =< C2 -> C=C1, Srow=Srow1,Scol=Scol1 ; C=C2, Srow=Srow2,Scol=Scol2), |
| 514 | ? | ((Erow1 > Erow2 ; Erow1=Erow2, Ecol1 >= Ecol2) |
| 515 | | -> Erow =Erow1, Ecol=Ecol1 |
| 516 | | ; Erow =Erow2, Ecol=Ecol2). |
| 517 | | |
| 518 | | |
| 519 | | % a version of create_texpr which collects automatically important infos from sub-expressions |
| 520 | | safe_create_texpr(Expr,Type,b(Expr,Type,Info)) :- % |
| 521 | ? | (sub_expression_contains_wd_condition(Expr) -> Info = [contains_wd_condition] ; Info=[]). |
| 522 | | |
| 523 | | safe_create_texpr(Expr,Type,Info,b(Expr,Type,FullInfo)) :- % |
| 524 | ? | (sub_expression_contains_wd_condition(Expr) -> FullInfo = [contains_wd_condition|Info] ; FullInfo=Info). |
| 525 | | |
| 526 | ? | sub_expression_contains_wd_condition(Expr) :- sub_expression_contains_wd_condition(Expr,_). |
| 527 | | sub_expression_contains_wd_condition(Expr,Sub) :- |
| 528 | ? | safe_syntaxelement(Expr,Subs,_Names,_L,_C), |
| 529 | ? | member(b(Sub,_,Infos),Subs), |
| 530 | | (var(Infos) |
| 531 | | -> add_internal_error('Expression not sufficiently instantiated: ',sub_expression_contains_wd_condition(Expr)), |
| 532 | | fail |
| 533 | | ; memberchk(contains_wd_condition,Infos)). |
| 534 | | |
| 535 | | % provide updated infos (e.g., reads(...)) and remove any old info fields with same functor |
| 536 | | update_infos([],Infos,Infos). |
| 537 | | update_infos([Update|T],OldInfos,NewInfos) :- |
| 538 | | functor(Update,F,N), |
| 539 | | functor(Old,F,N), |
| 540 | | delete(OldInfos,Old,OldInfos1), |
| 541 | | update_infos(T,[Update|OldInfos1],NewInfos). |
| 542 | | |
| 543 | | % merge two info lists and try to reconcile position information: |
| 544 | | merge_info(Info1,Info2,Res) :- |
| 545 | | extract_info_aux(Info2,Info1,NewInfo), |
| 546 | | (try_get_merged_position_info_aux(Info1,Info2,NewPos) |
| 547 | | -> delete_pos_info(NewInfo,NI2), |
| 548 | | Res = [NewPos|NI2] |
| 549 | | ; Res = NewInfo). |
| 550 | | |
| 551 | | % extract important info but without used_ids: |
| 552 | | extract_info_wo_used_ids(BExpr,Info) :- extract_info(BExpr,Info1), |
| 553 | ? | (select(used_ids(_),Info1,Rest) -> Info=Rest ; Info=Info1). |
| 554 | | extract_info_wo_used_ids(BExpr1,BExpr2,Info) :- extract_info(BExpr1,BExpr2,Info1), |
| 555 | | (select(used_ids(_),Info1,Rest) -> Info=Rest ; Info=Info1). |
| 556 | | |
| 557 | | % extract important info from one sub-expression: |
| 558 | | extract_info(b(_,_,Info1),NewInfo) :- |
| 559 | | extract_info_aux(Info1,[],I1),!, NewInfo = I1. |
| 560 | | extract_info(A,R) :- add_internal_error('Could not extract info: ',extract_info(A,R)), |
| 561 | | R=[]. |
| 562 | | % extract imortant info fields from two (sub-)expressions |
| 563 | | extract_info(b(_,_,Info1),b(_,_,Info2),NewInfo) :- |
| 564 | | extract_info_aux(Info1,[],I1), |
| 565 | ? | extract_info_aux(Info2,I1,I2),!, NewInfo = I2. |
| 566 | | %:- use_module(library(ordsets),[ord_intersection/3]). |
| 567 | | % ord_intersection(Info1,Info2,NewInfo),!. |
| 568 | | % TO DO: should we merge nodeid position information !? |
| 569 | | extract_info(A,B,R) :- add_internal_error('Could not extract info: ',extract_info(A,B,R)), |
| 570 | | R=[]. |
| 571 | | |
| 572 | | extract_info_aux([],Acc,Acc). |
| 573 | | extract_info_aux([used_ids(Ids)|T],Acc,Res) :- !, |
| 574 | ? | (select(used_ids(Ids2),Acc,Acc2) -> ord_union(Ids,Ids2,Ids3) ; Ids3 = Ids,Acc2=Acc), % merge used identifeirs |
| 575 | | extract_info_aux(T,[used_ids(Ids3)|Acc2],Res). |
| 576 | | extract_info_aux([H|T],Acc,Res) :- |
| 577 | ? | (important_info(H), \+ member(H,Acc) -> extract_info_aux(T,[H|Acc],Res) |
| 578 | | ; extract_info_aux(T,Acc,Res)). |
| 579 | | important_info(contains_wd_condition). |
| 580 | | important_info(prob_annotation(_)). |
| 581 | | important_info(allow_to_lift_exists). |
| 582 | | important_info(removed_typing). |
| 583 | | |
| 584 | | is_a_conjunct(b(conjunct(A,B),pred,_),A,B). |
| 585 | | % use is_a_conjunct_without_label if you want to avoid decomposing conjunction associated with a single label |
| 586 | | is_a_conjunct_without_label(b(conjunct(A,B),pred,I),A,B) :- \+ get_info_labels(I,_). |
| 587 | | % use decompose conjunct if you want to propagate labels down to the conjuncts |
| 588 | | decompose_conjunct(b(conjunct(A,B),pred,I),ResA,ResB) :- |
| 589 | | (get_info_labels(I,Labels) |
| 590 | | -> add_labels_to_texpr(A,Labels,ResA), add_labels_to_texpr(B,Labels,ResB) |
| 591 | | ; ResA=A, ResB=B). |
| 592 | | |
| 593 | | conjunction_to_list(C,L) :- var(C),!, |
| 594 | | add_error_fail(conjunction_to_list,'Internal error: var :',conjunction_to_list(C,L)). |
| 595 | | conjunction_to_list(C,List) :- |
| 596 | | conjunction_to_list2(C,List,[]). |
| 597 | | conjunction_to_list2(X,I,O) :- X=b(E,_,_), |
| 598 | | (E=conjunct(LHS,RHS) -> conjunction_to_list2(LHS,I,Inter), |
| 599 | | conjunction_to_list2(RHS,Inter,O) |
| 600 | | ; E = truth -> I=O |
| 601 | | ; I = [X|O]). |
| 602 | | |
| 603 | ? | member_in_conjunction(M,Conj) :- is_a_conjunct(Conj,LHS,RHS),!, |
| 604 | ? | (member_in_conjunction(M,LHS) ; member_in_conjunction(M,RHS)). |
| 605 | | member_in_conjunction(M,M). |
| 606 | | |
| 607 | | % a version of member_in_conjunction which can deal with lazy_let_pred : |
| 608 | | % member_in_conjunction_cse(FullConjunctWithLets,InnerConjunctNotALet, Conjunction) |
| 609 | | member_in_conjunction_cse(M,InnerConj,Conj) :- is_a_conjunct(Conj,LHS,RHS),!, |
| 610 | | (member_in_conjunction_cse(M,InnerConj,LHS) ; member_in_conjunction_cse(M,InnerConj,RHS)). |
| 611 | | member_in_conjunction_cse(Conj,InnerConj,b(lazy_let_pred(ID,Share,Body),pred,Info)) :- |
| 612 | | Conj = b(lazy_let_pred(ID,Share,BConj),pred,Info),!, |
| 613 | | member_in_conjunction_cse(BConj,InnerConj,Body). |
| 614 | | member_in_conjunction_cse(M,M,M). |
| 615 | | |
| 616 | | % not terribly efficient way to select and remove a conjunct from a predicate |
| 617 | ? | select_member_in_conjunction(M,Conj,Rest) :- is_a_conjunct(Conj,LHS,RHS),!, |
| 618 | ? | (select_member_in_conjunction(M,LHS,RL), conjunct_predicates([RL,RHS],Rest) |
| 619 | | ; select_member_in_conjunction(M,RHS,RR), conjunct_predicates([LHS,RR],Rest)). |
| 620 | | select_member_in_conjunction(M,M,b(truth,pred,[])). |
| 621 | | |
| 622 | | is_a_disjunct(b(disjunct(A,B),pred,_),A,B). |
| 623 | | is_a_negation(b(negation(A),pred,_),A). |
| 624 | | |
| 625 | | disjunction_to_list(C,L) :- var(C),!, |
| 626 | | add_error_fail(disjunction_to_list,'Internal error: var :',disjunction_to_list(C,L)). |
| 627 | | disjunction_to_list(C,List) :- |
| 628 | | disjunction_to_list2(C,List,[]). |
| 629 | | disjunction_to_list2(C,I,O) :- is_a_disjunct(C,LHS,RHS),!, |
| 630 | | disjunction_to_list2(LHS,I,Inter), |
| 631 | | disjunction_to_list2(RHS,Inter,O). |
| 632 | | disjunction_to_list2(X,[X|R],R). |
| 633 | | |
| 634 | | is_an_implication(b(implication(A,B),pred,_),A,B). |
| 635 | | |
| 636 | | is_an_equivalence(b(equivalence(A,B),pred,_),A,B). |
| 637 | | |
| 638 | | |
| 639 | | is_a_disjunct_or_implication(b(DI,pred,_),Type,A,B) :- is_a_disj_or_impl_aux(DI,Type,A,B). |
| 640 | | is_a_disj_or_impl_aux(disjunct(A,B),'disjunction',A,B). |
| 641 | | is_a_disj_or_impl_aux(implication(A,B),'implication',NA,B) :- |
| 642 | | create_negation(A,NA). |
| 643 | | is_a_disj_or_impl_aux(negation(b(conjunct(A,B),pred,_)),'negated conjunction',NA,NB) :- |
| 644 | | create_negation(A,NA),create_negation(B,NB). |
| 645 | | |
| 646 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 647 | | % remove all info fields |
| 648 | | remove_all_infos(TExpr,TNExpr) :- |
| 649 | | var(TExpr),!,TExpr=TNExpr. |
| 650 | | remove_all_infos(TExpr,TNExpr) :- |
| 651 | | get_texpr_expr(TExpr,Expr), |
| 652 | | get_texpr_type(TExpr,Type), |
| 653 | | syntaxtransformation(Expr,Subs,_,NSubs,NExpr), |
| 654 | | create_texpr(NExpr,Type,_,TNExpr), |
| 655 | | maplist(remove_all_infos,Subs,NSubs). |
| 656 | | |
| 657 | | % replace all info fields |
| 658 | | remove_all_infos_and_ground(TExpr,TNExpr) :- |
| 659 | | var(TExpr),!,TExpr=TNExpr. |
| 660 | | remove_all_infos_and_ground(TExpr,TNExpr) :- |
| 661 | | get_texpr_expr(TExpr,Expr), |
| 662 | | get_texpr_type(TExpr,Type), |
| 663 | | syntaxtransformation(Expr,Subs,_,NSubs,NExpr), |
| 664 | | create_texpr(NExpr,Type,[],TNExpr), |
| 665 | | maplist(remove_all_infos_and_ground,Subs,NSubs). |
| 666 | | |
| 667 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 668 | | |
| 669 | | % create_exists_opt(TIds,Preds,NewPred) |
| 670 | | % creating an existential quantification with some optimisations. |
| 671 | | % TIds: The typed identifiers that are quantified |
| 672 | | % Preds: A list of predicates |
| 673 | | % NewPred: The (optimised) quantified expression |
| 674 | | % Basically two optimisations are performed: |
| 675 | | % - identifiers that are not used at all are removed from the quantifier |
| 676 | | % - predicates that do not use one of the quantified identifiers are moved |
| 677 | | % outside the quantification, resulting in a predicate of the form "P & #x.Q(x)" |
| 678 | | |
| 679 | | create_exists_opt(TIds,Preds,NewPred) :- |
| 680 | | create_exists_opt(TIds,Preds,[],NewPred,_). |
| 681 | | create_exists_opt(TIds,Preds,NewPred,Modified) :- |
| 682 | | create_exists_opt(TIds,Preds,[],NewPred,Modified). |
| 683 | | create_exists_opt([],Preds,_,NewPred,Modified) :- !, Modified = false, |
| 684 | | conjunct_predicates(Preds,NewPred). |
| 685 | | create_exists_opt(TIds,Preds,AdditionalInfos,NewPred,Modified) :- |
| 686 | | preference(data_validation_mode,true), |
| 687 | | % no not lift predicates outside of existential quantifiers and change order; see rule_avec_DV.mch ClearSy example |
| 688 | | !, Modified=false, % print(not_optimizing_exists(TIds)),nl, |
| 689 | | conjunct_predicates(Preds,P), |
| 690 | | create_exists_detect_tautology_aux(TIds,P,AdditionalInfos,NewPred). |
| 691 | | create_exists_opt(TIds,Preds,AdditionalInfos,NewPred2,Modified) :- |
| 692 | | get_texpr_ids(TIds,UnsortedIds), sort(UnsortedIds,Ids), |
| 693 | | create_exists_opt2(Preds,Ids,[],Inner,Outer,UsedIds), |
| 694 | | % Inner: quantified part, Outer: part which does not have to be quantified |
| 695 | | ( Inner = [] -> AllPreds=Outer % no exists needed |
| 696 | | ; % Inner = [_|_] -> |
| 697 | | ceo_filter_used_ids(TIds,UsedIds,UsedTIds), % filter out unused variables |
| 698 | | conjunct_predicates(Inner,I), |
| 699 | | create_exists_detect_tautology_aux(UsedTIds,I,AdditionalInfos,Exists), |
| 700 | | % remove_typing also added in create_exists_detect_tautology_aux |
| 701 | | append(Outer,[Exists],AllPreds) |
| 702 | | ), |
| 703 | | (Outer=[_|_] -> Modified=true % TO DO: check if TIds=UsedTIds |
| 704 | | ; UsedIds == Ids -> Modified= false |
| 705 | | ; Modified=true), |
| 706 | | conjunct_predicates(AllPreds,NewPred2). |
| 707 | | create_exists_opt2([],_Ids,UsedIds,[],[],UsedIds) :- !. |
| 708 | | create_exists_opt2([Pred|Prest],Ids,UsedIdsIn,Inner,Outer,UsedIdsOut) :- !, |
| 709 | | find_identifier_uses(Pred, [], LocalUses), |
| 710 | | ord_intersection(Ids,LocalUses,LocalExUses), |
| 711 | | %translate:print_bexpr(Pred), format(' Uses ~w [~w]~n',[LocalUses,LocalExUses]), |
| 712 | | ( LocalExUses = [] -> |
| 713 | | Inner = Irest, |
| 714 | | Outer = [Pred|Orest], % move outside of existential quantifier |
| 715 | | UsedIdsIn = Urest |
| 716 | | ; LocalExUses = [_|_] -> |
| 717 | | Inner = [Pred|Irest], |
| 718 | | Outer = Orest, |
| 719 | | ord_union(UsedIdsIn,LocalExUses,Urest) |
| 720 | | ), |
| 721 | | create_exists_opt2(Prest,Ids,Urest,Irest,Orest,UsedIdsOut). |
| 722 | | create_exists_opt2(Pred,Ids,UsedIdsIn,Inner,Outer,UsedIdsOut) :- |
| 723 | | add_error(create_exists_opt,'Expecting predicate list: ',Pred), |
| 724 | | create_exists_opt2([Pred],Ids,UsedIdsIn,Inner,Outer,UsedIdsOut). |
| 725 | | |
| 726 | | ceo_filter_used_ids([],_UsedIds,[]). |
| 727 | | ceo_filter_used_ids([TId|Irest],UsedIds,Filtered) :- |
| 728 | | get_texpr_id(TId,Id), |
| 729 | | ( ord_member(Id,UsedIds) -> Filtered = [TId|Frest] % id used: keep it |
| 730 | | ; otherwise -> Filtered = Frest), |
| 731 | | ceo_filter_used_ids(Irest,UsedIds,Frest). |
| 732 | | |
| 733 | | % a version of create_exists which also detects x=E and x:E and x>E tautologies |
| 734 | | % we could replace this by a more generic prover |
| 735 | | create_exists_detect_tautology_aux([TID],Pred,_,Truth) :- % print(create(TID,Pred)),nl, |
| 736 | ? | is_equal(Pred,LHS,RHS), |
| 737 | | get_texpr_id(LHS,ID), get_texpr_id(TID,ID), |
| 738 | | \+ occurs_in_expr(ID,RHS), |
| 739 | | always_well_defined_or_disprover_mode(RHS), |
| 740 | | !, % replace #x.(x=E) by TRUTH |
| 741 | | debug_format(19,'Detected tautology exists equality over ~w~n',[ID]), |
| 742 | | Truth=b(truth,pred,[]). |
| 743 | | create_exists_detect_tautology_aux([TID],Pred,_,Truth) :- |
| 744 | | Pred = b(member(LHS,RHS),pred,_), |
| 745 | | get_texpr_id(LHS,ID), get_texpr_id(TID,ID), |
| 746 | | definitely_not_empty_set(RHS), |
| 747 | | always_well_defined_or_disprover_mode(RHS), |
| 748 | | !, % replace #x.(x=E) by TRUTH |
| 749 | | debug_format(19,'Detected tautology exists membership over ~w~n',[ID]), |
| 750 | | Truth=b(truth,pred,[]). |
| 751 | | create_exists_detect_tautology_aux([TID],b(Pred,_,_),_,Truth) :- |
| 752 | | is_comparison(Pred,L,R), get_texpr_id(TID,ID), |
| 753 | | ((LHS,RHS)=(L,R) ; (LHS,RHS)=(R,L)), |
| 754 | | get_texpr_id(LHS,ID), |
| 755 | | \+ occurs_in_expr(ID,RHS), |
| 756 | | always_well_defined_or_disprover_mode(RHS), |
| 757 | | !, % replace #x.(x COMP E) by TRUTH |
| 758 | | debug_format(19,'Detected tautology comparison over ~w~n',[ID]), |
| 759 | | Truth=b(truth,pred,[]). |
| 760 | | create_exists_detect_tautology_aux(Ids,Pred,AdditionalInfos,NewPred2) :- |
| 761 | | create_exists_or_let_predicate(Ids,Pred,NewPred), |
| 762 | | add_texpr_infos_if_new(NewPred,[removed_typing|AdditionalInfos],NewPred2). |
| 763 | | % removed_typing to avoid spurious exists_body_warning, see test 1681, 625 |
| 764 | | |
| 765 | | is_equal(b(equal(LHS,RHS),pred,_),A,B) :- |
| 766 | ? | ((A,B)=(LHS,RHS) ; (A,B)=(RHS,LHS)). |
| 767 | | |
| 768 | | is_comparison(greater(A,B),A,B). |
| 769 | | is_comparison(less(A,B),A,B). |
| 770 | | is_comparison(greater_equal(A,B),A,B). |
| 771 | | is_comparison(less_equal(A,B),A,B). |
| 772 | | |
| 773 | | % is true if a predicate Pred can be split into two parts: |
| 774 | | % Outer which does not depend on LocalIds and Inner which does |
| 775 | | detect_global_predicates(LocalIds,Pred,Outer,Inner) :- |
| 776 | | get_texpr_ids(LocalIds,UnsortedIds), sort(UnsortedIds,Ids), |
| 777 | | conjunction_to_list(Pred,Preds), |
| 778 | | split_predicate(Preds,Ids,OuterL,InnerL), |
| 779 | | OuterL \= [], |
| 780 | | conjunct_predicates(OuterL,Outer), |
| 781 | | conjunct_predicates(InnerL,Inner). |
| 782 | | split_predicate([],_Ids,[],[]). |
| 783 | | split_predicate([P|Ps],Ids,Outer,Inner) :- |
| 784 | | (is_local_predicate(Ids,P) |
| 785 | | -> Inner = [P|Is], split_predicate(Ps,Ids,Outer,Is) |
| 786 | | ; Outer = [P|Os], split_predicate(Ps,Ids,Os,Inner)). |
| 787 | | is_local_predicate(Ids,Pred) :- |
| 788 | | find_identifier_uses(Pred, [], LocalUses), |
| 789 | | ord_intersect(Ids,LocalUses). |
| 790 | | |
| 791 | | %:- use_module(b_global_sets,[b_global_set/1]). |
| 792 | | definitely_not_empty_set(b(SET,T,_)) :- not_empty_set_aux(SET,T). |
| 793 | | not_empty_set_aux(bool_set(_),_). |
| 794 | | not_empty_set_aux(integer_set(_),_). |
| 795 | | not_empty_set_aux(string_set,_). |
| 796 | | not_empty_set_aux(set_extension(X),_) :- dif(X,[]). |
| 797 | | not_empty_set_aux(sequence_extension(X),_) :- dif(X,[]). |
| 798 | | not_empty_set_aux(value(S),_) :- nonvar(S), (S=avl_set(_) -> true ; S=[_|_]). |
| 799 | | %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 ! |
| 800 | | % TO DO: determine which identifier(X) refer to global set names |
| 801 | | not_empty_set_aux(interval(A,B),_) :- get_texpr_expr(A,integer(IA)), get_texpr_expr(B,integer(IB)), IA =< IB. |
| 802 | | |
| 803 | | |
| 804 | | % a simple let-detection |
| 805 | | create_exists_or_let_predicate([H|T],b(conjunct(LHS,RHS),pred,I),NewPred) :- get_texpr_id(H,ID), |
| 806 | ? | is_equal(LHS,TID,IDEXPR), % TO DO: should we do a more complicated check here ? exist technique useful for SLOT-24 codespeed test |
| 807 | | get_texpr_id(TID,ID), \+ occurs_in_expr(ID,IDEXPR), |
| 808 | | maplist(not_occurs_in_expr(IDEXPR),T), |
| 809 | | !, |
| 810 | | NewPred = b(let_predicate([TID],[IDEXPR],Body),pred,I), |
| 811 | | %print('LET: '),translate:print_bexpr(NewPred),nl, |
| 812 | | create_exists_or_let_predicate(T,RHS,Body). |
| 813 | | create_exists_or_let_predicate(Ids,Pred,NewPred) :- create_exists(Ids,Pred,NewPred). |
| 814 | | |
| 815 | | not_occurs_in_expr(IDEXPR,TID) :- get_texpr_id(TID,ID), \+ occurs_in_expr(ID,IDEXPR). |
| 816 | | |
| 817 | | create_exists([],Pred,NewPred) :- !,Pred=NewPred. |
| 818 | | create_exists(Ids,Pred,NewPred) :- |
| 819 | | Ex = exists(Ids,Pred), |
| 820 | | find_identifier_uses(b(Ex,pred,[]), [], Used), |
| 821 | | extract_info_wo_used_ids(Pred,NewImportantInfo), |
| 822 | | create_texpr(Ex,pred,[used_ids(Used)|NewImportantInfo],NewPred). |
| 823 | | |
| 824 | | |
| 825 | | create_forall([],Pred,NewPred) :- !,Pred=NewPred. |
| 826 | | create_forall(Ids,Pred,NewPred) :- |
| 827 | | split_forall_body(Pred,LHS,RHS), |
| 828 | | For = forall(Ids,LHS,RHS), |
| 829 | | find_identifier_uses(b(For,pred,[]), [], Used), |
| 830 | | extract_info_wo_used_ids(LHS,RHS,NewImportantInfo), |
| 831 | | create_texpr(For,pred,[used_ids(Used)|NewImportantInfo],NewPred). |
| 832 | | split_forall_body(b(implication(LHS,RHS),_,_),LHS,RHS) :- !. |
| 833 | | split_forall_body(RHS,b(truth,pred,[]),RHS). |
| 834 | | |
| 835 | | create_implication(b(truth,pred,_),P,Res) :- !, Res=P. |
| 836 | | create_implication(b(falsity,pred,_),P,Res) :- !, create_negation(P,Res). |
| 837 | | create_implication(Lhs,Rhs,b(implication(Lhs,Rhs),pred,NewInfo)) :- |
| 838 | | extract_info(Lhs,Rhs,NewInfo). |
| 839 | | |
| 840 | | create_equivalence(Lhs,Rhs, b(equivalence(Lhs,Rhs),pred,NewInfo)) :- |
| 841 | | extract_info(Lhs,Rhs,NewInfo). |
| 842 | | |
| 843 | | create_negation(b(truth,pred,I),R) :- !, R=b(falsity,pred,I). |
| 844 | | create_negation(b(falsity,pred,I),R) :- !, R=b(truth,pred,I). |
| 845 | | create_negation(b(negation(Pred),pred,_),R) :- !, R=Pred. % not(not(P)) = P |
| 846 | | % we could add some rules about negating member <-> not_member, ... |
| 847 | | create_negation(Pred,b(negation(Pred),pred,NewInfo)) :- extract_info(Pred,NewInfo). |
| 848 | | |
| 849 | | % check if something is the negation of something else (quite stupid at the moment) |
| 850 | | is_negation_of(P,NP) :- |
| 851 | | create_negation(P,NotP), |
| 852 | | same_texpr(NotP,NP). |
| 853 | | is_negation_of(b(P,pred,_),b(NP,pred,_)) :- is_negation_aux(P,NP). |
| 854 | | |
| 855 | | is_negation_aux(equal(A,B),NP) :- |
| 856 | | is_negation_of_equality(NP,A,B). |
| 857 | | is_negation_aux(subset(XA,SA),not_subset(XB,SB)) :- same_texpr(XA,XB), same_texpr(SA,SB). |
| 858 | | is_negation_aux(not_subset(XA,SA),subset(XB,SB)) :- same_texpr(XA,XB), same_texpr(SA,SB). |
| 859 | | is_negation_aux(subset_strict(XA,SA),not_subset_strict(XB,SB)) :- same_texpr(XA,XB), same_texpr(SA,SB). |
| 860 | | is_negation_aux(not_subset_strict(XA,SA),subset_strict(XB,SB)) :- same_texpr(XA,XB), same_texpr(SA,SB). |
| 861 | | is_negation_aux(member(XA,SA),not_member(XB,SB)) :- same_texpr(XA,XB), same_texpr(SA,SB). |
| 862 | | is_negation_aux(not_member(XA,SA),member(XB,SB)) :- same_texpr(XA,XB), same_texpr(SA,SB). |
| 863 | | is_negation_aux(less(A,B),greater_equal(AA,BB)) :- same_texpr(A,AA), same_texpr(B,BB). |
| 864 | | is_negation_aux(less(A,B),less_equal(BB,AA)) :- same_texpr(A,AA), same_texpr(B,BB). |
| 865 | | is_negation_aux(less_equal(B,A),less(AA,BB)) :- same_texpr(A,AA), same_texpr(B,BB). |
| 866 | | is_negation_aux(less_equal(A,B),greater(AA,BB)) :- same_texpr(A,AA), same_texpr(B,BB). |
| 867 | | is_negation_aux(greater_equal(A,B),NP) :- is_negation_aux(less_equal(B,A),NP). |
| 868 | | is_negation_aux(greater(A,B),NP) :- is_negation_aux(less(B,A),NP). |
| 869 | | % TO DO: detect more ?? x < y <=> not ( x > y-1 ) |
| 870 | | |
| 871 | | is_negation_of_equality(not_equal(AA,BB),A,B) :- same_texpr(A,AA), same_texpr(B,BB). |
| 872 | | is_negation_of_equality(equal(AA,BB),A,B) :- same_texpr(A,AA), neg_value(BB,B). |
| 873 | | |
| 874 | | neg_value(b(boolean_true,_,_),b(boolean_false,_,_)). |
| 875 | | neg_value(b(boolean_false,_,_),b(boolean_true,_,_)). |
| 876 | | |
| 877 | | |
| 878 | | create_couple(A,B,b(couple(A,B),couple(TA,TB),Infos)) :- |
| 879 | | get_texpr_type(A,TA), get_texpr_type(B,TB), |
| 880 | | extract_info(A,B,Infos). |
| 881 | | |
| 882 | | create_couple([A],Couple) :- !,A=Couple. |
| 883 | | create_couple([A,B|Rest],Couple) :- |
| 884 | | create_couple(A,B,Couple1), |
| 885 | | create_couple([Couple1|Rest],Couple). |
| 886 | | |
| 887 | | |
| 888 | | % -------------------------------------- |
| 889 | | |
| 890 | | |
| 891 | | % find uses of identifiers |
| 892 | | |
| 893 | | occurs_in_expr(ID,TExpr) :- var(ID),!, |
| 894 | | add_internal_error('Variable id: ',occurs_in_expr(ID,TExpr)),fail. |
| 895 | | occurs_in_expr(ID,TExpr) :- ID=b(_,_,_),!, add_internal_error('Non-atomic identifier: ',occurs_in_expr(ID,TExpr)),fail. |
| 896 | | occurs_in_expr(ID,TExpr) :- |
| 897 | | (find_identifier_uses(TExpr,[],Used) |
| 898 | | -> %check_sorted(Used), |
| 899 | | ord_member(ID,Used) |
| 900 | | ; add_failed_call_error(find_identifier_uses(TExpr,[],_)),fail). |
| 901 | | % TO DO: optimize so that we only look for ID; we don't have to keep track of other IDs |
| 902 | | |
| 903 | | %check_sorted(List) :- sort(List,SL), (SL \= List -> add_internal_error('Not sorted:',List) ; true). |
| 904 | | |
| 905 | | some_id_occurs_in_expr([H|T],TExpr) :- (var(H) ; \+ atomic(H)), |
| 906 | | add_internal_error('Must be (sorted) atomic identifiers: ',some_id_occurs_in_expr([H|T],TExpr)), |
| 907 | | fail. |
| 908 | | some_id_occurs_in_expr(SortedIDs,TExpr) :- |
| 909 | | find_identifier_uses(TExpr,[],Used), |
| 910 | | list_to_ord_set(Used,UsedSorted), |
| 911 | | ord_intersect(UsedSorted,SortedIDs). |
| 912 | | |
| 913 | | :- use_module(tools,[safe_sort/3]). |
| 914 | | find_identifier_uses(TExpr,Ignored,Ids) :- |
| 915 | | %tools_printing:print_term_summary(find_identifier_uses(TExpr,Ignored,Ids)),nl, |
| 916 | | check_is_texpr(TExpr,find_identifier_uses), |
| 917 | | find_typed_identifier_uses(TExpr,Ignored,TIds), |
| 918 | | get_texpr_ids(TIds,Ids). |
| 919 | | find_identifier_uses_l(TExprs,Ignored,Ids) :- |
| 920 | | find_typed_identifier_uses_l(TExprs,Ignored,TIds), |
| 921 | | get_texpr_ids(TIds,Ids). |
| 922 | | |
| 923 | | check_is_texpr(X,Context) :- |
| 924 | | (get_texpr_expr(X,_) -> true ; add_internal_error('Expected TExpr: ', check_is_texpr(X,Context))). |
| 925 | | |
| 926 | | find_typed_identifier_uses(TExpr,Ids) :- |
| 927 | | 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 |
| 928 | | find_typed_identifier_uses(TExpr,Ignored,Ids). |
| 929 | | |
| 930 | | find_typed_identifier_uses(TExpr,Ignored,Ids) :- var(TExpr),!, |
| 931 | | add_internal_error('Variable typed expression: ', find_typed_identifier_uses(TExpr,Ignored,Ids)), |
| 932 | | Ids = []. |
| 933 | | find_typed_identifier_uses(TExpr,Ignored,Ids) :- |
| 934 | | find_typed_identifier_uses_l([TExpr],Ignored,Ids). |
| 935 | | find_typed_identifier_uses2(TExpr,Ignored,Ids,Rest) :- |
| 936 | | %syntaxtraversion_fixed(TExpr,Expr,QSubs,Subs,TNames), |
| 937 | | get_texpr_expr(TExpr,Expr),safe_syntaxelement(Expr,Subs,TNames,_,_), QSubs=[], |
| 938 | | ( uses_an_identifier(Expr,Id,TExpr,Ignored) -> |
| 939 | | ( memberchk(Id,Ignored) -> Ids=Rest % TO DO: use ord_member and ensure Ignored always sorted or use avl_set |
| 940 | | ; otherwise -> |
| 941 | | get_texpr_type(TExpr,Type), |
| 942 | | normalize_type(Type,NType), % replace seq by set |
| 943 | | create_texpr(identifier(Id),NType,[],TId), |
| 944 | | Ids = [TId|Rest]) |
| 945 | | ; otherwise -> |
| 946 | | find_typed_identifier_uses2_l(QSubs,Ignored,Ids,Ids2), |
| 947 | | get_texpr_ids(TNames,Names), |
| 948 | | append(Names,Ignored,Ignored2), |
| 949 | | find_typed_identifier_uses2_l(Subs,Ignored2,Ids2,Rest)). |
| 950 | | find_typed_identifier_uses2_l([],_) --> []. |
| 951 | | find_typed_identifier_uses2_l([Expr|Rest],Ignored) --> |
| 952 | | find_typed_identifier_uses2(Expr,Ignored), |
| 953 | | find_typed_identifier_uses2_l(Rest,Ignored). |
| 954 | | |
| 955 | | |
| 956 | | uses_an_identifier(Expr,Id) :- uses_an_identifier(Expr,Id,none,[]). |
| 957 | | |
| 958 | | uses_an_identifier(identifier(Id),Id,_,_). |
| 959 | | uses_an_identifier(lazy_lookup_pred(Id),Id,_,_). |
| 960 | | uses_an_identifier(lazy_lookup_expr(Id),Id,_,_). |
| 961 | ? | uses_an_identifier(value(_),Id,b(_,_,Info),Ignored) :- member(was_identifier(Id),Info), |
| 962 | | member('$examine_value_was_identifier_info',Ignored),!. |
| 963 | | |
| 964 | | find_typed_identifier_uses_l(TExprs,Ignored,Ids) :- |
| 965 | | find_typed_identifier_uses2_l(TExprs,Ignored,Unsorted,[]), |
| 966 | | safe_sort(find_typed_identifier_uses,Unsorted,Ids). |
| 967 | | |
| 968 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 969 | | % break predicate into components with disjunct identifiers |
| 970 | | % Pred: a predicate |
| 971 | | % Components: a list of terms component/2 where the first argument |
| 972 | | % is a predicate, the second is the set of used identifiers |
| 973 | | predicate_components(Pred,Res) :- predicate_components_in_scope(Pred,[],Res). |
| 974 | | predicate_components_in_scope(Pred,LocalVars,Res) :- |
| 975 | | predicate_components_with_restriction(Pred,LocalVars,all,Res). |
| 976 | | |
| 977 | | predicate_components_with_restriction(Pred,LocalVars,RestrictionList,Res) :- |
| 978 | | conjunction_to_list(Pred,Preds), |
| 979 | | l_predicate_identifiers(Preds,LocalVars,PredIds), |
| 980 | | ( RestrictionList=all -> R=all |
| 981 | | ; otherwise -> list_to_ord_set(RestrictionList,R)), |
| 982 | | try_find_and_remove_equalities(PredIds,PredIds2), |
| 983 | | % print(find_components(R)),nl,nl, |
| 984 | | %%(member(pred(P,Ids,X),PredIds2), nl,print(pred(Ids,X)),nl,translate:print_bexpr(P),nl,fail ; true), |
| 985 | | find_components(PredIds2,R,Components), |
| 986 | | !, |
| 987 | | %maplist(print_component,Components), |
| 988 | | Components=Res. |
| 989 | | predicate_components_with_restriction(Pred,_,_,[component(Pred,[])]) :- |
| 990 | | add_internal_error('predicate_components failed: ',predicate_components_with_restriction(Pred,_,_,_)). |
| 991 | | |
| 992 | | % print_component(component(Pred,Ids)) :- format('Component over ~w :~n',[Ids]), translate:print_bexpr(Pred),nl. |
| 993 | | |
| 994 | | % get the list of used identifiers for each predicate |
| 995 | | l_predicate_identifiers([],_LocalVars,[]). |
| 996 | | l_predicate_identifiers([Pred|PRest],LocalVars,[pred(Pred,Ids,_Selected)|IRest]) :- |
| 997 | | predicate_identifiers_in_scope(Pred,LocalVars,Ids), |
| 998 | | l_predicate_identifiers(PRest,LocalVars,IRest). |
| 999 | | |
| 1000 | | |
| 1001 | | try_find_and_remove_equalities(PredAndIds,PredAndIds2) :- |
| 1002 | | preferences:get_preference(partition_predicates_inline_equalities,true), |
| 1003 | | preferences:get_preference(try_kodkod_on_load,false), |
| 1004 | ? | find_and_remove_equalities(PredAndIds,RR), |
| 1005 | | !, PredAndIds2=RR. |
| 1006 | | try_find_and_remove_equalities(Ps,Ps). |
| 1007 | | |
| 1008 | | :- use_module(debug,[debug_println/2,formatsilent/2]). |
| 1009 | | % find and apply obvious equalities so that they do not interfere with partitioning into components |
| 1010 | | % example: c = 1 & f: 1..c --> A & g: 1..c --> B |
| 1011 | | % TO DO: preprocess and do one pass to detect potential equalities |
| 1012 | | find_and_remove_equalities([],[]). |
| 1013 | | find_and_remove_equalities(List,[pred(P,PIds,Sel)|FT]) :- |
| 1014 | ? | select(pred(P,PIds,Sel),List,Rest), |
| 1015 | | %PIds = [Id], |
| 1016 | ? | identifier_equality(P,Id,Value), |
| 1017 | | %(value_which_can_be_replaced(Value) -> true ; nl,print('Not replaced: '),translate:print_bexpr(Value),nl,fail), |
| 1018 | ? | (get_texpr_id(Value,Id2) |
| 1019 | | -> Id2 \= Id %,print(inline_id(Id,Id2)),nl |
| 1020 | | % Note: this inlining does *not* help with partitioning; but does help ProB detect common predicates/expressions |
| 1021 | | ; PIds=[Id],value_which_can_be_replaced(Value)), |
| 1022 | ? | debug_println(9,replace_simple_equality(Id,Value,PIds)), |
| 1023 | ? | maplist(apply_to_pred(Id,Value),Rest,RT), |
| 1024 | ? | !, |
| 1025 | ? | find_and_remove_equalities(RT,FT). |
| 1026 | | % TO DO: detect equalityes x = EXPR, where EXPR does not contain x and where x occurs in no other predicate |
| 1027 | | % we can then annotate x as not to enumerate |
| 1028 | | find_and_remove_equalities(R,R). |
| 1029 | | |
| 1030 | | identifier_equality(b(equal(LHS,RHS),_,_),Id,EqTerm) :- |
| 1031 | | (get_texpr_id(LHS,Id) -> EqTerm = RHS |
| 1032 | | ; get_texpr_id(RHS,Id) -> EqTerm = LHS). |
| 1033 | | |
| 1034 | | value_which_can_be_replaced(b(E,T,_)) :- value_which_can_be_replaced2(E,T). |
| 1035 | | %(value_which_can_be_replaced2(E,T) -> true ; print(not_val(E)),nl,fail). |
| 1036 | | value_which_can_be_replaced2(value(_),_). |
| 1037 | | value_which_can_be_replaced2(integer(_),_). |
| 1038 | | %value_which_can_be_replaced2(identifier(I),global(G)) :- b_global_constant(G), id_not_used_anywhere(I). |
| 1039 | | value_which_can_be_replaced2(integer_set(_),_). |
| 1040 | | value_which_can_be_replaced2(unary_minus(A),_) :- value_which_can_be_replaced(A). |
| 1041 | | value_which_can_be_replaced2(add(A,B),_) :- value_which_can_be_replaced(A), value_which_can_be_replaced(B). |
| 1042 | | % we could compute the value |
| 1043 | | value_which_can_be_replaced2(minus(A,B),_) :- value_which_can_be_replaced(A), value_which_can_be_replaced(B). |
| 1044 | | value_which_can_be_replaced2(multiplication(A,B),_) :- value_which_can_be_replaced(A), value_which_can_be_replaced(B). |
| 1045 | | value_which_can_be_replaced2(div(A,B),_) :- |
| 1046 | | integer_value(B,IB), number(IB), IB \= 0, |
| 1047 | | value_which_can_be_replaced(A). |
| 1048 | | value_which_can_be_replaced2(floored_div(A,B),T) :- value_which_can_be_replaced2(div(A,B),T). |
| 1049 | | % should we add: with WD check: division, modulo, .... ? see also simple2 in b_ast_cleanup |
| 1050 | | value_which_can_be_replaced2(max_int,_). |
| 1051 | | value_which_can_be_replaced2(min_int,_). |
| 1052 | | value_which_can_be_replaced2(string(_),_). |
| 1053 | | value_which_can_be_replaced2(string_set,_). |
| 1054 | | value_which_can_be_replaced2(boolean_true,_). |
| 1055 | | value_which_can_be_replaced2(boolean_false,_). |
| 1056 | | value_which_can_be_replaced2(bool_set,_). |
| 1057 | | value_which_can_be_replaced2(empty_set,_). |
| 1058 | | value_which_can_be_replaced2(empty_sequence,_). |
| 1059 | | value_which_can_be_replaced2(couple(A,B),_) :- value_which_can_be_replaced(A), value_which_can_be_replaced(B). |
| 1060 | | value_which_can_be_replaced2(interval(A,B),_) :- value_which_can_be_replaced(A), value_which_can_be_replaced(B). |
| 1061 | | value_which_can_be_replaced2(set_extension(L),_) :- maplist(value_which_can_be_replaced,L). |
| 1062 | | value_which_can_be_replaced2(sequence_extension(L),_) :- maplist(value_which_can_be_replaced,L). |
| 1063 | | value_which_can_be_replaced2(cartesian_product(A,B),_) :- % typing equations, like t_float = INTEGER*NATURAL1 |
| 1064 | | simple_value_set(A), simple_value_set(B). |
| 1065 | | value_which_can_be_replaced2(pow_subset(A),_) :- simple_value_set(A). |
| 1066 | | %value_which_can_be_replaced2(identifier(_),_). % TO DO: check that this is not the LHS identifier which we replace !! |
| 1067 | | % identifiers can also be replaced: we check above that the only identifier in the predicate is the equality identifier |
| 1068 | | % 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 |
| 1069 | | |
| 1070 | | % TO DO: also allow inlining of prj1/prj2 of simple_value_set: |
| 1071 | | % 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]))) |
| 1072 | | % 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]))) |
| 1073 | | |
| 1074 | | % TO DO: maybe check if it is an infinite type which cannot be evaluated anyway |
| 1075 | | simple_value_set(b(E,_,_)) :- simple_value_set2(E). |
| 1076 | | %simple_value_set2(bool_set). % Warning: we could have a finite construct which gets evaluated multiple times |
| 1077 | | simple_value_set2(string_set). |
| 1078 | | simple_value_set2(integer_set(_)). |
| 1079 | | simple_value_set2(cartesian_product(A,B)) :- simple_value_set(A), simple_value_set(B). |
| 1080 | | simple_value_set2(pow_subset(A)) :- simple_value_set(A). |
| 1081 | | % POW, records struct(_) set ? |
| 1082 | | |
| 1083 | | % apply a substiution of ID/Expr on a pred(EXPR,VarList,X) term |
| 1084 | | % Expr must either be a variable or contain no variables at all |
| 1085 | | apply_to_pred(ID,Expr,pred(E1,PIds1,X),pred(E2,PIds3,X)) :- |
| 1086 | ? | (select(ID,PIds1,PIds2) |
| 1087 | | -> replace_id_by_expr(E1,ID,Expr,E2), %,print(applied(ID)),nl,translate:print_bexpr(E2),nl |
| 1088 | | % 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 |
| 1089 | | (get_texpr_id(Expr,NewID) |
| 1090 | | -> ord_add_element(PIds2,NewID,PIds3) |
| 1091 | | ; PIds3 = PIds2) |
| 1092 | | %, format('Apply ~w -> ~w : ',[ID,NewID]),translate:print_bexpr(E2),nl |
| 1093 | | ; E1=E2,PIds1=PIds3). |
| 1094 | | |
| 1095 | | |
| 1096 | | % project a predicate : keep only those Predicates that are directly or |
| 1097 | | % indirectly relevant for Ids; FullIds are all identifiers used by ProjectedPredicate |
| 1098 | | project_predicate_on_identifiers(Pred,Ids,ProjectedPredicate,FullIds, RestList) :- |
| 1099 | | (debug:debug_mode(on) |
| 1100 | | -> print('project: '),print_bexpr(Pred),nl, print(' on : '), print(Ids),nl |
| 1101 | | ; true), |
| 1102 | | conjunction_to_list(Pred,Preds), |
| 1103 | | l_predicate_identifiers(Preds,[],PredIds), % TO DO: allow LocalVariables to be passed |
| 1104 | | % print(predids(PredIds)),nl, |
| 1105 | | try_find_and_remove_equalities(PredIds,PredIds2), |
| 1106 | | extract_all_predicates(Ids,all,Ids,PredIds2,ProjectedPredicates, RestList,FullIds), |
| 1107 | | conjunct_predicates(ProjectedPredicates,ProjectedPredicate), |
| 1108 | | (debug:debug_mode(on) |
| 1109 | | -> print('*result: '),print_bexpr(ProjectedPredicate),nl, |
| 1110 | | print(' on : '), print(FullIds),nl |
| 1111 | | ; true). |
| 1112 | | |
| 1113 | | %print_preds([]). |
| 1114 | | %print_preds([pred(P,_IDs,_)|T]) :- translate:print_bexpr(P), nl, print(' '), print_preds(T). |
| 1115 | | |
| 1116 | | :- use_module(b_global_sets,[b_get_global_constants/1, b_get_global_sets/1]). |
| 1117 | | predicate_identifiers(Pred,Ids) :- predicate_identifiers_in_scope(Pred,[],Ids). |
| 1118 | | predicate_identifiers_in_scope(Pred,LocalVariables,Ids) :- |
| 1119 | | get_global_identifiers(IS), |
| 1120 | | list_to_ord_set(LocalVariables,LV), |
| 1121 | | ord_subtract(IS,LV,Ignore2), % Do not ignore any local variable; it will be used instead of enumerate set element |
| 1122 | | find_identifier_uses(Pred,Ignore2,Ids1), % Ignore enumerated set names |
| 1123 | | list_to_ord_set(Ids1,Ids). |
| 1124 | | |
| 1125 | | % get global set and constant identifiers which you usually want to exclude for find_identifier_uses |
| 1126 | | get_global_identifiers(IDs) :- |
| 1127 | | b_get_global_constants(EnumeratedSetCsts), |
| 1128 | | % b_global_sets:b_get_global_enumerated_sets(GSets), % is there a reason to exclude deferred sets ??; cardinality inference,... are all done before partitioning ? |
| 1129 | | b_get_global_sets(GSets), |
| 1130 | | append(GSets,EnumeratedSetCsts,GE), |
| 1131 | | list_to_ord_set(GE,IDs). |
| 1132 | | |
| 1133 | | % find_components(ListOf_pred, Restrict, Out:ListOfComponents) |
| 1134 | | % role of Restrict: all if we do normal partition or List of VariableIDs on which we restrict our attention to (for Existential quantifier construction) |
| 1135 | | find_components([],_,[]). |
| 1136 | | find_components([pred(P,PIds,true)|PRest],Restrict,[component(Pred,Ids)|CRest]) :- |
| 1137 | | % find all predicates which are using identifiers occuring in PIds |
| 1138 | | % (and additionally those which use common identifiers ) |
| 1139 | | ord_restrict(Restrict,PIds,InterIDs), |
| 1140 | | ( InterIDs =[] -> |
| 1141 | | % we simply copy this predicate into a single component; not with the scope of Restricted IDs |
| 1142 | | % print(skip(PIds,P)),nl, % |
| 1143 | | Pred=P, Ids=PIds, PRest=Rest |
| 1144 | | ; otherwise -> |
| 1145 | | extract_all_predicates(PIds,Restrict,PIds,PRest,Preds,Rest,Ids), |
| 1146 | | conjunct_predicates([P|Preds],Pred) |
| 1147 | | ), |
| 1148 | | find_components(Rest,Restrict,CRest). |
| 1149 | | extract_all_predicates([],_,_,Preds,Found,Rest,[]) :- !, % selecting done at end: keep same order of conjuncts |
| 1150 | | select_predicates(Preds,Found,Rest). |
| 1151 | | extract_all_predicates(Ids,Restrict,OldIds,Preds,Found,Rest,ResultIds) :- |
| 1152 | | % search for all predicates that directly use one of the |
| 1153 | | % identifiers in "Ids" |
| 1154 | | select_all_using_preds(Preds,Ids,FoundIds), |
| 1155 | | ord_subtract(FoundIds,OldIds,NewIds), |
| 1156 | | ord_restrict(Restrict,NewIds,NewIdsToExtract), |
| 1157 | | ord_union(OldIds,FoundIds,OldIds2), |
| 1158 | | % now recursively do this which the new identifiers that we have found |
| 1159 | | extract_all_predicates(NewIdsToExtract,Restrict,OldIds2,Preds,Found,Rest,RestIds), |
| 1160 | | ord_union([Ids,NewIds,RestIds],ResultIds). |
| 1161 | | |
| 1162 | | % mark all predicates which intersect with ComponentIds and compute new ids to be added to the component |
| 1163 | | select_all_using_preds([],_,[]). |
| 1164 | | select_all_using_preds([pred(_P,PIds,Selected)|PRest],ComponentIds,NewFoundIds) :- |
| 1165 | ? | ( (Selected==true ; ord_disjoint(PIds,ComponentIds)) -> |
| 1166 | | NewFoundIds1 = [] |
| 1167 | | ; otherwise -> % we select the predicate for the component |
| 1168 | | ord_subtract(PIds,ComponentIds,NewFoundIds1), |
| 1169 | | Selected=true |
| 1170 | | ), |
| 1171 | | select_all_using_preds(PRest,ComponentIds,NewFoundIds2), |
| 1172 | | ord_union(NewFoundIds1,NewFoundIds2,NewFoundIds). |
| 1173 | | |
| 1174 | | % ord_intersection with special case for all term |
| 1175 | | ord_restrict(all,Ids,Res) :- !, Res=Ids. |
| 1176 | | ord_restrict(Restrict,Ids,Res) :- ord_intersection(Ids,Restrict,Res). |
| 1177 | | |
| 1178 | | select_predicates(Predicates,FoundPreds,OtherPreds) :- |
| 1179 | | split_list(is_selected_predicate,Predicates,FoundPredIds,OtherPreds), |
| 1180 | | maplist(extract_found_predicate,FoundPredIds,FoundPreds). |
| 1181 | | is_selected_predicate(pred(_P,_PIds,Selected)) :- ground(Selected). |
| 1182 | | extract_found_predicate(pred(P,_PIds,_Selected),P). |
| 1183 | | |
| 1184 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 1185 | | % replace (simultaneously) multiple identifiers by expressions |
| 1186 | | % this could be used to replace the predicate replace_id_by_expr by mapping everything in a |
| 1187 | | % singleton list. however, that would involve list operations instead of unifications |
| 1188 | | parse_pred(Codes,TExpr) :- bmachine:b_parse_machine_predicate_from_codes_open(no_quantifier,Codes,[],[],TExpr). |
| 1189 | | parse_expr(Codes,TExpr) :- bmachine:b_parse_machine_expression_from_codes(Codes,[],TExpr,_Type,true,_Error). |
| 1190 | | test_result(1,b(equal(b(comprehension_set([b(identifier(__FRESH____),integer,_)], |
| 1191 | | b(greater(b(identifier(__FRESH____2),integer,_),b(identifier(x),integer,_)),pred,_)),set(integer),_), |
| 1192 | | b(empty_set,set(integer),_)),pred,_)). |
| 1193 | | |
| 1194 | | :- assert_must_succeed((bsyntaxtree:parse_pred("{x|x>y}={}",T1), replace_ids_by_exprs(T1,[],[],T1))). |
| 1195 | | :- assert_must_succeed((bsyntaxtree:parse_pred("{x|x>y}={}",T1), bsyntaxtree:parse_expr("100",T2), |
| 1196 | | replace_ids_by_exprs(T1,[y],[T2],R),bsyntaxtree:parse_pred("{x|x>100}={}",T3),same_texpr(R,T3) )). |
| 1197 | | :- assert_must_succeed((bsyntaxtree:parse_pred("{x|x>y}={}",T1), |
| 1198 | | replace_ids_by_exprs(T1,[y],[b(identifier(x),integer,[])],R), |
| 1199 | | bsyntaxtree:test_result(1,R),bsyntaxtree:parse_pred("{x|x>x}={}",T3),\+ same_texpr(R,T3) )). |
| 1200 | | :- assert_must_succeed((bsyntaxtree:parse_pred("{x,y|x>v & y>w}={}",T1), |
| 1201 | | replace_ids_by_exprs(T1,[v,w],[b(identifier(w),integer,[]),b(identifier(v),integer,[])],R), |
| 1202 | | bsyntaxtree:parse_pred("{x,y|x>w & y>v}={}",T3), same_texpr(R,T3) )). |
| 1203 | | :- assert_must_succeed((gensym:reset_gensym, bsyntaxtree:parse_pred("{x,y|x>v & y>w}={}",T1), |
| 1204 | | replace_ids_by_exprs(T1,[v,w],[b(identifier(w),integer,[]),b(identifier(x),integer,[])],R), |
| 1205 | | translate:translate_bexpression(R,TR), |
| 1206 | | TR = '{__FRESH____1,y|__FRESH____1 > w & y > x} = {}')). %'{__FRESH____1,y|(__FRESH____1 : INTEGER & y : INTEGER) & (__FRESH____1 > w & y > x)} = {}' )). |
| 1207 | | |
| 1208 | | replace_ids_by_exprs(TExpr,[TId],[Inserted],Replaced) :- !, % better, more robust and efficient version |
| 1209 | | check_ids([TId],[Id]), |
| 1210 | | replace_id_by_expr(TExpr,Id,Inserted,Replaced). |
| 1211 | | replace_ids_by_exprs(TExpr,[],[],Replaced) :- !, Replaced=TExpr. % Nothing to do |
| 1212 | | replace_ids_by_exprs(TExpr,Ids,Exprs,Replaced) :- |
| 1213 | | check_ids(Ids,Ids2), % convert to atomic identifiers |
| 1214 | | find_identifier_uses_l(Exprs,[],ExprsUsedIds), |
| 1215 | | sort(ExprsUsedIds,SExprsUsedIds), |
| 1216 | | findall(rename(I,E),(nth0(N,Ids2,I),nth0(N,Exprs,E)),RenameList), |
| 1217 | | %print(replace(RenameList,SExprsUsedIds)),nl, |
| 1218 | | replace_ids_by_exprs2(RenameList,SExprsUsedIds,TExpr,Replaced,_). %, nl,print(done),nl. |
| 1219 | | % a version of replace_ids_by_exprs2 for maplist: |
| 1220 | | %replace_ids_by_exprs1(RenameList,SExprsUsedIds,TExpr,Replaced) :- |
| 1221 | | % replace_ids_by_exprs2(RenameList,SExprsUsedIds,TExpr,Replaced,_). %, print('Rep: '), translate:print_bexpr(Replaced),nl. |
| 1222 | | check_ids([],[]). |
| 1223 | | check_ids([H|T],[ID|IT]) :- (atomic(H) -> ID=H ; def_get_texpr_id(H,ID)), check_ids(T,IT). |
| 1224 | | replace_ids_by_exprs2(RenameList,ExprsUsedIds,TExpr,Replaced,WDC) :- |
| 1225 | | remove_bt(TExpr,Expr,NewExpr,TNewExpr), |
| 1226 | | ( Expr = identifier(Id), member(rename(Id,Inserted),RenameList) -> |
| 1227 | | Replaced = Inserted, |
| 1228 | | get_texpr_info(Inserted,Infos), |
| 1229 | | (memberchk(contains_wd_condition,Infos) |
| 1230 | | -> WDC = true ; WDC = false) % WDC = true means we have added a wd-condition where previously there was none |
| 1231 | | ; otherwise -> |
| 1232 | | syntaxtransformation_fixed(Expr,QSubs,Subs1,Names,NQSubs,NSubs,NewExpr), |
| 1233 | | find_variable_clashes(Names,ExprsUsedIds,RenameNames), % check for variable caputure |
| 1234 | | (RenameNames = [] |
| 1235 | | -> Subs = Subs1 % no variable capture occured |
| 1236 | | ; %format('*** VARIABLE CAPTURE : ~w~n~n',[RenameNames]), |
| 1237 | | %maplist(replace_ids_by_exprs1(RenameNames,[]),Subs1,Subs) % replace affected names by fresh ids in sub arguments |
| 1238 | | rename_bt_l(Subs1,RenameNames,Subs) % replace affected names by fresh ids in sub arguments (will also change list of quantified variables itself) |
| 1239 | | ), |
| 1240 | | %print(e(SNameIds,QSubs,Subs)),nl, |
| 1241 | | l_replace_ids_by_exprs2(QSubs,RenameList,ExprsUsedIds,NQSubs,WDC1), % QSubs are like RHS of let expression, where Names are not in scope |
| 1242 | | remove_hidden_names(Names,RenameList,UpdatedRenameList), |
| 1243 | | %print(rem_hidden(Names,UpdatedRenameList)),nl, |
| 1244 | | ( UpdatedRenameList = [] -> % all Ids are now hidden for the inner expressions |
| 1245 | | NSubs=Subs, WDC=WDC1 |
| 1246 | | ; otherwise -> %print(recur(Subs)),nl, |
| 1247 | | l_replace_ids_by_exprs2(Subs,UpdatedRenameList,ExprsUsedIds,NSubs,WDC2), |
| 1248 | | and_wdc(WDC1,WDC2,WDC) |
| 1249 | | ), |
| 1250 | | TNewExpr = b(E1,T1,Info1), |
| 1251 | | rename_update_used_ids_info(RenameList,Info1,Info2), |
| 1252 | | %(E1 = exists(P,_) -> print(exists(P,Id,Info1,Info2)),nl ; true), |
| 1253 | | add_wd_if_needed(WDC,b(E1,T1,Info2),Replaced) |
| 1254 | | ). |
| 1255 | | |
| 1256 | | % check if we have to rename any quantified variable to avoid variable capture of RHS of renamings |
| 1257 | | % 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} |
| 1258 | | find_variable_clashes([],_,[]). |
| 1259 | | find_variable_clashes([Name|Names],ExprsUsedIds,[rename(ID,FRESHID)|Renaming] ) :- |
| 1260 | | def_get_texpr_id(Name,ID), |
| 1261 | | ord_member(ID,ExprsUsedIds), % the quantified name is also introduced by the renaming |
| 1262 | | !, |
| 1263 | | gensym('__FRESH__',FRESHID), |
| 1264 | | find_variable_clashes(Names,ExprsUsedIds,Renaming). |
| 1265 | | find_variable_clashes([_|Names],ExprsUsedIds,Renaming) :- |
| 1266 | | find_variable_clashes(Names,ExprsUsedIds,Renaming). |
| 1267 | | |
| 1268 | | |
| 1269 | | l_replace_ids_by_exprs2([],_,_,[],false). |
| 1270 | | l_replace_ids_by_exprs2([H|T],UpdatedRenameList,ExprsUsedIds,[IH|IT],WDC) :- |
| 1271 | | replace_ids_by_exprs2(UpdatedRenameList,ExprsUsedIds,H,IH,WDC1), |
| 1272 | | l_replace_ids_by_exprs2(T,UpdatedRenameList,ExprsUsedIds,IT,WDC2), |
| 1273 | | and_wdc(WDC1,WDC2,WDC). |
| 1274 | | |
| 1275 | | % remove any identifiers that are now "invisible" because they are masked by quantified names |
| 1276 | | % e.g., when we enter #x.(P) then a renaming of x will be "hidden" inside P |
| 1277 | | remove_hidden_names([],RenameList,RenameList). |
| 1278 | | remove_hidden_names([Name|Names],RenameList,NewRenameList) :- |
| 1279 | | def_get_texpr_id(Name,ID), |
| 1280 | | delete(RenameList,rename(ID,_),RenameList1), |
| 1281 | | !, % only one rename should exist |
| 1282 | | %print(del(ID,RenameList1)),nl, |
| 1283 | | remove_hidden_names(Names,RenameList1,NewRenameList). |
| 1284 | | |
| 1285 | | find_rhs_ids(rename(Id,TExpr),rename_ids(Id,InsUsedIds)) :- find_identifier_uses(TExpr,[],InsUsedIds). |
| 1286 | | |
| 1287 | | % apply a rename list to the used_ids,... information fields |
| 1288 | | % this is more tricky than applying a single identifier, as we first have to deleted all ids |
| 1289 | | % and remember which ones were deleted, and only then insert the corresponding ids |
| 1290 | | % e.g., we could have a RenameList = [rename(p,q),rename(q,p)] ; see test 1776 M1_Internal_v3.mch |
| 1291 | | rename_update_used_ids_info(RenameList,IIn,IOut) :- |
| 1292 | | maplist(find_rhs_ids,RenameList,RenameList2), |
| 1293 | | maplist(apply_rename_list(RenameList2),IIn,IOut). |
| 1294 | | |
| 1295 | | apply_rename_list(RenameList,I,NI) :- |
| 1296 | | apply_rename_list2(I,RenameList,NI). |
| 1297 | | apply_rename_list2(used_ids(IDS),RenameList,used_ids(NewIDS)) :- !, apply_rename_list_to_ids(RenameList,IDS,[],NewIDS). |
| 1298 | | apply_rename_list2(reads(IDS),RenameList,reads(NewIDS)) :- !, apply_rename_list_to_ids(RenameList,IDS,[],NewIDS). |
| 1299 | | apply_rename_list2(modifies(IDS),RenameList,modifies(NewIDS)) :- !, apply_rename_list_to_ids(RenameList,IDS,[],NewIDS). |
| 1300 | | apply_rename_list2(Info,_,Info). |
| 1301 | | |
| 1302 | | % apply a rename list to a sorted list of ids |
| 1303 | | apply_rename_list_to_ids([],Acc,ToInsert,Res) :- ord_union(Acc,ToInsert,Res). |
| 1304 | | apply_rename_list_to_ids([rename_ids(Id,NewIds)|T],Acc,ToInsert,Res) :- |
| 1305 | | (ord_del_element(Acc,Id,Acc2) % the Id occurs and is deleted |
| 1306 | | -> ord_union(NewIds,ToInsert,ToInsert2), |
| 1307 | | apply_rename_list_to_ids(T,Acc2,ToInsert2,Res) |
| 1308 | | ; apply_rename_list_to_ids(T,Acc,ToInsert,Res)). |
| 1309 | | |
| 1310 | | % ----------------------- |
| 1311 | | % remove an Identifier from used_ids Info field if it exists |
| 1312 | | remove_used_id_from_info(I,ID_to_remove,NI) :- |
| 1313 | | update_used_ids_info(I,ID_to_remove,[],NI). |
| 1314 | | |
| 1315 | | remove_used_ids_from_info([],I,I). |
| 1316 | | remove_used_ids_from_info([ID_to_remove|T],I,NI) :- remove_used_id_from_info(I,ID_to_remove,I2), |
| 1317 | | remove_used_ids_from_info(T,I2,NI). |
| 1318 | | |
| 1319 | | % remove an Identifier from used_ids Info field if it exists and insert sorted list of ids instead |
| 1320 | | update_used_ids_info([],_,_,[]). |
| 1321 | | update_used_ids_info([InfoField|T],ID_to_remove,IDsInserted,[NewInfoField|NT]) :- |
| 1322 | ? | (update_id_from_info_field(ID_to_remove,IDsInserted,InfoField,R) -> NewInfoField=R |
| 1323 | | ; NewInfoField=InfoField), |
| 1324 | | update_used_ids_info(T,ID_to_remove,IDsInserted,NT). |
| 1325 | | |
| 1326 | | update_id_from_info_field(ID_to_remove,IDsInserted,I,NI) :- |
| 1327 | ? | update_id_from_info_field2(I,ID_to_remove,IDsInserted,NI). |
| 1328 | ? | update_id_from_info_field2(used_ids(IDS),ID,IDsInserted,used_ids(NewIDS)) :- update_id(IDS,ID,IDsInserted,NewIDS). |
| 1329 | | update_id_from_info_field2(reads(IDS),ID,IDsInserted,reads(NewIDS)) :- update_id(IDS,ID,IDsInserted,NewIDS). |
| 1330 | | update_id_from_info_field2(modifies(IDS),ID,IDsInserted,modifies(NewIDS)) :- update_id(IDS,ID,IDsInserted,NewIDS). |
| 1331 | | |
| 1332 | ? | update_id(IDS,ID_to_remove,IDsInserted,NewIDS) :- select(ID_to_remove,IDS,IDS2), |
| 1333 | | (IDsInserted=[] -> NewIDS = IDS2 |
| 1334 | | ; sort(IDS2,SIDS2), ord_union(IDsInserted,SIDS2,NewIDS)). |
| 1335 | | %if select fails we do not add IDsInserted: we assume the used_ids info is correct and ID_to_remove does not occur ! |
| 1336 | | % We could use this info to avoid traversing subtree ! |
| 1337 | | % print(projecting_away_unknown_id(ID_to_remove,IDS)),nl, |
| 1338 | | |
| 1339 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 1340 | | |
| 1341 | | :- 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), |
| 1342 | | TR = 'r = {__FRESH____1|__FRESH____1 : 1 .. x & __FRESH____1 mod 2 = 1}' )). |
| 1343 | | :- assert_must_succeed((bsyntaxtree:parse_pred("{x|x>y}={}",T1), |
| 1344 | | replace_id_by_expr(T1,y,b(identifier(x),integer,[]),R), |
| 1345 | | bsyntaxtree:test_result(1,R),bsyntaxtree:parse_pred("{x|x>x}={}",T3),\+ same_texpr(R,T3) )). |
| 1346 | | :- assert_must_succeed((bsyntaxtree:parse_pred("{x|x>y}={}",T1), bsyntaxtree:parse_expr("100",T2), |
| 1347 | | replace_id_by_expr(T1,y,T2,R),bsyntaxtree:parse_pred("{x|x>100}={}",T3),same_texpr(R,T3) )). |
| 1348 | | |
| 1349 | | % replace an identifier by an expression |
| 1350 | | replace_id_by_expr(TExpr,Id,Inserted,Replaced) :- \+ atomic(Id),!, |
| 1351 | | add_internal_error('Id not atomic: ',replace_id_by_expr(TExpr,Id,Inserted,Replaced)), |
| 1352 | | Replaced = TExpr. |
| 1353 | | replace_id_by_expr(TExpr,Id,Inserted,Replaced) :- |
| 1354 | | %find_all_relevant_quantified_vars(Id,TExpr,QVars), |
| 1355 | | find_identifier_uses(Inserted,[],InsUsedIds), |
| 1356 | | sort(InsUsedIds,SInsUsedIds), |
| 1357 | | replace_id_by_expr2(Id,Inserted,SInsUsedIds,TExpr,Replaced,_). |
| 1358 | | replace_id_by_expr2(Id,Inserted,InsUsedIds,TExpr,Replaced,WDC) :- |
| 1359 | | remove_bt(TExpr,Expr,NewExpr,TNewExpr), |
| 1360 | | ( Expr = identifier(Id) -> |
| 1361 | | Replaced = Inserted, |
| 1362 | | get_texpr_info(Inserted,Infos), |
| 1363 | | (memberchk(contains_wd_condition,Infos) |
| 1364 | | -> WDC = true ; WDC = false) % WDC = true means we have added a wd-condition where previously there was none |
| 1365 | | ; otherwise -> |
| 1366 | | syntaxtransformation_fixed(Expr,QSubs,Subs,Names,NQSubs,NSubs,NewExpr), |
| 1367 | | %maplist(replace_id_by_expr2(Id,Inserted),QSubs,NQSubs), |
| 1368 | | l_replace_id_by_expr2(QSubs,Id,Inserted,InsUsedIds,NQSubs,WDC1), |
| 1369 | | get_texpr_id(TId,Id), |
| 1370 | | ( memberchk(TId,Names) -> % the Id is now hidden for the inner expressions |
| 1371 | | NSubs=Subs, WDC=WDC1 |
| 1372 | | ; (InsUsedIds \= [], |
| 1373 | | get_texpr_ids(Names,Ns),sort(Ns,SNs), |
| 1374 | | ord_intersection(SNs,InsUsedIds,Captured), |
| 1375 | | Captured \= [] %, print(inter(SNs,InsUsedIds,Captured)),nl |
| 1376 | | ) |
| 1377 | | % The Names introduced clash with variables used in the Inserted expression |
| 1378 | | -> findall(rename(X,FRESHID),(member(X,Captured),gensym:gensym('__FRESH__',FRESHID)),RenameList), |
| 1379 | | %print(rename(RenameList)),nl, |
| 1380 | | rename_bt_l(Subs,RenameList,RenSubs), |
| 1381 | | l_replace_id_by_expr2(RenSubs,Id,Inserted,InsUsedIds,NSubs,WDC2), |
| 1382 | | and_wdc(WDC1,WDC2,WDC) |
| 1383 | | ; otherwise -> |
| 1384 | | l_replace_id_by_expr2(Subs,Id,Inserted,InsUsedIds,NSubs,WDC2), |
| 1385 | | and_wdc(WDC1,WDC2,WDC) |
| 1386 | | ), |
| 1387 | | TNewExpr = b(E1,T1,Info1), |
| 1388 | | update_used_ids_info(Info1,Id,InsUsedIds,Info2), |
| 1389 | | %(E1 = exists(P,_) -> print(exists(P,Id,Info1,Info2)),nl ; true), |
| 1390 | | add_wd_if_needed(WDC,b(E1,T1,Info2),Replaced) |
| 1391 | | ). |
| 1392 | | |
| 1393 | | l_replace_id_by_expr2([],_,_,_,[],false). |
| 1394 | | l_replace_id_by_expr2([H|T],Id,Inserted,InsUsedIds,[IH|IT],WDC) :- |
| 1395 | | replace_id_by_expr2(Id,Inserted,InsUsedIds,H,IH,WDC1), |
| 1396 | | l_replace_id_by_expr2(T,Id,Inserted,InsUsedIds,IT,WDC2), |
| 1397 | | and_wdc(WDC1,WDC2,WDC). |
| 1398 | | |
| 1399 | | and_wdc(true,_,R) :- !,R=true. |
| 1400 | | and_wdc(_,true,R) :- !, R=true. |
| 1401 | | and_wdc(_,_,false). |
| 1402 | | |
| 1403 | | % add contains_wd_condition if a change occured during replacement of id by expression |
| 1404 | | add_wd_if_needed(true,b(E,T,Infos),Replaced) :- |
| 1405 | | nonmember(contains_wd_condition,Infos), |
| 1406 | | !, |
| 1407 | | Replaced = b(E,T,[contains_wd_condition|Infos]). |
| 1408 | | add_wd_if_needed(_,T,T). |
| 1409 | | |
| 1410 | | |
| 1411 | | |
| 1412 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 1413 | | |
| 1414 | | |
| 1415 | | % syntaxtransformation_fixed/7 is the same as syntaxtransformation/5 with the exception |
| 1416 | | % that we distinguish between subexpressions that have the newly introduced identifiers (Names) |
| 1417 | | % in scope (OSubs) and those who don't (OExprs). The only expressions where the latter case is relevant |
| 1418 | | % are let_expression and let_predicate. |
| 1419 | | % TODO: This is a quick'n dirty fix for only some cases. |
| 1420 | | % NO LONGER REQUIRED: let_expression and let_predicate now obey another semantic, not the Z semantics anymore |
| 1421 | | %syntaxtransformation_fixed(OExpr,OExprs,OSubs,Names,NExprs,NSubs,NExpr) :- |
| 1422 | | % is_let_pred_or_expr(OExpr,OTIds,OExprs,OExprPred,LetType), |
| 1423 | | % !, |
| 1424 | | % Names=OTIds, |
| 1425 | | % is_let_pred_or_expr(NExpr,NTIds,NExprs,NExprPred,LetType), |
| 1426 | | % same_length(OExprs,NExprs),same_length(OTIds,NTIds), |
| 1427 | | % last(OTIds,OExprPred,OSubs),last(NTIds,NExprPred,NSubs), |
| 1428 | | % !. |
| 1429 | | syntaxtransformation_fixed(Expr,[],Subs,Names,[],NSubs,NExpr) :- |
| 1430 | | syntaxtransformation(Expr,Subs,Names,NSubs,NExpr). |
| 1431 | | |
| 1432 | | % note : LET substitution is dealt with differently as there we currently allow to use previously introduced IDs in RHS |
| 1433 | | %is_let_pred_or_expr(let_expression(TIds,Exprs,Expr),TIds,Exprs,Expr,let_expression). |
| 1434 | | %is_let_pred_or_expr(let_predicate(TIds,Exprs,Expr), TIds,Exprs,Expr,let_predicate). |
| 1435 | | %is_let_pred_or_expr(lazy_let_pred(ID,SharedExpr,Expr), [ID],[SharedExpr],Expr, lazy_let_pred). |
| 1436 | | %is_let_pred_or_expr(lazy_let_expr(ID,SharedExpr,Expr), [ID],[SharedExpr],Expr, lazy_let_expr). |
| 1437 | | %is_let_pred_or_expr(lazy_let_subst(ID,SharedExpr,Expr), [ID],[SharedExpr],Expr, lazy_let_subst). |
| 1438 | | |
| 1439 | | |
| 1440 | | |
| 1441 | | |
| 1442 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 1443 | | % rename identifier |
| 1444 | | |
| 1445 | | % r = {x|x : 1..y & x mod 2 = 1} |
| 1446 | | exists_ast(AST) :- AST = |
| 1447 | | b(equal(b(identifier(r),set(integer),[nodeid(none)]), |
| 1448 | | b(comprehension_set([b(identifier(x),integer,[nodeid(none)])], |
| 1449 | | b(conjunct(b(member(b(identifier(x),integer,[nodeid(none)]), |
| 1450 | | b(interval(b(integer(1),integer,[nodeid(none)]),b(identifier(y),integer,[nodeid(none)])), |
| 1451 | | set(integer),[nodeid(none)])),pred,[nodeid(none)]), |
| 1452 | | b(equal(b(modulo(b(identifier(x),integer,[nodeid(none)]), |
| 1453 | | b(integer(2),integer,[nodeid(none)])),integer,[contains_wd_condition,nodeid(none)]), |
| 1454 | | b(integer(1),integer,[nodeid(none)])),pred, |
| 1455 | | [contains_wd_condition,nodeid(none)])),pred,[contains_wd_condition,nodeid(none)])), |
| 1456 | | set(integer),[contains_wd_condition,nodeid(none)])), |
| 1457 | | pred,[contains_wd_condition,nodeid(none)]). |
| 1458 | | |
| 1459 | | :- assert_must_succeed((bsyntaxtree:exists_ast(A), rename_bt(A,[rename(x,xx)],RA), RA==A )). |
| 1460 | | :- assert_must_succeed((bsyntaxtree:exists_ast(A), rename_bt(A,[rename(r,v)],RA), |
| 1461 | | translate:translate_bexpression(RA,TR), TR='v = {x|x : 1 .. y & x mod 2 = 1}' )). |
| 1462 | | :- assert_must_succeed((gensym:reset_gensym, bsyntaxtree:exists_ast(A), rename_bt(A,[rename(y,x)],RA), RA \= A, |
| 1463 | | translate:translate_bexpression(RA,TR), |
| 1464 | | TR = 'r = {__FRESH____1|__FRESH____1 : 1 .. x & __FRESH____1 mod 2 = 1}' )). |
| 1465 | | |
| 1466 | | % a simplified version of replace_ids_by_exprs, which assumes target of renamings are variables |
| 1467 | | rename_bt(Expr,[],Res) :- !,Res=Expr. |
| 1468 | | rename_bt(OExpr,Renamings,NExpr) :- |
| 1469 | | create_texpr(Old,Type,OInfo,OExpr), |
| 1470 | | create_texpr(New,Type,NInfo,NExpr), |
| 1471 | | rename_in_infos(OInfo,Renamings,NInfo), |
| 1472 | | rename_bt2(Old,Renamings,New). |
| 1473 | | rename_bt2(identifier(Old),Renamings,identifier(New)) :- |
| 1474 | | !, rename_id(Old,Renamings,New). |
| 1475 | | rename_bt2(lazy_lookup_expr(Old),Renamings,lazy_lookup_expr(New)) :- |
| 1476 | | !, rename_id(Old,Renamings,New). |
| 1477 | | rename_bt2(lazy_lookup_pred(Old),Renamings,lazy_lookup_pred(New)) :- |
| 1478 | | !, rename_id(Old,Renamings,New). |
| 1479 | | rename_bt2(OExpr,Renamings,NExpr) :- |
| 1480 | | syntaxtransformation(OExpr,Subs,TNames,NSubs,NExpr), |
| 1481 | | get_texpr_exprs(TNames,Names), |
| 1482 | | remove_renamings(Names,Renamings,NRenamings), |
| 1483 | | rename_bt_l(Subs,NRenamings,NSubs). |
| 1484 | | rename_bt_l([],_,[]). |
| 1485 | | rename_bt_l([Old|ORest],Renamings,[New|NRest]) :- |
| 1486 | | rename_bt(Old,Renamings,New), |
| 1487 | | rename_bt_l(ORest,Renamings,NRest). |
| 1488 | | |
| 1489 | | remove_renamings([],Renamings,Renamings). |
| 1490 | | remove_renamings([identifier(Name)|Rest],Old,New) :- |
| 1491 | ? | ( select(rename(Name,_),Old,Inter1) -> true % Name no longer visible to renaming |
| 1492 | | ; Old = Inter1), |
| 1493 | | (member(rename(_OldName,Name),Inter1) -> |
| 1494 | | gensym('__FRESH__',FRESHID), |
| 1495 | | %print(variable_capture_in_rename(Name,from(OldName),FRESHID)),nl, |
| 1496 | | Inter2 = [rename(Name,FRESHID)|Inter1] |
| 1497 | | ; Inter2 = Inter1), |
| 1498 | | remove_renamings(Rest,Inter2,New). |
| 1499 | | |
| 1500 | | rename_in_infos(Old,Renamings,New) :- |
| 1501 | | ( has_info_to_rename(Old) -> |
| 1502 | | maplist(rename_in_infos2(Renamings),Old,New) |
| 1503 | | ; otherwise -> |
| 1504 | | Old = New). |
| 1505 | | rename_in_infos2(Renamings,OInfo,NInfo) :- |
| 1506 | | ( infos_to_rename(OInfo,OIds,SortedNIds,NInfo) -> |
| 1507 | | rename_ids(OIds,Renamings,NIds), |
| 1508 | | sort(NIds,SortedNIds) |
| 1509 | | ; otherwise -> |
| 1510 | | OInfo = NInfo). |
| 1511 | | |
| 1512 | | rename_ids([],_,[]). |
| 1513 | | rename_ids([OId|Orest],Renamings,[NId|Nrest]) :- |
| 1514 | | rename_id(OId,Renamings,NId), |
| 1515 | | rename_ids(Orest,Renamings,Nrest). |
| 1516 | | rename_id(Old,Renamings,New) :- |
| 1517 | | ( memberchk(rename(Old,New),Renamings) -> true % we could use ord_member if we sort ! |
| 1518 | | ; otherwise -> Old=New). |
| 1519 | | |
| 1520 | | has_info_to_rename(Infos) :- |
| 1521 | ? | member(I,Infos),infos_to_rename(I,_,_,_),!. |
| 1522 | | |
| 1523 | | infos_to_rename(modifies(O),O,N,modifies(N)). |
| 1524 | | infos_to_rename(reads(O),O,N,reads(N)). |
| 1525 | | infos_to_rename(non_det_modifies(O),O,N,non_det_modifies(N)). |
| 1526 | | infos_to_rename(modifies_locals(O),O,N,modifies_locals(N)). |
| 1527 | | infos_to_rename(reads_locals(O),O,N,reads_locals(N)). |
| 1528 | | infos_to_rename(used_ids(O),O,N,used_ids(N)). |
| 1529 | | |
| 1530 | | |
| 1531 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 1532 | | % remove type information for transformations |
| 1533 | | |
| 1534 | | remove_bt(b(Expr,Type,Infos),Expr,NExpr,b(NExpr,Type,Infos)). |
| 1535 | | |
| 1536 | | %remove_bt_l([],[],[],[]). |
| 1537 | | %remove_bt_l([OT|OTRest],[O|ORest],[N|NRest],[NT|NTRest]) :- |
| 1538 | | % remove_bt(OT,O,N,NT), |
| 1539 | | % remove_bt_l(OTRest,ORest,NRest,NTRest). |
| 1540 | | |
| 1541 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 1542 | | % traversations |
| 1543 | | % Takes a predicate or expression or substitution and extracts: |
| 1544 | | % the expression itself Expr, its type Type, the syntaxnode information Infos |
| 1545 | | % + the subexpressions as a list Subs and the local identifiers declared |
| 1546 | | syntaxtraversion(b(Expr,Type,Infos),Expr,Type,Infos,Subs,Names) :- !, |
| 1547 | | safe_syntaxelement(Expr,Subs,Names,_,_). |
| 1548 | | syntaxtraversion(IExpr,Expr,Type,Infos,Subs,Names) :- |
| 1549 | | add_internal_error('Not properly wrapped', syntaxtraversion(IExpr,Expr,Type,Infos,Subs,Names)), |
| 1550 | | fail. |
| 1551 | | |
| 1552 | | |
| 1553 | | map_over_full_bexpr_no_fail(P,BExpr) :- |
| 1554 | | syntaxtraversion(BExpr,Expr,_,_,Subs,_TNames), |
| 1555 | | call(P,Expr), % the predicate should not fail |
| 1556 | | (Subs=[] -> true ; maplist(map_over_full_bexpr_no_fail(P),Subs)). |
| 1557 | | |
| 1558 | | map_over_bexpr(P,BExpr) :- |
| 1559 | | syntaxtraversion(BExpr,Expr,_,_,Subs,_TNames), |
| 1560 | | (call(P,Expr) % should probably fail so that by backtrack we recurse |
| 1561 | | ; |
| 1562 | | member(Sub,Subs), map_over_bexpr(P,Sub) |
| 1563 | | ). |
| 1564 | | % same as above but gets typed expressions: |
| 1565 | | map_over_typed_bexpr(P,BExpr) :- |
| 1566 | ? | syntaxtraversion(BExpr,_Expr,_,_,Subs,_TNames), |
| 1567 | ? | (call(P,BExpr) |
| 1568 | | ; |
| 1569 | ? | member(Sub,Subs), map_over_typed_bexpr(P,Sub) |
| 1570 | | ). |
| 1571 | | % same as above but returns value: |
| 1572 | | map_over_typed_bexpr(P,BExpr,Result) :- |
| 1573 | | syntaxtraversion(BExpr,_Expr,_,_,Subs,_TNames), |
| 1574 | | (call(P,BExpr,Result) |
| 1575 | | ; |
| 1576 | | member(Sub,Subs), map_over_typed_bexpr(P,Sub,Result) |
| 1577 | | ). |
| 1578 | | |
| 1579 | | % same as map_over_expr but provides an accumulator passed top-down to children; needs to be used by failure driven loop |
| 1580 | | |
| 1581 | | map_over_bexpr_top_down_acc(P,BExpr,TDAcc) :- |
| 1582 | | syntaxtraversion(BExpr,Expr,_,_,Subs,_TNames), |
| 1583 | | (call(P,Expr,TDAcc,NewAcc) |
| 1584 | | -> member(Sub,Subs), map_over_bexpr_top_down_acc(P,Sub,NewAcc) |
| 1585 | | ; member(Sub,Subs), map_over_bexpr_top_down_acc(P,Sub,TDAcc) |
| 1586 | | ). |
| 1587 | | % now a version which gets the typed predicate as argument |
| 1588 | | |
| 1589 | | map_over_type_bexpr_top_down_acc(P,BExpr,TDAcc) :- |
| 1590 | | syntaxtraversion(BExpr,_Expr,_,_,Subs,_TNames), |
| 1591 | | (call(P,BExpr,TDAcc,NewAcc) |
| 1592 | | -> member(Sub,Subs), map_over_type_bexpr_top_down_acc(P,Sub,NewAcc) |
| 1593 | | ; member(Sub,Subs), map_over_type_bexpr_top_down_acc(P,Sub,TDAcc) |
| 1594 | | ). |
| 1595 | | |
| 1596 | | |
| 1597 | | reduce_over_bexpr(P,BExpr,InitialValue,ResultValue) :- |
| 1598 | ? | syntaxtraversion(BExpr,Expr,_,_,Subs,_TNames), |
| 1599 | ? | call(P,Expr,InitialValue,I1), % print(reduce(P,Expr,InitialValue,I1)),nl, |
| 1600 | ? | scanlist(reduce_over_bexpr(P),Subs,I1,ResultValue). |
| 1601 | | |
| 1602 | | % apply a predicate over a syntax tree (bottom-up) |
| 1603 | | |
| 1604 | | transform_bexpr(Pred,b(Expr,Type,Info),NewBExpr) :- |
| 1605 | | syntaxtransformation(Expr,Subs,_Names,NSubs,NewExpr1), |
| 1606 | | l_transform_bexpr(Subs,Pred,NSubs), |
| 1607 | ? | (call(Pred,b(NewExpr1,Type,Info),NewBExpr) -> true ; NewBExpr = b(NewExpr1,Type,Info)). |
| 1608 | | |
| 1609 | | l_transform_bexpr([],_,[]). |
| 1610 | | l_transform_bexpr([SubH|T],Pred,[TSubH|TT]) :- |
| 1611 | | transform_bexpr(Pred,SubH,TSubH), |
| 1612 | | l_transform_bexpr(T,Pred,TT). |
| 1613 | | |
| 1614 | | % apply a predicate over a syntax tree (bottom-up) with Accumulator result |
| 1615 | | % Accumulator is constructed bottom up; Pred receives *all* accumulators of sub expressions |
| 1616 | | |
| 1617 | | transform_bexpr_with_bup_accs(Pred,b(Expr,Type,Info),NewBExpr,EmptyAcc,Acc) :- |
| 1618 | | syntaxtransformation(Expr,Subs,_Names,NSubs,NewExpr1), |
| 1619 | | l_transform_bexpr_with_bup_accs(Subs,Pred,NSubs,EmptyAcc,SubAccs), |
| 1620 | | (call(Pred,b(NewExpr1,Type,Info),NewBExpr,SubAccs,Acc) -> true |
| 1621 | | ; NewBExpr = b(NewExpr1,Type,Info), Acc = EmptyAcc). |
| 1622 | | |
| 1623 | | l_transform_bexpr_with_bup_accs([],_,[],_,[]). |
| 1624 | | l_transform_bexpr_with_bup_accs([SubH|T],Pred,[TSubH|TT],EmptyAcc,[Acc1|RestAcc]) :- |
| 1625 | | transform_bexpr_with_bup_accs(Pred,SubH,TSubH,EmptyAcc,Acc1), |
| 1626 | | l_transform_bexpr_with_bup_accs(T,Pred,TT,EmptyAcc,RestAcc). |
| 1627 | | |
| 1628 | | % apply a predicate over a syntax tree (bottom-up) with Accumulator result |
| 1629 | | % a single Accumulator is passed along |
| 1630 | | |
| 1631 | | transform_bexpr_with_acc(_Pred,E,NewBExpr,InAcc,Acc) :- var(E),!, |
| 1632 | | NewBExpr=E, Acc=InAcc. |
| 1633 | | transform_bexpr_with_acc(Pred,b(Expr,Type,Info),NewBExpr,InAcc,Acc) :- |
| 1634 | | syntaxtransformation(Expr,Subs,_Names,NSubs,NewExpr1), |
| 1635 | | l_transform_bexpr_with_acc(Subs,Pred,NSubs,InAcc,SubAcc), |
| 1636 | | (call(Pred,b(NewExpr1,Type,Info),NewBExpr,SubAcc,Acc) -> true |
| 1637 | | ; NewBExpr = b(NewExpr1,Type,Info), Acc = SubAcc). |
| 1638 | | |
| 1639 | | l_transform_bexpr_with_acc([],_,[],Acc,Acc). |
| 1640 | | l_transform_bexpr_with_acc([SubH|T],Pred,[TSubH|TT],InAcc,ResAcc) :- |
| 1641 | | transform_bexpr_with_acc(Pred,SubH,TSubH,InAcc,Acc1), |
| 1642 | | l_transform_bexpr_with_acc(T,Pred,TT,Acc1,ResAcc). |
| 1643 | | |
| 1644 | | min_max_integer_value_used(BExpr,Min,Max) :- |
| 1645 | | min_max_integer_value_used(BExpr,none,none,Min,Max). |
| 1646 | | min_max_integer_value_used(BExpr,IMin,IMax,Min,Max) :- |
| 1647 | | reduce_over_bexpr(min_max_aux,BExpr,minmax(IMin,IMax),minmax(Min,Max)). |
| 1648 | | |
| 1649 | | min_max_aux(sequence_extension(L),minmax(Min,Max),minmax(NMin,NMax)) :- !, |
| 1650 | | length(L,Len), % we use implicitly numbers from 1..Len |
| 1651 | | ((number(Min),1>Min) -> NMin=Min ; NMin=1), |
| 1652 | | ((number(Max),Len<Max) -> NMax=Max ; NMax=Len). |
| 1653 | | min_max_aux(integer(N),minmax(Min,Max),minmax(NMin,NMax)) :- !, |
| 1654 | | ((number(Min),N>Min) -> NMin=Min ; NMin=N), |
| 1655 | | ((number(Max),N<Max) -> NMax=Max ; NMax=N). |
| 1656 | | min_max_aux(_,V,V). |
| 1657 | | |
| 1658 | | % check if a B expression uses something like NAT,NAT1,INT, MAXINT or MININT. |
| 1659 | | uses_implementable_integers(BExpr) :- |
| 1660 | | map_over_bexpr(uses_implementable_integers_aux,BExpr). |
| 1661 | | |
| 1662 | | uses_implementable_integers_aux(maxint). |
| 1663 | | uses_implementable_integers_aux(minint). |
| 1664 | | uses_implementable_integers_aux(integer_set(X)) :- |
| 1665 | | (X='NAT1' ; X='NAT' ; X='INT'). |
| 1666 | | |
| 1667 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 1668 | | % some checks |
| 1669 | | check_if_typed_predicate(b(Pred,X,_)) :- ground(X), X=pred, % at runtime there can be value(X) with variables inside ! |
| 1670 | | syntaxelement(Pred,_,_,_,_,pred). |
| 1671 | | check_if_typed_expression(b(Expr,Type,_)) :- |
| 1672 | | syntaxelement(Expr,_,_,_,_,expr), |
| 1673 | | Type \== pred, Type \== subst, ground(Type). |
| 1674 | | check_if_typed_substitution(b(Subst,X,_)) :- ground(X), X=subst, |
| 1675 | | syntaxelement(Subst,_,_,_,_,subst). |
| 1676 | | |
| 1677 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 1678 | | % transformations |
| 1679 | | |
| 1680 | | syntaxtransformation(Expr,Subs,Names,NSubs,NExpr) :- |
| 1681 | | functor(Expr,F,Arity), |
| 1682 | | functor(NExpr,F,Arity), |
| 1683 | | safe_syntaxelement(Expr,Subs,Names,Lists,Constant), |
| 1684 | | all_same_length(Lists,NLists), |
| 1685 | | syntaxelement(NExpr,NSubs,_,NLists,Constant,_). |
| 1686 | | |
| 1687 | | safe_syntaxelement(Expr,Subs,Names,Lists,Constant) :- |
| 1688 | | ( syntaxelement(Expr,SubsX,NamesX,Lists,ConstantX,_) -> |
| 1689 | | Subs=SubsX, Names=NamesX, Constant=ConstantX |
| 1690 | | ; otherwise -> |
| 1691 | | functor(Expr,F,Arity), |
| 1692 | | add_error_fail(bsyntaxtree,'Uncovered syntax element: ', F/Arity) |
| 1693 | | ). |
| 1694 | | |
| 1695 | | % syntaxelement(Expr,SubExprs,Identifiers,Lists,Constant,Type): |
| 1696 | | % Expr: the expression itself |
| 1697 | | % SubExprs: a list of sub-expressions |
| 1698 | | % Identifiers: a list of identifiers that are newly introduced (e.g. by a quantifier) |
| 1699 | | % Lists: A list of lists in the expression, to prevent infinite loops when having variable parts |
| 1700 | | % Constant: A part of the expression that is not a sub-expression (e.g. the number in integer(...)) |
| 1701 | | % Type: Fundamental type of the element (predicate, expression, etc) |
| 1702 | | |
| 1703 | | % predicates |
| 1704 | | syntaxelement(truth, [], [], [], [], pred). |
| 1705 | | syntaxelement(falsity, [], [], [], [], pred). |
| 1706 | | syntaxelement(conjunct(A,B), [A,B],[], [], [], pred). |
| 1707 | | syntaxelement(negation(A), [A], [], [], [], pred). |
| 1708 | | syntaxelement(disjunct(A,B), [A,B],[], [], [], pred). |
| 1709 | | syntaxelement(implication(A,B), [A,B],[], [], [], pred). |
| 1710 | | syntaxelement(equivalence(A,B), [A,B],[], [], [], pred). |
| 1711 | | syntaxelement(equal(A,B), [A,B],[], [], [], pred). |
| 1712 | | syntaxelement(not_equal(A,B), [A,B],[], [], [], pred). |
| 1713 | | syntaxelement(member(A,B), [A,B],[], [], [], pred). |
| 1714 | | syntaxelement(not_member(A,B), [A,B],[], [], [], pred). |
| 1715 | | syntaxelement(subset(A,B), [A,B],[], [], [], pred). |
| 1716 | | syntaxelement(subset_strict(A,B), [A,B],[], [], [], pred). |
| 1717 | | syntaxelement(not_subset(A,B), [A,B],[], [], [], pred). |
| 1718 | | syntaxelement(not_subset_strict(A,B),[A,B],[], [], [], pred). |
| 1719 | | syntaxelement(less_equal(A,B), [A,B],[], [], [], pred). |
| 1720 | | syntaxelement(less(A,B), [A,B],[], [], [], pred). |
| 1721 | | syntaxelement(greater_equal(A,B), [A,B],[], [], [], pred). |
| 1722 | | syntaxelement(greater(A,B), [A,B],[], [], [], pred). |
| 1723 | | syntaxelement(forall(Ids,D,P), [D,P|Ids],Ids,[Ids], [], pred). |
| 1724 | | syntaxelement(exists(Ids,P), [P|Ids], Ids,[Ids], [], pred). |
| 1725 | | syntaxelement(finite(A), [A], [], [], [], pred/only_typecheck). |
| 1726 | | syntaxelement(partition(S,Es), [S|Es],[],[Es],[],pred). |
| 1727 | | syntaxelement(kodkod(PId,Ids), Ids,[],[Ids],PId, pred). |
| 1728 | | syntaxelement(external_pred_call(F,Args),Args,[],[Args],F,pred). |
| 1729 | | |
| 1730 | | % expressions |
| 1731 | | syntaxelement(value(V), [], [], [], V, expr). |
| 1732 | | syntaxelement(operation_call_in_expr(Id,As), [Id|As], [], [As], [], expr). |
| 1733 | | syntaxelement(boolean_true, [], [], [], [], expr). |
| 1734 | | syntaxelement(boolean_false, [], [], [], [], expr). |
| 1735 | | syntaxelement(max_int, [], [], [], [], expr). |
| 1736 | | syntaxelement(min_int, [], [], [], [], expr). |
| 1737 | | syntaxelement(empty_set, [], [], [], [], expr). |
| 1738 | | syntaxelement(bool_set, [], [], [], [], expr). |
| 1739 | | syntaxelement(string_set, [], [], [], [], expr). |
| 1740 | | syntaxelement(convert_bool(A), [A], [], [], [], expr). |
| 1741 | | syntaxelement(add(A,B), [A,B],[], [], [], expr). |
| 1742 | | syntaxelement(minus(A,B), [A,B],[], [], [], expr). |
| 1743 | | syntaxelement(minus_or_set_subtract(A,B),[A,B],[], [], [], expr/only_typecheck). |
| 1744 | | syntaxelement(unary_minus(A), [A], [], [], [], expr). |
| 1745 | | syntaxelement(multiplication(A,B), [A,B],[], [], [], expr). |
| 1746 | | syntaxelement(mult_or_cart(A,B), [A,B],[], [], [], expr/only_typecheck). |
| 1747 | | syntaxelement(cartesian_product(A,B), [A,B],[], [], [], expr). |
| 1748 | | syntaxelement(div(A,B), [A,B],[], [], [], expr). |
| 1749 | | syntaxelement(floored_div(A,B), [A,B],[], [], [], expr). |
| 1750 | | syntaxelement(modulo(A,B), [A,B],[], [], [], expr). |
| 1751 | | syntaxelement(power_of(A,B), [A,B],[], [], [], expr). |
| 1752 | | syntaxelement(successor, [], [], [], [], expr). |
| 1753 | | syntaxelement(predecessor, [], [], [], [], expr). |
| 1754 | | syntaxelement(max(A), [A], [], [], [], expr). |
| 1755 | | syntaxelement(min(A), [A], [], [], [], expr). |
| 1756 | | syntaxelement(card(A), [A], [], [], [], expr). |
| 1757 | | syntaxelement(couple(A,B), [A,B],[], [], [], expr). |
| 1758 | | syntaxelement(pow_subset(A), [A], [], [], [], expr). |
| 1759 | | syntaxelement(pow1_subset(A), [A], [], [], [], expr). |
| 1760 | | syntaxelement(fin_subset(A), [A], [], [], [], expr). |
| 1761 | | syntaxelement(fin1_subset(A), [A], [], [], [], expr). |
| 1762 | | syntaxelement(interval(A,B), [A,B],[], [], [], expr). |
| 1763 | | syntaxelement(union(A,B), [A,B],[], [], [], expr). |
| 1764 | | syntaxelement(intersection(A,B), [A,B],[], [], [], expr). |
| 1765 | | syntaxelement(set_subtraction(A,B), [A,B],[], [], [], expr). |
| 1766 | | syntaxelement(general_union(A), [A], [], [], [], expr). |
| 1767 | | syntaxelement(general_intersection(A), [A] , [], [], [], expr). |
| 1768 | | syntaxelement(relations(A,B), [A,B],[], [], [], expr). |
| 1769 | | syntaxelement(identity(A), [A], [], [], [], expr). |
| 1770 | | syntaxelement(event_b_identity, [], [], [], [], expr). % for Rodin 1.0, TO DO: Daniel please check |
| 1771 | | syntaxelement(reverse(A), [A], [], [], [], expr). |
| 1772 | | syntaxelement(first_projection(A,B), [A,B],[], [], [], expr/only_typecheck). |
| 1773 | | syntaxelement(first_of_pair(A), [A], [], [], [], expr). |
| 1774 | | syntaxelement(event_b_first_projection(A),[A], [], [], [], expr/only_typecheck). |
| 1775 | | syntaxelement(event_b_first_projection_v2,[], [], [], [], expr/only_typecheck). % for Rodin 1.0, TO DO: Daniel please check |
| 1776 | | syntaxelement(second_projection(A,B), [A,B],[], [], [], expr/only_typecheck). |
| 1777 | | syntaxelement(event_b_second_projection_v2,[], [], [], [], expr/only_typecheck). % for Rodin 1.0, TO DO: Daniel please check |
| 1778 | | syntaxelement(second_of_pair(A), [A], [], [], [], expr). |
| 1779 | | syntaxelement(event_b_second_projection(A),[A], [], [], [], expr/only_typecheck). |
| 1780 | | syntaxelement(composition(A,B), [A,B],[], [], [], expr). |
| 1781 | | syntaxelement(ring(A,B), [A,B],[], [], [], expr/only_typecheck). |
| 1782 | | syntaxelement(direct_product(A,B), [A,B],[], [], [], expr). |
| 1783 | | syntaxelement(parallel_product(A,B), [A,B],[], [], [], expr). |
| 1784 | | syntaxelement(trans_function(A), [A], [], [], [], expr). |
| 1785 | | syntaxelement(trans_relation(A), [A], [], [], [], expr). |
| 1786 | | syntaxelement(iteration(A,B), [A,B],[], [], [], expr). |
| 1787 | | syntaxelement(reflexive_closure(A), [A], [], [], [], expr). |
| 1788 | | syntaxelement(closure(A), [A], [], [], [], expr). |
| 1789 | | syntaxelement(domain(A), [A], [], [], [], expr). |
| 1790 | | syntaxelement(range(A), [A], [], [], [], expr). |
| 1791 | | syntaxelement(image(A,B), [A,B],[], [], [], expr). |
| 1792 | | syntaxelement(domain_restriction(A,B), [A,B],[], [], [], expr). |
| 1793 | | syntaxelement(domain_subtraction(A,B), [A,B],[], [], [], expr). |
| 1794 | | syntaxelement(range_restriction(A,B), [A,B],[], [], [], expr). |
| 1795 | | syntaxelement(range_subtraction(A,B), [A,B],[], [], [], expr). |
| 1796 | | syntaxelement(overwrite(A,B), [A,B],[], [], [], expr). |
| 1797 | | syntaxelement(partial_function(A,B), [A,B],[], [], [], expr). |
| 1798 | | syntaxelement(total_function(A,B), [A,B],[], [], [], expr). |
| 1799 | | syntaxelement(partial_injection(A,B), [A,B],[], [], [], expr). |
| 1800 | | syntaxelement(total_injection(A,B), [A,B],[], [], [], expr). |
| 1801 | | syntaxelement(partial_surjection(A,B), [A,B],[], [], [], expr). |
| 1802 | | syntaxelement(total_surjection(A,B), [A,B],[], [], [], expr). |
| 1803 | | syntaxelement(total_bijection(A,B), [A,B],[], [], [], expr). |
| 1804 | | syntaxelement(partial_bijection(A,B), [A,B],[], [], [], expr). |
| 1805 | | syntaxelement(total_relation(A,B), [A,B],[], [], [], expr). |
| 1806 | | syntaxelement(surjection_relation(A,B),[A,B],[], [], [], expr). |
| 1807 | | syntaxelement(total_surjection_relation(A,B),[A,B],[], [], [], expr). |
| 1808 | | syntaxelement(seq(A), [A], [], [], [], expr). |
| 1809 | | syntaxelement(seq1(A), [A], [], [], [], expr). |
| 1810 | | syntaxelement(iseq(A), [A], [], [], [], expr). |
| 1811 | | syntaxelement(iseq1(A), [A], [], [], [], expr). |
| 1812 | | syntaxelement(perm(A), [A], [], [], [], expr). |
| 1813 | | syntaxelement(empty_sequence, [], [], [], [], expr). |
| 1814 | | syntaxelement(size(A), [A], [], [], [], expr). |
| 1815 | | syntaxelement(first(A), [A], [], [], [], expr). |
| 1816 | | syntaxelement(last(A), [A], [], [], [], expr). |
| 1817 | | syntaxelement(front(A), [A], [], [], [], expr). |
| 1818 | | syntaxelement(tail(A), [A], [], [], [], expr). |
| 1819 | | syntaxelement(rev(A), [A], [], [], [], expr). |
| 1820 | | syntaxelement(concat(A,B), [A,B],[], [], [], expr). |
| 1821 | | syntaxelement(insert_front(A,B), [A,B],[], [], [], expr). |
| 1822 | | syntaxelement(insert_tail(A,B), [A,B],[], [], [], expr). |
| 1823 | | syntaxelement(restrict_front(A,B), [A,B],[], [], [], expr). |
| 1824 | | syntaxelement(restrict_tail(A,B), [A,B],[], [], [], expr). |
| 1825 | | syntaxelement(general_concat(A), [A], [], [], [], expr). |
| 1826 | | syntaxelement(function(A,B), [A,B],[], [], [], expr). |
| 1827 | | syntaxelement(external_function_call(F,Args),Args,[],[Args],F,expr). |
| 1828 | | syntaxelement(identifier(I), [], [], [], I, expr). |
| 1829 | | syntaxelement(lazy_lookup_expr(I), [], [], [], I, expr). |
| 1830 | | syntaxelement(lazy_lookup_pred(I), [], [], [], I, pred). |
| 1831 | | syntaxelement(integer(I), [], [], [], I, expr). |
| 1832 | | syntaxelement(integer_set(T), [], [], [], T, expr). |
| 1833 | | syntaxelement(string(S), [], [], [], S, expr). |
| 1834 | | syntaxelement(set_extension(L), L, [], [L], [], expr). |
| 1835 | | syntaxelement(sequence_extension(L), L, [], [L], [], expr). |
| 1836 | | syntaxelement(comprehension_set(Ids,P),[P|Ids], Ids,[Ids], [], expr). |
| 1837 | | syntaxelement(event_b_comprehension_set(Ids,E,P),[E,P|Ids], Ids,[Ids], [], expr/only_typecheck). |
| 1838 | | syntaxelement(lambda(Ids,P,E), [P,E|Ids],Ids,[Ids], [], expr). |
| 1839 | | syntaxelement(general_sum(Ids,P,E), [P,E|Ids],Ids,[Ids], [], expr). |
| 1840 | | syntaxelement(general_product(Ids,P,E), [P,E|Ids],Ids,[Ids], [], expr). |
| 1841 | | syntaxelement(quantified_union(Ids,P,E), [P,E|Ids],Ids,[Ids], [], expr). |
| 1842 | | syntaxelement(quantified_intersection(Ids,P,E), [P,E|Ids],Ids,[Ids], [], expr). |
| 1843 | | syntaxelement(struct(Rec), [Rec], [], [], [], expr). |
| 1844 | | syntaxelement(rec(Fields), FContent, [], [FContent], FNames, expr) :- syntaxfields(Fields,FContent, FNames). |
| 1845 | | syntaxelement(record_field(R,I), [R], [], [], I, expr). |
| 1846 | | syntaxelement(assertion_expression(Cond,ErrMsg,Expr), [Cond,Expr], [], [], ErrMsg, expr). |
| 1847 | | syntaxelement(typeset, [], [], [], [], expr/only_typecheck). |
| 1848 | | |
| 1849 | | syntaxelement(tree(A), [A], [], [], [], expr). |
| 1850 | | syntaxelement(btree(A), [A], [], [], [], expr). |
| 1851 | | syntaxelement(const(A,B), [A,B],[], [], [], expr). |
| 1852 | | syntaxelement(top(A), [A], [], [], [], expr). |
| 1853 | | syntaxelement(sons(A), [A], [], [], [], expr). |
| 1854 | | syntaxelement(prefix(A), [A], [], [], [], expr). |
| 1855 | | syntaxelement(postfix(A), [A], [], [], [], expr). |
| 1856 | | syntaxelement(sizet(A), [A], [], [], [], expr). |
| 1857 | | syntaxelement(mirror(A), [A], [], [], [], expr). |
| 1858 | | syntaxelement(rank(A,B), [A,B],[], [], [], expr). |
| 1859 | | syntaxelement(father(A,B), [A,B],[], [], [], expr). |
| 1860 | | syntaxelement(son(A,B,C), [A,B,C],[], [], [], expr). |
| 1861 | | syntaxelement(subtree(A,B), [A,B],[], [], [], expr). |
| 1862 | | syntaxelement(arity(A,B), [A,B],[], [], [], expr). |
| 1863 | | syntaxelement(bin(A), [A],[], [], [], expr). |
| 1864 | | syntaxelement(bin(A,B,C), [A,B,C],[], [], [], expr). |
| 1865 | | syntaxelement(infix(A), [A], [], [], [], expr). |
| 1866 | | syntaxelement(left(A), [A], [], [], [], expr). |
| 1867 | | syntaxelement(right(A), [A], [], [], [], expr). |
| 1868 | | |
| 1869 | | % substitutions |
| 1870 | | syntaxelement(skip, [], [], [], [], subst). |
| 1871 | | syntaxelement(precondition(A,B), [A,B],[], [], [], subst). |
| 1872 | | syntaxelement(assertion(A,B), [A,B],[], [], [], subst). |
| 1873 | | syntaxelement(if_elsif(A,B), [A,B],[], [], [], subst/elsif). |
| 1874 | | syntaxelement(while(A,B,C,D), [A,B,C,D],[], [], [], subst). |
| 1875 | | % used only internally in the interpreter, contains last value of variant: |
| 1876 | | syntaxelement(while1(A,B,C,D,E), [A,B,C,D],[], [], E, subst). |
| 1877 | | syntaxelement(select_when(A,B), [A,B],[], [], [], subst/when). |
| 1878 | | syntaxelement(block(S),[S],[],[],[], subst/only_typecheck). |
| 1879 | | syntaxelement(assign(Lhs,Rhs),Exprs,[],[Lhs,Rhs], [], subst) :- append(Lhs,Rhs,Exprs). |
| 1880 | | syntaxelement(assign_single_id(Id,Rhs),[Id,Rhs],[],[], [], subst). |
| 1881 | | syntaxelement(any(Ids,P,S),[P,S|Ids],Ids,[Ids], [], subst). |
| 1882 | | syntaxelement(var(Ids,S), [S|Ids], Ids,[Ids], [], subst). |
| 1883 | | syntaxelement(if(Ifs), Ifs, [], [Ifs], [], subst). |
| 1884 | | syntaxelement(parallel(Ss), Ss, [], [Ss], [], subst). |
| 1885 | | syntaxelement(sequence(Ss), Ss, [], [Ss], [], subst). |
| 1886 | | syntaxelement(becomes_element_of(Ids,E), [E|Ids], [], [Ids], [], subst). |
| 1887 | | syntaxelement(becomes_such(Ids,P), [P|Ids], [], [Ids], [], subst). |
| 1888 | | syntaxelement(evb2_becomes_such(Ids,P), [P|Ids], [], [Ids], [], subst/only_typecheck). |
| 1889 | | syntaxelement(let(Ids,P,S), [P,S|Ids], Ids, [Ids], [], subst). |
| 1890 | | syntaxelement(operation_call(Id,Rs,As), [Id|Exprs], [], [Rs,As], [], subst) :- append(Rs,As,Exprs). |
| 1891 | | syntaxelement(case(E,Eithers,Else), [E,Else|Eithers], [], [Eithers], [], subst). |
| 1892 | | syntaxelement(case_or(Es,S), [S|Es], [], [Es], [], subst/caseor). |
| 1893 | | syntaxelement(choice(Ss), Ss, [], [Ss], [], subst). |
| 1894 | | syntaxelement(select(Whens), Whens, [], [Whens], [], subst). |
| 1895 | | syntaxelement(select(Whens,Else), [Else|Whens], [], [Whens], [], subst). |
| 1896 | | syntaxelement(operation(I,Rs,As,B), [I,B|Ids], Ids, [Rs,As], [], subst) :- append(Rs,As,Ids). |
| 1897 | | syntaxelement(external_subst_call(F,Args),Args,[],[Args],F,subst). |
| 1898 | | |
| 1899 | | % elements of a VALUES clause |
| 1900 | | syntaxelement(values_entry(I,E),[I,E],[],[],[],values_entry). |
| 1901 | | |
| 1902 | | % syntax for Event-B events |
| 1903 | | syntaxelement(rlevent(I,Sec,St,Ps,G,Ts,As,VWs,PWs,Ums,Rs), Subs, [], [Ps,Ts,As,VWs,PWs,Ums,Rs], [I,Sec], subst) :- |
| 1904 | | append([[St],Ps,[G],Ts,As,VWs,PWs,Ums,Rs],Subs). |
| 1905 | | syntaxelement(witness(I,P), [I,P], [], [], [], witness). |
| 1906 | | |
| 1907 | | % extended syntax for Z |
| 1908 | | syntaxelement(let_predicate(Ids,As,Pred), Exprs, Ids, [Ids,As], [], pred) :- append([Ids,As,[Pred]],Exprs). |
| 1909 | | syntaxelement(let_expression(Ids,As,Expr), Exprs, Ids, [Ids,As], [], expr) :- append([Ids,As,[Expr]],Exprs). |
| 1910 | | syntaxelement(let_expression_global(Ids,As,Expr), Exprs, Ids, [Ids,As], [], expr) :- % version used by b_compiler |
| 1911 | | append([Ids,As,[Expr]],Exprs). |
| 1912 | | syntaxelement(lazy_let_expr(TID,A,Expr), Exprs, [TID], [[TID],[A]], [], expr) :- |
| 1913 | | append([[TID],[A],[Expr]],Exprs). |
| 1914 | | syntaxelement(lazy_let_pred(TID,A,Expr), Exprs, [TID], [[TID],[A]], [], pred) :- |
| 1915 | | append([[TID],[A],[Expr]],Exprs). |
| 1916 | | syntaxelement(lazy_let_subst(TID,A,Expr), Exprs, [TID], [[TID],[A]], [], subst) :- |
| 1917 | | append([[TID],[A],[Expr]],Exprs). |
| 1918 | | syntaxelement(if_then_else(If,Then,Else),[If,Then,Else], [], [], [], expr). |
| 1919 | | syntaxelement(compaction(A), [A], [], [], [], expr). |
| 1920 | | syntaxelement(mu(A), [A], [], [], [], expr). |
| 1921 | | syntaxelement(bag_items(A), [A], [], [], [], expr). |
| 1922 | | |
| 1923 | | syntaxelement(freetype_set(Id), [], [], [], Id, expr). |
| 1924 | | syntaxelement(freetype_case(Type,Case,Expr), [Expr], [], [], [Type,Case], pred). |
| 1925 | | syntaxelement(freetype_constructor(Type,Case,Expr), [Expr], [], [], [Type,Case], expr). |
| 1926 | | syntaxelement(freetype_destructor(Type,Case,Expr), [Expr], [], [], [Type,Case], expr). |
| 1927 | | |
| 1928 | | syntaxelement(ordinary, [], [], [], [], status). |
| 1929 | | syntaxelement(anticipated(Variant), [Variant], [], [], [], status). |
| 1930 | | syntaxelement(convergent(Variant), [Variant], [], [], [], status). |
| 1931 | | |
| 1932 | | % Just one ID expected |
| 1933 | | syntaxelement(recursive_let(Id,C),[Id,C],[Id],[],[], expr). |
| 1934 | | |
| 1935 | | |
| 1936 | | % fields of records |
| 1937 | | %syntaxfields(Fields,C,_) :- var(Fields),var(C),var(N),!, add_internal_error('Illegal call: ',syntaxfields(Fields,C,N)),fail. |
| 1938 | | syntaxfields([],[],[]). |
| 1939 | | syntaxfields([field(N,C)|Rest],[C|CRest],[N|NRest]) :- syntaxfields(Rest,CRest,NRest). |
| 1940 | | |
| 1941 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 1942 | | % helper for declaration of quantified identifiers |
| 1943 | | |
| 1944 | | % has_declared_identifier/2 returns a list of identifiers which are declared in |
| 1945 | | % this AST node. The main difference to the Names variable when doing a |
| 1946 | | % syntaxtraversion/6 or similiar is that the identifiers are described by |
| 1947 | | % predicates. |
| 1948 | | has_declared_identifier(TExpr,Ids) :- |
| 1949 | | get_texpr_expr(TExpr,Expr), |
| 1950 | | ( default_declaration(Expr,_,Ids,_) |
| 1951 | | ; non_default_declaration(Expr,Ids)). |
| 1952 | | |
| 1953 | | add_declaration_for_identifier(TExpr,Decl,NTExpr) :- |
| 1954 | | remove_bt(TExpr,Expr,NExpr,NTExpr), |
| 1955 | | ( default_declaration(Expr,Predicate,Ids,Constant) -> |
| 1956 | | same_functor(Expr,NExpr), |
| 1957 | | conjunct_predicates([Decl,Predicate],NPredicate), |
| 1958 | | default_declaration(NExpr,NPredicate,Ids,Constant) |
| 1959 | | ; non_default_declaration(Expr,_Ids) -> |
| 1960 | | add_non_default_declaration(Expr,Decl,NExpr)). |
| 1961 | | |
| 1962 | | :- use_module(probsrc(btypechecker), [prime_identifiers/2]). |
| 1963 | | |
| 1964 | | default_declaration(forall(Ids,D,P),D,Ids,P). |
| 1965 | | default_declaration(exists(Ids,P),P,Ids,[]). |
| 1966 | | default_declaration(comprehension_set(Ids,P),P,Ids,[]). |
| 1967 | | default_declaration(lambda(Ids,P,E),P,Ids,E). |
| 1968 | | default_declaration(general_sum(Ids,P,E),P,Ids,E). |
| 1969 | | default_declaration(general_product(Ids,P,E),P,Ids,E). |
| 1970 | | default_declaration(quantified_union(Ids,P,E),P,Ids,E). |
| 1971 | | default_declaration(quantified_intersection(Ids,P,E),P,Ids,E). |
| 1972 | | default_declaration(any(Ids,P,S),P,Ids,S). |
| 1973 | | default_declaration(becomes_such(Ids,P),P,Ids,[]). |
| 1974 | | default_declaration(evb2_becomes_such(Ids,P),P,Primed,[]) :- nl,print(evb2(Ids,Primed)),nl,nl, % no longer used, as it is translated to becomes_such |
| 1975 | | prime_identifiers(Ids,Primed). |
| 1976 | | default_declaration(rlevent(I,Sec,St,Ps,G,Ts,As,VWs,PWs,Ums,Rs),G,Ps, |
| 1977 | | [I,Sec,St,Ps,Ts,As,VWs,PWs,Ums,Rs]). |
| 1978 | | |
| 1979 | | non_default_declaration(operation(_I,Rs,As,_TBody),Ids) :- |
| 1980 | | append(Rs,As,Ids). |
| 1981 | | |
| 1982 | | add_non_default_declaration(operation(I,Rs,As,TBody),Decl,operation(I,Rs,As,NTBody)) :- |
| 1983 | | ( remove_bt(TBody,precondition(P,S),precondition(NP,S),NTBody) -> |
| 1984 | | conjunct_predicates([Decl,P],NP) |
| 1985 | | ; otherwise -> |
| 1986 | | create_texpr(precondition(Decl,TBody),subst,[],NTBody)). |
| 1987 | | |
| 1988 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 1989 | | % pattern definitions (not yet finished) |
| 1990 | | |
| 1991 | | bsyntax_pattern(Expr,TExpr) :- |
| 1992 | | var(Expr),!,Expr=TExpr. |
| 1993 | | bsyntax_pattern(-Expr,TExpr) :- |
| 1994 | | !,remove_all_infos(Expr,TExpr). |
| 1995 | | bsyntax_pattern(Expr,TExpr) :- |
| 1996 | | functor(Expr,b,3),!,Expr=TExpr. |
| 1997 | | bsyntax_pattern(Expr:Type/Info,TExpr) :- |
| 1998 | | !,bsyntax_pattern2(Expr,Type,Info,TExpr). |
| 1999 | | bsyntax_pattern(Expr:Type,TExpr) :- |
| 2000 | | !,bsyntax_pattern2(Expr,Type,_Info,TExpr). |
| 2001 | | bsyntax_pattern(Expr/Info,TExpr) :- |
| 2002 | | !,bsyntax_pattern2(Expr,_Type,Info,TExpr). |
| 2003 | | bsyntax_pattern(Expr,TExpr) :- |
| 2004 | | !,bsyntax_pattern2(Expr,_Type,_Info,TExpr). |
| 2005 | | |
| 2006 | | bsyntax_pattern2(Pattern,Type,Info,TExpr) :- |
| 2007 | | functor(Pattern,Functor,Arity), |
| 2008 | | functor(R,Functor,Arity), |
| 2009 | | create_texpr(R,Type,Info,TExpr), |
| 2010 | | syntaxelement(Pattern,PSubs,_,PLists,Const,EType), |
| 2011 | | syntaxelement(R,RSubs,_,RLists,Const,EType), |
| 2012 | | ( EType==pred -> Type=pred |
| 2013 | | ; EType==subst -> Type=subst |
| 2014 | | ; otherwise -> true), |
| 2015 | | all_same_length(PLists,RLists), |
| 2016 | | maplist(bsyntax_pattern,PSubs,RSubs). |
| 2017 | | |
| 2018 | | all_same_length([],[]). |
| 2019 | | all_same_length([A|Arest],[B|Brest]) :- |
| 2020 | | ( var(A),var(B) -> |
| 2021 | | add_error_fail(bsyntaxtree,'At least one list should be nonvar',[A,B]) |
| 2022 | | ; otherwise -> |
| 2023 | | same_length(A,B)), |
| 2024 | | all_same_length(Arest,Brest). |
| 2025 | | |
| 2026 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 2027 | | % strip an AST into a more compact form (without b/3 terms) |
| 2028 | | |
| 2029 | | strip_and_norm_ast(TExpr,SNExpr) :- |
| 2030 | | get_texpr_expr(TExpr,Expr), |
| 2031 | | strip_and_norm_ast_aux(Expr,SNExpr). |
| 2032 | | |
| 2033 | | :- use_module(tools,[safe_univ_no_cutoff/2]). |
| 2034 | | strip_and_norm_ast_aux(Expr,Res) :- |
| 2035 | | comm_assoc_subs(Expr,Op,Subs,[]), !, % associative & commutative operator detected |
| 2036 | | %print(assoc(Op)),nl, |
| 2037 | | maplist(strip_and_norm_ast_aux,Subs,NSubs), % Subs are already unwrapped |
| 2038 | | sort(NSubs,Sorted), % in case there are associative operators that are not commutative: insert is_commutative check |
| 2039 | | safe_univ_no_cutoff(Res,[Op|Sorted]). |
| 2040 | | strip_and_norm_ast_aux(Expr,Res) :- |
| 2041 | | assoc_subs(Expr,Op,Subs,[]), !, % associative operator detected |
| 2042 | | %print(assoc(Op)),nl, |
| 2043 | | maplist(strip_and_norm_ast_aux,Subs,NSubs), % Subs are already unwrapped |
| 2044 | | safe_univ_no_cutoff(Res,[Op|NSubs]). |
| 2045 | | strip_and_norm_ast_aux(Expr,SNExpr) :- |
| 2046 | | syntaxtransformation(Expr,Subs,_,NSubs,SExpr), |
| 2047 | | strip_and_norm_ast_l(Subs,NSubs), |
| 2048 | | norm_strip(SExpr,SNExpr). |
| 2049 | | |
| 2050 | | strip_and_norm_ast_l([],[]). |
| 2051 | | strip_and_norm_ast_l([TExpr|Trest],[NExpr|Nrest]) :- |
| 2052 | | strip_and_norm_ast(TExpr,NExpr), |
| 2053 | | strip_and_norm_ast_l(Trest,Nrest). |
| 2054 | | |
| 2055 | | norm_strip(greater_equal(A,B),less_equal(B,A)) :- !. |
| 2056 | | norm_strip(greater(A,B),less(B,A)) :- !. |
| 2057 | | norm_strip(set_extension(NL),set_extension(SNL)) :- !, |
| 2058 | | sort(NL,SNL). |
| 2059 | | norm_strip(Old,New) :- |
| 2060 | | functor(Old,Functor,2), |
| 2061 | | is_commutative(Functor),!, |
| 2062 | | arg(1,Old,OA), |
| 2063 | | arg(2,Old,OB), |
| 2064 | | ( OA @> OB -> New =.. [Functor,OB,OA] |
| 2065 | | ; New=Old). |
| 2066 | | norm_strip(Old,Old). |
| 2067 | | % TO DO: flatten associative operators into lists ! |
| 2068 | | |
| 2069 | | comm_assoc_subs(conjunct(TA,TB),conjunct) --> !, |
| 2070 | | {get_texpr_expr(TA,A), get_texpr_expr(TB,B)}, |
| 2071 | | comm_assoc_subs(A,conjunct), comm_assoc_subs(B,conjunct). |
| 2072 | | comm_assoc_subs(disjunct(TA,TB),disjunct) --> !, |
| 2073 | | {get_texpr_expr(TA,A), get_texpr_expr(TB,B)}, |
| 2074 | | comm_assoc_subs(A,disjunct), comm_assoc_subs(B,disjunct). |
| 2075 | | comm_assoc_subs(add(TA,TB),add) --> !, |
| 2076 | | {get_texpr_expr(TA,A), get_texpr_expr(TB,B)}, |
| 2077 | | comm_assoc_subs(A,add), comm_assoc_subs(B,add). |
| 2078 | | comm_assoc_subs(multiplication(TA,TB),multiplication) --> !, |
| 2079 | | {get_texpr_expr(TA,A), get_texpr_expr(TB,B)}, |
| 2080 | | comm_assoc_subs(A,multiplication), comm_assoc_subs(B,multiplication). |
| 2081 | | comm_assoc_subs(union(TA,TB),union) --> !, |
| 2082 | | {get_texpr_expr(TA,A), get_texpr_expr(TB,B)}, |
| 2083 | | comm_assoc_subs(A,union), comm_assoc_subs(B,union). |
| 2084 | | comm_assoc_subs(intersection(TA,TB),intersection) --> !, |
| 2085 | | {get_texpr_expr(TA,A), get_texpr_expr(TB,B)}, |
| 2086 | | comm_assoc_subs(A,intersection), comm_assoc_subs(B,intersection). |
| 2087 | | comm_assoc_subs(Expr,Op) --> {nonvar(Op)},[Expr]. % base case for other operators |
| 2088 | | |
| 2089 | | % detect just associative operators |
| 2090 | | assoc_subs(concat(TA,TB),concat) --> !, |
| 2091 | | {get_texpr_expr(TA,A), get_texpr_expr(TB,B)}, |
| 2092 | | assoc_subs(A,concat), assoc_subs(B,concat). |
| 2093 | | assoc_subs(composition(TA,TB),composition) --> !, |
| 2094 | | {get_texpr_expr(TA,A), get_texpr_expr(TB,B)}, |
| 2095 | | assoc_subs(A,composition), assoc_subs(B,composition). |
| 2096 | | assoc_subs(Expr,Op) --> {nonvar(Op)},[Expr]. % base case for other operators |
| 2097 | | |
| 2098 | | is_commutative(conjunct). |
| 2099 | | is_commutative(disjunct). |
| 2100 | | is_commutative(equivalence). |
| 2101 | | is_commutative(equal). |
| 2102 | | is_commutative(not_equal). |
| 2103 | | is_commutative(add). |
| 2104 | | is_commutative(multiplication). |
| 2105 | | is_commutative(union). |
| 2106 | | is_commutative(intersection). |
| 2107 | | |
| 2108 | | % check if two type expressions are same modulo info fields and reordering of commutative operators |
| 2109 | | % same_texpr does not reorder wrt commutativity. |
| 2110 | | same_norm_texpr(TExpr1,TExpr2) :- |
| 2111 | | strip_and_norm_ast(TExpr1,N1), %print(n1(N1)),nl, |
| 2112 | | strip_and_norm_ast(TExpr2,N1). %print(n2(N2)),nl, N1=N2. |
| 2113 | | |
| 2114 | | % ------------------------- |
| 2115 | | |
| 2116 | | % check if a ProB type is a set type: |
| 2117 | | is_set_type(set(Type),Type). |
| 2118 | | is_set_type(seq(Type),couple(integer,Type)). |
| 2119 | | % 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 |
| 2120 | | % is_set_type(any,any). |
| 2121 | | |
| 2122 | | get_set_type(TypeX,Res) :- |
| 2123 | ? | (is_set_type(TypeX,SetType) -> Res=SetType ; add_error_fail(get_set_type,'Not a set type: ',TypeX)). |
| 2124 | | |
| 2125 | | get_texpr_set_type(X,Res) :- get_texpr_type(X,TypeX), |
| 2126 | | get_set_type(TypeX,Res). |
| 2127 | | |
| 2128 | | |
| 2129 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 2130 | | % check if a set contains all elements of a type, i.e., maximal type |
| 2131 | | is_just_type(Expr) :- is_just_type(Expr,[]). |
| 2132 | | % is_just_type(+Expr,+RTT): |
| 2133 | | % like is_just_type/1 but RTT is a list of identifiers (without type information) |
| 2134 | | % of variables or constants that are known to be types, too. |
| 2135 | | % E.g. is_just_type(a ** INTEGER) would fail but is_just_type(a ** INTEGER,[a]) would |
| 2136 | | % succeed. |
| 2137 | | is_just_type(b(E,T,I),RTT) :- is_just_type3(E,T,I,RTT). |
| 2138 | | |
| 2139 | | |
| 2140 | | is_just_type3(identifier(G),set(Type),Infos,RefsToTypes) :- |
| 2141 | ? | ( Type = global(G), memberchk(given_set,Infos) |
| 2142 | | ; memberchk(G,RefsToTypes)),!. |
| 2143 | | is_just_type3(freetype_set(_),_,_,_). |
| 2144 | | is_just_type3(pow_subset(E),_,_,RTT) :- is_just_type(E,RTT). |
| 2145 | | is_just_type3(fin_subset(E),T,_,RTT) :- \+ is_infinite_type(T),is_just_type(E,RTT). |
| 2146 | | is_just_type3(integer_set('INTEGER'),set(integer),_,_). |
| 2147 | | is_just_type3(bool_set,set(boolean),_,_). |
| 2148 | | is_just_type3(string_set,set(string),_,_). |
| 2149 | | is_just_type3(cartesian_product(A,B),_,_,RTT) :- |
| 2150 | | is_just_type(A,RTT),is_just_type(B,RTT). |
| 2151 | | is_just_type3(mult_or_cart(A,B),_,_,RTT) :- % is_just_type/1 could be called before the cleanup |
| 2152 | | is_just_type(A,RTT),is_just_type(B,RTT). % of an expression has finished |
| 2153 | | is_just_type3(relations(A,B),_,_,RTT) :- |
| 2154 | | is_just_type(A,RTT),is_just_type(B,RTT). |
| 2155 | | is_just_type3(struct(b(rec(Fields),_,_)),_,_,RTT) :- |
| 2156 | | maplist(field_is_just_type(RTT),Fields). |
| 2157 | | is_just_type3(typeset,_,_,_). |
| 2158 | | is_just_type3(comprehension_set(_,b(truth,_,_)),_,_,_). |
| 2159 | | is_just_type3(value(Val),ST,_,_) :- is_set_type(ST,Type), is_maximal_value(Val,Type). % also see: quick_is_definitely_maximal_set(Val). |
| 2160 | | |
| 2161 | | field_is_just_type(RTT,field(_,Set)) :- is_just_type(Set,RTT). |
| 2162 | | |
| 2163 | | is_maximal_value(V,_) :- var(V),!,fail. |
| 2164 | | 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) |
| 2165 | | |
| 2166 | | % Generate a custom matching / visitor predicate |
| 2167 | | % bsyntaxtree:gen_visitor(bexpr_variables_aux,bexpr_variables) |
| 2168 | | /* |
| 2169 | | gen_visitor(Pred, BodyPred) :- syntaxelement(Expr,SubsX,_NamesX,_Lists,_ConstantX,_), |
| 2170 | | print_clause(Pred,BodyPred,Expr,SubsX), |
| 2171 | | fail. |
| 2172 | | gen_visitor(Pred, BodyPred) :- nl. |
| 2173 | | |
| 2174 | | print_clause(Pred,BodyPred,Expr,SubsX) :- E=..[Op|SubsX], format('~w(~w) :- ',[Pred,Expr]). |
| 2175 | | */ |
| 2176 | | |
| 2177 | | /* |
| 2178 | | * create_recursive_compset(+Ids,+Cond,+Type,+Infos,-RecId,-TCompSet) |
| 2179 | | * creates a recursive comprehension set: |
| 2180 | | * Ids is the list of the introduced typed identifiers |
| 2181 | | * Cond is the condition (a typed predicate) |
| 2182 | | * Infos are additional informations for the comprehension set syntax element |
| 2183 | | * RecId is the identifier (untyped, an atom) that can be used in Cond to refer to the |
| 2184 | | * comprehension set recursively. Usually RecId is used in Cond as a variable |
| 2185 | | * TCompSet is the generated recursive comprehension set, the recursion parameter is introduced |
| 2186 | | * by a recusive(Id,CompSet) syntax element |
| 2187 | | */ |
| 2188 | | create_recursive_compset(Ids,Cond,Type,Infos,RecId,TCompSet) :- |
| 2189 | | unique_id("recursive.",RecId), |
| 2190 | | add_symbolic_annotation(Infos,RInfos), |
| 2191 | | create_texpr(comprehension_set(Ids,Cond),Type,RInfos,TCompSet1), |
| 2192 | | create_typed_id(RecId,Type,TRecId), |
| 2193 | | create_texpr(recursive_let(TRecId,TCompSet1),Type,[],TCompSet). |
| 2194 | | |
| 2195 | | unique_typed_id(Prefix,Type,TId) :- |
| 2196 | | unique_id(Prefix,Id), |
| 2197 | | create_typed_id(Id,Type,TId). |
| 2198 | | |
| 2199 | | |
| 2200 | | mark_bexpr_as_symbolic(b(E,T,I),b(E2,T,RI)) :- |
| 2201 | | add_symbolic_annotation(I,RI), |
| 2202 | | mark_aux(E,E2). |
| 2203 | | mark_aux(union(A,B),R) :- !, R=union(SA,SB), |
| 2204 | | mark_bexpr_as_symbolic(A,SA), mark_bexpr_as_symbolic(B,SB). |
| 2205 | | % union is currently the only operator that is kept symbolically |
| 2206 | | mark_aux(A,A). |
| 2207 | | |
| 2208 | | add_symbolic_annotation([H|I],R) :- H == prob_annotation('SYMBOLIC'),!, R=[H|I]. |
| 2209 | | add_symbolic_annotation(I,R) :- !, R=[prob_annotation('SYMBOLIC')|I]. |
| 2210 | | |
| 2211 | | % identifier_sub_ast(+TExpr,+Identifier,-SubPosition): |
| 2212 | | % Find occurences of an identifier "Identifier" in an expression "TExpr" |
| 2213 | | % Returns a list of positions (beginning with 0) that describes the position of a sub-expression |
| 2214 | | % that contains all occurrences of Identifier in TExpr. |
| 2215 | | % E.g. [1,0,1] means "second sub-expression of TExpr, then the first sub-expression of that, |
| 2216 | | % then the second sub-expression of that". |
| 2217 | | % When an identifier has multiple occurences, the position of the sub-expression is returned |
| 2218 | | % where all occurences of it are located. |
| 2219 | | % If the identifier is not found, the call fails. |
| 2220 | | % Sub-expressions are meant like the ones syntaxtraversion or syntaxtransformation return. |
| 2221 | | identifier_sub_ast(TExpr,Identifier,SubPosition) :- |
| 2222 | | syntaxtraversion(TExpr,Expr,_Type,_Infos,AllSubs,Names), |
| 2223 | | identifier_sub_ast_aux(Expr,AllSubs,Names,Identifier,SubPosition). |
| 2224 | | identifier_sub_ast_aux(identifier(Identifier),[],[],Identifier,[]) :- !. |
| 2225 | | identifier_sub_ast_aux(_Expr,AllSubs,Names,Identifier,SubPosition) :- |
| 2226 | | get_texpr_id(TId,Identifier),nonmember(TId,Names), |
| 2227 | | % For each sub-expression E in the list AllSubs create a term Pos-E |
| 2228 | | % where Pos is E's position (starting with 0) in AllSubs |
| 2229 | | foldl(annotate_pos,AllSubs,AllAnnotatedSubs,0,_), |
| 2230 | | % Introduced identifiers occur alsa as sub-expressions, remove those |
| 2231 | | foldl(select_sub,Names,AllAnnotatedSubs,RealAnnSubs), |
| 2232 | | convlist(identifier_sub_ast_aux2(Identifier),RealAnnSubs,SubPositions), |
| 2233 | | ( SubPositions = [SubPosition] -> true |
| 2234 | | ; SubPositions = [_,_|_] -> % More then one occurrences - make this the found node |
| 2235 | | SubPosition = []). |
| 2236 | | identifier_sub_ast_aux2(Identifier,Pos-TExpr,[Pos|SubPosition]) :- |
| 2237 | | identifier_sub_ast(TExpr,Identifier,SubPosition). |
| 2238 | | annotate_pos(TExpr,I-TExpr,I,I2) :- I2 is I+1. |
| 2239 | | select_sub(Name,AnnotatedSubs,Result) :- |
| 2240 | | selectchk(_Pos-Name,AnnotatedSubs,Result). |
| 2241 | | |
| 2242 | | % exchange_ast_position(+SubPosition,+OldTExpr,-OldInner,+NewInner,-NewTExpr): |
| 2243 | | % exchanges a sub-expression in the expression "OldTExpr". |
| 2244 | | % SubPosition is a list of positions like identifier_sub_ast/3 returns it. |
| 2245 | | % OldInner is the sub-expression found in OldTExpr. |
| 2246 | | % NewInner is the new sub-expression. |
| 2247 | | % NewTExpr is the new expression that originates from replacing OldInner by NewInner. |
| 2248 | | exchange_ast_position([],Old,Old,New,New). |
| 2249 | | exchange_ast_position([Pos|RestPos],OldTExpr,OldInner,NewInner,NewTExpr) :- |
| 2250 | | remove_bt(OldTExpr,OldExpr,NewExpr,NewTExpr), |
| 2251 | | syntaxtransformation(OldExpr,Subs,_Names,NSubs,NewExpr), |
| 2252 | | nth0(Pos,Subs, OldSelected,Rest), |
| 2253 | | nth0(Pos,NSubs,NewSelected,Rest), |
| 2254 | | exchange_ast_position(RestPos,OldSelected,OldInner,NewInner,NewSelected). |
| 2255 | | |
| 2256 | | |
| 2257 | | % ----------------------- |
| 2258 | | |
| 2259 | | % a simple checker to see if an AST is well-formed: |
| 2260 | | % can be tested e.g. as follows: b_get_invariant_from_machine(I), check_ast(I). |
| 2261 | | |
| 2262 | | check_ast(TE) :- check_ast(false,TE). |
| 2263 | | check_ast(AllowVars,TExpr) :- %nl,print('CHECK AST'),nl, |
| 2264 | | map_over_typed_bexpr(check_ast_texpr(AllowVars),TExpr). |
| 2265 | | check_ast(_,_). |
| 2266 | | |
| 2267 | | :- use_module(typing_tools,[valid_ground_type/1]). |
| 2268 | | %check_ast_texpr(X) :- print(check(X)),nl,fail. |
| 2269 | | check_ast_texpr(AllowVars,b(E,Type,Infos)) :- |
| 2270 | | (check_expr(E,Type,Infos) -> true ; add_error(check_ast_texpr,'Invalid Expr: ', b(E,Type,Infos))), |
| 2271 | | (check_type(Type,AllowVars) -> true ; add_error(check_ast_texpr,'Invalid Type: ',b(E,Type,Infos))), |
| 2272 | | safe_functor(E,F), |
| 2273 | | (check_infos(Infos,F) -> true ; add_error(check_ast_texpr,'Invalid Infos: ',b(E,Type,Infos))), |
| 2274 | | fail. % to force backtracking in map_over_typed_bexpr |
| 2275 | | |
| 2276 | | safe_functor(V,R) :- var(V),!,R='$VAR'. |
| 2277 | | safe_functor(E,F/N) :- functor(E,F,N). |
| 2278 | | |
| 2279 | | check_type(X,AllowVars) :- var(X),!, |
| 2280 | | (AllowVars==true -> true ; add_error(check_type,'Variable type: ',X),fail). |
| 2281 | | check_type(pred,_) :- !. |
| 2282 | | check_type(subst,_) :- !. |
| 2283 | | check_type(op(Paras,Returns),AllowVars) :- !, |
| 2284 | | maplist(check_normal_type(AllowVars),Paras), |
| 2285 | | maplist(check_normal_type(AllowVars),Returns). |
| 2286 | | check_type(T,AllowVars) :- check_normal_type(AllowVars,T). |
| 2287 | | |
| 2288 | | check_normal_type(AllowVars,T) :- |
| 2289 | | (AllowVars \== true -> valid_ground_type(T) |
| 2290 | | ; ground(T) -> valid_ground_type(T) |
| 2291 | | ; true). % TO DO: call valid_ground_type but pass AllowVars |
| 2292 | | |
| 2293 | | |
| 2294 | | check_infos(X,F) :- var(X),!, add_error(check_infos,'Info field list not terminated: ',F:X),fail. |
| 2295 | | check_infos([],_). |
| 2296 | | check_infos([H|_],F) :- \+ ground(H),!, add_error(check_infos,'Info field not ground: ',F:H),fail. |
| 2297 | | check_infos([[H|T]|_],F) :- !, add_error(check_infos,'Info field contains nested list: ',F:[H|T]),fail. |
| 2298 | | check_infos([cse_used_ids(H)|T],F) :- member(cse_used_ids(H2),T),!, |
| 2299 | | add_error(check_infos,'Multiple cse_used_ids entry: ',F:[H,H2]),fail. |
| 2300 | | check_infos([used_ids(H)|T],F) :- member(used_ids(H2),T),!, |
| 2301 | | add_error(check_infos,'Multiple used_ids entry: ',F:[H,H2]),fail. |
| 2302 | | check_infos([_|T],F) :- check_infos(T,F). |
| 2303 | | |
| 2304 | | check_expr(Expr,Type,Infos) :- nonmember(contains_wd_condition,Infos), |
| 2305 | | sub_expression_contains_wd_condition(Expr,Sub), |
| 2306 | | TE = b(Expr,Type,Infos), |
| 2307 | | (Type = subst -> fail % AST cleanup is not called for substitutions; WD-info not available for substitutions at the moment |
| 2308 | | %translate:translate_substitution(TE,PS) |
| 2309 | | ; translate_bexpression(TE,PS)), |
| 2310 | | functor(Expr,Functor,_), |
| 2311 | | functor(Sub,SubFunctor,_), |
| 2312 | | tools:ajoin(['Node for AST node ',Functor,' does not contain WD info from Subexpression ',SubFunctor,' :'],Msg), |
| 2313 | | add_warning(check_expr,Msg,PS,TE). |
| 2314 | | check_expr(member(LHS,RHS),Type,Infos) :- is_just_type(RHS), |
| 2315 | | get_preference(optimize_ast,true), |
| 2316 | | !, |
| 2317 | | TE = b(member(LHS,RHS),Type,Infos), |
| 2318 | | translate:translate_bexpression(TE,PS), |
| 2319 | | add_warning(check_expr,'AST contains redundant typing predicate: ',PS,TE). |
| 2320 | | check_expr(identifier(ID),_,_) :- illegal_id(ID),!, |
| 2321 | | add_error(check_infos,'Illegal identifier: ', identifier(ID)). |
| 2322 | | check_expr(lazy_lookup_expr(ID),_,_) :- illegal_id(ID),!, |
| 2323 | | add_error(check_infos,'Illegal identifier: ', lazy_lookup_expr(ID)). |
| 2324 | | check_expr(lazy_lookup_pred(ID),_,_) :- illegal_id(ID),!, |
| 2325 | | add_error(check_infos,'Illegal identifier: ', lazy_lookup_pred(ID)). |
| 2326 | | check_expr(exists(Parameters,Condition),pred,Infos) :- !, |
| 2327 | | b_interpreter:get_exists_used_ids(Parameters,Condition,Infos,_Used). % this will do some checks |
| 2328 | | check_expr(_,_,_). |
| 2329 | | |
| 2330 | | illegal_id(ID) :- var(ID),!. |
| 2331 | | illegal_id(op(ID)) :- !, \+ atom(ID). |
| 2332 | | illegal_id(ID) :- \+ atom(ID). |
| 2333 | | |
| 2334 | | % ----------------------- |
| 2335 | | |
| 2336 | | |
| 2337 | | indent_ws(X) :- X<1,!. |
| 2338 | | indent_ws(X) :- print(' '), X1 is X-1, indent_ws(X1). |
| 2339 | | |
| 2340 | | print_ast_td(b(E,T,I),Level,L1) :- |
| 2341 | | indent_ws(Level), |
| 2342 | | (E=identifier(_) |
| 2343 | | -> format('~w (~w) -> ~w~n',[E,T,I]) |
| 2344 | | ; functor(E,F,N), |
| 2345 | | format('~w/~w (~w) -> ~w~n',[F,N,T,I]) |
| 2346 | | ), |
| 2347 | | L1 is Level+1. |
| 2348 | | print_ast(TExpr) :- |
| 2349 | | (map_over_type_bexpr_top_down_acc(print_ast_td,TExpr,0),fail ; true). |
| 2350 | | |
| 2351 | | % --------------------- |
| 2352 | | |
| 2353 | | :- dynamic count_id_usage/2. |
| 2354 | | single_usage_id_count(Expr) :- uses_an_identifier(Expr,Id), |
| 2355 | | retract(count_id_usage(Id,Count)), |
| 2356 | | !, |
| 2357 | | Count=0, |
| 2358 | | C1 is Count+1, |
| 2359 | | assert(count_id_usage(Id,C1)). |
| 2360 | | single_usage_id_count(_). |
| 2361 | | |
| 2362 | | % check if an identifier is used at most once |
| 2363 | | single_usage_identifier(ID,ExprOrPredicate,Count) :- |
| 2364 | | retractall(count_id_usage(_,_)), |
| 2365 | | assert(count_id_usage(ID,0)), |
| 2366 | | % TO DO: take care of naming; do not count occurences when we enter scope defining ID |
| 2367 | | map_over_full_bexpr_no_fail(single_usage_id_count,ExprOrPredicate), |
| 2368 | | retract(count_id_usage(ID,Count)). |
| 2369 | | |