mill1.pl

#!/Applications/SWI-Prolog.app/Contents/MacOS//swipl -q -t main -f

:- use_module(dancing_links,       [compute_axioms/4,
				    update_roots_axiom/4,
				    update_roots_contraction/5]).
:- use_module(portray_graph_tikz, [portray_graph/1,graph_header/0,graph_footer/1,latex_graph/1]).
%:- use_module(portray_graph_none,  [portray_graph/1,graph_header/0,graph_footer/1,latex_graph/1]).
:- use_module(translations,        [translate_lambek/3,
				    translate_displacement/3,
				    translate_hybrid/6,
				    exhaustive_test/6]).
:- use_module(proof_generation,    [generate_proof/2,
				    generate_sequent_proof/2,
				    generate_natural_deduction_proof/2,
				    generate_nd_proof/2,
				    generate_hybrid_proof/2,
				    generate_displacement_proof/2]).
:- use_module(latex,               [proof_header/0,
				    proof_footer/0,
				    latex_semantics/1,
				    latex_lexicon/1,
				    latex_lexicon1/0]).
:- use_module(sem_utils,           [substitute_sem/3,
				    reduce_sem/2]).
:- use_module(replace,             [replace_graph/6,
				    replace_proofs_labels/4,
				    replace_formula/5]).
:- use_module(lexicon,             [lookup/5]).
:- use_module(auxiliaries,         [merge_fvs/3,
				    free_vars_n/2,
				    free_vars_p/2]).

:- dynamic '$PROOFS'/2, '$AXIOMS'/1, '$LOOKUP'/1.
:- dynamic node_formula/3.

:- op(400, xfy, \).
:- op(190, yfx, @).

% = adds some likely locations for pdflatex/lualatex to the file search path

user:file_search_path(path, '/usr/texbin/').
user:file_search_path(path, '/opt/local/bin/').

% = allow for simplified atomic_formula/1 declarations; does the completely general
% = translation to atomic_formula/3 automatically

term_expansion(atomic_formula(A), atomic_formula(A, F, Vs)) :-
	A =.. [F|Vs],
	!.

% = some definitions for pretty-printing

portray(neg(F, X, L)) :-
	atom(F),
	Term =.. [F|L],
	format('-~p ~p',[Term,X]).
portray(pos(F, X, L)) :-
	atom(F),
	Term =.. [F|L],
	format('+~p ~p',[Term,X]).
portray(at(X, Vs)) :-
	atom(X),
	Term =.. [X|Vs],
	print(Term).
portray(at(X, I1, I2, Vs)) :-
	atom(X),
	Term =.. [X|Vs],
	format('~w{~w,~w}', [Term,I1,I2]).
portray(impl(A,B)) :-
	format('(~p -o ~p)', [A,B]).
portray(rule(N,A,B,Ps)) :-
	copy_term(A-B, AA-BB),
	numbervars(AA-BB, 0, _),
	Ps \== [],
	format('rule(~p,~p  |-  ~p,...)', [N,AA,BB]).
portray(appl(appl(appl(appl(appl(F,W),V),Z),Y),X)) :-
	atom(F),
	!,
	Term =.. [F,X,Y,Z,V,W],
	print(Term).
portray(appl(appl(appl(appl(F,V),Z),Y),X)) :-
	atom(F),
	!,
	Term =.. [F,X,Y,Z,V],
	print(Term).
portray(appl(appl(appl(F,Z),Y),X)) :-
	atom(F),
	!,
	Term =.. [F,X,Y,Z],
	print(Term).
portray(appl(appl(F,Y),X)) :-
	atom(F),
	!,
	Term =.. [F,X,Y],
	print(Term).
portray(appl(F,X)) :-
	atom(F),
	!,
	Term =.. [F,X],
	print(Term).
portray(appl(M,N)) :-
	format('(~p ~p)', [M,N]).
portray(lambda(X,M)) :-
        format('(~p^~p)', [X,M]).
portray(bool(P,B,Q)) :-
	format('(~p ~p ~p)', [P,B,Q]).

% =======================================
% = Top-level theorem prover predicates =
% =======================================

% command line execution
%
% mill1 GrammarFile GoalFormula Words
%
% loads GrammarFile and passes Words and GoalFormula to parse/2

main :-
	current_prolog_flag(os_argv, Argv),
        append(_, [A|Av], Argv),
	file_base_name(A, 'mill1.pl'),
	!,
        main(Av).

main([silent|Rest]) :-
	!,
	retractall(output_error(_)),
	assert(output_error(0)),
	main(Rest).
main([GrammarFile,Atom|Words]) :-
	!,
	load_grammar(GrammarFile),
	/* allow goal formulas of the form "s\(fin\)", etc. (backslashes are necessary!) */
	read_term_from_atom(Atom, GoalFormula, []),
	parse(Words, GoalFormula),
	halt.
main(_) :-
	format(user_output, 'Usage: mill1 GrammarFileName GoalFormula Words~n', []).


% = load_grammar(File)
%
% compile Prolog grammar file File

load_grammar(File) :-
	absolute_file_name(File, GrammarFile, [access(read),file_type(prolog)]),
	grammar_cleanup,
	compile(GrammarFile).

% = grammar_cleanup
%
% remove lexicon and test sentences from previous grammar

grammar_cleanup :-		
	abolish(lex/3),
	abolish(lex/4),
	abolish(lex/5),
	abolish(atomic_formula/1),
	abolish(atomic_formula/3),
	abolish(test/1).

