/*
	LPAD and CP-Logic reasoning suite
	File semlpad.pl
	Program for building the semantics of an LPAD
	Queries are answered by using SLG in every instance
	Copyright (c) 2007, Fabrizio Riguzzi
*/

:-module(semlpad,[p/1,s/2,sc/3,set/2]).
:-use_module(library(lists)).
:-dynamic setting/2.
:-set_prolog_flag(unknown,fail).
:- dynamic new_number/1.

:-[library(slg)].
:-retract('slg$default'(_D)),assert('slg$default'(tabled)).

setting(epsilon,0.00001).
%setting(ground_body,true). 
setting(ground_body,false). 
/* available values: true, false
if true, both the head and the body of each clause will be grounded, otherwise
only the head is grounded. In the case in which the body contains variables 
not appearing in the head, the body represents an existential event */

%setting(grounding,variables).
setting(grounding,modes).
/* available values: variables, modes
if set to variables, the universe facts from the .uni file are used
if set to modes, the mode and type declaration from the .uni file are used
*/

new_number(0).

sc(Goals,Evidence,Prob):-
	s(Evidence,ProbE),
	append(Goals,Evidence,GE),
	s(GE,ProbGE),
	Prob is ProbGE/ProbE.

s(GoalsList,Prob):-
	program_names(L),
	convert_to_goal(GoalsList,Goal,L),
	run_query(L,Goal,0,Prob).

run_query([],_G,P,P).

run_query([Prog|T],Goal,PIn,POut):-
	elab_conj(Prog,Goal,Goal1),
	slg(Goal1),!,
	prob(Prog,P),
	P1 is PIn+P,
	run_query(T,Goal,P1,POut).
	
run_query([_Prog|T],Goal,PIn,POut):-
	run_query(T,Goal,PIn,POut).
	

convert_to_goal([Goal],Goal,_Pr):-!.

convert_to_goal(GoalsList,Head,Pr):-
	get_new_atom(Atom),
	extract_vars(GoalsList,[],V),
	Head=..[Atom|V],
	list2and(GoalsList,Body),
	elab_conj(Prog,Head,HeadP),
	elab_conj(Prog,Body,BodyP),
	do_term_expansion((HeadP:-BodyP),LC),
	assert_in_all_prog(LC,Prog,Pr).
		

get_new_atom(Atom):-
	retract(new_number(N)),
	N1 is N+1,
	assert(new_number(N1)),
	number_atom(N,NA),
	atom_concat('$call',NA,Atom).
	

assert_in_all_prog(_LC,_Prog,[]).

assert_in_all_prog(LC,Prog,[PrH|PrT]):-
	copy_term((LC,Prog),(LC1,Prog1)),
	Prog1=PrH,
	assert_all(LC1),
	assert_in_all_prog(LC,Prog,PrT).

/* predicate for parsing the program file */		
p(File):-
	atom_concat(File,'.uni',FileUni),
	consult(FileUni),
	atom_concat(File,'.cpl',FilePl),
	open(FilePl,read,S),
	read_clauses(S,C),
	close(S),
	process_clauses(C,ClausesVar),
	instantiate(ClausesVar,[],Clauses),
	assert(program(1)),
	assert(program_names([])),
	create_programs(Clauses).



create_programs(Clauses):-
	create_single_program(Clauses,1,Program),
	retract(program(N)),
	number_codes(N,NC),
	atom_codes(NA,NC),
	atom_concat(p,NA,Name),
	N1 is N+1,
	assert(program(N1)),
	format("Writing instance ~d~n",[N]),
	write_program(Name,Program),
	retract(program_names(L)),
	append(L,[Name],L1),
	assert(program_names(L1)),
	fail.

create_programs(_).

write_program(Name,[(prob(P):-true)]):-!,
	elab_conj(Name,prob(P),Pr),
	assertz(Pr).


write_program(Name,[(H:-B)|T]):-
	elab_conj(Name,H,H1),
	elab_conj(Name,B,B1),
	do_term_expansion((H1:-B1),LC),
	assert_all(LC),
	write_program(Name,T).

elab_conj(_Name,true,true):-!.

elab_conj(Name,\+(B),\+(B1)):-!,
	elab_conj(Name,B,B1).
		
elab_conj(Name,(BL,Rest),(BL1,Rest1)):-!,
	elab_conj(Name,BL,BL1),
	elab_conj(Name,Rest,Rest1).

elab_conj(Name,bagof(V,EV^G,L),bagof(V,EV^GL,L)):-!,
	elab_conj(Name,G,GL).

