1:- module(seqcal,[]). 2:- use_module(util(misc)). 3:- use_module(pac(basic)). 4:- use_module(util('emacs-handler')).
21:- current_op(X,_,->), X0 is X-10, op(X0,xfy,<>). 22:- initialization((current_op(X,_,->), X0 is X-10, op(X0,xfy,<>)), restore). 23
27
31
37
38prove(X):- seqcal([]>>[X], P), !,
39 format("~w is provable in LK.~n~n",[X]),
40 p2q(P,Q),
41 raster(Q,R),
42 raster(R).
43prove(X):-format("~w is NOT provable in LK.~n~n",[X]).
44
46
47seqcal(X >> Y, p(axiom, (X>>Y))):- member(Z,X), member(Z,Y), !.
48seqcal(X >> Y, p(left(R), (X>> Y), P)):-
49 removeOne(X,A,B),
50 rewrite(A,A1),
51 left(A1,C,R),
52 subgoals(B >> Y, C, L),
53 seqcallist(L, P).
54seqcal(X >> Y, p(right(R),X>>Y, P)):-
55 removeOne(Y,A,B),
56 rewrite(A,A1),
57 right(A1,C,R),
58 subgoals(X >> B,C,L),
59 seqcallist(L,P).
60
61subgoals(_,[],[]).
62subgoals((X >> Y),[A >> B|C],[X1 >> Y1|C1]):-
63 append(A,X,X1),
64 append(B,Y,Y1),
65 subgoals(X >> Y,C,C1).
66
67seqcallist([],[]).
68seqcallist([X|Y],[P|Q]):-seqcal(X,P),seqcallist(Y,Q).
69
70right(A * B, [[] >> [A], [] >> [B]], (*)).
71right(A + B, [[] >> [A,B]], (+)).
72right(A > B, [[A] >> [B]], (>)).
73right(!(A), [[A] >> []], (!)).
74
75left(A * B, [[A,B] >> []],(*)).
76left(A + B, [([A] >> []), ([B] >> [])], (+) ).
77left(A > B, [([] >> [A]), ([B] >> [])], (>) ).
78left(!(A), [[] >> [A]], (!)).
79
80macrodef(A<B, B>A).
81macrodef(<>(A,B), (A>B) * (B>A)).
82
83rewrite(A,B):-macrodef(A,B),!.
84rewrite(A,A).
85
86removeOne([A|B],A,B).
87removeOne([A|B],C,[A|D]):-removeOne(B,C,D).
127p2q(p(axiom, A),
128 q(W,
129 goal(A1,[0,W,0]),
130 rule([],[]),
131 subgoal([],[])
132 )
133) :- !,sequent_codes(A, A1), length(A1, W).
134p2q(p(J,A,S),
135 q(W,
136 goal(A1,[R1,R2,R3]),
137 rule(J1,[N1,N2,N3,N4]),
138 subgoal(S1,[P1,P2,P3])
139 )
140) :- sequent_codes(A,A1), length(A1,R2),
141 rule_codes(J,J1),length(J1,N3),
142 p2q_list(S,S1),
143 subgoal_width(S1,M1,M2,M3),
144 P2 is M1 + M2 + M3,
145 M2r is M2//2,
146 M2l is M2 - M2r,
147 R2r is R2//2,
148 R2l is R2-R2r,
149
150 ( M1+M2l >= R2l
151 ->
152 P1 = 0
153 ;
154 P1 is R2l - (M1 + M2l)
155 ),
156
157 ( M2 >= R2
158 ->
159 N2 = M2
160 ;
161 N2 = R2
162 ),
163
164 N2r is N2//2,
165 N2l is N2 - N2r,
166
167 (N2r + N3 =< M2r + M3
168 ->
169 P3 = 0,
170 N4 is M2r + M3 - (N2r + N3)
171 ;
172 P3 is N2r + N3 - (M2r + M3),
173 N4 = 0
174 ),
175
176 N1 is (P1 + M1 + M2l) - N2l,
177 R1 is (P1 + M1 + M2l) - R2l,
178 R3 is (M2r + M3 + P3) - R2r,
179 W is P1 + P2 + P3.
180
181sequent_codes((X >> Y), Z) :-
182 insert(`, `, X, X1),
183 insert(`, `, Y, Y1),
184 M = [` `, X1 , ` |- `, Y1 , ` `],
185 smash_codes(M, Z).
186
187
188subgoal_width(X,M1,M2,M3):-
189 subgoal_width1(X,M1),
190 subgoal_width2(X,L),
191 subgoal_width3(X,M3),
192 M2 is L - (M1 + M3).
193
194subgoal_width1([q(_, goal(_,[M|_]), _, _)|_], M).
195
196subgoal_width2([],0).
197subgoal_width2([q(W,_,_,_)|R],M):- subgoal_width2(R, M1), M is W + M1.
198
199subgoal_width3(X,M):- last(X, q(_, goal(_, [_, _, M]), _, _)).
200
201p2q_list([],[]).
202p2q_list([X|Y],[X1|Y1]):- p2q(X, X1), p2q_list(Y, Y1).
203
205
206spaces(N,X):-repeat_code(0'\s , N, X).
207
208line(N,X):-repeat_code(0'-, N, X).
209
210repeat_code(_,0,[]):-!.
211repeat_code(C,N,[C|R]):- N > 0, N1 is N-1, repeat_code(C,N1,R).
212
213rule_codes(right(X),Y):-!, smash_codes(X,X1), append([`(|-`,X1,`)`],Y).
214rule_codes(left(X),Y):-!, smash_codes(X,X1), append([`(`,X1,`|-)`],Y).
215rule_codes(X,Y):-smash_codes(X,Y).
216
217raster([]).
218raster([X|Y]):-raster(Y), format("~s~n",[X]).
219
220raster(q(_,
221 goal(A1, [L, _, R]),
222 rule(_, _),
223 subgoal([], _)
224 ),
225 [X]
226 ):- !, spaces(L, SL), spaces(R, SR), append([SL, A1, SR], X).
227raster(q(_,
228 goal(A1, [R1, _, R3]),
229 rule(J1, [N1, N2, _, N4]),
230 subgoal(S1, [P1, _, P3])
231 ),
232 [X, Y|Z]):-
233 spaces(R1,SR1), spaces(R3,SR3), append([SR1,A1,SR3],X),
234 spaces(N1,SN1), spaces(N4,SN4), line(N2,Hline),
235 append([SN1,Hline,J1,SN4],Y),
236 raster_list(S1,B),
237 spaces(P1,SP1),
238 spaces(P3,SP3),
239 map_append3(SP1,B,SP3,Z).
240
241map_append3(_,[],_,[]).
242map_append3(A,[X|Y],B,[X1|Y1]):- append([A,X,B],X1), map_append3(A,Y,B,Y1).
243
244height_adjust_append([],[],_,_,[]).
245height_adjust_append([X|Y],[],A,B,[Z|U]):-!,append(X,B,Z), height_adjust_append(Y,[],A,B,U).
246height_adjust_append([],[X|Y],A,B,[Z|U]):-!, append(A,X,Z), height_adjust_append([],Y,A,B,U).
247height_adjust_append([X|Y],[P|Q],A,B,[Z|U]):- append(X,P,Z), height_adjust_append(Y,Q,A,B,U).
248
249raster_list([],[[]]).
250raster_list([X|Y],Z):- raster(X,X1), raster_list(Y,Y1),
251 X1=[A|_],
252 Y1=[B|_],
253 length(A,L1),
254 length(B,L2),
255 spaces(L1,S1),
256 spaces(L2,S2),
257 height_adjust_append(X1,Y1,S1,S2,Z).
258
259gentzen --> peek(X, [[]>>[X],X]),
260 eh:phrase_on_car(seqcal:seqcal),
261 !,
262 eh:phrase_on_car(seqcal:(p2q, raster, rasterx)),
263 peek([A, B], [B, A]),
264 eh:phrase_on_car((smash_codes, seqcal:convert_special)),
265 peek([C, D], [`<p> `, C, ` is provable in LK.<br><br></p>`,
266 `<p><pre>`, D, `</pre></p>`]),
267 smash.
268gentzen --> smash_codes,
269 convert_special,
270 peek(A, [`<p> `, A, ` is NOT provable in LK.<br><br></p>`]),
271 smash.
272
273rasterx([],[]).
274rasterx([X|Y],Z):-rasterx(Y,Y1),
275 convert_special(X,X1),
276 append([X1, `<br>`, Y1],Z).
277
278convert_special(X,Y):-convert_special(X,Y,[]).
279
280convert_special([],X,X).
281convert_special([0'<|R],[0'&,0'l,0't,0';|X],Y):-!, convert_special(R,X,Y).
282convert_special([0'>|R],[0'&,0'g,0't,0';|X],Y):-!, convert_special(R,X,Y).
283convert_special([A|R],[A|X],Y):- convert_special(R,X,Y)