% = parse_all
%
% parse all test sentences in the currently loaded
% grammar file; test sentences are assumed to be
% of the form
%
% test(N) :-
%       parse(Words, Goal).
%
% or
%
% test(N) :-
%       prove(Antecedent, Goal).

parse_all :-
	findall(N, clause(test(N),_), List),
	parse_all(List, Solutions),
	print_solutions(List, Solutions).

parse_all([], []).
parse_all([N|Ns], [P-SemList|Ps]) :-
        test(N),
        user:'$PROOFS'(P, SemList),
	parse_all(Ns, Ps).

% = parse(+ListOfWords, +GoalFormula)
%
% true if there are lexical entries for each of the words in ListOfWords
% which allow us to derive GoalFormula; lexical entries for the Displacement
% calculus or hybrid type-logical grammars are translated into first-order
% linear logic beforehand.

parse(ListOfWords, Goal0) :-
	initialisation,
	retractall('$LOOKUP'(_)),
	assert('$LOOKUP'(0)),
	lookup(ListOfWords, Formulas, LexSem, Goal0, Goal),
	/* update lookup statistics */
	'$LOOKUP'(N0),
	N is N0 + 1,
	retractall('$LOOKUP'(_)),
	assert('$LOOKUP'(N)),
        format_error('~N= Lookup ~D~n', [N]),
	prove0(Formulas, Goal, LexSem),
	fail.
parse(_, _) :-
        format_error('~N= Done!~2n================~n=  statistics  =~n================~n', []),	
	'$LOOKUP'(L),
	write_lookups(L),
        final_statistics.
% Commented out since this is inconsistent with the behavior of parse_all
%	/* succeed only if at least one proof was found */
%        user:'$PROOFS'(N),
%        N > 0.

% = prove(+Antecedent, +GoalFormula)
%
% true if the sequent Antecedent |- GoalFormula is derivable in
% first-order linear logic.
%
% prove/2 and prove/3 are wrapper predicates: they do initialisation,
% call prove0/3, enumerate solutions by a failure-drive loop and
% outputs some proof statistics.
%
% The LaTeX headers and footers are also output here (when LaTeX
% output is generated).

prove(Antecedent, Goal) :-
	prove(Antecedent, Goal, []).

% = prove(+Antecedent, +GoalFormula, +LexicalSubstitutions)

prove(Antecedent, Goal, LexSem) :-
	initialisation,
	prove0(Antecedent, Goal, LexSem),
	fail.
prove(_, _, _) :-
        format_error('~N= Done!~2n================~n=  statistics  =~n================~n', []),	
	final_statistics.

initialisation :-
	/* LaTeX output */
	graph_header,
	proof_header,
	/* reset counters */
	retractall('$PROOFS'(_, _)),
	assert('$PROOFS'(0, [])),
	retractall('$AXIOMS'(_)),
	assert('$AXIOMS'(0)).

final_statistics :-
	/* print final statistics and generate pdf files */
	'$AXIOMS'(A),
	'$PROOFS'(N, _),
	write_proofs(N),
	write_axioms(A),
	/* LaTeX graphs */
	graph_footer(N),
	/* LaTeX proofs */
	proof_footer.

% prove0/2, prove0/3 is a second wrapper, doing sequent unfolding
% calling the recursive prover predicate prove1/3, doing lexical
% subsitution and outputing semantics
% and proofs.

prove0(Antecedent, Goal) :-
	prove0(Antecedent, Goal, []).

prove0(Antecedent, Goal, LexSem) :-
        unfold_sequent(Antecedent, Goal, Roots, Graph, Sem0, Stats),
	portray_sequent_statistics(Stats),
	format_error('Parsing: ', []),
	/* keep a copy of the initial graph (before any unificiations) for later proof generation */
	copy_term(Graph, GraphCopy),
	portray_graph(Graph),
        prove1(Graph, Roots, Trace),
	/* proof found */
	'$PROOFS'(N0, SemList),
	N is N0 + 1,
	/* generate semantics */
	substitute_sem(LexSem, Sem0, Sem1),
	reduce_sem(Sem1, Sem),
	format_info('~N= Semantics ~w: ~p~n', [N,Sem]),
	latex_semantics(Sem),
	/* update proof statistics */
	retractall('$PROOFS'(_, _)),
	assert('$PROOFS'(N, [Sem|SemList])),
	/* generate a LaTeX proof */
	/* generate_proof/2 outputs Displacement, hybrid, natural deduction and sequent proofs */
	/* if you are only interested in one type of proof, replace generate_proof/2 by one of: */
	/* generate_hybrid_proof/2, (natural deduction proofs in hybrid type-logical grammar) */
        /* generate_displacement_proof/2, (natural deduction proofs for the Displacement calculus) */
	/* generate_sequent_proof/2, (sequent proofs in first-order linear logic) */
	/* generate_natural_deduction_proof/2, (natural deduction proof in first-order linear logic) */
	/* generate_nd_proof/2, (natural deduction proof in first-order linear logic with implicit antecedents) */
%	generate_hybrid_proof(GraphCopy, Trace).
%	generate_displacement_proof(GraphCopy, Trace).
	generate_proof(GraphCopy, Trace).

% = first_proof
%
% a version of the prover predicate which only finds the first proof.

first_proof(Antecedent, Goal, Sem) :-
	first_proof(Antecedent, Goal, [], Sem).

