%% -*- prolog -*-
%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%
%% Copyright 2016 Éric Würbel, LSIS-CNRS, AMU
%%
%% This file is part of PASP, a possibilistic ASP solver.
%% PASP is free software: you can redistribute it and/or
%% modify it under the terms of the GNU General Public License as
%% published by the Free Software Foundation, either version 3 of
%% the License, or (at your option) any qlater version.
%%
%% PASP is distributed in the hope that it will be useful,
%% but WITHOUT ANY WARRANTY; without even the implied warranty of
%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
%% General Public License for more details.
%%
%% You should have received a copy of the GNU General Public
%% License along with PASP. If not, see
%% <http://www.gnu.org/licenses/>.
%%
%% PASP implements the simulation of possibilistic ASP with
%% a classical ASP solver.
%%
%% This module defines predicates for handling the generation of an ASP
%% progam from a PASP program
%%
%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:-module(generator, [
	     certp/2,
	     necessity/2,
	     pasp_to_asp/3
	 ]).

:-use_module(library(clpfd)).
:-use_module(library(apply)).
:-use_module(logic).
:-use_module(asp).

%%	cert(+Wff, -Cert)
%
%	compute the cert set (see Bauters & al 2013)

cert((A,B),Cert) :-
	cert(A,CertA),
	cert(B,CertB),
	union(CertA,CertB,Cert)
	.
cert((:-B),[N]) :-
	conjunct_member(nec__(N),B)
	.
cert((_:-B), [N]) :-
	conjunct_member(nec__(N),B)
	.


%%	certp(+Wff, -Certp)
%
%	Compute the cert+ set

certp(Wff,Certp) :-
	cert(Wff,Cert1),
	nec_complement(Cert1,L2),
	reverse(L2,Cert2),
	union(Cert1,Cert2,Cert3),
	union(Cert3,[0, 50, 100],Certp1),
	sort(Certp1,Certp)
	.

nec_complement([],[]).
nec_complement([N1|L1],[N2|L2]) :-
	N2 #= 100 - N1,
	nec_complement(L1,L2)
	.

%%	necessity(+Rule, -Necessity)
%
%	Necessity measure of a rule.

necessity((:-B),N) :-
	conjunct_member(nec__(N),B)
	.
necessity((_:-B),N) :-
	conjunct_member(nec__(N),B)
	.

%%	necesity(+Rule, -NewRule, -Necessity)
%
%	Necessity measure of a rule. NewRule is the rule without the
%	necessity atom.

necessity((:-B),(:-NewB),N) :-
	conjunct_member(nec__(N),B),
	apply_to_conjuncts(B,is_necessity,B1),
	flatten_conjunction(B1,NewB)
	.
necessity((H:-B),(H:-NewB),N) :-
	conjunct_member(nec__(N),B),
	apply_to_conjuncts(B,is_necessity,B1),
	flatten_conjunction(B1,NewB)
	.

%%	is_necessity(?Atom1, ?Atom2)
%
%	unifies Atom2 with true whenever Atom1 unifies with nec__/1.
%	Otherwise unifies Atom1 with Atom2.

is_necessity(nec__(_),true) :- !.
is_necessity(A,A).

%%	pasp_to_asp(+Pasp, +Certp, -ASP)
%
%	Generate an ASP program from a PASP program, using a cert+ set.
%

pasp_to_asp(PASP,Certp,ASP) :-
	collect_pasp_to_asp(PASP,Certp,true,ASP).

collect_pasp_to_asp((A,B),Certp,InASP,OutASP) :-
	collect_pasp_to_asp(A,Certp,InASP,OutASP1),
	collect_pasp_to_asp(B,Certp,OutASP1,OutASP)
	.
collect_pasp_to_asp((:-B),Certp,InASP,OutASP) :-
	pasp_rule_to_asp_rules((:-B),Certp,InASP,OutASP)
	.
