https://github.com/RichardMoot/GrailLight
Tip revision: 67fbacd0e365d9008c021016377c0cfe1f1e309d authored by Richard Moot on 27 April 2021, 15:02:38 UTC
Update Supertag.tcl
Update Supertag.tcl
Tip revision: 67fbacd
print_proof.pl
% ==============================================
% = output Prolog proof =
% ==============================================
:- module(print_proof, [print_proof/3,print_proof/4,xml_proof/3]).
:- use_module(sem_utils, [get_fresh_variable_number/2]).
:- dynamic ignore_variables/1.
ignore_variables(false).
print_proof(Index, Proof, Stream, Bool) :-
retractall(ignore_variables(_)),
assert(ignore_variables(Bool)),
print_proof(Index, Proof, Stream).
print_proof(Index, Proof, Stream) :-
get_fresh_variable_number(Proof, Max),
numbervars(Proof, Max, _, [singletons(true)]),
print_title(Proof, Index, Stream),
format(Stream, 'proof(~w, ', [Index]),
print_proof1(Proof, 0, Stream),
format(Stream, ').~2n', []).
print_proof1(rule(RName,Pros,FormulaSem0,Ds), T0, Stream) :-
update_sem(FormulaSem0, FormulaSem),
(
Ds = []
->
format(Stream, 'rule(~W, ~W, ~@, [])', [RName,[numbervars(true),quoted(true)],Pros,[quoted(true)],print_formula_sem(FormulaSem,Stream)])
;
Ds = [D|Ds0],
T is T0 + 3,
format(Stream, 'rule(~W, ~W, ~@, [~n', [RName,[numbervars(true),quoted(true)],Pros,[quoted(true)],print_formula_sem(FormulaSem,Stream)]),
tab(Stream, T),
print_proof_list(Ds0, D, T, Stream),
format(Stream, '])', [])
).
print_proof_list([], D, T, Stream) :-
print_proof1(D, T, Stream),
nl(Stream),
tab(Stream, T).
print_proof_list([D|Ds], D0, T, Stream) :-
print_proof1(D0, T, Stream),
write(Stream, ','),
nl(Stream),
tab(Stream, T),
print_proof_list(Ds, D, T, Stream).
print_title(rule(_, Pros, _, _), Sent, Stream) :-
format(Stream, '% ~w. ', [Sent]),
print_pros(Pros, Stream),
nl(Stream),
nl(Stream).
print_pros(Atom, Stream) :-
atomic(Atom),
!,
format(Stream, '~w ', [Atom]).
print_pros(L-R, Stream) :-
format(Stream, '~w-~w', [L,R]).
print_pros(hyp(_,_,Pros), Stream) :-
format(Stream, '~w ', [Pros]).
print_pros(leaf(_,_,Pros,_,_), Stream) :-
format(Stream, '~w ', [Pros]).
print_pros(p(_,_,_,L,R), Stream) :-
print_pros(L, Stream),
print_pros(R, Stream).
print_pros(p(_,L,R), Stream) :-
print_pros(L, Stream),
print_pros(R, Stream).
print_pros(t(List), Stream) :-
print_pros_list(List, Stream).
print_pros_list([], _).
print_pros_list([P|Ps], Stream) :-
print_pros(P, Stream),
print_pros_list(Ps, Stream).
update_sem(lit(let)-_, lit(let)-true) :-
/* special case for let to avoid singleton variable warnings */
!.
update_sem(FS, FS).
%update_sem(Formula-Sem, Formula-Sem) :-
% get_max_variable_number(Sem, Max),
% numbervars(Sem, Max, _).
print_formula_sem(tuple(Formula,Sem,Stacks), Stream) :-
print_formula_sem_stacks(Formula, Sem, Stacks, Stream).
print_formula_sem(Formula-Sem, Stream) :-
print_formula_sem(Formula, Sem, Stream).
print_formula_sem_stacks(Formula, Sem, Stacks, Stream) :-
print_formula(Formula, Stream),
format(Stream, '-~W', [Sem, [quoted(true)]]),
print_stacks(Stacks, Stream).
print_stacks(stacks(S1,S2,S3,S4), Stream) :-
print_stack(S1, 1, Stream),
print_stack(S2, 2, Stream),
print_stack(S3, 3, Stream),
print_stack(S4, 4, Stream).
print_stack(Stack, SN, Stream) :-
write(Stream, '-['),
print_stack0(Stack, SN, Stream).
print_stack0([], _, Stream) :-
write(Stream, ']').
print_stack0([S|Ss], SN, Stream) :-
print_stack1(Ss, S, SN, Stream).
print_stack1([], S, SN, Stream) :-
format(Stream, '~@]', [print_stack_item1(S,SN,Stream)]).
print_stack1([S|Ss], S0, SN, Stream) :-
format(Stream, '~@,', [print_stack_item1(S0,SN,Stream)]),
print_stack1(Ss, S, SN, Stream).
print_stack_item1(_-T, SN, Stream) :-
print_stack_item1(T, SN, Stream).
print_stack_item1(t(I1,I2,I3,I4), SN, Stream) :-
print_stack_item2(SN, I1, I2, I3, I4, Stream).
print_stack_item1(t(I1,I2,I3,I4,_), SN, Stream) :-
print_stack_item2(SN, I1, I2, I3, I4, Stream).
print_stack_item2(1, _, _, F, _, Stream) :-
print_formula_nv(F, Stream).
print_stack_item2(2, _, _, F, _, Stream) :-
print_formula_nv(F, Stream).
print_stack_item2(3, F, _, _, _, Stream) :-
print_formula_nv(F, Stream).
print_stack_item2(4, F, _, _, _, Stream) :-
print_formula_nv(F, Stream).
print_formula_nv(F0, Stream) :-
simplify_formula(F0, F),
print_formula(F, Stream).
simplify_formula(X, X) :-
var(X),
!.
simplify_formula(lit(s(A0)), lit(s(A))) :-
!,
simplify_argument(A0, A).
simplify_formula(lit(pp(A0)), lit(pp(A))) :-
!,
simplify_argument(A0, A).
simplify_formula(lit(np(_,_,_)), lit(np)) :-
!.
simplify_formula(lit(X), lit(X)) :-
!.
simplify_formula(dl(I,A0,B0), dl(I,A,B)) :-
simplify_formula(A0, A),
simplify_formula(B0, B).
simplify_formula(dr(I,A0,B0), dr(I,A,B)) :-
simplify_formula(A0, A),
simplify_formula(B0, B).
simplify_formula(p(I,A0,B0), p(I,A,B)) :-
simplify_formula(A0, A),
simplify_formula(B0, B).
simplify_formula(dia(_,A0), dia(1,A)) :-
simplify_formula(A0, A).
simplify_formula(box(_,A0), box(1,A)) :-
simplify_formula(A0, A).
simplify_argument('$VAR'(_), '$VAR'(0)) :-
!.
simplify_argument(A, A).
print_formula_sem(Formula, Sem, Stream) :-
print_formula(Formula, Stream),
format(Stream, '-~W', [Sem, [quoted(true)]]).
print_formula(lit(A), Stream) :-
!,
format(Stream, 'lit(~@)', [print_formula1(A,Stream)]).
print_formula(dr(I,A,B), Stream) :-
!,
format(Stream, 'dr(~w,~@,~@)', [I,print_formula(A,Stream),print_formula(B,Stream)]).
print_formula(dl(I,A,B), Stream) :-
!,
format(Stream, 'dl(~w,~@,~@)', [I,print_formula(A,Stream),print_formula(B,Stream)]).
print_formula(p(I,A,B), Stream) :-
!,
format(Stream, 'p(~w,~@,~@)', [I,print_formula(A,Stream),print_formula(B,Stream)]).
print_formula(dia(I,A), Stream) :-
!,
format(Stream, 'dia(~w,~@)', [I,print_formula(A,Stream)]).
print_formula(box(I,A), Stream) :-
!,
format(Stream, 'box(~w,~@)', [I,print_formula(A,Stream)]).
print_formula(Term, Stream) :-
functor(Term, F, A),
format(user_error, '{Warning: unknown term ~w with functor ~w/~w}', [Term,F,A]),
write(Stream, Term).
print_formula1(np(A,B,C), Stream) :-
format(Stream, 'np(~@,~@,~@)', [print_case_item(A,Stream),print_case_item(B,Stream),print_case_item(C,Stream)]).
print_formula1(s(A), Stream) :-
nonvar(A),
A = inf(B),
!,
format(Stream, 's(inf(~@))', [print_item(B,Stream)]).
print_formula1(s(A), Stream) :-
!,
format(Stream, 's(~@)', [print_item(A,Stream)]).
print_formula1(pp(A), Stream) :-
!,
format(Stream, 'pp(~@)', [print_item(A,Stream)]).
print_formula1(n, Stream) :-
!,
write(Stream, n).
print_formula1(np, Stream) :-
!,
write(Stream, np).
print_formula1(cl_r, Stream) :-
!,
write(Stream, cl_r).
print_formula1(cl_y, Stream) :-
!,
write(Stream, cl_y).
print_formula1(txt, Stream) :-
!,
write(Stream, txt).
print_formula1(let, Stream) :-
!,
write(Stream, let).
print_formula1(Strange, Stream) :-
format(user_error, '{Warning: unknown atom: ~w}~n', [Strange]),
write(Stream, Strange).
print_item(V, Stream) :-
var(V),
!,
(ignore_variables(true) -> write(Stream, '_') ; print(Stream, V)).
print_item('$VAR'(N), Stream) :-
integer(N),
!,
(ignore_variables(true) -> write(Stream, '_') ; print(Stream, '$VAR'(N))).
print_item('$VAR'(_), Stream) :-
!,
write(Stream, '_').
print_item(Atom, Stream) :-
format(Stream, '~W', [Atom,[quoted(true)]]).
print_case_item('$VAR'(_), Stream) :-
!,
write(Stream, '_').
print_case_item(Atom, Stream) :-
format(Stream, '~W', [Atom,[quoted(true)]]).
% ==============================================
% = output XML proof =
% ==============================================
xml_proof(Index, Proof, Stream) :-
format(Stream, '<?xml version="1.0" encoding="UTF-8"?>~n', []),
numbervars(Proof, 0, _),
Proof = rule(_, Pros, _, _),
format(Stream, '<!-- ~w. ', [Index]),
print_pros_xml(Pros, Stream),
format(Stream, '>~n', []),
xml_proof1(Proof, 0, Stream).
xml_proof1(rule(A,B0,C,Ds), T0, Stream) :-
reduce_pros(B0, B),
nl(Stream),
tab(Stream, T0),
format(Stream, '<rule name="~w" pros="~q" formula="~w">', [A,B,C]),
T is T0 + 3,
xml_proof_list(Ds, T, Stream),
nl(Stream),
tab(Stream, T0),
format(Stream, '</rule>', []).
xml_proof_list([], _, _).
xml_proof_list([P|Ps], T, Stream) :-
xml_proof1(P, T, Stream),
% nl(Stream),
% tab(Stream, T),
xml_proof_list(Ps, T, Stream).
print_pros_xml(Atom, Stream) :-
atomic(Atom),
!,
print_pros_xml1(Atom, Stream).
print_pros_xml('$VAR'(N), Stream) :-
format(Stream, 'p~w', [N]).
print_pros_xml(L-R, Stream) :-
format(Stream, '~w-~w', [L,R]).
print_pros_xml(leaf(_,_,Pros,_,_), Stream) :-
print_pros_xml1(Pros, Stream).
print_pros_xml(p(_,_,_,L,R), Stream) :-
print_pros_xml(L, Stream),
print_pros_xml(R, Stream).
print_pros_xml(p(_,L,R), Stream) :-
print_pros_xml(L, Stream),
print_pros_xml(R, Stream).
print_pros_xml1(Pros0, Stream) :-
name(Pros0, Codes0),
xml_codes(Codes0, Codes),
name(Pros, Codes),
write(Stream, Pros).
xml_codes([], []).
xml_codes([C|Cs], Ds0) :-
(
C = 38
->
/* & */
Ds0 = [38,97,109,112,59|Ds]
;
C = 39
->
/* ' */
Ds0 = [38,97,112,111,115,59|Ds]
;
C = 34
->
/* " */
Ds0 = [38,113,117,111,116,59|Ds]
;
/* default */
Ds0 = [C|Ds]
),
xml_codes(Cs, Ds).
reduce_pros(Atom, Atom) :-
atomic(Atom),
!.
reduce_pros('$VAR'(N), Atom) :-
atomic_concat(p, N, Atom).
reduce_pros(L-R, L-R).
reduce_pros(p(I,L,R), p(I,L,R)).
reduce_pros(hyp(_,_,Pros), Pros).
reduce_pros(leaf(_,_,Pros,_,_), Pros).
reduce_pros(p(I,_,_,L0,R0), p(I,L,R)) :-
reduce_pros(L0, L),
reduce_pros(R0, R).