first_proof(Antecedent, Goal, LexSem, Sem) :-
	( is_stream(graph) -> true ; open_null_stream(Stream), set_stream(Stream, alias(graph))),
        unfold_sequent(Antecedent, Goal, Roots, Graph, Sem0, _Stats),
        prove1(Graph, Roots, _Trace),
	!,
	substitute_sem(LexSem, Sem0, Sem1),
	reduce_sem(Sem1, Sem).


% = first_parse(+ListOfWords, +GoalFormula)
%
% a version of parse which finds only the first solution.

first_parse(ListOfWords, Goal0) :-
	initialisation,
	retractall('$LOOKUP'(_)),
	assert('$LOOKUP'(0)),
	lookup(ListOfWords, Formulas, LexSem, Goal0, Goal),
	/* update lookup statistics */
	'$LOOKUP'(N0),
	N is N0 + 1,
	retractall('$LOOKUP'(_)),
	assert('$LOOKUP'(N)),
        format_error('~N= Lookup ~D~n', [N]),
	prove0(Formulas, Goal, LexSem),
	!,
        format_error('~N= Done!~2n================~n=  statistics  =~n================~n', []),	
	'$LOOKUP'(L),
	write_lookups(L),
        final_statistics.

% = prove1(+Graph, +Roots, -Trace)
%
% true if Graph (with root nodes Roots) is a proof net, as justified by
% the axioms/contractions in Trace.
%
% the prove1 predicate operates by identifying, at each recursive step, a pair
% of atomic formulas and contracting the input graph (verifying for acyclicity
% and connectedness)

prove1([vertex(_, [], _, [])], _, []) :-
	/* a single vertex with atoms or links, we have succeeded ! */
        format_error('~N= Proof found!~n', []),
        !.
prove1(Graph0, Roots0, [ax(N0,AtV0,AtO0,N1,AtV1,AtO1)|Rest0]) :-
	/* forced choice for positive atom, using first-found from the best */
	/* choices returned by the dancing links algorithm */
	/* TODO: evaluate different tie-breakers here as a heuristic for selecting */
	/* atoms likely to fail quickly */
	compute_axioms(Roots0, Graph0, _ATree, Axioms),
	select_first(Axioms, Graph0, tuple(AtV1,AtO1,N1,Choices)),
        select(vertex(N1, [A|As0], FVs0, Ps0), Graph0, Graph1),
        select(pos(At,AtV1,AtO1,X,Vars), [A|As0], As),
	!,
	/* enumerate choices for negative atom */
%	select_manual(Choices, Graph1, tuple(AtV0,AtO0,N0)),
	member(tuple(AtV0,AtO0,N0), Choices),
	select(vertex(N0, [B|Bs0], FVs1, Ps1), Graph1, Graph2),
	select(neg(At,AtV0,AtO0,X,Vars), [B|Bs0], Bs),
        /* verify no cycle has been created */
        \+ cyclic(Ps0, Graph2, N0),
        \+ cyclic(Ps1, Graph2, N1),
	'$AXIOMS'(Ax0),
	Ax is Ax0 + 1,
	retractall('$AXIOMS'(_)),
	assert('$AXIOMS'(Ax)),
	/* identify nodes of positive and negative atom */
	/* (and do the necessary replacements) */
	append(As, Bs, Cs),
	append(Ps0, Ps1, Ps),
	merge_fvs(FVs0, FVs1, FVs),
	replace_graph(Graph2, Ps, N0, N1, Graph3, Rs),
	update_roots_axiom(Roots0, N0, N1, Roots1),
	Graph4 = [vertex(N1,Cs,FVs,Rs)|Graph3],
        portray_graph(Graph4),
	/* perform Danos-style graph contractions */
	contract(Graph4, Graph, Rest0, Rest, Roots1, Roots),
	/* verify the result is (at least potentially) connected */
	connected(Graph),
	mark_progress(Graph),
	prove1(Graph, Roots, Rest).

% =======================================
% =              Proof nets             =
% =======================================

% = axiom selection predicates

% default: select first

select_first([Item|_], _, Item).

select_random(List, _, Item) :-
	random_member(Item, List).
	
select_manual(List, Graph, Item) :-
	portray_atoms(List, Graph, 0, Len),
	Len > 0,
	read_integer_max(Len, ItemNo),
	nth1(ItemNo, List, Item).


read_integer_max(Max, Int) :-
	read(Int0),
   (
	integer(Int0),
	Int0 =< Max
   ->
        Int = Int0
   ;
        read_integer_max(Max, Int)
   ).
    
portray_atoms([], _, N, N) :-
	format('Selection?', []).
portray_atoms([A|As], Graph, N0, N) :-
	N1 is N0 + 1,
	portray_atom(A, N1, Graph),
	portray_atoms(As, Graph, N1, N).

portray_atom(tuple(AtV1,AtO1,N1), N, Graph) :-
        select(vertex(N1, [A|As0], _FVs0, _Ps0), Graph, _),
        select(neg(At,AtV1,AtO1,_X,Vars), [A|As0], _),
	!,
	format('[~d] -~w(~@) ~d-~d~n', [N, At, portray_vars(Vars), AtV1, AtO1]).
portray_atom(tuple(AtV1,AtO1,N1,Choices), N, Graph) :-
	length(Choices, Len),
	Len > 0,
        select(vertex(N1, [A|As0], _FVs0, _Ps0), Graph, _),
        select(pos(At,AtV1,AtO1,_X,Vars), [A|As0], _),
	!,
	format('[~d] +~w(~@) ~d-~d [~d]~n', [N, At, portray_vars(Vars), AtV1, AtO1, Len]).

