/* ========================================================================== */
/*                            TOP DOWN EXPLORATION                            */
/* ========================================================================== */
/*  Author              : Dominique BOUTHINON (db@lipn.univ-paris13.fr)       */            
/*                        LIPN Universite Paris 13 (France)                   */
/*                                                                            */
/* ========================================================================== */
/* History :										                          */
/*   - bad concept about "linked" atoms is fixed                              */
/*     (16/11/12)                                                             */       
/*   - we no more specialize a hypothesis by adding a constraint of equality  */
/*     between two variales. So we ensure that the hypothesis is compatible+  */
/*     with the seed                                                          */
/*     (17/10/12)                                                             */
/* ========================================================================== */


:- module(
          specialization7,
          [
            couv_sup_LC/2
          ]
          ).

:-
   getenv('LEAR_DIR', Lear),
   atom_concat(Lear, '/utilities_lear11.pl', Utilities),
   use_module(Utilities),
   atom_concat(Lear, '/domains.pl', Domains),
   use_module(Domains),
   atom_concat(Lear, '/term.pl', Term),
   use_module(Term),
   atom_concat(Lear, '/list.pl', List),
   use_module(List),
   atom_concat(Lear, '/manage_examples2.pl', Manage),
   use_module(Manage).

/* ========================= SPECIALIZE A LIST OF HYPOTHESIS ================ */

couv_sup_LC(LHyp, LHyp) :- 
   learn:first_step,             % do nothing at the firs step
   !. 

        /* couverture superieure des conjonctions de LC */
couv_sup_LC([], []) :-
        !.

couv_sup_LC(LHyp, LHyp_out):-
        getenv('LEAR_DIR', Lear),
        atom_concat(Lear, '/miscellaneous.pl', Misc),
        use_module(Misc),
        specialize_hypothesis(LHyp, LHyp_out).

       /* LHyp_out contains all specilizations of the list of hypotheses LHyp */
specialize_hypothesis([], []) :-
        !.

specialize_hypothesis([Hyp|LHyp], LHyp_out) :-
        specialize_one_hypothesis(Hyp, LHyp1),
        specialize_hypothesis(LHyp, LHyp2),
        append(LHyp1, LHyp2, LHyp_out).

        /* LHyp contains the maximally general specializations of
           the hypothesis Hyp */
specialize_one_hypothesis((Id, Hyp, Seed), LHyp) :-
	    
   	      % add an atom
      current_option(linked_clauses, Linked),
      specialize_tables(Linked, Hyp, Seed, LLHyp_tab_seed),
      length(LLHyp_tab_seed, T),    
	   build_maximal_specializations(1, T, Seed, LLHyp_tab_seed,LHyp1),  


	       % replace a variable by a constant (choosen in seed example)
      specialize_constants_hyp(Hyp, Seed, LHyp2),

   	append(LHyp1, LHyp2, LHypA),
   	learn:recorded(Id, Infos_mother_hypothesis, Reference),
      create_new_hypotheses(1, Id, Infos_mother_hypothesis, LHypA, LHyp),
      learn:erase(Reference).


 	/* create the new hypotheses */
 create_new_hypotheses(_N, _Id, _Infos, [], []) :-
    !.

 create_new_hypotheses(
 				 	N, 		           % Nth specializations
 				   Id,                  % identifier of mother hypothesis
 					Infos_hypothesis,    % information about mother
 					                     %  hypothesesis
 					[(Hyp, Seed)|LHyp],  % list of hypotheses,
 					[(New_id, Hyp, Seed) | LHyp_out]
 	                 ) :-
    create_new_hypothesis(Id, N, Infos_hypothesis, New_id),
    N1 is N+1,
    create_new_hypotheses(N1, Id, Infos_hypothesis, LHyp, LHyp_out).

	/* create a new hypothesis */
