1/* Part of LogicMOO Base Logicmoo Debug Tools
    2% ===================================================================
    3%   File   : mpred_why.pl
    4%   Author : Tim Finin, finin@prc.unisys.com
    5%   Updated:
    6%   Purpose: predicates for interactively exploring Pfc justifications.
    7
    8% ***** predicates for brousing justifications *****
    9% ===================================================================
   10*/
   11
   12%:- if(( ( \+ ((current_prolog_flag(logicmoo_include,Call),Call))) )).
   13
   14%:- throw(module(pfcumt,[umt/1])).
   15
   16:- module(mpred_justify, []).   17
   18%:- use_module(mpred_kb_ops).
   19%:- use_module(library(util_varnames)).
   20%:- use_module(library(no_repeats)).
   21
   22:- include('mpred_header.pi').   23
   24%:- endif.
   25
   26%   File   : pfcjust.pl
   27%   Author : Tim Finin, finin@prc.unisys.com
   28%   Author :  Dave Matuszek, dave@prc.unisys.com
   29%   Updated:
   30%   Purpose: predicates for accessing Pfc justifications.
   31%   Status: more or less working.
   32%   Bugs:
   33
   34%  *** predicates for exploring supports of a fact *****
   35
   36justification(F,J):- supporters_list(F,J).
   37
   38justifications(F,Js):- bagof_nr(J,justification(F,J),Js).
   39
   40mpred_why(M:Conseq,Ante):- atom(M),!,M:mpred_why_2(Conseq,Ante).
   41mpred_why(Conseq,Ante):- mpred_why_2(Conseq,Ante).
   42
   43mpred_why_2(Conseq,Ante):- var(Conseq),!,mpred_children(Ante,Conseq).
   44mpred_why_2(Conseq,Ante):- justifications(Conseq,Ante).
   45
   46
   47
   48mpred_info(O):-
   49 with_output_to(user_error,
   50 ((dmsg("======================================================================="),
   51  listing(O),
   52  dmsg("======================================================================="),
   53  quietly(call_with_inference_limit(ignore(on_xf_cont(deterministically_must(mpred_why_1(O)))),4000,_)),
   54  dmsg("======================================================================="),
   55  maplist(mp_printAll(O),
   56  [   mpred_db_type(O,v),  
   57      +(mpred_child(O,v)),
   58      % mpred_fact(O),
   59      mpred_axiom(O),
   60      well_founded(O),
   61      mpred_supported(local,O),
   62      mpred_supported(cycles,O),
   63      mpred_assumption(O),
   64      get_mpred_is_tracing(O)]),
   65 dmsg("=======================================================================")))).
   66
   67mp_printAll(S,+(O)):- subst(O,v,V,CALL),CALL\==O,!,
   68  subst(O,S,s,NAME),safe_functor(O,F,_),!,
   69  nl,flush_output, fmt("=================="),wdmsg(NAME),wdmsg("---"),flush_output,!,
   70  doall(((flush_output,(CALL),flush_output)*->fmt9(V);(fail=F))),nl,fmt("=================="),nl,flush_output.
   71mp_printAll(S,call(O)):- !,
   72  subst(O,S,s,NAME),
   73  nl,flush_output,fmt("=================="),wdmsg(NAME),wdmsg("---"),flush_output,!,
   74  doall(((flush_output,deterministically_must(O),flush_output)*->true;wdmsg(false=NAME))),fmt("=================="),nl,flush_output.
   75mp_printAll(S,(O)):- subst(O,v,V,CALL),CALL\==O,!,
   76  subst(O,S,s,NAME),safe_functor(O,F,_),
   77  nl,flush_output, fmt("=================="),wdmsg(NAME),wdmsg("---"),flush_output,!,
   78  doall(((flush_output,deterministically_must(CALL),flush_output)*->fmt9(V);(fail=F))),nl,fmt("=================="),nl,flush_output.
   79mp_printAll(S,(O)):-  !,  safe_functor(O,F,A),mp_nnvv(S,O,F,A),flush_output.
   80mp_nnvv(_,(O),F,1):- !, doall(((flush_output,deterministically_must(O),flush_output)*->wdmsg(+F);wdmsg(-F))).
   81mp_nnvv(S,(O),_,_):- !, subst(O,S,s,NAME), !,
   82  doall(((flush_output,deterministically_must(O),flush_output)*->wdmsg(-NAME);wdmsg(+NAME))).
 mpred_basis_list(+P, -L)
is true iff L is a list of "base" facts which, taken together, allows us to deduce P. A mpred "based on" list fact is an axiom (a fact added by the user or a raw Prolog fact (i.e. one w/o any support)) or an assumption.
   96mpred_basis_list(F,[F]):- (mpred_axiom(F) ; mpred_assumption(F)),!.
   97
   98mpred_basis_list(F,L):-
   99  % i.e. (reduce 'append (map 'mpred_basis_list (justification f)))
  100  justification(F,Js),
  101  bases_union(Js,L).
 bases_union(+L1, +L2)
is true if list L2 represents the union of all of the facts on which some conclusion in list L1 is based.
  109bases_union([],[]).
  110bases_union([X|Rest],L):-
  111  mpred_basis_list(X,Bx),
  112  bases_union(Rest,Br),
  113  mpred_union(Bx,Br,L).
  114
  115%mpred_axiom(F):- !, % Like OLD TODO
  116%  mpred_get_support(F,(_,ax)).
  117mpred_axiom(F):-
  118  mpred_get_support(F,UU),
  119  is_user_reason(UU),!.
 mpred_assumption(P)
