/* ========================================================================== */
/*                              TERMS HANDLING                                */
/* ========================================================================== */

:- module(term,
          [  
		   refresh_variables_list/2,

             make_variables_anonymous/2,
		   make_variables_syntactically_anonymous/2,

		
             instance_of/2,
	        atom_arity/2,
             similar_terms/2,
             get_arguments_term/2,
             arg_atom_list/2,
             arg_atom/2,
              	                  /* get the Kth argument of the tupple T */
		   get_atom_args/2,
		   get_kth_argument_tuple/3,


			  						% Tuple, 
			  						% K
			  						% Arg
          
            delete_nth_arg/3,    /* delete_nth_arg(N, Atom, Atom1)
          						         delete the Nth argument of Atom 
          						         resulting in Atom1 */

		 replace_nth_atom/4,
           replace_nth_atom_var/4,
           replace_term/4,
           share_variable/2,
           share_variable_list_term/2,

           partially_ground/1,
           get_partially_grounded_atoms_list/2,

		                      /* =========== VARIABILIZATIONS ============= */
           all_variabilizations_atom_types/2,
		 all_variabilizations_atom/2,      % (Atom, Variabilized_atoms)
		 variabilize_atoms_values/2,
           variabilize_term/3,
           variabilize_list/3,
           variabilize_literal/3,
           variabilize_atom/2,
           variabilize_atom_structurally/2,
           variabilize_atom_structurally_exclusion/3,

           check_negated_atom/2		
          ]
         ). 

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


/* ============================ COMPARING TERMS ============================= */

	/* check whether two terms are equivalent if we do not take into 
      account the name of the variables and the order of the elements */
similar_terms(T1, T2) :-

  duplicate_term(T1, TA),
  numbervars(TA, 0, _, [functor_name('$$var')]),
  sort(TA, T),

  duplicate_term(T2, TB),
  numbervars(TB, 0, _, [functor_name('$$var')]),
  sort(TB, T).   


/* ============================= TYPE OF TERMS ============================== */

	/* check whether the term X contains at least one atomic argument */
partially_ground(X) :-
   ground(X),
   !.
   
partially_ground(X) :-
   var(X),
   !,
   fail.   
   
partially_ground([X|_]) :-
   partially_ground(X),
   !.
   
partially_ground([_|L]) :-
   !,
   partially_ground(L).
   
partially_ground(X) :-
   X =..[_Functor|LArgs],
   partially_ground(LArgs).   

   
/* ======================== HANDLING ARGUMENTS OF A TERM ==================== */	 

	/* get the list of arguments of a (possibly compound) Term */
get_arguments_term(X, [X]) :-
   var(X),
   !.

get_arguments_term([], []) :-
   !.

	% get arguments of a list
get_arguments_term([X|L], LArgs) :-
  !,
  get_arguments_term(X, L1),
  get_arguments_term(L, L2),
  append(L1, L2, LArgs).

	% compound term
get_arguments_term(T, LArgs) :-
   compound(T),
   !,
   T=..[_|L],
   get_arguments_term(L, LArgs).

	% simple argument
get_arguments_term(X, [X]).


	/* check if X is an argument of an atom in List */
arg_atom_list(_X, []) :-
   !,
   fail.

arg_atom_list(X, [Atom|_LAtoms]) :-
   arg_atom(X, Atom),
   !.

arg_atom_list(X, [_Atom|LAtoms]) :-
   arg_atom_list(X, LAtoms).


	/* check if X is an argument of Atom */
arg_atom(X, Atom) :-
   Atom =..[_|LArgs],
   member_similar(X, LArgs, strictly).


	/* delete the Nth argument of Atom resulting in Atom1 */
delete_nth_arg(N, Atom, Atom1) :-
   Atom=..[Pred|LArgs],
   delete_nth(N, LArgs, LArgs1),
   Atom1=..[Pred|LArgs1].

	/* get all arguments of an atom */
get_atom_args(Atom, LArgs) :-
   Atom=..[_|LArgs].
   
   
    /* get the Kth argument of the tupple T */ 
