/* =============================== CLAUSES HANDLING ========================= */
/*             each clause is represented as a list e.g. [small(a), tall(a)]  */
/*             each clausal theory is represented as a list of lists          */
/*             a negative literal is represented as neg(small(a))             */
/* ========================================================================== */

:- module(clauses,
           [
              simplify_clauses/2  % (LClauses, LSimplified_clauses)
              			  % simplify clauses in LClauses 				   																				   		
           ]).


:- getenv('LEAR_DIR', Lear),
   atom_concat(Lear, '/list.pl', List),
   use_module(List).
   
:- dynamic has_changed/0.   


/* ============================== SIMPLIFY GROUNDED CLAUSES ================*/

simplify_clauses(LClauses, LClauses_out) :-
   simplify_clauses_iteration(LClauses, LClauses_out).
   
	
simplify_clauses_iteration(LClauses, LClauses_out) :-
   simplify_clauses_one_pass(LClauses, LClauses1),
   check_end_simplification(LClauses, LClauses1, LClauses_out).
   
check_end_simplification(LClauses, LClauses, LClauses) :-
   !.
   
check_end_simplification(_LClauses, LClauses1, LClauses_out) :-
   simplify_clauses_iteration(LClauses1, LClauses_out).
   
   
simplify_clauses_one_pass(LClauses, LClauses_out) :-
   simplify_inside_clauses(LClauses, LClauses1),
   consistant_clausal_theory(LClauses1),
   minimal_lists(LClauses1, LClauses2),
   delete_not_useful_facts(LClauses2, LClauses3),
   sort(LClauses3, LClauses_out).
   
   
delete_not_useful_facts(LClauses, LClauses_out) :-
   get_facts(LClauses, Facts),
   delete_facts(Facts, LClauses, LClauses_out).
   

	/* add each Fact as a new clause in LClauses */   
append_facts([], LClauses, LClauses) :-
   !.
   
append_facts([Fact|LFacts], LClauses, [[Fact]|LClauses1]) :-
   append_facts(LFacts, LClauses, LClauses1).
   
   
delete_facts([], LClauses, LClauses) :-
   !.
   
delete_facts([Fact|LFacts], LClauses, LClauses_out) :-
   simplify_clauses_fact(Fact, LClauses, LClauses1),
   delete_facts(LFacts, LClauses1, LClauses_out).


  /* simplify clauses knowing that Fact is true */
simplify_clauses_fact(_Fact, [], []) :-
   !.

simplify_clauses_fact(Fact, [Clause|LClauses], [Clause_out|LClauses_out]) :-
   simplify_one_clause_neg_fact(Fact, Clause, Clause_out),
   simplify_clauses_fact(Fact, LClauses, LClauses_out).


simplify_one_clause_neg_fact(Fact, Clause, Clause_out) :-
   negation(Fact, Neg_fact),
   member(Neg_fact, Clause),
   !,
   delete(Clause, Neg_fact, Clause_out).

 simplify_one_clause_neg_fact(_Fact, Clause, Clause).
  

	/* check that the list of clauses LClauses does not contain 
        an empty clause [] */

consistant_clausal_theory([]) :-
   !.

consistant_clausal_theory([[]|_LClauses]) :-
   !,
   fail.

consistant_clausal_theory([_|LClauses]) :-
   consistant_clausal_theory(LClauses).
   
 
/* ============================= MISCELENAOUS =============================== */

	/* simplify each clause of LClauses by removing duplicate facts */
simplify_inside_clauses([], []) :-
	!.
	
simplify_inside_clauses([Clause|LClauses], [Clause1|LClauses1]) :-
   sort(Clause, Clause1),
   simplify_inside_clauses(LClauses, LClauses1).
 
 
	/* get all facts included in LClauses */
get_facts([], []) :-
   !.
   
get_facts([[Fact]|LClauses], [Fact|LFacts]) :-
	!,
    get_facts(LClauses, LFacts).
    
get_facts([_Clause|LClauses], LFacts) :-
    get_facts(LClauses, LFacts). 
     
    
   /* compute the negation of an literal */
negation(neg(X), X) :-
   !.
   
negation(X, neg(X)).   
 
 
