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
   40:- set_prolog_flag(expect_pfc_file,never).   41
   42mpred_why(M:Conseq,Ante):- atom(M),!,M:mpred_why_2(Conseq,Ante).
   43
   44mpred_why(Conseq,Ante):- mpred_why_2(Conseq,Ante).
   45
   46mpred_why_2(Conseq,Ante):- var(Conseq),!,mpred_children(Ante,Conseq).
   47mpred_why_2(Conseq,Ante):- justifications(Conseq,Ante).
   48
   49
   50
   51mpred_info(O):-
   52 with_output_to(user_error,
   53 ((dmsg_pretty("======================================================================="),
   54  listing(O),
   55  dmsg_pretty("======================================================================="),
   56  quietly(call_with_inference_limit(ignore(on_xf_cont(deterministically_must(mpred_why_1(O)))),4000,_)),
   57  dmsg_pretty("======================================================================="),
   58  must_maplist(mp_printAll(O),
   59  [   mpred_db_type(O,v),  
   60      +(mpred_child(O,v)),
   61      % mpred_fact(O),
   62      mpred_axiom(O),
   63      well_founded(O),
   64      mpred_supported(local,O),
   65      mpred_supported(cycles,O),
   66      mpred_assumption(O),
   67      get_mpred_is_tracing(O)]),
   68 dmsg_pretty("=======================================================================")))).
   69
   70mp_printAll(S,+(O)):- subst(O,v,V,CALL),CALL\==O,!,
   71  subst(O,S,s,NAME),safe_functor(O,F,_),!,
   72  nl,flush_output, fmt("=================="),wdmsg_pretty(NAME),wdmsg_pretty("---"),flush_output,!,
   73  doall(((flush_output,(CALL),flush_output)*->fmt9(V);(fail=F))),nl,fmt("=================="),nl,flush_output.
   74mp_printAll(S,call(O)):- !,
   75  subst(O,S,s,NAME),
   76  nl,flush_output,fmt("=================="),wdmsg_pretty(NAME),wdmsg_pretty("---"),flush_output,!,
   77  doall(((flush_output,deterministically_must(O),flush_output)*->true;wdmsg_pretty(false=NAME))),fmt("=================="),nl,flush_output.
   78mp_printAll(S,(O)):- subst(O,v,V,CALL),CALL\==O,!,
   79  subst(O,S,s,NAME),safe_functor(O,F,_),
   80  nl,flush_output, fmt("=================="),wdmsg_pretty(NAME),wdmsg_pretty("---"),flush_output,!,
   81  doall(((flush_output,deterministically_must(CALL),flush_output)*->fmt9(V);(fail=F))),nl,fmt("=================="),nl,flush_output.
   82mp_printAll(S,(O)):-  !,  safe_functor(O,F,A),mp_nnvv(S,O,F,A),flush_output.
   83mp_nnvv(_,(O),F,1):- !, doall(((flush_output,deterministically_must(O),flush_output)*->wdmsg_pretty(+F);wdmsg_pretty(-F))).
   84mp_nnvv(S,(O),_,_):- !, subst(O,S,s,NAME), !,
   85  doall(((flush_output,deterministically_must(O),flush_output)*->wdmsg_pretty(-NAME);wdmsg_pretty(+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.

   99mpred_basis_list(F,[F]):- (mpred_axiom(F) ; mpred_assumption(F)),!.
  100
  101mpred_basis_list(F,L):-
  102  % i.e. (reduce 'append (map 'mpred_basis_list (justification f)))
  103  justification(F,Js),
  104  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.

  112bases_union([],[]).
  113bases_union([X|Rest],L):-
  114  mpred_basis_list(X,Bx),
  115  bases_union(Rest,Br),
  116  mpred_union(Bx,Br,L).
  117
  118%mpred_axiom(F):- !, % Like OLD TODO
  119%  mpred_get_support(F,(_,ax)).
  120mpred_axiom(F):-
  121  mpred_get_support(F,UU),
  122  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)

  129mpred_assumption(P):- !, % Like OLD TODO
  130  nonvar(P), mpred_unnegate(P,_).
  131mpred_assumption(P):- nonvar(P), 
  132  mpred_unnegate(P,N), 
  133 % fail,
  134  % added prohibited_check
  135  (current_prolog_flag(explicitly_prohibited_check,false) -> true ; \+ mpred_axiom(~ N)).
  136
  137
  138:- set_prolog_flag(explicitly_prohibited_check,false).

 mpred_assumptions(+X, +AsSet) is semidet

true if AsSet is a set of assumptions which underly X.

  144mpred_assumptions(X,[X]):- mpred_assumption(X).
  145mpred_assumptions(X,[]):- mpred_axiom(X).
  146mpred_assumptions(X,L):-
  147  justification(X,Js),
  148  do_assumpts(Js,L).

 do_assumpts(+Set1, ?Set2) is semidet

Assumptions Secondary Helper.

  155do_assumpts([],[]).
  156do_assumpts([X|Rest],L):-
  157  mpred_assumptions(X,Bx),
  158  do_assumpts(Rest,Br),
  159  mpred_union(Bx,Br,L).
  160
  161
  162%  mpred_proofTree(P,T) the proof tree for P is T where a proof tree is
  163%  of the form
  164%
  165%      [P , J1, J2, ;;; Jn]         each Ji is an independent P justifier.
  166%           ^                         and has the form of
  167%           [J11, J12,... J1n]      a list of proof trees.

 mpred_child(+P, ?Q) is semidet

is true iff P is an immediate justifier for Q.

  174mpred_child(P,Q):- is_list(P),!,maplist(mpred_child,P,Q).
  175mpred_child(P,Q):-
  176  mpred_get_support(Q,(P,_)).
  177mpred_child(P,Q):-
  178  mpred_get_support(Q,(_,Trig)),
  179  mpred_db_type(Trig,trigger(_TT)),
  180  mpred_child(P,Trig).

 mpred_children(+P, ?L) is semidet

PFC Children.

  187mpred_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.

  195mpred_descendant(P,Q):-
  196   mpred_descendant1(P,Q,[]).

 mpred_descendant1(+P, ?Q, ?Seen) is semidet

PFC Descendant Secondary Helper.

  203mpred_descendant1(P,Q,Seen):-
  204  mpred_child(X,Q),
  205  (\+ member(X,Seen)),
  206  (P=X ; mpred_descendant1(P,X,[X|Seen])).

 mpred_descendants(+P, ?L) is semidet

PFC Descendants.

  213mpred_descendants(P,L):-
  214  bagof_nr(Q,mpred_descendant1(P,Q,[]),L).
  215
  216:- meta_predicate(bagof_nr(?,^,*)).  217bagof_nr(T,G,B):- no_repeats(B,(bagof(T,G,B))).
  218:- meta_predicate(bagof_or_nil(?,^,-)).  219bagof_or_nil(T,G,B):- (bagof_nr(T,G,B) *-> true; B=[]).
  220
  221
  222:- meta_predicate(sanity_check(0,0)).  223sanity_check(When,Must):- When,Must,!.
  224sanity_check(When,Must):- must_ex((show_call(When),Must)),!.
  225
  226%
  227%  predicates for manipulating support relationships
  228%
  229
  230notify_if_neg_trigger(spft(P,Fact,Trigger)):- 
  231  (Trigger= nt(F,Condition,Action) ->
  232    (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',
  233      [F,Condition,Action,mpred_add_support_fast(P,(Fact,Trigger))]));true).
  234
  235%  mpred_add_support(+Fact,+Support)
  236mpred_add_support(P,(Fact,Trigger)):-
  237  MSPFT = spft(P,Fact,Trigger),
  238   fix_mp(mpred_add_support,MSPFT,M,SPFT),
  239   M:notify_if_neg_trigger(SPFT),
  240  M:(clause_asserted_u(SPFT)-> true; sanity_check(assertz_mu(SPFT),clause_asserted_u(SPFT))).
  241
  242%  mpred_add_support_fast(+Fact,+Support)
  243mpred_add_support_fast(P,(Fact,Trigger)):-
  244      MSPFT = spft(P,Fact,Trigger),
  245       fix_mp(mpred_add_support,MSPFT,M,SPFT),
  246   M:notify_if_neg_trigger(SPFT),
  247   M:sanity_check(assertz_mu(SPFT),clause_asserted_u(SPFT)).
  248
  249
  250                                                                
  251:- meta_predicate(mpred_get_support(*,-)).  252
  253mpred_get_support((H:-B),(Fact,Trigger)):- 
  254   lookup_u(spft((H <- B),_,_),Ref),
  255   clause(spft(HH<-BB,Fact,Trigger),true,Ref),
  256   clause_ref_module(Ref),   
  257   H=@=HH,B=@=BB.
  258mpred_get_support(P,(Fact,Trigger)):-
  259  lookup_spft(P,Fact,Trigger).
  260
  261
  262mpred_get_support_why(P,FT):-
  263  (mpred_get_support_perfect(P,FT)*->true;
  264   (mpred_get_support_deeper(P,FT))).
  265
  266mpred_get_support_perfect(P,(Fact,Trigger)):-
  267   lookup_spft_match_first(P,Fact,Trigger).
  268
  269mpred_get_support_deeper((H:-B),(Fact,Trigger)):- (nonvar(H) -> ! ; true),
  270 lookup_u(spft((H <- B),_,_),Ref),
  271  clause(spft(HH<-BB,Fact,Trigger),true,Ref),
  272  H=@=HH,B=@=BB.
  273
  274mpred_get_support_deeper(P,(Fact,Trigger)):-
  275    lookup_spft_match_deeper(P,Fact,Trigger).
  276
  277lookup_spft_match(A,B,C):- copy_term(A,AA),lookup_spft(A,B,C),A=@=AA.
  278
  279lookup_spft_match_deeper(H,Fact,Trigger):- 
  280  copy_term(H,HH),
  281  lookup_spft((H:- _B),Fact,Trigger),
  282  H=@=HH.
  283
  284lookup_spft_match_first(A,B,C):- nonvar(A),!, 
  285  no_repeats(((lookup_spft_match(A,B,C);lookup_spft(A,B,C)))).
  286
  287lookup_spft_match_first(A,B,C):- lookup_spft(A,B,C).
  288
  289
  290lookup_spft(A,B,C):- !, lookup_u(spft(A,B,C)).
  291% cutted above
  292/*
  293lookup_spft(A,B,C):- nonvar(A),!,lookup_spft_p(A,B,C).
  294lookup_spft(A,B,C):- var(B),!,lookup_spft_t(A,B,C).
  295lookup_spft(A,B,C):- lookup_spft_f(A,B,C).
  296
  297lookup_spft_p(A,B,C):- with_some_vars_locked(A,lookup_u(spft(A,B,C))).
  298% TODO UNCOMMENT MAYBE IF NEEDED lookup_spft_p(A,B,C):- full_transform(lookup,A,AA),!,A\=@=AA,!,show_mpred_success(baseKB:spft(AA,B,C)).
  299
  300lookup_spft_f(A,B,C):- with_some_vars_locked(B,lookup_u(spft(A,B,C))).
  301% TODO UNCOMMENT MAYBE IF NEEDED lookup_spft_f(A,B,C):- full_transform(lookup,B,BB),!,B\=@=BB,!,show_mpred_success(baseKB:spft(A,BB,C)).
  302
  303lookup_spft_t(A,B,C):- lookup_u(spft(A,B,C)).
  304*/
  305/*
  306%  TODO MAYBE
  307mpred_get_support(F,J):-
  308  full_transform(mpred_get_support,F,FF),!,
  309  F\==FF,mpred_get_support(FF,J).
  310*/
  311
  312mpred_rem_support_if_exists(P,(Fact,Trigger)):-
  313  lookup_spft(P,Fact,Trigger),
  314  mpred_retract_i_or_warn(spft(P,Fact,Trigger)).
  315
  316
  317mpred_rem_support(P,(Fact,Trigger)):-
  318  closest_u(spft(P,Fact,Trigger),spft(P,FactO,TriggerO)),
  319  mpred_retract_i_or_warn_1(spft(P,FactO,TriggerO)).
  320mpred_rem_support(P,S):-
  321  mpred_retract_i_or_warn(spft(P,Fact,Trigger)),
  322  ignore((Fact,Trigger)=S).
  323
  324
  325
  326closest_u(Was,WasO):-clause_asserted_u(Was),!,Was=WasO.
  327closest_u(Was,WasO):-lookup_u(Was),!,Was=WasO,!.
  328closest_u(Was,WasO):-lookup_u(WasO),ignore(Was=WasO),!.
  329closest_u(H,HH):- ref(_) = Result,closest_uu(H,H,HH,Result),ref(Ref)= Result,
  330  (H==HH -> true ; nonvar(Ref)),!.
  331
  332closest_uu(H,P,PP):- copy_term(H+P,HH+PP),
  333      ((lookup_u(HH)*-> (=@=(P,PP)->(!,HH=H);(fail));(!,fail));(true)).
  334closest_uu(H,P,PP,Result):-
  335      sanity(Result=@=ref(Ref)),
  336      (copy_term(H+P,HH+PP),
  337      ((lookup_u(HH,Ref)*-> (=@=(P,PP)->(!,HH=H);
  338          (nb_setarg(1,Result,Ref),fail));(!,fail));((clause(HH,B,Ref),must_ex(B))))).
  339
  340/*
  341*/
  342
  343mpred_collect_supports(Tripples):-
  344  bagof_or_nil(Tripple, mpred_support_relation(Tripple), Tripples).
  345
  346mpred_support_relation((P,F,T)):- lookup_spft(P,F,T).
  347
  348mpred_make_supports((P,S1,S2)):-
  349  mpred_add_support(P,(S1,S2)),
  350  (mpred_ain_object(P); true),
  351  !.
  352
  353
  354pp_why:-mpred_why.
  355
  356mpred_why:-
  357  call(t_l:whybuffer(P,_)),
  358  mpred_why_1(P).
  359
  360pp_why(A):-mpred_why_1(A).
  361
  362clear_proofs:- retractall(t_l:whybuffer(_P,_Js)),color_line(cyan,1).
  363
  364
  365:- thread_local(t_l:shown_why/1).  366
  367% see pfc_why
  368
  369:- export(with_no_english/1).  370:- meta_predicate(with_no_english(*)).  371with_no_english(Goal):- setup_call_cleanup(flag('english', Was, 0),Goal,flag('english', _, Was )).
  372
  373mpred_why(P):- clear_proofs,!,with_no_english((must(mpred_why_1(P)))).
  374
  375mpred_why_1(M:P):-  atom(M),!,call_from_module(M,mpred_why_1(P)).
  376mpred_why_1(NX):- number(NX),!, trace, pfcWhy0(NX),!.
  377mpred_why_1(P):- is_list(P), !, maplist(mpred_why_1, P).
  378mpred_why_1(P):- ((callable(P), ((must_ex((mpred_why_justs(P))))))) *-> true ; mpred_why_1_fallback(P).
  379
  380mpred_why_1_fallback(NX):-  
  381  (number(NX)-> true ; clear_proofs),
  382  trace,
  383  pfcWhy0(NX),!.
  384mpred_why_1_fallback(P):- mpred_why_sub(P).
  385
  386% mpred_why_1(N):- number(N),!, call(t_l:whybuffer(P,Js)), mpred_handle_why_command(N,P,Js).
  387
  388mpred_why_justs(P):- mpred_why_justs_1a(P)*->true;forall(mpred_why_justs_1b(P),true).
  389  
  390mpred_why_justs_1a(P) :-    
  391  color_line(green,2),!,
  392  findall(Js,((no_repeats(P-Js,(justifications(P,Js))),
  393    must((color_line(yellow,1),
  394      ignore(pfcShowJustifications(P,Js)))))),Count),
  395  (Count==[]-> format("~N No justifications for ~p. ~n~n",[P]) ; true),
  396  color_line(green,2).
  397
  398mpred_why_justs_1b(P) :- term_variables(P,VarsPC), 
  399  ((call_u_no_bc(P),mpred_why_justs_1a(P))*-> 
  400  (term_variables(P,VarsAC),(VarsPC==VarsAC->!;true));
  401   mpred_why_justs_1a(P)).
  402
  403/*
  404mpred_why_justs_2(P) :-    
  405  color_line(green,2),!,
  406  findall(Js,((no_repeats(P-Js,deterministically_must(justifications(P,Js))),
  407    must((color_line(yellow,1),
  408      ignore(pfcShowJustifications(P,Js)))))),Count),
  409  (Count==[]-> format("~N No justifications for ~p. ~n~n",[P]) ; true),
  410  color_line(green,2).
  411*/
  412/*
  413
  414mpred_why_1(P):- loop_check(quietly_ex((must_ex(mpred_why_try_each(P)),color_line(green,2))),true).
  415
  416% user:mpred_why_1((user:prolog_exception_hook(A, B, C, D) :- exception_hook(A, B, C, D))).
  417% mpred_why_1((prolog_exception_hook(A, B, C, D) :- exception_hook(A, B, C, D))).
  418
  419mpred_why_try_each(MN):- strip_module(MN,_,N),number(N),!,pfcWhy0(N),!.
  420
  421mpred_why_try_each(ain(H)):-!,mpred_why_try_each(H).
  422mpred_why_try_each(call_u(H)):-!,mpred_why_try_each(H).
  423mpred_why_try_each(clause(H,B)):-!,mpred_why_try_each(H:-B).
  424mpred_why_try_each(clause(H,B,_)):-!,mpred_why_try_each(H:-B).
  425mpred_why_try_each(clause_u(P)):-!,mpred_why_try_each(P).
  426mpred_why_try_each(clause_u(H,B)):-!,mpred_why_try_each(H:-B).
  427mpred_why_try_each(clause_u(H,B,_)):-!,mpred_why_try_each(H:-B).
  428
  429mpred_why_try_each(P):- once((retractall(t_l:whybuffer(P,_)),color_line(green,2),
  430    show_current_source_location,format("~NJustifications for ~p:",[P]))),
  431    fail.
  432
  433mpred_why_try_each(P):- mpred_why_try_each_0(P),!.
  434mpred_why_try_each(P):- mpred_why_sub(P),!.
  435mpred_why_try_each(M:P :- B):- atom(M),call_from_module(M,mpred_why_try_each_0(P:-B)),!.
  436mpred_why_try_each(M:P):- atom(M),call_from_module(M,mpred_why_try_each_0(P)),!.
  437mpred_why_try_each(P :- B):- is_true(B),!,mpred_why_try_each(P ).
  438mpred_why_try_each(M:H):- strip_module(H,Ctx,P),P==H,Ctx==M,!,mpred_why_try_each(H).
  439mpred_why_try_each(_):- format("~N No justifications. ~n").
  440
  441mpred_why_try_each_0(P):- findall(Js,mpred_why_try_each_1(P,Js),Count),Count\==[],!.
  442mpred_why_try_each_0(\+ P):- mpred_why_try_each_0(~P)*->true;(call_u(\+ P),wdmsgl(why:- \+ P)),!.
  443
  444mpred_why_try_each_1(P,Js):-
  445  ((no_repeats(P-Js,deterministically_must(justifications(P,Js))),
  446    ((color_line(yellow,1), pfcShowJustifications(P,Js))))).
  447mpred_why_try_each_1(\+ P,[MFL]):- !, find_mfl(P,MFL),ansi_format([fg(cyan)],"~N    ~q",[MFL]),fail.
  448mpred_why_try_each_1( P,[MFL]):-  find_mfl(P,MFL), \+ clause_asserted(t_l:shown_why(MFL)), ansi_format([fg(cyan)],"~N    ~q",[MFL]).
  449
  450*/
  451pfcWhy0(N) :-
  452  number(N),
  453  !,
  454  t_l:whybuffer(P,Js),
  455  pfcWhyCommand0(N,P,Js).
  456
  457pfcWhy0(P) :-
  458  justifications(P,Js),  
  459  assert(t_l:whybuffer(P,Js)),                     
  460  pfcWhyBrouse(P,Js).
  461
  462pfcWhy1(P) :-
  463  justifications(P,Js),
  464  pfcWhyBrouse(P,Js).
  465
  466pfcWhyBrouse(P,Js) :-    % non-interactive
  467  pfcShowJustifications(P,Js),source_file(_,_),!.
  468
  469pfcWhyBrouse(P,Js) :- 
  470  pfcShowJustifications(P,Js),
  471  ttyflush,
  472  read_pending_chars(current_input,_,[]),!,
  473  ttyflush,
  474  % pfcAsk(' >> ',Answer),
  475  % read_pending_chars(current_input,[Answer|_],[]),!,  
  476  format('~N',[]),write('proof [q/h/u/?.?]: '),get_char(Answer),
  477  pfcWhyCommand0(Answer,P,Js).
  478
  479pfcWhyCommand0(q,_,_) :- !.
  480pfcWhyCommand0(h,_,_) :- 
  481  !,
  482  format("~n
  483Justification Brouser Commands:
  484 q   quit.
  485 N   focus on Nth justification.
  486 N.M brouse step M of the Nth justification
  487 u   up a level
  488",
  489 []).
  490
  491pfcWhyCommand0(N,_P,Js) :-
  492  float(N),
  493  !,
  494  pfcSelectJustificationNode(Js,N,Node),
  495  pfcWhy1(Node).
  496
  497pfcWhyCommand0(u,_,_) :-
  498  % u=up
  499  !.
  500
  501pfcWhyCommand0(N,_,_) :-
  502  integer(N),
  503  !,
  504  format("~n~w is a yet unimplemented command.",[N]),
  505  fail.
  506
  507pfcWhyCommand0(X,_,_) :-
  508 format("~n~w is an unrecognized command, enter h. for help.",[X]),
  509 fail.
  510
  511reset_shown_justs:- retractall(t_l:shown_why(_)),color_line(red,1).
  512  
  513pfcShowJustifications(P,Js) :-
  514  show_current_source_location,
  515  reset_shown_justs,
  516  color_line(yellow,1),
  517  format("~N~nJustifications for ~p:~n",[P]),  
  518
  519  pfcShowJustification1(Js,1),!.
  520
  521pfcShowJustification1([],_):-!.
  522pfcShowJustification1([J|Js],N) :- !,
  523  % show one justification and recurse.    
  524  reset_shown_justs,
  525  pfcShowSingleJust(N,step(1),J),!,
  526  N2 is N+1,  
  527  pfcShowJustification1(Js,N2).
  528
  529pfcShowJustification1(J,N) :- 
  530  reset_shown_justs, % nl,
  531  pfcShowSingleJust(N,step(1),J),!.
  532
  533incrStep(StepNo,Step):-arg(1,StepNo,Step),X is Step+1,nb_setarg(1,StepNo,X).
  534
  535pfcShowSingleJust(JustNo,StepNo,C):- is_ftVar(C),!,incrStep(StepNo,Step),
  536  ansi_format([fg(cyan)],"~N    ~w.~w ~w ",[JustNo,Step,C]),!.
  537pfcShowSingleJust(_JustNo,_StepNo,[]):-!.
  538pfcShowSingleJust(JustNo,StepNo,(P,T)):-!, 
  539  pfcShowSingleJust(JustNo,StepNo,P),
  540  pfcShowSingleJust(JustNo,StepNo,T).
  541pfcShowSingleJust(JustNo,StepNo,(P,F,T)):-!, 
  542  pfcShowSingleJust1(JustNo,StepNo,P),
  543  pfcShowSingleJust(JustNo,StepNo,F),
  544  pfcShowSingleJust1(JustNo,StepNo,T).
  545pfcShowSingleJust(JustNo,StepNo,(P*->T)):-!, 
  546  pfcShowSingleJust1(JustNo,StepNo,P),format('      *-> ',[]),
  547  pfcShowSingleJust1(JustNo,StepNo,T).
  548
  549pfcShowSingleJust(JustNo,StepNo,(P:-T)):-!, 
  550  pfcShowSingleJust1(JustNo,StepNo,P),format(':- ~p.',[T]).
  551 
  552pfcShowSingleJust(JustNo,StepNo,(P : -T)):-!, 
  553  pfcShowSingleJust1(JustNo,StepNo,P),format('      :- ',[]),
  554  pfcShowSingleJust(JustNo,StepNo,T).
  555
  556pfcShowSingleJust(JustNo,StepNo,(P :- T) ):- !, 
  557  pfcShowSingleJust1(JustNo,StepNo,call(T)),  
  558  pfcShowSingleJust1(JustNo,StepNo,P).
  559
  560
  561pfcShowSingleJust(JustNo,StepNo,[P|T]):-!, 
  562  pfcShowSingleJust(JustNo,StepNo,P),
  563  pfcShowSingleJust(JustNo,StepNo,T).
  564
  565pfcShowSingleJust(JustNo,StepNo,pt(P,Body)):- !, 
  566  pfcShowSingleJust1(JustNo,StepNo,pt(P)),  
  567  pfcShowSingleJust(JustNo,StepNo,Body).
  568
  569pfcShowSingleJust(JustNo,StepNo,C):- 
  570 pfcShowSingleJust1(JustNo,StepNo,C).
  571
  572fmt_cl(P):- \+ \+ (numbervars(P,126,_,[attvar(skip),singletons(true)]),write_term(P,[portray(true)])).
  573
  574unwrap_litr(C,CCC+VS):- copy_term(C,CC,VS),
  575  numbervars(CC+VS,0,_),
  576  unwrap_litr0(CC,CCC),!.
  577unwrap_litr0(call(C),CC):-unwrap_litr0(C,CC).
  578unwrap_litr0(pt(C),CC):-unwrap_litr0(C,CC).
  579unwrap_litr0(body(C),CC):-unwrap_litr0(C,CC).
  580unwrap_litr0(head(C),CC):-unwrap_litr0(C,CC).
  581unwrap_litr0(C,C).
  582
  583pfcShowSingleJust1(JustNo,StepNo,C):- unwrap_litr(C,CC),!,pfcShowSingleJust4(JustNo,StepNo,C,CC).
  584pfcShowSingleJust4(_,_,_,CC):- t_l:shown_why(C),C=@=CC,!.
  585pfcShowSingleJust4(JustNo,StepNo,C,CC):- assert(t_l:shown_why(CC)),!,
  586   incrStep(StepNo,Step),
  587   ansi_format([fg(cyan)],"~N    ~w.~w ~@ ",[JustNo,Step,fmt_cl(C)]),   
  588   pfcShowSingleJust_C(C),!.
  589
  590pfcShowSingleJust_C(C):-is_file_ref(C),!.
  591pfcShowSingleJust_C(C):-find_mfl(C,MFL),assert(t_l:shown_why(MFL)),!,pfcShowSingleJust_MFL(MFL).
  592pfcShowSingleJust_C(_):-ansi_format([hfg(black)]," % [no_mfl] ",[]),!.
  593
  594short_filename(F,FN):- atomic_list_concat([_,FN],'/pack/',F),!.
  595short_filename(F,FN):- atomic_list_concat([_,FN],swipl,F),!.
  596short_filename(F,FN):- F=FN,!.
  597
  598pfcShowSingleJust_MFL(MFL):- MFL=mfl4(VarNameZ,_M,F,L),atom(F),short_filename(F,FN),!,varnames_load_context(VarNameZ),
  599   ansi_format([hfg(black)]," % [~w:~w] ",[FN,L]).
  600pfcShowSingleJust_MFL(MFL):- ansi_format([hfg(black)]," % [~w] ",[MFL]),!.
  601
  602pfcAsk(Msg,Ans) :-
  603  format("~n~w",[Msg]),
  604  read(Ans).
  605
  606pfcSelectJustificationNode(Js,Index,Step) :-
  607  JustNo is integer(Index),
  608  nth1(JustNo,Js,Justification),
  609  StepNo is 1+ integer(Index*10 - JustNo*10),
  610  nth1(StepNo,Justification,Step).
  611
  612
  613
  614
  615
  616
  617
  618mpred_why_maybe(_,(F:-P)):-!,wdmsgl(F:-P),!.
  619mpred_why_maybe(F,P):-wdmsgl(F:-P),!.
  620mpred_why_maybe(_,P):-ignore(mpred_why_1(P)).
  621
  622mpred_why_sub(P):- trace, loop_check(mpred_why_sub0(P),true).
  623mpred_why_sub0(P):- mpred_why_2(P,Why),!,wdmsg_pretty(:-mpred_why_1(P)),wdmsgl(mpred_why_maybe(P),Why).
  624mpred_why_sub0(P):-loop_check(mpred_why_sub_lc(P),trace_or_throw_ex(mpred_why_sub_lc(P)))-> \+ \+ call(t_l:whybuffer(_,_)),!.
  625mpred_why_sub_lc(P):- 
  626  justifications(P,Js),
  627  nb_setval('$last_printed',[]),
  628  clear_proofs,
  629  assertz(t_l:whybuffer(P,Js)),
  630  mpred_whyBrouse(P,Js).
  631  
  632
  633mpred_why_sub_sub(P):-
  634  justifications(P,Js),
  635  clear_proofs,
  636  % retractall_u(t_l:whybuffer(_,_)),
  637  (nb_hasval('$last_printed',P)-> dmsg_pretty(hasVal(P)) ;
  638   ((
  639  assertz(t_l:whybuffer(P,Js)),
  640   nb_getval('$last_printed',LP),
  641   ((mpred_pp_db_justification1(LP,Js,1),fmt('~N~n',[])))))).
  642
  643nb_pushval(Name,Value):-nb_current(Name,Before)->nb_setval(Name,[Value|Before]);nb_setval(Name,[Value]).
  644nb_peekval(Name,Value):-nb_current(Name,[Value|_Before]).
  645nb_hasval(Name,Value):-nb_current(Name,List),member(Value,List).
  646nb_popval(Name,Value):-nb_current(Name,[Value|Before])->nb_setval(Name,Before).
  647
  648mpred_why1(P):-
  649  justifications(P,Js),
  650  mpred_whyBrouse(P,Js).
  651
  652% non-interactive
  653mpred_whyBrouse(P,Js):-
  654   must_ex(quietly_ex(in_cmt((mpred_pp_db_justifications(P,Js))))), !.
  655
  656% Interactive
  657mpred_whyBrouse(P,Js):-
  658  mpred_pp_db_justifications(P,Js),
  659  mpred_prompt_ask(' >> ',Answer),
  660  mpred_handle_why_command(Answer,P,Js).
  661
  662mpred_handle_why_command(q,_,_):- !.
  663mpred_handle_why_command(h,_,_):-
  664  !,
  665  format("~N
  666Justification Brouser Commands:
  667 q   quit.
  668 N   focus on Nth justification.
  669 N.M brouse step M of the Nth justification
  670 user   up a level ~n",
  671  []).
  672
  673mpred_handle_why_command(N,_ZP,Js):-
  674  float(N),
  675  !,
  676  mpred_select_justification_node(Js,N,Node),
  677  mpred_why1(Node).
  678
  679mpred_handle_why_command(u,_,_):-
  680  % u=up
  681  !.
  682
  683mpred_unhandled_command(N,_,_):-
  684  integer(N),
  685  !,
  686  format("~N~p is a yet unimplemented command.",[N]),
  687  fail.
  688
  689mpred_unhandled_command(X,_,_):-
  690 format("~N~p is an unrecognized command, enter h. for help.",[X]),
  691 fail.
  692
  693mpred_pp_db_justifications(P,Js):-
  694 show_current_source_location, 
  695 must_ex(quietly_ex(( format("~NJustifications for ~p:",[P]),
  696  mpred_pp_db_justification1('',Js,1)))).
  697
  698mpred_pp_db_justification1(_Prefix,[],_).
  699
  700mpred_pp_db_justification1(Prefix,[J|Js],N):-
  701  % show one justification and recurse.
  702  nl,  
  703  mpred_pp_db_justifications2(Prefix,J,N,1),
  704  reset_shown_justs,
  705  N2 is N+1,
  706  mpred_pp_db_justification1(Prefix,Js,N2).
  707
  708mpred_pp_db_justifications2(_Prefix,[],_,_).
  709
  710mpred_pp_db_justifications2(Prefix,[C|Rest],JustNo,StepNo):-
  711(nb_hasval('$last_printed',C)-> dmsg_pretty(chasVal(C)) ;
  712(
  713 (StepNo==1->fmt('~N~n',[]);true),
  714  sformat(LP,' ~w.~p.~p',[Prefix,JustNo,StepNo]),
  715  nb_pushval('$last_printed',LP),
  716  format("~N  ~w ~p",[LP,C]),
  717  ignore(loop_check(mpred_why_sub_sub(C))),
  718  StepNext is 1+StepNo,
  719  mpred_pp_db_justifications2(Prefix,Rest,JustNo,StepNext))).
  720
  721mpred_prompt_ask(Info,Ans):-
  722  format("~N~p",[Info]),
  723  read(Ans).
  724
  725mpred_select_justification_node(Js,Index,Step):-
  726  JustNo is integer(Index),
  727  nth1(JustNo,Js,Justification),
  728  StepNo is 1+ integer(Index*10 - JustNo*10),
  729  nth1(StepNo,Justification,Step).

 mpred_supported(+P) is semidet