portray_vars([]).
portray_vars([V|Vs]) :-
	portray_vars(Vs, V).
portray_vars([], V) :-
	print(V).
portray_vars([V|Vs], V0) :-
	format('~p, ~@', [V0, portray_vars(Vs, V)]).
	

% = contract(+InGraph,-OutGraph, TraceDL, RootNodeAcc)
%
% perform all valid contractions on InGraph producing OutGraph;
% these are Danos-style contractions, performed in a first-found
% search.
%
% In addition, it returns a Trace of the contractions performed (as
% a difference list) and updates the root nodes of the graph (using
% an accumulator).

contract(Graph0, Graph, L0, L, R0, R) :-
        contract1(Graph0, Graph1, L0, L1, R0, R1),
        portray_graph(Graph1),
        !,
        contract(Graph1, Graph, L1, L, R1, R).
contract(Graph, Graph, L, L, R, R).

% par contraction
contract1(Graph0, [vertex(N1,Cs,FVs,Rs)|Graph], [N0-par(N1)|Rest], Rest, Roots0, Roots) :-
        select(vertex(N0, As, FVsA, Ps0), Graph0, Graph1),
        select(par(N1, N1), Ps0, Ps),
	select(vertex(N1, Bs, FVsB, Qs), Graph1, Graph2),
	\+ cyclic(Qs, Graph2, N0),
	!,
	append(As, Bs, Cs),
	append(Ps, Qs, Rs0),
	merge_fvs(FVsA, FVsB, FVs),
	replace_graph(Graph2, Rs0, N0, N1, Graph, Rs),
        update_roots_contraction(Roots0, Graph, N0, N1, Roots).
% forall contraction
contract1(Graph0, [vertex(N1,Cs,FVs,Rs)|Graph], [N0-univ(U,N1)|Rest], Rest, Roots0, Roots) :-
        select(vertex(N0, As, FVsA, Ps0), Graph0, Graph1),
        select(univ(U, N1), Ps0, Ps),
	select(vertex(N1, Bs, FVsB, Qs), Graph1, Graph2),
	no_occurrences(Bs, Qs, Graph2, U),
	no_occurrences1(FVsA, U),
	no_occurrences(Graph2, U),
	!,
	append(As, Bs, Cs),
	append(Ps, Qs, Rs0),
	merge_fvs(FVsA, FVsB, FVs),
	replace_graph(Graph2, Rs0, N0, N1, Graph, Rs),
        update_roots_contraction(Roots0, Graph, N0, N1, Roots).

% = no_occurrences
%
% verify that the module above the forall link has no remaining occurrences of the eigenvariable
% of the link in atomic formulas
%
% TODO: this can surely be done in a smarter way. For example, it only makes sense to try and
% contract a forall link after all atomic formulas containing its eigenvariable have been
% connected.

no_occurrences([], Ps, G, V) :-
	no_occurrences_pars(Ps, G, V).
no_occurrences([A|As], Ps, G, V) :-
	no_atom_occurrences(A, V),
	no_occurrences(As, Ps, G, V).

no_atom_occurrences(pos(_, _, _, _, Vs), V) :-
	no_varlist_occurrences(Vs, V).
no_atom_occurrences(neg(_, _, _, _, Vs), V) :-
	no_varlist_occurrences(Vs, V).

no_varlist_occurrences([], _).
no_varlist_occurrences([V|Vs], W) :-
	V \== var(W),
	no_varlist_occurrences(Vs, W).

no_occurrences_pars([], _, _).
no_occurrences_pars([P|Ps], G0, V) :-
	no_occurrences_par(P, V, G0, G),
	no_occurrences_pars(Ps, G, V).

no_occurrences_par(univ(_,N1), V, G0, G) :-
    (
	selectchk(vertex(N1,Cs,_,Rs), G0, G)
    ->			 
	no_occurrences(Cs, Rs, G, V)
    ;
        G = G0
    ).
no_occurrences_par(par(N1,N2), V, G0, G) :-
    (
	selectchk(vertex(N1,Cs,_,Rs), G0, G1)
    ->			 
	no_occurrences(Cs, Rs, G1, V)
    ;
        G1 = G0
    ),
    (
	selectchk(vertex(N2,Ds,_,Ss), G1, G)
    ->			 
	no_occurrences(Ds, Ss, G, V)
    ;
        G = G1
    ).


% test for cyclicity
% G2 contains unvisited nodes
% P contains paths from current node
% N is the node to reach for a cycle.

cyclic([P|_], Graph, N) :-
    cyclic1(P, Graph, N).
cyclic([_|Ps], Graph, N) :-
    cyclic(Ps, Graph, N).

cyclic1(par(M,P), Graph0, N) :-
    (
       N =:= M
    ;
       N =:= P
    ;
       select(vertex(M,_,_,Ps), Graph0, Graph),
       cyclic(Ps, Graph, N)
    ;
       P \== M,
       select(vertex(P,_,_,Ps), Graph0, Graph),
       cyclic(Ps, Graph, N)
    ).
cyclic1(univ(_,M), Graph0, N) :-
    (
       N =:= M
     ;
       select(vertex(M,_,_,Ps), Graph0, Graph),
       cyclic(Ps, Graph, N)
    ).        

