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
check_proofs.pl
%:- compile(proofs).
:- use_module(ordset, [ord_insert/3,ord_union/3]).
nd_file(aa1_nd).
nd_file(aa2_nd).
nd_file(ab2_nd).
nd_file(ae1_nd).
nd_file(af2_nd).
nd_file(ag1_nd).
nd_file(ag2_nd).
nd_file(ah1_nd).
nd_file(ah2_nd).
nd_file(ai1_nd).
nd_file(ai2_nd).
nd_file(aj1_nd).
nd_file(ak1_nd).
nd_file(ak2_nd).
nd_file(al1_nd).
nd_file(am1_nd).
nd_file(am2_nd).
nd_file(an1_nd).
nd_file(an2_nd).
nd_file(ao1_nd).
nd_file(ao2_nd).
nd_file(ap1_nd).
nd_file(aq2_nd).
nd_file(as2_nd).
nd_file(at_nd).
nd_file('300_nd').
nd_file('8000_nd').
nd_file(annodis_nd).
nd_file(monde_a_nd).
nd_file(monde_b_nd).
check_proofs :-
findall(N, proof(N, _), ProofList),
check_proofs(ProofList, []).
check_proofs([], RNs0) :-
msort(RNs0, RNs1),
collapse_duplicates(RNs1, RNs),
print_list(RNs).
check_proofs([N|Ns], RNs0) :-
proof(N, Proof),
check_proof(Proof, RNs0, RNs1),
check_proofs(Ns, RNs1).
check_proof(rule(Nm, _, _, Rs), RNs0, RNs) :-
% ord_insert(RNs0, Nm, RNs1),
functor(Nm, F, _),
keep_strange(F, RNs0, RNs1),
% RNs1 = [F|RNs0],
check_proof_list(Rs, RNs1, RNs).
all_sentences :-
tell('sentences.txt'),
findall(F, nd_file(F), FileList),
all_sentences(FileList, 0, 0).
all_sentences([], Sents, Words) :-
told,
format(user_error, '~NDone!~nTOTAL: ~D sentences, ~D words~n', [Sents, Words]).
all_sentences([F|Fs], Sents0, Words0) :-
abolish(proof/2),
style_check(-singleton),
compile(F),
style_check(+singleton),
findall(N, proof(N, _), ProofList),
all_sentences(ProofList, Sents0, Sents, Words0, Words),
all_sentences(Fs, Sents, Words).
all_sentences([], Sents, Sents, Words, Words).
all_sentences([N|Ns], Sents0, Sents, Words0, Words) :-
Sents1 is Sents0 + 1,
proof(N, rule(_, Pros, _, _)),
write_pros(Pros, Words0, Words1),
nl,
all_sentences(Ns, Sents1, Sents, Words1, Words).
write_pros(p(_,A,B), W0, W) :-
!,
write_pros(A, W0, W1),
write_pros(B, W1, W).
write_pros(A, W0, W) :-
W is W0 + 1,
write(A),
write(' ').
all_strange_proofs :-
findall(F, nd_file(F), FileList),
all_strange_proofs(FileList, 0, 0).
all_strange_proofs([], Strange, Total) :-
Normal is Total - Strange,
NPct is (Normal/Total)*100,
SPct is (Strange/Total)*100,
format('~N**TOTAL**~nNormal : ~D (~w%)~nStrange: ~D (~w%)~nTotal : ~D~2n', [Normal,NPct,Strange,SPct,Total]).
all_strange_proofs([F|Fs], Strange0, Total0) :-
abolish(proof/2),
style_check(-singleton),
compile(F),
style_check(+singleton),
findall(N, proof(N, _), ProofList),
strange_proofs(ProofList, 0, ST, 0, TT, Ss, []),
Normal is TT - ST,
NPct is (Normal/TT)*100,
SPct is (ST/TT)*100,
Total is Total0 + TT,
Strange is Strange0 + ST,
format('~N**~w**~nNormal : ~D (~w%)~nStrange: ~D (~w%)~nTotal : ~D~2n', [F,Normal,NPct,ST,SPct,TT]),
print_list(Ss),
all_strange_proofs(Fs, Strange, Total).
strange_proofs :-
findall(N, proof(N, _), ProofList),
strange_proofs(ProofList, 0, ST, 0, TT, Ss, []),
Normal is TT - ST,
NPct is (Normal/TT)*100,
SPct is (ST/TT)*100,
format('~NNormal : ~D (~w%)~nStrange: ~D (~w%)~nTotal : ~D~2n', [Normal,NPct,ST,SPct,TT]),
print_list(Ss).
strange_proofs([], ST, ST, T, T) -->
[].
strange_proofs([P|Ps], ST0, ST, T0, T) -->
is_strange(P, ST0, ST1),
{T1 is T0 + 1},
strange_proofs(Ps, ST1, ST, T1, T).
is_strange(N, ST0, ST, L0, L) :-
proof(N, P),
check_proof(P, [], Ss0),
sort(Ss0, Ss),
(
Ss = []
->
L = L0,
ST = ST0
;
L0 = [N-Ss|L],
ST is ST0 + 1
).
keep_strange(axiom, Rs, Rs) :-
!.
keep_strange(let, Rs, Rs) :-
!.
keep_strange(hyp, Rs, Rs) :-
!.
keep_strange(dr, Rs, Rs) :-
!.
keep_strange(dl, Rs, Rs) :-
!.
keep_strange(dl1, Rs, Rs) :-
!.
keep_strange(dli, Rs, Rs) :-
!.
keep_strange(dli1, Rs, Rs) :-
!.
keep_strange(dri, Rs, Rs) :-
!.
keep_strange(drdiaboxi, Rs, Rs) :-
!.
keep_strange(dldiaboxi, Rs, Rs) :-
!.
keep_strange(prod_i, Rs, Rs) :-
!.
keep_strange(prod_e, Rs, Rs) :-
!.
keep_strange(F, Rs, [F|Rs]).
collapse_duplicates([], []).
collapse_duplicates([A|As], Bs) :-
collapse_duplicates(As, A, 1, Bs).
collapse_duplicates([], B, N, [B-N]).
collapse_duplicates([A|As], B, N0, Cs0) :-
(
A = B
->
N is N0 + 1,
collapse_duplicates(As, B, N, Cs0)
;
Cs0 = [B-N0|Cs],
collapse_duplicates(As, A, 1, Cs)
).
check_proof_list([], RNs, RNs).
check_proof_list([R|Rs], RNs0, RNs) :-
check_proof(R, RNs0, RNs1),
check_proof_list(Rs, RNs1, RNs).
print_list([]).
print_list([A|As]) :-
format('~p~n', [A]),
print_list(As).