succeeds if P is "supported". What this means depends on the TMS mode selected.

  737mpred_supported(P):-
  738  must_ex(get_tms_mode(P,Mode))->
  739  mpred_supported(Mode,P).

 mpred_supported(+TMS, +P) is semidet

succeeds if P is "supported". What this means depends on the TMS mode supplied.

  746mpred_supported(local,P):- !, mpred_get_support(P,_),!, not_rejected(P).
  747mpred_supported(cycles,P):-  !, well_founded(P),!, not_rejected(P).
  748mpred_supported(How,P):- ignore(How=unknown),not_rejected(P).
  749
  750not_rejected(~P):- nonvar(P),  \+ mpred_get_support(P,_).
  751not_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.

  758well_founded(Fact):- each_E(well_founded_0,Fact,[_]).
  759
  760well_founded_0(F,_):-
  761  % supported by user (axiom) or an "absent" fact (assumption).
  762  (mpred_axiom(F) ; mpred_assumption(F)),
  763  !.
  764
  765well_founded_0(F,Descendants):-
  766  % first make sure we aren't in a loop.
  767  (\+ memberchk(F,Descendants)),
  768  % find a justification.
  769  supporters_list0(F,Supporters),!,
  770  % all of whose members are well founded.
  771  well_founded_list(Supporters,[F|Descendants]),
  772  !.

 well_founded_list(+List, -Decendants) is det

