% enhanced semantics for program points (induced eager engine)

:- module(induced_eager_abs, [go/3]).

:- use_module(input_normalize_pp).
:- use_module(unification_operations, [unify/2]).
:- use_module(lub_operations, [lub/1]).
:- use_module(facts,[fact/1]).
:- use_module(domain,[domain/1]).
:- use_module(utilities, [showfacts/0]).

:- use_module(library(lists),[append/3]).


%% interface
  go(File,Goal,Domain) :-              % Goal is atomic
      retractall(fact(_)),  
      retractall(domain(_)),    
      load_file(File),
      assert(domain(Domain)),
      new(call(0,0, Goal)),
      fail.
  go(_,_,_)   :- showfacts.

%% logic

  new(Fact) :- lub(Fact), eager(Fact).

  eager(ans(Atom)) :-                       
          my_clause(Head,Body),
          fact(call(_,_,Head)),
          append(Left,[pp(_,_,Atom)|Right],Body), 
          prove(Left),
          prove_right(Right),
          new(ans(Head)).

  eager(call(_,_, Atom)) :-                       
          my_clause(Atom,Body),
          prove_right(Body),
          new(ans(Atom)).

  prove([pp(_,_,B)|Bs]) :- 
        fact(ans(B)), prove(Bs).  
  prove([unify(A,B)|Bs]) :- 
        unify(A,B), prove(Bs).  
  prove([]).

  prove_right([pp(I,J,B)|_]) :-
      new(call(I,J,B)).
  prove_right([pp(_,_,B)|Bs]) :- 
      fact(ans(B)), prove_right(Bs).  
  prove_right([unify(A,B)|Bs]) :- 
      unify(A,B), prove_right(Bs).  
  prove_right([]).