get_kth_argument_tuple(','(Arg, _Tuple), 1, Arg) :-
   !.
   
get_kth_argument_tuple(Arg, 1, Arg) :-
   !.   
   
get_kth_argument_tuple(','(_Arg, Tuple), K, Arg) :-
   K1 is K-1,
   get_kth_argument_tuple(Tuple, K1, Arg).
 

        /* dans T1, remplace Y par X, resultat dans T2
           (conserver l'ordre des clauses !) */
replace_term(X, Y, T1, T2) :-
   var(T1),
   !,
   replace_simple_term(X, Y, T1, T2).

replace_term(_X, _Y, [], []) :-
        !.

replace_term(X, Y, [T1|L1], [T2|L2]) :-     % list
        !,
        replace_term(X, Y, T1, T2),
        replace_term(X, Y, L1, L2).

replace_term(X, Y, T1, T2) :-						% T1 constante
	\+ compound(T1),
   !,
   replace_simple_term(X, Y, T1, T2).

replace_term(X, Y, T1, T2) :-						% terme compose
    T1 =..[Pred|LArgs1],
    !,
    replace_term(X, Y, LArgs1, LArgs2),
    T2 =..[Pred|LArgs2].


replace_simple_term(X, Y, T1, X) :-
   T1 == Y,             % ne pas mettre replace_simple_term(X, Y, Y, X) !!!                          
   !.

replace_simple_term(_X, _Y, T1, T1).              % pas de remplacement


	/* replace the Nth argument of Atom by X */
replace_nth_atom(N, X, Atom, Atom1) :-
   Atom =..[Pred|L],
   replace_nth_list(N, X, L, L1),
   Atom1=..[Pred|L1].


	/* replace the Nth argument of Atom by X (if the Nth argument is a var) */
replace_nth_atom_var(N, X, Atom, Atom1) :-
   arg(N, Atom, Y),
   var(Y),
   !,
   Atom =..[Pred|L],
   replace_nth_list(N, X, L, L1),
   Atom1=..[Pred|L1].

replace_nth_atom_var(_N, _X, Atom, Atom).
   

/* ========================== CHECKING SHARE VARIABLES ====================== */

   /* check whether Term1 and Term2 share at least a variable */
share_variable(Term1, Term2) :-
   term_variables(Term1, L1),
   term_variables(Term2, L2),
   have_similar_element(L1, L2, strictly).


   /* check whether Term share a variable with at least a
      Term of List_terms */
share_variable_list_term([], _Term) :-
   !,
   fail.

share_variable_list_term([Term1|_List_terms], Term) :-
   share_variable(Term1, Term),
   !.

share_variable_list_term([_Term1|List_terms], Term) :-
   share_variable_list_term(List_terms, Term).


/* ========================== VARIABILIZATION OF TERMS ====================== */

/* --- VARIABILIZATIONS OF AN ATOM CONSIDERING THE TYPES OF ITS ARGUMENTS --- */

/* return all possible variabilizations of an atom according the types
           of its arguments. Here the arguments are types. 
           ex) p(object, person, person) will give the variabilizations :
               {p(X, Y, Z)}, p(X, Y, Y)}, while
               p(object, object, object) will give the variabilizations :
               {p(X,Y,Z), p(X,X,Y), p(X,Y,X), p(X,Y,Y), p(X,X,X)}
           Only the variables of same type can be equalized */ 
          
all_variabilizations_atom_types(Atom_types, Variabilized_atoms) :-
	 Atom_types =..[Name|LTypes],
     detect_positions_types(LTypes, LTypes_positions),
     build_variabilizations_positions_types(LTypes_positions, LTypes_vars_positions),
     cross_product_lists_of_lists(LTypes_vars_positions, LLTypes_vars_positions),
     build_atoms_types(LLTypes_vars_positions, Name, Variabilized_atoms).


build_atoms_types([], _Name, []) :-
   !.