simply maps well_founded over the list.

  778well_founded_list([],_).
  779well_founded_list([X|Rest],L):-
  780  well_founded_0(X,L),
  781  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].

  790supporters_list(F,ListO):- no_repeats_cmp(same_sets,ListO,supporters_list_each(F,ListO)).
  791
  792same_sets(X,Y):-
  793  flatten([X],FX),sort(FX,XS),
  794  flatten([Y],FY),sort(FY,YS),!,
  795  YS=@=XS.
  796
  797supporters_list_each(F,ListO):-   
  798   supporters_list0(F,ListM),
  799   expand_supporters_list(ListM,ListM,ListO).
  800
  801expand_supporters_list(_, [],[]):-!.
  802expand_supporters_list(Orig,[F|ListM],[F|NewListOO]):-
  803   supporters_list0(F,FList),
  804   list_difference_variant(FList,Orig,NewList),
  805   % NewList\==[],
  806   append(Orig,NewList,NewOrig),
  807   append(ListM,NewList,NewListM),!,
  808   expand_supporters_list(NewOrig,NewListM,ListO),
  809   append(ListO,NewList,NewListO),
  810   list_to_set_variant(NewListO,NewListOO).
  811expand_supporters_list(Orig,[F|ListM],[F|NewListO]):-
  812  expand_supporters_list(Orig,ListM,NewListO).
  813
  814
  815list_to_set_variant(List, Unique) :-
  816    list_unique_1(List, [], Unique),!.
  817
  818list_unique_1([], _, []).
  819list_unique_1([X|Xs], So_far, Us) :-
  820    memberchk_variant(X, So_far),!,
  821    list_unique_1(Xs, So_far, Us).
  822list_unique_1([X|Xs], So_far, [X|Us]) :-
  823    list_unique_1(Xs, [X|So_far], Us).
  824
  825% 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.

  834list_difference_variant([],_,[]).
  835list_difference_variant([X|Xs],Ys,L) :-
  836	(   memberchk_variant(X,Ys)
  837	->  list_difference_variant(Xs,Ys,L)
  838	;   L = [X|T],
  839	    list_difference_variant(Xs,Ys,T)
  840	).

 memberchk_variant(+Val, +List)

