% ------------------------------------------------------------
%
ground_file(FileIn, FileOut) :-
        read_clauses(FileIn,Clauses),
	ground(Clauses,GClauses),
	      write_program('Grounded Version',GClauses),
	write_clauses(FileOut,GClauses).

atomize_file(FileIn, FileOut) :-
        read_clauses(FileIn,Clauses),
	homogenize(Clauses,Clauses0),
	atomize(Clauses0,AClauses),
	      write_program('Atomized Version',AClauses),
	write_clauses(FileOut,AClauses).

% ------------------------------------------------------------
%
ground(P,GP) :-
	constants(P,Cs),
	apply_to_conjuncts1(P,Cs,instantiate_rule,GP).

% ------------------------------------------------------------
%
constants(Wff,L) :-
        Wff = (A :- B) ->
                constants(A,L1),
                constants(B,L2),
                union(L2,L1,L);
        Wff = (A , B) ->
                constants(A,L1),
                constants(B,L2),
                union(L2,L1,L);
        Wff = (A ; B) ->
                constants(A,L1),
                constants(B,L2),
                union(L2,L1,L);
        Wff = (not A) ->
                constants(A,L);
        Wff = (neg A) ->
                constants(A,L);
	Wff =.. [_|Terms] ->
	        constants1(Terms,L);
        %true ->
                error(constants:'unknown wff':Wff).

constants1(Term,L) :-
	var(Term) ->
	        L = [];
	Term = [] ->
                L = [];
        atomic(Term) ->
		L = [Term];
        Term = [H|R] ->
	        constants1(H,L1),
	        constants1(R,L2),
		union(L1,L2,L);
        Term =.. [_|Args] ->
	        constants1(Args,L);
        %true ->
                error(constants1:'unknown term':Term).

variables(Wff,L) :-
        atom(Wff) ->
		L = [];
	var(Wff) ->
	        L = [Wff];
        Wff = [H|R] ->
	        variables(H,L1),
	        variables(R,L2),
		idunion(L1,L2,L);
        Wff =.. [_|Args] ->
	        variables(Args,L);
        %true ->
                error(variables:'unknown term/wff':Wff).

% ------------------------------------------------------------
%
instantiate_rule(Constants, Rule, Instances) :-
	variables(Rule, Variables),
	setof(Rule,instantiate(Variables,Constants),InstanceList),
	list2conjuncts(InstanceList,Instances).

instantiate([],_).
instantiate([V|Vs],Cs) :-
	member(V,Cs),
	instantiate(Vs,Cs).

% ------------------------------------------------------------
%
atomize(Expr,Sxpr) :-
        atomic(Expr) ->
	       Expr = Sxpr;
        Expr = (Expr1 :- Expr2) ->
               atomize(Expr1,Sxpr1),
	       atomize(Expr2,Sxpr2),
	       Sxpr = (Sxpr1 :- Sxpr2);
        Expr = (Expr1, Expr2) ->
               atomize(Expr1,Sxpr1),
	       atomize(Expr2,Sxpr2),
	       Sxpr = (Sxpr1, Sxpr2);
        Expr = (Expr1; Expr2) ->
               atomize(Expr1,Sxpr1),
	       atomize(Expr2,Sxpr2),
	       Sxpr = (Sxpr1; Sxpr2);
        Expr = (not Literal) ->
               atomize(Literal,StrLiteral),
	       Sxpr = (not StrLiteral);
        Expr = (neg Literal) ->
               atomize(Literal,StrLiteral),
	       Sxpr = (neg StrLiteral);
        Expr = [T] ->
	       term2constant(T,S),
	       Sxpr = [S];
        Expr = [T|R] ->
	       term2constant(T,S),
	       atomize(R,U),
	       Sxpr = [S|U];
	Expr =.. [P|Args] ->
               atomize(Args,Strgs),
	       Sxpr =.. [P|Strgs];
        %true ->
	       error(atomize(Expr,Sxpr)).

term2constant(Term,Constant) :-
	term_string(Term,String),
	string_list(String,List),
	moulinette(List,List1),
	string_list(String1,List1),
	term_string(Constant,String1).

moulinette([],[]).
moulinette([X],[]) :-
	member(X,[41,32]),
	!.
moulinette([X|R1],[95|R2]) :-
	member(X,[40,41,44]),
	!,
	moulinette(R1,R2).
moulinette([X|R1],R2) :-
	member(X,[32]),
	!,
	moulinette(R1,R2).
moulinette([Z|R1],[Z|R2]) :-
	moulinette(R1,R2).

% ------------------------------------------------------------
% auxiliary procedures

apply_to_conjuncts1(Wff,Arg,P,Wff1) :-
        Wff = (A , B) ->
                apply_to_conjuncts1(A,Arg,P,A1),
                apply_to_conjuncts1(B,Arg,P,B1),
                conjoin(A1,B1,Wff1);
        %true ->
                T1 =.. [P,Arg,Wff,Wff1],
                call(T1).

list2conjuncts([],true).
list2conjuncts([X|L],C) :-
	list2conjuncts(L,C1),
	conjoin(X,C1,C).