/*
	Forum interpreter in LLP
	by Naoyuki Tamura (tamura@kobe-u.ac.jp)

	Based on the following paper:
		Joshua S. Hodas and Jeffrey Polakow. 
		Forum as a Logic Programming Language: 
		Preliminary Results and Observations,
		Linear Logic '96,
		Electronic Notes in Theoretical Computer Science, 
		Volume 3, Elsevier, 1996. 

	Forum's Web page
		http://www.cse.psu.edu/~dale/forum/
	Hodas's Web page
		http://www.cs.hmc.edu/~hodas/
	LLP's Web page
		http://bach.seg.kobe-u.ac.jp/llp/
*/
:- op(1200, xfy, ($)).
:- op( 950, xfy, (@)).
%:- op( 950, xfy, (=>)).
:- op( 900,  fy, (?)).
:- op( 900, fy, (~)).

forum :- forum(no).

forum_trace :- forum(yes).

forum(Trace) :-
	nl,
	write('Forum (Kobe version 0.1) '),
	write('by Naoyuki Tamura (tamura@kobe-u.ac.jp)'), nl,
	trace_flag(Trace) => forum_top.

forum_top :-
	forum_read(X),
	forum_exec(X).

forum_exec(end_of_file) :- !.
forum_exec((?- G)) :- !,
	forum_goal(G),
	forum_top.
forum_exec(Clause0) :-
	trans_clause(Clause0, As, Gs, Vs),
	!,
	(trace_flag(yes) ->
	     write('Clause defined: '),
	     forum_write((Vs $ As :- Gs)), nl
	;    true),
	psi(all, As, Gs, Vs) => forum_top.
forum_exec(Clause0) :-
	write('Syntax error: '),
	forum_write(Clause0), nl.

forum_goal(G) :-
	forum_goal0(G).
forum_goal(_).

forum_goal0(G0) :-
	trans_macro(G0, G),
	write('Goal: '), forum_write(G), nl,
	statistics(runtime, _),
	forum_prove([G]),
	statistics(runtime, [_,T]),
	!,
	write('Proved ('), write(T), write(' msec): '),
	forum_write(G), nl,
	fail.
forum_goal0(_) :-
	statistics(runtime, [_,T]),
	write('Not Proved ('), write(T), write(' msec)'), nl,
	fail.

trans_clause((Vs $ Clause0), As, Gs, Vs) :- !,
	trans_macro(Clause0, Clause),
	bc_form(Clause, As, Gs).
trans_clause(Clause0, As, Gs, []) :-
	trans_macro(Clause0, Clause),
	bc_form(Clause, As, Gs).

trans_macro((X0 :- Y0), X) :- !,
	trans_macro((Y0 -<> X0), X).
trans_macro((X0, Y0), X) :- !,
	trans_macro((X0 * Y0), X).
trans_macro(0, (erase -<> bottom)) :- !.
trans_macro(1, (bottom -<> bottom)) :- !.
trans_macro(~X0, X) :- !,
	trans_macro((X0 -<> bottom), X).
trans_macro(!X0, X) :- !,
	trans_macro(((X0 => bottom) -<> bottom), X).
trans_macro((X0 ; Y0), X) :- !,
	trans_macro(~ (~X0 & ~Y0), X).
trans_macro((X0 * Y0), X) :- !,
	trans_macro(~ (~X0 @ ~Y0), X).
trans_macro(?X0, X) :- !,
	trans_macro(((X0 -<> bottom) => bottom), X).
trans_macro((X0 & Y0), (X & Y)) :- !,
	trans_macro(X0, X), trans_macro(Y0, Y).
trans_macro((X0 @ Y0), (X @ Y)) :- !,
	trans_macro(X0, X), trans_macro(Y0, Y).
trans_macro((X0 -<> Y0), (X -<> Y)) :- !,
	trans_macro(X0, X), trans_macro(Y0, Y).
trans_macro((X0 => Y0), (X => Y)) :- !,
	trans_macro(X0, X), trans_macro(Y0, Y).
trans_macro(X, X).

%%%
%%% Prover
%%%
forum_prove([]) :-
	(trace_flag(yes) -> dump_sequent; true),
	pick(As, Gs, Ws),
	bc(As, Gs, Ws).
forum_prove([G|Gamma]) :-
	forum_prove(G, Gamma).