create_new_hypothesis(Identifier, N, Infos_hypothesis, New_identifier) :-
   build_hypothesis_identifier(Identifier, N, New_identifier),
   learn:recorda(New_identifier, Infos_hypothesis).


build_hypothesis_identifier(Id, N, Id_new_hyp) :-
   atom_concat(Id, '_', Id1),
   atom_number(AN, N),
   atom_concat(Id1, AN, Id_new_hyp).


        /* specialize all tables of the hypothesis Hyp from tables */
specialize_tables(_Linked, _Hyp, [], []):-
        !.

        /* returns all maximal specializations of the tables */
specialize_tables(
							Linked,
                  	Hyp,
                  	[Tab|LTab],
                  	[LHyp_tab_seed|LLHyp_tab_seed]
                 ):-
   specialize_one_table(Linked, Hyp, Tab, LHyp_tab_seed),
   specialize_tables(Linked, Hyp, LTab, LLHyp_tab_seed).


   /* return LTab_hyp_seed that contains all maximal
      specializations of Hyp wrt table Tab_seed */
specialize_one_table(Linked, Hyp, Tab, LHyp_tab_seed) :-
   specialize_atoms_hyp(Linked, Hyp, Tab, LHyp_tab_seed1),
   sort(LHyp_tab_seed1, LHyp_tab_seed2),
   discard_similar_elements(LHyp_tab_seed2, LHyp_tab_seed, structurally).


/* =================== SPCECIALIZE BY ADDING AN ATOM ======================== */
/*            (possibility of Linked restriction for the added atom)          */
/* ========================================================================== */


 /* Specialize Hyp by moving an atom from Tab_seed to Hyp  */
specialize_atoms_hyp(_Linked, _Hyp, [], []) :-
   !.

specialize_atoms_hyp(Linked, Hyp, [Possibility|LPossibility], LHyp_tab_seed) :-
   add_one_atom(Linked, Hyp, 1, Possibility, [], LHyp_tab_seed1),
   specialize_atoms_hyp(Linked, Hyp, LPossibility, LHyp_tab_seed2),
   append(LHyp_tab_seed1, LHyp_tab_seed2, LHyp_tab_seed).


    /* get all specializations of Conj built by adding to Conj the Nth atom
       from Possibility */
add_one_atom(_Linked, _Conj, N, Possibility, LResults, LResults) :-
   length(Possibility, N1),
   N > N1,
   !.

add_one_atom(
             Linked,          % true = only linked clauses in hypotheses
             Conj,
             N,
             Possibility,
             LResults,
             LResults_out
             ) :-
        select_nth(N, Possibility, (Atom, IAtom), Possibility1),
        get_mode_arguments(Atom, LModes, LTypes),
        Atom =..[_Pred|LArgs],
        build_atoms_modes(Linked, Conj, (Atom, IAtom),
                          LArgs, LModes, LTypes, Possibility1, LResults1),
        !,  
        N1 is N+1,
        append(LResults, LResults1, LResults2),
        add_one_atom(Linked, Conj, N1, Possibility, LResults2, LResults_out).

add_one_atom(
             Linked,
             Conj,
             N,
             Possibility,
             LResults,
             LResults_out
             ) :-                     % Nth atom cannot be add to Conj
    N1 is N + 1,
    add_one_atom(Linked, Conj, N1, Possibility, LResults, LResults_out).


	/* construit toutes les possibilites d'ajouter Atom a Conj, compte tenu
      des modes et du biais "Linked". Possibility est la possibilite dans 
      laquelle a ete pris Atom */

    % no variable in Atom : one adds Atom to Conj
build_atoms_modes(_Linked, [Conj, Conja], (Atom, Atoma), _LArgs, _LModes, _LTypes, 
                  Possibility, [([Conj1, Conja1], [Possibility])]) :-
      term_variables(Atom, []), 
      !,
      append(Conj, [Atom], Conj1),
      append(Conja, [Atoma], Conja1).
	   


	% no + mode : on adds Atom takking into account the bias "Linked"