build_atoms_types(
                  [LTypes_vars_positions|LLTypes_vars_positions],
                  Name,
                  [Atom|LAtoms]
                 ) :-
   build_final_atom(LTypes_vars_positions, Name, Atom),
   build_atoms_types(LLTypes_vars_positions, Name, LAtoms).


	/* build all variabilizations according to types and positions of arguments
       ex) Type_positions is [([object, [1,3], person, [2]) */
build_variabilizations_positions_types([], []) :-
   !.

build_variabilizations_positions_types(
                                       [(Type, LPositions)|LTypes_positions], 
                                       [LLVars_positions|LLLVars_positions]
                              ) :-
    build_variabilizations_positions_one_type(LPositions, Type, LLVars_positions),
    build_variabilizations_positions_types(LTypes_positions, LLLVars_positions).


build_variabilizations_positions_one_type(LPositions, Type, LLVars_positions) :-
    distribute_positions(LPositions, [[]], Arguments_sets), 
    build_variabilizations_positions(Arguments_sets, Type, LLVars_positions).


	/* */
build_variabilizations_positions([], _Type, []) :-
   !.

build_variabilizations_positions(
                                 [Arguments_set|LArguments_sets],
                                 Type,
                                 [LVars_positions1|LLVars_positions]
                                ) :-
    build_variables_positions(Arguments_set, Type, 0, LVars_positions),
   	sort_vars_positions(LVars_positions, LVars_positions1),
    build_variabilizations_positions(LArguments_sets, Type, LLVars_positions).


	/* detect the positions of arguments of same types in LTypes */

detect_positions_types(LTypes, LTypes_positions) :-
   detect_positions_types1(LTypes, 1, [], LTypes_positions).

detect_positions_types1([], _Position, LTypes_positions, LTypes_positions) :-
   !.
													% Type already seen
detect_positions_types1(
                        [Type|LTypes], 				% list of Types
                        Position,					% position of Type
                        LTypes_positions,           % types and positions seen
                        LTypes_positions_out        % final types and positions
                        ) :-
   select((Type, LPositions), LTypes_positions, LTypes_positions1),
   !,
   insert_last(Position, LPositions, LPositions1),
   Position1 is Position + 1,
   detect_positions_types1(LTypes, Position1, 
                     [(Type, LPositions1)|LTypes_positions1],
                     LTypes_positions_out).

													% Type never seen
detect_positions_types1(
                        [Type|LTypes], 				% list of Types
                        Position,					% position of Type
                        LTypes_positions,           % types and positions seen
                        LTypes_positions_out        % final types and positions
                        ) :-
   Position1 is Position + 1,
   detect_positions_types1(LTypes, Position1, 
                     [(Type, [Position])|LTypes_positions],
                     LTypes_positions_out).   
   

/*  VARIABILIZATIONS OF AN ATOM WITHOUT CONSIDERING THE TYPES OF ITS ARGUMENT */   

		/* return all possible variabilizations of an atom. 
             for example the variabilizations of p(a, b) are 
             {p(X,Y), p(X,X}.
            Note that ones does not take int account the binds
           of the initial atom. So p(a,b) will lead to the same
          set of variabilizations */    
all_variabilizations_atom(Atom, Variabilized_atoms) :-
	 functor(Atom, Name, N),
     create_numbers_list(N, Positions),
     distribute_positions(Positions, [[]], Arguments_sets),
     build_variabilized_atoms(Arguments_sets, Name, Variabilized_atoms).


	/* build variabilized atoms from sets of arguments */
build_variabilized_atoms([], _Name, []) :-
   !.
 
build_variabilized_atoms(
                         [Arguments_set|Arguments_sets], 
                          Name,
                         [Atom|Atoms]
                        ) :-
   build_atom(Name, Arguments_set, Atom),
   build_variabilized_atoms(Arguments_sets, Name, Atoms).


	/* build a variabilized Atom from this Arguments_set */
build_atom(Name,Arguments_set, Atom) :-
	build_variables_positions(Arguments_set, any, 0, LVars_positions),
    build_final_atom(LVars_positions, Name, Atom).
 