an mpred_assumption is a failed goal, i.e. were assuming that our failure to prove P is a proof of not(P)
  126mpred_assumption(P):- !, % Like OLD TODO
  127  nonvar(P), mpred_unnegate(P,_).
  128mpred_assumption(P):- nonvar(P), 
  129  mpred_unnegate(P,N), 
  130 % fail,
  131  % added prohibited_check
  132  (current_prolog_flag(explicitly_prohibited_check,false) -> true ; \+ mpred_axiom(~ N)).
  133
  134
  135:- set_prolog_flag(explicitly_prohibited_check,false).
 mpred_assumptions(+X, +AsSet) is semidet
true if AsSet is a set of assumptions which underly X.
  141mpred_assumptions(X,[X]):- mpred_assumption(X).
  142mpred_assumptions(X,[]):- mpred_axiom(X).
  143mpred_assumptions(X,L):-
  144  justification(X,Js),
  145  do_assumpts(Js,L).
 do_assumpts(+Set1, ?Set2) is semidet
Assumptions Secondary Helper.
  152do_assumpts([],[]).
  153do_assumpts([X|Rest],L):-
  154  mpred_assumptions(X,Bx),
  155  do_assumpts(Rest,Br),
  156  mpred_union(Bx,Br,L).
  157
  158
  159%  mpred_proofTree(P,T) the proof tree for P is T where a proof tree is
  160%  of the form
  161%
  162%      [P , J1, J2, ;;; Jn]         each Ji is an independent P justifier.
  163%           ^                         and has the form of
  164%           [J11, J12,... J1n]      a list of proof trees.
 mpred_child(+P, ?Q) is semidet
is true iff P is an immediate justifier for Q.
  171mpred_child(P,Q):- is_list(P),!,maplist(mpred_child,P,Q).
  172mpred_child(P,Q):-
  173  mpred_get_support(Q,(P,_)).
  174mpred_child(P,Q):-
  175  mpred_get_support(Q,(_,Trig)),
  176  mpred_db_type(Trig,trigger(_TT)),
  177  mpred_child(P,Trig).
 mpred_children(+P, ?L) is semidet
PFC Children.
  184mpred_children(P,L):- bagof_nr(C,mpred_child(P,C),L).
 mpred_descendant(+P, ?Q) is semidet
mpred_descendant(P,Q) is true iff P is a justifier for Q.
  192mpred_descendant(P,Q):-
  193   mpred_descendant1(P,Q,[]).
 mpred_descendant1(+P, ?Q, ?Seen) is semidet
PFC Descendant Secondary Helper.
  200mpred_descendant1(P,Q,Seen):-
  201  mpred_child(X,Q),
  202  (\+ member(X,Seen)),
  203  (P=X ; mpred_descendant1(P,X,[X|Seen])).
 mpred_descendants(+P, ?L) is semidet
