#!/usr/bin/pl -G16M -L32M -q -t main -f

%%%% 
%%%% EXPERIMENTAL !
%%%% 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Preprocessing Filter for Negation as Failure with Stable Semantics
%%%%
%%%% Usage: # naf.pl [-opt] myprogram.pl >result.pl
%%%%
%%%% Options:
%%%%
%%%%        -opt effects a more efficient translation, which uses
%%%%             certain features of KRHyper, see section OPT below.
%%%%             EXPERIMENTAL (!)
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% 
%%%% This is a straightforward naive implementation of K. Inoue,
%%%% M. Koshimura and R. Hasegawa: Embedding Negation as Failure
%%%% into a Model Generation Theorem Prover, CADE-11, 1992.
%%%% 
%%%% The input syntax extends that of krh:
%%%% 
%%%% - "Classical negation" (in the sense of [Inoue  et al])
%%%% 
%%%%   Instead of atoms, literals are used: a positive literal is expressed
%%%%   as the atom, a negative as:
%%%% 
%%%%      ~(Atom).
%%%% 
%%%% - "Negation as failure" (in the sense of [Inoue  et al]):
%%%% 
%%%%   A body literal can also be negated by negation as failure:
%%%% 
%%%%      not_naf(Literal)
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Notes:
%%%% 
%%%% - No provision or check for range restriction is made here.
%%%% 
%%%% - Technical syntactic restriction:
%%%% 
%%%%    ./2 (the list constructor) is not allowed as predicate name.
%%%% 
%%%% - A head may be a disjunction of conjunctions. It will be translated to
%%%%   a conjunction of literals or a disjunction of literals with the help
%%%%   of auxiliary predicates.
%%%% 
%%%% - Generated predicates have names starting with '$'.
%%%% 
%%%% - Constraint rules corrsponding to the schemas below are only generated
%%%%   if their predicate appears with the respective signs in the head of
%%%%   some clause.
%%%% 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:- op(900, fy, not_naf).

:- use_module(script_support).
:- use_module('../contrib/pl/swilib/pretty').
:- use_module('../contrib/pl/swilib/fromonto').
:- use_module('../contrib/pl/swilib/err').

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

main :-
	main(initialize, translate_clause(_, _),  pp_schema_clauses(_)).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

oa_to_list((A;B), C) :-
	!,
	oa_to_list(A, A1),
	oa_to_list(B, B1),
	append(A1, B1, C).
oa_to_list((A,B), [C]) :-
	!,
	ao_to_list(A, A1),
	ao_to_list(B, B1),
	append(A1, B1, C).
oa_to_list(A, [A]).
ao_to_list((A,B), C) :-
	!,
	ao_to_list(A, A1),
	ao_to_list(B, B1),
	append(A1, B1, C).
ao_to_list((A;B), [C]) :-
	!,
	oa_to_list(A, A1),
	oa_to_list(B, B1),
	append(A1, B1, C).
ao_to_list(A, [A]).

list_to_oa([E], E1) :-
	!,
	list_to_ao(E, E1).
list_to_oa([E|Es], (E1;Es1)) :-
	!,
	list_to_ao(E, E1),
	list_to_oa(Es, Es1).
list_to_oa(E, E).

list_to_ao([E], E1) :-
	!,
	list_to_oa(E, E1).
list_to_ao([E|Es], (E1,Es1)) :-
	!,
	list_to_oa(E, E1),
	list_to_ao(Es, Es1).
list_to_ao(E, E).

clause_to_cl((H :- B), cl(H1, B1)) :-
        !,
	oa_to_list(H, H1),
        ao_to_list(B, B1).
clause_to_cl(H, cl(H1, [])) :-
	oa_to_list(H, H1).

pp_cl(cl(H, B)) :-
	list_to_oa(H, H1),
	( B = [] ->
	  pp_clause(H1)
	; list_to_ao(B, B1),
	  pp_clause((H1 :- B1))
	),
	nl.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Notes about the translation:
%%%%
%%%% Facts can have 6 signs:
%%%%
%%%% A            % pos
%%%% ~A           % neg
%%%% k(A)         % k_pos
%%%% k(~(A))      % k_neg 
%%%% -k(A)        % not_k_pos
%%%% -k(~(A))     % not_k_neg
%%%%
%%%% Schemas:
%%%%
%%%% false :- -k(A), A.         (11) % S1
%%%% false :- -k(~A), ~A.       (11) % S2
%%%% false :- -k(A), k(A).      (12) % S3
%%%% false :- -k(~A), k(~A).    (12) % S4
%%%% false :- A, ~A.            (13) % S5
%%%% false :- k(A), ~A.         (14) % S6
%%%% false :- k(~A), A.         (14) % S7
%%%% false :- k(A), k(~A).      (15) % S8   
%%%%
%%%% T-Condition:
%%%%
%%%% false :- k(A), \+ A.
%%%% false :- k(~A), \+ ~A.
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:- dynamic(head_predicate/3).