forum_prove(erase, Gamma) :- !,
	erase.		% not complete
forum_prove(bottom, Gamma) :- !,
	forum_prove(Gamma).
forum_prove((B & C), Gamma) :- !,
	forum_prove(B, Gamma) & forum_prove(C, Gamma).
forum_prove((B @ C), Gamma) :- !,
	forum_prove(B, [C|Gamma]).
forum_prove((B -<> C), Gamma) :- !,
	bc_form(B, As, Gs),
	delta(exists, As, Gs, []) -<> forum_prove(C, Gamma).
forum_prove((B => C), Gamma) :- !,
	bc_form(B, As, Gs),
	psi(exists, As, Gs, []) => forum_prove(C, Gamma).
forum_prove(A, Gamma) :- !,
	a(A) -<> forum_prove(Gamma).

pick(As, Gs, Ws) :-
	(delta(Q, As0, Gs0, Ws0); psi(Q, As0, Gs0, Ws0)),
	pick0(Q, [As0,Gs0,Ws0], [As,Gs,Ws]).

pick0(all, X0, X) :- !, copy_term(X0, X).
pick0(_, X, X).

bc(As, Gs, Vs) :-
	head(As),
	all_nonvar(Vs),
	(trace_flag(yes) -> bc_trace(As, Gs, Vs); true),
	body(Gs).

head([]).
head([A|As]) :- a(A), head(As).

all_nonvar([]).
all_nonvar([V|Vs]) :- nonvar(V), all_nonvar(Vs).

body([]).
body([builtin(G)|Gs]) :- !, call(G), body(Gs).
body([!G|Gs]) :- !, !forum_prove([G]), body(Gs).
body([G|Gs]) :- !, forum_prove([G]), body(Gs).

bc_form(X, As, Gs) :-
	bc_form_pos(X, As, Gs).

bc_form_pos(bottom, [], []) :- !.
bc_form_pos((A & B), As, Gs) :- !,
	(bc_form_pos(A, As, Gs); bc_form_pos(B, As, Gs)).
bc_form_pos((A => B), As, [!A|Gs]) :- !,
	bc_form_pos(B, As, Gs).
bc_form_pos(((A -<> bottom) -<> B), As, Gs) :- !,
	bc_form_pos((A @ B), As, Gs).
bc_form_pos((A -<> B), As, [A|Gs]) :- !,
	bc_form_pos(B, As, Gs).
bc_form_pos((A @ B), As, Gs) :- !,
	bc_form_pos(A, As1, Gs1),
	bc_form_pos(B, As2, Gs2),
	append(As1, As2, As),
	append(Gs1, Gs2, Gs).
bc_form_pos(A, [A], []).

dump_sequent :-
	write('Atoms: '),
	a(X),
	forum_write(X), write(', '),
	fail.
dump_sequent :-
	nl.

bc_trace(As, Gs, Vs) :-
	write('BC with: '),
	forum_write(As),
	write(' :- '),
	forum_write(Gs),
	nl.

%psi(_,_,_,_) :- fail.
%delta(_,_,_,_) :- fail.
%a(_) :- fail.

%%%
%%% Utilities
%%%

forum_read(X) :-
	R = (current_op(1200, xfy, ($)), 
	     current_op( 950, xfy, (@)), 
	     current_op( 950, xfy, (=>)),
	     current_op( 900,  fy, (?))),
	R => read(X).

forum_write(X) :-
	R = (current_op(1200, xfy, ($)), 
	     current_op( 950, xfy, (@)), 
	     current_op( 950, xfy, (=>)),
	     current_op( 900,  fy, (?))),
	R => write(X).

%forum_read(X) :-
%	!current_op(1200, xfy, ($)) -<>
%	!current_op( 950, xfy, (@)) -<>
%	!current_op( 950, xfy, (=>)) -<>
%	!current_op( 900,  fy, (?)) -<>
%	read(X).
%
%forum_write(X) :-
%	!current_op(1200, xfy, ($)) -<>
%	!current_op( 950, xfy, (@)) -<>
%	!current_op( 950, xfy, (=>)) -<>
%	!current_op( 900,  fy, (?)) -<>
%	write(X).

append([], Zs, Zs).
append([W|Xs], Ys, [W|Zs]) :- append(Xs, Ys, Zs).