PFC Descendants.
  210mpred_descendants(P,L):-
  211  bagof_nr(Q,mpred_descendant1(P,Q,[]),L).
  212
  213:- meta_predicate(bagof_nr(?,^,*)).  214bagof_nr(T,G,B):- no_repeats(B,(bagof(T,G,B))).
  215:- meta_predicate(bagof_or_nil(?,^,-)).  216bagof_or_nil(T,G,B):- (bagof_nr(T,G,B) *-> true; B=[]).
  217
  218
  219:- meta_predicate(sanity_check(0,0)).  220sanity_check(When,Must):- When,Must,!.
  221sanity_check(When,Must):- must_ex((show_call(When),Must)),!.
  222
  223%
  224%  predicates for manipulating support relationships
  225%
  226
  227notify_if_neg_trigger(spft(P,Fact,Trigger)):- 
  228  (Trigger= nt(F,Condition,Action) ->
  229    (mpred_trace_msg('~N~n\tAdding NEG mpred_do_fcnt via support~n\t\ttrigger: ~p~n\t\tcond: ~p~n\t\taction: ~p~n\t from: ~p~N',
  230      [F,Condition,Action,mpred_add_support_fast(P,(Fact,Trigger))]));true).
  231
  232%  mpred_add_support(+Fact,+Support)
  233mpred_add_support(P,(Fact,Trigger)):-
  234  MSPFT = spft(P,Fact,Trigger),
  235   fix_mp(mpred_add_support,MSPFT,M,SPFT),
  236   M:notify_if_neg_trigger(SPFT),
  237  M:(clause_asserted_u(SPFT)-> true; sanity_check(assertz_mu(SPFT),clause_asserted_u(SPFT))).
  238
  239%  mpred_add_support_fast(+Fact,+Support)
  240mpred_add_support_fast(P,(Fact,Trigger)):-
  241      MSPFT = spft(P,Fact,Trigger),
  242       fix_mp(mpred_add_support,MSPFT,M,SPFT),
  243   M:notify_if_neg_trigger(SPFT),
  244   M:sanity_check(assertz_mu(SPFT),clause_asserted_u(SPFT)).
  245
  246
  247                                                                
  248:- meta_predicate(mpred_get_support(*,-)).  249
  250mpred_get_support((H:-B),(Fact,Trigger)):- lookup_u(spft((H <- B),_,_),Ref),clause(spft(HH<-BB,Fact,Trigger),true,Ref),
  251   clause_ref_module(Ref),   
  252   H=@=HH,B=@=BB.
  253mpred_get_support(P,(Fact,Trigger)):-
  254      lookup_spft(P,Fact,Trigger).
  255
  256
  257mpred_get_support_why(P,FT):-
  258  (mpred_get_support_perfect(P,FT)*->true;
  259   (mpred_get_support_deeper(P,FT))).
  260
  261mpred_get_support_perfect(P,(Fact,Trigger)):-
  262    lookup_spft_match_first(P,Fact,Trigger).
  263
  264mpred_get_support_deeper((H:-B),(Fact,Trigger)):- !,
  265 lookup_u(spft((H <- B),_,_),Ref),
  266  clause(spft(HH<-BB,Fact,Trigger),true,Ref),H=@=HH,B=@=BB.
  267mpred_get_support_deeper(P,(Fact,Trigger)):-
  268    lookup_spft_match_deeper(P,Fact,Trigger).
  269
  270/*
  271%  TODO MAYBE
  272mpred_get_support(F,J):-
  273  full_transform(mpred_get_support,F,FF),!,
  274  F\==FF,mpred_get_support(FF,J).
  275*/
  276
  277mpred_rem_support_if_exists(P,(Fact,Trigger)):-
  278  lookup_spft(P,Fact,Trigger),
  279  mpred_retract_i_or_warn(spft(P,Fact,Trigger)).
  280
  281
  282mpred_rem_support(P,(Fact,Trigger)):-
  283  closest_u(spft(P,Fact,Trigger),spft(P,FactO,TriggerO)),
  284  mpred_retract_i_or_warn_1(spft(P,FactO,TriggerO)).
  285mpred_rem_support(P,S):-
  286  mpred_retract_i_or_warn(spft(P,Fact,Trigger)),
  287  ignore((Fact,Trigger)=S).
  288
  289
  290
  291closest_u(Was,WasO):-clause_asserted_u(Was),!,Was=WasO.
  292closest_u(Was,WasO):-lookup_u(Was),!,Was=WasO,!.
  293closest_u(Was,WasO):-lookup_u(WasO),ignore(Was=WasO),!.
  294closest_u(H,HH):- ref(_) = Result,closest_uu(H,H,HH,Result),ref(Ref)= Result,
  295  (H==HH -> true ; nonvar(Ref)),!.
  296
  297closest_uu(H,P,PP):- copy_term(H+P,HH+PP),
  298      ((lookup_u(HH)*-> (=@=(P,PP)->(!,HH=H);(fail));(!,fail));(true)).
  299closest_uu(H,P,PP,Result):-
  300      sanity(Result=@=ref(Ref)),
  301      (copy_term(H+P,HH+PP),
  302      ((lookup_u(HH,Ref)*-> (=@=(P,PP)->(!,HH=H);
  303          (nb_setarg(1,Result,Ref),fail));(!,fail));((clause(HH,B,Ref),must_ex(B))))).
  304
  305/*
  306*/
  307
  308mpred_collect_supports(Tripples):-
  309  bagof_or_nil(Tripple, mpred_support_relation(Tripple), Tripples).
  310
  311mpred_support_relation((P,F,T)):- lookup_spft(P,F,T).
  312
  313mpred_make_supports((P,S1,S2)):-
  314  mpred_add_support(P,(S1,S2)),
  315  (mpred_ain_object(P); true),
  316  !.
  317
  318
  319pp_why:-mpred_why.
  320
  321mpred_why:-
  322  call(t_l:whybuffer(P,_)),
  323  mpred_why_1(P).
  324
  325pp_why(A):-mpred_why_1(A).
  326
  327clear_proofs:- retractall(t_l:whybuffer(_P,_Js)).
  328
  329
  330:- thread_local(t_l:shown_why/1).  331
  332% see pfc_why
  333
  334mpred_why(P):- must(mpred_why_1(P)).
  335
  336mpred_why_1(\+ P):- mpred_why_1(~P)*->true;(call_u(\+ P),wdmsgl(why:- \+ P)),!.
  337mpred_why_1(M:P):- atom(M),!,call_from_module(M,mpred_why_1(P)).
  338mpred_why_1(P):-  
  339  quietly_ex((must_ex((
  340  color_line(green,2),!,
  341  findall(Js,((no_repeats(P-Js,deterministically_must(justifications(P,Js))),
  342    ((color_line(yellow,1),
  343      pfcShowJustifications(P,Js))))),Count),
  344  (Count==[]-> format("~N No justifications for ~p. ~n~n",[P]) ; true),
  345  color_line(green,2)
  346  )))),!.
  347
  348mpred_why_1(NX):- 
  349  (number(NX)-> true ; retractall(t_l:whybuffer(_,_))),
  350  trace,
  351  pfcWhy0(NX),!.
  352
  353mpred_why_1(P):- mpred_why_sub(P).
  354
  355% mpred_why_1(N):- number(N),!, call(t_l:whybuffer(P,Js)), mpred_handle_why_command(N,P,Js).
  356
  357/*
  358
  359mpred_why_1(P):- loop_check(quietly_ex((must_ex(mpred_why_try_each(P)),color_line(green,2))),true).
  360
  361% user:mpred_why_1((user:prolog_exception_hook(A, B, C, D) :- exception_hook(A, B, C, D))).
  362% mpred_why_1((prolog_exception_hook(A, B, C, D) :- exception_hook(A, B, C, D))).
  363
  364mpred_why_try_each(MN):- strip_module(MN,_,N),number(N),!,pfcWhy0(N),!.
  365
  366mpred_why_try_each(ain(H)):-!,mpred_why_try_each(H).
  367mpred_why_try_each(call_u(H)):-!,mpred_why_try_each(H).
  368mpred_why_try_each(clause(H,B)):-!,mpred_why_try_each(H:-B).
  369mpred_why_try_each(clause(H,B,_)):-!,mpred_why_try_each(H:-B).
  370mpred_why_try_each(clause_u(P)):-!,mpred_why_try_each(P).
  371mpred_why_try_each(clause_u(H,B)):-!,mpred_why_try_each(H:-B).
  372mpred_why_try_each(clause_u(H,B,_)):-!,mpred_why_try_each(H:-B).
  373
  374mpred_why_try_each(P):- once((retractall(t_l:whybuffer(P,_)),color_line(green,2),
  375    show_current_source_location,format("~NJustifications for ~p:",[P]))),
  376    fail.
  377
  378mpred_why_try_each(P):- mpred_why_try_each_0(P),!.
  379mpred_why_try_each(P):- mpred_why_sub(P),!.
  380mpred_why_try_each(M:P :- B):- atom(M),call_from_module(M,mpred_why_try_each_0(P:-B)),!.
  381mpred_why_try_each(M:P):- atom(M),call_from_module(M,mpred_why_try_each_0(P)),!.
  382mpred_why_try_each(P :- B):- is_true(B),!,mpred_why_try_each(P ).
  383mpred_why_try_each(M:H):- strip_module(H,Ctx,P),P==H,Ctx==M,!,mpred_why_try_each(H).
  384mpred_why_try_each(_):- format("~N No justifications. ~n").
  385
  386mpred_why_try_each_0(P):- findall(Js,mpred_why_try_each_1(P,Js),Count),Count\==[],!.
  387mpred_why_try_each_0(\+ P):- mpred_why_try_each_0(~P)*->true;(call_u(\+ P),wdmsgl(why:- \+ P)),!.
  388
  389mpred_why_try_each_1(P,Js):-
  390  ((no_repeats(P-Js,deterministically_must(justifications(P,Js))),
  391    ((color_line(yellow,1), pfcShowJustifications(P,Js))))).
  392mpred_why_try_each_1(\+ P,[MFL]):- !, find_mfl(P,MFL),ansi_format([fg(cyan)],"~N    ~q",[MFL]),fail.
  393mpred_why_try_each_1( P,[MFL]):-  find_mfl(P,MFL), \+ clause_asserted(t_l:shown_why(MFL)), ansi_format([fg(cyan)],"~N    ~q",[MFL]).
  394
  395*/
  396pfcWhy0(N) :-
  397  number(N),
  398  !,
  399  t_l:whybuffer(P,Js),
  400  pfcWhyCommand0(N,P,Js).
  401
  402pfcWhy0(P) :-
  403  justifications(P,Js),  
  404  assert(t_l:whybuffer(P,Js)),                     
  405  pfcWhyBrouse(P,Js).
  406
  407pfcWhy1(P) :-
  408  justifications(P,Js),
  409  pfcWhyBrouse(P,Js).
  410
  411pfcWhyBrouse(P,Js) :-    % non-interactive
  412  pfcShowJustifications(P,Js),source_file(_,_),!.
  413
  414pfcWhyBrouse(P,Js) :- 
  415  pfcShowJustifications(P,Js),
  416  ttyflush,
  417  read_pending_chars(current_input,_,[]),!,
  418  ttyflush,
  419  % pfcAsk(' >> ',Answer),
  420  % read_pending_chars(current_input,[Answer|_],[]),!,  
  421  format('~N',[]),write('proof [q/h/u/?.?]: '),get_char(Answer),
  422  pfcWhyCommand0(Answer,P,Js).
  423
  424pfcWhyCommand0(q,_,_) :- !.
  425pfcWhyCommand0(h,_,_) :- 
  426  !,
  427  format("~n
  428Justification Brouser Commands:
  429 q   quit.
  430 N   focus on Nth justification.
  431 N.M brouse step M of the Nth justification
  432 u   up a level
  433",
  434 []).
  435
  436pfcWhyCommand0(N,_P,Js) :-
  437  float(N),
  438  !,
  439  pfcSelectJustificationNode(Js,N,Node),
  440  pfcWhy1(Node).
  441
  442pfcWhyCommand0(u,_,_) :-
  443  % u=up
  444  !.
  445
  446pfcWhyCommand0(N,_,_) :-
  447  integer(N),
  448  !,
  449  format("~n~w is a yet unimplemented command.",[N]),
  450  fail.
  451
  452pfcWhyCommand0(X,_,_) :-
  453 format("~n~w is an unrecognized command, enter h. for help.",[X]),
  454 fail.
  455  
  456pfcShowJustifications(P,Js) :-
  457  show_current_source_location,
  458  format("~N~nJustifications for ~p:~n",[P]),  
  459  pfcShowJustification1(Js,1),!.
  460
  461pfcShowJustification1([],_):-!.
  462pfcShowJustification1([J|Js],N) :- !,
  463  % show one justification and recurse.  
  464  retractall(t_l:shown_why(_)), % nl,
  465  pfcShowSingleJust(N,step(1),J),!,
  466  N2 is N+1,pfcShowJustification1(Js,N2).
  467pfcShowJustification1(J,N) :- retractall(t_l:shown_why(_)), % nl,
  468  pfcShowSingleJust(N,step(1),J),!.
  469
  470incrStep(StepNo,Step):-arg(1,StepNo,Step),X is Step+1,nb_setarg(1,StepNo,X).
  471
  472pfcShowSingleJust(JustNo,StepNo,C):- is_ftVar(C),!,incrStep(StepNo,Step),
  473  ansi_format([fg(cyan)],"~N    ~w.~w ~w ",[JustNo,Step,C]),!.
  474pfcShowSingleJust(_JustNo,_StepNo,[]):-!.
  475pfcShowSingleJust(JustNo,StepNo,(P,T)):-!, 
  476  pfcShowSingleJust(JustNo,StepNo,P),
  477  pfcShowSingleJust(JustNo,StepNo,T).
  478pfcShowSingleJust(JustNo,StepNo,(P,F,T)):-!, 
  479  pfcShowSingleJust1(JustNo,StepNo,P),
  480  pfcShowSingleJust(JustNo,StepNo,F),
  481  pfcShowSingleJust1(JustNo,StepNo,T).
  482pfcShowSingleJust(JustNo,StepNo,(P*->T)):-!, 
  483  pfcShowSingleJust1(JustNo,StepNo,P),format('      *-> ',[]),
  484  pfcShowSingleJust1(JustNo,StepNo,T).
  485pfcShowSingleJust(JustNo,StepNo,(P:-T)):-!, 
  486  pfcShowSingleJust1(JustNo,StepNo,P),format('      :- ',[]),
  487  pfcShowSingleJust(JustNo,StepNo,T).
  488pfcShowSingleJust(JustNo,StepNo,[P|T]):-!, 
  489  pfcShowSingleJust(JustNo,StepNo,P),
  490  pfcShowSingleJust(JustNo,StepNo,T).
  491pfcShowSingleJust(JustNo,StepNo,pt(P,Body)):- !, 
  492  pfcShowSingleJust1(JustNo,StepNo,pt(P)),  
  493  pfcShowSingleJust(JustNo,StepNo,Body).
  494pfcShowSingleJust(JustNo,StepNo,:- (P,Body) ):- !, 
  495  pfcShowSingleJust1(JustNo,StepNo,call(Body)),  
  496  pfcShowSingleJust1(JustNo,StepNo,P).
  497pfcShowSingleJust(JustNo,StepNo,C):- 
  498 pfcShowSingleJust1(JustNo,StepNo,C).
  499
  500fmt_cl(P):- \+ \+ (numbervars(P,126,_,[attvar(skip),singletons(true)]),write_term(P,[portray(true)])).
  501
  502unwrap_litr(C,CCC+VS):- copy_term(C,CC,VS),
  503  numbervars(CC+VS,0,_),
  504  unwrap_litr0(CC,CCC),!.
  505unwrap_litr0(call(C),CC):-unwrap_litr0(C,CC).
  506unwrap_litr0(pt(C),CC):-unwrap_litr0(C,CC).
  507unwrap_litr0(body(C),CC):-unwrap_litr0(C,CC).
  508unwrap_litr0(head(C),CC):-unwrap_litr0(C,CC).
  509unwrap_litr0(C,C).
  510
  511pfcShowSingleJust1(JustNo,StepNo,C):- unwrap_litr(C,CC),!,pfcShowSingleJust4(JustNo,StepNo,C,CC).
  512pfcShowSingleJust4(_,_,_,CC):- t_l:shown_why(C),C=@=CC,!.
  513pfcShowSingleJust4(JustNo,StepNo,C,CC):- assert(t_l:shown_why(CC)),!,
  514   incrStep(StepNo,Step),
  515   ansi_format([fg(cyan)],"~N    ~w.~w ~@ ",[JustNo,Step,fmt_cl(C)]),   
  516   pfcShowSingleJust_C(C),!.
  517
  518pfcShowSingleJust_C(C):-is_file_ref(C),!.
  519pfcShowSingleJust_C(C):-find_mfl(C,MFL),assert(t_l:shown_why(MFL)),!,pfcShowSingleJust_MFL(MFL).
  520pfcShowSingleJust_C(_):-ansi_format([hfg(black)]," % [no_mfl] ",[]),!.
  521
  522short_filename(F,FN):- atomic_list_concat([_,FN],'/pack/',F),!.
  523short_filename(F,FN):- atomic_list_concat([_,FN],swipl,F),!.
  524short_filename(F,FN):- F=FN,!.
  525
  526pfcShowSingleJust_MFL(MFL):- MFL=mfl4(VarNameZ,_M,F,L),atom(F),short_filename(F,FN),!,varnames_load_context(VarNameZ),
  527   ansi_format([hfg(black)]," % [~w:~w] ",[FN,L]).
  528pfcShowSingleJust_MFL(MFL):- ansi_format([hfg(black)]," % [~w] ",[MFL]),!.
  529
  530pfcAsk(Msg,Ans) :-
  531  format("~n~w",[Msg]),
  532  read(Ans).
  533
  534pfcSelectJustificationNode(Js,Index,Step) :-
  535  JustNo is integer(Index),
  536  nth1(JustNo,Js,Justification),
  537  StepNo is 1+ integer(Index*10 - JustNo*10),
  538  nth1(StepNo,Justification,Step).
  539
  540
  541
  542
  543
  544
  545
  546mpred_why_maybe(_,(F:-P)):-!,wdmsgl(F:-P),!.
  547mpred_why_maybe(F,P):-wdmsgl(F:-P),!.
  548mpred_why_maybe(_,P):-ignore(mpred_why_1(P)).
  549
  550mpred_why_sub(P):- trace, loop_check(mpred_why_sub0(P),true).
  551mpred_why_sub0(P):- mpred_why_2(P,Why),!,wdmsg(:-mpred_why_1(P)),wdmsgl(mpred_why_maybe(P),Why).
  552mpred_why_sub0(P):-loop_check(mpred_why_sub_lc(P),trace_or_throw_ex(mpred_why_sub_lc(P)))-> \+ \+ call(t_l:whybuffer(_,_)),!.
  553mpred_why_sub_lc(P):- 
  554  justifications(P,Js),
  555  nb_setval('$last_printed',[]),
  556  retractall(t_l:whybuffer(_,_)),
  557  assertz(t_l:whybuffer(P,Js)),
  558  mpred_whyBrouse(P,Js).
  559  
  560
  561mpred_why_sub_sub(P):-
  562  justifications(P,Js),
  563  clear_proofs,
  564  % retractall_u(t_l:whybuffer(_,_)),
  565  (nb_hasval('$last_printed',P)-> dmsg(hasVal(P)) ;
  566   ((
  567  assertz(t_l:whybuffer(P,Js)),
  568   nb_getval('$last_printed',LP),
  569   ((mpred_pp_db_justification1(LP,Js,1),fmt('~N~n',[])))))).
  570
  571nb_pushval(Name,Value):-nb_current(Name,Before)->nb_setval(Name,[Value|Before]);nb_setval(Name,[Value]).
  572nb_peekval(Name,Value):-nb_current(Name,[Value|_Before]).
  573nb_hasval(Name,Value):-nb_current(Name,List),member(Value,List).
  574nb_popval(Name,Value):-nb_current(Name,[Value|Before])->nb_setval(Name,Before).
  575
  576mpred_why1(P):-
  577  justifications(P,Js),
  578  mpred_whyBrouse(P,Js).
  579
  580% non-interactive
  581mpred_whyBrouse(P,Js):-
  582   must_ex(quietly_ex(in_cmt((mpred_pp_db_justifications(P,Js))))), !.
  583
  584% Interactive
  585mpred_whyBrouse(P,Js):-
  586  mpred_pp_db_justifications(P,Js),
  587  mpred_prompt_ask(' >> ',Answer),
  588  mpred_handle_why_command(Answer,P,Js).
  589
  590mpred_handle_why_command(q,_,_):- !.
  591mpred_handle_why_command(h,_,_):-
  592  !,
  593  format("~N
  594Justification Brouser Commands:
  595 q   quit.
  596 N   focus on Nth justification.
  597 N.M brouse step M of the Nth justification
  598 user   up a level ~n",
  599  []).
  600
  601mpred_handle_why_command(N,_ZP,Js):-
  602  float(N),
  603  !,
  604  mpred_select_justification_node(Js,N,Node),
  605  mpred_why1(Node).
  606
  607mpred_handle_why_command(u,_,_):-
  608  % u=up
  609  !.
  610
  611mpred_unhandled_command(N,_,_):-
  612  integer(N),
  613  !,
  614  format("~N~p is a yet unimplemented command.",[N]),
  615  fail.
  616
  617mpred_unhandled_command(X,_,_):-
  618 format("~N~p is an unrecognized command, enter h. for help.",[X]),
  619 fail.
  620
  621mpred_pp_db_justifications(P,Js):-
  622 show_current_source_location, 
  623 must_ex(quietly_ex(( format("~NJustifications for ~p:",[P]),
  624  mpred_pp_db_justification1('',Js,1)))).
  625
  626mpred_pp_db_justification1(_Prefix,[],_).
  627
  628mpred_pp_db_justification1(Prefix,[J|Js],N):-
  629  % show one justification and recurse.
  630  nl,
  631  mpred_pp_db_justifications2(Prefix,J,N,1),
  632  N2 is N+1,
  633  mpred_pp_db_justification1(Prefix,Js,N2).
  634
  635mpred_pp_db_justifications2(_Prefix,[],_,_).
  636
  637mpred_pp_db_justifications2(Prefix,[C|Rest],JustNo,StepNo):-
  638(nb_hasval('$last_printed',C)-> dmsg(chasVal(C)) ;
  639(
  640 (StepNo==1->fmt('~N~n',[]);true),
  641  sformat(LP,' ~w.~p.~p',[Prefix,JustNo,StepNo]),
  642  nb_pushval('$last_printed',LP),
  643  format("~N  ~w ~p",[LP,C]),
  644  ignore(loop_check(mpred_why_sub_sub(C))),
  645  StepNext is 1+StepNo,
  646  mpred_pp_db_justifications2(Prefix,Rest,JustNo,StepNext))).
  647
  648mpred_prompt_ask(Info,Ans):-
  649  format("~N~p",[Info]),
  650  read(Ans).
  651
  652mpred_select_justification_node(Js,Index,Step):-
  653  JustNo is integer(Index),
  654  nth1(JustNo,Js,Justification),
  655  StepNo is 1+ integer(Index*10 - JustNo*10),
  656  nth1(StepNo,Justification,Step).
 mpred_supported(+P) is semidet