build_final_atom(LVars_positions, Name, Atom) :-
   	sort_vars_positions(LVars_positions, LVars_positions1),
   	get_consts(LVars_positions1, LConsts),
   	Atom1=..[Name|LConsts],
    variabilize_atom_structurally(Atom1, Atom).


get_consts([], []) :-
   !.

get_consts([(_Pos, Const)|LPositions], [Const|LConsts]) :-
   get_consts(LPositions, LConsts). 

	/* sort the list [(3, value1), (1, value2), (2, value)] according to the
       the first element of (N, value) */
sort_vars_positions([], []) :-
   !.

sort_vars_positions([(X,Y)|L], Lsort) :-
   sort_vars_positions(L, L1),
   insert((X,Y), L1, Lsort).

insert(E, [], [E]) :-
   !.

insert((X,Y), [(A,B)|L], [(X,Y), (A,B)|L]) :-
	X =< A,
    !.

insert((X,Y), [(A,B)|L], [(A,B)|L1]) :-
   insert((X,Y), L, L1).   

	/* build a list of variables and the positions they have in the 
       head of a future atom. ex) [(X,1), (Y,2), (X,3)] for p(X,Y,X) */
build_variables_positions([], _Var_name, _N, []) :-
   !.

build_variables_positions([LPositions|LLPositions], Var_name,
                           N, LVars_positions) :-
   atom_number(AN, N),
   atom_concat(Var_name, AN, Var_name1),
   build_same_variable_positions(LPositions, Var_name1, LVars_positions1),
   N1 is N+1,
   build_variables_positions(LLPositions, Var_name, N1, LVars_positions2),
   append(LVars_positions1, LVars_positions2, LVars_positions).

	
build_same_variable_positions([], _Var_name, []) :-
   !.

build_same_variable_positions(
                              [Position|LPositions], 
                               Var_name, 
                              [(Position, Var_name)|LVars_positions]
                             ) :-
   build_same_variable_positions(LPositions, Var_name, LVars_positions).


		/* distribute positions of arguments in a set of lists,
             each list containing the positions of identical arguments */
distribute_positions([], Positions_sets, Positions_sets) :-
   !.

distribute_positions([Position|Positions], Positions_sets, Positions_sets1) :-
   distribute_positions(Positions, Positions_sets, Positions_sets2),
   distribute_one_position(Position, Positions_sets2, Positions_sets1).


		/* distribute one argument position in sets of lists,
             each list representing positions of identical arguments */
distribute_one_position(_Position, [], []) :-
   !.

distribute_one_position(
                        Position, 
                        [Positions_set|Positions_sets], 
                         Positions_sets1
                       ) :-
	distribute_one_position_one_set(Position, Positions_set, Positions_sets2),
    distribute_one_position(Position, Positions_sets, Positions_sets3),
    append(Positions_sets2, Positions_sets3, Positions_sets1).


		/* return all possibilities of addding position 
             to exactly one List of Positions_set */   

distribute_one_position_one_set(
                                Position, 
                                Positions_set, 
                                Positions_sets
                               ) :-
   findall(Positions_sets1, 
           insert_one_position_one_set(Position, Positions_set, Positions_sets1), 
           Positions_sets).
         
   
insert_one_position_one_set(
                                  Position, 
                                  [], 
                                  [[Position]]
                           ) :-
   !.


insert_one_position_one_set(
                                  Position, 
                                  [List_positions|Positions_set], 
                                  [[Position|List_positions]|Positions_set]
                            ).

insert_one_position_one_set(
                                  Position, 
                                  [List_positions|Positions_set], 
                                  [List_positions|Positions_set1]
                            ) :-
   insert_one_position_one_set(Position, Positions_set, Positions_set1).


   

	% Mode is either 'new' to create new variables or 
	% 'keep' to keep current variables 
	 						
variabilize_term(X, _Y, _Mode) :-
   atomic(X),
   !.
 
variabilize_term(X, _Y, new) :-
   var(X),
   !.

variabilize_term(X, X, keep) :-
   var(X),
   !.   
   
