/*
 * Gaurav S. Kc
 * [gskc@cs.columbia.edu] 13 November 1999
 *
 * Forward-chaining algorithm in Prolog
 * 
 * Constraint(s) of this system:
 *   i: the first letter of neither fact names, predicate names or
 *      constant atoms is allowed to be upper-case in the output.
 *  ii: the input is parsed and converted into HORN-form by another
 *      wrapper-C program so that this prolog program can read it in.
 *
*/

/* ------------------------------------------------------------------------------ */

?- use_module(library(lists)).
?- use_module(library(system)).

/* ------------------------------------------------------------------------------ */

main :-
  consult('input.txt'),
  buildFacts(Facts),
  buildRules(Rules),
  fc(Facts, Rules, [], CKB),
  tell('output.txt'),
  write('The facts are: '), nl,
  sort(CKB, SortedCKB), 
  disp(SortedCKB), nl,
  told, 
  halt.

buildFacts(Facts) :-
  findall(fact(Fname,Fargs), fact(Fname,Fargs), Facts).

buildRules(Rules) :-
  findall(rule(Prem,Concl), rule(Prem,Concl), Rules).

disp([]).
disp([fact(F,Args)|B]) :-
  write(F), write('('), dispArgs(Args), write(')'), nl, disp(B).

dispArgs([A]) :-
  !, write(A).
dispArgs([A|B]) :-
  write(A), write(', '), dispArgs(B).

/* ------------------------------------------------------------------------------ */

/*
 * Forward-chaining
 *
 *  -- fc(Facts, Rules, CurrentKB, CompleteKB).
 *
 * Add each fact at a time to the knowledge base
 *   - don't add if it is already in there
 *   - find the rules that have this fact/close predicate
 *       as a premise, ie the relevant Rules
 *
*/

fc([], _Rules, CKB, CKB).
fc([F|Facts], Rules, KB, CKB) :-
  addToKB(F, KB, TempNewKB),
  relevantRule(F, Rules, AddFacts, AddRules),
  addToList(AddFacts, TempNewKB, NewKB, AddedFacts),
  /* -- AddedFacts: list of facts that were just added to TempNewKB -- */
  addToList(AddedFacts, Facts, NewFacts, AddedFacts),
  addToList(AddRules, Rules, NewRules, _AddedRules),
  fc(NewFacts, NewRules, NewKB, CKB).

/* ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ */

addToKB(F, KB, KB) :- member(F,KB).
addToKB(F, KB, [F|KB]) :- \+ member(F,KB).

/* ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ */

/* -- addToList(NewList, OrigList, TotalList, AddedList) -- */
addToList([],List,List,[]).
addToList([X|Xs], List, RestList, RestAddedList) :-
  member(X, List),
  addToList(Xs, List, RestList, RestAddedList).
addToList([X|Xs], List, [X|RestList], [X|RestAddedList]) :-
  \+ member(X, List),
  addToList(Xs, List, RestList, RestAddedList).

/* ------------------------------------------------------------------------------ */

/*
 * -- relevantRule(Fact, Rules, NewFacts, NewRules).
 * 
 * relevantRule returns all the rules in "Rules" that have a premise that can
 *   unify with "Fact." Among these rules, all those that do not yet have an 
 *   empty list of premises as a result of the unification will get returned
 *   in "NewRules," and for all those rules with an empty list of premises,
 *   the conclusions [these are now known facts!] will be returned in NewFacts
 *
*/
relevantRule(_Fact, [], [], []).

relevantRule(Fact, [Rule|RestRules], RestNewFacts, RestNewRules) :-
  Rule = rule(Premises, _Conclusion),
  \+ matchPremise(Fact, Premises, _NonUnifiedPremises, _Unifier),
  /* -- "Fact" does not unify with any premise in "Premises" -- */
  relevantRule(Fact, RestRules, RestNewFacts, RestNewRules).

