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