Deterministic check of membership using =@= rather than unification.

  848memberchk_variant(X, [Y|Ys]) :-
  849   (   X =@= Y
  850   ->  true
  851   ;   memberchk_variant(X, Ys)
  852   ).
  853
  854:- module_transparent(supporters_list0/2).  855supporters_list0(Var,[is_ftVar(Var)]):-is_ftVar(Var),!.
  856supporters_list0(F,OUT):-  
  857 pfc_with_quiet_vars_lock(supporters_list00(F,OUT)).
  858
  859:- module_transparent(supporters_list00/2).  860supporters_list00(F,OUT):- supporters_list1a(F,OUT) *-> true; supporters_list1b(F,OUT).
  861
  862:- module_transparent(supporters_list1a/2).  863
  864supporters_list1a(F,[Fact|MoreFacts]):-
  865  mpred_get_support_why(F,(Fact,Trigger)),
  866  triggerSupports(Fact,Trigger,MoreFacts).
  867   
  868
  869:- module_transparent(supporters_list1b/2).  870supporters_list1b(Var,[is_ftVar(Var)]):- is_ftVar(Var),!.
  871supporters_list1b(U,[]):- axiomatic_supporter(U),!.
  872supporters_list1b((H:-B),[MFL]):- !, clause_match(H,B,Ref),find_hb_mfl(H,B,Ref,MFL).
  873supporters_list1b(\+ P, HOW):- !, supporters_list00(~ P,HOW),!.
  874supporters_list1b((H),[((H:-B))]):- may_cheat, clause_match(H,B,_Ref).
  875
  876may_cheat:- fail.
  877
  878uses_call_only(H):- predicate_property(H,foreign),!.
  879uses_call_only(H):- predicate_property(H,_), \+ predicate_property(H,interpreted),!.
  880
  881clause_match(H,_B,uses_call_only(H)):- uses_call_only(H),!.
  882clause_match(H,B,Ref):- clause_asserted(H,B,Ref),!.
  883clause_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).
  884
  885find_mfl(C,MFL):- lookup_spft_match(C,MFL,ax).
  886find_mfl(C,MFL):- unwrap_litr0(C,UC) -> C\==UC -> find_mfl(UC,MFL).
  887find_mfl(C,MFL):- expand_to_hb(C,H,B),
  888   find_hb_mfl(H,B,_Ref,MFL)->true; (clause_match(H,B,Ref),find_hb_mfl(H,B,Ref,MFL)).
  889
  890find_hb_mfl(_H,_B,Ref,mfl4(_VarNameZ,M,F,L)):- atomic(Ref),clause_property(Ref,line_count(L)),
  891 clause_property(Ref,file(F)),clause_property(Ref,module(M)). 
  892find_hb_mfl(H,B,_,mfl4(VarNameZ,M,F,L)):- lookup_spft_match_first( (H:-B),mfl4(VarNameZ,M,F,L),_),!.
  893find_hb_mfl(H,B,_Ref,mfl4(VarNameZ,M,F,L)):- lookup_spft_match_first(H,mfl4(VarNameZ,M,F,L),_),ground(B).
  894find_hb_mfl(H,_B,uses_call_only(H),MFL):- !,call_only_based_mfl(H,MFL).
  895
  896/*
  897
  898
  899clause_match(H,_B,uses_call_only(H)):- uses_call_only(H),!.
  900clause_match(H,B,Ref):- clause_asserted(H,B,Ref),!.
  901
  902clause_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)))).
  903
  904clause_match0(H,B,Ref):- no_repeats(Ref,clause_match1(H,B,Ref)).
  905
  906clause_match1(H,B,Ref):- clause(H,B,Ref).
  907clause_match1(M:H,B,Ref):- !, (M:clause(H,B,Ref) ; clause_match2(H,B,Ref)).
  908clause_match1(H,B,Ref):- clause_match2(H,B,Ref).
  909
  910clause_match2(H,B,Ref):- current_module(M),clause(M:H,B,Ref),(clause_property(Ref, module(MM))->MM==M;true).
  911
  912find_mfl(C,MFL):-find_mfl0(C,MFL),compound(MFL),MFL=mfl4(VarNameZ,_,F,_),nonvar(F).
  913find_mfl0(C,MFL):- lookup_spft_match(C,MFL,ax).
  914% find_mfl0(mfl4(VarNameZ,M,F,L),mfl4(VarNameZ,M,F,L)):-!.
  915find_mfl0(C,MFL):-expand_to_hb(C,H,B),
  916   find_hb_mfl(H,B,_Ref,MFL)->true; (clause_match(H,B,Ref),find_hb_mfl(H,B,Ref,MFL)).
  917find_mfl0(C,MFL):-expand_to_hb(C,H,B),
  918   find_hb_mfl(H,B,_Ref,MFL)->true; (clause_match0(H,B,Ref),find_hb_mfl(H,B,Ref,MFL)).
  919
  920*/
  921call_only_based_mfl(H,mfl4(_VarNameZ,M,F,L)):- 
  922  ignore(predicate_property(H,imported_from(M));predicate_property(H,module(M))),
  923  ignore(predicate_property(H,line_count(L))),
  924  ignore(source_file(M:H,F);predicate_property(H,file(F));(predicate_property(H,foreign),F=foreign)).
  925
  926axiomatic_supporter(Var):-is_ftVar(Var),!,fail.
  927axiomatic_supporter(is_ftVar(_)).
  928axiomatic_supporter(clause_u(_)).
  929axiomatic_supporter(U):- is_file_ref(U),!.
  930axiomatic_supporter(ax):-!.
  931
  932is_file_ref(A):-compound(A),A=mfl4(_VarNameZ,_,_,_).
  933
  934triggerSupports(_,Var,[is_ftVar(Var)]):-is_ftVar(Var),!.
  935triggerSupports(_,U,[]):- axiomatic_supporter(U),!.
  936triggerSupports(FactIn,Trigger,OUT):-
  937  mpred_get_support(Trigger,(Fact,AnotherTrigger))*->
  938  (triggerSupports(Fact,AnotherTrigger,MoreFacts),OUT=[Fact|MoreFacts]);
  939  triggerSupports1(FactIn,Trigger,OUT).
  940
  941triggerSupports1(_,X,[X]):- may_cheat.
  942/*
  943triggerSupports1(_,X,_):- mpred_db_type(X,trigger(_)),!,fail.
  944triggerSupports1(_,uWas(_),[]):-!.
  945triggerSupports1(_,U,[(U)]):- is_file_ref(U),!.
  946triggerSupports1(_,U,[uWas(U)]):- get_source_uu((U1,U2))->member(U12,[U1,U2]),U12=@=U.
  947triggerSupports1(_,X,[X]):- \+ mpred_db_type(X,trigger(_)).
  948*/
  949
  950
  951/*
  952:-module_transparent(mpred_ain/1).
  953:-module_transparent(mpred_aina/1).
  954:-module_transparent(mpred_ainz/1).
  955*/
  956
  957% :- '$current_source_module'(M),forall(mpred_database_term(F,A,_),(abolish(pfc_lib:F/A),abolish(user:F/A),abolish(M:F/A))).
  958% :- initialization(ensure_abox(baseKB)).
  959
  960
  961% % :- set_prolog_flag(mpred_pfc_file,true).
  962% local_testing
  963
  964:- fixup_exports.  965
  966:- set_prolog_flag(expect_pfc_file,unknown).