succeeds if P is "supported". What this means depends on the TMS mode selected.
  664mpred_supported(P):-
  665  must_ex(get_tms_mode(P,Mode))->
  666  mpred_supported(Mode,P).
 mpred_supported(+TMS, +P) is semidet
succeeds if P is "supported". What this means depends on the TMS mode supplied.
  673mpred_supported(local,P):- !, mpred_get_support(P,_),!, not_rejected(P).
  674mpred_supported(cycles,P):-  !, well_founded(P),!, not_rejected(P).
  675mpred_supported(How,P):- ignore(How=unknown),not_rejected(P).
  676
  677not_rejected(~P):- nonvar(P),  \+ mpred_get_support(P,_).
  678not_rejected(P):-  \+ mpred_get_support(~P,_).
 well_founded(+Fact) is semidet
a fact is well founded if it is supported by the user or by a set of facts and a rules, all of which are well founded.
  685well_founded(Fact):- each_E(well_founded_0,Fact,[_]).
  686
  687well_founded_0(F,_):-
  688  % supported by user (axiom) or an "absent" fact (assumption).
  689  (mpred_axiom(F) ; mpred_assumption(F)),
  690  !.
  691
  692well_founded_0(F,Descendants):-
  693  % first make sure we aren't in a loop.
  694  (\+ memberchk(F,Descendants)),
  695  % find a justification.
  696  supporters_list0(F,Supporters),!,
  697  % all of whose members are well founded.
  698  well_founded_list(Supporters,[F|Descendants]),
  699  !.
 well_founded_list(+List, -Decendants) is det