initialize :-
	retractall(head_predicate(_, _, _)).

gen_schema_clause(C) :-
	( gen_schema(not_k_pos, pos, C)
	; gen_schema(not_k_neg, neg, C)
	; gen_schema(not_k_pos, k_pos, C)
	; gen_schema(not_k_neg, k_neg, C)
	; gen_schema(pos, neg, C)
	; gen_schema(k_pos, neg, C)
	; gen_schema(k_neg, pos, C)
	; gen_schema(k_pos, k_neg, C)
	; gen_t_condition(k_pos, pos, C)
	; gen_t_condition(k_neg, neg, C)
	).

pp_schema_clauses(Options) :-
	( memberchk(opt, Options) ->
	  pp_schema_clauses_opt
	; pp_schema_clauses
	).

pp_schema_clauses :-
	( gen_schema_clause(C),
	  pp_cl(C),
	  fail
	; true
	).

gen_schema(Sign1, Sign2, cl([false], [C1, C2])) :-
	head_predicate(Pred, Arity, Sign1),
	head_predicate(Pred, Arity, Sign2),
	functor(Template, Pred, Arity),
	signed(Sign1, Template, C1),
	signed(Sign2, Template, C2).

gen_t_condition(Sign1, Sign2, cl([false], [C1, (\+ C2)])) :-
	head_predicate(Pred, Arity, Sign1),
	functor(Template, Pred, Arity),
	signed(Sign1, Template, C1),
	signed(Sign2, Template, C2).

signed(Sign, A, A1) :-
	sign_prefix(Sign, Prefix),
	A =.. [F|Args],
	atom_concat(Prefix, F, F1),
	A1 =.. [F1|Args].

sign_prefix(pos, '').
sign_prefix(neg, '$not_').
sign_prefix(k_pos, '$k_').
sign_prefix(k_neg , '$knot_').
sign_prefix(not_k_pos, '$notk_').
sign_prefix(not_k_neg, '$notknot_').

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

lit_sign_and_atom(~(X), neg, X) :- !.
lit_sign_and_atom('$k'(~(X)), k_neg, X) :- !.
lit_sign_and_atom('$k'(X), k_pos, X) :- !.
lit_sign_and_atom('$not_k'(~(X)), not_k_neg, X) :- !.
lit_sign_and_atom('$not_k'(X), not_k_pos, X) :- !.
lit_sign_and_atom(X, pos, X).

assert_head_predicates([D|Ds]) :-
	( D = [_|_] ->
	  assert_head_predicates(D)
	; lit_sign_and_atom(D, Sign, Atom),
	  functor(Atom, P, A),
	  ( head_predicate(P, A, Sign) ->
	    true
	  ; assert(head_predicate(P, A, Sign))
          )
	),
        assert_head_predicates(Ds).
assert_head_predicates([]).	

standardize_clause(cl(H, B), cl(H1, B1)) :-
	standardize_lits(H, H1),
	standardize_lits(B, B1).

standardize_lits([L|Ls], [L1|Ls1]) :-
	( L = [_|_] ->
	  standardize_lits(L, L1)
	; standardize_lit(L, L1)
	),
	standardize_lits(Ls, Ls1).
standardize_lits([], []).

standardize_lit(L, L1) :-
	lit_sign_and_atom(L, Sign, Atom),
	sign_prefix(Sign, Prefix),
	Atom =.. [F|Args],
	atom_concat(Prefix, F, F1),
	L1 =.. [F1|Args].

reduce_false_heads(H, H1) :-
	reduce_false_heads_1(H, H2),
	( H2 = [] ->
	  H1 = [false]
	; H1 = H2
	).

reduce_false_heads_1([false|Hs], Hs1) :-
	!,
	reduce_false_heads_1(Hs, Hs1).
reduce_false_heads_1([Ls|Hs], Hs1) :-
	Ls = [_|_],
	memberchk(false, Ls),
	!,
	reduce_false_heads_1(Hs, Hs1).
reduce_false_heads_1([H|Hs], [H|Hs1]) :-
	reduce_false_heads_1(Hs, Hs1).
reduce_false_heads_1([], []).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%
%%%% Generate aux predicates, as long has KRH can not have conjunctions
%%%% nested in disjunctions as heads.
%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

mk_disjuncts(cl(H, B), cl(H1, B), Auxs) :-
	( H = [[_|_]] ->
	  H1 = H,
	  Auxs = []
	; map_mk_disjunct(H, H1, Auxs)
	).
	
map_mk_disjunct([D|Ds], [D1|Ds1], Auxs) :-
	( D = [_|_] ->
	  free_variables(D, Vars),
	  gensym('$naf_aux', F),
	  D1 =.. [F|Vars],
	  Auxs = [cl([D], [D1])|Auxs1]
	; D1 = D,
	  Auxs1 = Auxs
	),
	map_mk_disjunct(Ds, Ds1, Auxs1).