build_atoms_modes(Linked, Conj, Atom, _LArgs, LModes, _LTypes,
                  Possibility, LResults) :-
     \+ member(plus, LModes),    
     !,
     build_atoms(Linked, Conj, Atom, Possibility, LResults).

	% Atom contains variables with + modes
build_atoms_modes(_Linked, [Conj, Conja], Atom, LArgs, LModes, LTypes,
                  Possibility, LResults) :-
     get_arguments_term(Conj, LArgs_conj),
     convert_atoms_types(Conj, LAtoms_conj),
     get_arguments_term(LAtoms_conj, LTypes_conj),
     sort_args_types(LArgs_conj, LTypes_conj, LArgs_conj1, LTypes_conj1),
     build_atoms_plus([Conj, Conja], LArgs_conj1, LTypes_conj1, 
                      Atom, 1, LArgs, LModes, LTypes, Possibility, LResults).


	/* Check if each arg with a "plus" mod of Atom is also an
        argument of Conj */

	% all modes + have been treated
build_atoms_plus(
                 [Conj, Conja], 
                 _LArgs_conj, 
                 _LTypes_conj,
                 (Atom, Atoma), 
                 _N, 
                 [],        % no more arguments of Atom to deal with
                 [],        % no more modes
                 [],        % no more type
                 Possibility, 
                 [([Conj1, Conja1], [Possibility])]
                ) :-
   !,
   append(Conj, [Atom], Conj1),
   append(Conja, [Atoma], Conja1).

	% + mode associated with a constant (link already done)
build_atoms_plus(
                 Conj, 
                 LArgs_conj,        % Arguments of Conj
			        LTypes_conj, % Types of arguments of Conj
                 Atom,              % Atom to add
                 N,                 % rank of Arg in Atom 
                 [Arg|LArgs],       % arguments of Atom
                 [plus|LModes],     % modes of Atom
                 [_Type|LTypes],    % Types of Atom
                 Possibility,       % Possibily where Atom comes from
                 LResults
                ) :-       
   ground(Arg),
   !,
   N1 is N+1,
   build_atoms_plus(Conj, LArgs_conj, LTypes_conj, Atom, N1, 
                    LArgs, LModes, LTypes, Possibility, LResults).
    
	% mode + associated with a variable already in Conj
build_atoms_plus([Conj, Conja], LArgs_conj, LTypes_conj, 
                 Atom, N, [Arg|LArgs], [plus|LModes], [_Type|LTypes], 
                 Possibility, LResults) :-
   !,
   arg_atom_list(Arg, Conj),     % Arg is an argument of Conj
   N1 is N+1,
   build_atoms_plus([Conj, Conja], LArgs_conj, LTypes_conj, Atom, N1, 
                    LArgs, LModes, LTypes, Possibility, LResults).

	% not a mode +
build_atoms_plus(Conj, LArgs_conj, LTypes_conj,
                 Atom, N, [_Arg|LArgs], [_Mode|LModes], [_Type|LTypes], 
                 Possibility, LResults) :-
   N1 is N+1,
   build_atoms_plus(Conj, LArgs_conj, LTypes_conj, Atom, N1, 
                    LArgs, LModes, LTypes, Possibility, LResults).
          

	/* ajout atom lorsqu'il n'y a pas de modes + */
						% pas de biais Linked : on ajoute Atom
build_atoms(false, [Hyp, Hypa], (Atom, Atoma), Possibility, 
                    [([Hyp1, Hypa1], [Possibility])]) :-
   !,
   append(Hyp,  [Atom],  Hyp1),
   append(Hypa, [Atoma], Hypa1).
   
	% biais Linked : on ajoute toutes les possibilites de Atom avec liaisons.
build_atoms(true, Conj, Atom, Possibility, LResults) :-
   build_linked_atoms(true, Conj, Atom, Possibility, LResults).


	/* build all conjunction adding Atom to Conj and making a var of Atom
      identical to a var of Conj.
      We know that Conj and Atom share no variable, and that Atom and Conj
      have variables */

