# HG changeset patch # User ryokka # Date 1508920536 -32400 # Node ID ead50a89470f62e2b2e568c3f7bf8e6e79b52746 # Parent d12b2800af6a651b8b5473e726b71f6f9e5c1c38 fix midterm diff -r d12b2800af6a -r ead50a89470f midterm/bussproofs.sty --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/bussproofs.sty Wed Oct 25 17:35:36 2017 +0900 @@ -0,0 +1,1136 @@ +% +\def\BPmessage{Proof Tree (bussproofs) style macros. Version 1.1.} +% bussproofs.sty. Version 1.1 +% (c) 1994,1995,1996,2004,2005,2006, 2011. +% Copyright retained by Samuel R. Buss. +% +% ==== Legal statement: ==== +% 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/1 or later. +% +% This work has the LPPL maintenance status 'maintained'. +% +% The Current Maintainer of the work is Sam Buss. +% +% This work consists of bussproofs.sty. +% ===== +% Informal summary of legal situation: +% This software may be used and distributed freely, except that +% if you make changes, you must change the file name to be different +% than bussproofs.sty to avoid compatibility problems. +% The terms of the LaTeX Public License are the legally controlling terms +% and override any contradictory terms of the "informal situation". +% +% Please report comments and bugs to sbuss@ucsd.edu. +% +% Thanks to Felix Joachimski for making changes to let these macros +% work in plain TeX in addition to LaTeX. Nothing has been done +% to see if they work in AMSTeX. The comments below mostly +% are written for LaTeX, however. +% July 2004, version 0.7 +% - bug fix, right labels with descenders inserted too much space. +% Thanks to Peter Smith for finding this bug, +% see http://www.phil.cam.ac.uk/teaching_staff/Smith/LaTeX/ +% March 2005, version 0.8. +% Added a default definition for \fCenter at Denis Kosygin's +% suggestion. +% September 2005, version 0.9. +% Fixed some subtle spacing problems, by adding %'s to the end of +% few lines where they were inadvertantly omitted. Thanks to +% Arnold Beckmann for finding and fixing this problem. +% April 2006, version 0.9.1. Updated comments and testbp2.tex file. +% No change to the actual macros. +% June 2006, version 1.0. The first integer numbered release. +% New feature: root of proof may now be at the bottom instead of +% at just the top. Thanks to Alex Hertel for the suggestion to implement +% this. +% June 2011, version 1.1. +% New feature: 4-ary and 5-ary inferences. Thanks to Thomas Strathmann +% for taking the initiative to implement these. +% Four new commands: QuaternaryInf(C) and QuinaryInf(C). +% Bug fix: \insertBetweenHyps now works for proofs with root at top and +% three or more hypotheses.. + +% A good exposition of how to use bussproofs.sty (version 0.9) has been written +% by Peter Smith and is available on the internet. +% The comments below also describe the features of bussproofs.sty, +% including user-modifiable parameters. + +% bussproofs.sty allows the construction of proof trees in the +% style of the sequent calculus and many other proof systems +% One novel feature of these macros is they support the horizontal +% alignment according to some center point specified with the +% command \fCenter. This is the style often used in sequent +% calculus proofs. +% Proofs are specified in left-to-right traversal order. +% For example a proof +% A B +% ----- +% D C +% --------- +% E +% +% if given in the order D,A,B,C,E. Each line in the proof is +% specified according to the arity of the inference which generates +% it. Thus, E would be specified with a \BinaryInf or \BinaryInfC +% command. +% +% The above proof tree could be displayed with the commands: +% +% \AxiomC{D} +% \AxiomC{A} +% \AxiomC{B} +% \BinaryInfC{C} +% \BinaryInfC{E} +% \DisplayProof +% +% Inferences in a proof may be nullary (axioms), unary, binary, or +% trinary. +% +% IMPORTANT: You must give the \DisplayProof command to make the proof +% be printed. To display a centered proof on a line by itself, +% put the proof inside \begin{center} ... \end{center}. +% +% There are two styles for specifying horizontal centering of +% lines (formulas or sequents) in a proof. One format \AxiomC{...} +% just centers the formula {...} in the usual way. The other +% format is \Axiom$...\fCenter...$. Here, the \fCenter specifies +% the center of the formula. (It is permissable for \fCenter to +% generate typeset material; in fact, I usually define it to generate +% the sequent arrow.) In unary inferences, the \fCenter +% positions will be vertically aligned in the upper and lower lines of +% the inference. Unary, Binary, Trinary inferences are specified +% with the same format as Axioms. The two styles of centering +% lines may be combined in a single proof. +% +% By using the optional \EnableBpAbbreviations command, various +% abbreviated two or three letter commands are enabled. This allows, +% in particular: +% \AX and \AXC for \Axiom and \AxiomC, (resp.), +% \DP for \DisplayProof, +% \BI and \BIC for \BinaryInf and \BinaryInfC, +% \UI and \UIC for \UnaryInf and \UnaryInfC, +% \TI and \TIC for \TrinaryInf and \TrinaryInfC, +% \LL and \RL for \LeftLabel and \RightLabel. +% See the source code below for additional abbreviations. +% The enabling of these short abbreviations is OPTIONAL, since +% there is the possibility of conflicting with names from other +% macro packages. +% +% By default, the inferences have single horizontal lines (scores) +% This can be overridden using the \doubleLine, \noLine commands. +% These two commands affect only the next inference. You can make +% make a permanent override that applies to the rest of the current +% proof using \alwaysDoubleLine and \alwaysNoLine. \singleLine +% and \alwaysSingleLine work in the analogous way. +% +% The macros do their best to give good placements of for the +% parts of the proof. Several macros allow you to override the +% defaults. These are \insertBetweenHyps{...} which overrides +% the default spacing between hypotheses of Binary and Trinary +% inferences with {...}. And \kernHyps{...} specifies a distance +% to shift the whole block of hypotheses to the right (modifying +% the default center position. +% Other macros set the vertical placement of the whole proof. +% The default is to try to do a good job of placement for inferences +% included in text. Two other useful macros are: \bottomAlignProof +% which aligns the hbox output by \DisplayProof according to the base +% of the bottom line of the proof, and \centerAlignProof which +% does a precise center vertical alignment. +% +% Often, one wishes to place a label next to an inference, usually +% to specify the type of inference. These labels can be placed +% by using the commands \LeftLabel{...} and \RightLabel{...} +% immediately before the command which specifies the inference. +% For example, to generate +% +% A B +% --------- X +% C +% +% use the commands +% \AxiomC{A} +% \AxiomC{B} +% \RightLabel{X} +% \BinaryInfC{C} +% \DisplayProof +% +% The \DisplayProof command just displays the proof as a text +% item. This allows you to put proofs anywhere normal text +% might appear; for example, in a paragraph, in a table, in +% a tabbing environment, etc. When displaying a proof as inline text, +% you should write \DisplayProof{} (with curly brackets) so that +% LaTeX will not "eat" the white space following the \DisplayProof +% command. +% For displaying proofs in a centered display: Do not use the \[...\] +% construction (nor $$...$$). Instead use +% \begin{center} ... \DisplayProof\end{center}. +% Actually there is a better construction to use instead of the +% \begin{center}...\DisplayProof\end{center}. This is to +% write +% \begin{prooftree} ... \end{prooftree}. +% Note there is no \DisplayProof used for this: the +% \end{prooftree} automatically supplies the \DisplayProof +% command. +% +% Warning: Any commands that set line types or set vertical or +% horizontal alignment that are given AFTER the \DisplayProof +% command will affect the next proof, no matter how distant. + + + + +% Usages: +% ======= +% +% \Axiom$\fCenter$ +% +% \AxiomC{\fCenter$ +% +% \UnaryInfC{} +% +% \BinaryInf$\fCenter$ +% +% \BinaryInfC{} +% +% \TrinaryInf$\fCenter$ +% +% \TrinaryInfC{} +% +% \QuaternaryInf$\fCenter$ +% +% \QuaternaryInfC{} +% +% \QuinaryInf$\fCenter$ +% +% \QuinaryInfC{} +% +% \LeftLabel{} - Puts as a label to the left +% of the next inference line. (Works even if +% \noLine is used too.) +% +% \RightLabel{} - Puts as a label to the right of the +% next inference line. (Also works with \noLine.) +% +% \DisplayProof - outputs the whole proof tree (and finishes it). +% The proof tree is output as an hbox. +% +% +% \kernHyps{} - Slides the upper hypotheses right distance +% (This is similar to shifting conclusion left) +% - kernHyps works with Unary, Binary and Trinary +% inferences and with centered or uncentered sequents. +% - Negative values for are permitted. +% +% \insertBetweenHyps{...} - {...} will be inserted between the upper +% hypotheses of a Binary or Trinary Inferences. +% It is possible to use negative horizontal space +% to push them closer together (and even overlap). +% This command affects only the next inference. +% +% \doubleLine - Makes the current (ie, next) horizontal line doubled +% +% \alwaysDoubleLine - Makes lines doubled for rest of proof +% +% \singleLine - Makes the current (ie, next) line single +% +% \alwaysSingleLine - Undoes \alwaysDoubleLine or \alwaysNoLine. +% +% \noLine - Make no line at all at current (ie next) inference. +% +% \alwaysNoLine - Makes no lines for rest of proof. (Untested) +% +% \solidLine - Does solid horizontal line for current inference +% +% \dottedLine - Does dotted horizontal line for current inference +% +% \dashedLine - Does dashed horizontal line for current inference +% +% \alwaysSolidLine - Makes the indicated change in line type, permanently +% \alwaysDashedLine until end of proof or until overridden. +% \alwaysDottedLine +% +% \bottomAlignProof - Vertically align proof according to its bottom line. +% \centerAlignProof - Vertically align proof proof precisely in its center. +% \normalAlignProof - Overrides earlier bottom/center AlignProof commands. +% The default alignment will look good in most cases, +% whether the proof is displayed or is +% in-line. Other alignments may be more +% appropriate when putting proofs in tables or +% pictures, etc. For custom alignments, use +% TeX's raise commands. +% +% \rootAtTop - specifies that proofs have their root a the top. That it, +% proofs will be "upside down". +% \rootAtBottom - (default) Specifies that proofs have root at the bottom +% The \rootAtTop and \rootAtBottom commands apply *only* to the +% current proof. If you want to make them persistent, use one of +% the next two commands: +% \alwaysRootAtTop +% \alwaysRootAtBottom (default) +% + +% Optional short abbreviations for commands: +\def\EnableBpAbbreviations{% + \let\AX\Axiom + \let\AXC\AxiomC + \let\UI\UnaryInf + \let\UIC\UnaryInfC + \let\BI\BinaryInf + \let\BIC\BinaryInfC + \let\TI\TrinaryInf + \let\TIC\TrinaryInfC + \let\QI\QuaternaryInf + \let\QIC\QuaternaryInfC + \let\QuI\QuinaryInf + \let\QuIC\QuinaryInfC + \let\LL\LeftLabel + \let\RL\RightLabel + \let\DP\DisplayProof +} + +% Parameters which control the style of the proof trees. +% The user may wish to override these parameters locally or globally. +% BUT DON'T CHANGE THE PARAMETERS BY CHANGING THIS FILE (to avoid +% future incompatibilities). Instead, you should change them in your +% TeX document right after including this style file in the +% header material of your LaTeX document. + +\def\ScoreOverhang{4pt} % How much underlines extend out +\def\ScoreOverhangLeft{\ScoreOverhang} +\def\ScoreOverhangRight{\ScoreOverhang} + +\def\extraVskip{2pt} % Extra space above and below lines +\def\ruleScoreFiller{\hrule} % Horizontal rule filler. +\def\dottedScoreFiller{\hbox to4pt{\hss.\hss}} +\def\dashedScoreFiller{\hbox to2.8mm{\hss\vrule width1.4mm height0.4pt depth0.0pt\hss}} +\def\defaultScoreFiller{\ruleScoreFiller} % Default horizontal filler. +\def\defaultBuildScore{\buildSingleScore} % In \singleLine mode at start. + +\def\defaultHypSeparation{\hskip.2in} % Used if \insertBetweenHyps isn't given + +\def\labelSpacing{3pt} % Horizontal space separating labels and lines + +\def\proofSkipAmount{\vskip.8ex plus.8ex minus.4ex} + % Space above and below a prooftree display. + +\def\defaultRootPosition{\buildRootBottom} % Default: Proofs root at bottom +%\def\defaultRootPosition{\buildRootTop} % Makes all proofs upside down + +\ifx\fCenter\undefined +\def\fCenter{\relax} +\fi + +% +% End of user-modifiable parameters. +% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% Here are some internal paramenters and defaults. Not really intended +% to be user-modifiable. + +\def\theHypSeparation{\defaultHypSeparation} +\def\alwaysScoreFiller{\defaultScoreFiller} % Horizontal filler. +\def\alwaysBuildScore{\defaultBuildScore} +\def\theScoreFiller{\alwaysScoreFiller} % Horizontal filler. +\def\buildScore{\alwaysBuildScore} %This command builds the score. +\def\hypKernAmt{0pt} % Initial setting for kerning the hypotheses. + +\def\defaultLeftLabel{} +\def\defaultRightLabel{} + +\def\myTrue{Y} +\def\bottomAlignFlag{N} +\def\centerAlignFlag{N} +\def\defaultRootAtBottomFlag{Y} +\def\rootAtBottomFlag{Y} + +% End of internal parameters and defaults. + +\expandafter\ifx\csname newenvironment\endcsname\relax% +% If in TeX: +\message{\BPmessage} +\def\makeatletter{\catcode`\@=11\relax} +\def\makeatother{\catcode`\@=12\relax} +\makeatletter +\def\newcount{\alloc@0\count\countdef\insc@unt} +\def\newdimen{\alloc@1\dimen\dimendef\insc@unt} +\def\newskip{\alloc@2\skip\skipdef\insc@unt} +\def\newbox{\alloc@4\box\chardef\insc@unt} +\makeatother +\else +% If in LaTeX +\typeout{\BPmessage} +\newenvironment{prooftree}% +{\begin{center}\proofSkipAmount \leavevmode}% +{\DisplayProof \proofSkipAmount \end{center} } +\fi + +\def\thecur#1{\csname#1\number\theLevel\endcsname} + +\newcount\theLevel % This counter is the height of the stack. +\global\theLevel=0 % Initialized to zero +\newcount\myMaxLevel +\global\myMaxLevel=0 +\newbox\myBoxA % Temporary storage boxes +\newbox\myBoxB +\newbox\myBoxC +\newbox\myBoxD +\newbox\myBoxLL % Boxes for the left label and the right label. +\newbox\myBoxRL +\newdimen\thisAboveSkip %Internal use: amount to skip above line +\newdimen\thisBelowSkip %Internal use: amount to skip below line +\newdimen\newScoreStart % More temporary storage. +\newdimen\newScoreEnd +\newdimen\newCenter +\newdimen\displace +\newdimen\leftLowerAmt% Amount to lower left label +\newdimen\rightLowerAmt% Amount to lower right label +\newdimen\scoreHeight% Score height +\newdimen\scoreDepth% Score Depth +\newdimen\htLbox% +\newdimen\htRbox% +\newdimen\htRRbox% +\newdimen\htRRRbox% +\newdimen\htAbox% +\newdimen\htCbox% + +\setbox\myBoxLL=\hbox{\defaultLeftLabel}% +\setbox\myBoxRL=\hbox{\defaultRightLabel}% + +\def\allocatemore{% + \ifnum\theLevel>\myMaxLevel% + \expandafter\newbox\curBox% + \expandafter\newdimen\curScoreStart% + \expandafter\newdimen\curCenter% + \expandafter\newdimen\curScoreEnd% + \global\advance\myMaxLevel by1% + \fi% +} + +\def\prepAxiom{% + \advance\theLevel by1% + \edef\curBox{\thecur{myBox}}% + \edef\curScoreStart{\thecur{myScoreStart}}% + \edef\curCenter{\thecur{myCenter}}% + \edef\curScoreEnd{\thecur{myScoreEnd}}% + \allocatemore% +} + +\def\Axiom$#1\fCenter#2${% + % Get level and correct names set. + \prepAxiom% + % Define the boxes + \setbox\myBoxA=\hbox{$\mathord{#1}\fCenter\mathord{\relax}$}% + \setbox\myBoxB=\hbox{$#2$}% + \global\setbox\curBox=% + \hbox{\hskip\ScoreOverhangLeft\relax% + \unhcopy\myBoxA\unhcopy\myBoxB\hskip\ScoreOverhangRight\relax}% + % Set the relevant dimensions for the boxes + \global\curScoreStart=0pt \relax + \global\curScoreEnd=\wd\curBox \relax + \global\curCenter=\wd\myBoxA \relax + \global\advance \curCenter by \ScoreOverhangLeft% + \ignorespaces +} + +\def\AxiomC#1{ % Note argument not in math mode + % Get level and correct names set. + \prepAxiom% + % Define the box. + \setbox\myBoxA=\hbox{#1}% + \global\setbox\curBox =% + \hbox{\hskip\ScoreOverhangLeft\relax% + \unhcopy\myBoxA\hskip\ScoreOverhangRight\relax}% + % Set the relevant dimensions for the boxes + \global\curScoreStart=0pt \relax + \global\curScoreEnd=\wd\curBox \relax + \global\curCenter=.5\wd\curBox \relax + \global\advance \curCenter by \ScoreOverhangLeft% + \ignorespaces +} + +\def\prepUnary{% + \ifnum \theLevel<1 + \errmessage{Hypotheses missing!} + \fi% + \edef\curBox{\thecur{myBox}}% + \edef\curScoreStart{\thecur{myScoreStart}}% + \edef\curCenter{\thecur{myCenter}}% + \edef\curScoreEnd{\thecur{myScoreEnd}}% +} + +\def\UnaryInf$#1\fCenter#2${% + \prepUnary% + \buildConclusion{#1}{#2}% + \joinUnary% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\UnaryInfC#1{ + \prepUnary% + \buildConclusionC{#1}% + %Align and join the curBox and the new box into one vbox. + \joinUnary% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\prepBinary{% + \ifnum\theLevel<2 + \errmessage{Hypotheses missing!} + \fi% + \edef\rcurBox{\thecur{myBox}}% Set up names of right hypothesis + \edef\rcurScoreStart{\thecur{myScoreStart}}% + \edef\rcurCenter{\thecur{myCenter}}% + \edef\rcurScoreEnd{\thecur{myScoreEnd}}% + \advance\theLevel by-1% + \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis + \edef\lcurScoreStart{\thecur{myScoreStart}}% + \edef\lcurCenter{\thecur{myCenter}}% + \edef\lcurScoreEnd{\thecur{myScoreEnd}}% +} + +\def\BinaryInf$#1\fCenter#2${% + \prepBinary% + \buildConclusion{#1}{#2}% + \joinBinary% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\BinaryInfC#1{% + \prepBinary% + \buildConclusionC{#1}% + \joinBinary% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\prepTrinary{% + \ifnum\theLevel<3 + \errmessage{Hypotheses missing!} + \fi% + \edef\rcurBox{\thecur{myBox}}% Set up names of right hypothesis + \edef\rcurScoreStart{\thecur{myScoreStart}}% + \edef\rcurCenter{\thecur{myCenter}}% + \edef\rcurScoreEnd{\thecur{myScoreEnd}}% + \advance\theLevel by-1% + \edef\ccurBox{\thecur{myBox}}% Set up names of center hypothesis + \edef\ccurScoreStart{\thecur{myScoreStart}}% + \edef\ccurCenter{\thecur{myCenter}}% + \edef\ccurScoreEnd{\thecur{myScoreEnd}}% + \advance\theLevel by-1% + \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis + \edef\lcurScoreStart{\thecur{myScoreStart}}% + \edef\lcurCenter{\thecur{myCenter}}% + \edef\lcurScoreEnd{\thecur{myScoreEnd}}% +} + +\def\TrinaryInf$#1\fCenter#2${% + \prepTrinary% + \buildConclusion{#1}{#2}% + \joinTrinary% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\TrinaryInfC#1{% + \prepTrinary% + \buildConclusionC{#1}% + \joinTrinary% + \resetInferenceDefaults% + \ignorespaces% +} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\def\prepQuaternary{% + \ifnum\theLevel<4 + \errmessage{Hypotheses missing!} + \fi% + \edef\rrcurBox{\thecur{myBox}}% Set up names of very right hypothesis + \edef\rrcurScoreStart{\thecur{myScoreStart}}% + \edef\rrcurCenter{\thecur{myCenter}}% + \edef\rrcurScoreEnd{\thecur{myScoreEnd}}% + \advance\theLevel by-1% + \edef\rcurBox{\thecur{myBox}}% Set up names of right hypothesis + \edef\rcurScoreStart{\thecur{myScoreStart}}% + \edef\rcurCenter{\thecur{myCenter}}% + \edef\rcurScoreEnd{\thecur{myScoreEnd}}% + \advance\theLevel by-1% + \edef\ccurBox{\thecur{myBox}}% Set up names of center hypothesis + \edef\ccurScoreStart{\thecur{myScoreStart}}% + \edef\ccurCenter{\thecur{myCenter}}% + \edef\ccurScoreEnd{\thecur{myScoreEnd}}% + \advance\theLevel by-1% + \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis + \edef\lcurScoreStart{\thecur{myScoreStart}}% + \edef\lcurCenter{\thecur{myCenter}}% + \edef\lcurScoreEnd{\thecur{myScoreEnd}}% +} + +\def\QuaternaryInf$#1\fCenter#2${% + \prepQuaternary% + \buildConclusion{#1}{#2}% + \joinQuaternary% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\QuaternaryInfC#1{% + \prepQuaternary% + \buildConclusionC{#1}% + \joinQuaternary% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\joinQuaternary{% Construct the quarterary inference into a vbox. + % Join the four hypotheses's boxes into one hbox. + \setbox\myBoxA=\hbox{\theHypSeparation}% + \lcurScoreEnd=\rrcurScoreEnd% + \advance\lcurScoreEnd by\wd\rcurBox% + \advance\lcurScoreEnd by\wd\lcurBox% + \advance\lcurScoreEnd by\wd\ccurBox% + \advance\lcurScoreEnd by3\wd\myBoxA% + \displace=\lcurScoreEnd% + \advance\displace by -\lcurScoreStart% + \lcurCenter=.5\displace% + \advance\lcurCenter by\lcurScoreStart% + \ifx\rootAtBottomFlag\myTrue% + \setbox\lcurBox=% + \hbox{\box\lcurBox\unhcopy\myBoxA\box\ccurBox% + \unhcopy\myBoxA\box\rcurBox + \unhcopy\myBoxA\box\rrcurBox}% + \else% + \htLbox = \ht\lcurBox% + \htAbox = \ht\myBoxA% + \htCbox = \ht\ccurBox% + \htRbox = \ht\rcurBox% + \htRRbox = \ht\rrcurBox% + \setbox\lcurBox=% + \hbox{\lower\htLbox\box\lcurBox% + \lower\htAbox\copy\myBoxA\lower\htCbox\box\ccurBox% + \lower\htAbox\copy\myBoxA\lower\htRbox\box\rcurBox% + \lower\htAbox\copy\myBoxA\lower\htRRbox\box\rrcurBox}% + \fi% + % Adjust center of upper hypotheses according to how much + % the lower sequent is off-center. + \displace=\newCenter% + \advance\displace by -.5\newScoreStart% + \advance\displace by -.5\newScoreEnd% + \advance\lcurCenter by \displace% + %Align and join the curBox and the two hypotheses's box into one vbox. + \edef\curBox{\lcurBox}% + \edef\curScoreStart{\lcurScoreStart}% + \edef\curScoreEnd{\lcurScoreEnd}% + \edef\curCenter{\lcurCenter}% + \joinUnary% +} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\def\prepQuinary{% + \ifnum\theLevel<5 + \errmessage{Hypotheses missing!} + \fi% + \edef\rrrcurBox{\thecur{myBox}}% Set up names of very very right hypothesis + \edef\rrrcurScoreStart{\thecur{myScoreStart}}% + \edef\rrrcurCenter{\thecur{myCenter}}% + \edef\rrrcurScoreEnd{\thecur{myScoreEnd}}% + \advance\theLevel by-1% + \edef\rrcurBox{\thecur{myBox}}% Set up names of very right hypothesis + \edef\rrcurScoreStart{\thecur{myScoreStart}}% + \edef\rrcurCenter{\thecur{myCenter}}% + \edef\rrcurScoreEnd{\thecur{myScoreEnd}}% + \advance\theLevel by-1% + \edef\rcurBox{\thecur{myBox}}% Set up names of right hypothesis + \edef\rcurScoreStart{\thecur{myScoreStart}}% + \edef\rcurCenter{\thecur{myCenter}}% + \edef\rcurScoreEnd{\thecur{myScoreEnd}}% + \advance\theLevel by-1% + \edef\ccurBox{\thecur{myBox}}% Set up names of center hypothesis + \edef\ccurScoreStart{\thecur{myScoreStart}}% + \edef\ccurCenter{\thecur{myCenter}}% + \edef\ccurScoreEnd{\thecur{myScoreEnd}}% + \advance\theLevel by-1% + \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis + \edef\lcurScoreStart{\thecur{myScoreStart}}% + \edef\lcurCenter{\thecur{myCenter}}% + \edef\lcurScoreEnd{\thecur{myScoreEnd}}% +} + +\def\QuinaryInf$#1\fCenter#2${% + \prepQuinary% + \buildConclusion{#1}{#2}% + \joinQuinary% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\QuinaryInfC#1{% + \prepQuinary% + \buildConclusionC{#1}% + \joinQuinary% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\joinQuinary{% Construct the quinary inference into a vbox. + % Join the five hypotheses's boxes into one hbox. + \setbox\myBoxA=\hbox{\theHypSeparation}% + \lcurScoreEnd=\rrrcurScoreEnd% + \advance\lcurScoreEnd by\wd\rrcurBox% + \advance\lcurScoreEnd by\wd\rcurBox% + \advance\lcurScoreEnd by\wd\lcurBox% + \advance\lcurScoreEnd by\wd\ccurBox% + \advance\lcurScoreEnd by4\wd\myBoxA% + \displace=\lcurScoreEnd% + \advance\displace by -\lcurScoreStart% + \lcurCenter=.5\displace% + \advance\lcurCenter by\lcurScoreStart% + \ifx\rootAtBottomFlag\myTrue% + \setbox\lcurBox=% + \hbox{\box\lcurBox\unhcopy\myBoxA\box\ccurBox% + \unhcopy\myBoxA\box\rcurBox + \unhcopy\myBoxA\box\rrcurBox + \unhcopy\myBoxA\box\rrrcurBox}% + \else% + \htLbox = \ht\lcurBox% + \htAbox = \ht\myBoxA% + \htCbox = \ht\ccurBox% + \htRbox = \ht\rcurBox% + \htRRbox = \ht\rrcurBox% + \htRRRbox = \ht\rrrcurBox% + \setbox\lcurBox=% + \hbox{\lower\htLbox\box\lcurBox% + \lower\htAbox\copy\myBoxA\lower\htCbox\box\ccurBox% + \lower\htAbox\copy\myBoxA\lower\htRbox\box\rcurBox% + \lower\htAbox\copy\myBoxA\lower\htRRbox\box\rrcurBox% + \lower\htAbox\copy\myBoxA\lower\htRRRbox\box\rrrcurBox}% + \fi% + % Adjust center of upper hypotheses according to how much + % the lower sequent is off-center. + \displace=\newCenter% + \advance\displace by -.5\newScoreStart% + \advance\displace by -.5\newScoreEnd% + \advance\lcurCenter by \displace% + %Align and join the curBox and the two hypotheses's box into one vbox. + \edef\curBox{\lcurBox}% + \edef\curScoreStart{\lcurScoreStart}% + \edef\curScoreEnd{\lcurScoreEnd}% + \edef\curCenter{\lcurCenter}% + \joinUnary% +} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\def\buildConclusion#1#2{% Build lower sequent w/ center at \fCenter position. + % Define the boxes + \setbox\myBoxA=\hbox{$\mathord{#1}\fCenter\mathord{\relax}$}% + \setbox\myBoxB=\hbox{$#2$}% + % Put them together in \myBoxC + \setbox\myBoxC =% + \hbox{\hskip\ScoreOverhangLeft\relax% + \unhcopy\myBoxA\unhcopy\myBoxB\hskip\ScoreOverhangRight\relax}% + % Calculate the center of the \myBoxC string. + \newScoreStart=0pt \relax% + \newCenter=\wd\myBoxA \relax% + \advance \newCenter by \ScoreOverhangLeft% + \newScoreEnd=\wd\myBoxC% +} + +\def\buildConclusionC#1{% Build lower sequent w/o \fCenter present. + % Define the box. + \setbox\myBoxA=\hbox{#1}% + \setbox\myBoxC =% + \hbox{\hbox{\hskip\ScoreOverhangLeft\relax% + \unhcopy\myBoxA\hskip\ScoreOverhangRight\relax}}% + % Calculate kerning to line up centers + \newScoreStart=0pt \relax% + \newCenter=.5\wd\myBoxC \relax% + \newScoreEnd=\wd\myBoxC% + \advance \newCenter by \ScoreOverhangLeft% +} + +\def\joinUnary{%Align and join \curBox and \myBoxC into a single vbox + \global\advance\curCenter by -\hypKernAmt% + \ifnum\curCenter<\newCenter% + \displace=\newCenter% + \advance \displace by -\curCenter% + \kernUpperBox% + \else% + \displace=\curCenter% + \advance \displace by -\newCenter% + \kernLowerBox% + \fi% + \ifnum \newScoreStart < \curScoreStart % + \global \curScoreStart = \newScoreStart \fi% + \ifnum \curScoreEnd < \newScoreEnd % + \global \curScoreEnd = \newScoreEnd \fi% + % Leave room for the left label. + \ifnum \curScoreStart<\wd\myBoxLL% + \global\displace = \wd\myBoxLL% + \global\advance\displace by -\curScoreStart% + \kernUpperBox% + \kernLowerBox% + \fi% + % Draw the score + \buildScore% + % Form the score and labels into a box. + \buildScoreLabels% + % Form the new box and its dimensions + \ifx\rootAtBottomFlag\myTrue% + \buildRootBottom% + \else% + \buildRootTop% + \fi% + \global \curScoreStart=\newScoreStart% + \global \curScoreEnd=\newScoreEnd% + \global \curCenter=\newCenter% +} + +\def\buildRootBottom{% + \global \setbox \curBox =% + \vbox{\box\curBox% + \vskip\thisAboveSkip \relax% + \nointerlineskip\box\myBoxD% + \vskip\thisBelowSkip \relax% + \nointerlineskip\box\myBoxC}% +} + +\def\buildRootTop{% + \global \setbox \curBox =% + \vbox{\box\myBoxC% + \vskip\thisAboveSkip \relax% + \nointerlineskip\box\myBoxD% + \vskip\thisBelowSkip \relax% + \nointerlineskip\box\curBox}% +} + +\def\kernUpperBox{% + \global\setbox\curBox =% + \hbox{\hskip\displace\box\curBox}% + \global\advance \curScoreStart by \displace% + \global\advance \curScoreEnd by \displace% + \global\advance\curCenter by \displace% +} + +\def\kernLowerBox{% + \global\setbox\myBoxC =% + \hbox{\hskip\displace\unhbox\myBoxC}% + \global\advance \newScoreStart by \displace% + \global\advance \newScoreEnd by \displace% + \global\advance\newCenter by \displace% +} + +\def\joinBinary{% Construct the binary inference into a vbox. + % Join the two hypotheses's boxes into one hbox. + \setbox\myBoxA=\hbox{\theHypSeparation}% + \lcurScoreEnd=\rcurScoreEnd% + \advance\lcurScoreEnd by\wd\lcurBox% + \advance\lcurScoreEnd by\wd\myBoxA% + \displace=\lcurScoreEnd% + \advance\displace by -\lcurScoreStart% + \lcurCenter=.5\displace% + \advance\lcurCenter by\lcurScoreStart% + \ifx\rootAtBottomFlag\myTrue% + \setbox\lcurBox=% + \hbox{\box\lcurBox\unhcopy\myBoxA\box\rcurBox}% + \else% + \htLbox = \ht\lcurBox% + \htAbox = \ht\myBoxA% + \htRbox = \ht\rcurBox% + \setbox\lcurBox=% + \hbox{\lower\htLbox\box\lcurBox% + \lower\htAbox\box\myBoxA\lower\htRbox\box\rcurBox}% + \fi% + % Adjust center of upper hypotheses according to how much + % the lower sequent is off-center. + \displace=\newCenter% + \advance\displace by -.5\newScoreStart% + \advance\displace by -.5\newScoreEnd% + \advance\lcurCenter by \displace% + %Align and join the curBox and the two hypotheses's box into one vbox. + \edef\curBox{\lcurBox}% + \edef\curScoreStart{\lcurScoreStart}% + \edef\curScoreEnd{\lcurScoreEnd}% + \edef\curCenter{\lcurCenter}% + \joinUnary% +} + +\def\joinTrinary{% Construct the trinary inference into a vbox. + % Join the three hypotheses's boxes into one hbox. + \setbox\myBoxA=\hbox{\theHypSeparation}% + \lcurScoreEnd=\rcurScoreEnd% + \advance\lcurScoreEnd by\wd\lcurBox% + \advance\lcurScoreEnd by\wd\ccurBox% + \advance\lcurScoreEnd by2\wd\myBoxA% + \displace=\lcurScoreEnd% + \advance\displace by -\lcurScoreStart% + \lcurCenter=.5\displace% + \advance\lcurCenter by\lcurScoreStart% + \ifx\rootAtBottomFlag\myTrue% + \setbox\lcurBox=% + \hbox{\box\lcurBox\unhcopy\myBoxA\box\ccurBox% + \unhcopy\myBoxA\box\rcurBox}% + \else% + \htLbox = \ht\lcurBox% + \htAbox = \ht\myBoxA% + \htCbox = \ht\ccurBox% + \htRbox = \ht\rcurBox% + \setbox\lcurBox=% + \hbox{\lower\htLbox\box\lcurBox% + \lower\htAbox\copy\myBoxA\lower\htCbox\box\ccurBox% + \lower\htAbox\copy\myBoxA\lower\htRbox\box\rcurBox}% + \fi% + % Adjust center of upper hypotheses according to how much + % the lower sequent is off-center. + \displace=\newCenter% + \advance\displace by -.5\newScoreStart% + \advance\displace by -.5\newScoreEnd% + \advance\lcurCenter by \displace% + %Align and join the curBox and the two hypotheses's box into one vbox. + \edef\curBox{\lcurBox}% + \edef\curScoreStart{\lcurScoreStart}% + \edef\curScoreEnd{\lcurScoreEnd}% + \edef\curCenter{\lcurCenter}% + \joinUnary% +} + +\def\DisplayProof{% + % Display (and purge) the proof tree. + % Choose the appropriate vertical alignment. + \ifnum \theLevel=1 \relax \else%x + \errmessage{Proof tree badly specified.}% + \fi% + \edef\curBox{\thecur{myBox}}% + \ifx\bottomAlignFlag\myTrue% + \displace=0pt% + \else% + \displace=.5\ht\curBox% + \ifx\centerAlignFlag\myTrue\relax + \else% + \advance\displace by -3pt% + \fi% + \fi% + \leavevmode% + \lower\displace\hbox{\copy\curBox}% + \global\theLevel=0% + \global\def\alwaysBuildScore{\defaultBuildScore}% Restore "always" + \global\def\alwaysScoreFiller{\defaultScoreFiller}% Restore "always" + \global\def\bottomAlignFlag{N}% + \global\def\centerAlignFlag{N}% + \resetRootPosition + \resetInferenceDefaults% + \ignorespaces +} + +\def\buildSingleScore{% Make an hbox with a single score. + \displace=\curScoreEnd% + \advance \displace by -\curScoreStart% + \global\setbox \myBoxD =% + \hbox to \displace{\expandafter\xleaders\theScoreFiller\hfill}% + %\global\setbox \myBoxD =% + %\hbox{\hskip\curScoreStart\relax \box\myBoxD}% +} + +\def\buildDoubleScore{% Make an hbox with a double score. + \buildSingleScore% + \global\setbox\myBoxD=% + \hbox{\hbox to0pt{\copy\myBoxD\hss}\raise2pt\copy\myBoxD}% +} + +\def\buildNoScore{% Make an hbox with no score (raise a little anyway) + \global\setbox\myBoxD=\hbox{\vbox{\vskip1pt}}% +} + +\def\doubleLine{% + \gdef\buildScore{\buildDoubleScore}% Set next score to this type + \ignorespaces +} +\def\alwaysDoubleLine{% + \gdef\alwaysBuildScore{\buildDoubleScore}% Do double for rest of proof. + \gdef\buildScore{\buildDoubleScore}% Set next score to be double + \ignorespaces +} +\def\singleLine{% + \gdef\buildScore{\buildSingleScore}% Set next score to be single + \ignorespaces +} +\def\alwaysSingleLine{% + \gdef\alwaysBuildScore{\buildSingleScore}% Do single for rest of proof. + \gdef\buildScore{\buildSingleScore}% Set next score to be single + \ignorespaces +} +\def\noLine{% + \gdef\buildScore{\buildNoScore}% Set next score to this type + \ignorespaces +} +\def\alwaysNoLine{% + \gdef\alwaysBuildScore{\buildNoScore}%Do nolines for rest of proof. + \gdef\buildScore{\buildNoScore}% Set next score to be blank + \ignorespaces +} +\def\solidLine{% + \gdef\theScoreFiller{\ruleScoreFiller}% Use solid horizontal line. + \ignorespaces +} +\def\alwaysSolidLine{% + \gdef\alwaysScoreFiller{\ruleScoreFiller}% Do solid for rest of proof + \gdef\theScoreFiller{\ruleScoreFiller}% Use solid horizontal line. + \ignorespaces +} +\def\dottedLine{% + \gdef\theScoreFiller{\dottedScoreFiller}% Use dotted horizontal line. + \ignorespaces +} +\def\alwaysDottedLine{% + \gdef\alwaysScoreFiller{\dottedScoreFiller}% Do dotted for rest of proof + \gdef\theScoreFiller{\dottedScoreFiller}% Use dotted horizontal line. + \ignorespaces +} +\def\dashedLine{% + \gdef\theScoreFiller{\dashedScoreFiller}% Use dashed horizontal line. + \ignorespaces +} +\def\alwaysDashedLine{% + \gdef\alwaysScoreFiller{\dashedScoreFiller}% Do dashed for rest of proof + \gdef\theScoreFiller{\dashedScoreFiller}% Use dashed horizontal line. + \ignorespaces +} +\def\kernHyps#1{% + \gdef\hypKernAmt{#1}% + \ignorespaces +} +\def\insertBetweenHyps#1{% + \gdef\theHypSeparation{#1}% + \ignorespaces +} + +\def\centerAlignProof{% + \def\centerAlignFlag{Y}% + \def\bottomAlignFlag{N}% + \ignorespaces +} +\def\bottomAlignProof{% + \def\centerAlignFlag{N}% + \def\bottomAlignFlag{Y}% + \ignorespaces +} +\def\normalAlignProof{% + \def\centerAlignFlag{N}% + \def\bottomAlignFlag{N}% + \ignorespaces +} + +\def\LeftLabel#1{% + \global\setbox\myBoxLL=\hbox{{#1}\hskip\labelSpacing}% + \ignorespaces +} +\def\RightLabel#1{% + \global\setbox\myBoxRL=\hbox{\hskip\labelSpacing #1}% + \ignorespaces +} + +\def\buildScoreLabels{% + \scoreHeight = \ht\myBoxD% + \scoreDepth = \dp\myBoxD% + \leftLowerAmt=\ht\myBoxLL% + \advance \leftLowerAmt by -\dp\myBoxLL% + \advance \leftLowerAmt by -\scoreHeight% + \advance \leftLowerAmt by \scoreDepth% + \leftLowerAmt=.5\leftLowerAmt% + \rightLowerAmt=\ht\myBoxRL% + \advance \rightLowerAmt by -\dp\myBoxRL% + \advance \rightLowerAmt by -\scoreHeight% + \advance \rightLowerAmt by \scoreDepth% + \rightLowerAmt=.5\rightLowerAmt% + \displace = \curScoreStart% + \advance\displace by -\wd\myBoxLL% + \global\setbox\myBoxD =% + \hbox{\hskip\displace% + \lower\leftLowerAmt\copy\myBoxLL% + \box\myBoxD% + \lower\rightLowerAmt\copy\myBoxRL}% + \global\thisAboveSkip = \ht\myBoxLL% + \global\advance \thisAboveSkip by -\leftLowerAmt% + \global\advance \thisAboveSkip by -\scoreHeight% + \ifnum \thisAboveSkip<0 % + \global\thisAboveSkip=0pt% + \fi% + \displace = \ht\myBoxRL% + \advance \displace by -\rightLowerAmt% + \advance \displace by -\scoreHeight% + \ifnum \displace<0 % + \displace=0pt% + \fi% + \ifnum \displace>\thisAboveSkip % + \global\thisAboveSkip=\displace% + \fi% + \global\thisBelowSkip = \dp\myBoxLL% + \global\advance\thisBelowSkip by \leftLowerAmt% + \global\advance\thisBelowSkip by -\scoreDepth% + \ifnum\thisBelowSkip<0 % + \global\thisBelowSkip = 0pt% + \fi% + \displace = \dp\myBoxRL% + \advance\displace by \rightLowerAmt% + \advance\displace by -\scoreDepth% + \ifnum\displace<0 % + \displace = 0pt% + \fi% + \ifnum\displace>\thisBelowSkip% + \global\thisBelowSkip = \displace% + \fi% + \global\thisAboveSkip = -\thisAboveSkip% + \global\thisBelowSkip = -\thisBelowSkip% + \global\advance\thisAboveSkip by\extraVskip% Extra space above line + \global\advance\thisBelowSkip by\extraVskip% Extra space below line +} + +\def\resetInferenceDefaults{% + \global\def\theHypSeparation{\defaultHypSeparation}% + \global\setbox\myBoxLL=\hbox{\defaultLeftLabel}% + \global\setbox\myBoxRL=\hbox{\defaultRightLabel}% + \global\def\buildScore{\alwaysBuildScore}% + \global\def\theScoreFiller{\alwaysScoreFiller}% + \gdef\hypKernAmt{0pt}% Restore to zero kerning. +} + + +\def\rootAtBottom{% + \global\def\rootAtBottomFlag{Y}% +} + +\def\rootAtTop{% + \global\def\rootAtBottomFlag{N}% +} + +\def\resetRootPosition{% + \global\edef\rootAtBottomFlag{\defaultRootAtBottomFlag} +} + +\def\alwaysRootAtBottom{% + \global\def\defaultRootAtBottomFlag{Y} + \rootAtBottom +} + +\def\alwaysRootAtTop{% + \global\def\defaultRootAtBottomFlag{N} + \rootAtTop +} + + diff -r d12b2800af6a -r ead50a89470f midterm/midterm.aux --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/midterm.aux Wed Oct 25 17:35:36 2017 +0900 @@ -0,0 +1,24 @@ +\relax +\citation{Yasutaka:2016} +\citation{agda} +\@writefile{toc}{\contentsline {section}{\numberline {1}研究目的}{1}} +\@writefile{toc}{\contentsline {section}{\numberline {2}Countinuation based C (CbC)}{1}} +\@writefile{toc}{\contentsline {section}{\numberline {3}Agda}{1}} +\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces 自然演繹での三段論法の証明}}{1}} +\newlabel{fig:modus-ponens}{{1}{1}} +\citation{*} +\bibstyle{junsrt} +\bibdata{reference} +\bibcite{Yasutaka:2016}{1} +\bibcite{agda}{2} +\bibcite{Tatsuki:2016}{3} +\bibcite{kaito:2015}{4} +\bibcite{agda-documentation}{5} +\newlabel{src:singlelinked}{{1}{2}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {1}CbCによるStack}{2}} +\newlabel{src:stack-agda}{{2}{2}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {2}AgdaによるStack}{2}} +\@writefile{toc}{\contentsline {section}{\numberline {4}RedBlackTree}{2}} +\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces RedBlackTreeの例}}{2}} +\newlabel{fig:rbtree}{{2}{2}} +\@writefile{toc}{\contentsline {section}{\numberline {5}今後の課題}{2}} diff -r d12b2800af6a -r ead50a89470f midterm/midterm.bbl --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/midterm.bbl Wed Oct 25 17:35:36 2017 +0900 @@ -0,0 +1,25 @@ +\begin{thebibliography}{1} + +\bibitem{Yasutaka:2016} +{比嘉 健太, 河野 真治}. +\newblock {メタ計算を用いた Continuation based C の検証手法}, 2016. + +\bibitem{agda} +The agda wiki. +\newblock \url{http://wiki.portal.chalmers.se/agda/pmwiki.php}. +\newblock Accessed: 2017/10/24(Tue). + +\bibitem{Tatsuki:2016} +{伊波 立樹, 東恩納 琢偉, 河野 真治}. +\newblock {Code Gear 、Data Gear に基づく OS のプロトタイプ}, 2016. + +\bibitem{kaito:2015} +{徳森 海斗, 河野 真治}. +\newblock {LLVM Clang 上の Continuation based C コンパイラ の改良}, 2015. + +\bibitem{agda-documentation} +Welcome to agda’s documentation! ― agda 2.6.0 documentation. +\newblock \url{http://agda.readthedocs.io/en/latest/index.html}. +\newblock Accessed: 2017/10/24(Tue). + +\end{thebibliography} diff -r d12b2800af6a -r ead50a89470f midterm/midterm.blg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/midterm.blg Wed Oct 25 17:35:36 2017 +0900 @@ -0,0 +1,47 @@ +This is pBibTeX, Version 0.99d-j0.33 (utf8.euc) (TeX Live 2016) +Capacity: max_strings=35307, hash_size=35307, hash_prime=30011 +The top-level auxiliary file: midterm.aux +The style file: junsrt.bst +Database file #1: reference.bib +You've used 5 entries, + 2270 wiz_defined-function locations, + 561 strings with 4741 characters, +and the built_in function-call counts, 806 in all, are: += -- 44 +> -- 14 +< -- 0 ++ -- 8 +- -- 3 +* -- 5 +:= -- 87 +add.period$ -- 12 +call.type$ -- 5 +change.case$ -- 5 +chr.to.int$ -- 0 +cite$ -- 5 +duplicate$ -- 55 +empty$ -- 121 +format.name$ -- 6 +if$ -- 201 +int.to.chr$ -- 0 +int.to.str$ -- 5 +missing$ -- 0 +newline$ -- 25 +num.names$ -- 3 +pop$ -- 63 +preamble$ -- 1 +purify$ -- 0 +quote$ -- 0 +skip$ -- 47 +stack$ -- 0 +substring$ -- 0 +swap$ -- 5 +text.length$ -- 0 +text.prefix$ -- 0 +top$ -- 0 +type$ -- 0 +warning$ -- 0 +while$ -- 3 +width$ -- 6 +write$ -- 44 +is.kanji.str$ -- 33 diff -r d12b2800af6a -r ead50a89470f midterm/midterm.dvi Binary file midterm/midterm.dvi has changed diff -r d12b2800af6a -r ead50a89470f midterm/midterm.fdb_latexmk --- a/midterm/midterm.fdb_latexmk Mon Oct 16 23:07:05 2017 +0900 +++ b/midterm/midterm.fdb_latexmk Wed Oct 25 17:35:36 2017 +0900 @@ -1,29 +1,18 @@ # Fdb version 3 -["bibtex finalPre"] 1508159110 "finalPre.aux" "finalPre.bbl" "finalPre" 1508159111 - "finalPre.aux" 1508159110 274 dda61d95357da4107ccf6ee2704b61c2 "" - "finalPre.bcf" 0 -1 0 "" +["bibtex midterm"] 0 "midterm.aux" "midterm.bbl" "midterm" 0 "junsrt.bst" 0 -1 0 "" - "reference.bib" 1495704071 639 40cd366700b46f001780c71f4608d3e3 "" - (generated) - "finalPre.bbl" -["dvipdf"] 1508159111 "finalPre.dvi" "finalPre.pdf" "finalPre" 1508159111 - "finalPre.dvi" 1508159110 1608 bc283e9dfdcab7e88dff872cb1176d13 "latex" + "midterm.aux" 1508332725 633 cb1069f0c006f1deecf5bae23f48fb04 "" + "midterm.bcf" 0 -1 0 "" + "reference.bib" 1508162081 342 e4f45eba33cb4afbbc5c44615e595cbc "" (generated) - "finalPre.pdf" -["latex"] 1508159110 "finalPre.tex" "finalPre.dvi" "finalPre" 1508159111 + "midterm.bbl" +["dvipdf"] 0 "midterm.dvi" "midterm.pdf" "midterm" 0 + "midterm.dvi" 0 -1 0 "latex" + (generated) + "midterm.pdf" +["latex"] 1508332725 "midterm.tex" "midterm.dvi" "midterm" 1508332725 "/usr/local/texlive/2016/texmf-dist/fonts/map/fontname/texfonts.map" 1272929888 3287 e6b82fe08f5336d4d5ebc73fb1152e87 "" - "/usr/local/texlive/2016/texmf-dist/fonts/tfm/ptex-fonts/standard/goth10.tfm" 1463434352 1196 5981e79c37b2cfd27b3612a6783cd4b6 "" - "/usr/local/texlive/2016/texmf-dist/fonts/tfm/ptex-fonts/standard/goth9.tfm" 1463434352 1196 b274fc006918dea9e5263e2117f4bddb "" - "/usr/local/texlive/2016/texmf-dist/fonts/tfm/ptex-fonts/standard/min10.tfm" 1463434352 1196 1be730212205a270378fba11a44765dc "" - "/usr/local/texlive/2016/texmf-dist/fonts/tfm/ptex-fonts/standard/min6.tfm" 1463434352 1196 ede67ffb8cb4a6a8b9436c82b428664c "" - "/usr/local/texlive/2016/texmf-dist/fonts/tfm/ptex-fonts/standard/min8.tfm" 1463434352 1196 d5b431ce76e19b70391960a9dd08fa4f "" - "/usr/local/texlive/2016/texmf-dist/fonts/tfm/ptex-fonts/standard/min9.tfm" 1463434352 1196 415df3c165ce605a3c248afbbe3c844b "" - "/usr/local/texlive/2016/texmf-dist/fonts/tfm/ptex-fonts/standard/tgoth10.tfm" 1463434352 856 7404843a5f798859944d7973a47821d5 "" - "/usr/local/texlive/2016/texmf-dist/fonts/tfm/ptex-fonts/standard/tgoth9.tfm" 1463434352 856 bed293689e159275e10c27a9927115b7 "" - "/usr/local/texlive/2016/texmf-dist/fonts/tfm/ptex-fonts/standard/tmin10.tfm" 1463434352 856 39c171483fe1bb7d0e1368980c0c205b "" - "/usr/local/texlive/2016/texmf-dist/fonts/tfm/ptex-fonts/standard/tmin9.tfm" 1463434352 856 b22b8128b44bf8881977f2c74b361f47 "" "/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmbx12.tfm" 1136768653 1324 c910af8c371558dc20f2d7822f66fe64 "" - "/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmbx9.tfm" 1136768653 1328 5442e22a7072966dbaf88ca900acf3f0 "" "/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmmi12.tfm" 1136768653 1524 4414a8315f39513458b80dfc63bff03a "" "/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmmi6.tfm" 1136768653 1512 f21f83efb36853c0b70002322c1ab3ad "" "/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmmi8.tfm" 1136768653 1520 eccf95517727cb11801f4f1aee3a21b4 "" @@ -31,11 +20,14 @@ "/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmr17.tfm" 1136768653 1292 296a67155bdbfc32aa9c636f21e91433 "" "/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmr6.tfm" 1136768653 1300 b62933e007d01cfd073f79b963c01526 "" "/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmr8.tfm" 1136768653 1292 21c1c5bfeaebccffdb478fd231a0997d "" - "/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmr9.tfm" 1136768653 1292 6b21b9c2c7bebb38aa2273f7ca0fb3af "" "/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm" 1136768653 1124 6c73e740cf17375f03eec0ee63599741 "" "/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmsy6.tfm" 1136768653 1116 933a60c408fc0a863a92debe84b2d294 "" "/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmsy8.tfm" 1136768653 1120 8b7d695260f3cff42e636090a8002094 "" "/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmtt10.tfm" 1136768653 768 1321e9409b4137d6fb428ac9dc956269 "" + "/usr/local/texlive/2016/texmf-dist/fonts/tfm/uptex-fonts/jis/upjisg-h.tfm" 1463242385 780 9d56a8f9483b0d090553358c515b7835 "" + "/usr/local/texlive/2016/texmf-dist/fonts/tfm/uptex-fonts/jis/upjisg-v.tfm" 1463242385 504 db18a8c0bf0b51f5d6237cc98872380d "" + "/usr/local/texlive/2016/texmf-dist/fonts/tfm/uptex-fonts/jis/upjisr-h.tfm" 1463242385 780 9d56a8f9483b0d090553358c515b7835 "" + "/usr/local/texlive/2016/texmf-dist/fonts/tfm/uptex-fonts/jis/upjisr-v.tfm" 1463242385 504 db18a8c0bf0b51f5d6237cc98872380d "" "/usr/local/texlive/2016/texmf-dist/tex/generic/oberdiek/infwarerr.sty" 1463608860 8253 473e0e41f9adadb1977e8631b8f72ea6 "" "/usr/local/texlive/2016/texmf-dist/tex/generic/oberdiek/ltxcmds.sty" 1463608860 18425 5b3c0c59d76fac78978b5558e83c1f36 "" "/usr/local/texlive/2016/texmf-dist/tex/latex/abstract/abstract.sty" 1252025310 5128 640a4c0ff76b3e578a4c5482af27ec14 "" @@ -50,15 +42,14 @@ "/usr/local/texlive/2016/texmf-dist/tex/platex/base/jarticle.cls" 1462837567 25231 a08460ff81096cb3e80d7be01474f985 "" "/usr/local/texlive/2016/texmf-dist/tex/platex/base/jsize10.clo" 1462837567 9313 f538ec39b9e111bf9320856d312460b2 "" "/usr/local/texlive/2016/texmf-dist/web2c/texmf.cnf" 1463093894 31953 b9489e6e586f798610c60aec1f5ec548 "" - "/usr/local/texlive/2016/texmf-var/web2c/eptex/platex.fmt" 1492015362 4058165 6f29dcc32a458d782f15489197b9f3b3 "" + "/usr/local/texlive/2016/texmf-var/web2c/euptex/uplatex.fmt" 1492015395 4047635 b3cd114470c56155cdcfdd945c0f085e "" "/usr/local/texlive/2016/texmf.cnf" 1463979140 577 2938757e76f31531e65cc647e3507693 "" - "dummy.tex" 1495704071 2711 ebf4ee4460f50857f8ebbbf2d432d91e "" - "finalPre.aux" 1508159110 274 dda61d95357da4107ccf6ee2704b61c2 "" - "finalPre.bbl" 1508159110 411 b36e426bd4e981fd613443e5a9228e9a "bibtex finalPre" - "finalPre.tex" 1508159107 1440 92f7390716dd4ba6eda6426685f05d86 "" - "pic/emblem-bitmap.pdf" 0 -1 0 "" - "picins.sty" 1495704071 17807 916739e9c8f52c6a085688f05d1594e2 "" + "dummy.tex" 1508162081 2711 ebf4ee4460f50857f8ebbbf2d432d91e "" + "midterm.aux" 1508332725 8 a94a2480d3289e625eea47cd1b285758 "" + "midterm.bbl" 1508229470 270 0ff43ed253eb90c3e1f0aa4c2531e4d9 "bibtex midterm" + "midterm.tex" 1508332620 2829 be97b3f887631e620bc0f43b4aa0ae20 "" + "picins.sty" 1508162081 17807 916739e9c8f52c6a085688f05d1594e2 "" (generated) - "finalPre.log" - "finalPre.dvi" - "finalPre.aux" + "midterm.aux" + "midterm.log" + "midterm.dvi" diff -r d12b2800af6a -r ead50a89470f midterm/midterm.fls --- a/midterm/midterm.fls Mon Oct 16 23:07:05 2017 +0900 +++ b/midterm/midterm.fls Wed Oct 25 17:35:36 2017 +0900 @@ -1,10 +1,10 @@ -PWD /Users/ryokka/cr/ryokka-thesis/final_pre +PWD /Users/ryokka/cr/ryokka-midterm/midterm INPUT /usr/local/texlive/2016/texmf.cnf INPUT /usr/local/texlive/2016/texmf-dist/web2c/texmf.cnf INPUT /usr/local/texlive/2016/texmf.cnf -INPUT /usr/local/texlive/2016/texmf-var/web2c/eptex/platex.fmt -INPUT finalPre.tex -OUTPUT finalPre.log +INPUT /usr/local/texlive/2016/texmf-var/web2c/euptex/uplatex.fmt +INPUT midterm.tex +OUTPUT midterm.log INPUT /usr/local/texlive/2016/texmf-dist/tex/platex/base/jarticle.cls INPUT /usr/local/texlive/2016/texmf-dist/tex/platex/base/jarticle.cls INPUT /usr/local/texlive/2016/texmf-dist/tex/platex/base/jsize10.clo @@ -35,12 +35,12 @@ INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/url/url.sty INPUT dummy.tex INPUT dummy.tex -INPUT finalPre.aux -INPUT finalPre.aux -OUTPUT finalPre.aux +INPUT midterm.aux +INPUT midterm.aux +OUTPUT midterm.aux INPUT /usr/local/texlive/2016/texmf-dist/fonts/map/fontname/texfonts.map -INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/ptex-fonts/standard/tmin10.tfm -INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/ptex-fonts/standard/min10.tfm +INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/uptex-fonts/jis/upjisr-v.tfm +INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/uptex-fonts/jis/upjisr-h.tfm INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmr17.tfm INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmr12.tfm INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmr8.tfm @@ -51,22 +51,14 @@ INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmsy8.tfm INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmsy6.tfm -INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/ptex-fonts/standard/min8.tfm -INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/ptex-fonts/standard/min6.tfm -INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/ptex-fonts/standard/tmin9.tfm -INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/ptex-fonts/standard/min9.tfm -INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmr9.tfm -INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/ptex-fonts/standard/tgoth9.tfm -INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/ptex-fonts/standard/goth9.tfm -INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmbx9.tfm -INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/ptex-fonts/standard/tmin10.tfm -INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/ptex-fonts/standard/min10.tfm +INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/uptex-fonts/jis/upjisr-v.tfm +INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/uptex-fonts/jis/upjisr-h.tfm INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmr12.tfm -INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/ptex-fonts/standard/tgoth10.tfm -INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/ptex-fonts/standard/goth10.tfm +INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/uptex-fonts/jis/upjisg-v.tfm +INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/uptex-fonts/jis/upjisg-h.tfm INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmbx12.tfm -INPUT finalPre.bbl -INPUT finalPre.bbl +INPUT midterm.bbl +INPUT midterm.bbl INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmtt10.tfm -OUTPUT finalPre.dvi -INPUT finalPre.aux +OUTPUT midterm.dvi +INPUT midterm.aux diff -r d12b2800af6a -r ead50a89470f midterm/midterm.log --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/midterm.log Wed Oct 25 17:35:36 2017 +0900 @@ -0,0 +1,262 @@ +This is e-pTeX, Version 3.14159265-p3.7-160201-2.6 (utf8.euc) (TeX Live 2016) (preloaded format=platex 2017.4.13) 25 OCT 2017 17:25 +entering extended mode + restricted \write18 enabled. + %&-line parsing enabled. +**midterm.tex +(./midterm.tex +pLaTeX2e <2016/05/07> (based on LaTeX2e <2016/03/31>) +Babel <3.9r> and hyphenation patterns for 83 language(s) loaded. +(/usr/local/texlive/2016/texmf-dist/tex/platex/base/jarticle.cls +Document Class: jarticle 2006/06/27 v1.6 Standard pLaTeX class +\c@@paper=\count81 +(/usr/local/texlive/2016/texmf-dist/tex/platex/base/jsize10.clo +File: jsize10.clo 2006/06/27 v1.6 Standard pLaTeX file (size option) +) +\c@part=\count82 +\c@section=\count83 +\c@subsection=\count84 +\c@subsubsection=\count85 +\c@paragraph=\count86 +\c@subparagraph=\count87 +\c@figure=\count88 +\c@table=\count89 +\abovecaptionskip=\skip41 +\belowcaptionskip=\skip42 +\symmincho=\mathgroup4 +LaTeX Font Info: Overwriting symbol font `mincho' in version `bold' +(Font) JY1/mc/m/n --> JY1/gt/m/n on input line 593. +\toclineskip=\dimen118 +\@lnumwidth=\dimen119 +\bibindent=\dimen120 +\heisei=\count90 +) +(/usr/local/texlive/2016/texmf-dist/tex/latex/graphics/graphicx.sty +Package: graphicx 2014/10/28 v1.0g Enhanced LaTeX Graphics (DPC,SPQR) + +(/usr/local/texlive/2016/texmf-dist/tex/latex/graphics/keyval.sty +Package: keyval 2014/10/28 v1.15 key=value parser (DPC) +\KV@toks@=\toks15 +) +(/usr/local/texlive/2016/texmf-dist/tex/latex/graphics/graphics.sty +Package: graphics 2016/05/09 v1.0r Standard LaTeX Graphics (DPC,SPQR) + +(/usr/local/texlive/2016/texmf-dist/tex/latex/graphics/trig.sty +Package: trig 2016/01/03 v1.10 sin cos tan (DPC) +) +(/usr/local/texlive/2016/texmf-dist/tex/latex/graphics-cfg/graphics.cfg +File: graphics.cfg 2016/01/02 v1.10 sample graphics configuration +) +Package graphics Info: Driver file: dvipdfmx.def on input line 96. + +(/usr/local/texlive/2016/texmf-dist/tex/latex/dvipdfmx-def/dvipdfmx.def +File: dvipdfmx.def 2016/04/06 v4.08 LaTeX color/graphics driver for dvipdfmx (T +eX Live/ChoF) + +(/usr/local/texlive/2016/texmf-dist/tex/generic/oberdiek/infwarerr.sty +Package: infwarerr 2016/05/16 v1.4 Providing info/warning/error messages (HO) +) +(/usr/local/texlive/2016/texmf-dist/tex/generic/oberdiek/ltxcmds.sty +Package: ltxcmds 2016/05/16 v1.23 LaTeX kernel commands for general use (HO) +))) +\Gin@req@height=\dimen121 +\Gin@req@width=\dimen122 +) +(./picins.sty Option `picins' Version 3.0 Sep. 1992, TH Darmstadt/HRZ +\@BILD=\box41 +\@TEXT=\box42 +\d@breite=\dimen123 +\d@hoehe=\dimen124 +\d@xoff=\dimen125 +\d@yoff=\dimen126 +\d@shad=\dimen127 +\d@dash=\dimen128 +\d@boxl=\dimen129 +\d@pichskip=\dimen130 +\d@tmp=\dimen131 +\d@tmpa=\dimen132 +\d@bskip=\dimen133 +\hsiz@=\dimen134 +\p@getot@l=\dimen135 +\c@breite=\count91 +\c@hoehe=\count92 +\c@xoff=\count93 +\c@yoff=\count94 +\c@pos=\count95 +\c@shad=\count96 +\c@dash=\count97 +\c@boxl=\count98 +\c@zeilen=\count99 +\@changemode=\count100 +\c@piccaption=\count101 +\c@piccaptionpos=\count102 +\c@picpos=\count103 +\c@whole=\count104 +\c@half=\count105 +\c@tmp=\count106 +\c@tmpa=\count107 +\c@tmpb=\count108 +\c@tmpc=\count109 +\c@tmpd=\count110 +\d@leftskip=\skip43 +\ptoti=\dimen136 +\ptotii=\dimen137 +\env@box=\box43 +\d@envdp=\dimen138 +\c@hsize=\count111 +\c@envdp=\count112 +\d@envb=\dimen139 +) +(/usr/local/texlive/2016/texmf-dist/tex/latex/listings/listings.sty +\lst@mode=\count113 +\lst@gtempboxa=\box44 +\lst@token=\toks16 +\lst@length=\count114 +\lst@currlwidth=\dimen140 +\lst@column=\count115 +\lst@pos=\count116 +\lst@lostspace=\dimen141 +\lst@width=\dimen142 +\lst@newlines=\count117 +\lst@lineno=\count118 +\lst@maxwidth=\dimen143 + +(/usr/local/texlive/2016/texmf-dist/tex/latex/listings/lstmisc.sty +File: lstmisc.sty 2015/06/04 1.6 (Carsten Heinz) +\c@lstnumber=\count119 +\lst@skipnumbers=\count120 +\lst@framebox=\box45 +) +(/usr/local/texlive/2016/texmf-dist/tex/latex/listings/listings.cfg +File: listings.cfg 2015/06/04 1.6 listings configuration +)) +Package: listings 2015/06/04 1.6 (Carsten Heinz) + +(./jlisting.sty +Package: jlisting 2006/02/20 0.2 (Thor) +\lst@nextchar=\count121 +\lst@inputfile=\read1 +) +(/usr/local/texlive/2016/texmf-dist/tex/latex/fancyhdr/fancyhdr.sty +\fancy@headwidth=\skip44 +\f@ncyO@elh=\skip45 +\f@ncyO@erh=\skip46 +\f@ncyO@olh=\skip47 +\f@ncyO@orh=\skip48 +\f@ncyO@elf=\skip49 +\f@ncyO@erf=\skip50 +\f@ncyO@olf=\skip51 +\f@ncyO@orf=\skip52 +) +(/usr/local/texlive/2016/texmf-dist/tex/latex/abstract/abstract.sty +Package: abstract 2009/06/08 v1.2a configurable abstracts +\abstitleskip=\skip53 +\absleftindent=\skip54 +\absrightindent=\skip55 +\absparindent=\skip56 +\absparsep=\skip57 +) +(/usr/local/texlive/2016/texmf-dist/tex/latex/url/url.sty +\Urlmuskip=\muskip10 +Package: url 2013/09/16 ver 3.4 Verb mode for urls, etc. +) (./bussproofs.sty +Proof Tree (bussproofs) style macros. Version 1.1. +\theLevel=\count122 +\myMaxLevel=\count123 +\myBoxA=\box46 +\myBoxB=\box47 +\myBoxC=\box48 +\myBoxD=\box49 +\myBoxLL=\box50 +\myBoxRL=\box51 +\thisAboveSkip=\dimen144 +\thisBelowSkip=\dimen145 +\newScoreStart=\dimen146 +\newScoreEnd=\dimen147 +\newCenter=\dimen148 +\displace=\dimen149 +\leftLowerAmt=\dimen150 +\rightLowerAmt=\dimen151 +\scoreHeight=\dimen152 +\scoreDepth=\dimen153 +\htLbox=\dimen154 +\htRbox=\dimen155 +\htRRbox=\dimen156 +\htRRRbox=\dimen157 +\htAbox=\dimen158 +\htCbox=\dimen159 +) (./dummy.tex) + +LaTeX Warning: Unused global option(s): + [9.5pt]. + +(./midterm.aux) +\openout1 = `midterm.aux'. + +LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 53. +LaTeX Font Info: ... okay on input line 53. +LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 53. +LaTeX Font Info: ... okay on input line 53. +LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 53. +LaTeX Font Info: ... okay on input line 53. +LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 53. +LaTeX Font Info: ... okay on input line 53. +LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 53. +LaTeX Font Info: ... okay on input line 53. +LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 53. +LaTeX Font Info: ... okay on input line 53. +LaTeX Font Info: Checking defaults for JY1/mc/m/n on input line 53. +LaTeX Font Info: ... okay on input line 53. +LaTeX Font Info: Checking defaults for JT1/mc/m/n on input line 53. +LaTeX Font Info: ... okay on input line 53. +\c@lstlisting=\count124 +LaTeX Font Info: External font `cmex10' loaded for size +(Font) <12> on input line 60. +LaTeX Font Info: External font `cmex10' loaded for size +(Font) <8> on input line 60. +LaTeX Font Info: External font `cmex10' loaded for size +(Font) <6> on input line 60. +LaTeX Font Info: Font shape `JT1/mc/bx/n' in size <14.4> not available +(Font) Font shape `JT1/gt/m/n' tried instead on input line 62. +LaTeX Font Info: Font shape `JY1/mc/bx/n' in size <14.4> not available +(Font) Font shape `JY1/gt/m/n' tried instead on input line 62. + +Underfull \hbox (badness 1275) in paragraph at lines 129--130 +[]\JY1/mc/m/n/10 比嘉 \OT1/cmr/m/n/10 (2016)[[]] \JY1/mc/m/n/10 では \OT1/cmr/m +/n/10 CbC \JY1/mc/m/n/10 における \OT1/cmr/m/n/10 Code-Seg-ment \JY1/mc/m/n/10 +、 + [] + +LaTeX Font Info: External font `cmex10' loaded for size +(Font) <7> on input line 139. +LaTeX Font Info: External font `cmex10' loaded for size +(Font) <5> on input line 139. +File: ../pic/modus-ponens.pdf Graphic file (type pdf) +<../pic/modus-ponens.pdf> +Overfull \hbox (17.80374pt too wide) in paragraph at lines 151--152 + [] + [] + +[1 + + +] +LaTeX Font Info: Try loading font information for OMS+cmr on input line 237. + + (/usr/local/texlive/2016/texmf-dist/tex/latex/base/omscmr.fd +File: omscmr.fd 2014/09/29 v2.5h Standard LaTeX font definitions +) +LaTeX Font Info: Font shape `OMS/cmr/m/n' in size <10> not available +(Font) Font shape `OMS/cmsy/m/n' tried instead on input line 237. +File: ../pic/rbtree.pdf Graphic file (type pdf) + +<../pic/rbtree.pdf> (./midterm.bbl) [2] (./midterm.aux) ) +Here is how much of TeX's memory you used: + 2621 strings out of 493693 + 35150 string characters out of 6149787 + 348144 words of memory out of 5000000 + 6171 multiletter control sequences out of 15000+600000 + 13613 words of font info for 54 fonts, out of 8000000 for 9000 + 929 hyphenation exceptions out of 8191 + 27i,7n,43p,246b,1003s stack positions out of 5000i,500n,10000p,200000b,80000s + +Output written on midterm.dvi (2 pages, 15628 bytes). diff -r d12b2800af6a -r ead50a89470f midterm/midterm.pdf Binary file midterm/midterm.pdf has changed diff -r d12b2800af6a -r ead50a89470f midterm/midterm.tex --- a/midterm/midterm.tex Mon Oct 16 23:07:05 2017 +0900 +++ b/midterm/midterm.tex Wed Oct 25 17:35:36 2017 +0900 @@ -1,11 +1,16 @@ +%% TODO Agdaに関してやったこと書く +%% TODO AgdaのStackとcbcのstackを例として出す。 + \documentclass[twocolumn,twoside,9.5pt]{jarticle} \usepackage[dvipdfmx]{graphicx} \usepackage{picins} +\usepackage{listings,jlisting} \usepackage{fancyhdr} \usepackage{abstract} \usepackage{url} +\usepackage{bussproofs} %\pagestyle{fancy} -\lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{../pic/emblem-bitmap.pdf}}琉球大学主催 工学部情報工学科 卒業研究発表会} +\lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{../pic/emblem-bitmap.pdf}}琉球大学主催 工学部情報工学科 中間発表予稿} \rhead{} \cfoot{} @@ -19,31 +24,257 @@ \setlength{\footskip}{0mm} \pagestyle{empty} +%% \lstset{% +%% breaklines=true +%% } + +\lstset{ + frame=single, + keepspaces=true, + stringstyle={\ttfamily}, + commentstyle={\ttfamily}, + identifierstyle={\ttfamily}, + keywordstyle={\ttfamily}, + basicstyle={\ttfamily}, + breaklines=true, + xleftmargin=0zw, + xrightmargin=0zw, + framerule=.2pt, + columns=[l]{fullflexible}, + language={}, + tabsize=4, + lineskip=-0.5zw, + escapechar={@}, +} + + \input{dummy.tex} \renewcommand{\abstractname}{Abstract} \begin{document} -\title{Agda言語によるCbC言語の信頼性の保証} -%\title{Supporting NAT in Screen Sharing System TreeVNC} + +\title{CbC言語による検証} + \author{145750B 氏名 {外間}{政尊} 指導教員 : 河野 真治} \date{} -\twocolumn [ + \maketitle -\begin{onecolabstract} -あぶすと -\end{onecolabstract}] -\thispagestyle{fancy} + +\section{研究目的} + +%% Agdaのお勉強のこと、Agdaに直したRedBlackTreeのこと、CbC側のDeletionのこと + +%% CbC でソフトウェアを検証できるかを CbCで書いた RBTree と Agda で同様に書いた RBTree を検証することで示す + +%% ソフトウェアの規模が大きくなるにつれて期待されない動作をすることが増える。ここでは期待される動作を仕様、期待されない動作をバグと呼ぶことにする。 +%% それにはソフトウェアが期待される仕様を満たすか検証する手法と、仕様を直接証明する手法とがある。 +%% 期待される仕様を満たすか検証する手法と、仕様を直接証明する手法とがある。 + +%% 特に実際に動作するソフトウェアを検証、証明できることが望ましい。 +%% そのために当研究室では CodeSegment 、 Data Segment という単位を用いてソフトウェアを記述する手法を提案している。 +%% 処理の単位である CodeSegment は、メタ計算によって相互に接続される。 +%% メタ計算を切り替えることで CodeSegment を変更することなくソフトウェアの性質を検証することができる。 +% CbC検証と実装が同一の言語で行える言語である。 +% CbCの特徴はだいじょうぶ？完全じゃなくていいけどある程度は乗せなきゃ駄目だよね + +ソフトウェアの信頼性を保証することは重要だ。 +現在ソフトウェアの信頼性を保証する方法として代表的なものはモデル検査と、定理証明が存在している。 + +モデル検査はソフトウェアの状態をすべて数え上げ、すべての状態で仕様が正しいことを確認する方法である。 +定理証明はソフトウェアが満たすべき仕様を論理式で記述し、その論理式が恒真であることを証明することである。%% atton-master papar より +モデル検査や、証明でソフトウェアを検証する際、検証に使われる言語と実装に使う言語が異なるという問題がある。 +そのため、二重で同じソフトウェアを記述する必要があるうえ、検証に用いるソースコードは状態が遷移する形で記述する必要があるなど実装されているコードに比べて記述が困難である。 +検証されたコードから実行可能なコードを生成可能な検証系もあるが、生成されたコードが検証のコードと別の言語であったり、既存の実際に対する検証は行えないなどの問題がある。 + +この問題を解決する為に当研究室では検証と実装を同一の言語で行える Continuation based C ( CbC )言語を開発している。 +本研究では、検証や証明に直接使用できる言語として CbC を用いる。 + + %% CbC 上に構築されたプログラムが持つ状態を数え挙げ、仕様を満たすか調べるモデル検査的手法は、比嘉(2016)\cite{Yasutaka:2016}により提案、実装されている。 +%% また、赤黒木の仕様が、限定的な木の大きさの範囲内で検証されている。 + +%% 木の大きさを制限せず実装が仕様を満たすことを示すには証明が必要である。 + +%% プログラムにおける証明は Curry-Howard Isomorphism で型付き $\lambda$計算に対応していることが知られている。 + +しかし、現段階ではCbCでCbC自身を証明することはできない。そのため本研究では依存型を持つ証明支援系 Agda を用いて証明を行なう。 + +%% 部分型を用いて CbC の項を型付けすることで、CbC の形式的定義を型システムより相似的に得る。 + +本研究では CbC を用いて RedBlackTree を実装し、 Insert、Delete などの操作の際に RedBlackTree が常にその仕様を満たせているかを検査、証明することで、 CbC 上で動くプログラムが正しく検証できることを示す。 + +%%検証と証明の話書かないとAgda出せなくない？ + +\section{Countinuation based C (CbC)} +Continuation based C (CbC) とは、当研究室で開発されているプログラミング言語である。 +CbC では OS や組み込みソフトウェアを主な対象としている。 +CbC は C 言語とほぼおなじ構文を持ち、よりアセンブラに近い形でプログラムを記述する。 + +CbC では C の関数の代わりに CodeSegment を用いて処理を記述する。 +CodeSegment は値を入力として受取り、出力を行う処理で、それらの状態を goto で遷移して記述する。この goto による処理の遷移を継続と呼ぶ。 +% 図\ref{fig:CSContinuation}は CodeSegment 感の処理の流れを表している。 + +%%% figure +%% \begin{figure}[htbp] +%% \begin{center} +%% \includegraphics[width=60mm]{../pic/codesegment.pdf} +%% \end{center} +%% \caption{ goto による CodeSegment 間の接続} +%% \label{fig:CSContinuation} +%% \end{figure} + + %% CbC ではこの継続処理にをメタ計算として定義されていて、実装や環境によって切り替えることできる。検証を行うメタ計算を定義することで、 CodeSegment の仕様を変更せずソフトウェアの検証を行う事ができる。 + + +%CbC で Fanctional に書かれた CodeSegment は等価な Agda のコードに置き換えることが可能だと考えている。 + +比嘉(2016)\cite{Yasutaka:2016}では CbC における CodeSegment 、 DataSegment が部分型で定義できることが示されている。 + +これより、 CbC で Fanctional に書かれたプログラムは等価な Agda のコードの置き換えることができる。 + + +\section{Agda} +Agda\cite{agda} とは定理証明支援器であり依存型という強力な型を持つ関数プログラミング言語である。 + +依存型とは型も第一級オブジェクトとする型システムであり、型の型や型を引数に取る関数、値を取って型を返す関数などが記述することができる。 + +型システムは Curry-Howard 同型対応により命題と型付き$\lambda$計算が一対一に対応する。 + +論理式は型に相当し、その型が持つ値の導出が証明となる。 + + + +ここでは A ならば B かつ B ならば C のとき A ならば C が成り立つという三段論法を例にとる。 + +この三段論法を自然演繹による証明木にすると次のようになる。 + +\begin{figure}[htpb] + \begin{center} + \includegraphics[width=95mm]{../pic/modus-ponens.pdf} + \end{center} + \caption{自然演繹での三段論法の証明} + \label{fig:modus-ponens} +\end{figure} + +この証明木に対応するAgdaによる証明は次のようになる。 -\section{せくしょん} -ほんぶん１ +\begin{lstlisting}[basicstyle=\ttfamily\footnotesize, frame=single] + f : {A B C : Set} → ((A → B) × (B → C)) → (A → C) + f = λ {x → (snd p) ((fst p) x)} +\end{lstlisting} + + + +% Agdaの知識ってどう出す？ + +%TODO 定理証明とプログラムの話 + +%% \begin{prooftree} +%% \AxiomC{ $ [A] $ $_{(1)}$} +%% \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ } +%% \RightLabel{ $ \land 1 \mathcal{E} $ } +%% \UnaryInfC{ $ (A \Rightarrow B) $ } +%% \RightLabel{ $ \Rightarrow \mathcal{E} $} +%% \BinaryInfC{ $ B $ } + + +%% \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ } +%% \RightLabel{ $ \land 2 \mathcal{E} $ } +%% \UnaryInfC{ $ (B \Rightarrow C) $ } + +%% \RightLabel{ $ \Rightarrow \mathcal{E} $} +%% \BinaryInfC{ $ C $ } +%% \RightLabel{ $ \Rightarrow \mathcal{I} _{(1)}$} +%% \UnaryInfC{ $ A \Rightarrow C $} +%% \RightLabel{ $ \Rightarrow \mathcal{I} _{(2)}$} +%% \UnaryInfC{ $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $} +%% \end{prooftree} + + +%% Agdaによる三段論法の証明 + +%% 定理証明支援器では Curry-Howard 同型対応により書いた命題通りに書いたプログラムをコンパイルが通ることはその命題を証明することが等しい。 + +現状の CbC では CbC 自身を証明する事ができないため本研究では代わりに等価なAgdaのコードに変換することで証明を行う。 + +CbC から Agda への変換は比嘉(2016)より、DataSegment がrecord型、 CodeSegmentが関数型で定義することが可能である。 +%% 以下に CbC で書かれた Stack の 定義の一部と それを Agda に変換したものの定義の一部分を示す。 +%% push だけじゃなく pop も入れたほうがいい…のかな + +以下にCbC で書かれた Stack の 定義と それを Agda に変換したものの定義を示す。 + +%%% CbCのCodeSegmentの例 + +%% context.h + + +%% \begin{lstlisting}[basicstyle=\ttfamily\footnotesize, frame=single] +%% \end{lstlisting} + + % Stack.agdaのコード +%% \begin{lstlisting}[basicstyle=\ttfamily\footnotesize, frame=single] +%% record Stack {a t : Set} (stackImpl : Set) : Set where +%% field +%% stack : stackImpl +%% push : stackImpl -> a -> (stackImpl -> t) -> t + +%% pushStack : {a t : Set} -> Stack a -> a -> (Stack t -> t) -> t +%% pushStack {a} {t} s0 d next = (push s0) (stack s0) d (\s1 -> next (record {stack = s1} )) +%% \end{lstlisting} + +\newpage +\lstinputlisting[label=src:singlelinked, caption=CbCによるStack]{./src/SingleLinkedStack.cbc.replace} + +\lstinputlisting[label=src:stack-agda, caption=AgdaによるStack]{./src/stack.agda.replace} +%CbC で書かれた Stack の CodeSegment が要素、Tree、 + + + + +\section{RedBlackTree} +RedBlackTree とは拡張された二分探索木で、木のバランスを取るための情報として各ノードにそれぞれ赤、黒の色を持っている。 +RedBlackTree は通常の二分探索木の性質とは別に次のような性質を持っている。 + +\begin{itemize} + \item 各ノードは赤か黒の色を持つ。 + \item ルートノードの色は黒である。 + \item 葉ノードの色は黒である。 + \item 赤ノードは2つの黒ノードを子として持つ(= 赤ノードが続くことは無い)。 + \item ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定である。 +\end{itemize} + +%%また、通常の二分探索木の条件に加えて、各ノードが赤か黒の色を持つ、ルートノードの色は黒、葉ノードの色は黒、赤ノードは二つの黒ノードを子として持つ、ルートから末端のノードへの経路に含まれる黒ノードの数は一定などの条件を持つ。 + +数値を要素に持つ RedBlackTree の例を以下の図\ref{fig:rbtree}に示す。 +条件に示されている通り、ルートノードは黒であり、赤ノードは連続していない。 +加えて各最下位ノードへの経路に含まれる黒ノードの個数は全て2である。 +%% atton-master fig3.1 + +%%%%figure +\begin{figure}[htpb] + \begin{center} + \includegraphics[width=50mm]{../pic/rbtree.pdf} + \end{center} + \caption{RedBlackTreeの例} + \label{fig:rbtree} +\end{figure} + +本研究で検証する RedBlackTree は非破壊であり、一度構築した木構造は破壊される操作ごとに新しい木が生成される。非破壊である理由は並列実行時のデータ保存である。 +%% atton-master@13p + +%% figure %\begin{figure}[htbp] % \begin{center} -% \includegraphics[width=50mm]{./pic/treeVnc.pdf} +% \includegraphics[width=50mm]{../pic/treeVnc.pdf} % \end{center} % \caption{構成される木構造} % \label{fig:tree} %\end{figure} +%% \lstinputlisting[label=src:agda-nat, caption=Agdaにおける自然数の定義] {src/AgdaNat.agda.replaced} + + \section{今後の課題} +現段階では CbC で書かれた RedBlackTree の一部を Agda のコードに変換した。 +今後は CbC での RedBlackTree の Deletion 部分が実装中であることと、Agdaでの証明が未完成である。また、依存型を導入することで CbC で自身を証明できるようにするなどの課題がある。今後はこれらの課題に着手していく。 \nocite{*} \bibliographystyle{junsrt} diff -r d12b2800af6a -r ead50a89470f midterm/modus-ponens/Makefile --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/modus-ponens/Makefile Wed Oct 25 17:35:36 2017 +0900 @@ -0,0 +1,37 @@ +# Settings +TARGET=modus-ponens +BIBTEX=echo # pbibtex +BB=extractbb + +vpath pdf fig +FIGURES=$(wildcard fig/*.pdf) +FIGURES_FOR_TEX=$(subst .pdf,.xbb,$(FIGURES)) + +# dependencies +$(TARGET).pdf : $(TARGET).dvi + dvipdfmx $< + +$(TARGET).dvi : $(wildcard *.tex) $(FIGURES_FOR_TEX) $(SOURCES_FOR_TEX) + platex $(TARGET).tex + $(BIBTEX) $(TARGET) + platex $(TARGET).tex + platex $(TARGET).tex + +%.xbb: %.pdf + $(BB) $< + + +# commands +.PHONY : clean all open remake + +clean: + rm -f *.dvi *.aux *.log *.pdf *.ps *.gz *.bbl *.blg *.toc *~ *.core *.cpt *.lof *.lot *.lol *.bbl *.blg + +all: $(TARGET).pdf + +open: $(TARGET).pdf + open $(TARGET).pdf + +remake: + make clean + make all diff -r d12b2800af6a -r ead50a89470f midterm/modus-ponens/bussproofs.sty --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/modus-ponens/bussproofs.sty Wed Oct 25 17:35:36 2017 +0900 @@ -0,0 +1,1136 @@ +% +\def\BPmessage{Proof Tree (bussproofs) style macros. Version 1.1.} +% bussproofs.sty. Version 1.1 +% (c) 1994,1995,1996,2004,2005,2006, 2011. +% Copyright retained by Samuel R. Buss. +% +% ==== Legal statement: ==== +% 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/1 or later. +% +% This work has the LPPL maintenance status 'maintained'. +% +% The Current Maintainer of the work is Sam Buss. +% +% This work consists of bussproofs.sty. +% ===== +% Informal summary of legal situation: +% This software may be used and distributed freely, except that +% if you make changes, you must change the file name to be different +% than bussproofs.sty to avoid compatibility problems. +% The terms of the LaTeX Public License are the legally controlling terms +% and override any contradictory terms of the "informal situation". +% +% Please report comments and bugs to sbuss@ucsd.edu. +% +% Thanks to Felix Joachimski for making changes to let these macros +% work in plain TeX in addition to LaTeX. Nothing has been done +% to see if they work in AMSTeX. The comments below mostly +% are written for LaTeX, however. +% July 2004, version 0.7 +% - bug fix, right labels with descenders inserted too much space. +% Thanks to Peter Smith for finding this bug, +% see http://www.phil.cam.ac.uk/teaching_staff/Smith/LaTeX/ +% March 2005, version 0.8. +% Added a default definition for \fCenter at Denis Kosygin's +% suggestion. +% September 2005, version 0.9. +% Fixed some subtle spacing problems, by adding %'s to the end of +% few lines where they were inadvertantly omitted. Thanks to +% Arnold Beckmann for finding and fixing this problem. +% April 2006, version 0.9.1. Updated comments and testbp2.tex file. +% No change to the actual macros. +% June 2006, version 1.0. The first integer numbered release. +% New feature: root of proof may now be at the bottom instead of +% at just the top. Thanks to Alex Hertel for the suggestion to implement +% this. +% June 2011, version 1.1. +% New feature: 4-ary and 5-ary inferences. Thanks to Thomas Strathmann +% for taking the initiative to implement these. +% Four new commands: QuaternaryInf(C) and QuinaryInf(C). +% Bug fix: \insertBetweenHyps now works for proofs with root at top and +% three or more hypotheses.. + +% A good exposition of how to use bussproofs.sty (version 0.9) has been written +% by Peter Smith and is available on the internet. +% The comments below also describe the features of bussproofs.sty, +% including user-modifiable parameters. + +% bussproofs.sty allows the construction of proof trees in the +% style of the sequent calculus and many other proof systems +% One novel feature of these macros is they support the horizontal +% alignment according to some center point specified with the +% command \fCenter. This is the style often used in sequent +% calculus proofs. +% Proofs are specified in left-to-right traversal order. +% For example a proof +% A B +% ----- +% D C +% --------- +% E +% +% if given in the order D,A,B,C,E. Each line in the proof is +% specified according to the arity of the inference which generates +% it. Thus, E would be specified with a \BinaryInf or \BinaryInfC +% command. +% +% The above proof tree could be displayed with the commands: +% +% \AxiomC{D} +% \AxiomC{A} +% \AxiomC{B} +% \BinaryInfC{C} +% \BinaryInfC{E} +% \DisplayProof +% +% Inferences in a proof may be nullary (axioms), unary, binary, or +% trinary. +% +% IMPORTANT: You must give the \DisplayProof command to make the proof +% be printed. To display a centered proof on a line by itself, +% put the proof inside \begin{center} ... \end{center}. +% +% There are two styles for specifying horizontal centering of +% lines (formulas or sequents) in a proof. One format \AxiomC{...} +% just centers the formula {...} in the usual way. The other +% format is \Axiom$...\fCenter...$. Here, the \fCenter specifies +% the center of the formula. (It is permissable for \fCenter to +% generate typeset material; in fact, I usually define it to generate +% the sequent arrow.) In unary inferences, the \fCenter +% positions will be vertically aligned in the upper and lower lines of +% the inference. Unary, Binary, Trinary inferences are specified +% with the same format as Axioms. The two styles of centering +% lines may be combined in a single proof. +% +% By using the optional \EnableBpAbbreviations command, various +% abbreviated two or three letter commands are enabled. This allows, +% in particular: +% \AX and \AXC for \Axiom and \AxiomC, (resp.), +% \DP for \DisplayProof, +% \BI and \BIC for \BinaryInf and \BinaryInfC, +% \UI and \UIC for \UnaryInf and \UnaryInfC, +% \TI and \TIC for \TrinaryInf and \TrinaryInfC, +% \LL and \RL for \LeftLabel and \RightLabel. +% See the source code below for additional abbreviations. +% The enabling of these short abbreviations is OPTIONAL, since +% there is the possibility of conflicting with names from other +% macro packages. +% +% By default, the inferences have single horizontal lines (scores) +% This can be overridden using the \doubleLine, \noLine commands. +% These two commands affect only the next inference. You can make +% make a permanent override that applies to the rest of the current +% proof using \alwaysDoubleLine and \alwaysNoLine. \singleLine +% and \alwaysSingleLine work in the analogous way. +% +% The macros do their best to give good placements of for the +% parts of the proof. Several macros allow you to override the +% defaults. These are \insertBetweenHyps{...} which overrides +% the default spacing between hypotheses of Binary and Trinary +% inferences with {...}. And \kernHyps{...} specifies a distance +% to shift the whole block of hypotheses to the right (modifying +% the default center position. +% Other macros set the vertical placement of the whole proof. +% The default is to try to do a good job of placement for inferences +% included in text. Two other useful macros are: \bottomAlignProof +% which aligns the hbox output by \DisplayProof according to the base +% of the bottom line of the proof, and \centerAlignProof which +% does a precise center vertical alignment. +% +% Often, one wishes to place a label next to an inference, usually +% to specify the type of inference. These labels can be placed +% by using the commands \LeftLabel{...} and \RightLabel{...} +% immediately before the command which specifies the inference. +% For example, to generate +% +% A B +% --------- X +% C +% +% use the commands +% \AxiomC{A} +% \AxiomC{B} +% \RightLabel{X} +% \BinaryInfC{C} +% \DisplayProof +% +% The \DisplayProof command just displays the proof as a text +% item. This allows you to put proofs anywhere normal text +% might appear; for example, in a paragraph, in a table, in +% a tabbing environment, etc. When displaying a proof as inline text, +% you should write \DisplayProof{} (with curly brackets) so that +% LaTeX will not "eat" the white space following the \DisplayProof +% command. +% For displaying proofs in a centered display: Do not use the \[...\] +% construction (nor $$...$$). Instead use +% \begin{center} ... \DisplayProof\end{center}. +% Actually there is a better construction to use instead of the +% \begin{center}...\DisplayProof\end{center}. This is to +% write +% \begin{prooftree} ... \end{prooftree}. +% Note there is no \DisplayProof used for this: the +% \end{prooftree} automatically supplies the \DisplayProof +% command. +% +% Warning: Any commands that set line types or set vertical or +% horizontal alignment that are given AFTER the \DisplayProof +% command will affect the next proof, no matter how distant. + + + + +% Usages: +% ======= +% +% \Axiom$\fCenter$ +% +% \AxiomC{\fCenter$ +% +% \UnaryInfC{} +% +% \BinaryInf$\fCenter$ +% +% \BinaryInfC{} +% +% \TrinaryInf$\fCenter$ +% +% \TrinaryInfC{} +% +% \QuaternaryInf$\fCenter$ +% +% \QuaternaryInfC{} +% +% \QuinaryInf$\fCenter$ +% +% \QuinaryInfC{} +% +% \LeftLabel{} - Puts as a label to the left +% of the next inference line. (Works even if +% \noLine is used too.) +% +% \RightLabel{} - Puts as a label to the right of the +% next inference line. (Also works with \noLine.) +% +% \DisplayProof - outputs the whole proof tree (and finishes it). +% The proof tree is output as an hbox. +% +% +% \kernHyps{} - Slides the upper hypotheses right distance +% (This is similar to shifting conclusion left) +% - kernHyps works with Unary, Binary and Trinary +% inferences and with centered or uncentered sequents. +% - Negative values for are permitted. +% +% \insertBetweenHyps{...} - {...} will be inserted between the upper +% hypotheses of a Binary or Trinary Inferences. +% It is possible to use negative horizontal space +% to push them closer together (and even overlap). +% This command affects only the next inference. +% +% \doubleLine - Makes the current (ie, next) horizontal line doubled +% +% \alwaysDoubleLine - Makes lines doubled for rest of proof +% +% \singleLine - Makes the current (ie, next) line single +% +% \alwaysSingleLine - Undoes \alwaysDoubleLine or \alwaysNoLine. +% +% \noLine - Make no line at all at current (ie next) inference. +% +% \alwaysNoLine - Makes no lines for rest of proof. (Untested) +% +% \solidLine - Does solid horizontal line for current inference +% +% \dottedLine - Does dotted horizontal line for current inference +% +% \dashedLine - Does dashed horizontal line for current inference +% +% \alwaysSolidLine - Makes the indicated change in line type, permanently +% \alwaysDashedLine until end of proof or until overridden. +% \alwaysDottedLine +% +% \bottomAlignProof - Vertically align proof according to its bottom line. +% \centerAlignProof - Vertically align proof proof precisely in its center. +% \normalAlignProof - Overrides earlier bottom/center AlignProof commands. +% The default alignment will look good in most cases, +% whether the proof is displayed or is +% in-line. Other alignments may be more +% appropriate when putting proofs in tables or +% pictures, etc. For custom alignments, use +% TeX's raise commands. +% +% \rootAtTop - specifies that proofs have their root a the top. That it, +% proofs will be "upside down". +% \rootAtBottom - (default) Specifies that proofs have root at the bottom +% The \rootAtTop and \rootAtBottom commands apply *only* to the +% current proof. If you want to make them persistent, use one of +% the next two commands: +% \alwaysRootAtTop +% \alwaysRootAtBottom (default) +% + +% Optional short abbreviations for commands: +\def\EnableBpAbbreviations{% + \let\AX\Axiom + \let\AXC\AxiomC + \let\UI\UnaryInf + \let\UIC\UnaryInfC + \let\BI\BinaryInf + \let\BIC\BinaryInfC + \let\TI\TrinaryInf + \let\TIC\TrinaryInfC + \let\QI\QuaternaryInf + \let\QIC\QuaternaryInfC + \let\QuI\QuinaryInf + \let\QuIC\QuinaryInfC + \let\LL\LeftLabel + \let\RL\RightLabel + \let\DP\DisplayProof +} + +% Parameters which control the style of the proof trees. +% The user may wish to override these parameters locally or globally. +% BUT DON'T CHANGE THE PARAMETERS BY CHANGING THIS FILE (to avoid +% future incompatibilities). Instead, you should change them in your +% TeX document right after including this style file in the +% header material of your LaTeX document. + +\def\ScoreOverhang{4pt} % How much underlines extend out +\def\ScoreOverhangLeft{\ScoreOverhang} +\def\ScoreOverhangRight{\ScoreOverhang} + +\def\extraVskip{2pt} % Extra space above and below lines +\def\ruleScoreFiller{\hrule} % Horizontal rule filler. +\def\dottedScoreFiller{\hbox to4pt{\hss.\hss}} +\def\dashedScoreFiller{\hbox to2.8mm{\hss\vrule width1.4mm height0.4pt depth0.0pt\hss}} +\def\defaultScoreFiller{\ruleScoreFiller} % Default horizontal filler. +\def\defaultBuildScore{\buildSingleScore} % In \singleLine mode at start. + +\def\defaultHypSeparation{\hskip.2in} % Used if \insertBetweenHyps isn't given + +\def\labelSpacing{3pt} % Horizontal space separating labels and lines + +\def\proofSkipAmount{\vskip.8ex plus.8ex minus.4ex} + % Space above and below a prooftree display. + +\def\defaultRootPosition{\buildRootBottom} % Default: Proofs root at bottom +%\def\defaultRootPosition{\buildRootTop} % Makes all proofs upside down + +\ifx\fCenter\undefined +\def\fCenter{\relax} +\fi + +% +% End of user-modifiable parameters. +% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% Here are some internal paramenters and defaults. Not really intended +% to be user-modifiable. + +\def\theHypSeparation{\defaultHypSeparation} +\def\alwaysScoreFiller{\defaultScoreFiller} % Horizontal filler. +\def\alwaysBuildScore{\defaultBuildScore} +\def\theScoreFiller{\alwaysScoreFiller} % Horizontal filler. +\def\buildScore{\alwaysBuildScore} %This command builds the score. +\def\hypKernAmt{0pt} % Initial setting for kerning the hypotheses. + +\def\defaultLeftLabel{} +\def\defaultRightLabel{} + +\def\myTrue{Y} +\def\bottomAlignFlag{N} +\def\centerAlignFlag{N} +\def\defaultRootAtBottomFlag{Y} +\def\rootAtBottomFlag{Y} + +% End of internal parameters and defaults. + +\expandafter\ifx\csname newenvironment\endcsname\relax% +% If in TeX: +\message{\BPmessage} +\def\makeatletter{\catcode`\@=11\relax} +\def\makeatother{\catcode`\@=12\relax} +\makeatletter +\def\newcount{\alloc@0\count\countdef\insc@unt} +\def\newdimen{\alloc@1\dimen\dimendef\insc@unt} +\def\newskip{\alloc@2\skip\skipdef\insc@unt} +\def\newbox{\alloc@4\box\chardef\insc@unt} +\makeatother +\else +% If in LaTeX +\typeout{\BPmessage} +\newenvironment{prooftree}% +{\begin{center}\proofSkipAmount \leavevmode}% +{\DisplayProof \proofSkipAmount \end{center} } +\fi + +\def\thecur#1{\csname#1\number\theLevel\endcsname} + +\newcount\theLevel % This counter is the height of the stack. +\global\theLevel=0 % Initialized to zero +\newcount\myMaxLevel +\global\myMaxLevel=0 +\newbox\myBoxA % Temporary storage boxes +\newbox\myBoxB +\newbox\myBoxC +\newbox\myBoxD +\newbox\myBoxLL % Boxes for the left label and the right label. +\newbox\myBoxRL +\newdimen\thisAboveSkip %Internal use: amount to skip above line +\newdimen\thisBelowSkip %Internal use: amount to skip below line +\newdimen\newScoreStart % More temporary storage. +\newdimen\newScoreEnd +\newdimen\newCenter +\newdimen\displace +\newdimen\leftLowerAmt% Amount to lower left label +\newdimen\rightLowerAmt% Amount to lower right label +\newdimen\scoreHeight% Score height +\newdimen\scoreDepth% Score Depth +\newdimen\htLbox% +\newdimen\htRbox% +\newdimen\htRRbox% +\newdimen\htRRRbox% +\newdimen\htAbox% +\newdimen\htCbox% + +\setbox\myBoxLL=\hbox{\defaultLeftLabel}% +\setbox\myBoxRL=\hbox{\defaultRightLabel}% + +\def\allocatemore{% + \ifnum\theLevel>\myMaxLevel% + \expandafter\newbox\curBox% + \expandafter\newdimen\curScoreStart% + \expandafter\newdimen\curCenter% + \expandafter\newdimen\curScoreEnd% + \global\advance\myMaxLevel by1% + \fi% +} + +\def\prepAxiom{% + \advance\theLevel by1% + \edef\curBox{\thecur{myBox}}% + \edef\curScoreStart{\thecur{myScoreStart}}% + \edef\curCenter{\thecur{myCenter}}% + \edef\curScoreEnd{\thecur{myScoreEnd}}% + \allocatemore% +} + +\def\Axiom$#1\fCenter#2${% + % Get level and correct names set. + \prepAxiom% + % Define the boxes + \setbox\myBoxA=\hbox{$\mathord{#1}\fCenter\mathord{\relax}$}% + \setbox\myBoxB=\hbox{$#2$}% + \global\setbox\curBox=% + \hbox{\hskip\ScoreOverhangLeft\relax% + \unhcopy\myBoxA\unhcopy\myBoxB\hskip\ScoreOverhangRight\relax}% + % Set the relevant dimensions for the boxes + \global\curScoreStart=0pt \relax + \global\curScoreEnd=\wd\curBox \relax + \global\curCenter=\wd\myBoxA \relax + \global\advance \curCenter by \ScoreOverhangLeft% + \ignorespaces +} + +\def\AxiomC#1{ % Note argument not in math mode + % Get level and correct names set. + \prepAxiom% + % Define the box. + \setbox\myBoxA=\hbox{#1}% + \global\setbox\curBox =% + \hbox{\hskip\ScoreOverhangLeft\relax% + \unhcopy\myBoxA\hskip\ScoreOverhangRight\relax}% + % Set the relevant dimensions for the boxes + \global\curScoreStart=0pt \relax + \global\curScoreEnd=\wd\curBox \relax + \global\curCenter=.5\wd\curBox \relax + \global\advance \curCenter by \ScoreOverhangLeft% + \ignorespaces +} + +\def\prepUnary{% + \ifnum \theLevel<1 + \errmessage{Hypotheses missing!} + \fi% + \edef\curBox{\thecur{myBox}}% + \edef\curScoreStart{\thecur{myScoreStart}}% + \edef\curCenter{\thecur{myCenter}}% + \edef\curScoreEnd{\thecur{myScoreEnd}}% +} + +\def\UnaryInf$#1\fCenter#2${% + \prepUnary% + \buildConclusion{#1}{#2}% + \joinUnary% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\UnaryInfC#1{ + \prepUnary% + \buildConclusionC{#1}% + %Align and join the curBox and the new box into one vbox. + \joinUnary% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\prepBinary{% + \ifnum\theLevel<2 + \errmessage{Hypotheses missing!} + \fi% + \edef\rcurBox{\thecur{myBox}}% Set up names of right hypothesis + \edef\rcurScoreStart{\thecur{myScoreStart}}% + \edef\rcurCenter{\thecur{myCenter}}% + \edef\rcurScoreEnd{\thecur{myScoreEnd}}% + \advance\theLevel by-1% + \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis + \edef\lcurScoreStart{\thecur{myScoreStart}}% + \edef\lcurCenter{\thecur{myCenter}}% + \edef\lcurScoreEnd{\thecur{myScoreEnd}}% +} + +\def\BinaryInf$#1\fCenter#2${% + \prepBinary% + \buildConclusion{#1}{#2}% + \joinBinary% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\BinaryInfC#1{% + \prepBinary% + \buildConclusionC{#1}% + \joinBinary% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\prepTrinary{% + \ifnum\theLevel<3 + \errmessage{Hypotheses missing!} + \fi% + \edef\rcurBox{\thecur{myBox}}% Set up names of right hypothesis + \edef\rcurScoreStart{\thecur{myScoreStart}}% + \edef\rcurCenter{\thecur{myCenter}}% + \edef\rcurScoreEnd{\thecur{myScoreEnd}}% + \advance\theLevel by-1% + \edef\ccurBox{\thecur{myBox}}% Set up names of center hypothesis + \edef\ccurScoreStart{\thecur{myScoreStart}}% + \edef\ccurCenter{\thecur{myCenter}}% + \edef\ccurScoreEnd{\thecur{myScoreEnd}}% + \advance\theLevel by-1% + \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis + \edef\lcurScoreStart{\thecur{myScoreStart}}% + \edef\lcurCenter{\thecur{myCenter}}% + \edef\lcurScoreEnd{\thecur{myScoreEnd}}% +} + +\def\TrinaryInf$#1\fCenter#2${% + \prepTrinary% + \buildConclusion{#1}{#2}% + \joinTrinary% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\TrinaryInfC#1{% + \prepTrinary% + \buildConclusionC{#1}% + \joinTrinary% + \resetInferenceDefaults% + \ignorespaces% +} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\def\prepQuaternary{% + \ifnum\theLevel<4 + \errmessage{Hypotheses missing!} + \fi% + \edef\rrcurBox{\thecur{myBox}}% Set up names of very right hypothesis + \edef\rrcurScoreStart{\thecur{myScoreStart}}% + \edef\rrcurCenter{\thecur{myCenter}}% + \edef\rrcurScoreEnd{\thecur{myScoreEnd}}% + \advance\theLevel by-1% + \edef\rcurBox{\thecur{myBox}}% Set up names of right hypothesis + \edef\rcurScoreStart{\thecur{myScoreStart}}% + \edef\rcurCenter{\thecur{myCenter}}% + \edef\rcurScoreEnd{\thecur{myScoreEnd}}% + \advance\theLevel by-1% + \edef\ccurBox{\thecur{myBox}}% Set up names of center hypothesis + \edef\ccurScoreStart{\thecur{myScoreStart}}% + \edef\ccurCenter{\thecur{myCenter}}% + \edef\ccurScoreEnd{\thecur{myScoreEnd}}% + \advance\theLevel by-1% + \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis + \edef\lcurScoreStart{\thecur{myScoreStart}}% + \edef\lcurCenter{\thecur{myCenter}}% + \edef\lcurScoreEnd{\thecur{myScoreEnd}}% +} + +\def\QuaternaryInf$#1\fCenter#2${% + \prepQuaternary% + \buildConclusion{#1}{#2}% + \joinQuaternary% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\QuaternaryInfC#1{% + \prepQuaternary% + \buildConclusionC{#1}% + \joinQuaternary% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\joinQuaternary{% Construct the quarterary inference into a vbox. + % Join the four hypotheses's boxes into one hbox. + \setbox\myBoxA=\hbox{\theHypSeparation}% + \lcurScoreEnd=\rrcurScoreEnd% + \advance\lcurScoreEnd by\wd\rcurBox% + \advance\lcurScoreEnd by\wd\lcurBox% + \advance\lcurScoreEnd by\wd\ccurBox% + \advance\lcurScoreEnd by3\wd\myBoxA% + \displace=\lcurScoreEnd% + \advance\displace by -\lcurScoreStart% + \lcurCenter=.5\displace% + \advance\lcurCenter by\lcurScoreStart% + \ifx\rootAtBottomFlag\myTrue% + \setbox\lcurBox=% + \hbox{\box\lcurBox\unhcopy\myBoxA\box\ccurBox% + \unhcopy\myBoxA\box\rcurBox + \unhcopy\myBoxA\box\rrcurBox}% + \else% + \htLbox = \ht\lcurBox% + \htAbox = \ht\myBoxA% + \htCbox = \ht\ccurBox% + \htRbox = \ht\rcurBox% + \htRRbox = \ht\rrcurBox% + \setbox\lcurBox=% + \hbox{\lower\htLbox\box\lcurBox% + \lower\htAbox\copy\myBoxA\lower\htCbox\box\ccurBox% + \lower\htAbox\copy\myBoxA\lower\htRbox\box\rcurBox% + \lower\htAbox\copy\myBoxA\lower\htRRbox\box\rrcurBox}% + \fi% + % Adjust center of upper hypotheses according to how much + % the lower sequent is off-center. + \displace=\newCenter% + \advance\displace by -.5\newScoreStart% + \advance\displace by -.5\newScoreEnd% + \advance\lcurCenter by \displace% + %Align and join the curBox and the two hypotheses's box into one vbox. + \edef\curBox{\lcurBox}% + \edef\curScoreStart{\lcurScoreStart}% + \edef\curScoreEnd{\lcurScoreEnd}% + \edef\curCenter{\lcurCenter}% + \joinUnary% +} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\def\prepQuinary{% + \ifnum\theLevel<5 + \errmessage{Hypotheses missing!} + \fi% + \edef\rrrcurBox{\thecur{myBox}}% Set up names of very very right hypothesis + \edef\rrrcurScoreStart{\thecur{myScoreStart}}% + \edef\rrrcurCenter{\thecur{myCenter}}% + \edef\rrrcurScoreEnd{\thecur{myScoreEnd}}% + \advance\theLevel by-1% + \edef\rrcurBox{\thecur{myBox}}% Set up names of very right hypothesis + \edef\rrcurScoreStart{\thecur{myScoreStart}}% + \edef\rrcurCenter{\thecur{myCenter}}% + \edef\rrcurScoreEnd{\thecur{myScoreEnd}}% + \advance\theLevel by-1% + \edef\rcurBox{\thecur{myBox}}% Set up names of right hypothesis + \edef\rcurScoreStart{\thecur{myScoreStart}}% + \edef\rcurCenter{\thecur{myCenter}}% + \edef\rcurScoreEnd{\thecur{myScoreEnd}}% + \advance\theLevel by-1% + \edef\ccurBox{\thecur{myBox}}% Set up names of center hypothesis + \edef\ccurScoreStart{\thecur{myScoreStart}}% + \edef\ccurCenter{\thecur{myCenter}}% + \edef\ccurScoreEnd{\thecur{myScoreEnd}}% + \advance\theLevel by-1% + \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis + \edef\lcurScoreStart{\thecur{myScoreStart}}% + \edef\lcurCenter{\thecur{myCenter}}% + \edef\lcurScoreEnd{\thecur{myScoreEnd}}% +} + +\def\QuinaryInf$#1\fCenter#2${% + \prepQuinary% + \buildConclusion{#1}{#2}% + \joinQuinary% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\QuinaryInfC#1{% + \prepQuinary% + \buildConclusionC{#1}% + \joinQuinary% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\joinQuinary{% Construct the quinary inference into a vbox. + % Join the five hypotheses's boxes into one hbox. + \setbox\myBoxA=\hbox{\theHypSeparation}% + \lcurScoreEnd=\rrrcurScoreEnd% + \advance\lcurScoreEnd by\wd\rrcurBox% + \advance\lcurScoreEnd by\wd\rcurBox% + \advance\lcurScoreEnd by\wd\lcurBox% + \advance\lcurScoreEnd by\wd\ccurBox% + \advance\lcurScoreEnd by4\wd\myBoxA% + \displace=\lcurScoreEnd% + \advance\displace by -\lcurScoreStart% + \lcurCenter=.5\displace% + \advance\lcurCenter by\lcurScoreStart% + \ifx\rootAtBottomFlag\myTrue% + \setbox\lcurBox=% + \hbox{\box\lcurBox\unhcopy\myBoxA\box\ccurBox% + \unhcopy\myBoxA\box\rcurBox + \unhcopy\myBoxA\box\rrcurBox + \unhcopy\myBoxA\box\rrrcurBox}% + \else% + \htLbox = \ht\lcurBox% + \htAbox = \ht\myBoxA% + \htCbox = \ht\ccurBox% + \htRbox = \ht\rcurBox% + \htRRbox = \ht\rrcurBox% + \htRRRbox = \ht\rrrcurBox% + \setbox\lcurBox=% + \hbox{\lower\htLbox\box\lcurBox% + \lower\htAbox\copy\myBoxA\lower\htCbox\box\ccurBox% + \lower\htAbox\copy\myBoxA\lower\htRbox\box\rcurBox% + \lower\htAbox\copy\myBoxA\lower\htRRbox\box\rrcurBox% + \lower\htAbox\copy\myBoxA\lower\htRRRbox\box\rrrcurBox}% + \fi% + % Adjust center of upper hypotheses according to how much + % the lower sequent is off-center. + \displace=\newCenter% + \advance\displace by -.5\newScoreStart% + \advance\displace by -.5\newScoreEnd% + \advance\lcurCenter by \displace% + %Align and join the curBox and the two hypotheses's box into one vbox. + \edef\curBox{\lcurBox}% + \edef\curScoreStart{\lcurScoreStart}% + \edef\curScoreEnd{\lcurScoreEnd}% + \edef\curCenter{\lcurCenter}% + \joinUnary% +} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\def\buildConclusion#1#2{% Build lower sequent w/ center at \fCenter position. + % Define the boxes + \setbox\myBoxA=\hbox{$\mathord{#1}\fCenter\mathord{\relax}$}% + \setbox\myBoxB=\hbox{$#2$}% + % Put them together in \myBoxC + \setbox\myBoxC =% + \hbox{\hskip\ScoreOverhangLeft\relax% + \unhcopy\myBoxA\unhcopy\myBoxB\hskip\ScoreOverhangRight\relax}% + % Calculate the center of the \myBoxC string. + \newScoreStart=0pt \relax% + \newCenter=\wd\myBoxA \relax% + \advance \newCenter by \ScoreOverhangLeft% + \newScoreEnd=\wd\myBoxC% +} + +\def\buildConclusionC#1{% Build lower sequent w/o \fCenter present. + % Define the box. + \setbox\myBoxA=\hbox{#1}% + \setbox\myBoxC =% + \hbox{\hbox{\hskip\ScoreOverhangLeft\relax% + \unhcopy\myBoxA\hskip\ScoreOverhangRight\relax}}% + % Calculate kerning to line up centers + \newScoreStart=0pt \relax% + \newCenter=.5\wd\myBoxC \relax% + \newScoreEnd=\wd\myBoxC% + \advance \newCenter by \ScoreOverhangLeft% +} + +\def\joinUnary{%Align and join \curBox and \myBoxC into a single vbox + \global\advance\curCenter by -\hypKernAmt% + \ifnum\curCenter<\newCenter% + \displace=\newCenter% + \advance \displace by -\curCenter% + \kernUpperBox% + \else% + \displace=\curCenter% + \advance \displace by -\newCenter% + \kernLowerBox% + \fi% + \ifnum \newScoreStart < \curScoreStart % + \global \curScoreStart = \newScoreStart \fi% + \ifnum \curScoreEnd < \newScoreEnd % + \global \curScoreEnd = \newScoreEnd \fi% + % Leave room for the left label. + \ifnum \curScoreStart<\wd\myBoxLL% + \global\displace = \wd\myBoxLL% + \global\advance\displace by -\curScoreStart% + \kernUpperBox% + \kernLowerBox% + \fi% + % Draw the score + \buildScore% + % Form the score and labels into a box. + \buildScoreLabels% + % Form the new box and its dimensions + \ifx\rootAtBottomFlag\myTrue% + \buildRootBottom% + \else% + \buildRootTop% + \fi% + \global \curScoreStart=\newScoreStart% + \global \curScoreEnd=\newScoreEnd% + \global \curCenter=\newCenter% +} + +\def\buildRootBottom{% + \global \setbox \curBox =% + \vbox{\box\curBox% + \vskip\thisAboveSkip \relax% + \nointerlineskip\box\myBoxD% + \vskip\thisBelowSkip \relax% + \nointerlineskip\box\myBoxC}% +} + +\def\buildRootTop{% + \global \setbox \curBox =% + \vbox{\box\myBoxC% + \vskip\thisAboveSkip \relax% + \nointerlineskip\box\myBoxD% + \vskip\thisBelowSkip \relax% + \nointerlineskip\box\curBox}% +} + +\def\kernUpperBox{% + \global\setbox\curBox =% + \hbox{\hskip\displace\box\curBox}% + \global\advance \curScoreStart by \displace% + \global\advance \curScoreEnd by \displace% + \global\advance\curCenter by \displace% +} + +\def\kernLowerBox{% + \global\setbox\myBoxC =% + \hbox{\hskip\displace\unhbox\myBoxC}% + \global\advance \newScoreStart by \displace% + \global\advance \newScoreEnd by \displace% + \global\advance\newCenter by \displace% +} + +\def\joinBinary{% Construct the binary inference into a vbox. + % Join the two hypotheses's boxes into one hbox. + \setbox\myBoxA=\hbox{\theHypSeparation}% + \lcurScoreEnd=\rcurScoreEnd% + \advance\lcurScoreEnd by\wd\lcurBox% + \advance\lcurScoreEnd by\wd\myBoxA% + \displace=\lcurScoreEnd% + \advance\displace by -\lcurScoreStart% + \lcurCenter=.5\displace% + \advance\lcurCenter by\lcurScoreStart% + \ifx\rootAtBottomFlag\myTrue% + \setbox\lcurBox=% + \hbox{\box\lcurBox\unhcopy\myBoxA\box\rcurBox}% + \else% + \htLbox = \ht\lcurBox% + \htAbox = \ht\myBoxA% + \htRbox = \ht\rcurBox% + \setbox\lcurBox=% + \hbox{\lower\htLbox\box\lcurBox% + \lower\htAbox\box\myBoxA\lower\htRbox\box\rcurBox}% + \fi% + % Adjust center of upper hypotheses according to how much + % the lower sequent is off-center. + \displace=\newCenter% + \advance\displace by -.5\newScoreStart% + \advance\displace by -.5\newScoreEnd% + \advance\lcurCenter by \displace% + %Align and join the curBox and the two hypotheses's box into one vbox. + \edef\curBox{\lcurBox}% + \edef\curScoreStart{\lcurScoreStart}% + \edef\curScoreEnd{\lcurScoreEnd}% + \edef\curCenter{\lcurCenter}% + \joinUnary% +} + +\def\joinTrinary{% Construct the trinary inference into a vbox. + % Join the three hypotheses's boxes into one hbox. + \setbox\myBoxA=\hbox{\theHypSeparation}% + \lcurScoreEnd=\rcurScoreEnd% + \advance\lcurScoreEnd by\wd\lcurBox% + \advance\lcurScoreEnd by\wd\ccurBox% + \advance\lcurScoreEnd by2\wd\myBoxA% + \displace=\lcurScoreEnd% + \advance\displace by -\lcurScoreStart% + \lcurCenter=.5\displace% + \advance\lcurCenter by\lcurScoreStart% + \ifx\rootAtBottomFlag\myTrue% + \setbox\lcurBox=% + \hbox{\box\lcurBox\unhcopy\myBoxA\box\ccurBox% + \unhcopy\myBoxA\box\rcurBox}% + \else% + \htLbox = \ht\lcurBox% + \htAbox = \ht\myBoxA% + \htCbox = \ht\ccurBox% + \htRbox = \ht\rcurBox% + \setbox\lcurBox=% + \hbox{\lower\htLbox\box\lcurBox% + \lower\htAbox\copy\myBoxA\lower\htCbox\box\ccurBox% + \lower\htAbox\copy\myBoxA\lower\htRbox\box\rcurBox}% + \fi% + % Adjust center of upper hypotheses according to how much + % the lower sequent is off-center. + \displace=\newCenter% + \advance\displace by -.5\newScoreStart% + \advance\displace by -.5\newScoreEnd% + \advance\lcurCenter by \displace% + %Align and join the curBox and the two hypotheses's box into one vbox. + \edef\curBox{\lcurBox}% + \edef\curScoreStart{\lcurScoreStart}% + \edef\curScoreEnd{\lcurScoreEnd}% + \edef\curCenter{\lcurCenter}% + \joinUnary% +} + +\def\DisplayProof{% + % Display (and purge) the proof tree. + % Choose the appropriate vertical alignment. + \ifnum \theLevel=1 \relax \else%x + \errmessage{Proof tree badly specified.}% + \fi% + \edef\curBox{\thecur{myBox}}% + \ifx\bottomAlignFlag\myTrue% + \displace=0pt% + \else% + \displace=.5\ht\curBox% + \ifx\centerAlignFlag\myTrue\relax + \else% + \advance\displace by -3pt% + \fi% + \fi% + \leavevmode% + \lower\displace\hbox{\copy\curBox}% + \global\theLevel=0% + \global\def\alwaysBuildScore{\defaultBuildScore}% Restore "always" + \global\def\alwaysScoreFiller{\defaultScoreFiller}% Restore "always" + \global\def\bottomAlignFlag{N}% + \global\def\centerAlignFlag{N}% + \resetRootPosition + \resetInferenceDefaults% + \ignorespaces +} + +\def\buildSingleScore{% Make an hbox with a single score. + \displace=\curScoreEnd% + \advance \displace by -\curScoreStart% + \global\setbox \myBoxD =% + \hbox to \displace{\expandafter\xleaders\theScoreFiller\hfill}% + %\global\setbox \myBoxD =% + %\hbox{\hskip\curScoreStart\relax \box\myBoxD}% +} + +\def\buildDoubleScore{% Make an hbox with a double score. + \buildSingleScore% + \global\setbox\myBoxD=% + \hbox{\hbox to0pt{\copy\myBoxD\hss}\raise2pt\copy\myBoxD}% +} + +\def\buildNoScore{% Make an hbox with no score (raise a little anyway) + \global\setbox\myBoxD=\hbox{\vbox{\vskip1pt}}% +} + +\def\doubleLine{% + \gdef\buildScore{\buildDoubleScore}% Set next score to this type + \ignorespaces +} +\def\alwaysDoubleLine{% + \gdef\alwaysBuildScore{\buildDoubleScore}% Do double for rest of proof. + \gdef\buildScore{\buildDoubleScore}% Set next score to be double + \ignorespaces +} +\def\singleLine{% + \gdef\buildScore{\buildSingleScore}% Set next score to be single + \ignorespaces +} +\def\alwaysSingleLine{% + \gdef\alwaysBuildScore{\buildSingleScore}% Do single for rest of proof. + \gdef\buildScore{\buildSingleScore}% Set next score to be single + \ignorespaces +} +\def\noLine{% + \gdef\buildScore{\buildNoScore}% Set next score to this type + \ignorespaces +} +\def\alwaysNoLine{% + \gdef\alwaysBuildScore{\buildNoScore}%Do nolines for rest of proof. + \gdef\buildScore{\buildNoScore}% Set next score to be blank + \ignorespaces +} +\def\solidLine{% + \gdef\theScoreFiller{\ruleScoreFiller}% Use solid horizontal line. + \ignorespaces +} +\def\alwaysSolidLine{% + \gdef\alwaysScoreFiller{\ruleScoreFiller}% Do solid for rest of proof + \gdef\theScoreFiller{\ruleScoreFiller}% Use solid horizontal line. + \ignorespaces +} +\def\dottedLine{% + \gdef\theScoreFiller{\dottedScoreFiller}% Use dotted horizontal line. + \ignorespaces +} +\def\alwaysDottedLine{% + \gdef\alwaysScoreFiller{\dottedScoreFiller}% Do dotted for rest of proof + \gdef\theScoreFiller{\dottedScoreFiller}% Use dotted horizontal line. + \ignorespaces +} +\def\dashedLine{% + \gdef\theScoreFiller{\dashedScoreFiller}% Use dashed horizontal line. + \ignorespaces +} +\def\alwaysDashedLine{% + \gdef\alwaysScoreFiller{\dashedScoreFiller}% Do dashed for rest of proof + \gdef\theScoreFiller{\dashedScoreFiller}% Use dashed horizontal line. + \ignorespaces +} +\def\kernHyps#1{% + \gdef\hypKernAmt{#1}% + \ignorespaces +} +\def\insertBetweenHyps#1{% + \gdef\theHypSeparation{#1}% + \ignorespaces +} + +\def\centerAlignProof{% + \def\centerAlignFlag{Y}% + \def\bottomAlignFlag{N}% + \ignorespaces +} +\def\bottomAlignProof{% + \def\centerAlignFlag{N}% + \def\bottomAlignFlag{Y}% + \ignorespaces +} +\def\normalAlignProof{% + \def\centerAlignFlag{N}% + \def\bottomAlignFlag{N}% + \ignorespaces +} + +\def\LeftLabel#1{% + \global\setbox\myBoxLL=\hbox{{#1}\hskip\labelSpacing}% + \ignorespaces +} +\def\RightLabel#1{% + \global\setbox\myBoxRL=\hbox{\hskip\labelSpacing #1}% + \ignorespaces +} + +\def\buildScoreLabels{% + \scoreHeight = \ht\myBoxD% + \scoreDepth = \dp\myBoxD% + \leftLowerAmt=\ht\myBoxLL% + \advance \leftLowerAmt by -\dp\myBoxLL% + \advance \leftLowerAmt by -\scoreHeight% + \advance \leftLowerAmt by \scoreDepth% + \leftLowerAmt=.5\leftLowerAmt% + \rightLowerAmt=\ht\myBoxRL% + \advance \rightLowerAmt by -\dp\myBoxRL% + \advance \rightLowerAmt by -\scoreHeight% + \advance \rightLowerAmt by \scoreDepth% + \rightLowerAmt=.5\rightLowerAmt% + \displace = \curScoreStart% + \advance\displace by -\wd\myBoxLL% + \global\setbox\myBoxD =% + \hbox{\hskip\displace% + \lower\leftLowerAmt\copy\myBoxLL% + \box\myBoxD% + \lower\rightLowerAmt\copy\myBoxRL}% + \global\thisAboveSkip = \ht\myBoxLL% + \global\advance \thisAboveSkip by -\leftLowerAmt% + \global\advance \thisAboveSkip by -\scoreHeight% + \ifnum \thisAboveSkip<0 % + \global\thisAboveSkip=0pt% + \fi% + \displace = \ht\myBoxRL% + \advance \displace by -\rightLowerAmt% + \advance \displace by -\scoreHeight% + \ifnum \displace<0 % + \displace=0pt% + \fi% + \ifnum \displace>\thisAboveSkip % + \global\thisAboveSkip=\displace% + \fi% + \global\thisBelowSkip = \dp\myBoxLL% + \global\advance\thisBelowSkip by \leftLowerAmt% + \global\advance\thisBelowSkip by -\scoreDepth% + \ifnum\thisBelowSkip<0 % + \global\thisBelowSkip = 0pt% + \fi% + \displace = \dp\myBoxRL% + \advance\displace by \rightLowerAmt% + \advance\displace by -\scoreDepth% + \ifnum\displace<0 % + \displace = 0pt% + \fi% + \ifnum\displace>\thisBelowSkip% + \global\thisBelowSkip = \displace% + \fi% + \global\thisAboveSkip = -\thisAboveSkip% + \global\thisBelowSkip = -\thisBelowSkip% + \global\advance\thisAboveSkip by\extraVskip% Extra space above line + \global\advance\thisBelowSkip by\extraVskip% Extra space below line +} + +\def\resetInferenceDefaults{% + \global\def\theHypSeparation{\defaultHypSeparation}% + \global\setbox\myBoxLL=\hbox{\defaultLeftLabel}% + \global\setbox\myBoxRL=\hbox{\defaultRightLabel}% + \global\def\buildScore{\alwaysBuildScore}% + \global\def\theScoreFiller{\alwaysScoreFiller}% + \gdef\hypKernAmt{0pt}% Restore to zero kerning. +} + + +\def\rootAtBottom{% + \global\def\rootAtBottomFlag{Y}% +} + +\def\rootAtTop{% + \global\def\rootAtBottomFlag{N}% +} + +\def\resetRootPosition{% + \global\edef\rootAtBottomFlag{\defaultRootAtBottomFlag} +} + +\def\alwaysRootAtBottom{% + \global\def\defaultRootAtBottomFlag{Y} + \rootAtBottom +} + +\def\alwaysRootAtTop{% + \global\def\defaultRootAtBottomFlag{N} + \rootAtTop +} + + diff -r d12b2800af6a -r ead50a89470f midterm/modus-ponens/modus-ponens.pdf Binary file midterm/modus-ponens/modus-ponens.pdf has changed diff -r d12b2800af6a -r ead50a89470f midterm/modus-ponens/modus-ponens.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/modus-ponens/modus-ponens.svg Wed Oct 25 17:35:36 2017 +0900 @@ -0,0 +1,322 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff -r d12b2800af6a -r ead50a89470f midterm/modus-ponens/modus-ponens.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/modus-ponens/modus-ponens.tex Wed Oct 25 17:35:36 2017 +0900 @@ -0,0 +1,56 @@ +% {{{ settings +% vim:set fileencoding=utf8: +\documentclass[10pt]{jarticle} + +\usepackage{amsmath} +\usepackage{cprotect} +\usepackage{listings} +\usepackage{moreverb} +\usepackage{url} +\usepackage{bussproofs} +\usepackage[dvipdfmx]{graphicx} + +% equation number with section number +\makeatletter +\renewcommand{\theequation}{\arabic{section}-\arabic{equation}} +\@addtoreset{equation}{section} +\makeatother + +\setlength{\textwidth}{179mm} +\setlength{\textheight}{251mm} +\setlength{\topmargin}{-2cm} +\setlength{\oddsidemargin}{-1cm} +\setlength{\evensidemargin}{-1cm} + +% }}} + +\pagenumbering{gobble} + +\begin{document} + +\title{} +\author{} +\date{} + +\begin{prooftree} + \AxiomC{ $ [A] $ $_{(1)}$} + \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ } + \RightLabel{ $ \land 1 \mathcal{E} $ } + \UnaryInfC{ $ (A \Rightarrow B) $ } + \RightLabel{ $ \Rightarrow \mathcal{E} $} + \BinaryInfC{ $ B $ } + + \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ } + \RightLabel{ $ \land 2 \mathcal{E} $ } + \UnaryInfC{ $ (B \Rightarrow C) $ } + + \RightLabel{ $ \Rightarrow \mathcal{E} $} + \BinaryInfC{ $ C $ } + \RightLabel{ $ \Rightarrow \mathcal{I} _{(1)}$} + \UnaryInfC{ $ A \Rightarrow C $} + \RightLabel{ $ \Rightarrow \mathcal{I} _{(2)}$} + \UnaryInfC{ $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $} +\end{prooftree} + +\end{document} + diff -r d12b2800af6a -r ead50a89470f midterm/reference.bib --- a/midterm/reference.bib Mon Oct 16 23:07:05 2017 +0900 +++ b/midterm/reference.bib Wed Oct 25 17:35:36 2017 +0900 @@ -1,11 +1,33 @@ +@Misc{Yasutaka:2016, + author = "{比嘉 健太, 河野 真治}", + title = "{メタ計算を用いた Continuation based C の検証手法}", + journal = "琉球大学工学部情報工学科平成 28 年度学位論文", + year = 2016 +} + +@Misc{Tatsuki:2016, + author = "{伊波 立樹, 東恩納 琢偉, 河野 真治}", + title = "{Code Gear 、Data Gear に基づく OS のプロトタイプ}", + journal = "{情報処理学会システムソフトウェアとオペレーティングシステム研究会}", + year = 2016 +} + @Misc{kaito:2015, - author = "{徳森 海斗, 河野真治}", - title = "LLVM Clang 上の Continuation based C コンパイラ の改良", - journal = "琉球大学工学部情報工学科平成 27 年度学位論文", + author = "{徳森 海斗, 河野 真治}", + title = "{LLVM Clang 上の Continuation based C コンパイラ の改良}", + journal = "{琉球大学工学部情報工学科平成 27 年度学位論文}", year = 2015 } -@Misc{llvm, - author = "{The LLVM Compiler Infrastructure}", - howpublished = "\url{http://llvm.org}" +@misc{agda, + title = {The Agda wiki}, + howpublished = {\url{http://wiki.portal.chalmers.se/agda/pmwiki.php}}, + note = {Accessed: 2017/10/24(Tue)} } + + +@misc{agda-documentation, + title = {Welcome to Agda’s documentation! — Agda 2.6.0 documentation}, + howpublished = {\url{http://agda.readthedocs.io/en/latest/index.html}}, + note = {Accessed: 2017/10/24(Tue)} +} \ No newline at end of file diff -r d12b2800af6a -r ead50a89470f midterm/src/SingleLinkedStack.cbc --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/src/SingleLinkedStack.cbc Wed Oct 25 17:35:36 2017 +0900 @@ -0,0 +1,32 @@ +__code pushSingleLinkedStack(struct Single LinkedStack* stack,union Data* data, __code next(...)) { + Element* element = new Element(); + element->next = stack->top; + element->data = data; + stack->top = element; + goto next(...); +} +__code popSingleLinkedStack(struct Single LinkedStack* stack, __code next(union Data* data, ...)) { + if (stack->top) { + data = stack->top->data; + stack->top = stack->top->next; + } else { + data = NULL; + } + goto next(data, ...); +} + +__code pop2SingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, union Data* data1, ...)) { + if (stack->top) { + data = stack->top->data; + stack->top = stack->top->next; + } else { + data = NULL; + } + if (stack->top) { + data1 = stack->top->data; + stack->top = stack->top->next; + } else { + data1 = NULL; + } + goto next(data, data1, ...); +} \ No newline at end of file diff -r d12b2800af6a -r ead50a89470f midterm/src/SingleLinkedStack.cbc.replace --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/src/SingleLinkedStack.cbc.replace Wed Oct 25 17:35:36 2017 +0900 @@ -0,0 +1,16 @@ +__code pushSingleLinkedStack(struct Single LinkedStack* stack,union Data* data, __code next(...)) { + Element* element = new Element(); + element->next = stack->top; + element->data = data; + stack->top = element; + goto next(...); +} +__code popSingleLinkedStack(struct Single LinkedStack* stack, __code next(union Data* data, ...)) { + if (stack->top) { + data = stack->top->data; + stack->top = stack->top->next; + } else { + data = NULL; + } + goto next(data, ...); +} diff -r d12b2800af6a -r ead50a89470f midterm/src/push-pop.cbc --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/src/push-pop.cbc Wed Oct 25 17:35:36 2017 +0900 @@ -0,0 +1,32 @@ + __code pushSingleLinkedStack(struct Single LinkedStack* stack,union Data* data, __code next(...)) { + Element* element = new Element(); + element->next = stack->top; + element->data = data; + stack->top = element; + goto next(...); +} + __code popSingleLinkedStack(struct Single LinkedStack* stack, __code next(union Data* data, ...)) { + if (stack->top) { + data = stack->top->data; + stack->top = stack->top->next; + } else { + data = NULL; + } + goto next(data, ...); +} + +__code pop2SingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, union Data* data1, ...)) { + if (stack->top) { + data = stack->top->data; + stack->top = stack->top->next; + } else { + data = NULL; + } + if (stack->top) { + data1 = stack->top->data; + stack->top = stack->top->next; + } else { + data1 = NULL; + } + goto next(data, data1, ...); +} \ No newline at end of file diff -r d12b2800af6a -r ead50a89470f midterm/src/stack.agda.replace --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/src/stack.agda.replace Wed Oct 25 17:35:36 2017 +0900 @@ -0,0 +1,5 @@ +pushStack : {a t : Set} -> Stack a -> a -> (Stack t -> t) -> t +pushStack {a} {t} s0 d next = (push s0) (stack s0) d (\s1 -> next (record {stack = s1} )) + +popStack : {a t : Set} -> Stack a -> (Stack t -> t) -> t +popStack {a} {t} s0 next = (pop s0) (stack s0) (\s1 -> next s0) \ No newline at end of file diff -r d12b2800af6a -r ead50a89470f midterm/src/stack_context.h.replace --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/src/stack_context.h.replace Wed Oct 25 17:35:36 2017 +0900 @@ -0,0 +1,14 @@ +struct Stack { + union Data* stack; + union Data* data; + union Data* data1; + enum Code whenEmpty; + enum Code clear; + enum Code push; + enum Code pop; + enum Code pop2; + enum Code isEmpty; + enum Code get; + enum Code get2; + enum Code next; +} Stack; diff -r d12b2800af6a -r ead50a89470f pic/codesegment.pdf Binary file pic/codesegment.pdf has changed diff -r d12b2800af6a -r ead50a89470f pic/modus-ponens.pdf Binary file pic/modus-ponens.pdf has changed diff -r d12b2800af6a -r ead50a89470f pic/rbtree.graffle Binary file pic/rbtree.graffle has changed diff -r d12b2800af6a -r ead50a89470f pic/rbtree.pdf Binary file pic/rbtree.pdf has changed