| 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 | :- module(bvisual, | |
| 5 | [ | |
| 6 | create_tree_node/4, get_tree_node_info/4, | |
| 7 | get_tree_from_expr/4, | |
| 8 | get_tree_from_expr2/4, | |
| 9 | write_dot_graph_to_file/2, | |
| 10 | %print_dot_graph/1, | |
| 11 | get_any/5, | |
| 12 | %get_any_most_satisfier/5, | |
| 13 | ||
| 14 | get_operation_pre/3, | |
| 15 | get_properties/2 | |
| 16 | ] | |
| 17 | ). | |
| 18 | ||
| 19 | :- use_module(module_information,[module_info/2]). | |
| 20 | :- module_info(group,dot). | |
| 21 | :- module_info(description,'Generate a dot visualization of B predicates and expressions.'). | |
| 22 | ||
| 23 | :- use_module(library(lists), [maplist/3, scanlist/4]). | |
| 24 | %:- use_module(library(terms)). | |
| 25 | ||
| 26 | :- use_module(bsyntaxtree). | |
| 27 | :- use_module(translate, [translate_bvalue_with_limit/3, | |
| 28 | translate_bexpression_with_limit/3]). | |
| 29 | :- use_module(kernel_waitflags, [ | |
| 30 | init_wait_flags/1, | |
| 31 | ground_wait_flags/1]). | |
| 32 | :- use_module(b_interpreter, [ | |
| 33 | b_test_boolean_expression_wf/3, | |
| 34 | b_not_test_boolean_expression_wf/3, | |
| 35 | b_compute_expression_nowf/4]). | |
| 36 | ||
| 37 | :- use_module(bvisual_any_maxsolver). | |
| 38 | :- use_module(error_manager). | |
| 39 | ||
| 40 | ||
| 41 | %:- use_module(self_check). | |
| 42 | ||
| 43 | %:- meta_predicate visit_tree(3,2,-,-,-). | |
| 44 | :- meta_predicate visit_tree(:,2,-,-,-). | |
| 45 | ||
| 46 | ||
| 47 | % PARAMETERS | |
| 48 | ||
| 49 | max_chars_per_line(40). | |
| 50 | max_lines(10). | |
| 51 | max_chars_total(400). % :- max_chars_per_line(X), max_lines(ML), T is X*ML. | |
| 52 | ||
| 53 | %% | |
| 54 | % Tree format: | |
| 55 | % Trees used by write_dot_graph_to_file/2 are modelled by the bind/3 | |
| 56 | % predicate: | |
| 57 | % bind(Children, NewLocalState, Metas). | |
| 58 | % Children is a list of subexpressions, whose numbers may be greater than two. | |
| 59 | % NewLocalState is a new local state for the subexpressions. | |
| 60 | % Metas are informations about the expression, like value, label etc. | |
| 61 | % | |
| 62 | % Important: Avoid access bind directly since it's structure may | |
| 63 | % be changed. Use accessors defined below. | |
| 64 | % They provide a convenient way to access the meta informations. | |
| 65 | % | |
| 66 | % Use get_tree_from_expr(Tree, Expr, LocalStale, State) to gain | |
| 67 | % a bind based tree from a predicate or expression evaluated in LocalState | |
| 68 | % and State. | |
| 69 | % | |
| 70 | % Use get_tree_from_expr2(State, LocalState, TExpr, Tree) to inspect the | |
| 71 | % predicate or expression only without walking down the children recursively. | |
| 72 | % | |
| 73 | ||
| 74 | %% | |
| 75 | % accessors & shortcuts | |
| 76 | % | |
| 77 | ||
| 78 | create_long_tree_node(bind(Children, Label, Type, Value, LongDesc), | |
| 79 | Children, Label, Type, Value, LongDesc). | |
| 80 | get_tree_node_info(NODE, Children, NewLocalState, Metas) :- | |
| 81 | (create_tree_node(NODE, C,N,M) -> Children=C, NewLocalState=N, Metas=M | |
| 82 | ; add_error(bvisual,'Illegal node: ',NODE)). | |
| 83 | create_tree_node(bind(Children, NewLocalState, Metas), | |
| 84 | Children, NewLocalState, Metas). | |
| 85 | ||
| 86 | ||
| 87 | % bind([],cv_o,nonboolean,137,b(identifier(cv_o),integer,[nodeid(pos(139677,56,192,18,192,21))])) | |
| 88 | ||
| 89 | has_no_children(Node) :- child_nodes(Node,[]). | |
| 90 | ||
| 91 | child_nodes(bind(ChildNodes,_,_,_,_), ChildNodes). | |
| 92 | child_nodes(bind(ChildNodes,_,_), ChildNodes). | |
| 93 | ||
| 94 | label(bind(_,Label,_,_,_), Label). | |
| 95 | label(bind(_,_, Metas), Val) :- member(label(Val), Metas),!. | |
| 96 | ||
| 97 | value(bind(_,_,_,Val,_), Val). | |
| 98 | value(bind(_,_, Metas), Val) :- member(value(Val), Metas),!. | |
| 99 | ||
| 100 | long_desc(bind(_,_,_,_,Val), Val). | |
| 101 | long_desc(bind(_,_, Metas), Val):- member(long_desc(Val), Metas),!. | |
| 102 | ||
| 103 | is_boolean(bind(_,_,boolean,_,_)). | |
| 104 | is_boolean(bind(_,_, Metas)):- member(type(boolean), Metas),!. | |
| 105 | ||
| 106 | %type(bind(_,_, Metas), Val):- member(type(Val), Metas),!. | |
| 107 | ||
| 108 | is_explicit_value_node(Node) :- long_desc(Node,Val), is_explicit_value(Val). | |
| 109 | ||
| 110 | %% | |
| 111 | % Evaluate an expression and it's subexpressions and | |
| 112 | % gain their values as a tree. | |
| 113 | % | |
| 114 | :- use_module(tools,[catch_call/1]). | |
| 115 | :- use_module(b_global_sets,[add_prob_deferred_set_elements_to_store/3]). | |
| 116 | get_tree_from_expr(Tree, Expr, LocalState, State) :- | |
| 117 | (get_preference(dot_use_unicode,true) -> translate:set_unicode_mode ; true), | |
| 118 | add_prob_deferred_set_elements_to_store(State,State1,visible), | |
| 119 | catch_call(get_tree_from_expr3(State1, LocalState, Expr, Tree)), | |
| 120 | (get_preference(dot_use_unicode,true) -> translate:unset_unicode_mode ; true). | |
| 121 | % catch: as this can sometimes generate resource_error(memory) error exceptions | |
| 122 | ||
| 123 | ||
| 124 | % whole tree at once | |
| 125 | get_tree_from_expr3(State, LocalState, Expr, Tree):- | |
| 126 | get_tree_from_expr2(State, LocalState, Expr, NewTree), | |
| 127 | get_tree_node_info(NewTree, SubExprs, NewLocalState, _), | |
| 128 | label(NewTree, Label), | |
| 129 | value(NewTree, Value), | |
| 130 | create_long_tree_node(Tree, Children, Label, Type, Value, Expr), | |
| 131 | % print(value(Value)),nl, | |
| 132 | ( is_boolean(NewTree) -> Type = boolean ; Type = nonboolean ), | |
| 133 | maplist(get_tree_from_expr3(State, NewLocalState), SubExprs, Children). | |
| 134 | ||
| 135 | ||
| 136 | ||
| 137 | ||
| 138 | % only one layer | |
| 139 | get_tree_from_expr2(State, LocalState, TExpr, Tree):- | |
| 140 | get_texpr_expr(TExpr, Expr), | |
| 141 | functor(Expr, Op, _), | |
| 142 | x_is_quantifier_like(Op),!, | |
| 143 | x_get_metas(State, LocalState, TExpr, Metas), | |
| 144 | member(value(Value), Metas), | |
| 145 | (create_new_local_state(TExpr, Value, State, LocalState, NewLocalState) -> | |
| 146 | x_get_sub_expressions(TExpr, State, LocalState, Children), | |
| 147 | create_tree_node(Tree, Children, NewLocalState, Metas) | |
| 148 | ; | |
| 149 | create_tree_node(Tree, [], LocalState, Metas) | |
| 150 | ),!. | |
| 151 | get_tree_from_expr2(State, LocalState, TExpr, Tree):- | |
| 152 | x_get_metas(State, LocalState, TExpr, Metas), | |
| 153 | x_get_sub_expressions(TExpr, State, LocalState, Children), | |
| 154 | create_tree_node(Tree, Children, LocalState, Metas),!. | |
| 155 | ||
| 156 | ||
| 157 | ||
| 158 | %% | |
| 159 | % Get all meta information for an expression/predicate | |
| 160 | % | |
| 161 | x_get_metas(State, LocalState, TExpr, Metas):- | |
| 162 | findall(MetaValue, x_get_meta(State, LocalState, TExpr, MetaValue), Metas). | |
| 163 | ||
| 164 | ||
| 165 | %% | |
| 166 | % Helpers, each single meta info. | |
| 167 | % There are value/1, type/1, label/1 and long_desc/1 | |
| 168 | % | |
| 169 | % compute the various attributes of a node: | |
| 170 | x_get_meta(State, LocalState, Expr, value(Value)):- | |
| 171 | x_get_value_of_expr(State, LocalState, Expr, Value). | |
| 172 | x_get_meta(_State, _LocalState, Expr, type(Type)):- | |
| 173 | ( check_if_typed_predicate(Expr) -> | |
| 174 | Type = boolean | |
| 175 | ; | |
| 176 | Type = nonboolean | |
| 177 | ). | |
| 178 | x_get_meta(_State, _LocalState, Expr, label(Label)):- | |
| 179 | once(x_get_label(Expr, Label)). | |
| 180 | x_get_meta(_State, _LocalState, TExpr, long_desc(Expr)):- | |
| 181 | get_texpr_expr(TExpr, Expr). | |
| 182 | x_get_meta(_State, _LocalState, TExpr, rodin_label(Label)):- | |
| 183 | once(get_texpr_label(TExpr,Label)). | |
| 184 | ||
| 185 | ||
| 186 | ||
| 187 | %% | |
| 188 | % Generate a new local state for subexpressions if necessary, like a forall | |
| 189 | % predicate. called for x_is_quantifier/1 predicate. | |
| 190 | % | |
| 191 | ||
| 192 | create_new_local_state(TExpr, Value, State, LocalState, NewLocalState):- | |
| 193 | get_texpr_expr(TExpr, Expr), | |
| 194 | (create_new_local_state2(Expr, Value, State, LocalState, NewLocalState) | |
| 195 | -> true | |
| 196 | ; add_error(bvisual,'Uncovered Expr in create_new_local_state: ',Expr:Value), | |
| 197 | NewLocalState=LocalState). | |
| 198 | ||
| 199 | create_new_local_state2(forall(IDs, LHS, _), true, State, LocalState, NewLocalState) :- !, | |
| 200 | (get_any(IDs, LHS, State, LocalState, NewLocalState) | |
| 201 | -> true /* there is a solution for LHS */ | |
| 202 | ; /* Forall true because no solution for LHS */ | |
| 203 | get_any(IDs, b(truth,pred,[]), State, LocalState, NewLocalState) | |
| 204 | ). | |
| 205 | create_new_local_state2(forall(IDs, LHS, RHS), false,State, LocalState, NewLocalState) :- !, | |
| 206 | safe_create_texpr(negation(RHS), pred, NotRHS), | |
| 207 | conjunct_predicates([LHS, NotRHS], Condition), | |
| 208 | get_any(IDs, Condition, State, LocalState, NewLocalState). | |
| 209 | create_new_local_state2(let_predicate(Ids,AssignmentExprs,Pred), Value, State, LocalState, NewLocalState) :- | |
| 210 | %print(let(Ids,AssignmentExprs,Pred)),nl, | |
| 211 | construct_pred(Ids,AssignmentExprs,Pred,Preds), | |
| 212 | conjunct_predicates(Preds,NewPred), | |
| 213 | EXISTS = exists(Ids,NewPred), % print(exists),nl,translate:print_bexpr(EXISTS),nl, | |
| 214 | create_new_local_state2(EXISTS, Value, State, LocalState, NewLocalState). | |
| 215 | create_new_local_state2(exists(IDs, LHS), true, State, LocalState, NewLocalState) :- !, | |
| 216 | get_any(IDs, LHS, State, LocalState, NewLocalState). | |
| 217 | create_new_local_state2(exists(IDs, LHS), Status, State, LocalState, NewLocalState) :- | |
| 218 | (Status=false ; Status=undefined),!, % for Status=undefined get_any can fail but get_any_most_satisfier should always succeed | |
| 219 | get_any_most_satisfier(IDs, LHS, State, LocalState, NewLocalState). | |
| 220 | create_new_local_state2(X, undefined, State, LocalState, NewLocalState) :- !, | |
| 221 | create_new_local_state2(X, true, State, LocalState, NewLocalState). | |
| 222 | create_new_local_state2(X, x_both_true_and_not_true, State, LocalState, NewLocalState) :- | |
| 223 | %print(x_both_true_and_not_true(X)),nl, % probably means a PROB BUG ! | |
| 224 | (X = forall(_,_,_) -> VAL=false ; VAL=true), | |
| 225 | create_new_local_state2(X, VAL, State, LocalState, NewLocalState). | |
| 226 | create_new_local_state2(comprehension_set(IDs, LHS), Val, State, LocalState, NewLocalState) :- !, | |
| 227 | % format(user_output,'Comprehension set ~w, Val=~w~n~n',[IDs,Val]), | |
| 228 | (is_empty_set_value(Val) -> | |
| 229 | get_any_most_satisfier(IDs, LHS, State, LocalState, NewLocalState) | |
| 230 | ; get_any(IDs, LHS, State, LocalState, NewLocalState)). | |
| 231 | ||
| 232 | % a bit of a hack; it would be better to look at the Prolog version of the value | |
| 233 | is_empty_set_value('{}'). | |
| 234 | is_empty_set_value('[]'). | |
| 235 | is_empty_set_value(X) :- translate:unicode_translation(empty_set,X). | |
| 236 | ||
| 237 | ||
| 238 | construct_pred([],[],Pred,[Pred]). | |
| 239 | construct_pred([ID|T],[EXPR|ET],Pred,[b(equal(ID,EXPR),pred,[])|TR]) :- | |
| 240 | construct_pred(T,ET,Pred,TR). | |
| 241 | ||
| 242 | ||
| 243 | %% | |
| 244 | % Get subexpressions, merge sub expressions with associative operators, like | |
| 245 | % 'and'. For example the predicate and(A,and(B,C)) has three sub expressions: | |
| 246 | % A, B and C. This behaviour is controlled by x_associative_operator/1. | |
| 247 | % | |
| 248 | ||
| 249 | x_get_sub_expressions(TExpr, Children) :- | |
| 250 | x_get_sub_expressions(TExpr, [], [], Children). | |
| 251 | ||
| 252 | x_get_sub_expressions(TExpr, _, _, Children) :- nonvar(TExpr), | |
| 253 | do_not_expand(TExpr), !, | |
| 254 | Children=[]. | |
| 255 | x_get_sub_expressions(TExpr, State, LocalState, Children) :- | |
| 256 | syntaxtraversion(TExpr,Expr,_,_,Children0,_), | |
| 257 | % add custom explanation rules for certain nodes: | |
| 258 | x_get_custom_explanation_subexpressions(Expr,State, LocalState, Children0,Children). | |
| 259 | ||
| 260 | :- use_module(preferences,[get_preference/2]). | |
| 261 | do_not_expand(b(equal(A,B),pred,_)) :- get_preference(pp_propositional_logic_mode,true), | |
| 262 | A = b(identifier(_),boolean,_), % do not expand such nodes | |
| 263 | is_explicit_value(B). | |
| 264 | ||
| 265 | :- use_module(library(lists)). | |
| 266 | % is a value which does not need to be further decomposed | |
| 267 | is_explicit_value(b(Val,_,_)) :- is_explicit_value2(Val). | |
| 268 | is_explicit_value2(integer(_N)). | |
| 269 | is_explicit_value2(string(_S)). | |
| 270 | is_explicit_value2(boolean_true). | |
| 271 | is_explicit_value2(boolean_false). | |
| 272 | is_explicit_value2(identifier(N)) :- b_global_sets:lookup_global_constant(N,_). | |
| 273 | is_explicit_value2(couple(A,B)) :- is_explicit_value(A), is_explicit_value(B). | |
| 274 | is_explicit_value2(value(_)). | |
| 275 | % to do: add further cases | |
| 276 | ||
| 277 | ||
| 278 | b_compute_expression_no_wd(Fun, LocalState, State, FunValue) :- | |
| 279 | temporary_set_preference(disprover_mode,true,CHNG), % avoid WD Errors, we detect WD issues by failure below | |
| 280 | temporary_set_preference(find_abort_values,false,CHNG2), | |
| 281 | (on_exception(E, | |
| 282 | b_compute_expression_nowf(Fun, LocalState, State, FunValue), | |
| 283 | (add_warning(bvisual,'Exception in bvisual while evaluating expression: ',E),fail) | |
| 284 | ) | |
| 285 | -> reset_temporary_preference(disprover_mode,CHNG), | |
| 286 | reset_temporary_preference(find_abort_values,CHNG2) | |
| 287 | ; reset_temporary_preference(disprover_mode,CHNG), | |
| 288 | reset_temporary_preference(find_abort_values,CHNG2), fail). | |
| 289 | ||
| 290 | x_get_custom_explanation_subexpressions(function(Fun,Value),State,LocalState,_C0,Children) :- | |
| 291 | % a custom rule for function application of closures | |
| 292 | % print(function(Fun)),nl, print(value(Value)),nl,print(C0),nl, | |
| 293 | simple_value(Fun), | |
| 294 | b_compute_expression_no_wd(Fun, LocalState, State, FunValue), | |
| 295 | FunValue = closure(P,T,Pred), | |
| 296 | P = [X,_Res], % TO DO: extend to functions with multiple arguments | |
| 297 | closures:is_lambda_closure(P,T,Pred, _OtherIDs,_OtherTypes, DomainPred, Expr),!, | |
| 298 | bsyntaxtree:replace_id_by_expr(Expr,X,Value,NewExpr), | |
| 299 | bsyntaxtree:replace_id_by_expr(DomainPred,X,Value,NewDomainPred), | |
| 300 | Children = [Fun,Value, NewDomainPred,NewExpr]. | |
| 301 | x_get_custom_explanation_subexpressions(Expr,_State,_LocalState, Children0,Children) :- | |
| 302 | x_get_custom_explanation_subexpressions(Expr, Children0,Children). | |
| 303 | ||
| 304 | simple_value(b(V,_,_)) :- simple_value_aux(V). | |
| 305 | simple_value_aux(identifier(_)). | |
| 306 | simple_value_aux(value(_)). | |
| 307 | ||
| 308 | % TO DO: add explanation rules, e.g., f:A --> B ==> f:TA +-> B & dom(f)=A ,... | |
| 309 | x_get_custom_explanation_subexpressions(Expr,_Children0, Children):- | |
| 310 | functor(Expr, Op, _), | |
| 311 | x_operator_with_local_variables(Op),!,Children=[]. | |
| 312 | x_get_custom_explanation_subexpressions(Expr,Children0, Children):- | |
| 313 | functor(Expr, Op, _), Op = set_extension, | |
| 314 | length(Children0,Len), (Len>50 ; maplist(is_explicit_value,Children0)), | |
| 315 | % can be a very large explicit node; no sense in expanding and showing every element | |
| 316 | % print(no_child(Expr)),nl, | |
| 317 | % TO DO: check if simple value | |
| 318 | !,Children=[]. | |
| 319 | x_get_custom_explanation_subexpressions(Expr,Children0, Children):- | |
| 320 | functor(Expr, Op, _), | |
| 321 | x_associative_operator(Op),!, | |
| 322 | maplist(x_collect_exprs_with_op(Op), Children0, Children1), | |
| 323 | scanlist(x_append_reverse, Children1, [], Children). | |
| 324 | x_get_custom_explanation_subexpressions(member(X,b(partial_function(Dom,Range),T,Info)),_,Children) :- | |
| 325 | T=set(set(couple(DomT,RanT))), | |
| 326 | %print(pf(Dom,Range)),nl, | |
| 327 | (\+ bsyntaxtree:is_just_type(Dom) ; \+ bsyntaxtree:is_just_type(Range)), | |
| 328 | nonmember(already_expanded,Info), | |
| 329 | % otherwise we may have an infinite recursion; maybe better to add other operator | |
| 330 | %print(not_type),nl,fail, | |
| 331 | !, | |
| 332 | Children = [A|TB], | |
| 333 | translate:set_type_to_maximal_texpr(DomT,DomType), | |
| 334 | translate:set_type_to_maximal_texpr(RanT,RanType), | |
| 335 | A = b(member(X,b(partial_function(DomType,RanType),T,[already_expanded|Info])),pred,[]), | |
| 336 | add_subset_check(b(domain(X),set(DomT),[]), Dom, TB,TC), | |
| 337 | add_subset_check(b(range(X),set(RanT),[]), Range, TC,[]), | |
| 338 | TB \= [],!. | |
| 339 | x_get_custom_explanation_subexpressions(member(X,b(total_function(Dom,Range),T,Info)),_,Children) :- | |
| 340 | T=set(set(couple(DomT,RanT))), !, | |
| 341 | Children = [A,B|TC], | |
| 342 | %print(total_fun_check(DomT,RanT)),nl, | |
| 343 | translate:set_type_to_maximal_texpr(DomT,DomType), | |
| 344 | translate:set_type_to_maximal_texpr(RanT,RanType), | |
| 345 | A = b(member(X,b(partial_function(DomType,RanType),T,Info)),pred,[]), | |
| 346 | B = b(equal(b(domain(X),set(DomT),[]), Dom),pred,[]), | |
| 347 | add_subset_check(b(range(X),set(RanT),[]), Range, TC,[]). | |
| 348 | x_get_custom_explanation_subexpressions(member(X,b(total_surjection(Dom,Range),T,Info)),_,Children) :- | |
| 349 | T=set(set(couple(DomT,RanT))), !, | |
| 350 | Children = [A,B,C], | |
| 351 | translate:set_type_to_maximal_texpr(DomT,DomType), | |
| 352 | translate:set_type_to_maximal_texpr(RanT,RanType), | |
| 353 | A = b(member(X,b(partial_function(DomType,RanType),T,Info)),pred,[]), | |
| 354 | B = b(equal(b(domain(X),set(DomT),[]), Dom),pred,[]), | |
| 355 | C = b(equal(b(range(X),set(RanT),[]), Range),pred,[]). | |
| 356 | x_get_custom_explanation_subexpressions(member(X,b(partial_surjection(Dom,Range),T,Info)),_,Children) :- | |
| 357 | T=set(set(couple(DomT,RanT))), !, | |
| 358 | Children = [A|TB], | |
| 359 | translate:set_type_to_maximal_texpr(DomT,DomType), | |
| 360 | translate:set_type_to_maximal_texpr(RanT,RanType), | |
| 361 | A = b(member(X,b(partial_function(DomType,RanType),T,Info)),pred,[]), | |
| 362 | add_subset_check(b(domain(X),set(DomT),[]), Dom, TB,[C]), | |
| 363 | C = b(equal(b(range(X),set(RanT),[]), Range),pred,[]). | |
| 364 | x_get_custom_explanation_subexpressions(_Expr,Children, Children). % :- filter_children(Children,Res). | |
| 365 | ||
| 366 | ||
| 367 | %filter_children([],[]). | |
| 368 | %filter_children([H|T],Res) :- (not_interesting(H) -> Res=R ; Res=[H|R]), filter_children(T,R). | |
| 369 | %not_interesting(b(integer(_),integer,_)). | |
| 370 | ||
| 371 | ||
| 372 | add_subset_check(LHS,RHS,Result,EndOfList) :- | |
| 373 | % add subset check, unless "obvious" | |
| 374 | (bsyntaxtree:is_just_type(RHS) -> Result=EndOfList | |
| 375 | ; Result = [b(subset(LHS, RHS),pred,[])|EndOfList] | |
| 376 | ). | |
| 377 | ||
| 378 | x_collect_exprs_with_op(Op, TExpr, Children):- | |
| 379 | syntaxtraversion(TExpr,Expr,_,_,_,_), | |
| 380 | ( functor(Expr, Op, _) -> | |
| 381 | x_get_sub_expressions(TExpr, Children); | |
| 382 | Children = [TExpr] | |
| 383 | ). | |
| 384 | ||
| 385 | x_append_reverse(X,Y,L):- append(Y,X,L). | |
| 386 | ||
| 387 | ||
| 388 | ||
| 389 | %% | |
| 390 | % Get label for an expression | |
| 391 | % | |
| 392 | ||
| 393 | x_get_label(TExpr, Label):- get_texpr_expr(TExpr,Expr), | |
| 394 | x_get_label_aux(Expr,Label). | |
| 395 | x_get_label_aux(value(V), Label) :- !, get_value_label(V,Label). | |
| 396 | x_get_label_aux(Expr, Label) :- | |
| 397 | %Expr =.. [Op, Label], | |
| 398 | functor(Expr,Op,1), arg(1,Expr,Label), | |
| 399 | x_literal_value_operator(Op). | |
| 400 | x_get_label_aux(Expr, Label):- | |
| 401 | functor(Expr, Fkt, _), | |
| 402 | x_functor_to_label(Fkt, Label). | |
| 403 | ||
| 404 | get_value_label(V,Label) :- var(V),!, Label='VAR-VALUE'. | |
| 405 | %get_value_label(global_set(GS),Label) :- !, Label=GS. % should we pretty print the value | |
| 406 | %get_value_label(V,stored_value(F)) :- functor(V,F,_N). | |
| 407 | get_value_label(V,Label) :- translate_bvalue_with_limit(V,40,Label). | |
| 408 | %% | |
| 409 | % Helpers | |
| 410 | % | |
| 411 | ||
| 412 | %% | |
| 413 | % Maps functor of prolog term to correct label | |
| 414 | % | |
| 415 | :- use_module(translate,[translate_prolog_constructor_in_mode/2]). | |
| 416 | x_functor_to_label(F,R) :- translate_prolog_constructor_in_mode(F,PPVersion), !, R=PPVersion. | |
| 417 | %x_functor_to_label(conjunct, conjunction):-!. | |
| 418 | %x_functor_to_label(disjunct, disjunction):-!. | |
| 419 | x_functor_to_label(function, R):-!, R='func.applic.'. | |
| 420 | x_functor_to_label(X, X). | |
| 421 | ||
| 422 | %% | |
| 423 | % List of operators which may generate a new local state, | |
| 424 | % like a forall predicate. | |
| 425 | % | |
| 426 | x_is_quantifier_like(comprehension_set). | |
| 427 | x_is_quantifier_like(X) :- x_is_quantifier(X). | |
| 428 | ||
| 429 | x_is_quantifier(forall). | |
| 430 | x_is_quantifier(exists). | |
| 431 | x_is_quantifier(let_predicate). | |
| 432 | ||
| 433 | %% | |
| 434 | % List of associative operators | |
| 435 | % | |
| 436 | ||
| 437 | x_associative_operator(conjunct). | |
| 438 | x_associative_operator(disjunct). | |
| 439 | x_associative_operator(add). | |
| 440 | x_associative_operator(mul). | |
| 441 | ||
| 442 | ||
| 443 | %% | |
| 444 | % List of operators with local variables | |
| 445 | % | |
| 446 | ||
| 447 | % x_operator_with_local_variables(comprehension_set). is now supported in create_new_local_state2 | |
| 448 | x_operator_with_local_variables(lambda). | |
| 449 | x_operator_with_local_variables(general_sum). | |
| 450 | x_operator_with_local_variables(general_product). | |
| 451 | x_operator_with_local_variables(quantified_union). | |
| 452 | x_operator_with_local_variables(quantified_intersection). | |
| 453 | x_operator_with_local_variables(lazy_let_expr). | |
| 454 | x_operator_with_local_variables(lazy_let_pred). | |
| 455 | x_operator_with_local_variables(lazy_let_subst). | |
| 456 | ||
| 457 | ||
| 458 | %% | |
| 459 | % List of literal values | |
| 460 | % | |
| 461 | x_literal_value_operator(identifier). | |
| 462 | x_literal_value_operator(value). | |
| 463 | x_literal_value_operator(integer). | |
| 464 | x_literal_value_operator(string). | |
| 465 | ||
| 466 | ||
| 467 | ||
| 468 | %% | |
| 469 | % Evaluate predicate or expression ... at least it tries XD | |
| 470 | % Expressions return value is translated by pretty printer. | |
| 471 | % Value is unknown if Expr is neither a predicate or expression. | |
| 472 | % | |
| 473 | ||
| 474 | %% | |
| 475 | % Evaluate the predicate Expr in LocaleState and State. | |
| 476 | % It does check for consistency by checking Expr == !!Expr. | |
| 477 | % Thus it yields in addition to true and false also | |
| 478 | % x_both_true_and_not_true and undefined | |
| 479 | % as flag signaling internal errors. | |
| 480 | ||
| 481 | :- use_module(preferences,[temporary_set_preference/3,reset_temporary_preference/2]). | |
| 482 | ||
| 483 | x_get_value_of_expr(State, LocalState, Expr, Value):- | |
| 484 | check_if_typed_predicate(Expr),!, | |
| 485 | temporary_set_preference(disprover_mode,false,CHNG), % avoid WD Errors, we detect WD issues by failure below | |
| 486 | temporary_set_preference(find_abort_values,false,CHNG2), | |
| 487 | % print('Test: '),translate:print_bexpr(Expr),nl, | |
| 488 | get_bool_expr_value(Expr,LocalState,State,Value), | |
| 489 | reset_temporary_preference(disprover_mode,CHNG), | |
| 490 | reset_temporary_preference(find_abort_values,CHNG2), | |
| 491 | clear_wd_errors. % ,print('Value: '), print(Value),nl. | |
| 492 | x_get_value_of_expr(State, LocalState, Expr, Value):- | |
| 493 | check_if_typed_expression(Expr),!, | |
| 494 | % print('Eval: '),translate:print_bexpr(Expr),nl, | |
| 495 | (b_compute_expression_no_wd(Expr, LocalState, State, Value0) | |
| 496 | -> max_chars_total(MaxT), | |
| 497 | translate_bvalue_with_limit(Value0, MaxT, Value) % we show maximally 10 lines a 40 chars | |
| 498 | ; Value = unknown). | |
| 499 | x_get_value_of_expr(_State, _LocalState, _Expr, unknown):-!. | |
| 500 | ||
| 501 | % (error(representation_error(max_clpfd_integer) | |
| 502 | ||
| 503 | get_bool_expr_value(Expr,LocalState,State,Value) :- | |
| 504 | on_exception(E,call(get_bool_expr_val2(Expr,LocalState,State,Value)), | |
| 505 | (add_warning(bvisual,'Exception in bvisual while evaluating predicate: ',E),Value=undefined)). | |
| 506 | get_bool_expr_val2(Expr,LocalState,State,Value) :- | |
| 507 | ( b_test_boolean_expression_wf(Expr,LocalState,State) -> | |
| 508 | ( b_not_test_boolean_expression_wf(Expr,LocalState,State) | |
| 509 | -> Value = x_both_true_and_not_true, % was x_unknown_true_and_not_true | |
| 510 | % we should add an error message here | |
| 511 | % this should never happen | |
| 512 | print('### Error, x_both_true_and_not_true: '), print(Expr),nl | |
| 513 | ; Value = true | |
| 514 | ) | |
| 515 | ; b_not_test_boolean_expression_wf(Expr,LocalState,State) -> | |
| 516 | Value = false | |
| 517 | %, print(value_false),nl | |
| 518 | ; otherwise -> | |
| 519 | Value = undefined % was x_undefined_false_and_not_false | |
| 520 | %, print(value_undefined),nl | |
| 521 | ). | |
| 522 | ||
| 523 | ||
| 524 | ||
| 525 | %% | |
| 526 | % Try to execute an 'Any' statement on LocalState and State. | |
| 527 | % New state with the values is returned by NewLocalState. | |
| 528 | % Compare to b_interpreter:b_execute_statement2(any(Parameters,PreCond,Body),...) | |
| 529 | % | |
| 530 | ||
| 531 | :- use_module(b_enumerate, [b_tighter_enumerate_values/2]). | |
| 532 | :- use_module(b_interpreter, [set_up_typed_localstate/6]). | |
| 533 | ||
| 534 | ||
| 535 | get_any(IDs, Condition, State, LocalState, NewLocalState) :- | |
| 536 | on_exception(E,call(get_any2(IDs, Condition, State, LocalState, NewLocalState)), | |
| 537 | (add_warning(bvisual,'Exception in bvisual while treating quantfier predicate: ',E),fail)). | |
| 538 | get_any2(IDs, Condition, State, LocalState, NewLocalState) :- | |
| 539 | set_up_typed_localstate(IDs, _FreshVars, TypedVals, LocalState, NewLocalState,positive), | |
| 540 | init_wait_flags(WF), | |
| 541 | b_interpreter:b_test_boolean_expression(Condition,NewLocalState, State, WF), /* check WHERE */ | |
| 542 | b_tighter_enumerate_values(TypedVals,WF), | |
| 543 | ground_wait_flags(WF). | |
| 544 | ||
| 545 | ||
| 546 | get_any_most_satisfier(IDs, Condition, State, LocalState, NewLocalState):- | |
| 547 | ( any_maxsolver(IDs, Condition, State, LocalState, NewLocalState) -> | |
| 548 | true; | |
| 549 | conjunct_predicates([], Truth), | |
| 550 | get_any(IDs, Truth, State, LocalState, NewLocalState) | |
| 551 | ). | |
| 552 | ||
| 553 | ||
| 554 | ||
| 555 | ||
| 556 | ||
| 557 | ||
| 558 | %% | |
| 559 | % Main predicate for writing dot graph | |
| 560 | % Use it to start. | |
| 561 | % | |
| 562 | % FileSpec is used by tell/1 to open a stream. | |
| 563 | % The graph is printed by print_dot_graph_for_tree/1. | |
| 564 | % | |
| 565 | ||
| 566 | :- use_module(tools,[catch_call/1]). | |
| 567 | ||
| 568 | write_dot_graph_to_file(Tree, FileSpec) :- | |
| 569 | catch_call(bvisual:write_dot_graph_to_file_aux(Tree, FileSpec)). | |
| 570 | write_dot_graph_to_file_aux(Tree, FileSpec) :- | |
| 571 | (get_preference(dot_use_unicode,true) -> translate:set_unicode_mode ; true), | |
| 572 | tell(FileSpec), | |
| 573 | call_cleanup(print_dot_graph(Tree), | |
| 574 | (told,(get_preference(dot_use_unicode,true) -> translate:unset_unicode_mode ; true))). | |
| 575 | ||
| 576 | print_dot_graph(Tree):- | |
| 577 | print('digraph g {'), nl, | |
| 578 | print('rankdir=RL;'), nl, | |
| 579 | visit_tree(x_print_dot_graph_visitor, child_nodes, Tree, [],_), | |
| 580 | print('}'), | |
| 581 | nl. | |
| 582 | ||
| 583 | ||
| 584 | %% | |
| 585 | % Helpers | |
| 586 | % | |
| 587 | :- public x_print_dot_graph_visitor/5. | |
| 588 | x_print_dot_graph_visitor(enter, Node, _Children, [], [1,root]) :- | |
| 589 | x_print_dot_graph_node_only(Node, root),!. | |
| 590 | x_print_dot_graph_visitor(enter, Node, _Children, In, [NewID|In]):- | |
| 591 | x_print_dot_graph_visitor(Node, In, [NewID|_]). | |
| 592 | x_print_dot_graph_visitor(leave, _Node, _Children, [NewID,_ID|Out], [NewID|Out]). | |
| 593 | ||
| 594 | /* for 3 args : */ | |
| 595 | x_print_dot_graph_visitor(Node, [], []):- | |
| 596 | x_print_dot_graph_node_only(Node, root), | |
| 597 | !. | |
| 598 | ||
| 599 | x_print_dot_graph_visitor(Node, [ID|Rest], [NewID|Rest]):- | |
| 600 | Rest = [PID|_], | |
| 601 | NewID is ID + 1, | |
| 602 | x_print_dot_graph_node_only(Node, ID), | |
| 603 | format('~8|Node~p -> Node~p;~N', [ID, PID]), | |
| 604 | !. | |
| 605 | ||
| 606 | ||
| 607 | ||
| 608 | ||
| 609 | shorten_atom(MaxLengthPerLine, Atom, NewAtom) :- | |
| 610 | max_lines(MaxLines), | |
| 611 | shorten_atom(MaxLengthPerLine, Atom, NewAtom,MaxLines). | |
| 612 | shorten_atom(MaxLengthPerLine, Atom, NewAtom,MaxLines) :- | |
| 613 | ( atom(Atom) -> | |
| 614 | atom_chars(Atom, AtomChars), | |
| 615 | shorten_atom_list(MaxLengthPerLine, AtomChars, NewAtom,MaxLines) | |
| 616 | ; | |
| 617 | NewAtom = Atom | |
| 618 | ). | |
| 619 | ||
| 620 | shorten_atom_list(MaxLengthPerLine, Chars, Atom,MaxLines):- | |
| 621 | %length(Chars, Length), | |
| 622 | split_chars(Chars,MaxLengthPerLine, Prefix,Suffix), | |
| 623 | ( Suffix=[] -> | |
| 624 | atom_chars(Atom, Chars) | |
| 625 | ; | |
| 626 | %lists:append_length(Prefix, Suffix, Chars, MaxLengthPerLine), | |
| 627 | %print( split_chars(Chars,MaxLengthPerLine, Prefix,Suffix) ),nl, | |
| 628 | (MaxLines>1 -> ML1 is MaxLines-1, | |
| 629 | shorten_atom_list(MaxLengthPerLine, Suffix, SuffixAtom,ML1) | |
| 630 | ; SuffixAtom = '...'), | |
| 631 | atom_chars(PrefixAtom, Prefix), | |
| 632 | atom_concat(PrefixAtom, '\\n', PrefixAtomNewLine), | |
| 633 | atom_concat(PrefixAtomNewLine, SuffixAtom, Atom) | |
| 634 | ). | |
| 635 | ||
| 636 | % bvisual:split_chars([a,b,d,e,f],2,P,S), P==[a,b], S==[d,e,f] | |
| 637 | ||
| 638 | % a predicate to split List if it is longer than MaxLen, but only outside of single and double quotes | |
| 639 | % List is suppoed to be already encoded using string_escape | |
| 640 | split_chars(List,MaxLen,Prefix,Suffix) :- | |
| 641 | split_chars(List,MaxLen,Prefix,Suffix,q(outside,outside)). | |
| 642 | ||
| 643 | split_chars(List,MaxL,R,Suffix,Q) :- MaxL < 1, Q=q(outside,outside), !, | |
| 644 | % only add newline if we are outside of quotes | |
| 645 | R=[], Suffix=List. | |
| 646 | split_chars([],_MaxL,[],[],_). | |
| 647 | split_chars(L,MaxL,LR,LeftOver,Q) :- | |
| 648 | is_a_unit(L,T,LR,TR),!, | |
| 649 | M1 is MaxL-1, split_chars(T,M1,TR,LeftOver,Q). | |
| 650 | split_chars([Slash,Quote|T],MaxL,[Slash,Quote|TR],LeftOver,Q) :- Slash = ('\\'), | |
| 651 | !, %(Quote=34;Quote=39), !, % \" or \' | |
| 652 | toggle_quotes(Quote,Q,TQ), | |
| 653 | M1 is MaxL-1, split_chars(T,M1,TR,LeftOver,TQ). | |
| 654 | split_chars([H|T],MaxL,[H|TR],LeftOver,Q) :- | |
| 655 | M1 is MaxL-1, split_chars(T,M1,TR,LeftOver,Q). | |
| 656 | ||
| 657 | toggle_quotes('\'',q(outside,Q2),q(inside,Q2)) :- !. | |
| 658 | toggle_quotes('\'',q(inside,Q2),q(outside,Q2)) :- !. | |
| 659 | toggle_quotes('\"',q(Q1,outside),q(Q1,inside)) :- !. | |
| 660 | toggle_quotes('\"',q(Q1,inside),q(Q1,outside)) :- !. | |
| 661 | toggle_quotes(_,Q,Q). | |
| 662 | ||
| 663 | % check for HTML encodings like à Ë α ... | |
| 664 | % these should be counted as a single character and not be split | |
| 665 | is_a_unit(['&'|T1],T,['&'|T1R],TR) :- get_lexeme(T1,10,LexUnit,T), | |
| 666 | append(LexUnit,TR,T1R). | |
| 667 | ||
| 668 | get_lexeme([';'|T],_,[';'],TRes) :- !, TRes=T. | |
| 669 | get_lexeme([H|T],L,[H|LexT],TRes) :- L>1, L1 is L-1, get_lexeme(T,L1,LexT,TRes). | |
| 670 | ||
| 671 | get_long_label(Node,MaxPerLine,Pretty1h) :- | |
| 672 | long_desc(Node, LongDesc), | |
| 673 | %tools:print_wtime(start_translate(ID)), | |
| 674 | translate_bexpression_with_limit(LongDesc, 250, Pretty0), | |
| 675 | %tools:print_wtime(translated(ID)), | |
| 676 | string_escape(Pretty0, Pretty1), | |
| 677 | shorten_atom(MaxPerLine, Pretty1, Pretty1h). % maximally 10 lines with 40 chars | |
| 678 | ||
| 679 | :- use_module(tools,[string_escape/2]). | |
| 680 | x_print_dot_graph_node_only(Node, ID) :- %tools:print_wtime(node(ID,Node)), | |
| 681 | label(Node, Label0), | |
| 682 | max_chars_per_line(MaxPerLine), | |
| 683 | string_escape(Label0, Label1), %tools:print_wtime(escaped(ID)), | |
| 684 | ( ID \= root, is_boolean(Node) | |
| 685 | -> | |
| 686 | Label=Label1, | |
| 687 | get_long_label(Node,MaxPerLine,Pretty1h), | |
| 688 | value(Node, TruthValue), | |
| 689 | string_escape(TruthValue, TVEsc), | |
| 690 | get_predicate_field_seperator(Sep), | |
| 691 | atom_concat(TVEsc, Sep, Pretty4), | |
| 692 | atom_concat(Pretty4, Pretty1h, Pretty) | |
| 693 | ; | |
| 694 | value(Node, Val), | |
| 695 | string_escape(Val, Pretty1), % TO DO: check that we also escape | in case of records! | |
| 696 | (is_boolean(Node) -> get_predicate_field_seperator(Sep) | |
| 697 | ; get_expression_field_seperator(Sep)), | |
| 698 | ((Pretty1=Label1 ; is_explicit_value_node(Node)) | |
| 699 | -> Pretty='', Label=Pretty1 % we have a simple value node like integer(1),... | |
| 700 | ; has_no_children(Node) | |
| 701 | -> get_long_label(Node,MaxPerLine,Label), | |
| 702 | shorten_atom(MaxPerLine, Pretty1, Pretty) | |
| 703 | ; Label=Label1, | |
| 704 | shorten_atom(MaxPerLine, Pretty1, Pretty) | |
| 705 | ) | |
| 706 | ), | |
| 707 | %tools:print_wtime(node_style(ID)), | |
| 708 | x_print_dot_graph_node_style(Node, Shape, Color,Style), | |
| 709 | %tools:print_wtime(printing(ID)), | |
| 710 | (Pretty='' | |
| 711 | -> format('~4|Node~p [label="~p", shape="~p", fillcolor="~p", style="~p"]~N', [ID, Label, Shape, Color,Style]) | |
| 712 | ; format('~4|Node~p [label="~p~p~p", shape="~p", fillcolor="~p", style="~p"]~N', [ID, Label, Sep, Pretty, Shape, Color,Style])). % ,tools:print_wtime(finished(ID)). | |
| 713 | ||
| 714 | ||
| 715 | x_print_dot_graph_node_style(Node, Shape, 'tomato','filled,rounded') :- | |
| 716 | is_boolean(Node), value(Node, false),!, boolean_shape(Shape). | |
| 717 | x_print_dot_graph_node_style(Node, Shape, 'olivedrab2','filled,rounded') :- | |
| 718 | is_boolean(Node), value(Node, true),!, boolean_shape(Shape). | |
| 719 | x_print_dot_graph_node_style(Node, Shape, 'orange','filled,rounded') :- % styles could be dashed,dotted, rounded, ... | |
| 720 | is_boolean(Node),!, boolean_shape(Shape). | |
| 721 | x_print_dot_graph_node_style(Node, Shape, 'yellow','filled') :- | |
| 722 | value(Node, unknown),!, get_preference(dot_expression_node_shape,Shape). | |
| 723 | x_print_dot_graph_node_style(_, Shape, 'white',filled) :- | |
| 724 | get_preference(dot_expression_node_shape,Shape). | |
| 725 | ||
| 726 | ||
| 727 | boolean_shape(Shape) :- get_preference(dot_predicate_node_shape,Shape). % ellipse, oval, record TO DO: other form for quantifiers | |
| 728 | ||
| 729 | % if we use a Dot record, we can use | to separate fields | |
| 730 | get_predicate_field_seperator('|') :- get_preference(dot_predicate_node_shape,record). | |
| 731 | get_predicate_field_seperator('\\n'). | |
| 732 | get_expression_field_seperator('|') :- get_preference(dot_expression_node_shape,record). | |
| 733 | get_expression_field_seperator('\\n'). | |
| 734 | ||
| 735 | :- use_module(bmachine, [ | |
| 736 | b_get_properties_from_machine/1, | |
| 737 | b_get_machine_constants/1, | |
| 738 | b_machine_has_constants_or_properties/0 | |
| 739 | ]). | |
| 740 | ||
| 741 | :- use_module(predicate_debugger). | |
| 742 | ||
| 743 | x_create_exists(IDs, Condition, Exists):- | |
| 744 | %print(x_create_exists(IDs,Condition)),nl, | |
| 745 | get_texpr_expr(Condition,exists(InnerVars,InnerCond)),!, | |
| 746 | % fuse two exists together | |
| 747 | append(IDs,InnerVars,Vars), | |
| 748 | x_create_exists(Vars,InnerCond,Exists). | |
| 749 | x_create_exists(IDs, Condition, Exists):- | |
| 750 | create_exists(IDs,Condition,Exists). | |
| 751 | ||
| 752 | ||
| 753 | ||
| 754 | get_properties(BExpr,CreateExists):- | |
| 755 | b_get_properties_from_machine(Condition), | |
| 756 | ( (CreateExists=true,b_machine_has_constants_or_properties) -> | |
| 757 | b_get_machine_constants(IDs), | |
| 758 | x_create_exists(IDs, Condition, BExpr) | |
| 759 | ; | |
| 760 | BExpr = Condition | |
| 761 | ). | |
| 762 | ||
| 763 | ||
| 764 | get_operation_pre(OpName, BExpr, BecomeSuchVars):- | |
| 765 | predicate_debugger:get_operation_enabling_condition(OpName, IDs, Condition,BecomeSuchVars,_Precise,true,false), | |
| 766 | ( IDs = [] -> | |
| 767 | BExpr = Condition; | |
| 768 | x_create_exists(IDs, Condition, BExpr) | |
| 769 | ). | |
| 770 | ||
| 771 | ||
| 772 | ||
| 773 | ||
| 774 | %% | |
| 775 | % Hierarchical Visitor Pattern for "trees" | |
| 776 | % used to be in gtree module | |
| 777 | % | |
| 778 | % For this implementation a tree is a (root) node and a functor, which | |
| 779 | % maps a node to it's child nodes. For example a Prolog term can be | |
| 780 | % understand as a tree by the functor: | |
| 781 | % children_fkt(Term, Subterms):- Term=..[_|Subterms]. | |
| 782 | % | |
| 783 | % Important: Do not use trees with cycles. This implementation will not | |
| 784 | % detect them and will not terminate. | |
| 785 | % | |
| 786 | % The indented calling is: | |
| 787 | % visit_tree(+VisitorFkt, +ChildrenFkt, +Node, +EnvIn, -EnvOut) | |
| 788 | % | |
| 789 | % If no functor is specified, the former mentioned one is used. | |
| 790 | % EnvIn and EnvOut are Variables for intermediate values or states, | |
| 791 | % which you might need to maintain between calls to VisitorFkt. You | |
| 792 | % might omit them, if you do not need them. | |
| 793 | % | |
| 794 | % During the visiting process the VisitorFkt functor is called for each | |
| 795 | % node starting with the "root". Calls are made in following order: | |
| 796 | % - VisitorFkt(Node, EnvIn, EnvOut), if Node is a leaf, | |
| 797 | % i.e. ChildrenFkt(Node, []). | |
| 798 | % - VisitorFkt(enter, Node, Children, EnvIn, EnvOut), before branching, | |
| 799 | % - VisitorFkt(leave, Node, Children, EnvIn, EnvOut), after branching | |
| 800 | % to Node's child nodes. | |
| 801 | % !- Only if VisitorFkt(enter, ...) succeeds, child nodes will be | |
| 802 | % visited and VisitorFkt(leave, ...) will be called. | |
| 803 | % | |
| 804 | ||
| 805 | :- use_module(library(lists), [scanlist/4, maplist/2]). | |
| 806 | ||
| 807 | ||
| 808 | visit_tree(VisitorFkt, ChildrenFkt, Node, EnvIn, EnvOut):- | |
| 809 | call(ChildrenFkt, Node, Children), | |
| 810 | ( Children == [] -> | |
| 811 | call(VisitorFkt, Node, EnvIn, EnvOut) | |
| 812 | ; | |
| 813 | ( call(VisitorFkt, enter, Node, Children, EnvIn, Env1) -> | |
| 814 | scanlist(visit_tree(VisitorFkt, ChildrenFkt), Children, Env1, Env2), | |
| 815 | call(VisitorFkt, leave, Node, Children, Env2, EnvOut) | |
| 816 | ; | |
| 817 | EnvOut = EnvIn | |
| 818 | ) | |
| 819 | ), | |
| 820 | !. | |
| 821 | ||
| 822 | ||
| 823 | ||
| 824 | %% | |
| 825 | % Default ChildrenFkt | |
| 826 | % | |
| 827 | %:- public x_default_children_fkt/2. | |
| 828 | %x_default_children_fkt(Node, Children):- | |
| 829 | % Node =.. [_|Children]. | |
| 830 | ||
| 831 | ||
| 832 | ||
| 833 |