106 lines
2.9 KiB
TeX
106 lines
2.9 KiB
TeX
\renewcommand{\topfraction}{1}
|
|
\renewcommand{\dbltopfraction}{1}
|
|
\renewcommand{\bottomfraction}{1}
|
|
\renewcommand{\textfraction}{0}
|
|
|
|
\renewcommand{\floatpagefraction}{.99} % for one-column
|
|
\renewcommand{\dblfloatpagefraction}{.99} % for two-.
|
|
|
|
|
|
%% macros for sample.tex
|
|
|
|
\usepackage{mathpartir}
|
|
|
|
%% metavariables
|
|
|
|
% types
|
|
\newmeta\s{s} % these are automatically wrapped in \ma
|
|
\newmeta\t{t}
|
|
|
|
% expressions
|
|
\newmeta\M{M}
|
|
\newmeta\N{N}
|
|
\newmeta\P{P}
|
|
\newmeta\n{n}
|
|
|
|
% we write a macro for every bit of abstract syntax. That way they
|
|
% will all look the same!
|
|
|
|
% types
|
|
\newbfop\any{any}
|
|
\newbfop\int{int}
|
|
\newbfop\bool{bool}
|
|
\newbfop\module{module}
|
|
\newbfop\true{true}
|
|
\newbfop\false{false}
|
|
\newbfop\blm{blame}
|
|
\newbfop\ifzero{if0}
|
|
\newcommand\dlsproctype[2]{(#1 \to #2)}
|
|
\newcommand\proccnt[2]{(#1 \to #2)}
|
|
% \proctype is a little overkill.
|
|
%% Reynolds' package can also abstract things like (\s1 \to \s2 \to \s3).
|
|
|
|
% terms
|
|
\newmeta\x{x} % not sure if \x is reserved...
|
|
\newmeta\c{c}
|
|
\newmeta\f{f}
|
|
\newmeta\e{e}
|
|
\newcommand\Tabs[3]{\ma{(\l #1 : #2 . #3)}}
|
|
\newcommand\dlsabs[2]{\ma{(\l #1 . #2)}}
|
|
|
|
% typing judgements
|
|
\newcommand\hastype[2]{\ma{#1 \mathbin{:} #2}}
|
|
\newcommand\typej[2]{\ma{\typejg{\Gamma}{#1}{#2}}}
|
|
\newcommand\typejg[3]{\ma{#1 \vdash \hastype{#2}{#3}}}
|
|
|
|
\newcommand\mtypej[3][P]{\ma{\mtypejg[#1]{\Gamma}{#2}{#3}}}
|
|
\newcommand\mtypejg[4][P]{\ma{\mtypejgp[#1]{#2}{#3}{#4}{}}}
|
|
\newcommand\mtypejgp[5][P]{\ma{#1, #2 \vdash^V_{#5} \hastype{#3}{#4}}}
|
|
|
|
\newcommand\subty[2]{\ma{#1 \mathbin{<:} #2}}
|
|
|
|
\newcommand\lift[1]{\ma{\lfloor #1 \rfloor}}
|
|
|
|
\newcommand\ifz[3]{(\ifzero\ #1\ #2\ #3)}
|
|
|
|
|
|
\newcommand\modu[2]{(\module\ #1\ #2)}
|
|
\newcommand\mc[3]{(\module\ #1\ #2\ #3)}
|
|
\newcommand\mt[3]{(\module\ #1\ #2\ #3)}
|
|
|
|
\newcommand\orcnt[2]{#1\ \vee\ #2}
|
|
\newcommand\cast[3]{\{#1 \Leftarrow^{#2} #3\}}
|
|
\newcommand\barrcnt[2]{(#1 \dashrightarrow #2)}
|
|
|
|
\newcommand\blame[1]{(\blm \ \ma{#1})}
|
|
\newcommand\redrule[3]{#1 & \longrightarrow & #2 & \mbox{\sc{#3}}}
|
|
\newcommand\redruletwoline[3]{{#1} & \longrightarrow &\multicolumn{2}{r}\mbox{\sc{#3}} \\
|
|
\multicolumn{2}{r}{#2} & & }
|
|
|
|
\newcommand\addcast[5]{P,#1 \vdash^{\Rightarrow} {\hastype{#2}{#3}} \rightsquigarrow #4 ; #5}
|
|
\newcommand\addcastg[4]{\addcast{\Gamma}{#1}{#2}{#3}{#4}}
|
|
|
|
\newcommand{\mathsmallest}[ 1]{\mbox{\scriptsize \ma{#1}}}
|
|
\newcommand{\mathtiny}[1]{\mbox{\tiny\ma{#1}}}
|
|
|
|
\newcommand\ttproves[4]{P,#1 \vdash {\hastype{#2}{#3}} \rightsquigarrow #4}
|
|
\newcommand\ttgproves[3]{\ttproves{\Gamma}{#1}{#2}{#3}}
|
|
|
|
\newcommand\rtproves[4]{#1 \vdash^{\mathsmallest{RT}} {\hastype{#2}{#3}} ; #4}
|
|
\newcommand\rtgproves[3]{\rtproves{\Gamma}{#1}{#2}{#3}}
|
|
|
|
\newcommand\below{\triangleleft}
|
|
|
|
\newcommand\dlsreduces{\rightarrow^*}
|
|
|
|
\newcommand\merge[2]{\ma{merge(#1,#2)}}
|
|
\newcommand\mergetbl[3]{\ma{\merge{#1}{#2} &=& #3}}
|
|
|
|
\newcommand\context[1]{E[{\ma{#1}}]}
|
|
|
|
\newcommand\related[3][\ma{a}]{\ma{#2 \trianglerighteq_{#1} #3}}
|
|
\newcommand\similar[2]{\ma{#1 \triangleright #2}}
|
|
|
|
\newcommand\sth[1]{}
|
|
%\newcommand\qed[1]{}
|