Exp_all.tex

% generated by Ott 0.33 from: Exp.ott
\documentclass[11pt]{article}
\usepackage{amsmath,amssymb}
\usepackage{supertabular}
\usepackage{geometry}
\usepackage{ifthen}
\usepackage{alltt}%hack
\geometry{a4paper,dvips,twoside,left=22.5mm,right=22.5mm,top=20mm,bottom=30mm}
\usepackage{color}
\newcommand{\ottdrule}[4][]{{\displaystyle\frac{\begin{array}{l}#2\end{array}}{#3}\quad\ottdrulename{#4}}}
\newcommand{\ottusedrule}[1]{\[#1\]}
\newcommand{\ottpremise}[1]{ #1 \\}
\newenvironment{ottdefnblock}[3][]{ \framebox{\mbox{#2}} \quad #3 \\[0pt]}{}
\newenvironment{ottfundefnblock}[3][]{ \framebox{\mbox{#2}} \quad #3 \\[0pt]\begin{displaymath}\begin{array}{l}}{\end{array}\end{displaymath}}
\newcommand{\ottfunclause}[2]{ #1 \equiv #2 \\}
\newcommand{\ottnt}[1]{\mathit{#1}}
\newcommand{\ottmv}[1]{\mathit{#1}}
\newcommand{\ottkw}[1]{\mathbf{#1}}
\newcommand{\ottsym}[1]{#1}
\newcommand{\ottcom}[1]{\text{#1}}
\newcommand{\ottdrulename}[1]{\textsc{#1}}
\newcommand{\ottcomplu}[5]{\overline{#1}^{\,#2\in #3 #4 #5}}
\newcommand{\ottcompu}[3]{\overline{#1}^{\,#2<#3}}
\newcommand{\ottcomp}[2]{\overline{#1}^{\,#2}}
\newcommand{\ottgrammartabular}[1]{\begin{supertabular}{llcllllll}#1\end{supertabular}}
\newcommand{\ottmetavartabular}[1]{\begin{supertabular}{ll}#1\end{supertabular}}
\newcommand{\ottrulehead}[3]{$#1$ & & $#2$ & & & \multicolumn{2}{l}{#3}}
\newcommand{\ottprodline}[6]{& & $#1$ & $#2$ & $#3 #4$ & $#5$ & $#6$}
\newcommand{\ottfirstprodline}[6]{\ottprodline{#1}{#2}{#3}{#4}{#5}{#6}}
\newcommand{\ottlongprodline}[2]{& & $#1$ & \multicolumn{4}{l}{$#2$}}
\newcommand{\ottfirstlongprodline}[2]{\ottlongprodline{#1}{#2}}
\newcommand{\ottbindspecprodline}[6]{\ottprodline{#1}{#2}{#3}{#4}{#5}{#6}}
\newcommand{\ottprodnewline}{\\}
\newcommand{\ottinterrule}{\\[5.0mm]}
\newcommand{\ottafterlastrule}{\\}
\newcommand{\ottmetavars}{
\ottmetavartabular{
 $ \text{Term variables} ,\, \ottmv{x} ,\, \ottmv{y} ,\, \ottmv{z} $ & \ottcom{variables} \\
 $ \text{Type variables} ,\, \ottmv{a} ,\, \ottmv{b} $ & \ottcom{type variables} \\
 $ \text{Integer} ,\, \ottmv{i} $ &  \\
}}

\newcommand{\otttyXXmono}{
\ottrulehead{\text{Monotypes}  ,\ \tau}{::=}{\ottcom{Monotypes}}\ottprodnewline
\ottfirstprodline{|}{ \texttt{Int} }{}{}{}{}\ottprodnewline
\ottprodline{|}{\ottmv{a}}{}{}{}{}\ottprodnewline
\ottprodline{|}{ \tau_{{\mathrm{1}}}   \to   \tau_{{\mathrm{2}}} }{}{}{}{}}

\newcommand{\otttyXXrho}{
\ottrulehead{\text{Rho-types}  ,\ \rho}{::=}{\ottcom{Rho-types}}\ottprodnewline
\ottfirstprodline{|}{\tau}{}{}{}{}\ottprodnewline
\ottprodline{|}{ ( \rho ) } {\textsf{S}}{}{}{}}

\newcommand{\otttyXXpoly}{
\ottrulehead{\text{Polytypes}  ,\ \sigma}{::=}{}\ottprodnewline
\ottfirstprodline{|}{\rho}{}{}{}{}\ottprodnewline
\ottprodline{|}{ \forall  \ottmv{a}  .  \sigma }{}{\textsf{bind}\; \ottmv{a}\; \textsf{in}\; \sigma}{}{}\ottprodnewline
\ottprodline{|}{ \left[  \ottmv{a}  \mapsto  \tau  \right]  \sigma } {\textsf{M}}{}{}{}}

\newcommand{\otttm}{
\ottrulehead{\text{Terms}  ,\ \ottnt{t}  ,\ \ottnt{u}}{::=}{}\ottprodnewline
\ottfirstprodline{|}{\ottmv{i}}{}{}{}{\ottcom{Literal}}\ottprodnewline
\ottprodline{|}{\ottmv{x}}{}{}{}{\ottcom{Variable}}\ottprodnewline
\ottprodline{|}{ \lambda  \ottmv{x}  .  \ottnt{t} }{}{\textsf{bind}\; \ottmv{x}\; \textsf{in}\; \ottnt{t}}{}{\ottcom{Abstraction}}\ottprodnewline
\ottprodline{|}{ \ottnt{t}  \;  \ottnt{u} }{}{}{}{\ottcom{Application}}\ottprodnewline
\ottprodline{|}{ \lambda ( \ottmv{x}  ::  \sigma ).  \ottnt{t} }{}{\textsf{bind}\; \ottmv{x}\; \textsf{in}\; \ottnt{t}}{}{\ottcom{Typed abstraction}}\ottprodnewline
\ottprodline{|}{ \texttt{let}\;  \ottmv{x}  =  \ottnt{u}  \;\texttt{in}\;  \ottnt{t} }{}{\textsf{bind}\; \ottmv{x}\; \textsf{in}\; \ottnt{t}}{}{\ottcom{Local binding}}\ottprodnewline
\ottprodline{|}{ \ottnt{t}  ::  \sigma }{}{}{}{\ottcom{Type annotation}}\ottprodnewline
\ottprodline{|}{ ( \ottnt{t} ) } {\textsf{S}}{}{}{}\ottprodnewline
\ottprodline{|}{ \ottnt{t}  \left[  \ottmv{x}  \leadsto  \ottnt{t'}  \right] } {\textsf{M}}{}{}{}}

\newcommand{\ottvalue}{
\ottrulehead{\ottnt{value}  ,\ \ottnt{v}}{::=}{}\ottprodnewline
\ottfirstprodline{|}{\ottmv{i}}{}{}{}{}\ottprodnewline
\ottprodline{|}{ \lambda  \ottmv{x}  .  \ottnt{t} }{}{\textsf{bind}\; \ottmv{x}\; \textsf{in}\; \ottnt{t}}{}{}\ottprodnewline
\ottprodline{|}{ \lambda ( \ottmv{x}  ::  \sigma ).  \ottnt{t} }{}{\textsf{bind}\; \ottmv{x}\; \textsf{in}\; \ottnt{t}}{}{}}

\newcommand{\ottctx}{
\ottrulehead{\text{Typing contexts}  ,\ \Gamma}{::=}{}\ottprodnewline
\ottfirstprodline{|}{ \epsilon }{}{}{}{\ottcom{empty context}}\ottprodnewline
\ottprodline{|}{\Gamma  \ottsym{,}  \ottmv{x}  \ottsym{:}  \sigma}{}{}{}{\ottcom{assumption}}}

\newcommand{\ottfv}{
\ottrulehead{\ottnt{fv}}{::=}{}\ottprodnewline
\ottfirstprodline{|}{\ottnt{fv}  \ottsym{(}  \ottnt{t}  \ottsym{)}} {\textsf{M}}{}{}{}}

\newcommand{\ottftvany}{
\ottrulehead{\ottnt{ftvany}}{::=}{}\ottprodnewline
\ottfirstprodline{|}{ \text{ftv} ( \tau ) } {\textsf{M}}{}{}{}\ottprodnewline
\ottprodline{|}{ \text{ftv} ( \rho ) } {\textsf{M}}{}{}{}\ottprodnewline
\ottprodline{|}{ \text{ftv} ( \sigma ) } {\textsf{M}}{}{}{}\ottprodnewline
\ottprodline{|}{ \text{ftv} ( \Gamma ) } {\textsf{M}}{}{}{}}

\newcommand{\ottterminals}{
\ottrulehead{\ottnt{terminals}}{::=}{}\ottprodnewline
\ottfirstprodline{|}{ \longrightarrow }{}{}{}{}\ottprodnewline
\ottprodline{|}{ \to }{}{}{}{}\ottprodnewline
\ottprodline{|}{ :: }{}{}{}{}\ottprodnewline
\ottprodline{|}{ \text{fv} }{}{}{}{}\ottprodnewline
\ottprodline{|}{ \text{ftv} }{}{}{}{}\ottprodnewline
\ottprodline{|}{ \in }{}{}{}{}\ottprodnewline
\ottprodline{|}{ \not\in }{}{}{}{}\ottprodnewline
\ottprodline{|}{ \vdash }{}{}{}{}}

\newcommand{\ottformula}{
\ottrulehead{\ottnt{formula}}{::=}{}\ottprodnewline
\ottfirstprodline{|}{\ottnt{judgement}}{}{}{}{}\ottprodnewline
\ottprodline{|}{ \mathsf{value}\, \ottnt{v} }{}{}{}{}\ottprodnewline
\ottprodline{|}{ \mathsf{uniq}\, \Gamma }{}{}{}{}\ottprodnewline
\ottprodline{|}{ \mathsf{closed}\, \sigma }{}{}{}{}\ottprodnewline
\ottprodline{|}{ \ottmv{a} \not\in \ottnt{ftvany} }{}{}{}{}\ottprodnewline
\ottprodline{|}{\ottmv{x}  \ottsym{:}  \sigma \, \in \, \Gamma}{}{}{}{}}

\newcommand{\ottJTyping}{
\ottrulehead{\ottnt{JTyping}}{::=}{}\ottprodnewline
\ottfirstprodline{|}{ \Gamma \vdash \ottnt{t} : \sigma }{}{}{}{}}

\newcommand{\ottJStep}{
\ottrulehead{\ottnt{JStep}}{::=}{}\ottprodnewline
\ottfirstprodline{|}{ \ottnt{t}   \longrightarrow   \ottnt{u} }{}{}{}{}}

\newcommand{\ottjudgement}{
\ottrulehead{\ottnt{judgement}}{::=}{}\ottprodnewline
\ottfirstprodline{|}{\ottnt{JTyping}}{}{}{}{}\ottprodnewline
\ottprodline{|}{\ottnt{JStep}}{}{}{}{}}

\newcommand{\ottuserXXsyntax}{
\ottrulehead{\ottnt{user\_syntax}}{::=}{}\ottprodnewline
\ottfirstprodline{|}{\text{Term variables}}{}{}{}{}\ottprodnewline
\ottprodline{|}{\text{Type variables}}{}{}{}{}\ottprodnewline
\ottprodline{|}{\text{Integer}}{}{}{}{}\ottprodnewline
\ottprodline{|}{\text{Monotypes}}{}{}{}{}\ottprodnewline
\ottprodline{|}{\text{Rho-types}}{}{}{}{}\ottprodnewline
\ottprodline{|}{\text{Polytypes}}{}{}{}{}\ottprodnewline
\ottprodline{|}{\text{Terms}}{}{}{}{}\ottprodnewline
\ottprodline{|}{\ottnt{value}}{}{}{}{}\ottprodnewline
\ottprodline{|}{\text{Typing contexts}}{}{}{}{}\ottprodnewline
\ottprodline{|}{\ottnt{fv}}{}{}{}{}\ottprodnewline
\ottprodline{|}{\ottnt{ftvany}}{}{}{}{}\ottprodnewline
\ottprodline{|}{\ottnt{terminals}}{}{}{}{}\ottprodnewline
\ottprodline{|}{\ottnt{formula}}{}{}{}{}}

\newcommand{\ottgrammar}{\ottgrammartabular{
\otttyXXmono\ottinterrule
\otttyXXrho\ottinterrule
\otttyXXpoly\ottinterrule
\otttm\ottinterrule
\ottvalue\ottinterrule
\ottctx\ottinterrule
\ottfv\ottinterrule
\ottftvany\ottinterrule
\ottterminals\ottinterrule
\ottformula\ottinterrule
\ottJTyping\ottinterrule
\ottJStep\ottinterrule
\ottjudgement\ottinterrule
\ottuserXXsyntax\ottafterlastrule
}}

% defnss
% defns JTyping
%% defn typing
\newcommand{\ottdruletypXXint}[1]{\ottdrule[#1]{%
}{
 \Gamma \vdash \ottmv{i} :  \texttt{Int}  }{%
{\ottdrulename{typ\_int}}{}%
}}


\newcommand{\ottdruletypXXvar}[1]{\ottdrule[#1]{%
\ottpremise{ \mathsf{uniq}\, \Gamma }%
\ottpremise{\ottmv{x}  \ottsym{:}  \sigma \, \in \, \Gamma}%
}{
 \Gamma \vdash \ottmv{i} : \sigma }{%
{\ottdrulename{typ\_var}}{}%
}}


\newcommand{\ottdruletypXXabs}[1]{\ottdrule[#1]{%
\ottpremise{ \Gamma  \ottsym{,}  \ottmv{x}  \ottsym{:}  \tau_{{\mathrm{1}}} \vdash \ottnt{t} : \tau_{{\mathrm{2}}} }%
}{
 \Gamma \vdash  (  \lambda  \ottmv{x}  .  \ottnt{t}  )  :  (  \tau_{{\mathrm{1}}}   \to   \tau_{{\mathrm{2}}}  )  }{%
{\ottdrulename{typ\_abs}}{}%
}}


\newcommand{\ottdruletypXXapp}[1]{\ottdrule[#1]{%
\ottpremise{ \Gamma \vdash \ottnt{t} :  \tau_{{\mathrm{1}}}   \to   \tau_{{\mathrm{2}}}  }%
\ottpremise{ \Gamma \vdash \ottnt{u} : \tau_{{\mathrm{1}}} }%
}{
 \Gamma \vdash  \ottnt{t}  \;  \ottnt{u}  : \tau_{{\mathrm{2}}} }{%
{\ottdrulename{typ\_app}}{}%
}}


\newcommand{\ottdruletypXXlet}[1]{\ottdrule[#1]{%
\ottpremise{ \Gamma \vdash \ottnt{u} : \sigma }%
\ottpremise{ \Gamma  \ottsym{,}  \ottmv{x}  \ottsym{:}  \sigma \vdash \ottnt{t} : \rho }%
}{
 \Gamma \vdash  \texttt{let}\;  \ottmv{x}  =  \ottnt{u}  \;\texttt{in}\;  \ottnt{t}  : \rho }{%
{\ottdrulename{typ\_let}}{}%
}}


\newcommand{\ottdruletypXXannot}[1]{\ottdrule[#1]{%
\ottpremise{ \mathsf{closed}\, \sigma }%
\ottpremise{ \Gamma \vdash \ottnt{t} : \sigma }%
}{
 \Gamma \vdash  (  \ottnt{t}  ::  \sigma  )  : \sigma }{%
{\ottdrulename{typ\_annot}}{}%
}}


\newcommand{\ottdruletypXXgen}[1]{\ottdrule[#1]{%
\ottpremise{ \Gamma \vdash \ottnt{t} : \rho }%
}{
 \Gamma \vdash \ottnt{t} :  \forall  \ottmv{a}  .  \rho  }{%
{\ottdrulename{typ\_gen}}{}%
}}


\newcommand{\ottdruletypXXinst}[1]{\ottdrule[#1]{%
\ottpremise{ \Gamma \vdash \ottnt{t} :  \forall  \ottmv{a}  .  \rho  }%
}{
 \Gamma \vdash \ottnt{t} :  \left[  \ottmv{a}  \mapsto  \tau  \right]  \rho  }{%
{\ottdrulename{typ\_inst}}{}%
}}

\newcommand{\ottdefntyping}[1]{\begin{ottdefnblock}[#1]{$ \Gamma \vdash \ottnt{t} : \sigma $}{}
\ottusedrule{\ottdruletypXXint{}}
\ottusedrule{\ottdruletypXXvar{}}
\ottusedrule{\ottdruletypXXabs{}}
\ottusedrule{\ottdruletypXXapp{}}
\ottusedrule{\ottdruletypXXlet{}}
\ottusedrule{\ottdruletypXXannot{}}
\ottusedrule{\ottdruletypXXgen{}}
\ottusedrule{\ottdruletypXXinst{}}
\end{ottdefnblock}}


\newcommand{\ottdefnsJTyping}{
\ottdefntyping{}}

% defns JStep
%% defn step
\newcommand{\ottdrulestepXXletOne}[1]{\ottdrule[#1]{%
\ottpremise{ \ottnt{u}   \longrightarrow   \ottnt{u'} }%
}{
  \texttt{let}\;  \ottmv{x}  =  \ottnt{u}  \;\texttt{in}\;  \ottnt{t}    \longrightarrow    \texttt{let}\;  \ottmv{x}  =  \ottnt{u'}  \;\texttt{in}\;  \ottnt{t}  }{%
{\ottdrulename{step\_let1}}{}%
}}


\newcommand{\ottdrulestepXXlet}[1]{\ottdrule[#1]{%
}{
  \texttt{let}\;  \ottmv{x}  =  \ottnt{v}  \;\texttt{in}\;  \ottnt{t}    \longrightarrow    \ottnt{t}  \left[  \ottmv{x}  \leadsto  \ottnt{v}  \right]  }{%
{\ottdrulename{step\_let}}{}%
}}


\newcommand{\ottdrulestepXXappOne}[1]{\ottdrule[#1]{%
\ottpremise{ \ottnt{t}   \longrightarrow   \ottnt{t'} }%
}{
  \ottnt{t}  \;  \ottnt{u}    \longrightarrow    \ottnt{t'}  \;  \ottnt{u}  }{%
{\ottdrulename{step\_app1}}{}%
}}


\newcommand{\ottdrulestepXXappTwo}[1]{\ottdrule[#1]{%
\ottpremise{ \ottnt{u}   \longrightarrow   \ottnt{u'} }%
}{
   (  \lambda  \ottmv{x}  .  \ottnt{t}  )   \;  \ottnt{u}    \longrightarrow     (  \lambda  \ottmv{x}  .  \ottnt{t}  )   \;  \ottnt{u'}  }{%
{\ottdrulename{step\_app2}}{}%
}}


\newcommand{\ottdrulestepXXapp}[1]{\ottdrule[#1]{%
}{
   (  \lambda  \ottmv{x}  .  \ottnt{t}  )   \;  \ottnt{v}    \longrightarrow    \ottnt{t}  \left[  \ottmv{x}  \leadsto  \ottnt{v}  \right]  }{%
{\ottdrulename{step\_app}}{}%
}}


\newcommand{\ottdrulestepXXannotXXappTwo}[1]{\ottdrule[#1]{%
\ottpremise{ \ottnt{u}   \longrightarrow   \ottnt{u'} }%
}{
   (  \lambda ( \ottmv{x}  ::  \sigma ).  \ottnt{t}  )   \;  \ottnt{u}    \longrightarrow     (  \lambda ( \ottmv{x}  ::  \sigma ).  \ottnt{t}  )   \;  \ottnt{u'}  }{%
{\ottdrulename{step\_annot\_app2}}{}%
}}


\newcommand{\ottdrulestepXXannotXXapp}[1]{\ottdrule[#1]{%
}{
   (  \lambda ( \ottmv{x}  ::  \sigma ).  \ottnt{t}  )   \;  \ottnt{v}    \longrightarrow    \ottnt{t}  \left[  \ottmv{x}  \leadsto  \ottnt{v}  \right]  }{%
{\ottdrulename{step\_annot\_app}}{}%
}}


\newcommand{\ottdrulestepXXerase}[1]{\ottdrule[#1]{%
}{
  \ottnt{t}  ::  \sigma    \longrightarrow   \ottnt{t} }{%
{\ottdrulename{step\_erase}}{}%
}}

\newcommand{\ottdefnstep}[1]{\begin{ottdefnblock}[#1]{$ \ottnt{t}   \longrightarrow   \ottnt{u} $}{}
\ottusedrule{\ottdrulestepXXletOne{}}
\ottusedrule{\ottdrulestepXXlet{}}
\ottusedrule{\ottdrulestepXXappOne{}}
\ottusedrule{\ottdrulestepXXappTwo{}}
\ottusedrule{\ottdrulestepXXapp{}}
\ottusedrule{\ottdrulestepXXannotXXappTwo{}}
\ottusedrule{\ottdrulestepXXannotXXapp{}}
\ottusedrule{\ottdrulestepXXerase{}}
\end{ottdefnblock}}


\newcommand{\ottdefnsJStep}{
\ottdefnstep{}}

\newcommand{\ottdefnss}{
\ottdefnsJTyping
\ottdefnsJStep
}

\newcommand{\ottall}{\ottmetavars\\[0pt]
\ottgrammar\\[5.0mm]
\ottdefnss}

\begin{document}
\ottall

\begin{verbatim}
Definition rules:        16 good    0 bad
Definition rule clauses: 31 good    0 bad
\end{verbatim}
\end{document}