elab_conj(Name,bagof(V,G,L),bagof(V,GL,L)):-!,
	elab_conj(Name,G,GL).

elab_conj(Name,setof(V,EV^G,L),setof(V,EV^GL,L)):-!,
	elab_conj(Name,G,GL).

elab_conj(Name,setof(V,G,L),setof(V,GL,L)):-!,
	elab_conj(Name,G,GL).

elab_conj(Name,findall(V,G,L),findall(V,GL,L)):-!,
	elab_conj(Name,G,GL).

elab_conj(_Name,A,A):-
	bg(A),!.

elab_conj(_Name,A,A):-
	builtin(A),!.

elab_conj(Name,Lit,Lit1):-
	Lit\=(_,_),
	Lit=..[Pred|Args],
	Lit1=..[Pred,Name|Args].


create_single_program([],P,[(prob(P):-true)]).
	
create_single_program([r(H,B)|T],PIn,[(HA:-B)|T1]):-
	member((HA:P),H),
	P1 is PIn*P,
	create_single_program(T,P1,T1).

/* predicates for producing the ground instances of program clauses */
instantiate([],C,C).

instantiate([r(_V,[H:1],B)|T],CIn,COut):-!,
	append(CIn,[r([H:1],B)],C1),
	instantiate(T,C1,COut).

instantiate([r(V,H,B)|T],CIn,COut):-
	(setting(grounding,variables)->
		findall(r(H,BOut),instantiate_clause_variables(V,H,B,BOut),L)
	;
		findall(r(H,BOut),instantiate_clause_modes(H,B,BOut),L)
	),
	append(CIn,L,C1),
	instantiate(T,C1,COut).
		

instantiate_clause_modes(H,B,BOut):-
	instantiate_head_modes(H),
	list2and(BL,B),
	instantiate_body_modes(BL,BLOut),
	list2and(BLOut,BOut).


instantiate_head_modes([]):-!.

instantiate_head_modes([H:_P|T]):-
	instantiate_atom_modes(H),
	instantiate_head_modes(T).


instantiate_body_modes(BL,BL):-
	setting(ground_body,false),!.
	
instantiate_body_modes(BL0,BL):-
	instantiate_list_modes(BL0,BL).


instantiate_list_modes([],[]).

instantiate_list_modes([H|T0],T):-
	builtin(H),!,
	call(H),
	instantiate_list_modes(T0,T).

instantiate_list_modes([\+ H|T0],T):-
	builtin(H),!,
	\+ call(H),
	instantiate_list_modes(T0,T).

instantiate_list_modes([\+ H|T0],[\+ H|T]):-!,
	instantiate_atom_modes(H),
	instantiate_list_modes(T0,T).

instantiate_list_modes([H|T0],[H|T]):-
	instantiate_atom_modes(H),
	instantiate_list_modes(T0,T).


instantiate_atom_modes(''):-!.

instantiate_atom_modes(A):-
	functor(A,F,NArgs),
	functor(TA,F,NArgs),
	A=..[F|Args],
	mode(TA),
	TA=..[F|Types],
	instantiate_args_modes(Args,Types).


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

instantiate_args_modes([H|T],[TH|TT]):-
	type(TH,Constants),
	member(H,Constants),
	instantiate_args_modes(T,TT).


instantiate_clause_variables([],_H,B,BOut):-
	list2and(BL,B),
	(setting(ground_body,true)->
		check_body(BL,BLOut)
	;
		BLOut=BL
	),
	list2and(BLOut,BOut).

instantiate_clause_variables([VarName=Var|T],H,BIn,BOut):-
	universe(VarNames,U),
	member(VarName,VarNames),
	member(Var,U),
	instantiate_clause_variables(T,H,BIn,BOut).	

instantiate_clause_variables([VarName=_Var|T],H,BIn,BOut):-
	\+ varName_present_variables(VarName),!,
	instantiate_clause_variables(T,H,BIn,BOut).	


varName_present_variables(VarName):-
	universe(VarNames,_U), member(VarName,VarNames).


check_body([],[]).

check_body([H|T],TOut):-
	builtin(H),!,
	call(H),
	check_body(T,TOut).

check_body([H|T],[H|TOut]):-
	check_body(T,TOut).
	

process_clauses([(end_of_file,[])],[]).

process_clauses([((H:-B),V)|T],[r(V,HL,B)|T1]):-
	H=(_;_),!,
	list2or(HL1,H),
	process_head(HL1,0,HL),
	process_clauses(T,T1).