relevantRule(Fact, [Rule|RestRules], TotalNewFacts, TotalNewRules) :-
  Rule = rule(Premises, Conclusion),
  findall(
    (NonUnifiedPremises-Conclusion, Unifier),
      (
        matchPremise(Fact, Premises, NonUnifiedPremises, Unifier),
        \+ Premises = NonUnifiedPremises
      ),
     OldRules_Unifiers
     /*
      * -- OldRules_Unifiers is the list of premises-conclusion
      * -- Here, the premises in the list are all those except
      *        the one that originally unified with "Fact"
      *
     */
    ),
  applyUnifiersToRule(OldRules_Unifiers, TempNewRules),
  getNewFactsAndRules(TempNewRules, AddFacts, AddRules),
  addNewFacts(AddFacts, RestNewFacts, TotalNewFacts),
  addNewRules(AddRules, RestNewRules, TotalNewRules),
  addNewRules(AddRules, RestRules, TotalRestRules),
  relevantRule(Fact, TotalRestRules, RestNewFacts, RestNewRules).

/* ------------------------------------------------------------------------------ */

/*
 * -- matchPremise(Fact, Premises, NonUnifiedPremises, Unifier).
 *
 * when "Fact" unifies with some "Premise" in "Premises," the
 *    unifier is returned in "Unifier."
 *
 * unification here is complete, because "Fact" is completely
 *    instantiated -- it has no variables
 *
 * pattern matching done on Premises
 *  - case 0: empty list of premises
 *  - case 1: first premise doesn't unify, add to NonUnifiedPremises
 *  - case 2: first premise completely unifies, don't add
 *  - case 3: first premise unifies, ignore to get next unification
 *
*/
matchPremise(_Fact, [], [], []).
matchPremise(Fact, [Premise|Rest], [Premise|NewRest], Unifier) :-
  \+ unifies(Fact, Premise, _Unifier),
  matchPremise(Fact, Rest, NewRest, Unifier).
matchPremise(Fact, [Premise|Rest], Rest, Unifier) :-
  unifies(Fact, Premise, Unifier).
matchPremise(Fact, [Premise|Rest], [Premise|NewRest], Unifier) :-
  unifies(Fact, Premise, _Unifier),
  matchPremise(Fact, Rest, NewRest, Unifier).

/* ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ */

/*
 * -- unifies(Fact, Premise, Unifier).
 *
 * returns the unifier: "Unifier" if "Fact" unifies with "Premise"
 *
*/
unifies(Fact, Fact, []).
unifies(Fact, Premise, Unifier) :-
  fact(FactName, FArgs) = Fact,
  pred(FactName, PArgs) = Premise,
  length(FArgs, ArgsLength),
  length(PArgs, ArgsLength),
  argsUnify(FArgs, PArgs, Unifier).

/* ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ */

/*
 * -- argsUnify(FactArguments, PredicateArguments, Unifier).
 *
 * returns the variable substitutions in "Unifier" for all 
 *   unifications between the fact arguments [constants], and
 *   the predicate arguments [constants/variables]
 *
*/
argsUnify([], [], []).
argsUnify([FArg|RestFArgs], [FArg|RestPArgs], Unifier) :-
  argsUnify(RestFArgs, RestPArgs, Unifier).
argsUnify([FArg|RestFArgs], [var(PArg)|RestPArgs], Unifier) :-
  argsUnify(RestFArgs, RestPArgs, RestUnifier),
  Unifier = [FArg-var(PArg)|RestUnifier].

/* ------------------------------------------------------------------------------ */

/*
 * -- applyUnifiersToRule(Rules_Unifiers, NewRules).
 *
 * all the predicates for each "Rule" are unified using "Unif"
 *
*/
applyUnifiersToRule([], []).
applyUnifiersToRule([(Rule,Unif)|RestRules_Unifs], [NewRule|NewRestRules]) :-
  Rule = Prems-Conc,
  NewRule = NewPrems-NewConc,
  applyUnifiers([Conc|Prems], Unif, [NewConc|NewPrems]),
  applyUnifiersToRule(RestRules_Unifs, NewRestRules).

/* ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ */

