| 1 | | % (c) 2009-2026 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, |
| 2 | | % Heinrich Heine Universitaet Duesseldorf |
| 3 | | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) |
| 4 | | |
| 5 | | |
| 6 | | :- module(b_compiler,[b_compile/6, b_optimize/6, b_optimize_closure/3]). |
| 7 | | |
| 8 | | :- use_module(library(lists)). |
| 9 | | |
| 10 | | :- use_module(self_check). |
| 11 | | :- use_module(bsyntaxtree). |
| 12 | | :- use_module(error_manager). |
| 13 | | :- use_module(debug,[debug_format/3]). |
| 14 | | :- use_module(btypechecker,[fasttype/2]). |
| 15 | | :- use_module(bmachine,[b_get_machine_operation_for_animation/6]). |
| 16 | | :- use_module(b_interpreter). |
| 17 | | :- use_module(custom_explicit_sets). |
| 18 | | :- use_module(kernel_waitflags,[add_error_wf/5, add_internal_error_wf/5]). |
| 19 | | %:- use_module(bmachine,[b_operation_reads_output_variables/3]). |
| 20 | | :- use_module(probsrc(performance_messages),[performance_monitoring_on/0,perfmessage/3]). |
| 21 | | |
| 22 | | :- use_module(module_information,[module_info/2]). |
| 23 | | :- module_info(group,interpreter). |
| 24 | | :- module_info(description,'This module compiles set comprehensions into closures; making them independent of the state of the B machine.'). |
| 25 | | |
| 26 | | /* compile boolean expression into a closure where the local state and the global |
| 27 | | state has been incorporated, but any parameter is left in the closure */ |
| 28 | | |
| 29 | | :- public test_bexpr/3, test_bexpr2/3. |
| 30 | | test_bexpr(Expr,[bind(cc,int(1)),bind(nn,int(2))], [bind(db,[(int(1),int(2))])]) :- |
| 31 | | fasttype( +conjunct( +conjunct( +member( global('Name')<<identifier(nn), +identifier('Name')), |
| 32 | | +member( global('Code')<<identifier(cc), +identifier('Code'))), |
| 33 | | +not_member( global('Name')<<identifier(nn), |
| 34 | | +domain(set(couple(global('Name'),global('Code')))<<identifier(db)))), Expr). |
| 35 | | |
| 36 | | test_bexpr2(Expr,[],[]) :- |
| 37 | | fasttype( +implication( +equal( set(couple(integer,any))<<identifier(ss), +empty_sequence), |
| 38 | | +equal( set(couple(integer,any))<<identifier(res), +empty_set)), Expr). |
| 39 | | |
| 40 | | |
| 41 | | |
| 42 | | b_optimize_closure(closure(P,T,Body),Res,WF) :- |
| 43 | | b_optimize(Body,P,[],[],CBody,WF),!, |
| 44 | | Res=closure(P,T,CBody). |
| 45 | | b_optimize_closure(C,C,_WF). |
| 46 | | |
| 47 | | |
| 48 | | % difference with b_compile: the states LS, S will not be thrown away by the interpreter |
| 49 | | % thus: we do not have to compile all accesses, in particular lazy lookups ! |
| 50 | | %b_optimize(TExpr,Parameters,_LS,_S,NTExpr,_WF) :- TExpr=b(_,_,Infos), member(already_optimized,Infos), |
| 51 | | % !, NTExpr=TExpr. |
| 52 | | b_optimize(TExpr,Parameters,LS,S,NTExpr,WF) :- %print('OPTIMIZE: '),translate:print_bexpr(TExpr),nl, trace, |
| 53 | | append(LS,[bind('$optimize_do_not_force_lazy_lookups',pred_true)],NewLS), |
| 54 | | b_compile(TExpr,Parameters,NewLS,S,NTExpr,WF). |
| 55 | | %bsyntaxtree:add_texpr_info_if_new(NTExpr,already_optimized,ResTExpr). |
| 56 | | |
| 57 | | b_compile(TExpr,Parameters,NewLS,S,NTExpr) :- |
| 58 | ? | b_compile(TExpr,Parameters,NewLS,S,NTExpr,no_wf_available). % for unit tests |
| 59 | | |
| 60 | | :- assert_must_succeed(( b_compiler:test_bexpr(E,L,S), |
| 61 | | b_compiler:b_compile(E,[nn],L,S,_R) )). |
| 62 | | :- assert_must_succeed(( b_compiler:test_bexpr2(E,L,S), |
| 63 | | b_compiler:b_compile(E,[ss,res],L,S,_R) )). |
| 64 | | :- assert_must_succeed(( b_compiler:b_compile(b(greater(b(value(int(2)),integer,[]), |
| 65 | | b(value(int(1)),integer,[])),pred,[]),[],[],[],Res), |
| 66 | | check_eq(Res,b(truth,pred,_)) )). |
| 67 | | :- assert_must_succeed(( b_compiler:b_compile(b(greater(b(value(int(2)),integer,[]), |
| 68 | | b(value(int(3)),integer,[])),pred,[]),[],[],[],Res), |
| 69 | | check_eq(Res,b(falsity,pred,_)) )). |
| 70 | | :- assert_must_succeed(( E = b(greater(b(value(int(2)),integer,[]), |
| 71 | | b(value(int(_)),integer,[])),pred,[]), |
| 72 | | b_compiler:b_compile(E,[],[],[],Res), |
| 73 | | check_eq(Res,E) )). |
| 74 | | :- assert_must_succeed(( E = b(greater(b(value(int(2)),integer,[]), |
| 75 | | b(value(_),integer,[])),pred,[]), |
| 76 | | b_compiler:b_compile(E,[],[],[],Res), |
| 77 | | check_eq(Res,E) )). |
| 78 | | :- assert_must_succeed(( E = b(greater(b(value(int(2)),integer,[]), |
| 79 | | b(identifier(x),integer,[])),pred,[]), |
| 80 | | b_compiler:b_compile(E,[],[bind(x,int(1))],[],Res), |
| 81 | | check_eq(Res,b(truth,pred,_)) )). |
| 82 | | :- assert_must_succeed(( E = b(greater(b(value(int(2)),integer,[]), |
| 83 | | b(identifier(x),integer,[])),pred,[]), |
| 84 | | b_compiler:b_compile(E,[],[bind(x,int(3))],[],Res), |
| 85 | | check_eq(Res,b(falsity,pred,_)) )). |
| 86 | | |
| 87 | | %:- assert_pre(b_compiler:b_compile_boolean_expression(E,Parameters,LS,S,_), |
| 88 | | % (type_check(E,boolean_expression),type_check(Parameters,list(variable_id)), |
| 89 | | % type_check(LS,store),type_check(S,store))). |
| 90 | | %:- assert_post(b_compiler:b_compile_boolean_expression(_,_,_,_,E), type_check(E,boolean_expression)). |
| 91 | | |
| 92 | | /* probably not worthwhile: |
| 93 | | b_compile(TExpr,Parameters,LS,S,NTExpr) :- get_texpr_info(TExpr,Info), |
| 94 | | (memberchk(compiled(Parameters),Info) -> NTExpr = TExpr ,print(already_compiled(Parameters)),nl, translate:print_bexpr(TExpr),nl |
| 95 | | ; b_compile0(TExpr,Parameters,LS,S,b(E,T,I)), translate:print(compiling(Parameters)),nl, translate:print_bexpr(TExpr),nl, |
| 96 | | NTExpr = b(E,T,[compiled(Parameters)|I])). |
| 97 | | */ |
| 98 | | :- use_module(closures,[get_recursive_identifier_of_closure_body/2]). |
| 99 | | b_compile(TExpr,Parameters,LS,S,NTExpr,WF) :- |
| 100 | | check_is_id_list(Parameters,Parameters0), |
| 101 | | (get_recursive_identifier_of_closure_body(TExpr,TRID), |
| 102 | | def_get_texpr_id(TRID,RID), nonmember(bind(RID,_),LS) |
| 103 | | -> Parameters1=[RID|Parameters0] % add recursive ID virtually to parameters to avoid error messages |
| 104 | | ; Parameters1=Parameters0), |
| 105 | | % print('compile : '),translate:print_bexpr(TExpr),nl, statistics(runtime,[Start,_]),%% |
| 106 | | sort(Parameters1,Parameters2), |
| 107 | ? | if(b_compile1(TExpr,Parameters2,LS,S,NTExpr0,eval,FullyKnown,WF), |
| 108 | | (FullyKnown=true |
| 109 | | -> copy_pos_infos(TExpr,NTExpr0,NTExpr) |
| 110 | | % ensure position info is not deleted if full expression compiled away, see PROB-412 (test 1677) |
| 111 | | ; NTExpr=NTExpr0), |
| 112 | | (add_internal_error_wf(b_compiler,'Compilation failed: ',TExpr,TExpr,WF), |
| 113 | | %b_compile1(TExpr,Parameters1,LS,S,NTExpr0,eval,_FullyKnown,WF), |
| 114 | | NTExpr = TExpr) |
| 115 | | ). |
| 116 | | %, bsyntaxtree:check_ast(NTExpr). |
| 117 | | %, check_infos(TExpr,NTExpr). |
| 118 | | %, print('compiled: '), translate:print_bexpr(NTExpr), print(' '),statistics(runtime,[Stop,_]), T is Stop-Start, print(T), print(' ms '),nl, bsyntaxtree:check_ast(NTExpr). % , print(NTExpr),nl. check_ast |
| 119 | | |
| 120 | | /* |
| 121 | | check_infos(Old,New) :- bsyntaxtree:get_texpr_info(Old,IO), |
| 122 | | bsyntaxtree:get_texpr_info(New,IN), |
| 123 | | member(X,IO), \+ member(X,IN), |
| 124 | | bsyntaxtree:important_info(X), |
| 125 | | print(check_infos(Old,New)),nl, |
| 126 | | print('Not copied: '), print(X),fail. |
| 127 | | check_infos(_,_). */ |
| 128 | | |
| 129 | | :- use_module(bsyntaxtree,[always_well_defined/1]). |
| 130 | | :- use_module(translate,[translate_bexpression_with_limit/2]). |
| 131 | | %:- use_module(hit_profiler,[add_profile_hit/1]). |
| 132 | | |
| 133 | | % Eval=eval means the expression will be needed in a successful branch and we can pre-compute more aggressively |
| 134 | | % Eval=false means the expression may not be needed (e.g., in a disjunction) and only perform efficient precomputations |
| 135 | | b_compile1(TExpr,Parameters,LS,S,ResultTExpr,Eval,FullyKnown1,WF) :- |
| 136 | | TExpr = b(Expr,Type,Infos), |
| 137 | | NTExpr = b(NewUntypedExpr,Type,NewInfos), |
| 138 | | %remove_bt(TExpr,Expr,NewUntypedExpr,NTExpr), % remove top-level Type Information |
| 139 | | %hit_profiler:add_profile_hit(Expr), |
| 140 | | %functor(Expr,E1,N1), %print(start_compile(E1/N1,Eval,FullyKnown1)),nl, |
| 141 | ? | b_compile1_infos(Expr,Type,Infos,Parameters,LS,S,NewUntypedExpr,NewInfos,Eval,FullyKnown,WF), |
| 142 | | %functor(NewUntypedExpr,E2,N2), |
| 143 | | %format(' compiled ~w/~w -> ~w/~w : ',[E1,N1,E2,N2]),translate:print_bexpr_or_subst(NTExpr),nl, |
| 144 | | %format(' fully=~w, eval=~w~n',[FullyKnown,Eval]), |
| 145 | | (NTExpr = b(value(_),_,_) |
| 146 | | -> FullyKnown1=FullyKnown, ResultTExpr=NTExpr |
| 147 | | ; evaluate_this(FullyKnown,Eval,NewUntypedExpr,Type,NewInfos) |
| 148 | | -> % print('eval : '),translate:print_bexpr(NTExpr),nl, % |
| 149 | | (nonvar(NewUntypedExpr), |
| 150 | | % if( would be more prudent !?, also: we used to call b_compute_expression_nowf |
| 151 | ? | b_interpreter:b_compute_expression(NTExpr,LS,S,ResultValue,WF) |
| 152 | | -> %print(result(ResultValue)),nl, |
| 153 | | %remove_bt(TExpr,Expr,value(ResultValue),ResultTExpr) |
| 154 | | get_texpr_type(TExpr,TT),ResultTExpr = b(value(ResultValue),TT,[]), |
| 155 | | FullyKnown1 = true |
| 156 | | %, print(compiled_value(ResultTExpr)),nl |
| 157 | | ; add_internal_error_wf(b_compiler,'Undefined value marked for evaluation:',NTExpr,Infos,WF), |
| 158 | | %trace, b_interpreter:b_compute_expression(NTExpr,LS,S,ResultValue,WF), |
| 159 | | ResultTExpr=NTExpr, FullyKnown1=false |
| 160 | | ) |
| 161 | | ; % ((FullyKnown=true, NTExpr\=b(value(_),_,_)) -> format('not eval: ~w (~w)~n',[NTExpr,Eval]) ; true), |
| 162 | | ResultTExpr=NTExpr, FullyKnown1=false |
| 163 | | ). |
| 164 | | |
| 165 | | |
| 166 | | :- use_module(library(ordsets),[ord_member/2, ord_union/3]). |
| 167 | | :- use_module(bsyntaxtree,[create_exists_or_let_predicate/3]). |
| 168 | | :- use_module(tools_lists,[delete_first/3]). |
| 169 | | add_parameters(SortedIds,NewIds,NewSortedIds) :- |
| 170 | | sort(NewIds,SNew), |
| 171 | | ord_union(SortedIds,SNew,NewSortedIds). |
| 172 | | |
| 173 | | b_compile1_infos(exists(ExistsPara,Pred),_,OldInfos,Parameters,LS,S,NExpr,NewInfos,Eval,FullyKnown,WF) :- !, |
| 174 | | FullyKnown=false, % predicates never automatically evaluated in b_compile1 |
| 175 | | get_texpr_ids(ExistsPara,AtomicIds), |
| 176 | | add_parameters(Parameters,AtomicIds,NParameters), |
| 177 | ? | b_compile1(Pred,NParameters,LS,S,NPred,Eval,_FullyKnown1,WF), |
| 178 | | (is_falsity(NPred) -> NExpr = falsity, NewInfos = OldInfos |
| 179 | | ; is_truth(NPred) -> NExpr = truth, NewInfos = OldInfos |
| 180 | | %; Pred==NPred, write(unchanged(Parameters)),nl, member(used_ids(Old),OldInfos), print(used(Old)),nl,nl,fail |
| 181 | | ; create_exists_or_let_predicate(ExistsPara,NPred,b(NExpr,pred,NI)), |
| 182 | | %print('COMPILED EXISTS: '), translate:print_bexpr(b(NExpr,pred,NI)),nl, |
| 183 | | (delete_first(OldInfos,used_ids(_),I1), |
| 184 | ? | member(used_ids(NewUsedIds),NI) -> NewInfos = [used_ids(NewUsedIds)|I1] |
| 185 | | ; %nl,print(missing_used_ids(OldInfos,NI)),nl, % can happen when we construt a let_predicate above |
| 186 | | update_infos(NExpr,OldInfos,Parameters,NewInfos)) |
| 187 | | ). |
| 188 | | b_compile1_infos(identifier(Id),Type,OldInfos,Parameters,LS,S,NExpr,NewInfos,_Eval,FullyKnown,WF) :- !, |
| 189 | | ( ord_member(Id,Parameters) -> |
| 190 | | NExpr = identifier(Id), FullyKnown=false, NewInfos = OldInfos |
| 191 | | ; Id=op(_) -> |
| 192 | | NExpr = identifier(Id), FullyKnown=false, NewInfos = OldInfos |
| 193 | | ; b_interpreter:lookup_value_in_store_and_global_sets_wf(Id,Type,LS,S,Value,OldInfos,WF) -> |
| 194 | | NExpr = value(Value), (known_value(Value) -> FullyKnown=true ; FullyKnown=false), |
| 195 | | NewInfos = [was_identifier(Id)|OldInfos] |
| 196 | | ; add_internal_error_wf(b_compiler,'Compilation of identifier failed: ',Id,OldInfos,WF), |
| 197 | | NExpr = identifier(Id), FullyKnown=false, NewInfos = OldInfos |
| 198 | | ). |
| 199 | | b_compile1_infos(Expr,_,OldInfos,_Parameters,_LS,_S,NewUntypedExpr,NewInfos,_Eval,FullyKnown,_WF) :- |
| 200 | ? | b_ast_cleanup:is_integer_set(Expr,_Set),!, |
| 201 | | NewUntypedExpr=Expr, NewInfos=OldInfos,FullyKnown=true. |
| 202 | | b_compile1_infos(operation_call_in_expr(Operation,OpCallParas),_Type,OldInfos,Parameters,LS,S, |
| 203 | | Compiled,NewInfos,Eval,FullyKnown,WF) :- !, |
| 204 | | def_get_texpr_id(Operation,op(OperationName)), |
| 205 | | FullyKnown = false, |
| 206 | | b_compile_l(OpCallParas,Parameters,LS,S,OpCallParaValues,Eval,_,WF), |
| 207 | | (b_get_operation_normalized_read_write_info(OperationName,ReadVars,Modified) -> true |
| 208 | | ; member(reads(ReadVars),OldInfos), member(modifies(Modified),OldInfos) |
| 209 | | -> add_message(b_compiler,'Unregistered operation in expression: ',OperationName) |
| 210 | | % should not happen; but proceed with the locally stored reads/writes info |
| 211 | | ; add_error_wf(b_compiler,'Cannot obtain read/write info for operation:',OperationName,OldInfos,WF), |
| 212 | | write(OldInfos),nl,nl, |
| 213 | | ReadVars=[], Modified=[] |
| 214 | | ), |
| 215 | | %exclude(operation_identifier,Read,ReadVars), % Read used to contain operations used via operation_call_in_expr; TO DO: check if this is ok in other places of source code of ProB; see test 1957 |
| 216 | | (Modified=[] -> true |
| 217 | | ; add_error_wf(b_compiler,'Calling operation that modifies state in expression:',OperationName,OldInfos,WF)), |
| 218 | | % print(compile_call_op(OperationName,ReadVars,Modified,OpCallParaValues)),nl, |
| 219 | | (ReadVars=[] |
| 220 | | -> Compiled = operation_call_in_expr(Operation,OpCallParaValues), |
| 221 | | NewInfos = OldInfos |
| 222 | | ; maplist(create_value_for_read_variable(LS,S,WF),ReadVars,TRead,TValues), |
| 223 | | safe_create_texpr(let_expression_global(TRead,TValues, |
| 224 | | b(operation_call_in_expr(Operation,OpCallParaValues),any,OldInfos)),any,[generated_by_b_compiler],New), |
| 225 | | New = b(Compiled,_,NewInfos) |
| 226 | | %NewInfos = [generated_by_b_compiler], |
| 227 | | %Compiled = let_expression_global(TRead,TValues, |
| 228 | | % b(operation_call_in_expr(Operation,OpCallParaValues),any,OldInfos)) |
| 229 | | ). |
| 230 | | b_compile1_infos(kodkod(Id,Identifiers),_,OldInfos,Parameters,LS,S,NExpr,NewInfos,_Eval,FullyKnown,WF) :- !, |
| 231 | | FullyKnown=false, NewInfos=OldInfos, |
| 232 | | exclude(is_parameter(Parameters),Identifiers,IdsToCompile), |
| 233 | | (IdsToCompile=[] |
| 234 | | -> NExpr = kodkod(Id,Identifiers) |
| 235 | | ; maplist(precompile_id(LS,S,WF),IdsToCompile,Values), |
| 236 | | % as we cannot inspect kodkod problem: wrap it into a let with the values stored: |
| 237 | | NExpr = let_predicate(IdsToCompile,Values,b(kodkod(Id,Identifiers),pred,OldInfos)) |
| 238 | | ). |
| 239 | | b_compile1_infos(Expr,_,OldInfos,Parameters,LS,S,NewUntypedExpr,NewInfos,Eval,FullyKnown,WF) :- |
| 240 | ? | b_compile2(Expr,Parameters,LS,S,NewUntypedExpr,Eval,FullyKnown,WF), |
| 241 | | update_infos(NewUntypedExpr,OldInfos,Parameters,NewInfos). |
| 242 | | |
| 243 | | |
| 244 | | is_parameter(Parameters,b(identifier(Id),_,_)) :- ord_member(Id,Parameters). |
| 245 | | |
| 246 | | precompile_id(LS,S,WF,b(identifier(Id),Type,Info),b(value(Value),Type,[])) :- |
| 247 | | b_interpreter:lookup_value_in_store_and_global_sets_wf(Id,Type,LS,S,Value,Info,WF). |
| 248 | | % was_identifier is aded in b_compile1_infos |
| 249 | | |
| 250 | | :- use_module(bmachine,[b_get_operation_normalized_read_write_info/3]). |
| 251 | | |
| 252 | | %operation_identifier(op(_)). |
| 253 | | create_value_for_read_variable(LS,S,WF,Variable,TVariable,TValue) :- |
| 254 | | b_interpreter:lookup_value_in_store_and_global_sets_wf(Variable,_Type,LS,S,Value,unknown,WF),!, |
| 255 | | % TO DO: try and find type? |
| 256 | | TVariable = b(identifier(Variable),any,[]), |
| 257 | | TValue = b(value(Value),any,[]). |
| 258 | | create_value_for_read_variable(_LS,_S,WF,Variable,TVariable,b(value(term(undefined)),any,[])) :- |
| 259 | | TVariable = b(identifier(Variable),any,[]), |
| 260 | | add_internal_error_wf(b_compiler,'Cannot find variable (read) while compiling operation:',Variable,unknown,WF), |
| 261 | | fail. |
| 262 | | |
| 263 | | :- use_module(library(ordsets)). |
| 264 | | update_infos(forall(EParas,LHS,RHS),Infos,Parameters,NewInfos) :- |
| 265 | | % forall also has used_ids field as it may call exists in negative context |
| 266 | | conjunct_predicates([LHS,RHS],Cond), |
| 267 | | update_infos_aux(EParas,Cond,Infos,Parameters,NewInfos),!. |
| 268 | | update_infos(exists(EParas,Cond),Infos,Parameters,NewInfos) :- % we create_exists_or_let_predicate above, but other transformations may generate an exists below: |
| 269 | | update_infos_aux(EParas,Cond,Infos,Parameters,NewInfos),!. |
| 270 | | update_infos(BOP,Infos,_,NewInfos) :- bsyntaxtree:syntaxelement(BOP, [A,B],[], [], [], _), |
| 271 | | wd_and_efficient(BOP), % should not generate WD errors itself |
| 272 | ? | (select(contains_wd_condition,Infos,NewInfos) % there is a WD condition attached |
| 273 | | -> fast_check_wd(A), |
| 274 | | fast_check_wd(B) |
| 275 | | ), |
| 276 | | %print(removing_wd_condition(BOP)),nl, |
| 277 | | !. |
| 278 | | update_infos(_,I,_,I). |
| 279 | | |
| 280 | | update_infos_aux(EParas,Cond,Infos,Parameters,NewInfos) :- |
| 281 | | select_used_ids(UsedIds,Infos,I1,EParas,Cond), |
| 282 | | UsedIds \= [],!, |
| 283 | | % remove those used identifiers which will be compiled into the predicate |
| 284 | | sort(Parameters,SParas), |
| 285 | | ord_intersection(UsedIds,SParas,NewUsedIds), |
| 286 | | %print(update(Parameters,UsedIds,I1,new(NewUsedIds))),nl, |
| 287 | | NewInfos = [used_ids(NewUsedIds)|I1]. |
| 288 | | |
| 289 | | :- use_module(bsyntaxtree,[find_identifier_uses/3]). |
| 290 | ? | select_used_ids(UsedIds,Infos,I1,_,_) :- select(used_ids(UsedIds),Infos,I1),!. |
| 291 | | % check_used_ids_info(Parameters,Condition,UsedIds,b_compiler) |
| 292 | | select_used_ids(UsedIds,Infos,Infos,_Parameters,Condition) :- |
| 293 | | %add_error(bcompiler,'Expected information of used identifiers in exists operation information : ',Parameters:Infos), %% missing info can happen due to simplifcation rules below ! |
| 294 | | find_identifier_uses(Condition, [], UsedIds). % ,print(used(UsedIds,in_exist(Parameters))),nl. |
| 295 | | % TO DO: avoid re-computing used-ids; we should refactor b_compile2 to return new Info field |
| 296 | | |
| 297 | | |
| 298 | | evaluate_this(true,Eval,NewUntypedExpr,Type,NewInfos) :- !, |
| 299 | | evaluate_this_if_fully_known(Eval,NewUntypedExpr,Type,NewInfos). |
| 300 | | evaluate_this(_FullyKnown,_,NewUntypedExpr,_,_) :- |
| 301 | | eval_even_if_not_fully_known(NewUntypedExpr). |
| 302 | | |
| 303 | | eval_even_if_not_fully_known(comprehension_set(A,B)) :- |
| 304 | | (is_falsity(B) -> true ; b_ast_cleanup:is_integer_set(comprehension_set(A,B),_)). |
| 305 | | % TODO: detect intervals? |
| 306 | | eval_even_if_not_fully_known(general_product(_A,B,_C)) :- is_falsity(B). |
| 307 | | eval_even_if_not_fully_known(general_sum(_A,B,_C)) :- is_falsity(B). |
| 308 | | |
| 309 | | evaluate_this_if_fully_known(eval,X,Type,Info) :- !, worth_it_type(Type,X,Info). |
| 310 | | evaluate_this_if_fully_known(_,function(A,B),Type,Info) :- !, |
| 311 | | A=b(value(VA),_,_), nonvar(VA), VA=avl_set(_), |
| 312 | | B=b(value(_),_,_), |
| 313 | | worth_it_type(Type,function(A,B),Info). % will check well-definedness |
| 314 | | evaluate_this_if_fully_known(_,X,_Type,_Info) :- wd_and_efficient(X). |
| 315 | | |
| 316 | | |
| 317 | | % things which are very quick to compute |
| 318 | | wd_and_efficient(sequence_extension(_)) :- !. |
| 319 | | wd_and_efficient(set_extension(_)) :- !. |
| 320 | | wd_and_efficient(integer_set(_)) :- !. % will be converted into value(global_set(_)) |
| 321 | | %% wd_and_efficient(value(_)) :- !. % is already computed |
| 322 | | % the following will reduce the size of the representation; usually a good thing; |
| 323 | | % we assume only avl_sets apprear here; inner set comprehensions are never computed into symbolic form by b_compile (see known_value below): |
| 324 | | %wd_and_efficient(identity(_)) :- !. |
| 325 | | wd_and_efficient(range(_)) :- !. |
| 326 | | wd_and_efficient(domain(_)) :- !. |
| 327 | | wd_and_efficient(domain_restriction(_,_)) :- !. |
| 328 | | wd_and_efficient(domain_subtraction(_,_)) :- !. |
| 329 | | wd_and_efficient(range_restriction(_,_)) :- !. |
| 330 | | wd_and_efficient(range_subtraction(_,_)) :- !. |
| 331 | | wd_and_efficient(intersection(_,_)) :- !. |
| 332 | | wd_and_efficient(set_subtraction(_,_)) :- !. |
| 333 | | wd_and_efficient(image(_,_)) :- !. |
| 334 | | wd_and_efficient(reverse(_)) :- !. % added for rgen_rgen_Worst_Case_Stopping_distance_NCT_trm13 |
| 335 | | % reverse has n.log(n) complexity, but is always wd and can be beneficial |
| 336 | | wd_and_efficient(union(A,B)) :- finite_set(A), finite_set(B), !. % has complexity n |
| 337 | | % usually the union of two avl_sets will be smaller than keeping them separate, what about intervals? |
| 338 | | wd_and_efficient(interval(_,_)) :- !. % ditto |
| 339 | | wd_and_efficient(card(S)) :- !, % added for rgen_rgen_Worst_Case_Stopping_distance_NCT_trm13 |
| 340 | | (finite_set(S) -> true % is wd for finite set; has currently linear complexity but reduces size of closure |
| 341 | | ; is_interval(S) -> true). % card is simple to compute |
| 342 | | wd_and_efficient(min(S)) :- !, % logarithmic for avl_set, see test 1338 |
| 343 | | finite_non_empty_set(S). |
| 344 | | wd_and_efficient(max(S)) :- !, % logarithmic for avl_set |
| 345 | | finite_non_empty_set(S). |
| 346 | | wd_and_efficient(string_set) :- !. |
| 347 | | % some other efficient operators: |
| 348 | | % external_function_call CHOOSE (test 1338) ? |
| 349 | | % first, last, ... need to ensure we have sequence |
| 350 | | wd_and_efficient(X) :- worth_it_int(X),!. |
| 351 | | wd_and_efficient(X) :- worth_it_other(X). |
| 352 | | |
| 353 | | is_interval(b(value(V),set(_),_)) :- nonvar(V), V=closure(P,T,B), |
| 354 | | is_fixed_interval(P,T,B,_,_). |
| 355 | | |
| 356 | | finite_set(b(value(V),ST,_)) :- is_set_type(ST,_), nonvar(V), finite_set_aux(V). |
| 357 | | finite_set_aux([]). |
| 358 | | finite_set_aux(avl_set(_)). |
| 359 | | finite_non_empty_set(b(value(V),ST,_)) :- is_set_type(ST,_), nonvar(V), V=avl_set(_). |
| 360 | | |
| 361 | | fast_check_wd(b(E,_,Infos)) :- |
| 362 | | (nonmember(contains_wd_condition,Infos) -> true |
| 363 | | ; nonvar(E), E=value(_)). |
| 364 | | |
| 365 | | check_wd(NTExpr) :- bsyntaxtree:always_well_defined(NTExpr). % ,print(wd(NTExpr)),nl. |
| 366 | | %(bsyntaxtree:always_well_defined(NTExpr) -> true ; print(not_guaranteed_wd(NTExpr)),nl). |
| 367 | | |
| 368 | | % (worth_it_type(Type,X,Info) -> true ; X=value(_) -> true ; print(not_evaluating(X)),nl,fail). |
| 369 | | worth_it_type(integer,X,Info) :- worth_it_int_wd(X),!, check_wd(b(X,integer,Info)). |
| 370 | | worth_it_type(T,function(A,B),Info) :- !, |
| 371 | | (check_wd(b(function(A,B),T,Info)) -> true |
| 372 | | ; fail). %print('not_precompiling_function '),translate:print_bexpr(A), print(' @ '), translate:print_bexpr(B),nl,fail). |
| 373 | | worth_it_type(integer,X,_) :- worth_it_int(X),!. |
| 374 | | worth_it_type(T,X,Info) :- worth_it_wd(X),!, check_wd(b(X,T,Info)). |
| 375 | | worth_it_type(set(_),X,_) :- worth_it_set(X),!. |
| 376 | | worth_it_type(seq(_),X,_) :- worth_it_set(X),!. |
| 377 | | worth_it_type(_,X,_) :- worth_it_other(X). |
| 378 | | |
| 379 | | % TO DO: we should use the predicate has_wd_condition from b_ast_cleanup |
| 380 | | |
| 381 | | % integer operations that could generate WD-errors |
| 382 | | worth_it_int_wd(div(_,_)). |
| 383 | | worth_it_int_wd(max(_)). |
| 384 | | worth_it_int_wd(min(_)). |
| 385 | | worth_it_int_wd(mod(_,_)). |
| 386 | | worth_it_int_wd(power_of(_,_)). |
| 387 | | worth_it_int_wd(card(_)). % has WD condition !! |
| 388 | | worth_it_int_wd(size(_)). |
| 389 | | |
| 390 | | % other operations that could generate WD-errors |
| 391 | | worth_it_wd(first(_)). |
| 392 | | worth_it_wd(last(_)). |
| 393 | | worth_it_wd(tail(_)). |
| 394 | | worth_it_wd(front(_)). |
| 395 | | worth_it_wd(restrict_front(_,_)). |
| 396 | | worth_it_wd(restrict_tail(_,_)). |
| 397 | | worth_it_wd(rel_iterate(_,_)). %% could be expensive |
| 398 | | worth_it_wd(general_intersection(_)). |
| 399 | | worth_it_wd(general_concat(_)). |
| 400 | | worth_it_wd(insert_front(_,_)). |
| 401 | | worth_it_wd(insert_tail(_,_)). |
| 402 | | |
| 403 | | % to do: check other operators that could be not well-defined ! |
| 404 | | |
| 405 | | worth_it_int(unary_minus(_)). |
| 406 | | worth_it_int(add(_,_)). |
| 407 | | worth_it_int(minus(_,_)). |
| 408 | | worth_it_int(multiplication(_,_)). |
| 409 | | worth_it_int(max_int). |
| 410 | | worth_it_int(min_int). |
| 411 | | |
| 412 | | %worth_it_set(empty_set). % treated below |
| 413 | | %worth_it_set(empty_sequence). % treated below |
| 414 | | %worth_it_set(closure(_)). % this is closure1; it is currently always kept symbolic and can be counterproductive to compile; e.g., card(closure1(%x.(x : 1 .. 200|x + 1))) |
| 415 | | %% ?? need to be more careful here; can be expensive --> need to keep track which parts need definitely to be evaluated |
| 416 | | worth_it_set(integer_set(_)). % will be converted into value(global_set(_)) |
| 417 | | %worth_it_set(comprehension_set(A,B)) :- % due to predicate B this will never be fully known |
| 418 | | % (is_falsity(B) -> true ; b_ast_cleanup:is_integer_set(comprehension_set(A,B),_)). |
| 419 | | worth_it_set(interval(_,_)). |
| 420 | | worth_it_set(reflexive_closure(A)) :- \+ symbolic_value(A). |
| 421 | | worth_it_set(reverse(_)). % function inverse |
| 422 | | worth_it_set(domain(_)). worth_it_set(range(_)). |
| 423 | | worth_it_set(union(_,_)). worth_it_set(intersection(_,_)). worth_it_set(set_subtraction(_,_)). |
| 424 | | worth_it_set(image(_,B)) :- \+ symbolic_value(B). |
| 425 | | worth_it_set(composition(_,_)). |
| 426 | | worth_it_set(domain_restriction(_,_)). worth_it_set(domain_subtraction(_,_)). |
| 427 | | worth_it_set(range_restriction(_,_)). worth_it_set(range_subtraction(_,_)). |
| 428 | | worth_it_set(direct_product(A,B)) :- \+ symbolic_value(A), \+ symbolic_value(B). |
| 429 | | worth_it_set(parallel_product(A,B)) :- \+ symbolic_value(A), \+ symbolic_value(B). |
| 430 | | worth_it_set(iteration(_,_)). |
| 431 | | worth_it_set(set_extension([H|_])) :- \+ symbolic_value(H). % otherwise we may get an enumeration warning |
| 432 | | worth_it_set(sequence_extension([H|_])) :- \+ symbolic_value(H). % ditto, TODO: check tail unless expensive |
| 433 | | worth_it_set(rev(_)). % reverse of sequence, in principle has wd condition |
| 434 | | worth_it_set(concat(_,_)). % ditto: requires args to be a sequence |
| 435 | | worth_it_set(seq(_)). % will be kept symbolic anyway |
| 436 | | worth_it_set(seq1(_)). % will be kept symbolic anyway; relevant for test 1731 |
| 437 | | % f=%x.(x:iseq(struct(a:seq1(NATURAL),b:BOOL))|x) & f([rec(a:[222],b:TRUE)])=[rec(a:[222],b:xx)] & xx=TRUE |
| 438 | | % however: value can be put into a set-extension! |
| 439 | | worth_it_set(iseq(_)). % will be kept symbolic anyway |
| 440 | | worth_it_set(iseq1(_)). % will be kept symbolic anyway |
| 441 | | worth_it_set(perm(_)). % will be kept symbolic anyway |
| 442 | | worth_it_set(pow_subset(_)). % will be kept symbolic anyway |
| 443 | | worth_it_set(pow1_subset(_)). % will be kept symbolic anyway |
| 444 | | worth_it_set(fin_subset(_)). % will be kept symbolic anyway |
| 445 | | worth_it_set(fin1_subset(_)). % will be kept symbolic anyway |
| 446 | | worth_it_set(general_union(X)) :- \+ symbolic_value(X). % otherwise we can get enumeration warnings |
| 447 | | worth_it_set(identity(_)). |
| 448 | | worth_it_set(first_of_pair(_)). % can also produce set |
| 449 | | worth_it_set(second_of_pair(_)). % can also produce set |
| 450 | | worth_it_set(cartesian_product(_,_)). % will usually be kept symbolic |
| 451 | | worth_it_set(string_set). % ensure we have values inside compiled closures, e.g., for custom_explicit_set card computations |
| 452 | | worth_it_set(bool_set). |
| 453 | | |
| 454 | | symbolic_value(b(value(Val),_,_)) :- nonvar(Val), symbolic_val_aux(Val). |
| 455 | | symbolic_val_aux(closure(P,T,B)) :- \+ is_fixed_interval(P,T,B,_,_). |
| 456 | | symbolic_val_aux(global_set(_)). |
| 457 | | |
| 458 | | :- use_module(external_functions,[not_declarative/1,external_fun_has_wd_condition/1, |
| 459 | | expects_unevaluated_args/1]). |
| 460 | | worth_it_other(boolean_true). |
| 461 | | worth_it_other(boolean_false). |
| 462 | | worth_it_other(real(_)). |
| 463 | | worth_it_other(string(_)). |
| 464 | | worth_it_other(first_of_pair(_)). |
| 465 | | worth_it_other(second_of_pair(_)). |
| 466 | | worth_it_other(couple(_,_)). |
| 467 | | worth_it_other(record_field(_,_)). |
| 468 | | worth_it_other(external_function_call(FunName,_)) :- |
| 469 | | \+ not_declarative(FunName), |
| 470 | | \+ external_fun_has_wd_condition(FunName). %print(compile(FunName)),nl. |
| 471 | | % CHOOSE for finite_non_empty_set ? |
| 472 | | worth_it_other(rec(_)). |
| 473 | | worth_it_other(struct(_)). |
| 474 | | %worth_it_other(value(_)). % does not have to be evaluted; already a value |
| 475 | | |
| 476 | | /* |
| 477 | | % To do: distinguish which parts definitely need to be evaluated |
| 478 | | %dont_eval_subexpressions(member). % special membership code can be used |
| 479 | | %dont_eval_subexpressions(not_member). % special membership code can be used |
| 480 | | dont_eval_subexpressions(disjunct(_,_)). % it may not be necessary to eval RHS |
| 481 | | dont_eval_subexpressions(implication(_,_)). % it may not be necessary to eval RHS |
| 482 | | */ |
| 483 | | |
| 484 | | :- use_module(bsyntaxtree, [get_negated_operator_expr/2]). |
| 485 | | :- use_module(kernel_objects,[equal_object/3]). |
| 486 | | :- use_module(kernel_mappings,[binary_boolean_operator/3]). |
| 487 | | :- use_module(kernel_tools,[filter_cannot_match/4, get_template_for_filter_cannot_match/2]). |
| 488 | | b_compile2(Exp,_Parameters,_LS,_S,NExpr,_Eval,FullyKnown,WF) :- var(Exp), !, |
| 489 | | add_internal_error_wf(b_compiler,'Variable Expression: ',Exp,unknown,WF), |
| 490 | | NExpr=Exp, FullyKnown=false. |
| 491 | | b_compile2(truth,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=truth, FullyKnown=false. % predicates never fully known |
| 492 | | b_compile2(falsity,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=falsity, FullyKnown=false. % predicates never fully known |
| 493 | | b_compile2(empty_set,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=value([]), FullyKnown=true. |
| 494 | | b_compile2(empty_sequence,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=value([]), FullyKnown=true. |
| 495 | | b_compile2(boolean_false,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=value(pred_false), FullyKnown=true. |
| 496 | | b_compile2(boolean_true,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=value(pred_true), FullyKnown=true. |
| 497 | | b_compile2(value(Val),_Parameters,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, |
| 498 | | NExpr=value(Val), |
| 499 | | (known_value(Val) -> % ground(Val) -> known_value ? |
| 500 | | FullyKnown=true ; FullyKnown=false). |
| 501 | | b_compile2(integer(Val),_Parameters,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, |
| 502 | | NExpr=value(int(Val)), (number(Val) -> FullyKnown=true ; FullyKnown=false). |
| 503 | | b_compile2(lazy_lookup_pred(Id),Parameters,LS,S,NExpr,_Eval,FullyKnown,WF) :- !, |
| 504 | | ( ord_member(Id,Parameters) -> %print(lazy_lookup_pred_id_as_parameter(Id,Parameters)),nl, |
| 505 | | NExpr = lazy_lookup_pred(Id), FullyKnown=false |
| 506 | | ; compute_lazy_lookup(Id,lazy_lookup_pred(Id),LS,S,NExpr,FullyKnown,WF) |
| 507 | | ). |
| 508 | | b_compile2(lazy_lookup_expr(Id),Parameters,LS,S,NExpr,_Eval,FullyKnown,WF) :- !, |
| 509 | | ( ord_member(Id,Parameters) -> %print(lazy_lookup_expr_id_as_parameter(Id,Parameters)),nl, |
| 510 | | NExpr = lazy_lookup_expr(Id), FullyKnown=false |
| 511 | | ; compute_lazy_lookup(Id,lazy_lookup_expr(Id),LS,S,NExpr,FullyKnown,WF) |
| 512 | | ). |
| 513 | | |
| 514 | | % treat a few common cases, more efficiently than syntaxtransformation |
| 515 | | b_compile2(equal(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, |
| 516 | | FullyKnown=false, % predicates never evaluated in b_compile1 |
| 517 | ? | b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF), |
| 518 | ? | b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF), |
| 519 | | ( FullyKnownA=true, FullyKnownB=true, |
| 520 | | NExprA = b(value(VA),_,_), NExprB = b(value(VB),_,_) |
| 521 | | -> (equal_object(VA,VB,b_compile2_1) -> NExpr = truth ; NExpr = falsity) |
| 522 | | ; generate_equality(NExprA,NExprB,NExpr) |
| 523 | | ). |
| 524 | | b_compile2(not_equal(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, |
| 525 | | FullyKnown=false, % predicates never evaluated in b_compile1 |
| 526 | | b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF), |
| 527 | | b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF), |
| 528 | | ( FullyKnownA=true, FullyKnownB=true, |
| 529 | | NExprA = b(value(VA),_,_), NExprB = b(value(VB),_,_) |
| 530 | | -> %print(computing_neq(VA,VB)),nl, |
| 531 | | (kernel_objects:equal_object(VA,VB,b_compile2_2) -> NExpr = falsity ; NExpr = truth) |
| 532 | | %, print(result(NExpr)),nl |
| 533 | | ; NExpr = not_equal(NExprA,NExprB) |
| 534 | | ). |
| 535 | | b_compile2(member(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, |
| 536 | | FullyKnown=false, % predicates never evaluated in b_compile1 |
| 537 | ? | b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF), |
| 538 | | (NExprB = b(value(X),BT,BI) |
| 539 | | -> (X==[], always_well_defined(A) -> NExpr = falsity |
| 540 | ? | ; b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF), |
| 541 | | % check if we can decide membership (e.g., 1:{1}) |
| 542 | ? | (quick_test_membership1(NExprA,X,PRes) |
| 543 | | -> convert_pred_res(PRes,NExpr) |
| 544 | | % TO DO: maybe optimize x: {y|P(y)} --> P(x) ; by commenting in code below |
| 545 | | % However, ensure test 273 succeeds and closure equality correctly detected (e.g., for BV16 = {bt|bt : BIT_VECTOR & bv_size(bt) = 16}) |
| 546 | | % ; (get_texpr_id(NExprA,IDA), |
| 547 | | % get_comprehension_set(NExprB,IDB,Pred), get_texpr_info(NExprB,Info), |
| 548 | | % print(rename(IDB,IDA,Info)),nl, |
| 549 | | % bsyntaxtree:rename_bt(Pred,[rename(IDB,IDA)],PredA)) -> get_texpr_expr(PredA,NExpr) |
| 550 | | ; custom_explicit_sets:singleton_set(X,El) % replace x:{El} -> x=El |
| 551 | | -> get_texpr_type(NExprA,TA), |
| 552 | | generate_equality_with_value(NExprA,FullyKnownA,El,FullyKnownB,TA,NExpr) |
| 553 | | ; get_template_for_filter_cannot_match(NExprA,VA) |
| 554 | | -> filter_cannot_match(X,VA,NewX,Filtered), |
| 555 | | % (Filtered=false -> true ; print(filtered(NewX,VA,X)),nl), |
| 556 | | (Filtered=false -> NExpr = member(NExprA,NExprB) |
| 557 | | ; (NewX==[], always_well_defined(A)) -> NExpr = falsity |
| 558 | | ; custom_explicit_sets:singleton_set(NewX,El) |
| 559 | | -> get_texpr_type(NExprA,TA), |
| 560 | | %nl,print(create_equal(NExprA,FullyKnownA,El,FullyKnownB,NExprB)),nl,nl, |
| 561 | | generate_equality_with_value(NExprA,FullyKnownA,El,FullyKnownB,TA,NExpr) |
| 562 | | ; NExpr = member(NExprA, b(value(NewX),BT,BI)) |
| 563 | | ) |
| 564 | | % end fo filtering |
| 565 | | ; NExpr = member(NExprA,NExprB) |
| 566 | | ) |
| 567 | | % , print('compile: '),print(NExpr),nl |
| 568 | | ) |
| 569 | | ; NExpr = member(NExprA,NExprB), |
| 570 | | b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF) |
| 571 | | ). |
| 572 | | % TO DO: also optimize things like: (ev1 |-> 0) |-> eg : #221:{((1|->0)|->3),((2|->0)|->0),...,((233|->0)|->218),((234|->0)|->228)} |
| 573 | | |
| 574 | | b_compile2(not_member(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, |
| 575 | | FullyKnown=false, % predicates never evaluated in b_compile1 |
| 576 | | b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF), |
| 577 | | (NExprB = b(value(X),_,_) |
| 578 | | -> (X==[], always_well_defined(A) -> NExpr = truth |
| 579 | | ; b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF), |
| 580 | | (quick_test_membership1(NExprA,X,PRes) |
| 581 | | -> convert_neg_pred_res(PRes,NExpr) |
| 582 | | ; NExpr = not_member(NExprA,NExprB)) |
| 583 | | ) |
| 584 | | ; NExpr = not_member(NExprA,NExprB), |
| 585 | | b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF) |
| 586 | | ). |
| 587 | | b_compile2(function(Fun,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, |
| 588 | | (is_lazy_extension_function_for_fun_app(Fun) |
| 589 | | -> Eval1=false % extension function applications treated lazily |
| 590 | | % TO DO: first evaluate B, if known then only evaluate relevant part of extension function |
| 591 | | ; Eval1=Eval), |
| 592 | | b_compile1(Fun,Parameters,LS,S,NExprA,Eval1,FullyKnown1,WF), |
| 593 | | combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown12), |
| 594 | | b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown2,WF), |
| 595 | | %tools_printing:print_term_summary(compiled_function(FullyKnown1,FullyKnown2,NExprA,NExprB)),nl, |
| 596 | | (FullyKnown2=true, |
| 597 | | (NExprA=b(value(_),_,_) -> true % no WD issue can be removed by apply, value already computed |
| 598 | | ; preferences:preference(find_abort_values,false) % in a sequence extension we could remove non-WD elements |
| 599 | | ), |
| 600 | | % check if we have enough information to apply a partially specified function as a list |
| 601 | | % e.g. if the function is [(int(1),A),(int(2),B)] and the argument is int(2): we can apply the function without knowing A or B; can have a dramatic importance when expanding unversal quantifiers ! |
| 602 | ? | can_apply_partially_specified_function(NExprA,NExprB,ResultExpr,WF) |
| 603 | | -> NExpr = ResultExpr, |
| 604 | | (FullyKnown12=true -> FullyKnown=true |
| 605 | | ; ResultExpr=value(ResultValue),known_value(ResultValue) -> FullyKnown=true |
| 606 | | ; FullyKnown = false) |
| 607 | | ; %tools_printing:print_term_summary(cannot_apply_function(FullyKnown2,NExprA,NExprB)),nl, |
| 608 | | %translate:print_bexpr(NExprA),nl, translate:print_bexpr(NExprB),nl, |
| 609 | | NExpr = function(NExprA,NExprB), FullyKnown = FullyKnown12). |
| 610 | | |
| 611 | | b_compile2(conjunct(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, |
| 612 | | FullyKnown=false, % predicates never automatically evaluated in b_compile1 |
| 613 | ? | b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF), |
| 614 | | (is_falsity(NExprA) -> NExpr = falsity |
| 615 | | ; |
| 616 | | % TO DO: propagate static information from A to B, e.g. if A :: x=10 -> add x=10 to LS/Parameters |
| 617 | | % also: try and detect unsatisfiable predicates beforehand |
| 618 | ? | b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF), |
| 619 | | (is_falsity(NExprB) -> NExpr = falsity |
| 620 | | ; is_truth(NExprB) -> get_texpr_expr(NExprA,NExpr) |
| 621 | | ; is_truth(NExprA) -> get_texpr_expr(NExprB,NExpr) |
| 622 | | ; NExpr = conjunct(NExprA,NExprB)) |
| 623 | | ). |
| 624 | | b_compile2(disjunct(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, |
| 625 | | FullyKnown=false, % predicates never automatically evaluated in b_compile1 |
| 626 | ? | b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF), |
| 627 | | (is_truth(NExprA) -> NExpr = truth |
| 628 | ? | ; b_compile1(B,Parameters,LS,S,NExprB,false,_,WF), % does not have to be executed in a successful branch: set Eval to false to avoid computing expensive expressions which may not be needed |
| 629 | | (is_truth(NExprB) -> NExpr = truth |
| 630 | | ; is_falsity(NExprA) -> get_texpr_expr(NExprB,NExpr) |
| 631 | | ; is_falsity(NExprB) -> get_texpr_expr(NExprA,NExpr) |
| 632 | | ; NExpr = disjunct(NExprA,NExprB)) |
| 633 | | ). |
| 634 | | b_compile2(implication(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, |
| 635 | | FullyKnown=false, % predicates never automatically evaluated in b_compile1 |
| 636 | | b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF), |
| 637 | | (is_falsity(NExprA) -> NExpr = truth |
| 638 | | ; is_truth(NExprA) -> b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF), get_texpr_expr(NExprB,NExpr) |
| 639 | | ; NExpr = implication(NExprA,NExprB), |
| 640 | | b_compile1(B,Parameters,LS,S,NExprB,false,_,WF) % B does not have to be executed in a successful branch: set Eval to false to avoid computing expensive expressions which may not be needed |
| 641 | | % TO DO: add preference to force pre-computation everywhere and pass Eval instead of false to b_compile1; ditto for disjunction |
| 642 | | ). |
| 643 | | b_compile2(negation(A),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, |
| 644 | | FullyKnown=false, % predicates never automatically evaluated in b_compile1 |
| 645 | | b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF), |
| 646 | | ( get_negated_operator_expr(NExprA,NegatedA) -> NExpr = NegatedA |
| 647 | | ; NExpr = negation(NExprA) |
| 648 | | ). |
| 649 | | b_compile2(if_then_else(A,B,C),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, |
| 650 | | b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF), |
| 651 | | (is_falsity(NExprA) -> b_compile1(C,Parameters,LS,S,NExprC,Eval,FullyKnown,WF), get_texpr_expr(NExprC,NExpr) |
| 652 | | ; is_truth(NExprA) -> b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown,WF), get_texpr_expr(NExprB,NExpr) |
| 653 | | ; NExpr = if_then_else(NExprA,NExprB,NExprC), FullyKnown=false, |
| 654 | | b_compile1(B,Parameters,LS,S,NExprB,false,_,WF), % set Eval to false as we do not know if B will be needed |
| 655 | | b_compile1(C,Parameters,LS,S,NExprC,false,_,WF) % ditto for C |
| 656 | | ). |
| 657 | | /* b_compile2(comprehension_set(CParas,Body),Parameters,LS,S,NExpr,_Eval,FullyKnown,WF) :- |
| 658 | | sort(Parameters,SParas), |
| 659 | | b_ast_cleanup:not_occurs_in_predicate(SParas,Body), %can only be applied if Body does not reference Parameters |
| 660 | | !, |
| 661 | | b_generate_inner_closure_if_necessary(Parameters,CParas,Body,LS,S,Result), % will itself call b_compile |
| 662 | | NExpr = value(Result), |
| 663 | | (ground(Result) -> FullyKnown=true ; FullyKnown=false). */ |
| 664 | | b_compile2(forall(ForallPara,A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, |
| 665 | | FullyKnown=false, % predicates never automatically evaluated in b_compile1 |
| 666 | | get_texpr_ids(ForallPara,AtomicIds), |
| 667 | | add_parameters(Parameters,AtomicIds,NParameters), |
| 668 | | b_compile1(A,NParameters,LS,S,NA,Eval,_FullyKnownA,WF), |
| 669 | | (is_falsity(NA) -> NExpr = truth |
| 670 | | ; b_compile1(B,NParameters,LS,S,NB,Eval,_FullyKnownB,WF), |
| 671 | | (is_truth(NB) -> NExpr = truth |
| 672 | | ; NExpr = forall(ForallPara,NA,NB) |
| 673 | | % TO DO ??: if we have an equality -> replace Body by value and remove quantifier |
| 674 | | %,print('COMPIlED: '),translate:print_bexpr(b(NExpr,pred,[])),nl |
| 675 | | ) |
| 676 | | ). |
| 677 | | % some special cases to avoid calling syntaxtransformation |
| 678 | | b_compile2(record_field(A,FieldName),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, |
| 679 | | b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF), |
| 680 | | % First: we can try compute even if value not fully known !, we just need record field list |
| 681 | | (get_record_field(NExprA,FieldName,NExpr,FullyKnown) -> true |
| 682 | | ; NExpr = record_field(NExprA,FieldName), FullyKnown=FullyKnownA). |
| 683 | | b_compile2(couple(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, |
| 684 | | %NExpr = couple(NExprA,NExprB), |
| 685 | | b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF), |
| 686 | | combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown), |
| 687 | | b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown2,WF), |
| 688 | | (FullyKnown \== true, % evaluation will already combine the result |
| 689 | | NExprA=b(value(VA),_,_),NExprB=b(value(VB),_,_) |
| 690 | | -> NExpr = value((VA,VB)) |
| 691 | | ; NExpr = couple(NExprA,NExprB)). |
| 692 | | b_compile2(image(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, |
| 693 | | b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF), |
| 694 | | combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown), |
| 695 | | b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown2,WF), |
| 696 | | (FullyKnown \= true, NExprA=b(value(VA),BT,BI), |
| 697 | | NExprB=b(value(VB),_,_), nonvar(VB), |
| 698 | | custom_explicit_sets:singleton_set(VB,VBX) |
| 699 | | -> filter_cannot_match(VA,(VBX,_),NewVA,_Filtered), %nl,print(filtered_image(VBX,VA,NewVA)),nl, |
| 700 | | NExpr = image(b(value(NewVA),BT,BI),NExprB) |
| 701 | | % TO DO: add case where VB==[] or VA==[] are the empty set |
| 702 | | ; NExpr = image(NExprA,NExprB) |
| 703 | | ). %, print('compile image: '),translate:print_bexpr(NExpr),nl. |
| 704 | | % TO DO: do something like can_apply_partially_specified_function; or filter_can_match |
| 705 | | b_compile2(composition(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, |
| 706 | | b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF), |
| 707 | | combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown), |
| 708 | | NExpr = composition(NExprA,NExprB), |
| 709 | | b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown2,WF), |
| 710 | | (FullyKnown=false, Eval=eval, performance_monitoring_on, |
| 711 | | ( FullyKnown1=true, NExprB=b(value(_),_,Info), large_known_value(NExprA,2) |
| 712 | | -> true %translate:nested_print_bexpr(NExprB),nl |
| 713 | | ; FullyKnown2=true, NExprA=b(value(_),_,Info), large_known_value(NExprB,2) |
| 714 | | -> true %translate:nested_print_bexpr(NExprA),nl |
| 715 | | ) |
| 716 | | -> perfmessage(b_compiler,'Cannot compile relational composition (try lift it out of quantification)',Info) |
| 717 | | ; true). |
| 718 | | b_compile2(assertion_expression(A,Msg,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, |
| 719 | | b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF), |
| 720 | | (is_truth(NExprA) -> % the ASSERT EXPR is redundant |
| 721 | | %print(removed_assert),nl, translate:print_bexpr(B),nl, |
| 722 | | b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown,WF), |
| 723 | | get_texpr_expr(NExprB,NExpr) |
| 724 | | ; b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF), |
| 725 | | FullyKnown=false, % we cannot get rid of WD condition |
| 726 | | NExpr = assertion_expression(NExprA,Msg,NExprB) |
| 727 | | ). |
| 728 | | b_compile2(domain(A),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, |
| 729 | | b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF), |
| 730 | | (FullyKnown1=false,get_texpr_expr(NExprA,NA),evaluate_domain(NA,Domain) % try and compute domain even if not fully known |
| 731 | | -> FullyKnown = true, NExpr = value(Domain) |
| 732 | | ; FullyKnown = FullyKnown1, NExpr = domain(NExprA)). |
| 733 | | b_compile2(range(A),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, |
| 734 | | b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF), |
| 735 | | (FullyKnown1=false,evaluate_range(NExprA,Range) % try and compute range even if not fully known |
| 736 | | -> FullyKnown = true, NExpr = value(Range) |
| 737 | | ; FullyKnown = FullyKnown1, NExpr = range(NExprA)). |
| 738 | | b_compile2(assign(LHS_List,RHS_List),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !, |
| 739 | | NExpr = assign(New_LHS_List,NewRHS_List), FullyKnown = false, |
| 740 | | maplist(b_compile_lhs(Parameters,LS,S,Eval,WF),LHS_List,New_LHS_List), |
| 741 | | b_compile_l(RHS_List,Parameters,LS,S,NewRHS_List,Eval,_FullyKnown2,WF). |
| 742 | | b_compile2(assign_single_id(ID,B),Parameters,LS,S,assign_single_id(ID,NExprB),Eval,FullyKnown,WF) :- !, |
| 743 | | FullyKnown = false, |
| 744 | | b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF). |
| 745 | | b_compile2(operation_call(Operation,OpCallResults,OpCallParas),Parameters,LS,S,InlinedOpCall,Eval,FullyKnown,WF) :- |
| 746 | | % TO DO: evaluate if we should also use the let_expression_global approach used for operation_call_in_expr |
| 747 | | !, |
| 748 | | def_get_texpr_id(Operation,op(OperationName)), |
| 749 | | FullyKnown = false, |
| 750 | | b_compile_l(OpCallParas,Parameters,LS,S,OpCallParaValues,Eval,_,WF), |
| 751 | | TopLevel=false, |
| 752 | | b_get_machine_operation_for_animation(OperationName,OpResults,OpFormalParameters,Body,_OType,TopLevel), |
| 753 | | bsyntaxtree:replace_ids_by_exprs(Body,OpResults,OpCallResults,Body2), |
| 754 | | get_texpr_ids(OpFormalParameters,OpIds), |
| 755 | | add_parameters(Parameters,OpIds,InnerParas), |
| 756 | | b_compile1(Body2,InnerParas,[],S,NBody,Eval,FullyKnown,WF), % do not pass local state: this may override constants,... from the called machine |
| 757 | | % Note: global state S should be valid for all machines in currently loaded specification |
| 758 | | get_texpr_ids(OpCallResults,OpRIds), |
| 759 | | add_parameters(Parameters,OpRIds,LocalKnownParas), |
| 760 | | simplify_assignment(OpFormalParameters,OpCallParaValues,LHSFormalParas,RHSCallVals), %% |
| 761 | | split_formal_parameters(LHSFormalParas,RHSCallVals,LocalKnownParas, |
| 762 | | FreshOpParas,FreshCallVals, |
| 763 | | ClashOpParas, ClashCallVals), % only set up VAR for fresh Paras |
| 764 | | % print(split(LHSFormalParas,LocalKnownParas,fresh(FreshOpParas),clash(ClashOpParas))),nl, |
| 765 | | (FreshOpParas=[] -> get_texpr_expr(NBody,Let1) |
| 766 | | ; create_equality_for_let(FreshOpParas,FreshCallVals,Equality1), |
| 767 | | Let1 = let(FreshOpParas,Equality1,NBody)), |
| 768 | | (ClashOpParas = [] |
| 769 | | -> InlinedOpCall = Let1 |
| 770 | | ; %nl,print(clash(ClashOpParas)),nl, |
| 771 | | maplist(create_fresh_id,ClashOpParas,FreshCopy), |
| 772 | | create_equality_for_let(ClashOpParas,FreshCopy,Equality2), % copy Values from Fresh Ids |
| 773 | | create_equality_for_let(FreshCopy,ClashCallVals,Equality3), % assign Parameter Vals to Fresh Ids |
| 774 | | get_texpr_pos(Body,BodyPos), BodyPosInfo = [nodeid(BodyPos)], |
| 775 | | Let2 = let(ClashOpParas,Equality2,b(Let1,subst,[BodyPosInfo])), |
| 776 | | InlinedOpCall = let(FreshCopy,Equality3,b(Let2,subst,[BodyPosInfo])) |
| 777 | | ). |
| 778 | | %, print('Compiled operation call: '), translate:print_subst(b(InlinedOpCall,subst,BodyPosInfo)),nl,nl. |
| 779 | | % Maybe this version is faster when no OpCallResults: |
| 780 | | %b_compile2(operation_call(Operation,OpCallResults,OpCallParas),Parameters,LS,S,InlinedOpCall,Eval,FullyKnown,WF) :- |
| 781 | | % OpCallResults=[], |
| 782 | | % !, |
| 783 | | % def_get_texpr_id(Operation,op(OperationName)), |
| 784 | | % FullyKnown = false, |
| 785 | | %% b_compile_l(Results,Parameters,LS,S,NResults,Eval,_,WF), |
| 786 | | % b_compile_l(OpCallParas,Parameters,LS,S,OpCallParaValues,Eval,_,WF), |
| 787 | | % TopLevel=false, |
| 788 | | % b_get_machine_operation_for_animation(OperationName,OpResults,OpParameters,Body,_OType,TopLevel), |
| 789 | | % % Note: input parameters cannot be assigned to: so replace ids is ok |
| 790 | | % % However, we cannot replace output parameters: these can be assigned to and we can have aliasing |
| 791 | | % % Note: no aliasing is allowed in OpCallResults (cf Atelier-B handbook x,x <-- op not allowed) |
| 792 | | % bsyntaxtree:replace_ids_by_exprs(Body,OpParameters,OpCallParaValues,Body2), |
| 793 | | % get_texpr_ids(OpResults,OpIds), |
| 794 | | % append(OpIds,Parameters,InnerParas), |
| 795 | | % b_compile1(Body2,InnerParas,LS,S,NBody,Eval,FullyKnown,WF), |
| 796 | | % FinalBody = NBody. |
| 797 | | b_compile2(Expr,Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- |
| 798 | | functor(Expr,BOP,2), |
| 799 | | binary_boolean_operator(BOP,_,_),!, % from kernel_mappings, slightly more efficient than syntaxtransformation |
| 800 | | arg(1,Expr,A), |
| 801 | | FullyKnown=false, % predicates never evaluated in b_compile1 |
| 802 | | b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF), |
| 803 | | arg(2,Expr,B), |
| 804 | | b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF), |
| 805 | | (eval_binary_bool(FullyKnownA,NExprA,FullyKnownB,NExprB,BOP,Result) |
| 806 | | -> NExpr = Result |
| 807 | | ; functor(NExpr,BOP,2), arg(1,NExpr,NExprA), arg(2,NExpr,NExprB) |
| 808 | | ). |
| 809 | | b_compile2(external_function_call(ExtFun,Args),_Parameters,LS,_S,NExpr,_Eval,FullyKnown,_WF) :- |
| 810 | | expects_unevaluated_args(ExtFun), |
| 811 | | memberchk(bind('$optimize_do_not_force_lazy_lookups',_),LS), % this is an optimize call |
| 812 | | !, |
| 813 | | debug_format(9,'Not compiling external function call to ~w~n',[ExtFun]), |
| 814 | | NExpr=external_function_call(ExtFun,Args), |
| 815 | | FullyKnown=false. |
| 816 | | b_compile2(Expr,Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- |
| 817 | | functor(Expr,BOP,2), |
| 818 | | kernel_mappings:binary_function(BOP,_,_),!, % slightly more efficient than syntaxtransformation |
| 819 | | arg(1,Expr,A), |
| 820 | ? | b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF), |
| 821 | | combine_fully_known(FullyKnownA,FullyKnownB,FullyKnown), |
| 822 | | arg(2,Expr,B), |
| 823 | | b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF), |
| 824 | | functor(NExpr,BOP,2), arg(1,NExpr,NExprA), arg(2,NExpr,NExprB). |
| 825 | | b_compile2(Expr,Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- |
| 826 | | functor(Expr,UOP,1), |
| 827 | | kernel_mappings:unary_function(UOP,_,_),!, % slightly more efficient than syntaxtransformation |
| 828 | | arg(1,Expr,A), |
| 829 | | b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown,WF), |
| 830 | | functor(NExpr,UOP,1), arg(1,NExpr,NExprA). |
| 831 | | b_compile2(Expr,Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- % GENERAL CASE |
| 832 | | %hit_profiler:add_profile_hit(Expr), |
| 833 | ? | syntaxtransformation(Expr,Subs,Names,NSubs,NExpr), |
| 834 | | get_texpr_ids(Names,Ids), |
| 835 | | add_parameters(Parameters,Ids,NParameters), |
| 836 | ? | b_compile_l(Subs,NParameters,LS,S,NSubs,Eval,FullyKnown,WF). |
| 837 | | |
| 838 | | b_compile_l([],_,_,_,[],_Eval,true,_WF). |
| 839 | | b_compile_l([Expr|ExprRest],P,LS,S,[NExpr|NExprRest],Eval,FullyKnown,WF) :- |
| 840 | ? | b_compile1(Expr,P,LS,S,NExpr,Eval,FullyKnown1,WF), |
| 841 | | combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown), |
| 842 | | b_compile_l(ExprRest,P,LS,S,NExprRest,Eval,FullyKnown2,WF). |
| 843 | | |
| 844 | | % detecth when a parameter clashes with existing known ids |
| 845 | | id_clash(LocalKnownParas,TID) :- def_get_texpr_id(TID,ID), member(ID,LocalKnownParas). |
| 846 | | |
| 847 | | /* comment in if we want to compile inner comprehension sets: |
| 848 | | :- use_module(bsyntaxtree,[split_names_and_types/3]). |
| 849 | | :- use_module(closures,[construct_closure_if_necessary/4]). |
| 850 | | b_generate_inner_closure_if_necessary(OuterParameters,ClosureParas,Condition,LocalState,State,Result) :- |
| 851 | | split_names_and_types(ClosureParas,Names,Types), |
| 852 | | add_parameters(OuterParameters,Names,FullNames), |
| 853 | | b_compile(Condition,FullNames,LocalState,State,ClosurePred), |
| 854 | | print('INNER COMPILE: '), translate:print_bexpr(ClosurePred),nl, |
| 855 | | construct_closure_if_necessary(Names,Types,ClosurePred,Result). |
| 856 | | */ |
| 857 | | |
| 858 | | |
| 859 | | % the LHS contains l-values which should not be looked up in the environment |
| 860 | | % however, we need to deal with things like f(i) := RHS and compile i |
| 861 | | b_compile_lhs(Parameters,LS,S,Eval,WF,TExpr,NewTExpr) :- |
| 862 | | TExpr = b(Expr,Type,Info), NewTExpr = b(NewExpr,Type,Info), |
| 863 | | b_compile_lhs_aux(Expr,Parameters,LS,S,NewExpr,Eval,WF). |
| 864 | | |
| 865 | | b_compile_lhs_aux(function(A,B),Parameters,LS,S,function(NewA,NewB),Eval,WF) :- !, |
| 866 | | b_compile_lhs(Parameters,LS,S,Eval,WF,A,NewA), % we can have nexted function calls f(e)(g) := |
| 867 | | b_compile1(B,Parameters,LS,S,NewB,Eval,_,WF). |
| 868 | | b_compile_lhs_aux(E,_,_,_,E,_,_WF). % other LHS should be identifier -> just copy |
| 869 | | |
| 870 | | get_record_field(b(value(Val),_,_),FieldName,value(Field),FullyKnown) :- !, |
| 871 | | nonvar(Val), Val=rec(Fields), |
| 872 | | safe_get_field(Fields,FieldName,Field), |
| 873 | | known_value(Field,FullyKnown). |
| 874 | | get_record_field(b(function(FUN,ARG),_Type,_Info),FieldName,function(ReducedFUN,ARG),false) :- |
| 875 | | % {1|->rec(a:1,b:2),...}(x)'b --> {1|->2,...}(x) |
| 876 | | %nl,print(get_field(FUN,ARG,FieldName)),nl, |
| 877 | | % TO DO: also allow nested functions calls {1|->rec(a:1,b:2),...}(x)(y)'b or other reduction operators |
| 878 | | get_field_in_range(FUN,FieldName,ReducedFUN). |
| 879 | | safe_get_field(V,FN,_) :- (var(V) ; var(FN)),!,fail. |
| 880 | | safe_get_field([field(N,V)|T],FieldName,Result) :- nonvar(N), |
| 881 | | (N=FieldName -> Result=V ; safe_get_field(T,FieldName,Result)). |
| 882 | | |
| 883 | | :- use_module(probsrc(custom_explicit_sets),[expand_custom_set_to_list/4, convert_to_avl/2]). |
| 884 | | :- use_module(probsrc(avl_tools),[avl_height_less_than/2]). |
| 885 | | get_field_in_range(b(value(OldVal),OldType,Info),FieldName, |
| 886 | | b(value(NewVal),set(couple(Dom,NewRange)),Info)) :- |
| 887 | | is_set_type(OldType,couple(Dom,OldRange)), |
| 888 | | nonvar(OldVal), OldVal=avl_set(AVL), |
| 889 | | avl_height_less_than(AVL,10), |
| 890 | | OldRange = record(Fields), |
| 891 | | member(field(FieldName,NewRange),Fields),!, |
| 892 | | expand_custom_set_to_list(avl_set(AVL),List,_,get_field_in_range), |
| 893 | | maplist(safe_get_range_field(FieldName),List,NewList), |
| 894 | | convert_to_avl(NewList,NewVal). |
| 895 | | |
| 896 | | % compute the field access for the range elements: |
| 897 | | safe_get_range_field(FieldName,(Dom,rec(Fields)),(Dom,Field)) :- safe_get_field(Fields,FieldName,Field). |
| 898 | | |
| 899 | | |
| 900 | | eval_binary_bool(true,b(value(ValA),_,_),true,b(value(ValB),_,_),BOP,Result) :- |
| 901 | | ground(ValA), |
| 902 | | ground(ValB), |
| 903 | | eval_binary_aux(BOP,ValA,ValB,Result). |
| 904 | | |
| 905 | | eval_binary_aux(less,int(A),int(B),Result) :- |
| 906 | | (A < B -> Result = truth ; Result = falsity). |
| 907 | | eval_binary_aux(greater,int(A),int(B),Result) :- |
| 908 | | (A > B -> Result = truth ; Result = falsity). |
| 909 | | eval_binary_aux(less_equal,int(A),int(B),Result) :- |
| 910 | | (A =< B -> Result = truth ; Result = falsity). |
| 911 | | eval_binary_aux(greater_equal,int(A),int(B),Result) :- |
| 912 | | (A >= B -> Result = truth ; Result = falsity). |
| 913 | | eval_binary_aux(subset,avl_set(A1),avl_set(A2),Result) :- |
| 914 | | (custom_explicit_sets:check_avl_subset(A1,A2) -> Result = truth ; Result = falsity). |
| 915 | | eval_binary_aux(subset,[],_,Result) :- Result=truth. |
| 916 | | %eval_binary_aux(less_real,real(A),real(B),Result) :- % TO DO |
| 917 | | % (A < B -> Result = truth ; Result = falsity). |
| 918 | | % TO DO: other operators are not_subset, strict_subset, ... intervals for subset,... |
| 919 | | |
| 920 | | |
| 921 | | |
| 922 | | :- use_module(store,[lookup_value_for_existing_id_wf/5]). |
| 923 | | compute_lazy_lookup(Id,Expr,LS,S,NExpr,FullyKnown,WF) :- |
| 924 | | lookup_value_for_existing_id_wf(Id,LS,S,(Evaluated,Value),WF), |
| 925 | | % the lazy expression has already been registered, but maybe not yet evaluated |
| 926 | | !, |
| 927 | | known_value(Value,FullyKnown), % compute if value fully known |
| 928 | | (Evaluated==pred_true -> NExpr = value(Value) |
| 929 | | ; FullyKnown==true -> NExpr = value(Value) |
| 930 | | ; memberchk(bind('$optimize_do_not_force_lazy_lookups',_),LS) |
| 931 | | -> NExpr = Expr % we do not force lookup: there could be WD issues ! |
| 932 | | % TO DO: examine Infos for wd_condition; we could also return NExpr = lazy_value(Id,Evaluated,Value) |
| 933 | | ; if(Evaluated = pred_true, |
| 934 | | % will force evaluation ! Note: this means shared expression inside a compiled expression must be well-defined |
| 935 | | NExpr = value(Value), |
| 936 | | (add_internal_error_wf(b_compiler,'Compilation failed: ', Id, unknown,WF), |
| 937 | | fail)) |
| 938 | | ). |
| 939 | | compute_lazy_lookup(Id,_E,_LS,_S,_LazyValue,_,WF) :- |
| 940 | | add_internal_error_wf(b_compiler,'Compilation failed, illegal lazy_lookup_value: ',Id,unknown,WF), |
| 941 | | fail. |
| 942 | | |
| 943 | | combine_fully_known(true,A,A). |
| 944 | | combine_fully_known(false,_,false). |
| 945 | | |
| 946 | | :- use_module(tools_lists,[length_greater/2]). |
| 947 | | % is an extension function with at least two elements, but not too long |
| 948 | | % (for long set extensions it is much better to compile them to avl once; see private_examples/ClearSy/2019_Sep/rule_dummy) |
| 949 | | % extension functions are treated lazily in b_interpreter for function application under the condition: |
| 950 | | % memberchk(contains_wd_condition,FInfo) ; preferences:preference(use_clpfd_solver,false) ; ground_value(ArgValue) |
| 951 | | is_lazy_extension_function_for_fun_app(b(A,_,FInfo)) :- |
| 952 | | preferences:preference(data_validation_mode,false), |
| 953 | | (memberchk(contains_wd_condition,FInfo) -> Lim=98 ; Lim = 23), |
| 954 | | is_extension_function_aux(A,Lim). |
| 955 | | is_extension_function_aux(set_extension([_A,_|T]),Lim) :- \+ length_greater(T,Lim). |
| 956 | | is_extension_function_aux(sequence_extension([_,_|T]),Lim) :- \+ length_greater(T,Lim). |
| 957 | | |
| 958 | | :- use_module(bsyntaxtree,[is_set_type/2]). |
| 959 | | % check if we can apply an argument to a partially specified function (as a list and now also as AVL) |
| 960 | | %can_apply_partially_specified_function(Fun,X,_,_) :- print(fun(Fun)),nl,print(val(X)),nl,fail. |
| 961 | | can_apply_partially_specified_function(b(Expr,TYPE,_), b(value(X),TA,_),ResultExpr,WF) :- |
| 962 | ? | can_apply_aux(Expr,TYPE,X,TA,ResultExpr,WF). |
| 963 | | |
| 964 | | can_apply_aux(value(VAL),TYPE,X,TA,value(ResultValue),WF) :- |
| 965 | | is_set_type(TYPE,couple(TA,_TB)), |
| 966 | ? | lookup_result(VAL,X,ResultValue,WF). |
| 967 | | can_apply_aux(sequence_extension(List),_,X,integer,ResultExpr,_WF) :- |
| 968 | | % important, e.g., for solving test 1551: {b|[a,b,c](2)=333} =res & a : res & b:res |
| 969 | | nonvar(X), X=int(Index), number(Index), |
| 970 | | % this will prevent computing rest of sequence extension: can hide WD issues ! |
| 971 | | % print(apply_seq_extension(Index,List)),nl, |
| 972 | | nth1(Index,List,b(ResultExpr,_,_)). |
| 973 | | |
| 974 | | :- use_module(kernel_equality,[equality_objects_wf/4, equality_can_be_decided_by_unification/1]). |
| 975 | | %lookup_result(VAR,ArgValue,Result,WF) :- var(VAR),!,kernel_mappings:kernel_call_apply_to(VAR,ArgValue,Result,unknown,unknown,WF). |
| 976 | | % the clause above is unsound; as apply_to CAN RAISE WD ERRORS !! what if we have IF 1:dom(f) THEN f(1) ELSE f(0) END; we do not want to compute f(1) ! it can also instantiate unbound variables ! |
| 977 | | % the idea was to avoid that we wait on the full function, before compiled closure can be evaluated; test 1552 |
| 978 | | % important for e.g. a = {(1, {([]|->2)} ), (2, const(1, [a(1)]))} |
| 979 | | % or: a = {1 |-> {[] |-> 2}, 2 |-> (dom({pi,ff,p|((pi : seq(INTEGER) & ff : INTEGER) & p : seq(INTEGER)) & (p |-> ff : [a(1)](1) & pi = 1 -> p)}) \/ {[] |-> 1})} |
| 980 | | % test 1552 is currently skipped |
| 981 | | % TO DO: think whether there are other deterministic computations that can be done in b_compile: prj1,prj2, record-field access ? this would ensure that closures,... can be computed earlier |
| 982 | | lookup_result(VAR,_,_,_WF) :- var(VAR),!,fail. |
| 983 | | lookup_result(avl_set(A),X,Result,WF) :- |
| 984 | ? | if(custom_explicit_sets:try_apply_to_avl_set_wf(X,Result,A,WF), |
| 985 | | true, % precompiled function application |
| 986 | | (debug_format(19,'Function application in b_compiler for avl_set is not well-defined for: ~w~n',[X]), |
| 987 | | % We could transform the function application into a construct that raises a WD error |
| 988 | | fail)). |
| 989 | | lookup_result(closure(_P,_T,_B),_X,_Result,_WF) :- !, |
| 990 | | fail. % TODO: should we replace parameters by values in body? if domain is full type? |
| 991 | | lookup_result(List,X,Result,WF) :- List = [_|_],equality_can_be_decided_by_unification(X),!, |
| 992 | | % this is relevant for long lists, |
| 993 | | % see public_examples/B/ExternalFunctions/Satsolver/QueensBoardVersionTF_Satsolver.mch |
| 994 | | fast_lookup_result(List,X,Result,WF). |
| 995 | | lookup_result(List,X,Result,WF) :- |
| 996 | | regular_lookup_result_in_list(List,X,Result,WF). |
| 997 | | |
| 998 | | regular_lookup_result_in_list([],X,_Result,_WF) :- |
| 999 | | debug_format(19,'Function application in b_compiler for list is not well-defined for: ~w~n',[X]), % ditto |
| 1000 | | fail. |
| 1001 | | regular_lookup_result_in_list([(HFrom,HTo)|T],X,Result,WF) :- |
| 1002 | | equality_objects_wf(HFrom,X,PredRes,WF), |
| 1003 | | %kernel_equality:equality_objects1(HFrom,X,PredRes,WF), % this could be called if X is guaranteed nonvar |
| 1004 | | nonvar(PredRes), % only proceed if we have enough information to determine the result of the comparison |
| 1005 | | (PredRes = pred_true -> Result = HTo % we have found the value; we assume there is no other value later |
| 1006 | | % TO DO: if find_abort_values=true: look later in the list if for all other HFrom PredRes=pred_false |
| 1007 | | ; regular_lookup_result_in_list(T,X,Result,WF)). |
| 1008 | | |
| 1009 | | % a faster version which does not use equality_objects_wf |
| 1010 | | fast_lookup_result([(HFrom,HTo)|T],X,Result,WF) :- |
| 1011 | | equality_can_be_decided_by_unification(HFrom), !, |
| 1012 | | (HFrom=X -> Result = HTo |
| 1013 | | ; fast_lookup_result(T,X,Result,WF) |
| 1014 | | ). |
| 1015 | | fast_lookup_result(List,X,Result,WF) :- |
| 1016 | | regular_lookup_result_in_list(List,X,Result,WF). |
| 1017 | | |
| 1018 | | |
| 1019 | | % get_comprehension_set(b(SET,_,_),ID,PRED) :- get_comprehension_set_aux(SET,ID,PRED). |
| 1020 | | % get_comprehension_set_aux(comprehension_set([TID],PRED),ID,PRED) :- |
| 1021 | | % get_texpr_id(TID,ID). |
| 1022 | | % get_comprehension_set_aux(value(V),ID,PRED) :- nonvar(V), V = closure([ID],_,PRED). |
| 1023 | | |
| 1024 | | |
| 1025 | | |
| 1026 | | |
| 1027 | | quick_test_membership1(b(value(VA),_,_),VB,Result) :- |
| 1028 | ? | quick_test_membership_aux(VB,VA,Result). |
| 1029 | | quick_test_membership_aux(VAR,_,_) :- var(VAR),!,fail. |
| 1030 | | quick_test_membership_aux([],_,pred_false). |
| 1031 | | quick_test_membership_aux(avl_set(AVL),X,Result) :- |
| 1032 | | custom_explicit_sets:quick_test_avl_membership(AVL,X,Result). % we could also check that in case X is not ground but partially instantiated, whether there is a possible match in AVL (if not Result = pred_false) |
| 1033 | | quick_test_membership_aux(global_set(GS),X,Result) :- nonvar(X), X=int(IX), nonvar(IX), |
| 1034 | | custom_explicit_sets:membership_global_set(GS,X,R,_WF), |
| 1035 | | nonvar(R), Result=R. |
| 1036 | | quick_test_membership_aux(closure(P,T,B),X,Result) :- nonvar(X), X=int(IX), nonvar(IX), |
| 1037 | | is_fixed_interval(P,T,B,LOW,UP), |
| 1038 | | kernel_equality:in_nat_range_test(X,int(LOW),int(UP),R), |
| 1039 | | nonvar(R), Result=R. |
| 1040 | | quick_test_membership_aux(closure(P,T,B),X,Result) :- X==[], % check {} : POW(_) / FIN(_) and {} : POW1(_) / FIN1(_) |
| 1041 | ? | custom_explicit_sets:is_powerset_closure(closure(P,T,B),Kind,_), |
| 1042 | | (contains_empty_set(Kind) -> Result = pred_true ; Result=pred_false). |
| 1043 | | |
| 1044 | | is_fixed_interval(P,T,B,LOW,UP) :- |
| 1045 | | custom_explicit_sets:is_interval_closure(P,T,B,LOW,UP), integer(LOW),integer(UP). |
| 1046 | | |
| 1047 | | contains_empty_set(pow). |
| 1048 | | contains_empty_set(fin). |
| 1049 | | |
| 1050 | | convert_pred_res(pred_false,falsity). |
| 1051 | | convert_pred_res(pred_true,truth). |
| 1052 | | convert_neg_pred_res(pred_true,falsity). |
| 1053 | | convert_neg_pred_res(pred_false,truth). |
| 1054 | | |
| 1055 | | generate_equality(b(A,_,_),b(B,_,_),Res) :- |
| 1056 | | ( generate_equality_aux(A,B,Res) ; |
| 1057 | | generate_equality_aux(B,A,Res) ), |
| 1058 | | !. |
| 1059 | | generate_equality(A,B,equal(A,B)). |
| 1060 | | |
| 1061 | | generate_equality_aux(convert_bool(AA),value(PT),Res) :- |
| 1062 | | PT==pred_true, |
| 1063 | | get_texpr_expr(AA,TA), |
| 1064 | | !, |
| 1065 | | Res = TA. |
| 1066 | | generate_equality_aux(convert_bool(AA),value(PF),Res) :- |
| 1067 | | PF==pred_false,!, |
| 1068 | | Res = negation(AA). |
| 1069 | | |
| 1070 | | % generate an equal(_,_) node where the second one is a Value |
| 1071 | | generate_equality_with_value(b(value(ValA),_,_),true,ValB,true,_TA,NExpr) :- |
| 1072 | | % both are FullyKnown |
| 1073 | | simple_value(ValA), % we should avoid closures |
| 1074 | | !, |
| 1075 | | kernel_equality:equality_objects(ValA,ValB,PRes), |
| 1076 | | convert_pred_res(PRes,NExpr). |
| 1077 | | generate_equality_with_value(NExprA,_,Value,_,TA,equal(NExprA,b(value(Value),TA,[]))). |
| 1078 | | |
| 1079 | | % similar to custom_explicit_sets:simple_value |
| 1080 | | % values where we can decide equality easily |
| 1081 | | simple_value(fd(_,_)). |
| 1082 | | simple_value(pred_true /* bool_true */). |
| 1083 | | simple_value(pred_false /* bool_false */). |
| 1084 | | simple_value(int(_)). |
| 1085 | | simple_value((A,B)) :- simple_value(A), simple_value(B). |
| 1086 | | simple_value(rec(Fields)) :- maplist(simple_field,Fields). |
| 1087 | | simple_value(string(_)). |
| 1088 | | |
| 1089 | | simple_field(field(_,Val)) :- simple_value(Val). |
| 1090 | | |
| 1091 | | known_value(X,FullyKnown) :- (known_value(X) -> FullyKnown=true ; FullyKnown=false). |
| 1092 | | known_value(X) :- nonvar(X), known_value2(X). |
| 1093 | | known_value2(global_set(GS)) :- nonvar(GS). |
| 1094 | | known_value2(freetype(GS)) :- nonvar(GS). |
| 1095 | | known_value2(closure(P,T,B)) :- known_closure(P,T,B). |
| 1096 | | %Note: for other closures: they still may have to be computed; some of the computations in wd_and_efficient could be expensive for closures |
| 1097 | | known_value2(avl_set(_)). % already fully normalised |
| 1098 | | known_value2((X,Y)) :- known_value(X),known_value(Y). |
| 1099 | | known_value2(fd(A,B)) :- number(A),atomic(B). |
| 1100 | | known_value2(int(N)) :- number(N). |
| 1101 | | known_value2([]). |
| 1102 | | known_value2(pred_true). |
| 1103 | | known_value2(pred_false). |
| 1104 | | known_value2(string(S)) :- atomic(S). |
| 1105 | | known_value2([H|T]) :- known_value(H), known_value(T). |
| 1106 | | %known_value2(record(Fields)) :- known_fields(Fields). |
| 1107 | | known_value2(rec(Fields)) :- known_fields(Fields). |
| 1108 | | |
| 1109 | | :- use_module(avl_tools,[avl_height_less_than/2]). |
| 1110 | | % large known avl_set value; for issueing perfmessage warnings |
| 1111 | | large_known_value(b(value(V),_,_),Lim) :- nonvar(V), large_known_aux(V,Lim). |
| 1112 | | large_known_aux(avl_set(A),Lim) :- |
| 1113 | | \+ avl_height_less_than(A,Lim). |
| 1114 | | |
| 1115 | | % something we could do: |
| 1116 | | %optimize_known_value([H|T],Res) :- (convert_to_avl([H|T],CS) -> Res=CS ; print(failed_to_convert_known_list),nl,fail). |
| 1117 | | % try_convert_to_avl |
| 1118 | | |
| 1119 | | known_closure(P,T,B) :- custom_explicit_sets:is_interval_closure(P,T,B,Low,Up), !, |
| 1120 | | number(Low), number(Up), |
| 1121 | | Up < Low+1000. |
| 1122 | | known_closure(P,T,B) :- |
| 1123 | | is_cartesian_product_closure(closure(P,T,B),A1,A2), |
| 1124 | | !,% we could call is_cartesian_product_closure_aux(P,T,B,A1,A2) |
| 1125 | | known_value(A1), known_value(A2). |
| 1126 | | |
| 1127 | | known_fields(X) :- var(X),!,fail. |
| 1128 | | known_fields([]). |
| 1129 | | known_fields([field(N,V)|T]) :- ground(N),known_value(V),known_fields(T). |
| 1130 | | |
| 1131 | | %b_evaluate1(TExpr,Parameters,LS,S,ResultTExpr,FullyKnown) :- |
| 1132 | | |
| 1133 | | check_is_id_list([],[]). |
| 1134 | | check_is_id_list([H|T],Res) :- |
| 1135 | | (H=b(identifier(_),_,_) |
| 1136 | | -> add_internal_error('Typed id list as argument: ',check_is_id_list([H|T],Res)), % use get_texpr_ids or maplist(def_get_texpr_id,P,PIDs) |
| 1137 | | maplist(def_get_texpr_id,[H|T],Res) |
| 1138 | | ; Res=[H|T]). |
| 1139 | | |
| 1140 | | :- use_module(kernel_frozen_info,[kfi_domain/2]). |
| 1141 | | |
| 1142 | | :- use_module(custom_explicit_sets,[construct_interval_closure/3]). |
| 1143 | | % try and evaluate domain of a list (avl_set already dealt with separately) |
| 1144 | | %evaluate_domain(X,_) :- print(dom(X)),nl,fail. |
| 1145 | | evaluate_domain(sequence_extension(L),Domain) :- length(L,Len), |
| 1146 | | % this will prevent computing range of sequence extension: can hide WD issues ! TO DO: check wd info and/or preference |
| 1147 | | construct_interval_closure(1,Len,Domain). |
| 1148 | | % TO DO: set_extension when possible ? |
| 1149 | | evaluate_domain(value(L),Domain) :- |
| 1150 | | get_domain(L,Domain). |
| 1151 | | |
| 1152 | | get_domain(V,Dom) :- var(V),!,kfi_domain(V,Dom). % try infer domain from attached co-routines |
| 1153 | | get_domain([],[]). |
| 1154 | | get_domain([V|VT],Result) :- nonvar(V), V=(D,_), |
| 1155 | | known_value(D),get_list_domain(VT,DT), |
| 1156 | | %length(DT,Len),print(got_list_domain(D,Len)),nl, |
| 1157 | | (custom_explicit_sets:try_convert_to_avl([D|DT],Res) -> Result=Res |
| 1158 | | ; write(could_not_convert_domain_to_avl(D)),nl, Result=[D|DT]). %sort([D|DT],Result)? |
| 1159 | | % we could also do this: |
| 1160 | | %get_domain(closure(Par,Typ,Body),Result) :- |
| 1161 | | % is_lambda_value_domain_closure(Par,Typ,Body, DomainValue,Expr), check_wd(Expr), |
| 1162 | | % Result=DomainValue. |
| 1163 | | get_list_domain(V,_) :- var(V),!,fail. |
| 1164 | | get_list_domain([],[]). |
| 1165 | | get_list_domain([V|VT],[D|DT]) :- nonvar(V), V=(D,_), |
| 1166 | | known_value(D),get_list_domain(VT,DT). |
| 1167 | | |
| 1168 | | |
| 1169 | | :- use_module(kernel_frozen_info,[kfi_range/2]). |
| 1170 | | |
| 1171 | | % try and evaluate range of a list (avl_set already dealt with separately) |
| 1172 | | evaluate_range(b(value(L),_T,_),Range) :- |
| 1173 | | get_range(L,Range). |
| 1174 | | get_range(V,Dom) :- var(V),!,kfi_range(V,Dom). % try infer range from attached co-routines |
| 1175 | | get_range([],[]). |
| 1176 | | get_range([V|VT],Result) :- nonvar(V), V=(_,D), |
| 1177 | | known_value(D), |
| 1178 | | get_list_range(VT,DT), |
| 1179 | | sort([D|DT],Result). |
| 1180 | | |
| 1181 | | get_list_range(V,_) :- var(V),!,fail. |
| 1182 | | get_list_range([],[]). |
| 1183 | | get_list_range([V|VT],[D|DT]) :- |
| 1184 | | nonvar(V), V=(_,D), |
| 1185 | | known_value(D), |
| 1186 | | get_list_range(VT,DT). |
| 1187 | | |
| 1188 | | create_equality_for_let(LHS,RHS,Conj) :- |
| 1189 | | maplist(create_eq,LHS,RHS,CL), |
| 1190 | | conjunct_predicates(CL,Conj). |
| 1191 | | create_eq(Id,Expr,TPred) :- safe_create_texpr(equal(Id,Expr),pred,TPred). |
| 1192 | | |
| 1193 | | % split formal operation call parameters into those which clash and those that do not: |
| 1194 | | split_formal_parameters([],[],_,[],[],[],[]). |
| 1195 | | split_formal_parameters([Formal1|FormalT],[Val1|VT],LocalKnownParas,Fresh,FV,Clash,CV) :- |
| 1196 | | (id_clash(LocalKnownParas,Formal1) |
| 1197 | | -> Fresh = FreshT, FV=FVT, Clash = [Formal1|ClashT], CV = [Val1|CVT] |
| 1198 | | ; Fresh = [Formal1|FreshT], FV = [Val1|FVT], Clash = ClashT, CV = CVT |
| 1199 | | ), split_formal_parameters(FormalT,VT,LocalKnownParas,FreshT,FVT,ClashT,CVT). |
| 1200 | | |
| 1201 | | :- use_module(gensym,[gensym/2]). |
| 1202 | | create_fresh_id(b(identifier(_),T,I),b(identifier(FRESHID),T,I)) :- |
| 1203 | | gensym('__COMPILED_ID__',FRESHID). |
| 1204 | | |
| 1205 | | :- use_module(bsyntaxtree, [get_texpr_pos/2,same_id/3]). |
| 1206 | | % compute which assignments are really necessary, remove skip assignments x := x |
| 1207 | | simplify_assignment([],[],[],[]). |
| 1208 | | simplify_assignment([ID1|T1],[ID2|T2],Res1,Res2) :- |
| 1209 | | (same_id(ID1,ID2,_) -> Res1=TR1, Res2=TR2 ; Res1=[ID1|TR1], Res2=[ID2|TR2]), |
| 1210 | | simplify_assignment(T1,T2,TR1,TR2). |
| 1211 | | |
| 1212 | | |
| 1213 | | /* |
| 1214 | | % check if an AST term is a total lambda without WD condition: |
| 1215 | | % NExprA=value(closure([x,...,'_lambda_result_'],b(equal())), NExprB=couple(,,,,) -> replace x by parameters |
| 1216 | | % possibly better to do this via contains_wd_condition or similar Info field?! |
| 1217 | | |
| 1218 | | |
| 1219 | | is_total_lambda(b(value(V),_,_),OtherIDs,LambdaExpr) :- nonvar(V), |
| 1220 | | V=closure(Args,_Types,Body), |
| 1221 | | is_total_lambda_closure(Args,Body, OtherIDs, LambdaExpr). |
| 1222 | | |
| 1223 | | :- use_module(probsrc(bsyntaxtree),[conjunction_to_list/2,occurs_in_expr/2]). |
| 1224 | | is_total_lambda_closure(Args,b(equal(TLambda,LambdaExpr),pred,_),OtherIDs,LambdaExpr) :- |
| 1225 | | get_texpr_id(TLambda,LambdaID), |
| 1226 | | append(OtherIDs,[LambdaID],Args), |
| 1227 | | \+ occurs_in_expr(LambdaID,LambdaExpr). |
| 1228 | | |
| 1229 | | % try and get arguments from expression |
| 1230 | | get_actual_arguments([_],Expr,Args) :- !, |
| 1231 | | % print('arg1: '),tools_printing:print_term_summary(Expr),nl, |
| 1232 | | check_simple(Expr), |
| 1233 | | Args= [Expr]. |
| 1234 | | get_actual_arguments([_|T],b(Couple,_,_),[Arg1|TArgs]) :- |
| 1235 | | get_couple(Couple,Arg1,Arg2), print('arg: '),tools_printing:print_term_summary(Arg1),nl, |
| 1236 | | check_simple(Arg1), |
| 1237 | | get_actual_arguments(T,Arg2,TArgs). |
| 1238 | | |
| 1239 | | check_simple(b(V,_,_)) :- simple2(V). |
| 1240 | | simple2(value(_)). |
| 1241 | | simple2(identifier(_)). |
| 1242 | | simple2(integer(_)). |
| 1243 | | |
| 1244 | | get_couple(couple(A,B),A,B). |
| 1245 | | %get_couple(value(V),A,B) :- nonvar(V), V=(V1,V2), ... % TODO |
| 1246 | | |
| 1247 | | |
| 1248 | | Code for bcompile2(function(...)) |
| 1249 | | |
| 1250 | | |
| 1251 | | % ; is_total_lambda(NExprA,Ids,Expr) , |
| 1252 | | % get_actual_arguments(Ids,NExprB,Args) %, print(ok),nl, translate:l_print_bexpr_or_subst(Args),nl |
| 1253 | | % -> |
| 1254 | | % bsyntaxtree:replace_ids_by_exprs(Expr,Ids,Args,Result), |
| 1255 | | % % only ok if we do not replicate expressions !! we could repeatedly re-apply rule / compilation on result |
| 1256 | | % print(' replaced: '),translate:print_bexpr(Result),nl, |
| 1257 | | % Result = b(NExpr,_,_), FullyKnown = FullyKnown12 |
| 1258 | | |
| 1259 | | */ |