map_mk_disjunct([], [], []).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

split_naf_literals([], [], []).
split_naf_literals([not_naf(L)|Ls], Ls1, [L|Ls2]) :-
	!,
	split_naf_literals(Ls, Ls1, Ls2).
split_naf_literals([L|Ls], [L|Ls1], Ls2) :-
	split_naf_literals(Ls, Ls1, Ls2).

map_add_disjunct([Ls|Ls1], NK, [NK1|NKs1]) :-
	Ls = [_|_],
	!,
	append(Ls, NK, NK1),
	map_add_disjunct(Ls1, NK, NKs1).
map_add_disjunct([L|Ls1], NK, [[L|NK]|NKs1]) :-
	map_add_disjunct(Ls1, NK, NKs1).
map_add_disjunct([], _, []).

map_wrap_neg_k([X|Xs], ['$not_k'(X)|Xs1]) :-
	map_wrap_neg_k(Xs, Xs1).
map_wrap_neg_k([], []).

map_wrap_pos_k([X|Xs], ['$k'(X)|Xs1]) :-
	map_wrap_pos_k(Xs, Xs1).
map_wrap_pos_k([], []).

translate_clause(C, Options) :-
	( memberchk('opt', Options) ->
	  translate_clause_opt(C)
	; translate_clause(C)
	).

translate_clause(C) :-
	clause_to_cl(C, cl(H, B)),
	split_naf_literals(B, B1, B2),
	( B2 = [] ->
	  C1 = cl(H, B)
	; map_wrap_neg_k(B2, NK),
	  map_wrap_pos_k(B2, PK),
	  map_add_disjunct(H, NK, NKs),
	  append(NKs, PK, H1),
	  C1 = cl(H1, B1)
	),
	C1 = cl(Head1, Body1),
	reduce_false_heads(Head1, Head2),
	C1a = cl(Head2, Body1),
	assert_head_predicates(Head2),
	standardize_clause(C1a, C2),
	mk_disjuncts(C2, C3, Cauxs),
	pp_cl(C3),
	( member(Caux, Cauxs),
	  pp_cl(Caux),
	  fail
	; true
	).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% 
%%%% OPT (EXPERIMENTAL)
%%%% 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% 
%%%% This uses complement splitting to implement the negative literals: -
%%%% use options to enable complement splitting, prevent re-ordering of
%%%% head literals and enable subsumption of a derived head against facts.
%%%% 
%%%% Negative literals do not appear explicitely in the translation.
%%%% Instead of schemas S1 and S2
%%%% 
%%%%   false :- -k(A), A.         (11) % S1
%%%%   false :- -k(~A), ~A.       (11) % S2
%%%% 
%%%% the following Schemas (not in the paper of Inoue) are used:
%%%% 
%%%%   k(A) :- A.
%%%%   k(~A) :- ~A.
%%%% 
%%%% (where A is a "plain" atom).
%%%% 
%%%% Rationale:
%%%%   A should complement with ~k(A).
%%%%   No interfering with other schemas and the T-condition.
%%%% 
%%%% The schemas S3 and S4 are implicitely implemented by standard
%%%% complement processing:
%%%% 
%%%%   false :- -k(A), k(A).      (12) % S3
%%%%   false :- -k(~A), k(~A).    (12) % S4
%%%% 
%%%% 

gen_schema_clause_opt(C) :-
	( gen_schema_opt(pos, C)
	; gen_schema_opt(neg, C)
	; gen_schema(pos, neg, C)
	; gen_schema(k_pos, neg, C)
	; gen_schema(k_neg, pos, C)
	; gen_schema(k_pos, k_neg, C)
	; gen_t_condition(k_pos, pos, C)
	; gen_t_condition(k_neg, neg, C)
	).

pp_schema_clauses_opt :-
	( gen_schema_clause_opt(C),
	  pp_cl(C),
	  fail
	; true
	).

k_sign(pos, k_pos).
k_sign(neg, k_neg).

gen_schema_opt(Sign1, cl([C1], [C2])) :-
	head_predicate(Pred, Arity, Sign1),
	k_sign(Sign1, Sign2),
	functor(Template, Pred, Arity),
	signed(Sign2, Template, C1),
	signed(Sign1, Template, C2).

translate_clause_opt(C) :-
	clause_to_cl(C, cl(H, B)),
	split_naf_literals(B, B1, B2),
	( B2 = [] ->
	  C1 = cl(H, B)
	; map_wrap_pos_k(B2, PK),
	  append(H, PK, H1),
	  C1 = cl(H1, B1)
	),
	C1 = cl(Head1, Body1),
	reduce_false_heads(Head1, Head2),
	C1a = cl(Head2, Body1),
	assert_head_predicates(Head2),
	standardize_clause(C1a, C2),
	mk_disjuncts(C2, C3, Cauxs),
	pp_cl(C3),
	( member(Caux, Cauxs),
	  pp_cl(Caux),
	  fail
	; true
	).