build_linked_atoms([Hyp, Hypa], (Atom, Atoma), Possibility, LResults) :-
	  convert_atoms_types([Atom], Atom_types),
     bk:sets_vars_not_under_oi(LVars_not_oi),

     get_sets_vars(not_oi, [Atom], Atom_types, LVars_not_oi, LTypes_vars_atom),
     convert_atoms_types(Hyp, Conj_types),
     get_sets_vars(not_oi, Hyp, Conj_types, LVars_not_oi, LTypes_vars_conj),

     append(Hyp, [Atom], Hyp1),
     append(Hypa, [Atoma], Hypa1),
	  build_coples_types(LTypes_vars_atom, LTypes_vars_conj,
                        [Hyp1, Hypa1], Possibility, LResults).


	/* build coples of variables of same type one taken in LVars_atom and
        one taken in LVars_conj */

build_coples_types([], _LTypes_vars_conj, _Hyp, _Possibility, []) :-
	!.

build_coples_types([Type_var|LTypes_vars],
                   LTypes_vars_conj,
                   Hyp, Possibility, LResults) :-
   build_coples_one_type(Type_var, LTypes_vars_conj,
                         Hyp, Possibility, LResults1),
   build_coples_types(LTypes_vars, LTypes_vars_conj, Hyp, Possibility, LResults2),
   append(LResults1, LResults2, LResults).


build_coples_one_type(Type_var, LTypes_vars_conj, Hyp, Possibility, LResults) :-
   Type_var =..[Type|[Lvars]],
   member_type(LTypes_vars_conj, Type, Type_vars_conj),
   !,		% a same type is found
   Type_vars_conj =..[Type|[Lvars_conj]],
   build_pairs(Lvars, Lvars_conj, Lcoples),
   build_constraints_hyp(Lcoples, Hyp, Type, Possibility, LResults).

build_coples_one_type(_Type, _LTypes_vars_conj, _Hyp, _Possibility, []).


	/* Form a new conjunction by constraining pairs of variables to be equals */
build_constraints_hyp([], _Hyp, _Type, _Possibility, []) :-
   !.

build_constraints_hyp([Pair|LPairs], Hyp, Type, Possibility, LResults) :-
   Type_vars=..[Type|[Pair]],
   constraint_one_type([Possibility], Type_vars, Hyp, LResults1),
   build_constraints_hyp(LPairs, Hyp, Type, Possibility, LResults2),
   append(LResults1, LResults2, LResults).


	/* cherche le type Type dans LTypes_var */
member_type([], _Type, _) :-
   !,						% Type pas trouve
   fail.

member_type([Type_var|_LTypes_vars], Type, Type_var) :-
   Type_var=..[Type|_],
   !.

member_type([_|LTypes_vars], Type, Type_var) :-
  member_type(LTypes_vars, Type, Type_var).


	/* build all pairs of elements of L1 and L2 */
build_pairs([], _, []) :-
   !.

build_pairs([X|L1], L2, Lpairs) :-
   build_pairs_one_element(X, L2, Lpairs1),
   build_pairs(L1, L2, Lpairs2),
   append(Lpairs1, Lpairs2, Lpairs).


	/* build all pairs with X and one element of L */
build_pairs_one_element(_X, [], []) :-
   !.

build_pairs_one_element(X, [Y|L], [[X,Y]|Lpairs]) :-
   build_pairs_one_element(X, L, Lpairs).


         /* build all specialization from LL_hyp_tab_seed */
build_maximal_specializations(I, T, _Seed, _LL_hyp_tab_seed, []) :-
        I > T,
        !.