collect_pasp_to_asp((H:-B),Certp,InASP,OutASP) :-
	pasp_rule_to_asp_rules((H:-B),Certp,InASP,OutASP)
	.

%%	pasp_rule_to_asp_rules(+Rule, +Certp, +InASP, -OutASP)
%
%	Generate the ASP rules corresponding to a PASP rule.

pasp_rule_to_asp_rules((H:-B),Certp,InASP,OutASP) :-
	necessity((H:-B),(H:-NewB),N),
	include(between(0,N),Certp,[0|L]),
	rule2rules((H:-NewB),Certp,L,Rules),
	conjoin(InASP,Rules,OutASP)
	.
pasp_rule_to_asp_rules((:-B),Certp,InASP,OutASP) :-
	necessity((:-B),(:-NewB),N),
	include(between(0,N),Certp,[0|L]),
	rule2rules((:-NewB),Certp,L,Rules),
	conjoin(InASP,Rules,OutASP)
	.

rule2rules(_,_,[],true).
rule2rules((H:-B),Certp,[Cp|L],Rules) :-
	splitbody(B,PB,NB),
%	NB \= true, % peut etre inutile. À voir.
	D #= 100 - Cp,
	include(between(D,100),Certp,[V1,V2|_]),
	(  V1 =:= D
	-> MaxD = V2
	;  MaxD = V1
	),
	newlit(H,Cp,H1),
	(   PB = true
	->  PosB = true
	;   new_posbody(PB,Cp,PosB)
	),
	(   NB = true
	->  NegB = true
	;   new_negbody(NB,MaxD,NegB)
	),
	conjoin(PosB,NegB,B1),
	flatten_conjunction(B1,Body),
	rule2rules((H:-B),Certp,L,Rules1),
	(   Body = true
	->  conjoin(H1,Rules1,Rules)
	;   conjoin((H1:-Body),Rules1,Rules)
	)
	.
rule2rules((:-B),Certp,[Cp|L],Rules) :-
	splitbody(B,PB,NB),
%	NB \= true, % peut etre inutile. À voir.
	D #= 100 - Cp,
	include(between(D,100),Certp,[V1,V2|_]),
	(   V1 =:= D
	->  MaxD = V2
	;   MaxD = V1
	),
	(   PB = true
	->  PosB = true
	;   new_posbody(PB,Cp,PosB)
	),
	(   NB = true
	->  NegB = true
	;   new_negbody(NB,MaxD,NegB)
	),
	conjoin(PosB,NegB,B1),
	flatten_conjunction(B1,Body),
	rule2rules((:-B),Certp,L,Rules1),
	(   Body = true
	->  error('empty constraint : ~w~n', [(:-B)])
	;   conjoin((:-Body),Rules1,Rules)
	)
	.

newlit(-A,V,-Lit) :-
	atom(A),
	Lit =.. [A,V]
	.
newlit(A,V,Lit) :-
	atom(A), A \= -_,
	Lit =.. [A,V]
	.
newlit(-A,V,-Lit) :-
	compound(A),
	A =.. [F|Args],
	append(Args,[V],NArgs),
	Lit =.. [F|NArgs]
	.
newlit(A,V,Lit) :-
	A \= -_,
	compound(A),
	A =.. [F|Args],
	append(Args,[V],NArgs),
	Lit =.. [F|NArgs]
	.


new_posbody((A,B),V,PosB) :-
	new_posbody(A,V,A1),
	new_posbody(B,V,B1),
	conjoin(A1,B1,PosB)
	.
new_posbody(Lit,V,NewLit) :-
	Lit \= (_,_),
	is_asp_literal(Lit),
	newlit(Lit,V,NewLit)
	.

new_negbody((A,B),V,NegB) :-
	new_negbody(A,V,A1),
	new_negbody(B,V,B1),
	conjoin(A1,B1,NegB)
	.
new_negbody((not Lit),V,(not NewLit)) :-
	Lit \= (_,_),
	is_asp_literal(Lit),
	newlit(Lit,V,NewLit)
	.