% this is the classic ground tp loop
% load_file(File): the logic program in File is loaded to 
%                   "my_clause(head,Body)" form;
% alphabet: represents each function symbol F/N by a template
%           symbol(f(_,...,_))



:- use_module(library(lists),[member/2]).
:- use_module(input).
:- use_module(alphabet).

go(File) :-
    load_file(File),
    alphabet,
    iterate_tp([],['$'],MinimalModel),
    show(MinimalModel).


iterate_tp(Result, [], Result) :- !.

iterate_tp(Facts,_,Result) :-
        findall(NewFact, tp(Facts,NewFact), Facts1),
        extend(Facts1,Facts,Extension,[],Diff),
        iterate_tp(Extension,Diff,Result).
     
tp(Facts,Head) :-
    my_clause(Head,Body), prove(Body,Facts),
    ground_instance(Head).

prove([X|Xs],Set) :- member(X,Set), prove(Xs,Set).
prove([],_).

extend([X|Xs],Ys,Extension,Acc,Diff) :-
        (   member(X,Ys) 
        ->
            extend(Xs,Ys,Extension,Acc,Diff)
        ;
            extend(Xs,[X|Ys],Extension,[X|Acc],Diff)
        ).
extend([],Extension,Extension,Diff,Diff).

%------------------------------------------------------
ground_instance(T) :- 
    T =.. [_PredicateSymbol|Args],
    ground_terms(Args).

ground_term(T) :- 
    symbol(T), 
    T=..[_FunctionSymbol|Args],
    ground_terms(Args).

ground_terms([]).
ground_terms([T|Ts]) :- 
    ground_term(T), ground_terms(Ts).

show([]).
show([F|Fs]) :-
        write(F), nl, show(Fs).
