/*----------------------------------------------------------
                      INFERENCE ENGINE
----------------------------------------------------------*/


%%% parse(-Value)
%%% =============
%%%
%%%     Value is the value corresponding to a final item
%%%     generated by parsing a sentence typed in from the
%%%     standard input. 

parse(Value) :-
    read_input,              % read a sentence
    init_chart,              % init. to an empty chart
    init_agenda(Agenda),     % init. agenda to include axioms
    exhaust(Agenda),         % process agenda until exhausted
    final_item(Goal, Value), % get form of final goal item
    item_in_chart(Goal).     % find all such items in chart


%%% init_agenda(+Axioms, -Agenda)
%%% =============================
%%%
%%%     Add indices corresponding to each of the Axioms to
%%%     an empty Agenda.

init_agenda(Agenda) :-
    initial_items(Axioms),      % get axioms
    empty_agenda(Empty),
    add_items_to_agenda(Axioms, Empty, Agenda).


%%% exhaust(+Agenda)
%%% ================
%%%
%%%     Generate all the consequences that follow from the 
%%%     indices in the Agenda.

exhaust(Empty) :-
    is_empty_agenda(Empty).

exhaust(Agenda0) :-
    pop_agenda(Agenda0, Index, Agenda1),
    add_item_to_chart(Index),
    add_consequences_to_agenda(Index, Agenda1, Agenda),
    exhaust(Agenda).


%%% add_consequences_to_agenda(+Index, +Agenda0, -Agenda)
%%% =====================================================
%%%
%%%     Add to Agenda0 all the indices that follow
%%%     immediately from Index, yielding Agenda.

add_consequences_to_agenda(Index, Agenda0, Agenda) :-
    all_solutions(Consequence, 
            consequence(Index, Consequence), 
            Consequences),
    add_items_to_agenda(Consequences, Agenda0, Agenda).


%%% consequence(Index, Consequent)
%%% =============================
%%%
%%%     Consequent is the consequent of an inference rule
%%%     whose antecedent is satisfied by the item given by
%%%     Index and other items in the chart. 

consequence(Index, Consequent) :-
    index_to_item(Index, Trigger),
    matching_rule(Trigger, RuleName, Others, Consequent, 
        SideConds),
    items_in_chart(Others, Index),
    hold(SideConds),
    notify_consequence(RuleName, Trigger, Others, 
        SideConds, Consequent).


%%% items_in_chart(+Items, +Index)
%%% =============================
%%%
%%%     All the elements of Items, generated when processing
%%%     Index from the agenda, are satisfied by stored items
%%%     in the chart.

items_in_chart([], _Index).
items_in_chart([Antecedent|Antecedents], Index) :-
    item_in_chart(Antecedent, Index),
    items_in_chart(Antecedents, Index).


%%% hold(+Conditions)
%%% =================
%%%
%%%     All the side Conditions hold.

hold([]).
hold([Cond|Conds]) :-
    call(Cond),
    hold(Conds).


%%% matching_rule(+Trigger, 
%%%               -RuleName, -Others, -Consequent, -SideConds)
%%% ==========================================================
%%%
%%%     Find an inference rule RuleName with antecedent of
%%%     the form U @ [Trigger] @ V, where Others is U @ V,
%%%     Consequent is the consequent of the rule and
%%%     SideConds are its side conditions.  (@ denotes here
%%%     list concatenation). 

matching_rule(Trigger, 
              RuleName, Others, Consequent, SideConds) :-
    inference(RuleName, Antecedent, Consequent, SideConds),
    split(Trigger, Antecedent, Others).