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

abduce(Body, Vars, Consequent):- abduce(Body, Vars, true, true, true, Consequent).

abduce(Body, Vars, Asks1, Abs1, Assumptions, Consequent) :- 
   run(Body, Asks1, Abs1, Asks, Abs, Flag), 
   (Flag == reduced
       -> abduce((Asks, Abs), Vars, true, true, Assumptions, Consequent)
       ; abduce(Asks, Vars, Abs, Assumptions, Consequent)).

run(Body, Asks, Abs, Flag) :-  run(Body, true, true, Asks, Abs, Flag).
run(true, Asks, Abs, Asks, Abs, _Flag):- !.
run((G1, G2), Asks, Abs, Ask_res, Abs_res, Flag) :- !,
    run(G1, Asks, Abs, Asks1, Abs1, Flag),
    run(G2, Asks1, Abs1, Ask_res, Abs_res, Flag).
run(A=B, Asks, Abs, Asks, Abs, reduced) :- !, A=B.
run((Ask -> Body), Asks, Abs, Ask_res, Abs_res, Flag) :- !,
     (ask(Ask)
        -> (Flag=reduced, run(Body, Asks, Abs, Ask_res, Abs_res,_Flag))
        ; (Abs_res = Abs,
           (satisfiable(Ask) 
              -> Ask_res = ((Ask -> Body), Asks)
              ; Ask_res = Asks))).
run((Ask => Body), Asks, Abs, Ask_res, Abs_res, Flag) :- !,
     (ask(Ask)
        -> (Flag=reduced, run(Body, Asks, Abs, Ask_res, Abs_res,_Flag))
        ; (Ask_res = Asks,
           (satisfiable(Ask) 
              -> Abs_res = ((Ask => Body), Abs)
              ;  Abs_res = Abs))).
run(Goal, Asks, Abs, Ask_res, Abs_res, reduced) :- 
    clause((Goal :: Body)), !,
    run(Body, Asks, Abs, Ask_res, Abs_res, _Flag).
run(Goal, Asks, Abs, Asks, Abs, reduced) :-     clause((Goal)).

abduce(Asks, Vars, Abs, Assumptions, Consequent) :-
   ask(Consequent) 
      -> format("Explanation:~p.~n", [Assumptions])
      ; (satisfiable(Consequent), 
         try_each(Abs, Vars, Asks, Assumptions, Consequent)).

try_each(((Abs => Body), Rest), Vars, Asks, Assumptions, Consequent) :-
    (assume(Abs, Vars, Assumptions, Ass_1), 
     abduce(Body, Vars, Asks, Rest, Ass_1, Consequent)) ;
   try_each(Rest, Vars, ((Abs -> Body), Asks), Assumptions, Consequent).

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), A=B.

satisfiable(Ask):- \+(\+(call(Ask))).
ask((A1, A2)):- ask(A1), ask(A2).
ask(A=B):- A==B.

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