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
   11%%% convert text base proof figure  into prooftrees
   12%%% [2006/07/21]
   13% platex via lisp.
   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
   36comment_out_region --> split, maplist(comment_out), insert("\n").
   37
   38comment_out(X, Y) :- append(`%`, _, X) -> Y = X ; append(`% `, X, Y).
   39
   40% ?- trace, prooftree:prooftree(`a\n--(rule)\nb`, X).
   41% ?- trace, prooftree:prooftree(`a\n--c\nb\n`, X).
   42%@ X = "$$\\prooftree\na\n\\justifies\nb\n\\using c\n\\endprooftree$$\n" .
   43
   44%@ X = "$$\\prooftree\na\n\\justifies\nb\n\\using c\n\\endprooftree$$\n" .
   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
   93%%--------------------------------------------------------------
   94%% create a proof tree:  p(rule-name, coclusion, antecedents)
   95%%--------------------------------------------------------------
   96
   97mkproof(F,p(void,F,[]),[]).	% make proof tree
   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([],[],_).   	 % make proof tree list
  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
  127% ?- expand_exp(:flip([Y]:- string_codes(Y, X)), p, V, user, G, P, []).
  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
  139%%-------------------------------------------------------
  140%% checking a proof tree
  141%%-------------------------------------------------------
  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)