% = connected(+Graph)
%
% true if Graph is connected or at least can be made connected
% by vertex identifications (corresponding to axioms)
%
% This test presupposes that all possible contractions for the
% current graph have been performed.

connected([V|Vs]) :-
   (
       Vs = []
   ->
       /* a single-node graph is connected */
       true
   ;
       connected1([V|Vs])
   ).

connected1([]).
connected1([vertex(_,As,_,Ps)|Vs]) :-
    (
        As = []
    ->  /* in a multiple-node graph, if a node has no */
        /* atoms, it must have a link */
	/* In other words, in a fully contracted graph, */
	/* a node cannot have both As and Ps empty */    
        Ps = [_|_]
    ;
        true
    ),
    connected1(Vs).

% = no_occurrences(+Graph, +VarNum)
%
% walks through +Graph and checks that none of its vertices
% has the variable +VarNum in their list of free variables
% (this is the condition on the forall contraction)

no_occurrences([], _).
no_occurrences([vertex(_, _, FVs, _)|Rest], U) :-
        no_occurrences1(FVs, U),
        no_occurrences(Rest, U).

no_occurrences1([], _).
no_occurrences1([V|Vs], U) :-
        var(U) \== V,
        no_occurrences1(Vs, U).

% =======================================
% =      Formula/sequent unfolding      =
% =======================================

% transforms sequents, antecedents and (polarized) formulas into graphs

% = unfold_sequent(+ListOfFormulas, +GoalFormula, -RootNodes, -Vertices, -Semantics) 
%
% unfold the sequent ListOfFormulas |- GoalFormula into the graph Vertices, keeping
% track of the RootNodes (of the resulting forest) and the term representing the
% Semantics (after all axiom links have been performed).
%
% In addition, for later proof generation, all nodes in the initial graph will have
% their node number, polarity and the formula corresponding to this node stored by
% means of an asserted
%
% node_formula(NodeNumber, Polarity, Formula)
%
% declaration (with Polarity one of pos/neg).
	    
unfold_sequent(List, Goal, Roots, Vs0, Sem, Stats) :-
        retractall(node_formula(_,_,_)),
	init_stats(Stats0),
	unfold_antecedent(List, 0, _W, 0, N0, 0, M, Roots0, Vs0, [vertex(N0,As,FVsG,Es)|Vs1], Stats0, Stats1),
	N is N0 + 1,
	append(Roots0, [N0], Roots),
	number_subformulas_pos(Goal, N0, N, _, _-NGoal),
        assert(node_formula(N0, pos, NGoal)),
	free_vars_p(Goal, FVsG),
	unfold_pos(NGoal, Sem, M, _, As, [], Es, [], Vs1, [], Stats1, Stats).

unfold_antecedent([], W, W, N, N, M, M, [], Vs, Vs, Stats, Stats).
unfold_antecedent([F|Fs], W0, W, N0, N, M0, M, [N0|Rs], [vertex(N0,As,FVsF,Es)|Vs0], Vs, Stats0, Stats) :-
        N1 is N0 + 1,
        W1 is W0 + 1,
	free_vars_n(F, FVsF),
	number_subformulas_neg(F, N0, N1, N2, _-NF),
        assert(node_formula(N0, neg, NF)),
	unfold_neg(NF, '$VAR'(W0), M0, M1, As, [], Es, [], Vs0, Vs1, Stats0, Stats1),
	unfold_antecedent(Fs, W1, W, N2, N, M1, M, Rs, Vs1, Vs, Stats1, Stats).

%= unfold_neg(+Formula, Sem, VertexNo, VarNoAcc, AtomsDL, AtomsDL, EdgesDL, VerticesDL)

unfold_neg(at(A,C,N,Vars), X, M, M, [neg(A,C,N,X,Vars)|As], As, Es, Es, Vs, Vs, Stats0, Stats) :-
	add_neg_atom(Stats0, Stats).
unfold_neg(forall(_,_-A), X, M0, M, As0, As, Es0, Es, Vs0, Vs, Stats0, Stats) :-
	add_unary_tensor(Stats0, Stats1),
	unfold_neg(A, X, M0, M, As0, As, Es0, Es, Vs0, Vs, Stats1, Stats).
unfold_neg(exists(var(M0),N-A), X, M0, M, As, As, [univ(M0,N)|Es], Es, [vertex(N,Bs,FVsA,Fs)|Vs0], Vs, Stats0, Stats) :-
        assert(node_formula(N, neg, A)),
        free_vars_n(A, FVsA),
	M1 is M0 + 1,
	add_unary_par(Stats0, Stats1),
	unfold_neg(A, X, M1, M, Bs, [], Fs, [], Vs0, Vs, Stats1, Stats).
unfold_neg(p(N0-A,N1-B), X, M0, M, As, As, [par(N0,N1)|Es], Es, [vertex(N0,Bs,FVsA,Fs),vertex(N1,Cs,FVsB,Gs)|Vs0], Vs, Stats0, Stats) :-
        assert(node_formula(N0, neg, A)),
        assert(node_formula(N1, neg, B)),
        free_vars_n(A, FVsA),
        free_vars_n(B, FVsB),
	add_binary_par(Stats0, Stats1),
	unfold_neg(A, pi1(X), M0, M1, Bs, [], Fs, [], Vs0, Vs1, Stats1, Stats2),
	unfold_neg(B, pi2(X), M1, M, Cs, [], Gs, [], Vs1, Vs, Stats2, Stats).