process_clauses([((H:-B),V)|T],[r(V,HL,B)|T1]):-
	H=(_:_),!,
	list2or(HL1,H),
	process_head(HL1,0,HL),
	process_clauses(T,T1).
	
process_clauses([((H:-B),V)|T],[r(V,[H:1],B)|T1]):-!,
	process_clauses(T,T1).

process_clauses([(H,V)|T],[r(V,HL,true)|T1]):-
	H=(_;_),!,
	list2or(HL1,H),
	process_head(HL1,0,HL),
	process_clauses(T,T1).

process_clauses([(H,V)|T],[r(V,HL,true)|T1]):-
	H=(_:_),!,
	list2or(HL1,H),
	process_head(HL1,0,HL),
	process_clauses(T,T1).
	
process_clauses([(H,V)|T],[r(V,[H:1],true)|T1]):-
	process_clauses(T,T1).

process_head([H:PH],P,[H:PH1|Null]):-
	PH1 is PH,
	PNull is 1-P-PH1,
	setting(epsilon,Eps),
	EpsNeg is - Eps,
	PNull > EpsNeg,
	(PNull>Eps->
		Null=['':PNull]
	;
		Null=[]
	).

process_head([H:PH|T],P,[H:PH1|NT]):-
	PH1 is PH,
	P1 is P+PH1,
	process_head(T,P1,NT).

/* predicates for reading in the program clauses */
read_clauses(S,Clauses):-
	(setting(ground_body,true)->
		read_clauses_ground_body(S,Clauses)
	;
		read_clauses_exist_body(S,Clauses)
	).


read_clauses_ground_body(S,[(Cl,V)|Out]):-
	read_term(S,Cl,[variable_names(V)]),
	(Cl=end_of_file->
		Out=[]
	;
		read_clauses_ground_body(S,Out)
	).


read_clauses_exist_body(S,[(Cl,V)|Out]):-
	read_term(S,Cl,[variable_names(VN)]),
	extract_vars_cl(Cl,VN,V),
	(Cl=end_of_file->
		Out=[]
	;
		read_clauses_exist_body(S,Out)
	).


extract_vars_cl(end_of_file,[]).

extract_vars_cl(Cl,VN,Couples):-
	(Cl=(H:-_B)->
		true
	;
		H=Cl
	),
	extract_vars(H,[],V),
	pair(VN,V,Couples).
	

pair(_VN,[],[]).

pair([VN= _V|TVN],[V|TV],[VN=V|T]):-
	pair(TVN,TV,T).	
	

extract_vars(Var,V0,V):-
	var(Var),!,
	(member_eq(Var,V0)->
		V=V0
	;
		append(V0,[Var],V)
	).
	
extract_vars(Term,V0,V):-
	Term=..[_F|Args],
	extract_vars_list(Args,V0,V).


extract_vars_list([],V,V).

extract_vars_list([Term|T],V0,V):-
	extract_vars(Term,V0,V1),
	extract_vars_list(T,V1,V).

member_eq(A,[H|_T]):-
	A==H,!.
	
member_eq(A,[_H|T]):-
	member_eq(A,T).

/* auxiliary predicates */
list2or([X],X):-
		X\=;(_,_),!.

list2or([H|T],(H ; Ta)):-!,
		list2or(T,Ta).


list2and([],true):-!.

list2and([X],X):-
		X\=(_,_),!.

list2and([H|T],(H,Ta)):-!,
		list2and(T,Ta).


builtin(_A is _B).
builtin(_A > _B).
builtin(_A < _B).
builtin(_A >= _B).
builtin(_A =< _B).
builtin(_A =:= _B).
builtin(_A =\= _B).
builtin(true).
builtin(false).
builtin(_A = _B).
builtin(_A==_B).
builtin(_A\=_B).
builtin(_A\==_B).


bg(member(_El,_L)).
bg(average(_L,_Av)).
bg(max_list(_L,_Max)).
bg(min_list(_L,_Max)).


average(L,Av):-
	sum_list(L,Sum),
	length(L,N),
	Av is Sum/N.

/* set(Par,Value) can be used to set the value of a parameter */
set(Parameter,Value):-
	retract(setting(Parameter,_)),
	assert(setting(Parameter,Value)).


assert_all([]):-!.

assert_all([(:- G)|T]):-!,
	call(G),
	assert_all(T).
	
assert_all([H|T]):-!,
	assertz((H)),
	assert_all(T).
	
assert_all(C):-
	assertz((C)).