variabilize_term(L, L_out, Mode) :-
    is_list(L),
    !,
    variabilize_list(L, L_out, Mode).
    
variabilize_term(X, X_out, Mode) :-
   compound(X),
   !,
   variabilize_literal(X, X_out, Mode).
   
   
variabilize_list([], [], _Mode) :-
   !.
   
variabilize_list([X|L],[X_out|L_out], Mode) :-
   variabilize_term(X, X_out, Mode),
   variabilize_list(L, L_out, Mode).
 
 
variabilize_literal(X, X_out, Mode) :-
    X =..[Pred|LArgs],
    variabilize_list(LArgs, LArgs_out, Mode),
    X_out =..[Pred|LArgs_out].


variabilize_atom(Term, Term_out) :-
   functor(Term, Pred, N),
   functor(Term_out, Pred, N).
   
   
   /* each constant of Term is replaced by a variable */
variabilize_atom_structurally(Atom, Atom_out) :-
   Atom=..[Funct|LArgs],				
   replace_consts_by_vars(LArgs, [], LArgs_out),
   Atom_out=..[Funct|LArgs_out].


   /* each constant of Atom that is not in the exclusion List 
      is replaced by a variable */
variabilize_atom_structurally_exclusion(Atom, LExclusion, Atom_out) :-
   Atom=..[Funct|LArgs],				
   replace_consts_by_vars_exclusion(LArgs, [], LExclusion, LArgs_out),
   Atom_out=..[Funct|LArgs_out].
   
   

	/* variabilize the list of atoms by replacing each encountered constant
	   by a new var */
variabilize_atoms_values([], []) :-
   !.
   
variabilize_atoms_values([Atom|LAtoms], [Atom1|LAtoms1]) :-
   Atom=..[Functor|LArgs],
   variabilize_values(LArgs, LArgs1),
   Atom1=..[Functor|LArgs1],
   variabilize_atoms_values(LAtoms, LAtoms1). 
   
	/* variabilize the list of constants by replacing each constant
	   by a new var */
variabilize_values([], []) :-
   !.
   
variabilize_values([X|L], [_Var|L1]) :-
   atomic(X),
   !,
   variabilize_values(L, L1).    
   
variabilize_values([X|L], [X|L1]) :-
   variabilize_values(L, L1). 


	/* each constant of LConst is replaced by a variable */
replace_consts_by_vars_exclusion([], _, _LExclusion, []) :-
   !.	
	
replace_consts_by_vars_exclusion([Const|LConsts], LConsts_vars, 
                                 LExclusion, [Var|LVars]) :-
   member((Const, Var), LConsts_vars),    % Const already seen
   !,
   replace_consts_by_vars_exclusion(LConsts, LConsts_vars, LExclusion, LVars).
   
replace_consts_by_vars_exclusion([Const|LConsts], LConsts_vars, 
                                  LExclusion, [Const|LVars]) :-
   member(Const, LExclusion),
   !,
   replace_consts_by_vars_exclusion(LConsts, [(Const, Const)|LConsts_vars], 
                                    LExclusion, LVars).   

replace_consts_by_vars_exclusion([Const|LConsts], LConsts_vars, 
                                  LExclusion, [Var|LVars]) :-
   replace_consts_by_vars_exclusion(LConsts, [(Const, Var)|LConsts_vars], 
                                    LExclusion, LVars).   


	/* each constant of LConst is replaced by a variable */
replace_consts_by_vars([], _, []) :-
   !.	
	
replace_consts_by_vars([Const|LConsts], LConsts_vars, [Var|LVars]) :-
   member((Const, Var), LConsts_vars),    % Const already seen
   !,
   replace_consts_by_vars(LConsts, LConsts_vars, LVars).
   
replace_consts_by_vars([Const|LConsts], LConsts_vars, [Var|LVars]) :-
   replace_consts_by_vars(LConsts, [(Const, Var)|LConsts_vars], LVars).   
     

/* ============================= MISCELLENAOUS ============================== */

	/* make that each element of a list of terms do not share
       variable with an another element */ 