unfold_neg(impl(_-A,_-B), X, M0, M, As0, As, Es0, Es, Vs0, Vs, Stats0, Stats) :-
	add_binary_tensor(Stats0, Stats1),
	unfold_pos(A, Y, M0, M1, As0, As1, Es0, Es1, Vs0, Vs1, Stats1, Stats2),
	unfold_neg(B, appl(X,Y), M1, M, As1, As, Es1, Es, Vs1, Vs, Stats2, Stats).

%= unfold_pos(+Formula, Sem, VertexNo, VarNoAcc, AtomsDL, AtomsDL, EdgesDL, VerticesDL)

unfold_pos(at(A,C,N,Vars), X, M, M, [pos(A,C,N,X,Vars)|As], As, Es, Es, Vs, Vs, Stats0, Stats) :-
	add_pos_atom(Stats0, Stats).
unfold_pos(forall(var(M0),N0-A), X, M0, M, As, As, [univ(M0,N0)|Es], Es, [vertex(N0,Bs,FVsA,Fs)|Vs0], Vs, Stats0, Stats) :-
        assert(node_formula(N0, pos, A)),
        free_vars_p(A, FVsA),
	M1 is M0 + 1,
	add_unary_par(Stats0, Stats1),
	unfold_pos(A, X, M1, M, Bs, [], Fs, [], Vs0, Vs, Stats1, Stats).
unfold_pos(exists(_,_-A), X, M0, M, As0, As, Es0, Es, Vs0, Vs, Stats0, Stats) :-
	add_unary_tensor(Stats0, Stats1),
	unfold_pos(A, X, M0, M, As0, As, Es0, Es, Vs0, Vs, Stats1, Stats).
unfold_pos(p(_-A,_-B), pair(X,Y), M0, M, As0, As, Es0, Es, Vs0, Vs, Stats0, Stats) :-
	add_binary_tensor(Stats0, Stats1),
	unfold_pos(A, X, M0, M1, As0, As1, Es0, Es1, Vs0, Vs1, Stats1, Stats2),
	unfold_pos(B, Y, M1, M, As1, As, Es1, Es, Vs1, Vs, Stats2, Stats).
unfold_pos(impl(N0-A,N1-B), lambda(X,Y), M0, M, As, As, [par(N0,N1)|Es], Es, [vertex(N0,Bs,FVsA,Fs),vertex(N1,Cs,FVsB,Gs)|Vs0], Vs, Stats0, Stats) :-
        assert(node_formula(N0, neg, A)),
        assert(node_formula(N1, pos, B)),
        free_vars_n(A, FVsA),
        free_vars_p(B, FVsB),
	add_binary_par(Stats0, Stats1),
	unfold_neg(A, X, M0, M1, Bs, [], Fs, [], Vs0, Vs1, Stats1, Stats2),
	unfold_pos(B, Y, M1, M, Cs, [], Gs, [], Vs1, Vs, Stats2, Stats).

% = number_subformulas_neg(+Formula, +CurrentNodeNumber, +NextNodeNumberIn, -NextNodeNumberOut, -NumberFormula)
%
% assigns node numbers to all subformulas of Formula, allowing us to designate
% all (sub-)formula occurrences in a sequent by a unique node number, and in the
% case of atomic formulas a combination of node-index (where index is a
% left-to-right numbering of the atomic subformulas at a node).

number_subformulas_neg(F, C, N0, N, NF) :-
        number_subformulas_neg(F, C, N0, N, 1, _, NF).

number_subformulas_neg(at(A,Vars), C, N, N, M0, M, C-at(A,C,M0,Vars)) :-
        M is M0 + 1.
number_subformulas_neg(forall(X,A), C, N0, N, M0, M, C-forall(X,NA)) :-
	number_subformulas_neg(A, C, N0, N, M0, M, NA).
number_subformulas_neg(exists(X,A), C, N0, N, M, M, C-exists(X,NA)) :-
	N1 is N0 + 1,
	number_subformulas_neg(A, N0, N1, N, 1, _, NA).
number_subformulas_neg(p(A,B), C, N0, N, M, M, C-p(NA,NB)) :-
	N1 is N0 + 1,
	N2 is N1 + 1,
	number_subformulas_neg(A, N0, N2, N3, 1, _, NA),
	number_subformulas_neg(B, N1, N3, N, 1, _, NB).
number_subformulas_neg(impl(A,B), C, N0, N, M0, M, C-impl(NA,NB)) :-
	number_subformulas_pos(A, C, N0, N1, M0, M1, NA),
	number_subformulas_neg(B, C, N1, N, M1, M, NB).

number_subformulas_pos(F, C, N0, N, NF) :-
        number_subformulas_pos(F, C, N0, N, 1, _, NF).

number_subformulas_pos(at(A,Vars), C, N, N, M0, M, C-at(A,C,M0,Vars)) :-
	M is M0 + 1.
number_subformulas_pos(forall(X,A), C, N0, N, M, M, C-forall(X,NA)) :-
	N1 is N0 + 1,
	number_subformulas_pos(A, N0, N1, N, 1, _, NA).
number_subformulas_pos(exists(X,A), C, N0, N, M0, M, C-exists(X,NA)) :-
	number_subformulas_pos(A, C, N0, N, M0, M, NA).