build_maximal_specializations(I, T, Seed, LLHyp_tab_seed, LHyp) :-
        select_nth(I, Seed, _Tab, Seed1),
                                    % Seed1 is Seed without the Tab_seed
        select_nth(I, LLHyp_tab_seed, LHyp_tab_seed, _),
                                    % LHyp_tab_seed contains the maximally
                                    % general specialization of Hyp
        build_specializations(1, I, Seed1,  LHyp_tab_seed, LHyp1),
        I1 is I+1,

        build_maximal_specializations(I1, T, Seed, LLHyp_tab_seed, LHyp2),
        append(LHyp1, LHyp2, LHyp).


        /* build specializations using Tab_i instances */
build_specializations(_N, _I, _LTab_seed, [], []) :-
   !.

build_specializations(N, I, Seed, [(Hyp1, Tab1)|LHyp_tab_seed],
                      [(Hyp1, Seed1) |LHyp]) :-
                                           % Ith table of seed
   insert_nth(I, Tab1, Seed, Seed1),       % create a new hypothesis
   N1 is N+1,
   build_specializations(N1, I, Seed, LHyp_tab_seed, LHyp).


/* ========================================================================== */
/*           SPECIALIZING BY REPLACING ONE VARIABLE BY A CONSTANT             */
/*   This possibility is authorized for variables having an instantiable type */
/*                      (under oi or not under oi)                            */
/* ========================================================================== */

specialize_constants_hyp([Hyp, Hypa], Seed, LHyp) :-
   get_vars_consts(Hyp, Hypa, LVars_consts),
   sort(LVars_consts, LVars_consts1),
   build_instantiated_hypotheses(LVars_consts1, Hyp, Hypa, Seed, LHyp).


	/* build all possible hypotheses by instantiating a variable of Hyp with
      a constant */

build_instantiated_hypotheses([], _Hyp, _Hypa, _Seed, []) :-
   !.

build_instantiated_hypotheses(
                              [vc(Var, Const)|LVars_consts], 
                              Hyp, 
                              Hypa,
                              Seed, 
                              [([Hyp1, Hypa1], Seed1)|LHyp]
                              ) :-
   duplicate_term(t(Var, Hyp, Hypa, Seed), t(Var1, Hyp1, Hypa1, Seed1)),
   Var1 = Const,
   build_instantiated_hypotheses(LVars_consts, Hyp, Hypa, Seed, LHyp).


	/* get coples (var, const) where a var can be instantiated with const */
get_vars_consts([], [], []) :-
   !.

get_vars_consts([Atom|LAtom], [Atoma|LAtoma], LVars_consts) :-
   Atom  =..[Pred|LArgs],
   Atoma =..[Pred|LArgsa],
   get_coples_vars_consts(LArgs, LArgsa, LVars_consts1),
   get_vars_consts(LAtom, LAtoma, LVars_consts2),
   append(LVars_consts1, LVars_consts2, LVars_consts).


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

get_coples_vars_consts(
                       [Arg|LArg], 
                       [Arga|LArga], 
                       [vc(Arg, Arga)|LVars_consts]
                      ) :-
   var(Arg),
   nonvar(Arga),
   !,
   get_coples_vars_consts(LArg, LArga, LVars_consts).

get_coples_vars_consts(
                       [_Arg|LArg], 
                       [_Arga|LArga], 
                       LVars_consts
                      ) :-
   get_coples_vars_consts(LArg, LArga, LVars_consts).


/* ========================================================================== */
/*	                HANDING EQUALITY CONSTRAINTS BETWEEN VARIABLES           */
/* ========================================================================== */


	/* specialize Hyp by adding a constraint between two variables
	    (not under OI) */
specialize_variables_hyp(Hyp, Seed, LHyp) :-
     convert_atoms_types(Hyp, Hyp_types),
     bk:sets_vars_not_under_oi(LVars_not_oi),
     get_sets_vars(not_oi, Hyp, Hyp_types, LVars_not_oi, LVars_not_oi1),
     constraint_types(Seed, LVars_not_oi1, Hyp, LHyp).


   /* specialize Hyp by constraining two variables of same type
      to be equal */
