1:- module(prooftree, [prooftree/2, checkproof/2, proof/2, proof_figure/2]). 2
3:- use_module(util(misc)). 4
5:- use_module(pac('expand-pac')). 6:- use_module(pac(op)). 7:- use_module(pac(basic)). 8
9term_expansion --> pac:expand_pac.
10
14
15proof --> region, prooftree, math.
16
17math --> latex_math( (generate_tex, platex, get_size,
18 dvipdfmx, cleaning_tmp_file,
19 latex_open_file(pdf), clear) ).
20
21proof_figure --> current(T0),
22 prooftree,
23 current(P),
24 math,
25 { comment_out_region(T0, T) },
26 peek([T,"\n", P]),
27 overwrite.
28
29proof_platex_region --> current(T0),
30 prooftree, current(P),
31 { comment_out_region(T0, T) },
32 peek([T,"\n", P]),
33 overwrite,
34 { elisp:send_off("(command-execute 'latex-region-interactive)") }.
35
--> split, maplist(comment_out), insert("\n").
37
(X, Y) :- append(`%`, _, X) -> Y = X ; append(`% `, X, Y).
39
43
45
46prooftree -->
47 paragraph,
48 maplist(split),
49 maplist(remove([])),
50 remove([]),
51 maplist(text2proof),
52 maplist(prooftree:gentex),
53 smash.
54
55checkproof --> paragraph, remove([]), maplist(oneproof_check),
56 cons(["**** Checking proof trees figure: \n"]), flatten.
57
58oneproof_check --> split,
59 maplist(kleene_star_greedy(`%`)),
60 reverse,
61 textpos,
62 prooftree_check.
63
64text2proof(P, Y):-maplist(kleene_star_greedy(`%`),P,P0),
65 reverse(P0, X),
66 textpos(X, X1),
67 X1=[[M]|L],
68 mkproof(M, Y, L).
69
70textpos([],[]).
71textpos([X|Y],[X1|Y1]):-
72 line(X1,0,_,X,[]),
73 !,
74 textpos(Y,Y1).
75
76line(X,I,K)-->spaces(I,J),line1(X,J,K).
77line(X,I,K)-->line1(X,I,K).
78
79line1([c(X,I,J)|Y],I,K)-->token(X,I,J),line(Y,J,K).
80line1([],I,I)-->[].
81
82token([X|Y],I,K)-->[X],{X\==(0'\s),J is I+1},tokenx(Y,J,K). 83
84tokenx([X|Y],I,K)-->[X],{X\==(0'\s),J is I+1},tokenx(Y,J,K). 85tokenx([(0'\s)|X],I,K)-->[(0'\s)],{J is I+1},token(X,J,K). 86tokenx([],I,I)-->[].
87
88spaces(I,K)-->[(0'\s)],{J is I+1},spaces(J,K). 89spaces(I,I)-->[].
90
91manyspaces(I,K)-->spaces(I,K),{K-I>=2}.
92
96
97mkproof(F,p(void,F,[]),[]). 98mkproof(F,p(J,F,A),[L,R|S]):-
99 mkusing(F,J,L),
100 mkantecedents(J,B,R),
101 mkprooflist(B,A,S).
102
103mkprooflist([],[],_). 104mkprooflist([A|B],[A1|B1],L):-
105 mkproof(A,A1,L),
106 mkprooflist(B,B1,L).
107
108mkusing(c(_,S,E),c(M,S1,E1),L):-
109 member(c(M,S1,E1),L),
110 touch([S,E],[S1,E1]),
111 !.
112mkusing(_,void,_).
113
114mkantecedents(void,[],_):-!.
115mkantecedents(X,A,L):-suclist(X,L,A).
116
117touch([_,B],[X,_]):-B<X,!,fail.
118touch([A,_],[_,Y]):-Y<A,!,fail.
119touch(_,_).
120
121touchx(c(_,A,B), c(_,X,Y)):-touch([A,B],[X,Y]).
122
123gentex --> displaymath.
124
125displaymath(X, ["$$", X1, "$$\n"]):- proof2tex(X, X1).
126
128proof2tex(p(void,c(X,_,_),_),Y):-!,string_codes(Y,X) .
129proof2tex(p(c(X,_,_),c(Y,_,_),L0),
130 ["\\prooftree\n",A,"\n","\\",Conclusion,"\n",Y,"\n","\\using ",Rule,"\n","\\endprooftree"]):- (kleene_string_codes("-",X,Rule)->Conclusion="justifies";kleene_string_codes("=",X,Rule)->Conclusion="Justifies";kleene_string_codes(".",X,Rule)->Conclusion="leadsto"),!,(insert(" ",L0,A5),flatten(A5,A6)),maplist(proof2tex,A6,A) .
131proof2tex(p(c(X,_,_),c(Y,_,_),L0),["\\mathvbox{",A,"}{",Y,"}"]):-kleene_string_codes("*",X,_),!,(insert(" ",L0,A6),flatten(A6,A7)),maplist(proof2tex,A7,A) .
132proof2tex(X,X):-! .
133
134suclist(_,[],[]).
135suclist(X,[Y|Z],[Y|U]):- touchx(X,Y),!,suclist(X,Z,U).
136suclist(X,[_|Z],U):- suclist(X,Z,U).
137
138
142prooftree_check(X,[ "main: ", X1,
143 "height: ", X2,
144 "conclusion: ", X3,
145 "antecedent: ", X4,
146 "using: ", X5]):-checkmain(X,X1),
147 checkheight(X,X2),
148 checkconcl(X,X3),
149 checkante(X,X4),
150 checkusing(X,X5).
151
152checkmain([[_]|_], "ok\n").
153checkmain([_|_], "multiple main conclusion\n").
154checkmain(_,"ok\n").
155
156checkheight([_,_,_|_],"ok\n").
157checkheight(_, ["too short proof tree\n"]).
158
159checkconcl([X,Y|Z], A):-function(Y,X),!,checkconcl([Y|Z], A).
160checkconcl([_,_|_], ["multiple conclusions", " or ", "ambiguous antecedents", " or ", "orphant\n"]).
161checkconcl(_,"ok\n").
162
163checkante([_|A],B):-checkante1(A,B).
164
165checkante1([X,Y|Z],B):-totalrel(X,Y),!,checkante1(Z,B).
166checkante1([_,_|_], ["empty antecedants\n"]).
167checkante1(_,"ok\n").
168
169checkusing([X,Y|L],M):-checkusing1(X,Y),!,checkusing(L,M).
170checkusing([_,_|_], "multiple usings\n").
171checkusing(_,"ok\n").
172
173checkusing1([],_).
174checkusing1([X|Y],Z):- suclist(X,Z,A),atmostone(A),checkusing1(Y,Z).
175
176atmostone([]).
177atmostone([_]).
178
179function([],_).
180function([X|Y],Z):-suclist(X,Z,S),S=[_],function(Y,Z).
181
182totalrel([],_).
183totalrel([X|Y],Z):-suclist(X,Z,S),S=[_|_],totalrel(Y,Z)