summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/metapost/drv/drv.mp
diff options
context:
space:
mode:
Diffstat (limited to 'Master/texmf-dist/metapost/drv/drv.mp')
-rw-r--r--Master/texmf-dist/metapost/drv/drv.mp2245
1 files changed, 2245 insertions, 0 deletions
diff --git a/Master/texmf-dist/metapost/drv/drv.mp b/Master/texmf-dist/metapost/drv/drv.mp
new file mode 100644
index 00000000000..5eb38396144
--- /dev/null
+++ b/Master/texmf-dist/metapost/drv/drv.mp
@@ -0,0 +1,2245 @@
+%% 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.
+% <laurent.mehats@gmail.com>
+%
+% This work consists of the file drv.mp
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% User's macros summary
+%
+%
+% * Judgment & inference declarations
+% ===================================
+%
+% jgm <nat> <str list>
+% <nat> judgment index
+% <str list> sub-judgments math-mode LaTeX code
+%
+% nfr <nat> (<nat list>) (<str>, <id>)
+% <nat> inference index
+% <nat list> list of premise indices
+% <str> inference label math-mode LaTeX code
+% <id> 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 <nat 1> (<nat 2>, <id>)
+% <nat 1> index of the origin judgment
+% <nat 2> number of phantom steps
+% <id> phantom steps path-style identifier
+% (0, 1, 2, 3, 4, 5, 6 or _)
+%
+% Nfr <nat> (<nat list>) (<str 1>, <str 2>, <str 3>, <id>)
+% <nat> inference index
+% <nat list> list of premise indices
+% <str 1> inference label math-mode LaTeX code
+% <str 2> left delimiter label math-mode LaTeX code
+% <str 3> right delimiter label math-mode LaTeX code
+% <id> inference line style identifier
+% (0, 1, 2, 3, 4, 5, 6 or _)
+%
+% Mvd <nat 1> (<nat 2>, <str 1>, <str 2>, <id>)
+% <nat 1> index of the origin judgment
+% <nat 2> number of phantom steps
+% <str 1> left label math-mode LaTeX code
+% <str 2> right label math-mode LaTeX code
+% <id> phantom steps path-style identifier
+% (0, 1, 2, 3, 4, 5, 6 or _)
+%
+% NFR <nat> (<nat list>) (<str 1>, <str 2>, <str 3>, <str 4>)
+% (<id 1>, <id 2>, <id 3>)
+% <nat> inference index
+% <nat list> list of premise indices
+% <str 1> left inference label math-mode LaTeX code
+% <str 2> right inference label math-mode LaTeX code
+% <str 3> left delimiter label math-mode LaTeX code
+% <str 4> right delimiter label math-mode LaTeX code
+% <id 1> 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)
+% <id 2> alignment style identifier (l, c, r, u or _)
+% l left
+% c centered
+% r right
+% u user specified (tricky)
+% _ default (set by drv_alignment_style)
+% <id 3> inference line style identifier
+% (0, 1, 2, 3, 4, 5, 6 or _)
+%
+% MVD <nat 1> (<nat 2>, <str 1>, <str 2>, <id 1> <id 2>)
+% <nat 1> index of the origin judgment
+% <nat 2> number of phantom steps
+% <str 1> left label math-mode LaTeX code
+% <str 2> right label math-mode LaTeX code
+% <id 1> alignment style identifier (l, c, r, u or _)
+% <id 2> phantom steps path-style identifier
+% (0, 1, 2, 3, 4, 5, 6 or _)
+%
+% NFR_opt <nat> (<nat list>) (<str list 1>) (<str list 2>)
+% (<id 1>, <id 2>, <id 3>)
+% <nat> inference index
+% <nat list> list of premise indices
+% <str list 1> list of inference labels math-mode LaTeX code
+% <str list 2> list of delimiter labels math-mode LaTeX code
+% <id 1> junction style identifier (0, 1, 2, 3 or _)
+% <id 2> alignment style identifier (l, c, r, u or _)
+% <id 3> inference line style identifier
+% (0, 1, 2, 3, 4, 5, 6 or _)
+%
+% MVD_opt <nat 1> (<nat 2>) (<str list>) (<id 1> <id 2>)
+% <nat 1> index of the origin judgment
+% <nat 2> number of phantom steps
+% <str list> list of labels math-mode LaTeX code
+% <id 1> alignment style identifier (l, c, r or u)
+% <id 2> phantom steps path-style identifier
+% (0, 1, 2, 3, 4, 5, 6 or _)
+%
+% * Tunings
+% =========
+%
+% drv_font_size <str>
+% <str> LaTeX font-size command
+% "\tiny"
+% "\scriptsize"
+% "\footnotesize"
+% "\small"
+% "\normalsize"
+% "\large"
+% "\Large"
+% etc.
+%
+% drv_math_style (<id>, <str>)
+% <id> component identifier (drv, jdg, ilb, dlb or plb)
+% drv derivation trees
+% jdg judgments
+% ilb inference labels
+% dlb delimiter labels
+% plb phantom steps labels
+% <str> LaTeX math-style command
+%
+% drv_scale (<id>, <float>)
+% <id> 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)
+% <float> scale value
+%
+% drv_junction_style <id>
+% <id> junction style identifier (0, 1 or 2)
+% 0 ``fully-interlacing''
+% 1 ``semi-interlacing''
+% 2 ``non-interlacing''
+%
+% drv_alignment_style <id>
+% <id> alignment style identifier (l, c or r)
+% l left
+% c centered
+% r right
+%
+% drv_path_style (<id 1>, <id 2>)
+% <id 1> path-type identifier (iln or phm)
+% iln inference lines
+% phm phantom steps paths
+% <id 2> path-style identifier (0, 1, 2, 3, 4, 5 or 6)
+%
+% drv_labels_position (<id 1>, <id 2>)
+% <id 1> label-type identifier (ilb, plb or dlb)
+% ilb inference labels
+% dlb delimiter labels
+% plb phantom steps labels
+% <id 2> position identifier (l or r)
+% l left
+% r right
+%
+% drv_roots_position <id>
+% <id> position identifier (t or b)
+% t top
+% b bottom
+%
+% drv_axis_reference <id>
+% <id> reference identifier (iln or jdg)
+% iln root inference line axis
+% jdg root judgment math-axis
+%
+% drv_left_delimiter <str>
+% <str> left delimiter math-mode LaTeX code
+% "(" $($
+% "[" $[$
+% "\lbrace" $\lbrace$
+% "\langle" $\langle$
+% etc.
+%
+% drv_right_delimiter <str>
+% <str> right delimiter math-mode LaTeX code
+% ")"
+% "]"
+% "\rbrace"
+% "\rangle"
+% etc.
+%
+% drv_box_mode <id>
+% <id> status identifier (on or off)
+% on
+% off
+%
+% drv_fraction_mode <id>
+% <id> status identifier (on or off)
+% on
+% off
+%
+% drv_proof_mode <id>
+% <id> status identifier (on or off)
+% on
+% off
+%
+% * Derivation tree pictures
+% ==========================
+%
+% drv_bbox <nat>
+% <nat> sub-tree root index
+%
+% drv_axis (<id>, <nat>)
+% <id> reference type identifier (iln, jdg or dlm)
+% iln inference line axis
+% jdg judgment math-axis
+% dlm delimiter axis
+% <nat> reference index
+%
+% <path> drv_styled <id>
+% <path> MetaPost path expression
+% <id> 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] <nice explanation>
+% jdg_skp[s] <nice explanation>
+% ilb_skp[s] <nice explanation>
+% plb_skp[s] <nice explanation>
+%
+
+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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-06 11:22:35 +0000