%% drv.mp 0.93 %% Copyright 2009 Laurent M\'ehats % % This work may be distributed and/or modified under the % conditions of the LaTeX Project Public License, either version 1.3 % of this license or (at your option) any later version. % The latest version of this license is in % http://www.latex-project.org/lppl.txt % and version 1.3 or later is part of all distributions of LaTeX % version 2005/12/01 or later. % % This work has the LPPL maintenance status `maintained'. % % The Current Maintainer of this work is Laurent M\'ehats. % % % This work consists of the file drv.mp %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % User's macros summary % % % * Judgment & inference declarations % =================================== % % jgm % judgment index % sub-judgments math-mode LaTeX code % % nfr () (, ) % inference index % list of premise indices % inference label math-mode LaTeX code % inference line style identifier % (0, 1, 2, 3, 4, 5, 6 or _) % 0 none % 1 simple % 2 double % 3 dotted % 4 dashed % 5 waved % 6 TeX-dotted % _ default (set by drv_path_style) % % mvd (, ) % index of the origin judgment % number of phantom steps % phantom steps path-style identifier % (0, 1, 2, 3, 4, 5, 6 or _) % % Nfr () (, , , ) % inference index % list of premise indices % inference label math-mode LaTeX code % left delimiter label math-mode LaTeX code % right delimiter label math-mode LaTeX code % inference line style identifier % (0, 1, 2, 3, 4, 5, 6 or _) % % Mvd (, , , ) % index of the origin judgment % number of phantom steps % left label math-mode LaTeX code % right label math-mode LaTeX code % phantom steps path-style identifier % (0, 1, 2, 3, 4, 5, 6 or _) % % NFR () (, , , ) % (, , ) % inference index % list of premise indices % left inference label math-mode LaTeX code % right inference label math-mode LaTeX code % left delimiter label math-mode LaTeX code % right delimiter label math-mode LaTeX code % junction style identifier (0, 1, 2, 3 or _) % 0 fully-interlacing % 1 semi-interlacing % 2 non-interlacing % 3 user specified (tricky) % _ default (set by drv_junction_style) % alignment style identifier (l, c, r, u or _) % l left % c centered % r right % u user specified (tricky) % _ default (set by drv_alignment_style) % inference line style identifier % (0, 1, 2, 3, 4, 5, 6 or _) % % MVD (, , , ) % index of the origin judgment % number of phantom steps % left label math-mode LaTeX code % right label math-mode LaTeX code % alignment style identifier (l, c, r, u or _) % phantom steps path-style identifier % (0, 1, 2, 3, 4, 5, 6 or _) % % NFR_opt () () () % (, , ) % inference index % list of premise indices % list of inference labels math-mode LaTeX code % list of delimiter labels math-mode LaTeX code % junction style identifier (0, 1, 2, 3 or _) % alignment style identifier (l, c, r, u or _) % inference line style identifier % (0, 1, 2, 3, 4, 5, 6 or _) % % MVD_opt () () ( ) % index of the origin judgment % number of phantom steps % list of labels math-mode LaTeX code % alignment style identifier (l, c, r or u) % phantom steps path-style identifier % (0, 1, 2, 3, 4, 5, 6 or _) % % * Tunings % ========= % % drv_font_size % LaTeX font-size command % "\tiny" % "\scriptsize" % "\footnotesize" % "\small" % "\normalsize" % "\large" % "\Large" % etc. % % drv_math_style (, ) % component identifier (drv, jdg, ilb, dlb or plb) % drv derivation trees % jdg judgments % ilb inference labels % dlb delimiter labels % plb phantom steps labels % LaTeX math-style command % % drv_scale (, ) % scale identifier (clr, prm, jdg or ilb) % clr nice explanation soon (see examples) % prm nice explanation soon (see examples) % jdg nice explanation soon (see examples) % ilb nice explanation soon (see examples) % scale value % % drv_junction_style % junction style identifier (0, 1 or 2) % 0 ``fully-interlacing'' % 1 ``semi-interlacing'' % 2 ``non-interlacing'' % % drv_alignment_style % alignment style identifier (l, c or r) % l left % c centered % r right % % drv_path_style (, ) % path-type identifier (iln or phm) % iln inference lines % phm phantom steps paths % path-style identifier (0, 1, 2, 3, 4, 5 or 6) % % drv_labels_position (, ) % label-type identifier (ilb, plb or dlb) % ilb inference labels % dlb delimiter labels % plb phantom steps labels % position identifier (l or r) % l left % r right % % drv_roots_position % position identifier (t or b) % t top % b bottom % % drv_axis_reference % reference identifier (iln or jdg) % iln root inference line axis % jdg root judgment math-axis % % drv_left_delimiter % left delimiter math-mode LaTeX code % "(" $($ % "[" $[$ % "\lbrace" $\lbrace$ % "\langle" $\langle$ % etc. % % drv_right_delimiter % right delimiter math-mode LaTeX code % ")" % "]" % "\rbrace" % "\rangle" % etc. % % drv_box_mode % status identifier (on or off) % on % off % % drv_fraction_mode % status identifier (on or off) % on % off % % drv_proof_mode % status identifier (on or off) % on % off % % * Derivation tree pictures % ========================== % % drv_bbox % sub-tree root index % % drv_axis (, ) % reference type identifier (iln, jdg or dlm) % iln inference line axis % jdg judgment math-axis % dlm delimiter axis % reference index % % drv_styled % MetaPost path expression % path style identifier (0, 1, 2, 3, 4, 5 or 6) % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % MetaPost messages formatting % % drv_format prevents messages from being automatically cut into lines every % 79 characters: if possible, a word which would otherwise be cut is 'pushed' % to the following line by inserting space characters before it. vardef drv_format (expr str, fst_len, nxt_len, dbl_pcs)= % str: the message to be formatted % fst_len: first line length % nxt_len: following lines length % dbl_pcs (boolean): occurrences of the percent character must be doubled save str_len, sub_len, aux_len, chr_rnk, occ_num; numeric str_len, sub_len, aux_len, chr_rnk, occ_num; save aux_str, chr; string aux_str, chr; str_len:=length str; sub_len:=0; chr_rnk:=0; occ_num:=0; aux_len:=0; aux_str:=""; forever: exitif (chr_rnk=fst_len) or (chr_rnk=str_len); chr:=substring (chr_rnk, chr_rnk+1) of str; aux_str:=aux_str&chr; if chr=" ": sub_len:=chr_rnk+1; aux_len:=sub_len+occ_num; elseif (chr="%") and dbl_pcs: aux_str:=aux_str&"%"; occ_num:=occ_num+1; fi chr_rnk:=chr_rnk+1; endfor if chr_rnk=fst_len: begingroup if sub_len=0: sub_len:=fst_len; aux_len:=sub_len+occ_num; fi substring (0, aux_len) of aux_str& for idx=sub_len+1 upto fst_len: " "& endfor drv_format (substring (sub_len, str_len) of str, nxt_len, nxt_len, dbl_pcs) endgroup else: aux_str fi enddef; boolean drv_inside_fig; drv_inside_fig:=false; vardef drv_context= "drv"&if drv_inside_fig: " (fig. "&decimal charcode&")"&fi ": " enddef; vardef drv_message expr str= message drv_format (drv_context&str, 79, 79, false); enddef; vardef drv_errhelp expr str= % Occurrences of the percent character must be doubled: errhelp makes single % single occurrences behave as newline characters (this is inherited from % MetaFont). errhelp drv_format (str, 79, 79, true); enddef; vardef drv_errmessage expr str= % errmessage inserts the 2-characters string "! " before its argument. % Hence 77 as a first line length argument. errmessage drv_format (drv_context&str, 77, 79, false); enddef; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % Delayed LaTeX processing % picture tex_pct[]; string delayed_tex_file; delayed_tex_file:=jobname&"-delayed.mp"; % % reading LaTeX picture definitions % boolean drv_nullpicture; drv_nullpicture:=true; string readfrom_str; readfrom_str:=readfrom delayed_tex_file; if readfrom_str<>EOF: closefrom delayed_tex_file; drv_message ("reading `"&delayed_tex_file&"' LateX picture definitions."); batchmode; scantokens ("input "&delayed_tex_file); errorstopmode; drv_message "done."; drv_nullpicture:=false; fi % % copying LaTeX preamble % vardef drv_read (expr search_str) (suffix accum_str)= save readfrom_str, readfrom_substr; string readfrom_str, readfrom_substr; accum_str:=""; forever: readfrom_str:=readfrom jobname; readfrom_substr:=substring (0, length search_str) of readfrom_str; exitif (readfrom_substr=search_str) or (readfrom_str=EOF); accum_str:=accum_str&readfrom_str&char(10); endfor if readfrom_str=EOF: closefrom jobname; drv_errhelp ("`"&jobname&".mp' should contain a line starting with "& ditto&search_str&ditto&"."); drv_errmessage (ditto&search_str&ditto&" is missing"); fi enddef; string tex_preamble_str[]; % tex_preamble_str[0] from "verbatimtex %&latex" to "\begin{document}" % tex_preamble_str[1] from "\begin{document}" to "etex;" drv_message ("reading `"&jobname&".mp' LateX preamble."); drv_read ("verbatimtex %&latex", tex_preamble_str[0]); drv_read ("\begin{document}", tex_preamble_str[0]); drv_read ("etex;", tex_preamble_str[1]); closefrom jobname; write "%"&char(10)& "% AUTOMATICALLY GENERATED BY DRV.MP - DO NOT MODIFY."&char(10)& "%"&char(10)&char(10)& "verbatimtex %&latex"&char(10)& tex_preamble_str[0]& "\begin{document}"&char(10)& tex_preamble_str[1]& "etex;" to delayed_tex_file; drv_message "done."; % % writing LaTeX picture definitions % numeric tex_pct_idx; tex_pct_idx:=0; % Math style indices: 0, 1, 2, 3 string mth_sty_str[]; mth_sty_str[0]:="\displaystyle"; mth_sty_str[1]:="\textstyle"; mth_sty_str[2]:="\scriptstyle"; mth_sty_str[3]:="\scriptscriptstyle"; string drv_fontsize; vardef drv_tex[] expr tex_str= % @: math style index % tex_str: math mode LaTeX code save def_str, pct; string def_str; picture pct; def_str:="btex{"&drv_fontsize&"$"&mth_sty_str[@]&"{}"&tex_str&"{}$}etex;"; write "tex_pct["&(decimal tex_pct_idx)&"]:="&def_str to delayed_tex_file; pct:= if known tex_pct[tex_pct_idx]: tex_pct[tex_pct_idx] else: nullpicture fi; tex_pct_idx:=tex_pct_idx+1; pct enddef; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % MetaPost shorthands % vardef depth expr pct= ypart llcorner pct enddef; vardef height expr pct= ypart urcorner pct enddef; vardef width expr pct= xpart urcorner pct-xpart llcorner pct enddef; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % Font-specific parameters % % % em[s] width of an m (s: mathstyle index) % ex[s] height of an x % axis_hg[s] height of the mathematical axis % num_bl_hg[s] height of a numerator baseline w.r.t. the fraction bar axis % den_bl_dp[s] depth of a denominator baseline w.r.t. the fraction bar axis % rul_thk[s] default rule thickness % numeric em[], ex[], axis_hg[], num_bl_hg[], den_bl_dp[], rul_thk[]; % % thn_sp[s] thin space, usually 1em/6 % med_sp[s] medium space, usually 2em/9 % thk_sp[s] thick space, usually 5em/18 % numeric thn_sp[], med_sp[], thk_sp[]; % % pdt_hg[s] height of a punctuation ldot % pdt_wd[s] width of a punctuation ldot % numeric pdt_hg[], pdt_wd[]; % % tt_dgt[s][i] typewriter typeface digits (i ranges from 0 to 9) % picture tt_dgt[][]; % % min_clr[s] minimal clearance between a numerator % or a denominator and the fraction bar % prm_skp[s] % jdg_skp[s] % ilb_skp[s] % plb_skp[s] % numeric min_clr[], prm_skp[], jdg_skp[], ilb_skp[], plb_skp[]; vardef drv_fontdimen[] expr font= save dim_pct; picture dim_pct; dim_pct:=drv_tex[0] ("\rule{\the\fontdimen"&(decimal @)&font&"}{0bp}"); width dim_pct enddef; vardef drv_font_size expr size_str= save pdt_pct, sp_pct; picture pdt_pct, sp_pct; drv_fontsize:=size_str; write char(10)&"% font-specific parameters ("&drv_fontsize&")"&char(10) to delayed_tex_file; ex[0]:=drv_fontdimen[5] "\textfont2"; ex[1]:=drv_fontdimen[5] "\textfont2"; ex[2]:=drv_fontdimen[5] "\scriptfont2"; ex[3]:=drv_fontdimen[5] "\scriptscriptfont2"; em[0]:=drv_fontdimen[6] "\textfont2"; em[1]:=drv_fontdimen[6] "\textfont2"; em[2]:=drv_fontdimen[6] "\scriptfont2"; em[3]:=drv_fontdimen[6] "\scriptscriptfont2"; rul_thk[0]:=drv_fontdimen[8] "\textfont3"; rul_thk[1]:=drv_fontdimen[8] "\textfont3"; rul_thk[2]:=drv_fontdimen[8] "\scriptfont3"; rul_thk[3]:=drv_fontdimen[8] "\scriptscriptfont3"; axis_hg[0]:=drv_fontdimen[22] "\textfont2"; axis_hg[1]:=drv_fontdimen[22] "\textfont2"; axis_hg[2]:=drv_fontdimen[22] "\scriptfont2"; axis_hg[3]:=drv_fontdimen[22] "\scriptscriptfont2"; num_bl_hg[0]:=(drv_fontdimen[8] "\textfont2")-axis_hg[0]; num_bl_hg[1]:=(drv_fontdimen[9] "\textfont2")-axis_hg[1]; num_bl_hg[2]:=(drv_fontdimen[9] "\scriptfont2")-axis_hg[2]; num_bl_hg[3]:=(drv_fontdimen[9] "\scriptscriptfont2")-axis_hg[3]; den_bl_dp[0]:=-(drv_fontdimen[11] "\textfont2")-axis_hg[0]; den_bl_dp[1]:=-(drv_fontdimen[12] "\textfont2")-axis_hg[1]; den_bl_dp[2]:=-(drv_fontdimen[12] "\scriptfont2")-axis_hg[2]; den_bl_dp[3]:=-(drv_fontdimen[12] "\scriptscriptfont2")-axis_hg[3]; min_clr[0]:=3*rul_thk[0]; % The TEXbook, min_clr[1]:=1*rul_thk[1]; % Appendix G, min_clr[2]:=1*rul_thk[2]; % Rule 15d. min_clr[3]:=1*rul_thk[3]; % for mth_sty:=0 upto 3: sp_pct:=drv_tex[mth_sty] "\,"; thn_sp[mth_sty]:=width sp_pct; sp_pct:=drv_tex[mth_sty] "\>"; med_sp[mth_sty]:=width sp_pct; sp_pct:=drv_tex[mth_sty] "\;"; thk_sp[mth_sty]:=width sp_pct; pdt_pct:=drv_tex[mth_sty] "\ldotp"; pdt_hg[mth_sty]:=height pdt_pct; pdt_wd[mth_sty]:=width pdt_pct; for dgt=0 upto 9: tt_dgt[mth_sty][dgt]:=drv_tex[mth_sty] "\texttt{"&(decimal dgt)&"}"; endfor prm_skp[mth_sty]:=3*med_sp[mth_sty]; % arbitrary jdg_skp[mth_sty]:=thn_sp[mth_sty]; % arbitrary ilb_skp[mth_sty]:=thn_sp[mth_sty]; % arbitrary plb_skp[mth_sty]:=thk_sp[mth_sty]; % arbitrary endfor enddef; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % Math-related parameters & macros % % % Math styles % drv_sty derivation trees % jdg_sty[drv_sty] judgments % ilb_sty[drv_sty] inference labels % dlb_sty[drv_sty] delimiter labels % plb_sty[drv_sty] phantom steps labels % numeric drv_sty, jdg_sty[], ilb_sty[], dlb_sty[], plb_sty[]; % % Math-axis centered LaTeX pictures % vardef mth_tex[] expr tex_str= (drv_tex[@] tex_str) shifted (0, -axis_hg[@]) enddef; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % drv-boxes % vardef drv_box text STR= for str=STR: expandafter picture scantokens str; expandafter pair scantokens str.l; expandafter pair scantokens str.c; expandafter pair scantokens str.r; expandafter numeric scantokens str.hg; expandafter numeric scantokens str.dp; endfor enddef; vardef box_init @# (expr pct)= @#:=pct; @#.r-@#.l=(width pct, 0); @#.c=(@#.l+@#.r)/2; @#.hg:=height pct; @#.dp:=depth pct; enddef; vardef box_freeze @#= @#:=@# shifted @#.l; enddef; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % beginfig & endfig % % % drv_beginfig: figure initialization % pen drv_pen; vardef drv_beginfig= % % Judgments % % jdg[i] judgment drv-box % sbj_num[i] number of sub-judgments % sbj[i][j] sub-judgment drv-box (j ranges from 0 to sbj_num[i]-1) % drv_box "jdg[]"; numeric sbj_num[]; drv_box "sbj[][]"; % % Inferences % % prm_num[i] number of premises % prm[i][j] premise index (j ranges from 0 to prm_num[i]-1) % ccl[i] conclusion index % jct_sty[i] junction style % alg_sty[i] alignment style % iln_sty[i] inference line style % l_prm[i] leftmost `graphical' premise index % r_prm[i] rightmost `graphical' premise index % numeric prm_num[], prm[][], ccl[]; numeric jct_sty[]; string alg_sty[]; numeric iln_sty[]; numeric l_prm[], r_prm[]; % % imin_x[i] inference minimal x % l_dlb[i] left delimiter label drv-box % l_dlm[i] left delimiter drv-box % l_ilb[i] left label drv-box % iln[i] inference line drv-box % r_ilb[i] right label drv-box % r_dlm[i] right delimiter drv-box % r_dlb[i] right delimiter label drv-box % imax_x[i] inference maximal x % numeric imin_x[]; drv_box "l_dlb[]", "l_dlm[]", "l_ilb[]"; drv_box "iln[]"; drv_box "r_ilb[]", "r_dlm[]", "r_dlb[]"; numeric imax_x[]; % % Sub-trees % % smin_x[i] sub-tree minimal x % smax_x[i] sub-tree maximal x % smin_y[i] sub-tree minimal y % smax_y[i] sub-tree maximal y % boxed[i] boolean % numeric smin_x[], smax_x[], smin_y[], smax_y[]; boolean boxed[]; % % Pen initialization % drv_pen:=pencircle scaled rul_thk[drv_sty]; % % num_hg height of a numerator axis w.r.t. the fraction bar axis % den_dp depth of a denominator axis w.r.t. the fraction bar axis % iln_hg[s] height of a style s inference line % iln_dp[s] depth of a style s inference line % numeric num_hg, den_dp, iln_hg[], iln_dp[]; num_hg:=num_bl_hg[drv_sty]+axis_hg[jdg_sty[drv_sty]]; den_dp:=den_bl_dp[drv_sty]+axis_hg[jdg_sty[drv_sty]]; picture iln_pct; for sty=0 upto 6: iln_pct:=((0, 0)--(10, 0)) drv_styled sty; iln_hg[sty]:=height iln_pct; iln_dp[sty]:=depth iln_pct; endfor % % Derivation trees % % root_num number of roots % root[i] root index (i ranges from 0 to root_num-1) % drv_built boolean % drv_frozen boolean % numeric root_num, root[]; boolean drv_checked, drv_built, drv_frozen; root_num:=0; drv_checked:=false; drv_built:=false; drv_frozen:=false; % % Phantom steps % % phm_idx phantom inferences index % src[i] base phantom judgment index (in case of an origin judgment) % tgt[i] origin judgment index (in case of a base phantom judgment) % phm_sty[i] phantom steps style % l_plb[i] left phantom steps label drv-box (in case of a base % phantom judgment) % phm[i] phantom steps drv-box (in case of a base phantom % judgment) % r_plb[i] right phantom steps label drv-box (in case of a base % phantom judgment) % numeric phm_idx, src[], tgt[], phm_sty[]; phm_idx:=0; drv_box "l_plb[]", "phm[]", "r_plb[]"; % % Proof pictures % % jdg_prf[i] judgment index drv-box % sbj_prf[i][j] sub-judgment index drv-box (j ranges from 0 to % sbj_num[i]-1) % drv_box "jdg_prf[]", "sbj_prf[][]"; % % Info % write char(10)&"% fig. "&(decimal charcode)&char(10) to delayed_tex_file; drv_inside_fig:=true; % context: inside a figure enddef; extra_beginfig:=extra_beginfig&"drv_beginfig;"; % % drv_endfig: proof-file generation % string proof_file; proof_file:=jobname&"-proof.tex"; % TODO: taking outputtemplate into account. vardef output_file[]= jobname&"."&(decimal @) enddef; string buf_str; buf_str:= "%"&char(10)& "% AUTOMATICALLY GENERATED BY DRV.MP."&char(10)& "%"&char(10)&char(10)& tex_preamble_str[0]& "\usepackage{graphicx}"&char(10)& "\makeatletter"&char(10)& "\def\Gin@def@bp#1\relax#2#3{\gdef#2{#3}}"&char(10)& "\newsavebox{\graphicsbox}"&char(10)& "\newcommand*{\drv}[1]{%"&char(10)& "\sbox{\graphicsbox}{\includegraphics{#1}}%"&char(10)& "\raisebox{\Gin@lly bp}%"&char(10)& "{\usebox{\graphicsbox}}}"&char(10)& "\makeatother"&char(10)&char(10)& "\newcount\h"&char(10)& "\newcount\m"&char(10)& "\h=\time"&char(10)& "\divide\h 60"&char(10)& "\m=-\h"&char(10)& "\multiply\m 60"&char(10)& "\advance\m\time"&char(10)& "\def\hm{\number\h:\ifnum\m<10{}0\fi\number\m}"&char(10)&char(10)& "\newcommand{\mathaxis}{\frac{\quad}{}}"&char(10)&char(10)& "\begin{document}"&char(10)& tex_preamble_str[1]& "\noindent\today\ at \hm\medskip"&char(10)&char(10)&"\noindent"; vardef drv_endfig= drv_inside_fig:=false; % context: outside a figure buf_str:=buf_str&char(10)& "\texttt{"&output_file[charcode]&"}"&char(10)& " (\verb+"&drv_fontsize&"+, \verb+"&(mth_sty_str[drv_sty])&"+)"&char(10)& " {"&drv_fontsize&char(10)& " \["&(mth_sty_str[drv_sty])&char(10)& " \mathaxis\drv{"&output_file[charcode]&"}\mathaxis"&char(10)& " \]}\\"; write EOF to proof_file; % erases the previous content write buf_str&char(10)&"\end{document}" to proof_file; write EOF to proof_file; if drv_nullpicture: draw btex{\tt drv}: run {\tt mpost} again.etex withcolor (1, 0, 0); fi enddef; extra_endfig:="drv_endfig;"&extra_endfig; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % Judgment declarations % vardef jgm[] text SUB= % @: judgment index % SUB: list of `sub-judgments' (pictures or strings) if @<0: drv_errhelp "An judgment index can not be negative."; drv_errmessage (decimal @)&" is negative"; elseif known jdg[@]: drv_errhelp "An index can be used only once to declare a judgment."; drv_errmessage (decimal @)&" has been used already as a judgment index"; else: save jdg_pct, sbj_pct, jdg_wd, sbj_rnk; picture jdg_pct, sbj_pct; numeric jdg_wd, sbj_rnk; jdg_pct:=nullpicture; jdg_wd:=0; sbj_rnk:=0; for sub=SUB: sbj_pct:= if picture sub: sub elseif sub<>"": mth_tex[jdg_sty[drv_sty]] sub else: nullpicture fi; box_init sbj[@][sbj_rnk] (sbj_pct); if sbj_rnk>0: sbj[@][sbj_rnk-1].r=sbj[@][sbj_rnk].l; fi addto jdg_pct also sbj_pct shifted (jdg_wd, 0); jdg_wd:=width jdg_pct; sbj_rnk:=sbj_rnk+1; endfor sbj_num[@]:=sbj_rnk; box_init jdg[@] (jdg_pct); if sbj_num[@]>0: jdg[@].l=sbj[@][0].l; jdg[@].r=sbj[@][sbj_num[@]-1].r; fi fi enddef; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % Inference declarations % vardef check_junction_style (suffix sty_sfx) (expr default)= save sty_str; string sty_str; sty_str:=str sty_sfx; if (sty_str="0") or (sty_str="1") or (sty_str="2") or (sty_str="3"): sty_sfx elseif (sty_str="_"): default else: begingroup drv_errhelp "Valid identifiers are"& " 0 (fully-interlacing),"& " 1 (semi-interlacing),"& " 2 (non-interlacing),"& " 3 (user specified) and"& " _ (default)."; drv_errmessage sty_str&" is not a valid junction style identifier"; default endgroup fi enddef; vardef check_alignment_style (suffix sty_sfx) (expr default)= save sty_str; string sty_str; sty_str:=str sty_sfx; if (sty_str="l") or (sty_str="c") or (sty_str="r") or (sty_str="u"): sty_str elseif (sty_str="_"): default else: begingroup drv_errhelp "Valid identifiers are"& " l (none),"& " c (simple),"& " r (double),"& " u (dotted) and"& " _ (default)."; drv_errmessage sty_str&" is not a valid alignment style identifier"; default endgroup fi enddef; vardef check_path_style (suffix sty_sfx) (expr default)= save sty_str; string sty_str; sty_str:=str sty_sfx; if (sty_str="0") or (sty_str="1") or (sty_str="2") or (sty_str="3") or (sty_str="4") or (sty_str="5") or (sty_str="6"): sty_sfx elseif (sty_str="_"): default else: begingroup drv_errhelp "Valid identifiers are"& " 0 (none),"& " 1 (simple),"& " 2 (double),"& " 3 (dotted),"& " 4 (dashed),"& " 5 (waved),"& " 6 (TeX-dotted) and"& " _ (default)."; drv_errmessage sty_str&" is not a valid path style identifier"; default endgroup fi enddef; vardef opt_init[] @# expr arg= if picture arg: if arg<>nullpicture: box_init @# (arg); fi elseif arg<>"": box_init @# (mth_tex[@] arg); fi enddef; vardef NFR[] (text PRM) (expr lilb, rilb, ldlb, rdlb) (suffix j_sty, a_sty, i_sty)= % % @: inference index % if known prm_num[@]: drv_errhelp "An index can be used only once to declare an inference."; drv_errmessage (decimal @)&" has been used already as an inference index"; else: % % PRM: list of premise indices % save prm_rnk; numeric prm_rnk; prm_rnk:=0; for prm_idx=PRM: if prm_idx=@: drv_errhelp "An inference index can not be used"& " as one of its own premise indices."; drv_errmessage "the inference index "&(decimal prm_idx)& " is used as one of its own premise indices"; elseif known ccl[prm_idx]: drv_errhelp "An index can be used only once as a premise index."; drv_errmessage (decimal prm_idx)&" has been used already as a"& " premise index for inference declaration "&(decimal ccl[prm_idx]); else: if known prm_num[prm_idx]: % % roots list update % save root_idx; numeric root_idx; root_idx:=0; forever: exitif root[root_idx]=prm_idx; root_idx:=root_idx+1; endfor forever: exitif root_idx=root_num-1; root[root_idx]:=root[root_idx+1]; root_idx:=root_idx+1; endfor root_num:=root_num-1; fi ccl[prm_idx]:=@; prm[@][prm_rnk]:=prm_idx; prm_rnk:=prm_rnk+1; fi endfor prm_num[@]:=prm_rnk; if known ccl[@]: % % cycle detection % save ccl_idx, ccl_str; numeric ccl_idx; string ccl_str; ccl_idx:=@; ccl_str:=decimal ccl_idx; forever: ccl_idx:=ccl[ccl_idx]; if ccl_idx>=0: ccl_str:=(decimal ccl_idx)&", "&ccl_str; fi exitif (unknown ccl[ccl_idx]) or (ccl_idx=@); endfor if ccl_idx=@: drv_errhelp "Inferences declarations can not be cyclic."; drv_errmessage "inference declaration "&(decimal @)&" creates a"& " cycle of inferences (indices "&ccl_str&" from conclusions to"& " premises)"; fi else: root[root_num]:=@; root_num:=root_num+1; fi % % lilb, rilb: inference labels % opt_init[ilb_sty[drv_sty]] l_ilb[@] lilb; opt_init[ilb_sty[drv_sty]] r_ilb[@] rilb; % % ldlb, rdlb: delimiter labels % opt_init[dlb_sty[drv_sty]] l_dlb[@] ldlb; opt_init[dlb_sty[drv_sty]] r_dlb[@] rdlb; % % j_sty, a_sty and i_sty: junction, alignment and inference styles % jct_sty[@]:=check_junction_style (j_sty, drv_jct_sty); alg_sty[@]:=check_alignment_style (a_sty, drv_alg_sty); iln_sty[@]:=check_path_style (i_sty, drv_iln_sty); if drv_boxmode_on: boxed[@]:=true; fi fi enddef; vardef DCL[] (text PRM) (expr lilb, rilb, ldlb, rdlb) (suffix j_sty, a_sty, i_sty) text SUB= NFR[@] (PRM) (lilb, rilb, ldlb, rdlb, j_sty, a_sty, i_sty); jgm[@] SUB; enddef; vardef MVD[] (expr inf_num, lplb, rplb) (suffix a_sty, p_sty)= if inf_num<1: drv_errhelp "The minimal value is 1."; drv_errmessage (decimal inf_num)&" is not a valid number of inference"& " steps"; else: save aux_idx, aux_sty, phm_jdg; numeric aux_idx, aux_sty; picture phm_jdg; aux_sty:=check_path_style (p_sty, drv_phm_sty); phm_jdg:=nullpicture; setbounds phm_jdg to (0, 0)--(iln_hg[aux_sty]-iln_dp[aux_sty], 0)--cycle; aux_idx:=@; for i=1 upto inf_num: phm_idx:=phm_idx-1; box_init jdg[phm_idx] (phm_jdg); sbj_num[phm_idx]:=0; NFR[phm_idx] (aux_idx) ("", "", "", "", 0, a_sty, 0); aux_idx:=phm_idx; endfor src[@]:=phm_idx; tgt[phm_idx]:=@; phm_sty[phm_idx]:=aux_sty; % % lplb, rplb: phantom steps labels % opt_init[plb_sty[drv_sty]] l_plb[phm_idx] lplb; opt_init[plb_sty[drv_sty]] r_plb[phm_idx] rplb; phm_idx fi enddef; vardef bxd[]= boxed[@]:=true; @ enddef; % % Optional labels & shorthands % numeric drv_jct_sty; % default junction style string drv_alg_sty; % default junction style numeric drv_iln_sty; % default inference line path-style numeric drv_phm_sty; % default phantom steps path-style boolean drv_left_ilb; % inference labels on the left boolean drv_left_dlb; % delimiter labels (hence delimiters) on the left boolean drv_left_plb; % phantom steps labels on the left vardef arg_type expr arg= if picture arg: "picture" else: "string" fi enddef; vardef opt_lbls @# (text LBL) expr left_lbls= save lbl_num, fst_lbl, snd_lbl; numeric lbl_num; lbl_num:=0; for lbl=LBL: if lbl_num=0: scantokens (arg_type lbl) fst_lbl; fst_lbl:=lbl; elseif lbl_num=1: scantokens (arg_type lbl) snd_lbl; snd_lbl:=lbl; else: drv_errhelp "At most two labels can be specified:"& " a left one and a right one."; drv_errmessage "more than two labels have been specified"; fi lbl_num:=lbl_num+1; endfor if lbl_num=0: string @#.l; string @#.r; @#.l:=""; @#.r:=""; elseif lbl_num=1: if left_lbls: scantokens (arg_type fst_lbl) @#.l; string @#.r; @#.l:=fst_lbl; @#.r:=""; else: string @#.l; scantokens (arg_type fst_lbl) @#.r; @#.l:=""; @#.r:=fst_lbl; fi else: scantokens (arg_type fst_lbl) @#.l; scantokens (arg_type snd_lbl) @#.r; @#.l:=fst_lbl; @#.r:=snd_lbl; fi enddef; vardef NFR_opt[] (text PRM) (text ILB) (text DLB) (suffix j_sty, a_sty, i_sty)= opt_lbls ilb (ILB) drv_left_ilb; opt_lbls dlb (DLB) drv_left_dlb; NFR[@] (PRM) (ilb.l, ilb.r, dlb.l, dlb.r, j_sty, a_sty, i_sty); enddef; vardef DCL_opt[] (text PRM) (text ILB) (text DLB) (suffix j_sty, a_sty, i_sty) text SUB= NFR_opt[@] (PRM) (ILB) (DLB) (j_sty, a_sty, i_sty); jgm[@] SUB; enddef; vardef MVD_opt[] (expr inf_num) (text PLB) (suffix a_sty, p_sty)= opt_lbls plb (PLB) drv_left_plb; MVD[@] (inf_num, plb.l, plb.r, a_sty, p_sty) enddef; % Nfr, Dcl & Mvd vardef Nfr[] (text PRM) (expr ilb, ldlb, rdlb) (suffix i_sty)= NFR_opt[@] (PRM) (ilb) (ldlb, rdlb) (_, _, i_sty); enddef; vardef Dcl[] (text PRM) (expr ilb, ldlb, rdlb) (suffix i_sty) text SUB= Nfr[@] (PRM) (ilb, ldlb, rdlb, i_sty); jgm[@] SUB; enddef; vardef Mvd[] (expr inf_num, lplb, rplb) (suffix p_sty)= MVD[@] (inf_num, lplb, rplb, _, p_sty) enddef; % nfr, dcl & mvd vardef nfr[] (text PRM) (expr ilb) (suffix i_sty)= NFR_opt[@] (PRM) (ilb) () (_, _, i_sty); enddef; vardef dcl[] (text PRM) (expr ilb) (suffix i_sty) text SUB= nfr[@] (PRM) (ilb, i_sty); jgm[@] SUB; enddef; vardef mvd[] (expr inf_num) (suffix p_sty)= MVD_opt[@] (inf_num) () (_, p_sty) enddef; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % Pictured paths % vardef dotted_aux (expr pth, dot_wd, dots_dist)= save pth_len, pct; numeric pth_len; picture pct; pth_len:=arclength pth; pct:=nullpicture; if dots_dist>0: stp_num:=round ((pth_len-dot_wd)/dots_dist); if stp_num>0: stp_len:=(pth_len-dot_wd)/stp_num; addto pct doublepath pth dashed dashpattern (on 0 off stp_len) shifted (dot_wd/2, 0) withpen pencircle scaled dot_wd; fi fi pct enddef; primarydef pth dotted wd_dist= dotted_aux(pth, xpart wd_dist, ypart wd_dist) enddef; vardef expanded_aux (expr pth, scl, dir, stp_len)= save pth_len, aux_len; numeric pth_len, aux_len; pth_len:=arclength pth; if (stp_len>0) and (pth_len>stp_len): aux_len:=pth_len/(pth_len div stp_len); point arctime 0 of pth of pth shifted (unitvector direction arctime 0 of pth of pth rotated dir scaled scl).. {direction arctime 0 of pth of pth} for i=aux_len step aux_len until pth_len-aux_len: point arctime i of pth of pth shifted (unitvector direction arctime i of pth of pth rotated dir scaled scl) {direction arctime i of pth of pth}.. endfor point arctime pth_len of pth of pth shifted (unitvector direction arctime pth_len of pth of pth rotated dir scaled scl) {direction arctime pth_len of pth of pth} else: pth fi enddef; primarydef pth expanded scl_dir_len= expanded_aux (pth, redpart scl_dir_len, greenpart scl_dir_len, bluepart scl_dir_len) enddef; vardef waved_aux (expr pth, amp)= save pth_len, mid; numeric pth_len, mid; pth_len:=arclength pth; if (amp>0) and (pth_len>2(1+sqrt 5)*amp): mid:=pth_len/(2(pth_len div (2(1+sqrt 5)*amp))); point arctime 0 of pth of pth shifted (unitvector direction arctime 0 of pth of pth rotated -90 scaled amp) {direction arctime 0 of pth of pth} for i=mid step 2mid until pth_len: ..point arctime i of pth of pth shifted (unitvector direction arctime i of pth of pth rotated 90 scaled amp) {direction arctime i of pth of pth} ..point arctime i+mid of pth of pth shifted (unitvector direction arctime i+mid of pth of pth rotated -90 scaled amp) {direction arctime i+mid of pth of pth} endfor else: pth fi enddef; primarydef pth waved amp= waved_aux(pth, amp) enddef; vardef drv_styled_aux[] expr pth= save sty_idx, pth_len, pct; numeric sty_idx, pth_len; picture pct; sty_idx:=check_path_style (@, 1); pth_len:=arclength pth; pct:=nullpicture; if sty_idx=1: interim linecap:=butt; addto pct doublepath pth withpen drv_pen; elseif sty_idx=2: interim linecap:=butt; addto pct doublepath pth expanded (1.25rul_thk[drv_sty], 90, rul_thk[drv_sty]) withpen drv_pen; addto pct doublepath pth expanded (1.25rul_thk[drv_sty], -90, rul_thk[drv_sty]) withpen drv_pen; elseif sty_idx=3: addto pct also pth dotted (rul_thk[drv_sty], 2rul_thk[drv_sty]); elseif sty_idx=4: if rul_thk[drv_sty]>0: interim linecap:=butt; save dsh_num, dsh_len; numeric dsh_num, dsh_len; dsh_num:=round(pth_len/(3rul_thk[drv_sty])); dsh_len:= if odd dsh_num: pth_len/dsh_num else: pth_len/(dsh_num+1) fi; addto pct doublepath pth dashed dashpattern(on dsh_len off dsh_len) withpen drv_pen; fi elseif sty_idx=5: interim linecap:=butt; addto pct doublepath pth waved 1.25rul_thk[drv_sty] withpen drv_pen; elseif (sty_idx=6) and (pth_len>0): addto pct also pth dotted (pdt_hg[drv_sty], pdt_wd[drv_sty]); fi pct enddef; primarydef pth drv_styled sty= drv_styled_aux[sty] pth enddef; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % Delimiters % % % 1. Global parameters % string drv_l_dlm; % left delimiter LaTeX code string drv_r_dlm; % right delimiter LaTeX code % % 2. Macros % vardef minmax_y[]=( if drv_bot_roots: if known ccl[@]: ypart jdg[@].c-num_hg+iln_hg[(iln_sty[ccl[@]])] +min_clr_scl*min_clr[drv_sty]/2 else: smin_y[@]-min_clr_scl*min_clr[drv_sty] fi, smax_y[@]+min_clr_scl*min_clr[drv_sty] else: smin_y[@]-min_clr_scl*min_clr[drv_sty], if known ccl[@]: ypart jdg[@].c-den_dp-iln_hg[(iln_sty[ccl[@]])] -min_clr_scl*min_clr[drv_sty]/2 else: smax_y[@]+min_clr_scl*min_clr[drv_sty] fi fi) enddef; vardef delim @# expr dlm_len= save rule_str, dlm_str, dlm_pct, dlm_dp; string rule_str, dlm_str; picture dlm_pct; numeric dlm_dp; rule_str:="\rule{0bp}{"&(decimal(dlm_len/2+axis_hg[drv_sty]))&"bp}"; dlm_str:= if str @#="l": "\left"&drv_l_dlm&rule_str&"\right." else: "\left."&rule_str&"\right"&drv_r_dlm fi; dlm_pct:=mth_tex[drv_sty] dlm_str; dlm_dp:=depth dlm_pct; if dlm_dp=0: nullpicture else: begingroup setbounds dlm_pct to (xpart llcorner dlm_pct, dlm_dp) --(xpart ulcorner dlm_pct, -dlm_dp) --(xpart urcorner dlm_pct, -dlm_dp) --(xpart lrcorner dlm_pct, dlm_dp) --cycle; dlm_pct yscaled (dlm_len/(2*height dlm_pct)) endgroup fi enddef; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % Checking, building, freezing (very inefficient, to be improved) % % % 1. Global parameters % numeric min_clr_scl; % numeric prm_skp_scl; % numeric jdg_skp_scl; % numeric ilb_skp_scl; % numeric plb_skp_scl; % boolean drv_bot_roots; % boolean drv_boxmode_on; % boolean drv_fractionmode_on; % string drv_axis_ref; % % % 2. Macros % % % Checking % vardef fraction_inference[]= (prm_num[@]=0) and (iln_sty[@]=0) and (unknown l_ilb[@]) and (unknown r_ilb[@]) and drv_fractionmode_on enddef; vardef drv_check_root[]= if unknown jdg[@]: drv_errhelp "An index must be used to declare a both a judgment and an"& " inference."; drv_errmessage (decimal @)&" has been used as an inference index but not"& " as a judgment index"; elseif unknown prm_num[@]: drv_errhelp "An index must be used to declare a both a judgment and an"& " inference."; drv_errmessage (decimal @)&" has been used as a judgment index but not"& " as an inference index"; else: save i_sty, prm_idx; numeric i_sty, prm_idx; i_sty:=iln_sty[@]; for prm_rnk=0 upto prm_num[@]-1: prm_idx:=prm[@][prm_rnk]; drv_check_root[prm_idx]; % % numerators and denominators clearances % The TEXbook, Appendix G, Rule 15d. % if drv_bot_roots: num_hg:=max(num_hg, iln_hg[i_sty]+min_clr_scl*min_clr[drv_sty]-jdg[prm_idx].dp); else: den_dp:=min(den_dp, iln_dp[i_sty]-min_clr_scl*min_clr[drv_sty]-jdg[prm_idx].hg); fi endfor if not fraction_inference[@]: if drv_bot_roots: den_dp:=min(den_dp, iln_dp[i_sty]-min_clr_scl*min_clr[drv_sty]-jdg[@].hg); else: num_hg:=max(num_hg, iln_hg[i_sty]+min_clr_scl*min_clr[drv_sty]-jdg[@].dp); fi fi if unknown boxed[@]: boxed[@]:=false; fi fi enddef; vardef drv_check= if root_num=0: drv_errhelp "Well ..."; drv_errmessage "no inference has been declared"; else: save root_idx; numeric root_idx; root_idx:=root[0]; drv_check_root[root_idx]; if root_num>1: save root_str; string root_str; root_str:=decimal root_idx; for idx=1 upto root_num-1: root_idx:=root[idx]; drv_check_root[root_idx]; root_str:=root_str&", "&(decimal root_idx); endfor drv_message "warning, multiple root indices ("&root_str&")."; fi fi drv_checked:=true; enddef; % % Building % vardef drv_build_root[]= % % premises junction (from left to right) % for prm_rnk=0 upto prm_num[@]-1: drv_build_root[prm[@][prm_rnk]]; if prm_rnk>0: save ll_idx, lr_idx, rl_idx, rr_idx; save lmax_x, rmin_x, min_skp; numeric ll_idx, lr_idx, rl_idx, rr_idx; numeric lmax_x, rmin_x, min_skp; ypart jdg[prm[@][prm_rnk-1]].c=ypart jdg[prm[@][prm_rnk]].c; ll_idx:=prm[@][0]; lr_idx:=prm[@][prm_rnk-1]; rl_idx:=prm[@][prm_rnk]; rr_idx:=prm[@][prm_rnk]; lmax_x:=imax_x[lr_idx]; rmin_x:=imin_x[rl_idx]; min_skp[0]:=rmin_x-lmax_x; forever: exitif (unknown r_prm[lr_idx]) or (unknown l_prm[rl_idx]); ll_idx:=l_prm[ll_idx]; lr_idx:=r_prm[lr_idx]; rl_idx:=l_prm[rl_idx]; rr_idx:=r_prm[rr_idx]; lmax_x:=max(lmax_x, imax_x[lr_idx]); rmin_x:=min(rmin_x, imin_x[rl_idx]); min_skp[0]:=min(min_skp[0], imin_x[rl_idx]-imax_x[lr_idx]); endfor min_skp[1]:=rmin_x-lmax_x; if known r_prm[lr_idx]: r_prm[rr_idx]:= r_prm[lr_idx]; lmax_x:=smax_x[lr_idx]; elseif known l_prm[rl_idx]: l_prm[ll_idx]:=l_prm[rl_idx]; rmin_x:=smin_x[rl_idx]; fi min_skp[2]:=rmin_x-lmax_x; if jct_sty[@]<3: min_skp[jct_sty[@]]=prm_skp_scl*prm_skp[drv_sty]; fi fi endfor if prm_num[@]>0: l_prm[@]:=prm[@][0]; r_prm[@]:=prm[@][prm_num[@]-1]; fi % % judgment alignment % if prm_num[@]=0: imin_x[@]:=xpart jdg[@].l-jdg_skp_scl*jdg_skp[jdg_sty[drv_sty]]; imax_x[@]:=xpart jdg[@].r+jdg_skp_scl*jdg_skp[jdg_sty[drv_sty]]; else: save l_xref, r_xref; l_xref= if boxed[prm[@][0]]: smin_x[prm[@][0]] else: xpart jdg[prm[@][0]].l fi; r_xref= if boxed[prm[@][prm_num[@]-1]]: smax_x[prm[@][prm_num[@]-1]] else: xpart jdg[prm[@][prm_num[@]-1]].r fi; if alg_sty[@]="l": xpart jdg[@].l=l_xref; elseif alg_sty[@]="c": xpart jdg[@].c=(l_xref+r_xref)/2; elseif alg_sty[@]="r": xpart jdg[@].r=r_xref; fi imin_x[@]:=min(xpart jdg[@].l, l_xref) -jdg_skp_scl*jdg_skp[jdg_sty[drv_sty]]; imax_x[@]:=max(xpart jdg[@].r, r_xref) +jdg_skp_scl*jdg_skp[jdg_sty[drv_sty]]; fi % % inference line % save iln_wd, iln_pct; numeric iln_wd; picture iln_pct; iln_wd:=imax_x[@]-imin_x[@]; iln_pct:=((0, 0)--(iln_wd, 0)) drv_styled iln_sty[@]; setbounds iln_pct to (0, ypart llcorner iln_pct) --(0, ypart ulcorner iln_pct) --(iln_wd, ypart ulcorner iln_pct) --(iln_wd, ypart llcorner iln_pct) --cycle; % ! `linecap:=butt' and `linecap:=squared' -> same bounding box ! box_init iln[@] (iln_pct); xpart iln[@].c=(imin_x[@]+imax_x[@])/2; % % orientation, smin_y & smax_y % if drv_bot_roots: ypart iln[@].c=ypart jdg[@].c-den_dp; smin_y[@]:=ypart jdg[@].c+jdg[@].dp; smax_y[@]:= if iln_sty[@]=0: ypart jdg[@].c+jdg[@].hg else: ypart iln[@].c+iln[@].hg fi; if prm_num[@]>0: ypart iln[@].c=ypart jdg[prm[@][0]].c-num_hg; for prm_rnk=0 upto prm_num[@]-1: smax_y[@]:=max(smax_y[@], smax_y[prm[@][prm_rnk]]); endfor; fi else: ypart iln[@].c=ypart jdg[@].c-num_hg; smin_y[@]:= if iln_sty[@]=0: ypart jdg[@].c+jdg[@].dp else: ypart iln[@].c+iln[@].dp fi; smax_y[@]:=ypart jdg[@].c+jdg[@].hg; if prm_num[@]>0: ypart iln[@].c=ypart jdg[prm[@][0]].c-den_dp; for prm_rnk=0 upto prm_num[@]-1: smin_y[@]:=min(smin_y[@], smin_y[prm[@][prm_rnk]]); endfor; fi fi % % inference labels % if known l_ilb[@]: l_ilb[@].r=iln[@].l shifted (-ilb_skp_scl*ilb_skp[drv_sty], 0); imin_x[@]:=xpart l_ilb[@].l; smin_y[@]:=min(smin_y[@], ypart l_ilb[@].c+l_ilb[@].dp); smax_y[@]:=max(smax_y[@], ypart l_ilb[@].c+l_ilb[@].hg); fi if known r_ilb[@]: r_ilb[@].l=iln[@].r shifted (ilb_skp_scl*ilb_skp[drv_sty], 0); imax_x[@]:=xpart r_ilb[@].r; smin_y[@]:=min(smin_y[@], ypart r_ilb[@].c+r_ilb[@].dp); smax_y[@]:=max(smax_y[@], ypart r_ilb[@].c+r_ilb[@].hg); fi % % phantom steps % if known tgt[@]: save phm_pth, phm_pct; path phm_pth; picture phm_pct; save top_y, mid_y, bot_y; numeric top_y, bot_y; if drv_bot_roots: bot_y:=xpart minmax_y[@]+min_clr_scl*min_clr[drv_sty]/2; top_y:=xpart minmax_y[tgt[@]]; else: bot_y:=ypart minmax_y[tgt[@]]; top_y:=ypart minmax_y[@]-min_clr_scl*min_clr[drv_sty]/2; fi mid_y:=(top_y+bot_y)/2; phm_pth:=(0, (bot_y-top_y)/2)--(0, (top_y-bot_y)/2); phm_pct:=phm_pth drv_styled phm_sty[@]; box_init phm[@] (phm_pct shifted ((width phm_pct)/2, 0)); phm[@].c=(xpart jdg[@].c, mid_y); imin_x[@]:=min(imin_x[@], xpart phm[@].l); imax_x[@]:=max(imax_x[@], xpart phm[@].r); % % phantom steps labels % if known l_plb[@]: l_plb[@].r=phm[@].l shifted (-plb_skp[drv_sty], 0); imin_x[@]:=min(imin_x[@], xpart l_plb[@].l); fi if known r_plb[@]: r_plb[@].l=phm[@].r shifted ( plb_skp[drv_sty], 0); imax_x[@]:=max(imax_x[@], xpart r_plb[@].r); fi fi % % smin_x & smax_x % smin_x[@]:=imin_x[@]; smax_x[@]:=imax_x[@]; for prm_rnk=0 upto prm_num[@]-1: smin_x[@]:=min(smin_x[@], smin_x[prm[@][prm_rnk]]); smax_x[@]:=max(smax_x[@], smax_x[prm[@][prm_rnk]]); endfor % % delimiters % if known l_dlb[@] or known r_dlb[@]: save idx, mmy, min_y, max_y; numeric idx, min_y, max_y; pair mmy; mmy:=minmax_y[@]; min_y:=xpart mmy; max_y:=ypart mmy; if known l_dlb[@]: box_init l_dlm[@] (delim l (max_y-min_y)); l_dlm[@].r=(smin_x[@], (max_y+min_y)/2); l_dlb[@].r=l_dlm[@].l; smin_x[@]:=xpart l_dlb[@].l; fi if known r_dlb[@]: box_init r_dlm[@] (delim r (max_y-min_y)); r_dlm[@].l=(smax_x[@], (max_y+min_y)/2); r_dlb[@].l=r_dlm[@].r; smax_x[@]:=xpart r_dlb[@].r; fi fi if (known l_dlb[@]) or boxed[@]: idx:=@; forever: imin_x[idx]:=smin_x[@]; exitif unknown l_prm[idx]; idx:=l_prm[idx]; endfor fi if (known r_dlb[@]) or boxed[@]: idx:=@; forever: imax_x[idx]:=smax_x[@]; exitif unknown r_prm[idx]; idx:=r_prm[idx]; endfor fi enddef; vardef drv_build= if not drv_checked: drv_check; fi for idx=0 upto root_num-1: drv_build_root[root[idx]]; endfor drv_built:=true; enddef; % % Freezing % vardef drv_freeze_root[]= for prm_rnk=0 upto prm_num[@]-1: drv_freeze_root[prm[@][prm_rnk]]; endfor for sbj_rnk=0 upto sbj_num[@]-1: box_freeze sbj[@][sbj_rnk]; endfor forsuffixes sfx= iln, jdg, phm, l_dlb, l_dlm, l_ilb, l_plb, r_dlb, r_dlm, r_ilb, r_plb: if known sfx[@]: box_freeze sfx[@]; fi endfor enddef; vardef drv_freeze= if not drv_built: drv_build; fi save root_idx; numeric root_idx; root_idx:=root[0]; if unknown iln[root_idx].c: % % default math axis % if drv_axis_ref="iln": iln[root_idx].c=(0, axis_hg[drv_sty]); else: % drv_axis_ref="jdg" jdg[root_idx].c=(0, axis_hg[drv_sty]); fi drv_freeze_root[root_idx]; fi for idx=1 upto root_num-1: root_idx:=root[idx]; if unknown iln[root_idx].c: smin_x[root_idx]=smax_x[root[idx-1]]+prm_skp_scl*prm_skp[drv_sty]; ypart iln[root_idx].c=ypart iln[root[idx-1]].c; fi drv_freeze_root[root_idx]; endfor drv_frozen:=true; enddef; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % Derivation tree pictures % % % 1. Global parameters % boolean drv_proofmode_on; % color prf_clr; % color jdg_clr; % color sbj_clr; % prf_clr:=.75background; % arbitrary jdg_clr:=red; % arbitrary sbj_clr:=blue; % arbitrary % % 2. Macros % vardef drv_tree_addto @# (expr idx) text draw_options= for prm_rnk=0 upto prm_num[idx]-1: drv_tree_addto @# (prm[idx][prm_rnk]) draw_options; endfor forsuffixes sfx= jdg, phm, l_dlb, l_dlm, l_ilb, l_plb, r_dlb, r_dlm, r_ilb, r_plb: if known sfx[idx]: addto @# also sfx[idx] draw_options; fi endfor if iln_sty[idx]>0: addto @# also iln[idx] draw_options; fi enddef; vardef tt_nat[] expr nat= % typewriter typeface naturals save nat_aux, nat_pct_wd, dgt_num, nat_pct; numeric nat_aux, nat_pct_wd, dgt_num; picture nat_pct; nat_aux:=abs nat; nat_pct:=nullpicture; nat_pct_wd:=0; dgt_num:=1; forever: exitif nat_aux div (10**dgt_num)=0; dgt_num:=dgt_num+1; endfor for rnk:=1 upto dgt_num: addto nat_pct also tt_dgt[@][nat_aux div (10**(dgt_num-rnk))] shifted (nat_pct_wd, 0); nat_pct_wd:=width nat_pct; nat_aux:=nat_aux mod (10**(dgt_num-rnk)); endfor nat_pct shifted (0, -axis_hg[@]) enddef; vardef prf_tree_addto @# expr idx= for prm_rnk=0 upto prm_num[idx]-1: prf_tree_addto @# (prm[idx][prm_rnk]); endfor if idx>=0: box_init jdg_prf[idx] (tt_nat[2] idx); jdg_prf[idx].r=jdg[idx].l; box_freeze jdg_prf[idx]; addto @# also jdg_prf[idx] withcolor jdg_clr; addto @# doublepath jdg[idx].c withcolor jdg_clr withpen pencircle scaled (2*pdt_hg[drv_sty]); fi for sbj_rnk=0 upto sbj_num[idx]-1: box_init sbj_prf[idx][sbj_rnk] (tt_nat[3] sbj_rnk); if odd sbj_rnk: sbj_prf[idx][sbj_rnk].c shifted (0, sbj_prf[idx][sbj_rnk].hg)= sbj[idx][sbj_rnk].c shifted (0, -den_dp-min_clr_scl*min_clr[drv_sty]/2); else: sbj_prf[idx][sbj_rnk].c shifted (0, sbj_prf[idx][sbj_rnk].dp)= sbj[idx][sbj_rnk].c shifted (0, -num_hg+min_clr_scl*min_clr[drv_sty]/2); fi box_freeze sbj_prf[idx][sbj_rnk]; addto @# also sbj_prf[idx][sbj_rnk] withcolor sbj_clr; addto @# doublepath sbj[idx][sbj_rnk].c withcolor sbj_clr withpen pencircle scaled pdt_hg[drv_sty]; endfor enddef; vardef drv_tree= save pct; picture pct; pct:=nullpicture; if not drv_frozen: drv_freeze; fi for root_idx=0 upto root_num-1: if drv_proofmode_on: drv_tree_addto pct (root[root_idx]) withcolor prf_clr; prf_tree_addto pct (root[root_idx]); else: drv_tree_addto pct (root[root_idx]); fi endfor pct enddef; vardef drv_bbox[]= save min_x, max_x, mmy, min_y, max_y; pair mmy; numeric min_x, max_x, max_y, min_y; if not drv_frozen: drv_freeze; fi min_x:= if known l_dlm[@].r: xpart l_dlm[@].r else: smin_x[@] fi-jdg_skp_scl*jdg_skp[jdg_sty[drv_sty]]; max_x:= if known r_dlm[@].l: xpart l_dlm[@].l else: smax_x[@] fi+jdg_skp_scl*jdg_skp[jdg_sty[drv_sty]]; mmy:=minmax_y[@]; min_y:=xpart mmy; max_y:=ypart mmy; (min_x, min_y)-- (min_x, max_y)-- (max_x, max_y)-- (max_x, min_y)-- cycle enddef; vardef mth_axis @# (suffix ref_sfx) (expr idx)= if not drv_frozen: drv_freeze; fi if unknown prm_num[idx]: drv_errhelp "An index must be used to declare an inference before it is"& " used to set the math axis of a picture."; drv_errmessage "no inference has been declared using index "&(decimal idx); else: save ref_str, yref; string ref_str; numeric yref; ref_str:=str ref_sfx; if ref_str="iln": yref:=ypart iln[idx].c; elseif ref_str="jdg": yref:=ypart jdg[idx].c; elseif ref_str="dlm": if known l_dlm[idx]: yref:=ypart l_dlm[idx].c; elseif known r_dlm[idx]: yref:=ypart r_dlm[idx].c; else: drv_errhelp "Well ..."; drv_errmessage "no delimiter is attached to inference "&(decimal idx); fi else: drv_errhelp "Valid identifiers are"& " iln (inference line axis),"& " jdg (judgment math-axis) and"& " dlm (delimiter axis)."; drv_errmessage (ref_str&" is not a valid reference type identifier"); fi if known yref: @#:=@# shifted (0, axis_hg[drv_sty]-yref); fi fi enddef; vardef drv_axis (suffix ref) (expr idx)= mth_axis currentpicture (ref, idx); enddef; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % Tunings % vardef check_math_style (expr sty_str, default)= if sty_str="\displaystyle": 0 elseif sty_str="\textstyle": 1 elseif sty_str="\scriptstyle": 2 elseif sty_str="\scriptscriptstyle": 3 else: begingroup drv_errhelp "Valid commands are"& " \displaystyle,"& " \textstyle,"& " \scriptstyle and"& " \scriptscriptstyle."; drv_errmessage (sty_str&" is not a valid math-style command"); default endgroup fi enddef; vardef check_position_left (suffix pos_sfx) (expr default)= save pos_str; string pos_str; pos_str:=str pos_sfx; if (pos_str="l"): true elseif (pos_str="r"): false else: begingroup drv_errhelp "Valid identifiers are l (left) and r (right)."; drv_errmessage (pos_str&" is not a valid label position identifier"); default endgroup fi enddef; vardef check_mode_on (suffix status_sfx) (expr default)= save status_str; string status_str; status_str:=str status_sfx; if status_str="on": true elseif status_str="off": false else: begingroup drv_errhelp "Possible identifiers are on and off"; drv_errmessage (status_str&" is not a valid status identifier"); default endgroup fi enddef; vardef drv_math_style (suffix typ_sfx) (expr sty_str)= save typ_str, sty_idx; string typ_str; numeric sty_idx; typ_str:=str typ_sfx; if (typ_str<>"drv") and (typ_str<>"jdg") and (typ_str<>"ilb") and (typ_str<>"dlb") and (typ_str<>"plb"): drv_errhelp "Valid identifiers are"& " drv (derivation tree),"& " jdg (judgment),"& " ilb (inference label),"& " dlb (delimiter label) and"& " plb (phantom steps label)."; drv_errmessage (sty_str&" is not a valid component identifier"); else: sty_idx:=check_math_style (sty_str, 0); if typ_str="drv": drv_sty:=sty_idx; else: forsuffixes sfx=scantokens (typ_str&"_sty"): for idx=0 upto 3: sfx[idx]:=min(idx+sty_idx, 3); endfor endfor fi fi enddef; vardef drv_scale (suffix scl_sfx) (expr scl)= save scl_str; string scl_str; scl_str:=str scl_sfx; if scl_str="clr": min_clr_scl:=scl; elseif scl_str="prm": prm_skp_scl:=scl; elseif (scl_str="jdg") or (scl_str="jgm"): % "jgm" is deprecated jdg_skp_scl:=scl; elseif (scl_str="ilb") or (scl_str="lbl"): % "lbl" is deprecated ilb_skp_scl:=scl; else: drv_errhelp "Valid identifiers are"& " clr,"& " prm,"& " jdg and"& " ilb."; drv_errmessage (scl_str&" is not a valid scale identifier"); fi enddef; vardef drv_junction_style suffix sty_sfx= drv_jct_sty:=check_junction_style (sty_sfx, drv_jct_sty); enddef; vardef drv_alignment_style suffix sty_sfx= drv_alg_sty:=check_alignment_style (sty_sfx, drv_alg_sty); enddef; vardef drv_path_style (suffix typ_sfx, sty_sfx)= save typ_str; string typ_str; typ_str:=str typ_sfx; if typ_str="iln": drv_iln_sty:=check_path_style (sty_sfx, drv_iln_sty); elseif typ_str="phm": drv_phm_sty:=check_path_style (sty_sfx, drv_phm_sty); else: drv_errhelp "Valid identifiers are"& " iln (inference line) and"& " phm (phantom steps path)."; drv_errmessage (typ_str&" is not a valid path-type identifier"); fi enddef; vardef drv_labels_position_aux (suffix typ_sfx, pos_sfx)= save typ_str, idt_str, pos_str; string typ_str, idt_str, pos_str; typ_str:=str typ_sfx; if typ_str="ilb": drv_left_ilb:=check_position_left (pos_sfx, drv_left_ilb); elseif typ_str="dlb": drv_left_dlb:=check_position_left (pos_sfx, drv_left_dlb); elseif typ_str="plb": drv_left_plb:=check_position_left (pos_sfx, drv_left_plb); else: drv_errhelp "Valid identifiers are"& " ilb (inference label),"& " dlb (delimiter label) and"& " plb (phantom steps label)."; drv_errmessage (typ_str&" is not a valid label-type identifier"); fi enddef; vardef drv_labels_position text ARG= drv_labels_position_aux if pair ARG: ARG else: (ilb, ARG) fi; enddef; vardef drv_roots_position suffix pos_sfx= save pos_str; string pos_str; pos_str:=str pos_sfx; if pos_str="t": drv_bot_roots:=false; elseif pos_str="b": drv_bot_roots:=true; else: drv_errhelp "Valid identifiers are"& " t (top) and"& " b (bottom)."; drv_errmessage (pos_str&" is not a valid root position identifier"); fi enddef; vardef drv_axis_reference suffix ref_sfx= save ref_str; string ref_str; ref_str:=str ref_sfx; if (ref_str<>"iln") and (ref_str<>"jdg"): drv_errhelp "Valid identifiers are iln (inference line axis) and"& " jdg (judgment math-axis)."; drv_errmessage (ref_str&" is not a valid reference identifier"); else: drv_axis_ref:=ref_str; fi enddef; vardef drv_delimiter (suffix pos_sfx) (expr dlm_str)= if check_position_left (pos_sfx, true): drv_l_dlm:=dlm_str; else: drv_r_dlm:=dlm_str; fi enddef; vardef drv_left_delimiter expr dlm_str= drv_delimiter (l, dlm_str); enddef; vardef drv_right_delimiter expr dlm_str= drv_delimiter (r, dlm_str); enddef; vardef drv_box_mode suffix status_sfx= drv_boxmode_on:=check_mode_on (status_sfx, drv_boxmode_on); enddef; vardef drv_fraction_mode suffix status_sfx= drv_fractionmode_on:=check_mode_on (status_sfx, drv_fractionmode_on); enddef; vardef drv_proof_mode suffix status_sfx= drv_proofmode_on:=check_mode_on (status_sfx, drv_proofmode_on); enddef; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % Default settings % drv_font_size "\normalsize"; drv_math_style (drv, "\displaystyle"); drv_math_style (jdg, "\textstyle"); drv_math_style (ilb, "\scriptstyle"); drv_math_style (dlb, "\textstyle"); drv_math_style (plb, "\textstyle"); drv_scale (clr, 1); drv_scale (prm, 1); drv_scale (jdg, 1); drv_scale (ilb, 1); drv_junction_style 1; drv_alignment_style c; drv_path_style (iln, 1); drv_path_style (phm, 3); drv_labels_position (ilb, r); drv_labels_position (dlb, l); drv_labels_position (plb, l); drv_roots_position b; drv_axis_reference iln; drv_left_delimiter "\lbrace"; drv_right_delimiter "\rbrace"; drv_box_mode off; drv_fraction_mode on; drv_proof_mode off; %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % LaTeX inclusion macro % % \drv includes a picture file in such a way that the baseline of the included % picture coincides with the baseline of the inclusion point. The code for \drv % was suggested by Josselin Noirel on the fr.comp.text.tex usenet group. % % \usepackage{graphicx} % \makeatletter % \def\Gin@def@bp#1\relax#2#3{\gdef#2{#3}} % \newsavebox{\graphicsbox} % \newcommand*{\drv}[1]{% % \sbox{\graphicsbox}{\includegraphics{#1}}% % \raisebox{\Gin@lly bp}% % {\usebox{\graphicsbox}}} % \makeatother