/*  WHY.PL  */
 
 
:- module why.
 
 
:- public trace_question/2,
          justify_question/2.
 
 
/*
SPECIFICATION
-------------
 
 
PUBLIC trace_question( Q+, Where+ ):
 
Gives a trace for question Q. The database is assumed to be in sync.
 
If Where=screen, the trace goes to the screen, if not, to a printer.
This is used in determining how the TLI interacts with the user.
 
 
PUBLIC justify_question( Q+, Where+ ):
 
Gives a justification ("why") for question Q. The database is assumed to
be in sync.
 
 
In both predicates, Q is a question-structure, as defined in EDITOR.PL.
*/
 
 
/*
IMPLEMENTATION
--------------
 
The implementation of trace_question(Q) is easy. Q is a
question-structure, so we extract its goal and variable names. The goal
is a conjunction of simple goals; we convert it into a corresponding
list of simple goals, because that's the form needed by the tracer. Then
call trace_goals.
 
 
For why_question(Q), we pass a goal-list and variable names over to
why_goals, as before. This returns an and-or-tree (format defined in
AND_OR.PL) and a success-fail indicator. We then prune the tree to
remove all those branches that do not lead to the final solution, and
then pretty-print the pruned tree with the SDO rules in WHY_SDO.SDO.
 
Note: this is a fairly primitive attempt at explanation. I designed the
tracer so that the tree would contain all the information about
execution, including failures. It should be possible to explain these
("this clause almost succeeded, but the last goal failed to unify...").
However, I haven't tried this yet. I'd like to hear from anyone who
does.
 
Note also that "why" only explains the first solution. I haven't made
it explain others. It would be possible to do so, by trapping the
generated tree just before and_or_tli in AND_OR.PL is called. However,
this is (slightly?) more complicated, and I haven't had time to
try it.
*/
 
 
:- needs
    and_list_out / 3,
    assertion / 3,
    bug / 1,
    bug / 2,
    conj_vs_list / 2,
    last / 2,
    output / 1,
    pretty / 3,
    question_vs_goal_and_vars / 3,
    trace_goals / 3,
    why_goals / 5.
 
 
trace_question( Q, Where ) :-
    question_vs_goal_and_vars( Q, Goals, Bindings ),
    conj_vs_list( Goals, GoalList ),
    trace_goals( GoalList, Bindings, Where ).
 
 
why_question( Q, Where ) :-
    question_vs_goal_and_vars( Q, Goals, Bindings ),
    conj_vs_list( Goals, GoalList ),
    why_goals( GoalList, Bindings, Tree, SF, Where ),              
    (
        SF = a
    ->
        output( 'The question was aborted.'~ )
    ;
        SF = f
    ->
        output( 'The question failed, and I can\'t explain failures.'~ )
    ;
        output( 'The question succeeded. I shall explain the first solution only:'~ ),
        prune_and_list( Tree, Tree_ ),
        pretty( and_list_out( Tree_ ), 72, prolog )
 
    ).
 
 
/*  prune_or_list( AL+, AL_- ):
        AL_ is the result of pruning AL.
 
        We eliminate from AL all but the final 'fd' branches, and
        compactify the result so that AL_ is a list of decorated
        and-nodes.
*/
prune_and_list( [], [] ) :- !.
 
prune_and_list( [H|T], [H_|T__] ) :-
    prune_decorated_and_node( H, H_ ),
    assertion( T\=[], 'prune_and_list: no fd\'s' ),
    final_fd( T, T_ ),
    prune_and_list( T_, T__ ).
 
 
/*  final_fd( AL+, AL_- ):
        AL is a list of fd branches. All but the final one correspond
        to 'ghosts' which were later failed over, so we eliminate these.                     
*/
final_fd( [fd(AL)], AL ) :- !.
 
final_fd( [_|T], AL ) :-
    final_fd( T, AL ).
 
 
/*  prune_decorated_or_node( DAN+, DAN_- ):
        DAN_ is the result of pruning DAN.
        DAN should always be a success node.
*/
prune_decorated_and_node( a(N,Goal,SF,Bindings), a(N_,Goal,SF_,Bindings) ) :-
    assertion( N\=fail(_), 'prune_and_node: goal failed', [a(N,Goal,SF,Bindings)] ),
    last( SF_, SF ),
    prune_and_node( N, Goal, Bindings, N_ ).
 
 
/*  prune_and_node( AN+, Goal+, Bindings+, AN_- ):
        AN_ is the result of pruning AN.
        AN should always be a success node.
 
        Goal is AN's goal, used only so we can include it in
        pruned not-nodes. Bindings are the variables bound when Goal
        was called, also used for not-output.
*/
prune_and_node( success(S), _, _, success(S) ) :- !.
 
prune_and_node( fail(F), Goal, Bindings, _ ) :-
    !,
    bug( 'prune_and_node: fail(_)', [fail(F),Goal,Bindings] ).
 
prune_and_node( not(N), Goal, Bindings, not(Goal,Bindings) ) :-
    !.
 
prune_and_node( N, _, _, N_ ) :-
    prune_or_list( N, N_ ).
 
 
/*  prune_or_list( OL+, OL_- ):
        OL_ is the result of pruning OL.
        OL should always contain at least one node, otherwise it
        can't lead to success.
*/
prune_or_list( [], _ ) :-
    !,
    bug( 'prune_or_list: empty list' ).
 
prune_or_list( [H], [H_] ) :-
    !,
    prune_decorated_or_node( H, H_ ).
 
prune_or_list( [_|T], T_ ) :-
    prune_or_list( T, T_ ).
 
 
/*  prune_decorated_or_node( DON+, DON_- ):
        DON_ is the result of pruning DON.
        DON should always be a success node.
*/
prune_decorated_or_node( o(N,Clause,Bindings), o(N_,Clause,Bindings) ) :-
    prune_or_node( N, N_ ).
 
 
/*  prune_or_node( ON+, ON_- ):
        ON_ is the result of pruning ON.
        ON should always be a success node.
*/
prune_or_node( success(S), success(S) ) :- !.
 
prune_or_node( fail(F), _ ) :-
    !,
    bug( 'prune_or_node: failed node', [fail(F)] ).
 
prune_or_node( N, N_ ) :-
    prune_and_list( N, N_ ).
 
 
:- endmodule.