simply maps well_founded over the list.
  705well_founded_list([],_).
  706well_founded_list([X|Rest],L):-
  707  well_founded_0(X,L),
  708  well_founded_list(Rest,L).
 supporters_list(+F, -ListofSupporters) is det
where ListOfSupports is a list of the supports for one justification for fact F -- i.e. a list of facts which, together allow one to deduce F. One of the facts will typically be a rule. The supports for a user-defined fact are: [ax].
  718supporters_list(F,ListO):- no_repeats_cmp(same_sets,ListO,supporters_list_each(F,ListO)).
  719
  720same_sets(X,Y):-
  721  flatten(X,FX),sort(FX,XS),
  722  flatten(Y,FY),sort(FY,YS),!,
  723  YS=@=XS.
  724
  725supporters_list_each(F,ListO):-   
  726   supporters_list0(F,ListM),
  727   expand_supporters_list(ListM,ListM,ListO).
  728
  729expand_supporters_list(_, [],[]):-!.
  730expand_supporters_list(Orig,[F|ListM],[F|NewListOO]):-
  731   supporters_list0(F,FList),
  732   list_difference_variant(FList,Orig,NewList),
  733   % NewList\==[],
  734   append(Orig,NewList,NewOrig),
  735   append(ListM,NewList,NewListM),!,
  736   expand_supporters_list(NewOrig,NewListM,ListO),
  737   append(ListO,NewList,NewListO),
  738   list_to_set_variant(NewListO,NewListOO).
  739expand_supporters_list(Orig,[F|ListM],[F|NewListO]):-
  740  expand_supporters_list(Orig,ListM,NewListO).
  741
  742
  743list_to_set_variant(List, Unique) :-
  744    list_unique_1(List, [], Unique),!.
  745
  746list_unique_1([], _, []).
  747list_unique_1([X|Xs], So_far, Us) :-
  748    memberchk_variant(X, So_far),!,
  749    list_unique_1(Xs, So_far, Us).
  750list_unique_1([X|Xs], So_far, [X|Us]) :-
  751    list_unique_1(Xs, [X|So_far], Us).
  752
  753% dif_variant(X,Y):- freeze(X,freeze(Y, X \=@= Y )).
 list_difference_variant(+List, -Subtract, -Rest)
