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
transform_proof.pl
#!/Applications/SWI-Prolog.app/Contents/MacOS/swipl -q -g start -f
:- module(transform_proof, [start/0,transform_proof/2,transform_all_proofs/0,transform_all_proofs/1, latex_transform/1, latex_transform_full/1]).
:- use_module(sem_utils, [replace_sem/4,get_fresh_variable_number/2,equivalent_semantics/2,unify_semantics/2]).
:- use_module(ordset, [ord_dup_union/3,ord_dup_insert/3,ord_subtract/3,ord_select/3,ord_subset/2]).
:- use_module(latex, [latex_proof/2,latex_header/2,latex_tail/1]).
:- use_module(print_proof, [print_proof/3,print_proof/4]).
:- dynamic user:proof/2.
start :-
current_prolog_flag(os_argv, Argv),
append(_, [A|Av], Argv),
file_base_name(A, 'transform_proof.pl'),
!,
chart_dir(ChDir),
nd_dir(NDDir),
tap(Av, ChDir, NDDir).
tap([], _, _) :-
/* treat all files if no file argument specified */
transform_all_proofs,
halt.
tap([F|Fs], ChDir, NDDir) :-
tap1([F|Fs], ChDir, NDDir).
tap1([], _, _) :-
halt.
tap1([File0|Files], ChDir, NDDir) :-
(
match_file(File0, File)
->
format(user_error, '~NStarting ~w~n', [File]),
atom_concat(File, '_proofs.pl', InFile0),
atom_concat(ChDir, InFile0, InFile),
atom_concat(File, '_nd.pl', OutFile0),
atom_concat(NDDir, OutFile0, OutFile),
abolish(user:proof/2),
user:compile(InFile),
transform_all_proofs(OutFile),
format(user_error, '~NDone ~w~n', [File])
;
format(user_error, '~NIgnored ~w~n', [File0])
),
tap1(Files, ChDir, NDDir).
match_file(File0, File) :-
/* coverts atoms like '8000' and '300' to Prolog integers */
name(File0, Name),
name(File1, Name),
infile(File1),
!,
File = File1.
match_file(File0, File) :-
name('chart_proofs/', X),
name('_proofs.pl', W),
name(File0, FN),
append(X, Y, FN),
append(V, W, Y),
name(File, V),
infile(File).
quote_mode(1, 1).
% ==============================================
% = proof transformations =
% ==============================================
infile(aa1).
infile(aa2).
infile(ab2).
infile(ae1).
infile(af2).
infile(ag1).
infile(ag2).
infile(ah1).
infile(ah2).
infile(ai1).
infile(ai2).
infile(aj1).
infile(ak1).
infile(ak2).
infile(al1).
infile(am1).
infile(am2).
infile(an1).
infile(an2).
infile(ao1).
infile(ao2).
infile(ap1).
infile(aq2).
infile(as2).
infile(at).
infile(300).
infile(1000).
infile(8000).
infile(annodis).
infile(frwiki1).
infile(frwiki2).
infile(europar).
infile(emea_d).
infile(emea_t).
infile(monde_a).
infile(monde_b).
chart_dir('chart_proofs/').
nd_dir('nd_proofs/').
% = transform_all_proofs
%
% transform all infiles chart proofs in chart_dir into natural deduction proofs in nd_dir.
transform_all_proofs :-
chart_dir(ChDir),
nd_dir(NDDir),
infile(Root),
format(user_error, '~NStarting ~w~n', [Root]),
atom_concat(Root, '_proofs.pl', InFile0),
atom_concat(ChDir, InFile0, InFile),
atom_concat(Root, '_nd.pl', OutFile0),
atom_concat(NDDir, OutFile0, OutFile),
abolish(proof/2),
compile(InFile),
transform_all_proofs(OutFile),
format(user_error, '~NDone ~w~n', [Root]),
fail.
transform_all_proofs.
% = transform_all_proofs(+OutFile)
%
% transform all proofs in memory (per the proof/2 predicate) into natural deduction
% files in the OutFile given as an argument.
transform_all_proofs(OutputFile) :-
open(OutputFile, write, Stream, []),
transform_all_proofs1(Stream).
transform_all_proofs1(Stream) :-
user:proof(N, P0),
(
transform_proof(P0, P)
->
print_proof(N, P, Stream, true)
;
format(user_error, '~N{Warning: failed to transform proof ~d!}~n', [N])
),
fail.
transform_all_proofs1(Stream) :-
close(Stream).
% = numbervars_proof(+Proof)
%
% uses numbervars/3 only on the different semantic components of the proof.
numbervars_proof(Proof) :-
numbervars_proof(Proof, 0, _).
numbervars_proof(rule(_, _, _-Sem, Premisses), N0, N) :-
/* ensure correct behaviour even when the semantics already contains occurrences of '$VAR'(N) terms */
get_fresh_variable_number(Sem, Max0),
Max is max(Max0, N0),
numbervars(Sem, Max, N1),
numbervars_proof_list(Premisses, N1, N).
numbervars_proof_list([], N, N).
numbervars_proof_list([P|Ps], N0, N) :-
numbervars_proof(P, N0, N1),
numbervars_proof_list(Ps, N1, N).
latex_transform(N) :-
user:proof(N, P),
transform_proof(P, Q),
open('proof.tex', write, Stream),
latex_header(Stream, 'paperwidth=400cm,textwidth=395cm'),
latex_proof(P, Stream),
latex_proof(Q, Stream),
latex_tail(Stream),
close(Stream).
latex_transform_full(N) :-
user:proof(N, P),
open('proof.tex', write, Stream),
latex_header(Stream, 'paperwidth=400cm,textwidth=395cm'),
latex_proof(P, Stream),
latex_transform_proof_full1(P, Stream),
latex_tail(Stream),
close(Stream).
latex_transform_proof_full1(P, Stream) :-
numbervars_proof(P),
latex_transform_proof_full1(P, 0, _N, Stream).
latex_transform_proof_full1(P, N0, N, Stream) :-
transform_proof(P, N0, N1, Q),
(
P = Q
->
N = N1
;
latex_proof(Q, Stream),
latex_transform_proof_full1(Q, N1, N, Stream)
).
transform_proof(P, Q) :-
numbervars_proof(P),
transform_proof1(P, 0, _N, Q).
% = iterate transform_proof/4 until the proof stays the same
transform_proof1(P, N0, N, Q) :-
transform_proof(P, N0, N1, Q1),
(
P = Q1
->
Q = Q1,
N = N1
;
transform_proof1(Q1, N1, N, Q)
).
% Invariant: N0 is the index of the first unused prosodic variable (that is '$VAR'(N0) does not occur in the proof).
% = remove "let" rule altogether
transform_proof(rule(let, Pros, D-Sem, [Proof1, Proof2]), N0, N, Proof) :-
(
Proof1 = rule(axiom, _, lit(let)-true, []),
Proof2 = rule(Nm, _, D-Sem, Proofs)
->
true
;
Proof1 = rule(Nm, _, D-Sem, Proofs),
Proof2 = rule(axiom, _, lit(let)-true, [])
->
true
),
N = N0,
Proof = rule(Nm, Pros, D-Sem, Proofs).
transform_proof(rule(gap_i, GoalPros, D-Sem, [Proof3, Proof2, Proof1]), N0, N,
rule(dr, GoalPros, D-Sem,
[rule(dl, p(0,ProsC2,Pros1), dr(0,Y,box(I,dia(I,dr(0,Z,V))))-appl(Term2,lambda(Var,TermX)),
[rule(drdiaboxi(I,N0), ProsC2, X-lambda(Var,TermX), [ProofC1]),
Proof1
]),
Proof2
])) :-
N1 is N0 + 1,
Sem = appl(appl(Term2,lambda(Var,TermX)),_Term0),
rule_conclusion(Proof1, Pros1, ExtrForm, _),
rule_conclusion(Proof2, Pros2, dr(0,Z,V), _),
/* do a recursive transformation before replace_proof_bag which may otherwise erase information */
transform_proof1(Proof3, N1, N, Proof4),
rule_conclusion(Proof4, _Pros3, _, _),
ExtrForm = dl(0,X,dr(0,Y,box(I,dia(I,dr(0,Z,V))))),
bag_of_words(Pros2, Bag),
replace_proof_bag(Proof4, Bag, '$VAR'(N0), rule(hyp(N0), '$VAR'(N0), dr(0,Z,V)-Var, []), ProofC1),
/* TODO: globally replace Sem by Var in all of ProofC0 */
rule_conclusion(ProofC1, ProsC1, _, _),
replace_pros(ProsC1, '$VAR'(N0), '$TRACE'(N0), ProsC2),
!.
transform_proof(rule(gap_i, GoalPros, D-Sem, [Proof3, Proof2, Proof1]), N0, N,
rule(dr, GoalPros, D-Sem,
[rule(dl, p(0,ProsC2,Pros1), dr(0,Y,box(I,dia(I,dl(0,Z,V))))-appl(Term2,lambda(Var,TermX)),
[rule(drdiaboxi(I,N0), ProsC2, X-lambda(Var,TermX), [ProofC1]),
Proof1
]),
Proof2
])) :-
N1 is N0 + 1,
Sem = appl(appl(Term2,lambda(Var,TermX)),_Term0),
rule_conclusion(Proof1, Pros1, ExtrForm, _),
/* special case for vp gapping */
rule_conclusion(Proof2, Pros2, dl(0,Z,V), _),
/* do a recursive transformation before replace_proof_bag which may otherwise erase information */
transform_proof1(Proof3, N1, N, Proof4),
rule_conclusion(Proof4, _Pros3, _, _),
ExtrForm = dl(0,X,dr(0,Y,box(I,dia(I,dl(0,Z,V))))),
bag_of_words(Pros2, Bag),
replace_proof_bag(Proof4, Bag, '$VAR'(N0), rule(hyp(N0), '$VAR'(N0), dl(0,Z,V)-Var, []), ProofC1),
/* TODO: globally replace Sem by Var in all of ProofC0 */
rule_conclusion(ProofC1, ProsC1, _, _),
replace_pros(ProsC1, '$VAR'(N0), '$TRACE'(N0), ProsC2),
!.
transform_proof(rule(e_end, GoalPros, D-Sem, [Proof1, Proof2]), N0, N,
rule(dr, GoalPros, D-Sem,
[Proof1,
rule(drdiaboxi(I,N0), YZ, dr(0,C,dia(I,box(I,dr(0,A,B))))-true,
[Proof4])
])) :-
/* X = "et", YZ = sentence with extracted verb */
GoalPros = p(_,X,YZ),
ExtrForm = dr(0,D,dr(0,C,dia(I,box(I,dr(0,A,B))))),
rule_conclusion(Proof1, X, ExtrForm, _),
/* Pros = (prosody of) argument B */
find_e_start(Proof2, ef_start, X, ExtrForm, dr(0,A,B), N0, Pros, Proof3),
global_replace_pros(Proof3, Pros, p(0,'$VAR'(N0), Pros), N0, Proof4),
N is N0 + 1,
!.
transform_proof(rule(e_end, GoalPros, D-Sem, [Proof1, Proof2]), N0, N,
rule(dr, GoalPros, D-Sem,
[Proof1,
rule(drdiaboxi(I,N0), YZ, dr(0,C,dia(I,box(I,dl(0,A,B))))-true,
[Proof4])
])) :-
/* X = "et", YZ = sentence with extracted verb */
GoalPros = p(_,X,YZ),
ExtrForm = dr(0,D,dr(0,C,dia(I,box(I,dl(0,A,B))))),
rule_conclusion(Proof1, X, ExtrForm, _),
/* Pros = (prosody of) argument A */
find_e_start(Proof2, ef_start_iv, X, ExtrForm, dl(0,A,B), N0, Pros, Proof3),
global_replace_pros(Proof3, Pros, p(0, Pros, '$VAR'(N0)), N0, Proof4),
N is N0 + 1,
!.
transform_proof(rule(e_end, GoalPros, D-Sem, [Proof1, Proof2]), N0, N,
rule(dr, GoalPros, D-Sem,
[Proof1,
rule(drdiaboxi(I,N0), YZ, dr(0,C,dia(I,box(I,B)))-true, [Proof4])
])) :-
GoalPros = p(_,X,YZ),
ExtrForm = dr(0,D,dr(0,C,dia(I,box(I,B)))),
rule_conclusion(Proof1, X, ExtrForm, _),
find_e_start(Proof2, e_start, X, ExtrForm, B, N0, Pros, Proof3),
global_replace_pros(Proof3, Pros, p(0,Pros,'$VAR'(N0)), N0, Proof4),
N is N0 + 1,
!.
transform_proof(rule(e_endd, GoalPros, dl(I0,E,D)-Sem, [Proof1,Proof2]), N0, N,
rule(dli1(I,N1), GoalPros, dl(I,E,D)-Sem,
[rule(dr, p(II,X,p(1,'$VAR'(N1),YZ)), D-Sem,
[Proof1,
rule(drdiaboxi(J,N0), p(1,'$VAR'(N1),YZ), dr(0,C,dia(J,box(J,B)))-true,
[rule(dl, p(1,'$VAR'(N1),YZ1), C-appl(Sem1,Var),
[rule(hyp(N1), '$VAR'(N1), E-Var, []),
Proof4
])])])])) :-
N1 is N0 + 1,
N is N1 + 1,
GoalPros = p(II,X,YZ),
ExtrForm = dr(0,D,dr(0,C,dia(J,box(J,B)))),
rule_conclusion(Proof1, X, ExtrForm, _),
rule_conclusion(Proof2, YZ, dl(I0,E,C), Sem1),
quote_mode(I0, I),
find_e_start(Proof2, e_start, X, ExtrForm, B, N0, Pros, Proof3),
global_replace_pros(Proof3, Pros, p(0,Pros,'$VAR'(N0)), N0, Proof4),
rule_conclusion(Proof4, YZ1, _, _),
!.
transform_proof(rule(e_end_l, GoalPros, D-Sem, [Proof1, Proof2]), N0, N,
rule(dl, GoalPros, D-Sem,
[rule(dldiaboxi(I,N0), XY, dr(0,C,dia(I,box(I,B)))-true, [Proof4]),
Proof2])) :-
GoalPros = p(_,XY,Z),
ExtrForm = dl(0,dr(0,C,dia(I,box(I,B))),D),
rule_conclusion(Proof2, Z, ExtrForm, _),
find_e_start(Proof1, e_start_l, Z, ExtrForm, B, N0, Pros, Proof3),
global_replace_pros(Proof3, Pros, p(0,Pros,'$VAR'(N0)), N0, Proof4),
N is N0 + 1,
!.
transform_proof(rule(gap_e, GoalPros, dr(0,X,Y)-Sem, [Proof1, Proof2]), N0, N,
rule(drdiaboxi(0,N0), GoalPros, dr(0,X,Y)-Sem,
[Proof4])) :-
ExtrForm = dl(0,dr(0,_,dia(I,box(I,dr(0,X,Y)))),_),
rule_conclusion(Proof2, Z, ExtrForm, _),
find_e_start(Proof1, gap_c, Z, ExtrForm, Y, N0, Pros, Proof3),
global_replace_pros(Proof3, Pros, p(0,Pros,'$VAR'(N0)), N0, Proof4),
N is N0 +1,
!.
transform_proof(rule(wpop_vp, GoalPros, _-Sem, [Proof1]), N0, N, ProofC) :-
(
Sem = lambda(X,appl(SemADV,appl(_SemVP,X0))),
X0 == X
;
Sem = lambda(CL,lambda(X,appl(SemADV,appl(appl(_SemVP,CL0),X0)))),
X0 == X,
CL0 == CL
),
find_w_start(Proof1, LPros, RPros, _AdvF, SemADV, ProofB, Proof2),
global_replace_pros(Proof2, p(1,LPros,RPros), LPros, ProofA),
merge_proofs(ProofA, ProofB, Wrap, Wrap, GoalPros, N0, N, ProofC),
!.
transform_proof(rule(wpop_vp, GoalPros, dl(0,CL,dl(0,NP,S))-Sem, [Proof1]), N0, N,
rule(dli(N3), GoalPros, dl(0,CL,dl(0,NP,S))-Sem,
[rule(dli(N2), p(0,'$VAR'(N3),GoalPros), dl(0,NP,S)-true,
[rule(prod_e(NB), p(0,'$VAR'(N2),p(0,'$VAR'(N3),GoalPros)), S-true,
[ProofP,
rule(dl1, p(0,'$VAR'(N2),p(0,'$VAR'(N3), GPP)), S-true,
[rule(dl, p(0,'$VAR'(N2), p(0,'$VAR'(N3), GPB)), S-true,
[rule(hyp(N2), '$VAR'(N2), NP-'$VAR'(VB), []),
rule(dl, p(0,'$VAR'(N3), GPB), dl(0,NP,S)-true,
[rule(hyp(N3), '$VAR'(N3), CL-'$VAR'(V2),[]),
Proof3])]),
rule(hyp(N0), '$VAR'(NA), dl(1,S,S)-'$VAR'(VA), [])])])])])) :-
/* VP with clitic */
Sem = lambda(_CL,lambda(_X,appl(Adv0,_))),
(
Adv0 = pi1(SemAdv),NA=N0,NB=N1,VA=V0,VB=V1
;
Adv0 = pi2(SemAdv),NA=N1,NB=N0,VA=V1,VB=V0
),
get_fresh_variable_number(Sem, V0),
V1 is V0 + 1,
V2 is V1 + 1,
N1 is N0 + 1,
N2 is N1 + 1,
N3 is N2 + 1,
N is N2 + 1,
find_prod_w_start(Proof1, N0, NB, VB, SemAdv, PPros, ProofP, Proof2),
global_replace_pros(Proof2, PPros, '$VAR'(NB), Proof3),
replace_pros(GoalPros, PPros, '$VAR'(NB), GPB),
replace_pros(GoalPros, PPros, p(0,'$VAR'(N0),'$VAR'(N1)), GPP),
!.
transform_proof(rule(wpop_vp, GoalPros, dl(0,NP,S)-Sem, [Proof1]), N0, N,
rule(dli(N2), GoalPros, dl(0,NP,S)-Sem,
[rule(prod_e(NB), p(0,'$VAR'(N2),GoalPros), S-true,
[ProofP,
rule(dl1, p(0,'$VAR'(N2), GPP), S-true,
[rule(dl, p(0,'$VAR'(N2), GPB), S-true,
[rule(hyp(N2), '$VAR'(N2), NP-'$VAR'(VB), []),
Proof3]),
rule(hyp(N0), '$VAR'(NA), dl(1,S,S)-'$VAR'(VA), [])])])])) :-
/* VP-scope adverb */
Sem = lambda(X,appl(Adv0,appl(_SemVP,X))),
(
Adv0 = pi1(SemAdv),NA=N0,NB=N1,VA=V0,VB=V1
;
Adv0 = pi2(SemAdv),NA=N1,NB=N0,VA=V1,VB=V0
),
get_fresh_variable_number(Sem, V0),
V1 is V0 + 1,
N1 is N0 + 1,
N2 is N1 + 1,
N is N2 + 1,
find_prod_w_start(Proof1, N0, NB, VB, SemAdv, PPros, ProofP, Proof2),
global_replace_pros(Proof2, PPros, '$VAR'(NB), Proof3),
replace_pros(GoalPros, PPros, '$VAR'(NB), GPB),
replace_pros(GoalPros, PPros, p(0,'$VAR'(N0),'$VAR'(N1)), GPP),
!.
transform_proof(rule(wpop, GoalPros, S-Sem, [Proof1]), N0, N,
rule(prod_e(NB), GoalPros, S-Sem,
[ProofP,
rule(dl1, GPP, S-true,
[Proof3,
rule(hyp(N0), '$VAR'(NA), dl(1,S,S)-'$VAR'(VA), [])])])) :-
/* sentence-scope adverb */
Sem = appl(Adv0,_Sem),
(
Adv0 = pi1(SemAdv),NA=N0,NB=N1,VA=V0,VB=V1
;
Adv0 = pi2(SemAdv),NA=N1,NB=N0,VA=V1,VB=V0
),
get_fresh_variable_number(Sem, V0),
V1 is V0 + 1,
N1 is N0 + 1,
N2 is N1 + 1,
N is N2 + 1,
find_prod_w_start(Proof1, N0, NB, VB, SemAdv, PPros, ProofP, Proof2),
global_replace_pros(Proof2, PPros, '$VAR'(NB), Proof3),
replace_pros(GoalPros, PPros, p(0,'$VAR'(N0),'$VAR'(N1)), GPP),
!.
transform_proof(rule(wpop_vpi, GoalPros, _, [ProofA,ProofB]), N0, N, ProofC) :-
merge_proofs_left(ProofA, ProofB, Wrap, Wrap, GoalPros, N0, N, ProofC),
!.
transform_proof(rule(wpop, GoalPros, _-Sem, [Proof1]), N0, N, ProofC) :-
Sem = appl(SemADV, _),
find_w_start(Proof1, LPros, RPros, _AdvF, SemADV, ProofB, Proof2),
global_replace_pros(Proof2, p(1,LPros,RPros), LPros, ProofA),
merge_proofs(ProofA, ProofB, Wrap, Wrap, GoalPros, N0, N, ProofC),
!.
% = simplify dit_np/se_dit/a_dit combinations
transform_proof(rule(dit_np, p(0,p(0,P,p(0,Q,R)),P1), dl(I0,lit(s(ST)),lit(s(ST)))-Sem,
[rule(se_dit, p(0,P,p(0,Q,R)), dl(I0,lit(s(ST)),_)-_,
[ProofClr,
rule(a_dit_se, p(0,Q,R), dl(I0,lit(s(ST)),Res)-_,
[ProofAux,
ProofPPart])]),
ProofNP]),
N0, N,
rule(dli1(I,N0), p(0,p(0,P,p(0,Q,R)),P1), dl(I,lit(s(ST)),lit(s(ST)))-Sem,
[rule(dr, p(0,p(0,P,p(0,Q,p(I,'$VAR'(N0),R))),P1), lit(s(ST))-true,
[rule(dl, p(0,P,p(0,Q,p(I,'$VAR'(N0),R))), dr(0,lit(s(ST)),lit(np(_,_,_)))-true,
[ProofClr,
rule(dr, p(0,Q,p(I,'$VAR'(N0),R)), Res-true,
[ProofAux,
rule(dl, p(I,'$VAR'(N0),R), PPart-appl(_,Z),
[rule(hyp(N0), '$VAR'(N0), lit(s(ST))-Z, []),
ProofPPart])])
]),
ProofNP])])) :-
!,
N is N0 + 1,
quote_mode(I0, I),
ProofAux = rule(_, _, dr(0,Res,PPart)-_, _).
transform_proof(rule(dit_np, p(0,p(0,P,p(0,Q,R)),P1), dl(I0,lit(s(ST)),lit(s(ST)))-Sem,
[rule(se_dit, p(0,P,p(0,Q,R)), dl(I0,lit(s(ST)),_)-_,
[ProofClr,
rule(a_dit, p(0,Q,R), dl(I0,lit(s(ST)),Res)-_,
[ProofAux,
ProofPPart])]),
ProofNP]),
N0, N,
rule(dli1(I,N0), p(0,p(0,P,p(0,Q,R)),P1), dl(I,lit(s(ST)),lit(s(ST)))-Sem,
[rule(dr, p(0,p(0,P,p(0,Q,p(I,'$VAR'(N0),R))),P1), lit(s(ST))-true,
[rule(dl, p(0,P,p(0,Q,p(I,'$VAR'(N0),R))), dr(0,lit(s(ST)),lit(np(_,_,_)))-true,
[ProofClr,
rule(dr, p(0,Q,p(I,'$VAR'(N0),R)), Res-true,
[ProofAux,
rule(dl, p(I,'$VAR'(N0),R), PPart-appl(_,Z),
[rule(hyp(N0), '$VAR'(N0), lit(s(ST))-Z, []),
ProofPPart])])
]),
ProofNP])])) :-
!,
N is N0 + 1,
quote_mode(I0, I),
ProofAux = rule(_, _, dr(0,Res,PPart)-_, _).
%Sem2 = appl(lambda(Z,appl(_X,appl(Y,Z))),_V),
% Sem1 = appl(Sem2,W),
% Sem = lambda(W,Sem1).
% = simplify dit_np/a_dit combinations
transform_proof(rule(dit_np, p(0,p(0,P,Q),R), dl(I0,lit(s(ST)),lit(s(ST)))-Sem,
[rule(a_dit, p(0,P,Q), dl(I0,lit(s(ST)),dr(0,lit(s(ST)),lit(np(A,B,C))))-_, [ProofAux,ProofPPart]), ProofNP]),
N0, N,
rule(dli1(I,N0), p(0,p(0,P,Q),R), dl(I,lit(s(ST)),lit(s(ST)))-Sem,
[rule(dr, p(0,p(0,P,p(I,'$VAR'(N0),Q)),R), lit(s(ST))-Sem1,
[rule(dr, p(0,P,p(I,'$VAR'(N0),Q)), dr(0,lit(s(ST)),lit(np(A,B,C)))-Sem2,
[ProofAux,
rule(dl, p(I,'$VAR'(N0),Q), PPart-appl(Y,Z),
[rule(hyp(N0), '$VAR'(N0), lit(s(ST))-Z, []),
ProofPPart])]),
ProofNP])])) :-
!,
N is N0 + 1,
quote_mode(I0, I),
ProofAux = rule(_, _, dr(0,_,PPart)-_, _),
Sem2 = appl(lambda(Z,appl(_X,appl(Y,Z))),_V),
Sem1 = appl(Sem2,W),
unify_semantics(Sem,lambda(W,Sem1)).
transform_proof(rule(a_dit, p(0,ProsL,ProsR), dl(I0,Y,X)-Sem, [Left,Right]), N0, N,
rule(dli1(I,N0), p(0,ProsL,ProsR), dl(I,Y,X)-Sem,
[rule(dr, p(0,ProsL,p(I,'$VAR'(N0),ProsR)), X-appl(Sem1,appl(Sem2,S)),
[Left,
rule(dl, p(I,'$VAR'(N0),ProsR), PPart-appl(Sem2,S),
[rule(hyp(N0), '$VAR'(N0), Y-S, []),
Right])])])) :-
!,
N is N0 + 1,
quote_mode(I0, I),
Right = rule(_, _, dl(1,Y,PPart)-_, _),
Sem = lambda(S, appl(Sem1,appl(Sem2,S))).
transform_proof(rule(a_dit_se, p(0,ProsL,ProsR), dl(I0,Y,X)-Sem, [Left,Right]), N0, N,
rule(dli1(I,N0), p(0,ProsL,ProsR), dl(I,Y,X)-Sem,
[rule(dr, p(0,ProsL,p(I,'$VAR'(N0),ProsR)), X-appl(Sem1,appl(Sem2,S)),
[Left,
rule(dl, p(I,'$VAR'(N0),ProsR), PPart-appl(Sem2,S),
[rule(hyp(N0), '$VAR'(N0), Y-S, []),
Right])])])) :-
!,
N is N0 + 1,
quote_mode(I0, I),
Right = rule(_, _, dl(1,Y,PPart)-_, _),
Sem = lambda(S, appl(Sem1,appl(Sem2,S))).
transform_proof(rule(dit_np, p(0,ProsL,ProsR), dl(I0,Y,X)-Sem, [Left,Right]), N0, N,
rule(dli1(I,N0), p(0,ProsL,ProsR), dl(I,Y,X)-Sem,
[rule(dr, p(0,p(1,'$VAR'(N0),ProsL), ProsR), X-Sem1,
[rule(dl, p(1,'$VAR'(N0),ProsL), dr(0,X,lit(np(A,B,C)))-appl(PrtSem,S),
[rule(hyp(N0), '$VAR'(N0), Y-S, []),
Left]),
Right])])) :-
!,
N is N0 + 1,
quote_mode(I0, I),
Right = rule(_, _, lit(np(A,B,C))-_, _),
Sem1 = appl(appl(PrtSem, S), _),
Sem = lambda(S, Sem1).
transform_proof(rule(se_dit, p(0,ProsL,ProsR), dl(I0,Y,X)-Sem, [Left,Right]), N0, N,
rule(dli1(I,N0), p(0,ProsL,ProsR), dl(I,Y,X)-Sem,
[rule(dl, p(0,ProsL,p(1,'$VAR'(N0),ProsR)), X-Sem1,
[Left,
rule(dl, p(1,'$VAR'(N0),ProsR), dl(0,lit(cl_r),X)-appl(PrtSem,S),
[rule(hyp(N0), '$VAR'(N0), Y-S, []),
Right])])])) :-
!,
N is N0 + 1,
quote_mode(I0, I),
Left = rule(_, _, lit(cl_r)-_, _),
Sem1 = appl(appl(PrtSem, S), _),
Sem = lambda(S, Sem1).
transform_proof(rule(e_end_l_lnr, Pros1, F1-Sem1, [LeftProofs, rule(e_end_r_lnr, Pros2, F2-Sem2, [AndProof,RightProofs])]),
N0, N,
rule(dl, Pros1, F1-Sem1, [Left, rule(dr, Pros2, F2-Sem2, [AndProof, Right])])) :-
!,
collect_left_proofs(LeftProofs, N0, N1, Left),
collect_right_proofs(RightProofs, N1, N, Right).
transform_proof(rule(e_end_l_lnr, Pros1, F1-Sem1, [LeftProofs, AndProof]),
N0, N,
rule(dl, Pros1, F1-Sem1, [Left, AndProof])) :-
!,
collect_left_proofs(LeftProofs, N0, N, Left).
% product rules
transform_proof(rule(prod_i, p(0,Pros1,Pros2), p(0,A,B)-Sem, [Left,Mid,Right]), N, N,
rule(prod_i, p(0,Pros1,Pros2), p(0,A,B)-Sem, [Proof1,Proof2])) :-
/* remove auxiliary hypothesis (of the form C/(A*B) or (A*B)\C) */
!,
(
Left = rule(_, Pros1, A-_, _),
Mid = rule(_, Pros2, B-_, _)
->
Proof1 = Left,
Proof2 = Mid
;
Mid = rule(_, Pros1, A-_, _),
Right = rule(_, Pros2, B-_, _)
->
Proof1 = Mid,
Proof2 = Right
).
transform_proof(rule(prod_i3, p(0,p(0,Pros1,Pros2),Pros3), p(0,p(0,A,B),C)-Sem, [Left,Mid1,Mid2,Right]), N, N,
rule(prod_i, p(0,p(0,Pros1,Pros2),Pros3), p(0,p(0,A,B),C)-Sem,
[rule(prod_i, p(0,Pros1,Pros2), p(0,A,B)-true, [Proof1,Proof2]),
Proof3])) :-
/* remove auxiliary hypothesis (of the form C/(A*B) or (A*B)\C) */
select(rule(NmA, Pros1, A-SA, PrmsA), [Left,Mid1,Mid2,Right], Rest0),
select(rule(NmB, Pros2, B-SB, PrmsB), Rest0, Rest1),
member(rule(NmC, Pros3, C-SC, PrmsC), Rest1),
!,
Proof1 = rule(NmA, Pros1, A-SA, PrmsA),
Proof2 = rule(NmB, Pros2, B-SB, PrmsB),
Proof3 = rule(NmC, Pros3, C-SC, PrmsC).
transform_proof(rule(prod_e, Pros, FS,
[rule(prod_c, _, _, [Proof1, Proof2])]),
N0, N,
rule(prod_e(N0), Pros, FS,
[PProof,
rule(dr, p(0,p(0,Pros1,'$VAR'(N0)),'$VAR'(N1)), A-appl(appl(Sem1,'$VAR'(V0)),'$VAR'(V1)),
[rule(dr, p(0,Pros1,'$VAR'(N0)), dr(0,A,C)-appl(Sem1,'$VAR'(V0)),
[Proof1,
AProof]),
rule(hyp(N0), '$VAR'(N1), C-'$VAR'(V1), [])
])
])) :-
Proof1 = rule(_, Pros1, dr(0,dr(0,A,C),B)-Sem1, _),
Proof2 = rule(_, _, p(0,B,dia(0,box(0,C)))-Sem2, _),
/* obtain two variables which as fresh wrt Sem1 and Sem2 */
get_fresh_variable_number(appl(Sem1,Sem2), V0),
V1 is V0 + 1,
N1 is N0 + 1,
N is N1 + 1,
prod_root(Proof2, p(0,B,dia(0,box(0,C))), PProof, rule(hyp(N0),'$VAR'(N0), B-'$VAR'(V0), []), AProof),
!.
transform_proof(rule(prod_dr, Pros, FS, Proofs), N, N, rule(dr, Pros, FS, Proofs)) :-
!.
transform_proof(rule(Nm, Pros, F, Ds0), N0, N, rule(Nm, Pros, F, Ds)) :-
is_list(Ds0),
!,
transform_proof_list(Ds0, N0, N, Ds).
transform_proof(Strange, _, _, null) :-
(
var(Strange)
->
format(user_error, '~N{Error: free variable used for proof!}~n', [])
;
functor(Strange, F, A),
format(user_error, '{Error: strange proof term with functor ~w/~w: ~w}', [F,A,Strange])
),
fail.
transform_proof_list([], N, N, []).
transform_proof_list([P|Ps], N0, N, [Q|Qs]) :-
transform_proof(P, N0, N1, Q),
transform_proof_list(Ps, N1, N, Qs).
% = product introduction rules
prod_root(rule(prod_cl, _, _, [Proof1, Proof2]), p(0,A,dia(0,box(0,C))),
PProof, rule(Nm, HPros, A-V, []), rule(dl, p(0,Pros1,Pros2), B-appl(Y,X), [Proof1,Result])) :-
!,
Proof1 = rule(_, Pros1, A-X, _),
Proof2 = rule(_, _, p(0,dl(0,A,B),dia(0,box(0,C)))-_, _),
prod_root(Proof2, p(0,B,dia(0,box(0,C))), PProof, rule(Nm, HPros, B-V, []), Result),
Result = rule(_, Pros2, _-Y, _).
prod_root(rule(prod_c, _, _, [Proof1, Proof2]), p(0,A,dia(0,box(0,C))),
PProof, rule(Nm, HPros, A-V, []), rule(dr, p(0,Pros1,Pros2), A-appl(X,Y), [Proof1,Result])) :-
!,
Proof1 = rule(_, Pros1, dr(0,A,B)-X, _),
Proof2 = rule(_, _, p(0,B,dia(0,box(0,C)))-_, _),
prod_root(Proof2, p(0,B,dia(0,box(0,C))), PProof, rule(Nm, HPros, B-V, []), Result),
Result = rule(_, Pros2, _-Y, _).
prod_root(PProof, _, PProof, Result, Result).
% left-node-raising constructions
collect_left_proofs(LeftProofs, N0, N, rule(dldiaboxi(0,N0), Pros, dl(0,dia(0,box(0,lit(n))),lit(n))-X, [Left])) :-
LeftProofs = rule(_, Pros, _-X, _),
list_left_proofs(LeftProofs, List, []),
N is N0 + 1,
StartL = rule(hyp(N0), '$VAR'(N0), lit(n)-_, []),
combine_lnr_proofs(List, StartL, Left).
collect_right_proofs(RightProofs, N0, N, rule(drdiaboxi(0,N0), Pros, dl(0,dia(0,box(0,lit(n))),lit(n))-X, [Left])) :-
RightProofs = rule(_, Pros, _-X, _),
list_right_proofs(RightProofs, List, []),
N is N0 +1,
StartR = rule(hyp(N0), '$VAR'(N0), lit(n)-_, []),
combine_lnr_proofs(List, StartR, Left).
list_left_proofs(rule(c_l_lnr, _, _, [L1, L2, _]), Rest0, Rest) :-
!,
list_left_proofs(L1, Rest0, Rest1),
list_left_proofs(L2, Rest1, Rest).
list_left_proofs(Proof, [Proof|Rest], Rest).
list_right_proofs(rule(c_r_lnr, _, _, [_, R1, R2]), Rest0, Rest) :-
!,
list_right_proofs(R1, Rest0, Rest1),
list_right_proofs(R2, Rest1, Rest).
list_right_proofs(Proof, [Proof|Rest], Rest).
combine_lnr_proofs([], Proof, Proof).
combine_lnr_proofs([L|Ls], Proof0, Proof) :-
L = rule(_, Pros2, _-X, _),
Proof0 = rule(_, Pros1, _-Y, _),
combine_lnr_proofs(Ls, rule(dl, p(0,Pros1,Pros2), lit(n)-appl(X,Y), [Proof0, L]), Proof).
%
merge_proofs_left(RuleA, RuleB, Wrap0, Wrap, GoalPros, N, N, rule(dl1, Wrap0, A-appl(P,M), [RuleB, RuleA])) :-
/* REMARK: this instance of the \_1 rule is not necessarily a right daughter */
/* If it is important to distinguish this case, change the rule name above from "dl1" to something else */
RuleA = rule(_, _, dl(1,B,A)-P, _),
RuleB = rule(_, _, B-M, _),
!,
Wrap = GoalPros.
merge_proofs_left(RuleA, RuleB, Pros0, p(0,Pros,'$VAR'(N0)), GoalPros, N0, N, rule(dri(N0), ProsA, dr(I,A,B)-lambda(X,M), [Rule])) :-
RuleB = rule(_, ProsB, dr(I,A,B)-SemAB, _),
!,
N1 is N0 + 1,
Hyp = rule(hyp(N0), '$VAR'(N0), B-X, []),
Rule = rule(_, p(_, ProsA, _), A-M, _),
merge_proofs_left(RuleA, rule(dr, p(I,ProsB,'$VAR'(N0)), A-appl(SemAB,X), [RuleA, Hyp]), Pros0, Pros, GoalPros, N1, N, Rule).
merge_proofs_left(RuleA, RuleB, Pros0, p(0,'$VAR'(N0),Pros), GoalPros, N0, N, rule(dli(N0), ProsA, dl(I,B,A)-lambda(X,M), [Rule])) :-
RuleB = rule(_, ProsB, dl(I,B,A)-SemBA, _),
!,
N1 is N0 + 1,
Hyp = rule(hyp(N0), '$VAR'(N0), B-X, []),
Rule = rule(_, p(_, _, ProsA), A-M, _),
merge_proofs_left(RuleA, rule(dl, p(I,'$VAR'(N0),ProsB), A-appl(SemBA,X), [Hyp, RuleB]), Pros0, Pros, GoalPros, N1, N, Rule).
merge_proofs(RuleA, RuleB, Wrap0, Wrap, GoalPros, N, N, rule(dl1, Wrap0, A-appl(P,M), [RuleA, RuleB])) :-
RuleA = rule(_, _ProsA, B-M, _),
RuleB = rule(_, _ProsB, dl(1,B,A)-P, _),
!,
Wrap = GoalPros.
merge_proofs(RuleA, RuleB, Pros0, p(0,Pros,'$VAR'(N0)), GoalPros, N0, N, rule(dri(N0), ProsB, dr(I,A,B)-lambda(X,M), [Rule])) :-
RuleA = rule(_, ProsA, dr(I,A,B)-SemAB, _),
!,
N1 is N0 + 1,
Hyp = rule(hyp(N0), '$VAR'(N0), B-X, []),
Rule = rule(_, p(_, ProsB, _), A-M, _),
merge_proofs(rule(dr, p(I,ProsA,'$VAR'(N0)), A-appl(SemAB,X), [RuleA, Hyp]), RuleB, Pros0, Pros, GoalPros, N1, N, Rule).
merge_proofs(RuleA, RuleB, Pros0, p(0,'$VAR'(N0),Pros), GoalPros, N0, N, rule(dli(N0), ProsB, dl(I,B,A)-lambda(X,M), [Rule])) :-
RuleA = rule(_, ProsA, dl(I,B,A)-SemBA, _),
!,
N1 is N0 + 1,
Hyp = rule(hyp(N0), '$VAR'(N0), B-X, []),
Rule = rule(_, p(_, _, ProsB), A-M, _),
merge_proofs(rule(dl, p(I,'$VAR'(N0),ProsA), A-appl(SemBA,X), [Hyp, RuleA]), RuleB, Pros0, Pros, GoalPros, N1, N, Rule).
match_pros(X, X) :-
!.
match_pros(p(0,X,'$VAR'(_)), Pros) :-
!,
match_pros(X, Pros).
match_pros(p(0,'$VAR'(_),X), Pros) :-
!,
match_pros(X, Pros).
match_pros_i(X, X) :-
!.
match_pros_i(p(0,I,X), Y) :-
match_interpunction_pros(I),
!,
match_pros_i(X, Y).
match_interpunction_pros(I) :-
interpunction_pros(I),
!.
match_interpunction_pros(p(0,I0,I1)) :-
match_interpunction_pros(I0),
match_interpunction_pros(I1).
interpunction_pros(',').
interpunction_pros('"').
interpunction_pros(':').
interpunction_pros('(').
interpunction_pros(')').
interpunction_pros('-').
interpunction_pros(';').
% find_prod_w_start(Proof1, NB, VB, Adv0, PPros, ProofP, Proof2),
find_prod_w_start(rule(prod_wl, Pros, _, [Prem]),
N0, NB, VB, Adv, Pros, Prem,
rule(hyp(N0), '$VAR'(NB), Y-'$VAR'(VB), [])) :-
Prem = rule(_, _, p(0,dl(1,_,_),dia(0,box(0,Y)))-Sem, _),
Sem =@= Adv,
!.
find_prod_w_start(rule(prod_w, Pros, _, [Prem]),
N0, NB, VB, Adv, Pros, Prem,
rule(hyp(N0), '$VAR'(NB), Y-'$VAR'(VB), [])) :-
Prem = rule(_, _, p(0,Y,dl(1,_,_))-Sem, _),
Sem =@= Adv,
!.
find_prod_w_start(rule(Nm, Pros, F, Rs0), N0, NB, VB, Adv, PPros, ProofP, rule(Nm, Pros, F, Rs)) :-
find_prod_w_start_list(Rs0, N0, NB, VB, Adv, PPros, ProofP, Rs).
find_prod_w_start_list([P0|Ps], N0, NB, VB, Adv, PPros, ProofP, [P|Ps]) :-
find_prod_w_start(P0, N0, NB, VB, Adv, PPros, ProofP, P).
find_prod_w_start_list([P|Ps0], N0, NB, VB, Adv, PPros, ProofP, [P|Ps]) :-
find_prod_w_start_list(Ps0, N0, NB, VB, Adv, PPros, ProofP, Ps).
%
find_w_start(rule(wr,RPros,_,[LProof,RProof]), Left, Pros, AdvF, Sem, RProof, LProof) :-
match_pros(RPros, p(1,Left,Pros)),
RProof = rule(_, Pros, AdvF-Sem0, _),
equivalent_semantics(Sem0, Sem),
!.
find_w_start(rule(wr_a,RPros,_,[LProof,RProof]), Left, Pros, AdvF, Sem, RProof, LProof) :-
match_pros(RPros, p(1,Left,Pros)),
RProof = rule(_, Pros, AdvF-Sem0, _),
equivalent_semantics(Sem0, Sem),
!.
find_w_start(rule(Nm, P, A, Ds0), Left, Pros, AdvF, Sem, AdvProof, rule(Nm, P, A, Ds)) :-
find_w_start_list(Ds0, Left, Pros, AdvF, Sem, AdvProof, Ds),
!.
find_w_start_list([P0|Ps], Left, Pros, AdvF, Sem, AdvProof, [P|Ps]) :-
find_w_start(P0, Left, Pros, AdvF, Sem, AdvProof, P).
find_w_start_list([P|Ps0], Left, Pros, AdvF, Sem, AdvProof, [P|Ps]) :-
find_w_start_list(Ps0, Left, Pros, AdvF, Sem, AdvProof, Ps).
find_e_start(rule(gap_c, Pros, A-Sem, [Proof,rule(_, Y, EF-_,_)]),
gap_c, X, EF, B, N, Pros,
rule(dr, Pros, A-Sem, [Proof,rule(hyp(N),'$VAR'(N),B-Var0,[])])) :-
Sem = appl(_,Var0),
match_pros_i(X, Y),
!.
find_e_start(rule(ef_start, Pros, A-Sem, [rule(_, Y, EF-_, _), Proof]),
ef_start, X, EF, dr(0,A,B), N, Pros,
rule(dr, Pros, A-Sem, [rule(hyp(N),'$VAR'(N),dr(0,A,B)-Var0,[]),Proof])) :-
Sem = appl(Var0, _),
match_pros_i(X, Y),
!.
find_e_start(rule(ef_start_iv, Pros, B-Sem, [rule(_, Y, EF-_, _), Proof]),
ef_start_iv, X, EF, dl(0,A,B), N, Pros,
rule(dl, Pros, A-Sem, [Proof,rule(hyp(N),'$VAR'(N),dl(0,A,B)-Var0,[])])) :-
Sem = appl(Var0, _),
match_pros_i(X, Y),
!.
find_e_start(rule(e_start, Pros, A-Sem, [rule(_, Y, EF-_, _), Proof]),
e_start, X, EF, B, N, Pros,
rule(dr, Pros, A-Sem, [Proof,rule(hyp(N),'$VAR'(N),B-Var0,[])])) :-
Sem = appl(_, Var0),
match_pros_i(X, Y),
!.
find_e_start(rule(e_start_l, Pros, A-Sem, [Proof,rule(_, Y, EF-_, _)]),
e_start_l, X, EF, B, N, Pros,
rule(dr, Pros, A-Sem, [Proof,rule(hyp(N),'$VAR'(N),B-Var0,[])])) :-
Sem = appl(_, Var0),
match_pros_i(X, Y),
% format(user_error, '~N!!! e_start_l !!!~n', [TermC]),
!.
find_e_start(rule(Nm, P, A, Ds0),
StartName, X, EF, B, N, Pros,
rule(Nm, P, A, Ds)) :-
% Term = find_e_start(rule(Nm, P, A, Ds0),StartName, X, EF, B, N, Pros, _),
% copy_term(Term, TermC),
% numbervars(TermC, 0, _),
% TermC = Term,
rule_premisses(Nm, Ds0, Ds1, Ds2, Ds),
find_e_start_list(Ds1, StartName, X, EF, B, N, Pros, Ds2),
!.
find_e_start_list([P0|Ps], StartName, X, EF, B, N, Pros, [P|Ps]) :-
find_e_start(P0, StartName, X, EF, B, N, Pros, P).
find_e_start_list([P|Ps0], StartName, X, EF, B, N, Pros, [P|Ps]) :-
find_e_start_list(Ps0, StartName, X, EF, B, N, Pros, Ps).
%! rule_premisses(+RuleName, +PremissesIn, -AccessiblePremissesIn, -AccessiblePremissesOut, -PremissesOut)
%
%
rule_premisses(e_start_l, [P1,P2], [P1], [P3], [P3,P2]) :-
!.
rule_premisses(e_start, [P1,P2], [P2], [P3], [P1,P3]) :-
!.
rule_premisses(_, Ds, Ds, Es, Es).
rule_conclusion(rule(_, A, F-S, _), A, F, S).
rule_daughters(rule(_, _, _, Ds), Ds).
% = replace_proof(+InProof, +SubProof1, +SubProof2, -OutProof)
%
% true if OutProof is a copy of InProof where all occurrences of SubProof1 have been
% replace by SubProof2
replace_proof(ProofA, ProofA, ProofB, ProofB) :-
!.
replace_proof(rule(Nm, P, F, Ds0), ProofA, ProofB, rule(Nm, P, F, Ds)) :-
replace_proof_list(Ds0, ProofA, ProofB, Ds).
replace_proof_list([], _, _, []).
replace_proof_list([P0|Ps0], ProofA, ProofB, [P|Ps]) :-
replace_proof(P0, ProofA, ProofB, P),
replace_proof_list(Ps0, ProofA, ProofB, Ps).
% =
% = special case to prevent accidental capture of hypotheses
replace_proof_bag(rule(gap_e, Pros0, X-Sem, [A,B0]), Bag, Var, Proof, rule(gap_e, Pros, X-Sem, [A,B])) :-
!,
replace_bag(Pros0, Pros, Bag, Var),
replace_proof_bag(B0, Bag, Var, Proof, B).
replace_proof_bag(rule(Nm0, Pros0, X-Sem, Rs0), Bag, Var, Proof, Result) :-
bag_of_words(Pros0, Bag0),
(
Bag0 = Bag
->
Result = Proof
;
replace_bag(Pros0, Pros, Bag, Var),
Result = rule(Nm, Pros, X-Sem, Rs),
replace_proof_bag_list(Rs0, Bag, Var, Proof, Rs1),
/* collapse superfluous unary branches */
( Rs1 = [rule(Nm, Pros, _, Rs)] -> true ; Rs = Rs1, Nm = Nm0)
).
replace_proof_bag_list([], _, _, _, []).
replace_proof_bag_list([A|As], Bag, Var, Proof, Results) :-
replace_proof_bag_list(As, A, Bag, Var, Proof, Results).
replace_proof_bag_list([], A0, Bag, Var, Proof, [A]) :-
replace_proof_bag(A0, Bag, Var, Proof, A).
replace_proof_bag_list([B0], A0, Bag0, Var, Proof, Result) :-
A0 = rule(_, ProsA, _, _),
B0 = rule(_, ProsB, _, _),
bag_of_words(ProsA, BagA),
bag_of_words(ProsB, BagB),
(
/* the conclusion of the left subproof contains only words from the extracted element */
ord_subset(BagA, Bag0),
BagA \= Bag0
->
/* forget left subproof and reduce bag */
ord_subtract(Bag0, BagA, Bag),
Result = [B],
replace_proof_bag(B0, Bag, Var, Proof, B)
;
ord_subset(BagB, Bag0),
BagB \= Bag0
->
ord_subtract(Bag0, BagB, Bag),
Result = [A],
replace_proof_bag(A0, Bag, Var, Proof, A)
;
ord_subset(Bag0, BagA)
->
B = B0,
Result = [A,B],
replace_proof_bag(A0, Bag0, Var, Proof, A)
;
ord_subset(Bag0, BagB)
->
A = A0,
Result = [A,B],
replace_proof_bag(B0, Bag0, Var, Proof, B)
).
% = global_replace_pros(+InProof, +Pros1, +Pros2, -OutProof)
%
% true if OutProof is a copy of InProof where all occurrences of Pros1 have been
% replace by Pros2
global_replace_pros(rule(Nm, P0, F, Ds0), A, B, rule(Nm, P, F, Ds)) :-
replace_pros(P0, A, B, P),
global_replace_pros_list(Ds0, A, B, Ds).
global_replace_pros_list([], _, _, []).
global_replace_pros_list([P|Ps], A, B, [Q|Qs]) :-
global_replace_pros(P, A, B, Q),
global_replace_pros_list(Ps, A, B, Qs).
% = global_replace_pros(+InProof, +Pros1, +Pros2, +VarNo, -OutProof)
%
% true if OutProof is a copy of InProof where all occurrences of Pros1 have been
% replace by Pros2
%
% Unlike global_replace_pros/4, the replacement takes place only for those labels
% occurring in proof nodes which are parents of the hypothesis label '$VAR'(VarNo).
global_replace_pros(rule(Nm, P0, F, [rule(Nm1, '$VAR'(N), F1, Ds), Right]), A, B, N,
rule(Nm, P, F, [rule(Nm1, '$VAR'(N), F1, Ds), Right])) :-
/* we have arrived at the end */
!,
replace_pros(P0, A, B, P).
global_replace_pros(rule(Nm, P0, F, [Left, rule(Nm1, '$VAR'(N), F1, Ds)]), A, B, N,
rule(Nm, P, F, [Left, rule(Nm1, '$VAR'(N), F1, Ds)])) :-
/* we have arrived at the end */
!,
replace_pros(P0, A, B, P).
global_replace_pros(rule(Nm, P0, F, Ds0), A, B, N, rule(Nm, P, F, Ds)) :-
replace_pros(P0, A, B, P),
global_replace_pros_list(Ds0, A, B, N, Ds).
global_replace_pros_list([], _, _, _, []).
global_replace_pros_list([P|Ps], A, B, N, [Q|Qs]) :-
global_replace_pros(P, A, B, N, Q),
global_replace_pros_list(Ps, A, B, N, Qs).
replace_pros(A, A, B, B) :-
!.
replace_pros(p(I,A0,B0), C, D, p(I,A,B)) :-
!,
replace_pros(A0, C, D, A),
replace_pros(B0, C, D, B).
replace_pros(A, _, _, A).
%
replace_bag(Pros0, Pros, Bag, R) :-
replace_bag(Pros0, Pros1, Bag, [], R),
cleanup_pros(Pros1, Pros).
replace_bag(p(I,A0,B0), p(I,A,B), Bag0, Bag, R) :-
!,
replace_bag(A0, A, Bag0, Bag1, R),
replace_bag(B0, B, Bag1, Bag, R).
replace_bag(A, Result, Bag0, Bag, R) :-
ord_select(A, Bag0, Bag),
!,
(Bag = [] -> Result = R ; Result = '$EMPTY').
replace_bag(B, B, Bag, Bag, _R).
cleanup_pros(p(I,X0,Y0), Z) :-
!,
cleanup_pros(X0, X),
(
X == '$EMPTY'
->
cleanup_pros(Y0, Z)
;
cleanup_pros(Y0, Y),
(
Y == '$EMPTY'
->
Z = X
;
Z = p(I,X,Y)
)).
cleanup_pros(X, X).
bag_of_words(p(_,A,B), Bag) :-
!,
bag_of_words(A, Bag0),
bag_of_words(B, Bag1),
ord_dup_union(Bag0, Bag1, Bag).
bag_of_words('$VAR'(_), []) :-
!.
bag_of_words(X, [X]).
