/* ========================================================================== */
/*                              COMPLETION                                    */
/*                 complete intentional ambiguous examples                    */
/*    Author  : Dominique Bouthinon (LIPN, Universite Paris13)                */
/* ========================================================================== */
  
:- module(completion, 
          [
			complete_intentional_examples/3, 
                                  % (File_int, File_bkg, File_int_out)
           	  			    % complete intentional examples of 
           	  			    % File_int by using negation by failure
           	  			    % and background knowledge in File_bkg.
           	  			    % Complete examples are in File_int_out
		     completion_intentional_examples/3
						    % (File_int, File_bkg, File_int_out)
           	  			    % complete intentional examples of 
           	  			    % File_int by using observed frequencies
						    % of non ambiguous values.
           	  			    % Complete examples are in File_int_out	
          ]).

:- getenv('LEAR_DIR', Lear),
   atom_concat(Lear, '/intentional_data.pl', Intentional),
   use_module(Intentional),
   atom_concat(Lear, '/term.pl', Term),
   use_module(Term),
   atom_concat(Lear,'/utilities_lear11.pl', Utils),
   use_module(Utils).


/* ====== COMPLETE EXAMPLES USING OBSERVED FREQUENCES OF CERTAIN FACTS ===== */


completion_intentional_examples(File_int, File_bkg, File_out) :-
   writeln('completion of the examples...'),

   read_intentional_examples(ex, File_int, LPos_int, LNeg_int),

   consult_background_knowledge(bk, File_bkg),
   get_modes(bk, LModes),
   get_clauses_background(bk, LClauses_bkg),
   get_irrelevant(bk, LIrrelevant),
   get_types_under_oi(bk, LOi_types),	

   discard_plus_minus(LModes, LModes1),

   compute_known_unknown_facts(LIrrelevant, LPos_int, LClauses_bkg, 
                               LModes1, LPos_known_unknown),
   compute_known_unknown_facts(LIrrelevant, LNeg_int, LClauses_bkg, 
                               LModes1, LNeg_known_unknown),

   completion_examples(LPos_known_unknown, LPos_known_unknown, 
                       LModes1, LOi_types, [], LPos_int1),
   completion_examples(LNeg_known_unknown, LNeg_known_unknown, 
                       LModes1, LOi_types, [], LNeg_int1), 

   write_intentional_examples(File_out, LPos_int1, LNeg_int1),

   finish_completion,
   
   writeln('end completion.').

	/* complete unknonwn values of the examples taking into account values
   		of the most specific first order motif they correspond with */
completion_examples([], _Initial_LEx, _LModes, _LOi_types, 
                    _LStats_patterns, []) :-
   !.

completion_examples([Ex|LEx], Initial_LEx, LModes, LOi_types,
                    LStats_predicates, [Ex1|LEx1]) :-
   completion_one_example(Ex, Initial_LEx, LModes, LOi_types,
                          LStats_predicates, LStats_predicates1, Ex1),
   completion_examples(LEx, Initial_LEx, LModes, LOi_types,
                       LStats_predicates1, LEx1).

	/* completion of one example */
completion_one_example(ex(Known_atoms, Unknown_atoms, Domains, Target),
                       Initial_LEx, LModes, LOi_types,
                       LStats_predicates, LStats_predicates1, 
                       (Ex1, Domains, Target)) :-
   completion_unknown_atoms(Unknown_atoms, Initial_LEx, LModes, LOi_types,
                            LStats_predicates, LStats_predicates1, Completed_atoms),
   append(Known_atoms, Completed_atoms, Ex1).   


	/* completion of a list of unknown atoms */
completion_unknown_atoms([], _Initial_LEx, _LModes, _LOi_types,
                          LStats_predicates, LStats_predicates, []) :-
   !.