Delete all elements of Subtract from List and unify the result with Rest. Element comparision is done using =@=/2.
  762list_difference_variant([],_,[]).
  763list_difference_variant([X|Xs],Ys,L) :-
  764	(   memberchk_variant(X,Ys)
  765	->  list_difference_variant(Xs,Ys,L)
  766	;   L = [X|T],
  767	    list_difference_variant(Xs,Ys,T)
  768	).
 memberchk_variant(+Val, +List)
Deterministic check of membership using =@= rather than unification.
  776memberchk_variant(X, [Y|Ys]) :-
  777   (   X =@= Y
  778   ->  true
  779   ;   memberchk_variant(X, Ys)
  780   ).
  781
  782supporters_list0(Var,[is_ftVar(Var)]):-is_ftVar(Var),!.
  783supporters_list0(F,OUT):- 
  784  with_quiet_vars_lock((((mpred_get_support_why(F,(Fact,Trigger)),
  785    triggerSupports(Fact,Trigger,MoreFacts)))*-> OUT=[Fact|MoreFacts] ; supporters_list1(F,OUT))).
  786
  787supporters_list1(Var,[is_ftVar(Var)]):-is_ftVar(Var),!.
  788supporters_list1(U,[]):- axiomatic_supporter(U),!.
  789supporters_list1((H:-B),[MFL]):- !, clause_match(H,B,Ref),find_hb_mfl(H,B,Ref,MFL).
  790supporters_list1(\+ P, HOW):- supporters_list0(~ P,HOW),!.
  791supporters_list1((H),[((H:-B))]):- clause_match(H,B,_Ref).
  792
  793uses_call_only(H):- predicate_property(H,foreign),!.
  794uses_call_only(H):- predicate_property(H,_), \+ predicate_property(H,interpreted),!.
  795
  796clause_match(H,_B,uses_call_only(H)):- uses_call_only(H),!.
  797clause_match(H,B,Ref):- clause_asserted(H,B,Ref),!.
  798clause_match(H,B,Ref):- ((copy_term(H,HH),clause_u(H,B,Ref),H=@=HH)*->true;clause_u(H,B,Ref)), \+ reserved_body_helper(B).
  799
  800find_mfl(C,MFL):- lookup_spft_match(C,MFL,ax).
  801find_mfl(C,MFL):- unwrap_litr0(C,UC) -> C\==UC -> find_mfl(UC,MFL).
  802find_mfl(C,MFL):- expand_to_hb(C,H,B),
  803   find_hb_mfl(H,B,_Ref,MFL)->true; (clause_match(H,B,Ref),find_hb_mfl(H,B,Ref,MFL)).
  804
  805find_hb_mfl(_H,_B,Ref,mfl4(_VarNameZ,M,F,L)):- atomic(Ref),clause_property(Ref,line_count(L)),
  806 clause_property(Ref,file(F)),clause_property(Ref,module(M)). 
  807find_hb_mfl(H,B,_,mfl4(VarNameZ,M,F,L)):- lookup_spft_match_first( (H:-B),mfl4(VarNameZ,M,F,L),_),!.
  808find_hb_mfl(H,B,_Ref,mfl4(VarNameZ,M,F,L)):- lookup_spft_match_first(H,mfl4(VarNameZ,M,F,L),_),ground(B).
  809find_hb_mfl(H,_B,uses_call_only(H),MFL):- !,call_only_based_mfl(H,MFL).
  810
  811/*
  812
  813
  814clause_match(H,_B,uses_call_only(H)):- uses_call_only(H),!.
  815clause_match(H,B,Ref):- clause_asserted(H,B,Ref),!.
  816
  817clause_match(H,B,Ref):- no_repeats(Ref,((((copy_term(H,HH),clause_u(H,B,Ref),H=@=HH)*->true;clause_u(H,B,Ref)), \+ reserved_body_helper(B)))).
  818
  819clause_match0(H,B,Ref):- no_repeats(Ref,clause_match1(H,B,Ref)).
  820
  821clause_match1(H,B,Ref):- clause(H,B,Ref).
  822clause_match1(M:H,B,Ref):- !, (M:clause(H,B,Ref) ; clause_match2(H,B,Ref)).
  823clause_match1(H,B,Ref):- clause_match2(H,B,Ref).
  824
  825clause_match2(H,B,Ref):- current_module(M),clause(M:H,B,Ref),(clause_property(Ref, module(MM))->MM==M;true).
  826
  827find_mfl(C,MFL):-find_mfl0(C,MFL),compound(MFL),MFL=mfl4(VarNameZ,_,F,_),nonvar(F).
  828find_mfl0(C,MFL):- lookup_spft_match(C,MFL,ax).
  829% find_mfl0(mfl4(VarNameZ,M,F,L),mfl4(VarNameZ,M,F,L)):-!.
  830find_mfl0(C,MFL):-expand_to_hb(C,H,B),
  831   find_hb_mfl(H,B,_Ref,MFL)->true; (clause_match(H,B,Ref),find_hb_mfl(H,B,Ref,MFL)).
  832find_mfl0(C,MFL):-expand_to_hb(C,H,B),
  833   find_hb_mfl(H,B,_Ref,MFL)->true; (clause_match0(H,B,Ref),find_hb_mfl(H,B,Ref,MFL)).
  834
  835*/
  836call_only_based_mfl(H,mfl4(_VarNameZ,M,F,L)):- 
  837  ignore(predicate_property(H,imported_from(M));predicate_property(H,module(M))),
  838  ignore(predicate_property(H,line_count(L))),
  839  ignore(source_file(M:H,F);predicate_property(H,file(F));(predicate_property(H,foreign),F=foreign)).
  840
  841axiomatic_supporter(Var):-is_ftVar(Var),!,fail.
  842axiomatic_supporter(is_ftVar(_)).
  843axiomatic_supporter(clause_u(_)).
  844axiomatic_supporter(U):- is_file_ref(U),!.
  845axiomatic_supporter(ax):-!.
  846
  847is_file_ref(A):-compound(A),A=mfl4(VarNameZ,_,_,_).
  848
  849triggerSupports(_,Var,[is_ftVar(Var)]):-is_ftVar(Var),!.
  850triggerSupports(_,U,[]):- axiomatic_supporter(U),!.
  851triggerSupports(FactIn,Trigger,OUT):-
  852  mpred_get_support(Trigger,(Fact,AnotherTrigger))*->
  853  (triggerSupports(Fact,AnotherTrigger,MoreFacts),OUT=[Fact|MoreFacts]);
  854  triggerSupports1(FactIn,Trigger,OUT).
  855
  856triggerSupports1(_,X,[X]).
  857/*
  858triggerSupports1(_,X,_):- mpred_db_type(X,trigger(_)),!,fail.
  859triggerSupports1(_,uWas(_),[]):-!.
  860triggerSupports1(_,U,[(U)]):- is_file_ref(U),!.
  861triggerSupports1(_,U,[uWas(U)]):- get_source_uu((U1,U2))->member(U12,[U1,U2]),U12=@=U.
  862triggerSupports1(_,X,[X]):- \+ mpred_db_type(X,trigger(_)).
  863*/
  864
  865
  866/*
  867:-module_transparent(mpred_ain/1).
  868:-module_transparent(mpred_aina/1).
  869:-module_transparent(mpred_ainz/1).
  870*/
  871
  872% :- '$current_source_module'(M),forall(mpred_database_term(F,A,_),(abolish(mpred_core:F/A),abolish(user:F/A),abolish(M:F/A))).
  873% :- initialization(ensure_abox(baseKB)).
  874% :- kb_shared(mpred_is_spying_pred/2).
  875
  876
  877% % :- set_prolog_flag(mpred_pfc_file,true).
  878% local_testing
  879
  880:- fixup_exports.