refresh_variables_list([], []) :-
   !.

refresh_variables_list([Term|LTerm], [Term1|LTerm1]) :-
   copy_term(Term, Term1),
   refresh_variables_list(LTerm, LTerm1).


	/* check if Term is an instance of Pattern 
        (without instantiating Pattern) */
instance_of(Term, Pattern) :- 
   copy_term(Pattern, Pattern1),
   Term = Pattern1.


	/* build an atom with the name of a predicate and its arity */
atom_arity(Atom, Pred) :-
   functor(Atom, Pred1, Arity),
   atom_number(Atom_arity, Arity),
   atom_concat(Pred1, '/', Pred2),
   atom_concat(Pred2, Atom_arity, Pred).


    /* get the grounded atoms (facts) present in list of clauses */
get_facts_from_clauses(LClauses, LFacts) :-
   get_facts(LClauses, LFacts1),
   sort(LFacts1, LFacts).

   /* get the grounded atoms (facts) present in list of clauses */
get_facts([],[]) :-
   !.
   
get_facts([Clause|LClauses], LFacts) :-
   get_facts_one_clause(Clause, LFacts1),
   get_facts(LClauses, LFacts2),
   append(LFacts1, LFacts2, LFacts).
   
   
get_facts_one_clause([], []) :-
   !.
   
get_facts_one_clause([Atom|LAtoms], [Atom1|LAtoms1]) :-
   ground(Atom),
   !,
   check_negated_atom(Atom, Atom1),
   get_facts_one_clause(LAtoms, LAtoms1).
   
get_facts_one_clause([_Atom|LAtoms], LAtoms1) :-
   get_facts_one_clause(LAtoms, LAtoms1).      
   
   
check_negated_atom(not(Atom), Atom) :-
   !.
   
 check_negated_atom(Atom, Atom).
 
 			   
/* ========================================================================== */
/*                       TERMS CONTAINED IN A LIST                            */
/* ========================================================================== */  

	/* get all grounded atoms appearing in the list L */
get_partially_grounded_atoms_list([], []) :-
   !.
   
get_partially_grounded_atoms_list([Atom|LAtoms], [Atom|LAtoms_out]) :-
	partially_ground(Atom),
	!,
	get_partially_grounded_atoms_list(LAtoms, LAtoms_out).
	
get_partially_grounded_atoms_list([_Atom|LAtoms], LAtoms_out) :-
	get_partially_grounded_atoms_list(LAtoms, LAtoms_out).	      	     
     	   

/* =============================== UTILITIES ================================ */

	/* make anonymous all variables of an atom */
make_variables_anonymous(Atom, Atom_out) :-
   Atom=..[Pred|LArgs],
   anonymous_variables(LArgs, LArgs_out),
   Atom_out=..[Pred|LArgs_out].


anonymous_variables([], []) :-
   !.

anonymous_variables([_Var|LVars], [_|LVars1]) :-
   anonymous_variables(LVars, LVars1).


	/* replace each variable by the atom '_' */
make_variables_syntactically_anonymous(Atom, Atom_out) :-
   Atom=..[Pred|LArgs],
   syntactically_anonymous_variables(LArgs, LArgs_out),
   Atom_out=..[Pred|LArgs_out].


syntactically_anonymous_variables([], []) :-
   !.

syntactically_anonymous_variables([_Var|LVars], ['_'|LVars1]) :-
   syntactically_anonymous_variables(LVars, LVars1).



	/* create N empty lists */
create_empty_lists(0, []) :-
   !.

create_empty_lists(N, [[]|L]) :-
   N1 is N-1,
   create_empty_lists(N1, L).

	/* create a list of successive number (starting from one) */

create_numbers_list(N, L) :-
   create_numbers_list1(N, L1),
   reverse(L1, L).

create_numbers_list1(0, []) :-
   !.

create_numbers_list1(N, [N|L]) :-
   N1 is N-1,
   create_numbers_list1(N1, L).

/* ============================= END OF LISTING ============================= */                       