constraint_types(_Seed, _LVars_not_oi, [], []) :-   % Hyp is empty
   !.

constraint_types(_Seed, [], _Hyp, []) :-            % all vars are under oi
   !.

constraint_types(Seed, [Type_vars|LTypes_vars], Hyp, LHyp) :-
   constraint_one_type(Seed, Type_vars, Hyp, LHyp1),
   constraint_types(Seed, LTypes_vars, Hyp, LHyp2),
   append(LHyp1, LHyp2, LHyp).


        /* get variables of same type and add a constraint of equality between
           two of them */
constraint_one_type(Seed, Type_vars, Hyp, LHyp) :-
   Type_vars=..[_Type|[LVars]],              % LVars contains vars of same type
   findall(
           (Hypc, Seedc),
           specialize_with_one_constraint(LVars, Hyp, Seed, Hypc, Seedc),
           LHyp
          ).

specialize_with_one_constraint(LVars, [Hyp, Hypa], Seed, 
                               [Hypc, Hypac], Seedc) :-
   add_one_constraint(LVars, X,Y),
   change_arguments(Hyp, X,Y, Hypc, _),
   change_arguments(Hypa, X, Y, Hypac, _),
   change_arguments(Seed, X,Y, Seedc, _),
   \+ contains_similar_occurrences(Hypc, strictly).


add_one_constraint(L, X,Y) :-
   sort(L, L1),
   append(_, [X|R], L1),
   member(Y, R).


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

	/* discard redundant coples (arg, type) */
sort_args_types([], [], [], []) :-
   !.

sort_args_types([Arg|LArgs], [Type|LTypes], LArgs1, LTypes1) :-
   strict_member_nth(Arg, LArgs, N),
   strict_member_nth(Type, LTypes, N),
   !,
   sort_args_types(LArgs, LTypes, LArgs1, LTypes1).

sort_args_types([Arg|LArgs], [Type|LTypes], [Arg|LArgs1], [Type|LTypes1]) :-
    sort_args_types(LArgs, LTypes, LArgs1, LTypes1).


  	/* toutes les occurrences de Y sont remplacees par X dans la possibilite */
change_arguments_possibility([], _, _, []) :-
        !.

change_arguments_possibility(
                             [(Atom, Atoma)|LAtom], 
                             X, Y, 
                             [(Atom1, Atoma1)|LAtom_out]
                            ):-
        gtrace,
        Atom =..[P|Args_atom],     
        replace_term(X,Y, Args_atom, Args_atom1),
        Atom1=..[P|Args_atom1],
         
        Atoma =..[P|Args_atoma],     
        replace_term(X,Y, Args_atoma, Args_atoma1),
        Atoma1=..[P|Args_atoma1],

        change_arguments_possibility(LAtom, X, Y, LAtom_out).

  
  	/* toutes les occurrences de Y sont remplacees par X */
change_arguments([], _, _, [], []) :-
        !.

change_arguments([A1|Conj], X, Y, [A2|Conjc], LAtomes_modifies):-
        A1 =..[P|ArgsA1],     
        replace_term(X,Y, ArgsA1, ArgsA2),
        A2=..[P|ArgsA2],
        change_arguments(Conj, X, Y, Conjc, LAtomes_modifies1),
        update_modified_atoms(A2, ArgsA1, ArgsA2, LAtomes_modifies1,
                             LAtomes_modifies).


update_modified_atoms(_, ArgsA1, ArgsA2, LAtomes, LAtomes) :-
        ArgsA1 == ArgsA2,
        !.

update_modified_atoms(A2, _, _, LAtomes, [A2|LAtomes]).

update_modified_atoms(_, ArgsA1, ArgsA2, LAtomes, LAtomes) :-
        ArgsA1 == ArgsA2,
        !.

update_modified_atoms(A2, _, _, LAtomes, [A2|LAtomes]).


/* =================================== END ================================== */

