/*
\section{Abductive cc implementation}
\begin{description}
\item[Authors] Vijay Saraswat, Philippe Codognet
\item[Bugs to:] saraswat@parc.xerox.com,codognet@minos.inria.fr
\item[Copyright:] \copyright Xerox Corporation, 1992, INRIA, 1992
\item[This File:] ab\_cc.pl
\item[Last Modified]: Sun Mar 22 09:42:28 1992
\item[Brief Description:]
   The code in this file implements a top-level interpreter
   for abductive \cc.
   \begin{itemize}
   \item Source programs are of the form:
\begin{verbatim} 
                g::a.
\end{verbatim}
        where {\tt a} (agents) is given by:
\begin{verbatim} 
             a ::= true | g | c | c -> a | c => a | a,a
\end{verbatim}
        `{\tt ,}' binds tighter than `{\tt ->}' or `{\tt =>}'.

   \item At this time constraints are given by:
\begin{verbatim} 
           c ::= X=t | c,c
\end{verbatim}
       Richer constraints will be added subsequently.

   \item  A top-level call is of the form:
\begin{verbatim} 
            abduce(Sys, Vars, Conclusion)
\end{verbatim}

         Here {\tt Sys} is an agent, {\tt Conclusion} is a constraint,
         and {\tt Vars} is a list of variables on which constraints
         can be abduced. {\tt Vars} is a list each of whose entry is
         of the form {\tt Varname-Var}, where {\tt Varname} is a constant (the
         name of the variable). The list should associate at most one
         name for a variable. The system prints out the constraints
         abduced on these variables so that running {\tt Sys} entails
         {\tt Conclusions}. Multiple explanations are generated on backtracking.

    \item The algorithm used is the following:
     \begin{itemize}
         \item Initialize {\tt Assumptions} to true. 
         \item Run {\tt Sys} as an agent, until it quiesces. 
             Note that this will reduce an abducible agent if its
             ask condition is satisfied. 
         \item If {\tt Conclusion} is entailed stop, and print
             {\tt Assumptions}.
         \item Otherwise check that the {\tt Conclusion} is still
             consistent. If so, and there is an abducible
             agent {\tt c => a}, assume  {\tt c}, and continue with {\tt a}
             added to the current quiescent system.
             When this fails, continue at (2) with the next abducible
             agent, downgrading {\tt c => a} to {\tt c -> a}.
         \end{itemize}
         The algorithm will generate explanations, not minimal explanations. 
          Minimization will be costly. Also, the same explanation may be
          generated multiple times, if there multiple derivations are possible.
    \end{itemize}
    Examples of the usage of this program are given in the files {\tt ex\_\{1,2,3\}.pl}
    in this directory. 

    To run this program, just consult this file into Prolog, and the files
    that describe your input \cc{} program.

\item[Gotchas:]
    There is no explicit syntax for existential quantification. Any variable
    occurring in the body of a definition g::a, and not occurring in the head,
    is automatically treated as an existential variable.
 
    Also, disjunction (backtracking) is not supported in this implementation.

\item[Exports:] {\tt     abduce/3.}

\item[Things to do:]
    Augment with richer constraint. 
    Think of compilation.
    How can information in the Conclusion be used to focus the search
    for assumptions?
    See the gotchas.
\end{description}
\newpage{\footnotesize\begin{verbatim}*/


:- op( 1200, xfx, ::).
:- op(1055, xfy, =>).

abduce(Body, Vars, Consequent):- abduce(Body, Vars, true, Consequent).
abduce(Body, Vars, Assumptions, Consequent) :- 
   run(Body, NewBody, true, Flag), 
   (Flag == reduced
       -> abduce(NewBody, Vars,  Assumptions, Consequent)
       ; (ask(Consequent) 
             -> format("Explanation: ~p.~n", [Assumptions])
             ; (satisfiable(Consequent), split(Body, Abs, Ask),
                try_each(Abs, Vars, Ask, Assumptions, Consequent)))).

try_each(((Abs => Agent), Rest), Vars, Ask, Assumptions, Consequent) :-
    (assume(Abs, Vars, Assumptions, Ass_1), call(Abs), 
     abduce((Agent, Ask, Rest), Vars,  Ass_1, Consequent)) ;
    try_each(Rest, Vars, ((Abs -> Agent), Ask), Assumptions, Consequent).

run(true, NewBody, Body, _Flag):- !, NewBody=Body.
run(A=B, NewBody, Body, reduced) :- !, A=B, NewBody=Body.
run((Ask -> Agent), NewBody, Body, Flag) :- !,
     (ask(Ask)
        -> (Flag=reduced, run(Agent, NewBody, Body, _Flag))
        ; (satisfiable(Ask) 
              -> NewBody = ((Ask -> Agent), Body)
              ; NewBody = Body)).
run((Ask => Agent), NewBody, Body, Flag) :- !,
     (ask(Ask)
        -> (Flag=reduced, run(Agent, NewBody, Body, _Flag))
        ; (satisfiable(Ask) 
             -> NewBody = ((Ask => Agent), Body)
              ;  NewBody = Body)).
run((G1, G2), NewBody, Body, Flag) :- !,
    run(G1, NewBody, Body1, Flag),
    run(G2, Body1, Body, Flag).
run(Goal, NewBody, Body, reduced) :- 
     (Goal :: Agent), 
     run(Agent, NewBody, Body, _Flag).

/* \end{verbatim}}  
\newpage\paragraph{Support routines.} 
{\footnotesize\begin{verbatim}
*/
assume(true, _Vars, Assumptions, Assumptions).
assume((G1, G2), Vars, Ass, Res) :- 
    assume(G1, Vars, Ass, Ass1), assume(G2, Vars, Ass1, Res).
assume((A=B), Vars, Ass, (Extname=B, Ass)) :- memchk(A, Vars, Extname).

satisfiable(Ask):- \+(\+(call(Ask))).

ask((A1, A2)):- ask(A1), ask(A2).
ask(A=B):- A==B.

memchk(A, [Name-B | _], Name) :- A == B, !.
memchk(A, [_  | R], Name) :- memchk(A, R, Name). 

split(A, Abs, Ask) :- split(A, Abs, Ask, true, true).
split(true, Abs, Ask, Abs, Ask):- !.
split((A -> B), Abs, ((A -> B), Ask), Abs, Ask) :- !.
split((A => B), ((A => B), Abs), Ask, Abs, Ask) :- !.
split((L1, L2),  Abs1, Ask1, Abs3, Ask3) :- 
  split(L1, Abs1, Ask1, Abs2, Ask2), split(L2, Abs2, Ask2, Abs3, Ask3).

/*\end{verbatim}} */