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