number_subformulas_pos(p(A,B), C, N0, N, M0, M, C-p(NA,NB)) :-
	number_subformulas_pos(A, C, N0, N1, M0, M1, NA),
	number_subformulas_pos(B, C, N1, N, M1, M, NB).
number_subformulas_pos(impl(A,B), C, N0, N, M, M, C-impl(NA,NB)) :-
	N1 is N0 + 1,
	N2 is N1 + 1,	
	number_subformulas_neg(A, N0, N2, N3, 1, _, NA),
	number_subformulas_pos(B, N1, N3, N, 1, _, NB).


% =======================================
% =             Input/output            =
% =======================================

mark_progress(G) :-
	length(G, L),
	format_error('~D.', [L]),
        flush_output(user_error).
	

% = sequent statistics predicates

init_stats(stats(0,0,0,0,0,0)).

add_neg_atom(stats(A0,B,C,D,E,F), stats(A,B,C,D,E,F)) :-
	A is A0 + 1.

add_pos_atom(stats(A,B0,C,D,E,F), stats(A,B,C,D,E,F)) :-
	B is B0 + 1.

add_unary_tensor(stats(A,B,C0,D,E,F), stats(A,B,C,D,E,F)) :-
	C is C0 + 1.

add_unary_par(stats(A,B,C,D0,E,F), stats(A,B,C,D,E,F)) :-
	D is D0 + 1.

add_binary_tensor(stats(A,B,C,D,E0,F), stats(A,B,C,D,E,F)) :-
	E is E0 + 1.

add_binary_par(stats(A,B,C,D,E,F0), stats(A,B,C,D,E,F)) :-
	F is F0 + 1.


portray_sequent_statistics(stats(A,B,C,D,E,F)) :-
   (
	A =:= B
    ->
	format_error('~NAtoms:   ~|~t~D~4+~n', [A])
    ;
        format_error('~NAtoms:   ~|~t-~D~4+  ~|~t+~D~4+~n', [A,B])
    ),
        format_error('Unary : T~|~t~D~4+ P~|~t~D~4+~n', [C,D]),
	format_error('Binary: T~|~t~D~4+ P~|~t~D~4+~n', [E,F]).




% = print_trace(+Stream, +List).
%
% output proof trace in List to Stream

print_trace(Stream, [A|As]) :-
        format(Stream, '~n= Proof trace =~n', []),
        print_trace(As, A, Stream).

print_trace([], A, Stream) :-
        format(Stream, '~p~n= End of trace =~2n', [A]).
print_trace([B|Bs], A, Stream) :-
        format(Stream, '~p~n', [A]),
        print_trace(Bs, B, Stream).


% = print_list(+List)
%
% output List to user_error

print_list([]).
print_list([A|As]) :-
	format_error('~p~n', [A]),
	print_list(As).

% = write_proof(P)
%
% output a message stating P proofs have been found

write_proofs(P) :-
   (
       P =:= 0
   ->
       format_error('No proofs found!~n', [])
   ;
       P =:= 1
   ->
       format_error('1 proof found.~n', [])
   ;
       format_error('~D proofs found.~n', [P])
   ).

% = write_axioms(A)
%
% output a message stating A axioms have been performed

write_axioms(A) :-
   (
       A =:= 0
   ->
       format_error('No axioms performed!~n', [])
   ;
       A =:= 1
   ->
       format_error('1 axiom performed.~n', [])
   ;
       format_error('~D axioms performed.~n', [A])
   ).

% = write_lookup(L)
%
% output a message stating L lexical lookups have been done

write_lookups(L) :-
   (
       L =:= 0
   ->
       format_error('No lexical lookups!~n', [])
   ;
       L =:= 1
   ->
       format_error('1 lexical lookup.~n', [])
   ;
       format_error('~D lexical lookups.~n', [L])
   ).


% = print_solutions(+ExampleNos, +NumSolutions)
%
% display for each example in ExampleNo its number of solutions
% in NumSolutions and print an overview of the number of failed,
% succeeded and total examples.

print_solutions(L, NS) :-
	open('parse_log.txt', write, Stream, []), 
	format(Stream, 'SentNo Solutions~n', []),
	format_error('SentNo Solutions~n', []),
	print_solutions(L, Stream, 0, 0, NS),
	close(Stream).
print_solutions([], Stream, S, F, []) :-
	Total is S + F,
	format(Stream, '~nTotal sentences :~|~t~d~4+~nSucceeded       :~|~t~d~4+~nFailed          :~|~t~d~4+~n', [Total, S, F]),
	format_error('~nTotal sentences :~|~t~d~4+~nSucceeded       :~|~t~d~4+~nFailed          :~|~t~d~4+~n', [Total, S, F]).
print_solutions([N|Ns], Stream, S0, F0, [P-SemList|Ps]) :-
	format(Stream, '~|~t~d~6+ ~|~t~d~9+', [N,P]),
	format_error('~|~t~d~6+ ~|~t~d~9+', [N,P]),
    (
	P =:= 0
    ->
        format(Stream, ' * ~p~n', [SemList]),
        format_error(' * ~p~n', [SemList]),
	F is F0 + 1,
	S = S0
    ;
        format(Stream, '   ~p~n', [SemList]),
        format_error('   ~p~n', [SemList]),
        S is S0 + 1,
        F = F0
    ),
	print_solutions(Ns, Stream, S, F, Ps).

% = some test predicates

test :-
        /* this should fail ! */
	prove([forall(X,exists(Y,at(f,[X,Y])))], exists(V,forall(W,at(f,[W,V])))).