completion_unknown_atoms(
					[Atom|LAtoms],  % atoms to be completed 
					Initial_LEx,    % list of examples
                         LModes,         % [pred1(typeArg1, typeArg2),...]
                         LOi_types,      % types under_oi
                         LStats_predicates,  % list of order 1 patterns whith
                                          % statitics (number of true and false instances) 
                         LStats_predicates1,     % list of patterns (possibly statistics
                                         % of the pattern associated with Atom 
                                         % are modified 
                         [Atom1|LAtoms1] % Atom1 is Atom or neg(Atom)
                        ):-
   completion_one_atom(Atom,  Initial_LEx, LModes, LOi_types,
                       LStats_predicates, LStats_predicatesA, Atom1),
   completion_unknown_atoms(LAtoms, Initial_LEx, LModes, LOi_types,
                            LStats_predicatesA, LStats_predicates1, LAtoms1).


	/* completion of one atom */
		  
completion_one_atom(Atom, Initial_LEx, LModes, LOi_types,
                    LStats_predicates, LStats_predicates_out, Atom1) :-
   compute_exclusion(Atom, LModes, LOi_types, LExclusion),
   variabilize_atom_structurally_exclusion(Atom, LExclusion, Pattern),
   atom_arity(Atom, Name),
   get_stats_pattern(Name, Pattern, Initial_LEx, 
                     LStats_predicates, stats(_Pattern, NTrue, NFalse), 
                     LStats_predicates_out),
   complete_atom(Atom, NTrue, NFalse, Atom1).

 
	/* attribute the value true of false to Atom given 
        the NTrue and NFalse values */
complete_atom(Atom, NTrue, NFalse, Atom) :-
   NTrue > NFalse,
   !.

complete_atom(Atom, _NTrue, _NFalse, neg(Atom)).


	/* compute the list of constants that cannot be variabilized from
        (they have not a type under object identity (oi) */
compute_exclusion(Atom, LModes, LOi_types, LExclusion) :-
   Atom =..[Predicate_name|LArgs],
   length(LArgs, N),
   functor(Mode, Predicate_name, N),
   member(Mode, LModes),            % we have got the mode of Atom
   Mode =..[Predicate_name|LTypes],
   compute_the_exclusions(LArgs, LTypes, LOi_types, LExclusion1),
   sort(LExclusion1, LExclusion).

compute_the_exclusions([], [], _LOi_types, []):-
   !.
							% Type not excluded
compute_the_exclusions([_Const|LConsts], [Type|LTypes], LOi_types,
                       LConsts1) :-
   member(Type, LOi_types),
   !,
  compute_the_exclusions(LConsts, LTypes, LOi_types, LConsts1).

							% Type excluded
compute_the_exclusions([Const|LConsts], [_Type|LTypes], LOi_types,
                       [Const|LConsts1]) :-
  compute_the_exclusions(LConsts, LTypes, LOi_types, LConsts1).


/* ========= COMPLETE EXAMPLES ACCORDING TO CLOSE WORLD ASSUMPTION ========== */
   
	/* complete intentional examples using negation by failure,
        so there is no more ambiguity */
complete_intentional_examples(File_int, File_bkg, File_int_out) :-

   writeln('completing examples...'),

   read_intentional_examples(ex, File_int, LPos_int, LNeg_int),
   consult_background_knowledge(bk, File_bkg),
   get_modes(bk, LModes),
   get_clauses_background(bk, LClauses_bkg),

   discard_plus_minus(LModes, LModes1),
  
   complete_examples(LIrrelevant, LPos_int, pos, LClauses_bkg, 
                     LModes1, LPos_int1),
   complete_examples(LIrrelevant, LNeg_int, negative, LClauses_bkg, 
                     LModes1,LNeg_int1),

   write_intentional_examples(File_int_out, LPos_int1, LNeg_int1),

   finish_completion,
   
   writeln('end completing.').


	/* make each intentional example complete using negation by failure */
deal_with_examples(_Signe, [], _Stream) :-
   !.
   
deal_with_examples(Signe, [Ex|Lex], Stream) :-
   write_example(Ex, Signe, Stream),
   deal_with_examples(Signe, Lex, Stream).
   
    
	/* complete intentional examples using negation by failure */		
complete_examples(_LIrrelevant, [], _Signe, _LClauses_bkg, _LModes, []) :-
   !.
   
complete_examples(LIrrelevant, [(Ex_int, LDomains, Target)|LEx_int], Signe, 
                  LClauses_bkg, LModes, 
                  [(Ex_int1, LDomains, Target)|LEx_int1]) :- 

  compute_grounded_theory_complete(Ex_int, LDomains, 
                                   LClauses_bkg, LModes, LIrrelevant,
                                   LClauses_negB, HB, LHead2),
  !,  
  delete_non_facts(LClauses_negB, LFacts),
  get_positive_facts(LFacts, LPositive_facts),
  compute_negative_facts(HB, LPositive_facts, LNegative_facts),
  append(LPositive_facts, LNegative_facts, Ex_int1),
   
  discard_clauses_intentional2(LHead2), 
  complete_examples(LIrrelevant, LEx_int, Signe, LClauses_bkg, LModes, LEx_int1).

	% the current example is not consistent
complete_examples(LIrrelevant, [(Ex_int, _LDomains, Target)|LEx_int], Signe, 
                  LClauses_bkg, LModes, LEx_int1) :-
   writeln('!!! the following example is not consistent !!!'),
   writeln(Target),
   writeln(Ex_int),
   complete_examples(LIrrelevant, LEx_int, Signe, 
                     LClauses_bkg, LModes, LEx_int1).
    

    /* 
       !!! (domi 2013) attention si la théorie clausale
       formée de l'exemple et du background contient des clauses générales,
       la completion donnera des resultats qui ne sont pas des modeles de 
       la theorie clausale.
       Par exemple la clause a ou b completee donnera non(a) et non(b), 
       ce qui est faux.
    */	
   /* each clause with several facts will give a set of negative facts */
complete_grounded_theory([], []) :-
   !.
   
complete_grounded_theory([[Fact]|LClauses], [Fact|LClauses1]) :-  
   complete_grounded_theory(LClauses, LClauses1).
   
complete_grounded_theory([Clause|LClauses], LClauses1) :-
   set_negative_facts(Clause, LClauses2),
   complete_grounded_theory(LClauses, LClauses3),
   append(LClauses2, LClauses3, LClauses1).
   
   
   /* compute a set of negative facts */
set_negative_facts([], []) :-
   !.
   
set_negative_facts([neg(X)|LFacts], [neg(X)|LClauses]) :-
   !,
   set_negative_facts(LFacts, LClauses).
   
set_negative_facts([Fact|LFacts], [neg(Fact)|LClauses]) :-
   set_negative_facts(LFacts, LClauses).   
   

get_positive_examples(LPos) :-
   findall(Ex, bk:pos(_N,Ex), LPos).
   
get_negative_examples(LNeg) :-
   findall(Ex, bk:neg(_N,Ex), LNeg).   
   

	/* compute the grounded clausal theory representing the intentional
        ambiguous examples (specific version for complete the examples) */
compute_grounded_theory_complete(
                        LClauses_ex, 
                        LDomains,
                        LClauses_bkg,
                        LModes,
                        LIrrelevant,
                        LClauses_negB,
                        HB,
                        LHead2
                       ) :-

   append(LClauses_ex, LClauses_bkg, LClauses_ex_bkg),

   lear_clauses_to_prolog(LClauses_ex_bkg, LHead),
   discard_similar_elements(LHead, LHead1, structurally),

   build_Herbrand_base(LIrrelevant, LModes, LDomains, HB),
   
   delete_similar_elements([], LHead1, LTrue1, strictly),

   inserer_dans_base(LTrue1),
   
   append(LClauses_ex_bkg, LTrue1, LClauses),
   append(LHead1, LTrue1, LHead2),
  
   translate_clauses(LClauses, LClauses_int),

  						  % builds instantiated clauses according to HB
   instantiate_clauses(LClauses_int, HB, LClauses_neg),
   simplify_clauses(LClauses_neg, LClauses_negA),
   discard_similar_elements(LClauses_negA, LClauses_negB, structurally).


/* ======================== PATTERN HANDLING ================================ */

	/* get Pattern in a list [
                                  predicate1(stats(Pattern11, NTrue11, NFalse11), 
                                             stats(Pattern12, NTrue2, NFalse12),...]),
                                  predicate2(stats(Pattern21, NTrue21, NFalse22),...]),
                              ] */

									% no Pattern for Predicate is seen 
get_stats_pattern(Predicate, Pattern, Initial_LEx, 
                  [], Stats_pattern,[LStats_pattern]) :-
  !,
  set_stats_pattern(Initial_LEx, Pattern, NTrue, NFalse),
  Stats_pattern = stats(Pattern, NTrue, NFalse),
  LStats_pattern =..[Predicate|[[Stats_pattern]]].
 

	% list of Pattern corresponding to Predicate found
get_stats_pattern(
               	Predicate,					% predicate name 
                    Pattern, 					     % search Pattern
                    Initial_LEx,                       % list of examples
               	[Stats_predicate|LStats_others_predicates], 
               	 Stats_pattern, 
               	[Stats_predicate1|LStats_others_predicates]
                 ) :-
   Stats_predicate =..[Predicate|[LStats_patterns]],	
   take_stats_pattern(Pattern, Initial_LEx, LStats_patterns, Stats_pattern,
                      LStats_patterns1),
   Stats_predicate1 =..[Predicate|[LStats_patterns1]].	
   
   
								      % lists of Pattern corresponding
 									 % to Predicate not found
get_stats_pattern(
               	Predicate, Pattern, Initial_LEx,
               	[Stats_predicate|LStats_others_predicates], 
               	stats(Pattern1, NTrue, NFalse), 
               	[Stats_predicate|LStats_others_predicates1]
                  ) :-
   get_stats_pattern(Predicate, Pattern, Initial_LEx, LStats_others_predicates, 
                     stats(Pattern1, NTrue, NFalse), 
                     LStats_others_predicates1).
  

/* select Pattern in a list [ stats(Pattern11, NTrue11, NFalse11), 
                              stats(Pattern12, NTrue2, NFalse12),...])
   where all Patterns are build from the same predicate */
           

	/* check whether Pattern has stats in LStats, if not compute these stats */

		% Stats of Pattern found in LStats
take_stats_pattern(Pattern, _Initial_LEx, LStats, Stats_pattern, LStats) :-
   get_the_pattern(Pattern, LStats, Stats_pattern),
   !.

	% Stats of Pattern not found in LStats
take_stats_pattern(Pattern, Initial_LEx, LStats, 
                   stats(Pattern, NTrue, NFalse),
                   [stats(Pattern, NTrue, NFalse)|LStats]) :-
  set_stats_pattern(Initial_LEx, Pattern, NTrue, NFalse).

        
						% Stats of the pattern not found
get_the_pattern(_Pattern, [], _) :-
   !,
   fail.

						% Stats of the Pattern found
get_the_pattern(Pattern, [stats(Pattern1, NTrue, NFalse)|_LPatterns], 
                stats(Pattern1, NTrue, NFalse)) :-
   Pattern =@= Pattern1,
   !.


get_the_pattern(Pattern, [_Stats_pattern|LStats_patterns], 
                   stats(Pattern1, NTrue, NFalse)) :-
   get_the_pattern(Pattern, LStats_patterns, stats(Pattern1, NTrue, NFalse)).  


	/* associate Pattern with the number of Times it is false and true
        in examplex LEx */					
set_stats_pattern([], _Pattern, 0, 0) :-
   !.

set_stats_pattern([ex(Known, _Unknown, _Domains, _Target)|LEx], 
                  Pattern, NTrue, NFalse) :-
   numbers_instances_pattern(Known, Pattern, NTrue1, NFalse1),
   set_stats_pattern(LEx, Pattern, NTrue2, NFalse2),
   NTrue  is NTrue1 + NTrue2,
   NFalse is NFalse1 + NFalse2. 


	/* numbers the instances of Pattern in a set of examples */
numbers_instances_pattern([], _Pattern, 0, 0) :-
   !.

numbers_instances_pattern([neg(Atom)|LAtoms], Pattern, NTrue, NFalse) :-
   instance_of(Atom, Pattern),
   !,
   numbers_instances_pattern(LAtoms, Pattern, NTrue, NFalse1),
   NFalse is NFalse1 + 1.
   

numbers_instances_pattern([Atom|LAtoms], Pattern, NTrue, NFalse) :-
   instance_of(Atom, Pattern),
   !,
   numbers_instances_pattern(LAtoms, Pattern, NTrue1, NFalse),
   NTrue is NTrue1 + 1.
   
numbers_instances_pattern([_Atom|LAtoms], Pattern, NTrue, NFalse) :-
   numbers_instances_pattern(LAtoms, Pattern, NTrue, NFalse).




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

finish_completion :-
   discard_intentional_knowledge,
   intentional2:retractall(:-dynamic).


	/* every non positive fact is assumed negative (c.w.assumptions) */
compute_negative_facts(HB, LPositive_facts, LNegative_facts) :-
     subtract(HB, LPositive_facts, LNegative_facts1),
     set_negative_facts(LNegative_facts1, LNegative_facts).
     
/* ============================ END OF LISTING ============================== */
