:- use_module(input).

:- use_module(lub_operations, [set_union/2]).
:- use_module(facts,[fact/2]).
:- use_module(utilities, [showfacts_it/0]).

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


%% interface
  go(File,Goal) :-              % Goal is atomic
      retractall(fact(_)),      
      load_file(File),
      assert(fact(0, call(Goal))),
      iterate(0,1),
      showfacts_it.

%% control

  iterate(Prev,Curr) :- operator(Prev,Curr), fail.
  iterate(_,Current) :-
      fact(Current,_), !, Next is Current + 1, 
      iterate(Current,Next).
  iterate(_,_).

%% logic

  operator(Prev,Curr) :- 
      fact(Prev,NewAtom), 
      solve_ind(Curr,NewAtom).

  solve_ind(N,call(H)) :-
      my_clause(H,Body), 
      prove_right(N,Body),
      set_union(N,ans(H)).

  solve_ind(N,ans(A)) :-
      my_clause(H,Body), 
      append(Left,[A|Right],Body),
      fact(_,call(H)), prove(Left),
      prove_right(N,Right),
      set_union(N,ans(H)).

  prove_right(N,[B|Bs]) :- 
      set_union(N,call(B)), fail.
  prove_right(N,[B|Bs]) :- 
      fact(_,ans(B)), prove_right(N,Bs).  
  prove_right(_,[]).


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