test0 :-
	prove([exists(X,forall(Y,at(f,[X,Y])))], forall(V,exists(W,at(f,[W,V])))).

test1 :-
        translate_lambek(p(dr(at(np),at(n)),at(n)), [0,1], F),
        prove([F], at(np, [0,1])).

test2 :-
	prove([at(np,[0,1]),forall(X,impl(at(np,[X,1]),at(s,[X,2])))], at(s,[0,2])).

test3 :-
	prove([forall(Y,forall(Z,impl(impl(at(np,[0,1]),at(s,[Y,Z])),at(s,[Y,Z])))),forall(X,impl(at(np,[X,1]),at(s,[X,2])))], at(s,[0,2])).

test4 :-
        translate_hybrid(at(np), lambda(X,appl(john,X)), john, 0, 1, John),
	translate_hybrid(h(h(at(s),at(np)),at(np)), lambda(P,lambda(Q,lambda(Z,appl(Q,appl(loves,appl(P,Z)))))), loves, 1, 2, Loves),
        translate_hybrid(at(np), lambda(V,appl(mary,V)), mary, 2, 3, Mary),
	prove([John, Loves, Mary], at(s, [0,3])).

test5 :-
        translate_hybrid(at(np), lambda(X,appl(john,X)), john, 0, 1, John),
	translate_hybrid(h(h(at(s),at(np)),at(s)), lambda(P,lambda(Q,lambda(Z,appl(Q,appl(believes,appl(P,Z)))))), believes, 1, 2, Believes),
	translate_hybrid(h(at(s),h(at(s),at(np))), lambda(VP,lambda(Z,appl(appl(VP,someone),Z))), someone, 2, 3, Someone),
	translate_hybrid(h(at(s),at(np)), lambda(S,lambda(Z1,appl(S,appl(left,Z1)))), left, 3, 4, Left),
	prove([John, Believes, Someone, Left], at(s, [0,4])).

% = I need a better axiom selection strategy

% succeeds, but proof generation fails
test6 :-
	translate_displacement(at(np), [0,1], John),
	translate_displacement(dl(at(np),at(s)), [1,2], Left),
	translate_displacement(dr(dl(dl(at(np),at(s)),dl(at(np),at(s))),at(s)), [2,3], Before),
	translate_displacement(at(np), [3,4], Mary),
	translate_displacement(dl(dr(dr(>,dl(at(np),at(s)),dl(at(np),at(s))),dl(at(np),at(s))),dr(>,dl(at(np),at(s)),dl(at(np),at(s)))), [4,5], Did),
	prove([John,Left,Before,Mary,Did], at(s,[0,5])).

% fails (verify!)
test7 :-
        translate_hybrid(at(np), lambda(X,appl(john,X)), john, 0, 1, John),
	translate_hybrid(dr(dl(at(np),at(s)),at(np)), lambda(Y,appl(studies,Y)), studies, 1, 2, Studies),
        translate_hybrid(at(np), lambda(Z,appl(logic,Z)), logic, 2, 3, Logic),
	translate_hybrid(h(h(h(at(s),dr(dl(at(np),at(s)),at(np))),h(at(s),dr(dl(at(np),at(s)),at(np)))),h(at(s),dr(dl(at(np),at(s)),at(np)))),
			 lambda(STV2,lambda(STV1,lambda(TV,lambda(V,appl(appl(STV1,TV),appl(and,appl(appl(STV2,lambda(W,W)),V))))))), and, 3, 4, And),
        translate_hybrid(at(np), lambda(X1,appl(charles,X1)), charles, 4, 5, Charles),
        translate_hybrid(at(np), lambda(Z1,appl(phonetics,Z1)), phonetics, 5, 6, Phonetics),
	prove([John, Studies, Logic, And, Charles, Phonetics], at(s,[0,6])).

%

test_eta :-
	prove([exists(Y,p(at(a,[Y]),at(b,[Y])))], exists(Y,p(at(a,[Y]),at(b,[Y])))).
	
% = test translations

test_d1(F) :-
	/* generalized quantifier */
	translate_displacement(dl(>,dr(>,at(s),at(np)),at(s)), [1,2], F).
test_d2(F) :-
	/* did */
	translate_displacement(dl(dr(dr(>,at(vp),at(vp)),at(vp)),dr(>,at(vp),at(vp))), [4,5], F).
test_d3(F) :-
	/* himself */
	translate_displacement(dl(<,dr(<,dr(>,at(vp),at(np)),at(np)),dr(>,at(vp),at(np))), [3,4], F).

test_h1(F) :-
	translate_hybrid(h(at(s),at(np)), lambda(P,lambda(Z,appl(P,appl(walks,Z)))), walks, 1, 2, F).
test_h2(F) :-
	translate_hybrid(h(at(s),h(at(s),at(np))), lambda(P,lambda(Z,appl(appl(P,everyone),Z))), everyone, 0, 1, F).

% = generate exhaustive test file	


% = control over messages
%
% use output_error(0) to suppress diagnostic messages

:- dynamic output_error/1, output_info/1.

% output_error(0) % suppress diagnostic messages
output_error(1). % print diagnostic messages
output_info(1).

format_error(_, _) :-
	output_error(0),
	!.
format_error(X, Y) :-
	format(user_error, X, Y).


format_info(_, _) :-
	output_info(0),
	!.
format_info(X, Y) :-
	format(user_output, X, Y).