/*
 * -- applyUnifiers(Predicates, Unifier, NewPredicates).
 *
 * all the predicates in "Predicates" are unified using "Unifier"
 *
*/
applyUnifiers([], _Unifier, []).
applyUnifiers([Pred|RestPreds], Unifier, [NewPred|NewRestPreds]) :-
  pred(PredName, PArgs) = Pred,
  pred(PredName, NewPArgs) = NewPred,
  applyUnifierToArgs(PArgs, Unifier, NewPArgs),
  applyUnifiers(RestPreds, Unifier, NewRestPreds).

/* ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ */

/*
 * -- applyUnifierToArgs(PremiseArguments, Unifier, NewPremiseArgs).
 *
 * all the premise arguments in "PremiseArguments" are unified
 *    using the unifier "Unifier"
 * 
 * pattern matching done on arguments of premise 
 *  - case 0: end of arguments, unify NewPremisArgs with []
 *  - case 1: first argument is a variable that has a unifier
 *  - case 2: first argument is a variable without a unifier
 *  - case 3: first argument is a constant
 *
*/
applyUnifierToArgs([], _Unifier, []).
applyUnifierToArgs([var(PArg)|RestPArgs], Unifier, [Const|RestNewPArgs]) :-
  member((Const-var(PArg)), Unifier),
  applyUnifierToArgs(RestPArgs, Unifier, RestNewPArgs).
applyUnifierToArgs([var(PArg)|RestPArgs], Unifier, [var(PArg)|RestNewPArgs]) :-
  \+ member((_Const-var(PArg)), Unifier),
  applyUnifierToArgs(RestPArgs, Unifier, RestNewPArgs).
applyUnifierToArgs([SomeConst|RestPArgs], Unifier, [SomeConst|RestNewPArgs]) :-
  \+ SomeConst = var(_SomeArg),
  applyUnifierToArgs(RestPArgs, Unifier, RestNewPArgs).

/* ------------------------------------------------------------------------------ */

/*
 *  -- getNewFactsAndRules(NewRules, NewFacts, AddRules).
 *
 * getNewFactsAndRules returns:
 *   i: the conclusion of all those rules that have an empty list of 
 *       premises -- the result of unifying the premises with facts in the KB
 *  ii: all the rules that don't have an empty list of premises
 *
*/

getNewFactsAndRules([], [], []).
getNewFactsAndRules([([]-Conc)|RestRules], [Conc|RestFacts], RestAddRules) :-
  !, getNewFactsAndRules(RestRules, RestFacts, RestAddRules).
getNewFactsAndRules([Rule|RestRules], RestFacts, [Rule|RestAddRules]) :-
  getNewFactsAndRules(RestRules, RestFacts, RestAddRules).

/* ------------------------------------------------------------------------------ */

/*
 * -- addNewFacts(NewFacts, OldFacts, NewTotalFacts).
 *
 * addNewFacts returns:
 *  - the result of appending all the facts in NewFacts and OldFacts
 *  - facts are stored as "pred" in NewFacts, and as "fact" in NewTotalFacts
 *
*/
addNewFacts([], Facts, Facts).
addNewFacts([pred(PredName, PArgs)|RestNewFacts], Facts, [NewFact|RestTotalFacts]) :-
  NewFact = fact(PredName, PArgs),
  append(RestNewFacts, Facts, RestTotalFacts).

/* ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ */

/*
 * -- addNewRules(NewRules, OldRules, NewTotalRules).
 *
 * addNewRules returns:
 *  - the result of appending all the rules in NewRules and OldRules
 *  - rules are stored as "premises-concl" in NewRules, 
 *      and as "rule(premises,concl)" in NewTotalRules
 *
*/
addNewRules([], Rules, Rules).
addNewRules([(Premises-Concl)|RestNewRules], Rules, [NewRule|RestTotalRules]) :-
  NewRule = rule(Premises, Concl),
  addNewRules(RestNewRules, Rules, RestTotalRules).

/* ------------------------------------------------------------------------------ */

?- main.
