1274 lines
42 KiB
TeX
1274 lines
42 KiB
TeX
% generated by Ott 0.33 from: cbpv.ott
|
|
\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{\gap}{\:}
|
|
\newcommand{\kw}[1]{ \mathsf{#1} }
|
|
|
|
\newcommand{\ottmetavars}{
|
|
\ottmetavartabular{
|
|
$ \ottmv{x} ,\, \ottmv{y} ,\, \ottmv{z} $ & \ottcom{term variables} \\
|
|
}}
|
|
|
|
\newcommand{\ottv}{
|
|
\ottrulehead{\ottnt{v} ,\ \ottnt{w}}{::=}{\ottcom{values}}\ottprodnewline
|
|
\ottfirstprodline{|}{\ottmv{x}}{}{}{}{}\ottprodnewline
|
|
\ottprodline{|}{ \kw{unit} }{}{}{}{}\ottprodnewline
|
|
\ottprodline{|}{ \kw{inl} \gap \ottnt{v} }{}{}{}{}\ottprodnewline
|
|
\ottprodline{|}{ \kw{inr} \gap \ottnt{v} }{}{}{}{}\ottprodnewline
|
|
\ottprodline{|}{ \kw{thunk} \gap \ottnt{m} }{}{}{}{}\ottprodnewline
|
|
\ottprodline{|}{ ( \ottnt{v} ) } {\textsf{S}}{}{}{\ottcom{parentheses}}\ottprodnewline
|
|
\ottprodline{|}{ \ottnt{v} [ \sigma ] } {\textsf{S}}{}{}{}}
|
|
|
|
\newcommand{\ottm}{
|
|
\ottrulehead{\ottnt{m} ,\ \ottnt{n}}{::=}{\ottcom{computations}}\ottprodnewline
|
|
\ottfirstprodline{|}{ \kw{force} \gap \ottnt{v} }{}{}{}{}\ottprodnewline
|
|
\ottprodline{|}{ \lambda \ottmv{x} \mathpunct{.} \ottnt{m} }{}{\textsf{bind}\; \ottmv{x}\; \textsf{in}\; \ottnt{m}}{}{}\ottprodnewline
|
|
\ottprodline{|}{ \ottnt{m} \gap \ottnt{v} }{}{}{}{}\ottprodnewline
|
|
\ottprodline{|}{ \kw{return} \gap \ottnt{v} }{}{}{}{}\ottprodnewline
|
|
\ottprodline{|}{ \kw{let} \gap \ottmv{x} \leftarrow \ottnt{m} \gap \kw{in} \gap \ottnt{n} }{}{\textsf{bind}\; \ottmv{x}\; \textsf{in}\; \ottnt{n}}{}{}\ottprodnewline
|
|
\ottprodline{|}{ \kw{case} \gap \ottnt{v} \gap \kw{of} \gap \lbrace \kw{inl} \gap \ottmv{y} \Rightarrow \ottnt{m} \mathrel{;} \kw{inr} \gap \ottmv{z} \Rightarrow \ottnt{n} \rbrace }{}{\textsf{bind}\; \ottmv{y}\; \textsf{in}\; \ottnt{m}}{}{}\ottprodnewline
|
|
\ottbindspecprodline{}{}{}{\textsf{bind}\; \ottmv{z}\; \textsf{in}\; \ottnt{n}}{}{}\ottprodnewline
|
|
\ottprodline{|}{ ( \ottnt{m} ) } {\textsf{S}}{}{}{\ottcom{parentheses}}\ottprodnewline
|
|
\ottprodline{|}{ \ottnt{m} [ \sigma ] } {\textsf{S}}{}{}{}}
|
|
|
|
\newcommand{\ottA}{
|
|
\ottrulehead{\ottnt{A}}{::=}{\ottcom{value types}}\ottprodnewline
|
|
\ottfirstprodline{|}{ \kw{Unit} }{}{}{}{}\ottprodnewline
|
|
\ottprodline{|}{ \ottnt{A_{{\mathrm{1}}}} + \ottnt{A_{{\mathrm{2}}}} }{}{}{}{}\ottprodnewline
|
|
\ottprodline{|}{ \kw{U} \gap \ottnt{B} }{}{}{}{}}
|
|
|
|
\newcommand{\ottB}{
|
|
\ottrulehead{\ottnt{B}}{::=}{\ottcom{computation types}}\ottprodnewline
|
|
\ottfirstprodline{|}{ \kw{F} \gap \ottnt{A} }{}{}{}{}\ottprodnewline
|
|
\ottprodline{|}{ \ottnt{A} \rightarrow \ottnt{B} }{}{}{}{}}
|
|
|
|
\newcommand{\otts}{
|
|
\ottrulehead{\sigma}{::=}{\ottcom{substitutions}}\ottprodnewline
|
|
\ottfirstprodline{|}{ \cdot }{}{}{}{\ottcom{identity substitution}}\ottprodnewline
|
|
\ottprodline{|}{ \sigma , \ottmv{x} \mapsto \ottnt{v} }{}{}{}{\ottcom{substitution extension}}\ottprodnewline
|
|
\ottprodline{|}{ \ottmv{x} \mapsto \ottnt{v} } {\textsf{S}}{}{}{\ottcom{single substitution}}\ottprodnewline
|
|
\ottprodline{|}{ \mathop{\Uparrow} \sigma }{}{}{}{\ottcom{lifting substitution}}}
|
|
|
|
\newcommand{\ottG}{
|
|
\ottrulehead{\Gamma ,\ \Delta}{::=}{\ottcom{contexts}}\ottprodnewline
|
|
\ottfirstprodline{|}{ \cdot }{}{}{}{\ottcom{empty context}}\ottprodnewline
|
|
\ottprodline{|}{ \Gamma , \ottmv{x} \mathbin{:} \ottnt{A} }{}{}{}{\ottcom{context extension}}}
|
|
|
|
\newcommand{\ottP}{
|
|
\ottrulehead{\ottnt{P} ,\ \ottnt{Q}}{::=}{}\ottprodnewline
|
|
\ottfirstprodline{|}{ \lbrace \ottnt{v} \mid \ottnt{formula} \rbrace }{}{}{}{}\ottprodnewline
|
|
\ottprodline{|}{ \lbrace \ottnt{m} \mid \ottnt{formula} \rbrace }{}{}{}{}}
|
|
|
|
\newcommand{\ottgrammar}{\ottgrammartabular{
|
|
\ottv\ottinterrule
|
|
\ottm\ottinterrule
|
|
\ottA\ottinterrule
|
|
\ottB\ottinterrule
|
|
\otts\ottinterrule
|
|
\ottG\ottinterrule
|
|
\ottP\ottafterlastrule
|
|
}}
|
|
|
|
% defnss
|
|
% defns SN
|
|
%% defn SNeVal
|
|
\newcommand{\ottdruleSNeXXVar}[1]{\ottdrule[#1]{%
|
|
}{
|
|
\ottmv{x} \in \kw{SNe} }{%
|
|
{\ottdrulename{SNe\_Var}}{}%
|
|
}}
|
|
|
|
\newcommand{\ottdefnSNeVal}[1]{\begin{ottdefnblock}[#1]{$ \ottnt{v} \in \kw{SNe} $}{}
|
|
\ottusedrule{\ottdruleSNeXXVar{}}
|
|
\end{ottdefnblock}}
|
|
|
|
%% defn SNeCom
|
|
\newcommand{\ottdruleSNeXXForce}[1]{\ottdrule[#1]{%
|
|
}{
|
|
\kw{force} \gap \ottmv{x} \in \kw{SNe} }{%
|
|
{\ottdrulename{SNe\_Force}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSNeXXApp}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \in \kw{SNe} }%
|
|
\ottpremise{ \ottnt{v} \in \kw{SN} }%
|
|
}{
|
|
\ottnt{m} \gap \ottnt{v} \in \kw{SNe} }{%
|
|
{\ottdrulename{SNe\_App}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSNeXXLet}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \in \kw{SNe} }%
|
|
\ottpremise{ \ottnt{n} \in \kw{SN} }%
|
|
}{
|
|
\kw{let} \gap \ottmv{x} \leftarrow \ottnt{m} \gap \kw{in} \gap \ottnt{n} \in \kw{SNe} }{%
|
|
{\ottdrulename{SNe\_Let}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSNeXXCase}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \in \kw{SN} }%
|
|
\ottpremise{ \ottnt{n} \in \kw{SN} }%
|
|
}{
|
|
\kw{case} \gap \ottmv{x} \gap \kw{of} \gap \lbrace \kw{inl} \gap \ottmv{y} \Rightarrow \ottnt{m} \mathrel{;} \kw{inr} \gap \ottmv{z} \Rightarrow \ottnt{n} \rbrace \in \kw{SNe} }{%
|
|
{\ottdrulename{SNe\_Case}}{}%
|
|
}}
|
|
|
|
\newcommand{\ottdefnSNeCom}[1]{\begin{ottdefnblock}[#1]{$ \ottnt{m} \in \kw{SNe} $}{}
|
|
\ottusedrule{\ottdruleSNeXXForce{}}
|
|
\ottusedrule{\ottdruleSNeXXApp{}}
|
|
\ottusedrule{\ottdruleSNeXXLet{}}
|
|
\ottusedrule{\ottdruleSNeXXCase{}}
|
|
\end{ottdefnblock}}
|
|
|
|
%% defn SNVal
|
|
\newcommand{\ottdruleSNXXVar}[1]{\ottdrule[#1]{%
|
|
}{
|
|
\ottmv{x} \in \kw{SN} }{%
|
|
{\ottdrulename{SN\_Var}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSNXXUnit}[1]{\ottdrule[#1]{%
|
|
}{
|
|
\kw{unit} \in \kw{SN} }{%
|
|
{\ottdrulename{SN\_Unit}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSNXXInl}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{v} \in \kw{SN} }%
|
|
}{
|
|
\kw{inl} \gap \ottnt{v} \in \kw{SN} }{%
|
|
{\ottdrulename{SN\_Inl}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSNXXInr}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{v} \in \kw{SN} }%
|
|
}{
|
|
\kw{inr} \gap \ottnt{v} \in \kw{SN} }{%
|
|
{\ottdrulename{SN\_Inr}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSNXXThunk}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \in \kw{SN} }%
|
|
}{
|
|
\kw{thunk} \gap \ottnt{m} \in \kw{SN} }{%
|
|
{\ottdrulename{SN\_Thunk}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSNXXForceXXinv}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \kw{force} \gap \ottnt{v} \in \kw{SN} }%
|
|
}{
|
|
\ottnt{v} \in \kw{SN} }{%
|
|
{\ottdrulename{SN\_Force\_inv}}{}%
|
|
}}
|
|
|
|
\newcommand{\ottdefnSNVal}[1]{\begin{ottdefnblock}[#1]{$ \ottnt{v} \in \kw{SN} $}{}
|
|
\ottusedrule{\ottdruleSNXXVar{}}
|
|
\ottusedrule{\ottdruleSNXXUnit{}}
|
|
\ottusedrule{\ottdruleSNXXInl{}}
|
|
\ottusedrule{\ottdruleSNXXInr{}}
|
|
\ottusedrule{\ottdruleSNXXThunk{}}
|
|
\ottusedrule{\ottdruleSNXXForceXXinv{}}
|
|
\end{ottdefnblock}}
|
|
|
|
%% defn SNCom
|
|
\newcommand{\ottdruleSNXXLam}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \in \kw{SN} }%
|
|
}{
|
|
\lambda \ottmv{x} \mathpunct{.} \ottnt{m} \in \kw{SN} }{%
|
|
{\ottdrulename{SN\_Lam}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSNXXRet}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{v} \in \kw{SN} }%
|
|
}{
|
|
\kw{return} \gap \ottnt{v} \in \kw{SN} }{%
|
|
{\ottdrulename{SN\_Ret}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSNXXSNe}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \in \kw{SNe} }%
|
|
}{
|
|
\ottnt{m} \in \kw{SN} }{%
|
|
{\ottdrulename{SN\_SNe}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSNXXRed}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \leadsto \ottnt{n} }%
|
|
\ottpremise{ \ottnt{n} \in \kw{SN} }%
|
|
}{
|
|
\ottnt{m} \in \kw{SN} }{%
|
|
{\ottdrulename{SN\_Red}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSNXXReds}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \leadsto^* \ottnt{n} }%
|
|
\ottpremise{ \ottnt{n} \in \kw{SN} }%
|
|
}{
|
|
\ottnt{m} \in \kw{SN} }{%
|
|
{\ottdrulename{SN\_Reds}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSNXXExt}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \gap \ottmv{x} \in \kw{SN} }%
|
|
}{
|
|
\ottnt{m} \in \kw{SN} }{%
|
|
{\ottdrulename{SN\_Ext}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSNXXLift}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \Gamma \vDash \sigma }%
|
|
\ottpremise{ \Gamma , \ottmv{x} \mathbin{:} \ottnt{A} \vDash \ottnt{m} : \ottnt{B} }%
|
|
}{
|
|
\ottnt{m} [ \mathop{\Uparrow} \sigma ] \in \kw{SN} }{%
|
|
{\ottdrulename{SN\_Lift}}{}%
|
|
}}
|
|
|
|
\newcommand{\ottdefnSNCom}[1]{\begin{ottdefnblock}[#1]{$ \ottnt{m} \in \kw{SN} $}{}
|
|
\ottusedrule{\ottdruleSNXXLam{}}
|
|
\ottusedrule{\ottdruleSNXXRet{}}
|
|
\ottusedrule{\ottdruleSNXXSNe{}}
|
|
\ottusedrule{\ottdruleSNXXRed{}}
|
|
\ottusedrule{\ottdruleSNXXReds{}}
|
|
\ottusedrule{\ottdruleSNXXExt{}}
|
|
\ottusedrule{\ottdruleSNXXLift{}}
|
|
\end{ottdefnblock}}
|
|
|
|
%% defn SR
|
|
\newcommand{\ottdruleSRXXThunk}[1]{\ottdrule[#1]{%
|
|
}{
|
|
\kw{force} \gap ( \kw{thunk} \gap \ottnt{m} ) \leadsto \ottnt{m} }{%
|
|
{\ottdrulename{SR\_Thunk}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSRXXLam}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{v} \in \kw{SN} }%
|
|
}{
|
|
( \lambda \ottmv{x} \mathpunct{.} \ottnt{m} ) \gap \ottnt{v} \leadsto \ottnt{m} [ \ottmv{x} \mapsto \ottnt{v} ] }{%
|
|
{\ottdrulename{SR\_Lam}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSRXXRet}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{v} \in \kw{SN} }%
|
|
}{
|
|
\kw{let} \gap \ottmv{x} \leftarrow ( \kw{return} \gap \ottnt{v} ) \gap \kw{in} \gap \ottnt{m} \leadsto \ottnt{m} [ \ottmv{x} \mapsto \ottnt{v} ] }{%
|
|
{\ottdrulename{SR\_Ret}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSRXXInl}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{v} \in \kw{SN} }%
|
|
\ottpremise{ \ottnt{n} \in \kw{SN} }%
|
|
}{
|
|
\kw{case} \gap ( \kw{inl} \gap \ottnt{v} ) \gap \kw{of} \gap \lbrace \kw{inl} \gap \ottmv{y} \Rightarrow \ottnt{m} \mathrel{;} \kw{inr} \gap \ottmv{z} \Rightarrow \ottnt{n} \rbrace \leadsto \ottnt{m} [ \ottmv{y} \mapsto \ottnt{v} ] }{%
|
|
{\ottdrulename{SR\_Inl}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSRXXInr}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{v} \in \kw{SN} }%
|
|
\ottpremise{ \ottnt{m} \in \kw{SN} }%
|
|
}{
|
|
\kw{case} \gap ( \kw{inr} \gap \ottnt{v} ) \gap \kw{of} \gap \lbrace \kw{inl} \gap \ottmv{y} \Rightarrow \ottnt{m} \mathrel{;} \kw{inr} \gap \ottmv{z} \Rightarrow \ottnt{n} \rbrace \leadsto \ottnt{n} [ \ottmv{z} \mapsto \ottnt{v} ] }{%
|
|
{\ottdrulename{SR\_Inr}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSRXXApp}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \leadsto \ottnt{n} }%
|
|
}{
|
|
\ottnt{m} \gap \ottnt{v} \leadsto \ottnt{n} \gap \ottnt{v} }{%
|
|
{\ottdrulename{SR\_App}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSRXXLet}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \leadsto \ottnt{m'} }%
|
|
}{
|
|
\kw{let} \gap \ottmv{x} \leftarrow \ottnt{m} \gap \kw{in} \gap \ottnt{n} \leadsto \kw{let} \gap \ottmv{x} \leftarrow \ottnt{m'} \gap \kw{in} \gap \ottnt{n} }{%
|
|
{\ottdrulename{SR\_Let}}{}%
|
|
}}
|
|
|
|
\newcommand{\ottdefnSR}[1]{\begin{ottdefnblock}[#1]{$ \ottnt{m} \leadsto \ottnt{n} $}{}
|
|
\ottusedrule{\ottdruleSRXXThunk{}}
|
|
\ottusedrule{\ottdruleSRXXLam{}}
|
|
\ottusedrule{\ottdruleSRXXRet{}}
|
|
\ottusedrule{\ottdruleSRXXInl{}}
|
|
\ottusedrule{\ottdruleSRXXInr{}}
|
|
\ottusedrule{\ottdruleSRXXApp{}}
|
|
\ottusedrule{\ottdruleSRXXLet{}}
|
|
\end{ottdefnblock}}
|
|
|
|
%% defn SRs
|
|
\newcommand{\ottdruleSRsXXRefl}[1]{\ottdrule[#1]{%
|
|
}{
|
|
\ottnt{m} \leadsto^* \ottnt{m} }{%
|
|
{\ottdrulename{SRs\_Refl}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSRsXXTrans}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \leadsto \ottnt{m'} }%
|
|
\ottpremise{ \ottnt{m'} \leadsto^* \ottnt{n} }%
|
|
}{
|
|
\ottnt{m} \leadsto^* \ottnt{n} }{%
|
|
{\ottdrulename{SRs\_Trans}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSRsXXOnce}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \leadsto \ottnt{n} }%
|
|
}{
|
|
\ottnt{m} \leadsto^* \ottnt{n} }{%
|
|
{\ottdrulename{SRs\_Once}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSRsXXTransPP}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \leadsto^* \ottnt{m'} }%
|
|
\ottpremise{ \ottnt{m'} \leadsto^* \ottnt{n} }%
|
|
}{
|
|
\ottnt{m} \leadsto^* \ottnt{n} }{%
|
|
{\ottdrulename{SRs\_Trans'}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSRsXXApp}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \leadsto^* \ottnt{n} }%
|
|
}{
|
|
\ottnt{m} \gap \ottnt{v} \leadsto^* \ottnt{n} \gap \ottnt{v} }{%
|
|
{\ottdrulename{SRs\_App}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSRsXXLet}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \leadsto^* \ottnt{m'} }%
|
|
}{
|
|
\kw{let} \gap \ottmv{x} \leftarrow \ottnt{m} \gap \kw{in} \gap \ottnt{n} \leadsto^* \kw{let} \gap \ottmv{x} \leftarrow \ottnt{m'} \gap \kw{in} \gap \ottnt{n} }{%
|
|
{\ottdrulename{SRs\_Let}}{}%
|
|
}}
|
|
|
|
\newcommand{\ottdefnSRs}[1]{\begin{ottdefnblock}[#1]{$ \ottnt{m} \leadsto^* \ottnt{n} $}{}
|
|
\ottusedrule{\ottdruleSRsXXRefl{}}
|
|
\ottusedrule{\ottdruleSRsXXTrans{}}
|
|
\ottusedrule{\ottdruleSRsXXOnce{}}
|
|
\ottusedrule{\ottdruleSRsXXTransPP{}}
|
|
\ottusedrule{\ottdruleSRsXXApp{}}
|
|
\ottusedrule{\ottdruleSRsXXLet{}}
|
|
\end{ottdefnblock}}
|
|
|
|
|
|
\newcommand{\ottdefnsSN}{
|
|
\ottdefnSNeVal{}\ottdefnSNeCom{}\ottdefnSNVal{}\ottdefnSNCom{}\ottdefnSR{}\ottdefnSRs{}}
|
|
|
|
% defns LR
|
|
%% defn ValType
|
|
\newcommand{\ottdruleLRXXUnit}[1]{\ottdrule[#1]{%
|
|
}{
|
|
\mathopen{\llbracket} \kw{Unit} \mathclose{\rrbracket} \searrow \lbrace \ottnt{v} \mid \ottnt{v} \in \kw{SNe} \vee \ottnt{v} = \kw{unit} \rbrace }{%
|
|
{\ottdrulename{LR\_Unit}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleLRXXSum}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \mathopen{\llbracket} \ottnt{A_{{\mathrm{1}}}} \mathclose{\rrbracket} \searrow \ottnt{P} }%
|
|
\ottpremise{ \mathopen{\llbracket} \ottnt{A_{{\mathrm{2}}}} \mathclose{\rrbracket} \searrow \ottnt{Q} }%
|
|
}{
|
|
\mathopen{\llbracket} \ottnt{A_{{\mathrm{1}}}} + \ottnt{A_{{\mathrm{2}}}} \mathclose{\rrbracket} \searrow \lbrace \ottnt{v} \mid \ottnt{v} \in \kw{SNe} \vee ( \exists \ottnt{w} \mathpunct{.} \ottnt{v} = \kw{inl} \gap \ottnt{w} \wedge \ottnt{w} \in \ottnt{P} ) \vee ( \exists \ottnt{w} \mathpunct{.} \ottnt{v} = \kw{inr} \gap \ottnt{w} \wedge \ottnt{w} \in \ottnt{Q} ) \rbrace }{%
|
|
{\ottdrulename{LR\_Sum}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleLRXXU}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \mathopen{\llbracket} \ottnt{B} \mathclose{\rrbracket} \searrow \ottnt{P} }%
|
|
}{
|
|
\mathopen{\llbracket} \kw{U} \gap \ottnt{B} \mathclose{\rrbracket} \searrow \lbrace \ottnt{v} \mid \kw{force} \gap \ottnt{v} \in \ottnt{P} \rbrace }{%
|
|
{\ottdrulename{LR\_U}}{}%
|
|
}}
|
|
|
|
\newcommand{\ottdefnValType}[1]{\begin{ottdefnblock}[#1]{$ \mathopen{\llbracket} \ottnt{A} \mathclose{\rrbracket} \searrow \ottnt{P} $}{}
|
|
\ottusedrule{\ottdruleLRXXUnit{}}
|
|
\ottusedrule{\ottdruleLRXXSum{}}
|
|
\ottusedrule{\ottdruleLRXXU{}}
|
|
\end{ottdefnblock}}
|
|
|
|
%% defn ComType
|
|
\newcommand{\ottdruleLRXXF}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \mathopen{\llbracket} \ottnt{A} \mathclose{\rrbracket} \searrow \ottnt{P} }%
|
|
}{
|
|
\mathopen{\llbracket} \kw{F} \gap \ottnt{A} \mathclose{\rrbracket} \searrow \lbrace \ottnt{m} \mid ( \exists \ottnt{n} \mathpunct{.} \ottnt{m} \leadsto^* \ottnt{n} \wedge \ottnt{n} \in \kw{SNe} ) \vee ( \exists \ottnt{v} \mathpunct{.} \ottnt{m} \leadsto^* \kw{return} \gap \ottnt{v} \wedge \ottnt{v} \in \ottnt{P} ) \rbrace }{%
|
|
{\ottdrulename{LR\_F}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleLRXXArr}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \mathopen{\llbracket} \ottnt{A} \mathclose{\rrbracket} \searrow \ottnt{P} }%
|
|
\ottpremise{ \mathopen{\llbracket} \ottnt{B} \mathclose{\rrbracket} \searrow \ottnt{Q} }%
|
|
}{
|
|
\mathopen{\llbracket} \ottnt{A} \rightarrow \ottnt{B} \mathclose{\rrbracket} \searrow \lbrace \ottnt{m} \mid \forall \ottnt{v} \mathpunct{.} \ottnt{v} \in \ottnt{P} \Rightarrow \ottnt{m} \gap \ottnt{v} \in \ottnt{Q} \rbrace }{%
|
|
{\ottdrulename{LR\_Arr}}{}%
|
|
}}
|
|
|
|
\newcommand{\ottdefnComType}[1]{\begin{ottdefnblock}[#1]{$ \mathopen{\llbracket} \ottnt{B} \mathclose{\rrbracket} \searrow \ottnt{P} $}{}
|
|
\ottusedrule{\ottdruleLRXXF{}}
|
|
\ottusedrule{\ottdruleLRXXArr{}}
|
|
\end{ottdefnblock}}
|
|
|
|
|
|
\newcommand{\ottdefnsLR}{
|
|
\ottdefnValType{}\ottdefnComType{}}
|
|
|
|
% defns LRs
|
|
%% defn ValTypes
|
|
\newcommand{\ottdruleLRPPXXUnitXXvar}[1]{\ottdrule[#1]{%
|
|
}{
|
|
\ottmv{x} \in \mathopen{\llbracket} \kw{Unit} \mathclose{\rrbracket} }{%
|
|
{\ottdrulename{LR'\_Unit\_var}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleLRPPXXUnitXXunit}[1]{\ottdrule[#1]{%
|
|
}{
|
|
\kw{unit} \in \mathopen{\llbracket} \kw{Unit} \mathclose{\rrbracket} }{%
|
|
{\ottdrulename{LR'\_Unit\_unit}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleLRPPXXSumXXvar}[1]{\ottdrule[#1]{%
|
|
}{
|
|
\ottmv{x} \in \mathopen{\llbracket} \ottnt{A_{{\mathrm{1}}}} + \ottnt{A_{{\mathrm{2}}}} \mathclose{\rrbracket} }{%
|
|
{\ottdrulename{LR'\_Sum\_var}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleLRPPXXSumXXinl}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{v} \in \mathopen{\llbracket} \ottnt{A_{{\mathrm{1}}}} \mathclose{\rrbracket} }%
|
|
}{
|
|
\kw{inl} \gap \ottnt{v} \in \mathopen{\llbracket} \ottnt{A_{{\mathrm{1}}}} + \ottnt{A_{{\mathrm{2}}}} \mathclose{\rrbracket} }{%
|
|
{\ottdrulename{LR'\_Sum\_inl}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleLRPPXXSumXXinr}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{v} \in \mathopen{\llbracket} \ottnt{A_{{\mathrm{2}}}} \mathclose{\rrbracket} }%
|
|
}{
|
|
\kw{inr} \gap \ottnt{v} \in \mathopen{\llbracket} \ottnt{A_{{\mathrm{1}}}} + \ottnt{A_{{\mathrm{2}}}} \mathclose{\rrbracket} }{%
|
|
{\ottdrulename{LR'\_Sum\_inr}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleLRPPXXForce}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \kw{force} \gap \ottnt{v} \in \mathopen{\llbracket} \ottnt{B} \mathclose{\rrbracket} }%
|
|
}{
|
|
\ottnt{v} \in \mathopen{\llbracket} \kw{U} \gap \ottnt{B} \mathclose{\rrbracket} }{%
|
|
{\ottdrulename{LR'\_Force}}{}%
|
|
}}
|
|
|
|
\newcommand{\ottdefnValTypes}[1]{\begin{ottdefnblock}[#1]{$ \ottnt{v} \in \mathopen{\llbracket} \ottnt{A} \mathclose{\rrbracket} $}{}
|
|
\ottusedrule{\ottdruleLRPPXXUnitXXvar{}}
|
|
\ottusedrule{\ottdruleLRPPXXUnitXXunit{}}
|
|
\ottusedrule{\ottdruleLRPPXXSumXXvar{}}
|
|
\ottusedrule{\ottdruleLRPPXXSumXXinl{}}
|
|
\ottusedrule{\ottdruleLRPPXXSumXXinr{}}
|
|
\ottusedrule{\ottdruleLRPPXXForce{}}
|
|
\end{ottdefnblock}}
|
|
|
|
%% defn ComTypes
|
|
\newcommand{\ottdruleLRPPXXFXXvar}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \leadsto^* \ottnt{n} }%
|
|
\ottpremise{ \ottnt{n} \in \kw{SNe} }%
|
|
}{
|
|
\ottnt{m} \in \mathopen{\llbracket} \kw{F} \gap \ottnt{A} \mathclose{\rrbracket} }{%
|
|
{\ottdrulename{LR'\_F\_var}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleLRPPXXFXXret}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \leadsto^* \kw{return} \gap \ottnt{v} }%
|
|
\ottpremise{ \ottnt{v} \in \mathopen{\llbracket} \ottnt{A} \mathclose{\rrbracket} }%
|
|
}{
|
|
\ottnt{m} \in \mathopen{\llbracket} \kw{F} \gap \ottnt{A} \mathclose{\rrbracket} }{%
|
|
{\ottdrulename{LR'\_F\_ret}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleLRPPXXArr}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \forall \ottnt{v} \mathpunct{.} \ottnt{v} \in \mathopen{\llbracket} \ottnt{A} \mathclose{\rrbracket} \Rightarrow \ottnt{m} \gap \ottnt{v} \in \mathopen{\llbracket} \ottnt{B} \mathclose{\rrbracket} }%
|
|
}{
|
|
\ottnt{m} \in \mathopen{\llbracket} \ottnt{A} \rightarrow \ottnt{B} \mathclose{\rrbracket} }{%
|
|
{\ottdrulename{LR'\_Arr}}{}%
|
|
}}
|
|
|
|
\newcommand{\ottdefnComTypes}[1]{\begin{ottdefnblock}[#1]{$ \ottnt{m} \in \mathopen{\llbracket} \ottnt{B} \mathclose{\rrbracket} $}{}
|
|
\ottusedrule{\ottdruleLRPPXXFXXvar{}}
|
|
\ottusedrule{\ottdruleLRPPXXFXXret{}}
|
|
\ottusedrule{\ottdruleLRPPXXArr{}}
|
|
\end{ottdefnblock}}
|
|
|
|
|
|
\newcommand{\ottdefnsLRs}{
|
|
\ottdefnValTypes{}\ottdefnComTypes{}}
|
|
|
|
% defns Sem
|
|
%% defn SemCtxt
|
|
\newcommand{\ottdruleSXXNil}[1]{\ottdrule[#1]{%
|
|
}{
|
|
\Gamma \vDash \cdot }{%
|
|
{\ottdrulename{S\_Nil}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSXXCons}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \Gamma \vDash \sigma }%
|
|
\ottpremise{ \mathopen{\llbracket} \ottnt{A} \mathclose{\rrbracket} \searrow \ottnt{P} }%
|
|
\ottpremise{ \ottnt{v} \in \ottnt{P} }%
|
|
}{
|
|
\Gamma , \ottmv{x} \mathbin{:} \ottnt{A} \vDash \sigma , \ottmv{x} \mapsto \ottnt{v} }{%
|
|
{\ottdrulename{S\_Cons}}{}%
|
|
}}
|
|
|
|
\newcommand{\ottdefnSemCtxt}[1]{\begin{ottdefnblock}[#1]{$ \Gamma \vDash \sigma $}{}
|
|
\ottusedrule{\ottdruleSXXNil{}}
|
|
\ottusedrule{\ottdruleSXXCons{}}
|
|
\end{ottdefnblock}}
|
|
|
|
%% defn SemVal
|
|
\newcommand{\ottdruleSXXVar}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottmv{x} : \ottnt{A} \in \Gamma }%
|
|
}{
|
|
\Gamma \vDash \ottmv{x} : \ottnt{A} }{%
|
|
{\ottdrulename{S\_Var}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSXXUnit}[1]{\ottdrule[#1]{%
|
|
}{
|
|
\Gamma \vDash \kw{unit} : \kw{Unit} }{%
|
|
{\ottdrulename{S\_Unit}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSXXInl}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \Gamma \vDash \ottnt{v} : \ottnt{A_{{\mathrm{1}}}} }%
|
|
}{
|
|
\Gamma \vDash \kw{inl} \gap \ottnt{v} : \ottnt{A_{{\mathrm{1}}}} + \ottnt{A_{{\mathrm{2}}}} }{%
|
|
{\ottdrulename{S\_Inl}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSXXInr}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \Gamma \vDash \ottnt{v} : \ottnt{A_{{\mathrm{2}}}} }%
|
|
}{
|
|
\Gamma \vDash \kw{inr} \gap \ottnt{v} : \ottnt{A_{{\mathrm{1}}}} + \ottnt{A_{{\mathrm{2}}}} }{%
|
|
{\ottdrulename{S\_Inr}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSXXThunk}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \Gamma \vDash \ottnt{m} : \ottnt{B} }%
|
|
}{
|
|
\Gamma \vDash \kw{thunk} \gap \ottnt{m} : \kw{U} \gap \ottnt{B} }{%
|
|
{\ottdrulename{S\_Thunk}}{}%
|
|
}}
|
|
|
|
\newcommand{\ottdefnSemVal}[1]{\begin{ottdefnblock}[#1]{$ \Gamma \vDash \ottnt{v} : \ottnt{A} $}{}
|
|
\ottusedrule{\ottdruleSXXVar{}}
|
|
\ottusedrule{\ottdruleSXXUnit{}}
|
|
\ottusedrule{\ottdruleSXXInl{}}
|
|
\ottusedrule{\ottdruleSXXInr{}}
|
|
\ottusedrule{\ottdruleSXXThunk{}}
|
|
\end{ottdefnblock}}
|
|
|
|
%% defn SemCom
|
|
\newcommand{\ottdruleSXXForce}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \Gamma \vDash \ottnt{v} : \kw{U} \gap \ottnt{B} }%
|
|
}{
|
|
\Gamma \vDash \kw{force} \gap \ottnt{v} : \ottnt{B} }{%
|
|
{\ottdrulename{S\_Force}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSXXArr}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \Gamma , \ottmv{x} \mathbin{:} \ottnt{A} \vDash \ottnt{m} : \ottnt{B} }%
|
|
}{
|
|
\Gamma \vDash \lambda \ottmv{x} \mathpunct{.} \ottnt{m} : \ottnt{A} \rightarrow \ottnt{B} }{%
|
|
{\ottdrulename{S\_Arr}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSXXApp}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \Gamma \vDash \ottnt{m} : \ottnt{A} \rightarrow \ottnt{B} }%
|
|
\ottpremise{ \Gamma \vDash \ottnt{v} : \ottnt{A} }%
|
|
}{
|
|
\Gamma \vDash \ottnt{m} \gap \ottnt{v} : \ottnt{B} }{%
|
|
{\ottdrulename{S\_App}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSXXRet}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \Gamma \vDash \ottnt{v} : \ottnt{A} }%
|
|
}{
|
|
\Gamma \vDash \kw{return} \gap \ottnt{v} : \kw{F} \gap \ottnt{A} }{%
|
|
{\ottdrulename{S\_Ret}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSXXLet}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \Gamma \vDash \ottnt{m} : \kw{F} \gap \ottnt{A} }%
|
|
\ottpremise{ \Gamma , \ottmv{x} \mathbin{:} \ottnt{A} \vDash \ottnt{n} : \ottnt{B} }%
|
|
}{
|
|
\Gamma \vDash \kw{let} \gap \ottmv{x} \leftarrow \ottnt{m} \gap \kw{in} \gap \ottnt{n} : \ottnt{B} }{%
|
|
{\ottdrulename{S\_Let}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleSXXCase}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \Gamma \vDash \ottnt{v} : \ottnt{A_{{\mathrm{1}}}} + \ottnt{A_{{\mathrm{2}}}} }%
|
|
\ottpremise{ \Gamma , \ottmv{y} \mathbin{:} \ottnt{A_{{\mathrm{1}}}} \vDash \ottnt{m} : \ottnt{B} }%
|
|
\ottpremise{ \Gamma , \ottmv{z} \mathbin{:} \ottnt{A_{{\mathrm{2}}}} \vDash \ottnt{n} : \ottnt{B} }%
|
|
}{
|
|
\Gamma \vDash \kw{case} \gap \ottnt{v} \gap \kw{of} \gap \lbrace \kw{inl} \gap \ottmv{y} \Rightarrow \ottnt{m} \mathrel{;} \kw{inr} \gap \ottmv{z} \Rightarrow \ottnt{n} \rbrace : \ottnt{B} }{%
|
|
{\ottdrulename{S\_Case}}{}%
|
|
}}
|
|
|
|
\newcommand{\ottdefnSemCom}[1]{\begin{ottdefnblock}[#1]{$ \Gamma \vDash \ottnt{m} : \ottnt{B} $}{}
|
|
\ottusedrule{\ottdruleSXXForce{}}
|
|
\ottusedrule{\ottdruleSXXArr{}}
|
|
\ottusedrule{\ottdruleSXXApp{}}
|
|
\ottusedrule{\ottdruleSXXRet{}}
|
|
\ottusedrule{\ottdruleSXXLet{}}
|
|
\ottusedrule{\ottdruleSXXCase{}}
|
|
\end{ottdefnblock}}
|
|
|
|
|
|
\newcommand{\ottdefnsSem}{
|
|
\ottdefnSemCtxt{}\ottdefnSemVal{}\ottdefnSemCom{}}
|
|
|
|
% defns Typing
|
|
%% defn ValWt
|
|
\newcommand{\ottdruleTXXVar}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottmv{x} : \ottnt{A} \in \Gamma }%
|
|
}{
|
|
\Gamma \vdash \ottmv{x} : \ottnt{A} }{%
|
|
{\ottdrulename{T\_Var}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleTXXUnit}[1]{\ottdrule[#1]{%
|
|
}{
|
|
\Gamma \vdash \kw{unit} : \kw{Unit} }{%
|
|
{\ottdrulename{T\_Unit}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleTXXInl}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \Gamma \vdash \ottnt{v} : \ottnt{A_{{\mathrm{1}}}} }%
|
|
}{
|
|
\Gamma \vdash \kw{inl} \gap \ottnt{v} : \ottnt{A_{{\mathrm{1}}}} + \ottnt{A_{{\mathrm{2}}}} }{%
|
|
{\ottdrulename{T\_Inl}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleTXXInr}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \Gamma \vdash \ottnt{v} : \ottnt{A_{{\mathrm{2}}}} }%
|
|
}{
|
|
\Gamma \vdash \kw{inr} \gap \ottnt{v} : \ottnt{A_{{\mathrm{1}}}} + \ottnt{A_{{\mathrm{2}}}} }{%
|
|
{\ottdrulename{T\_Inr}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleTXXThunk}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \Gamma \vdash \ottnt{m} : \ottnt{B} }%
|
|
}{
|
|
\Gamma \vdash \kw{thunk} \gap \ottnt{m} : \kw{U} \gap \ottnt{B} }{%
|
|
{\ottdrulename{T\_Thunk}}{}%
|
|
}}
|
|
|
|
\newcommand{\ottdefnValWt}[1]{\begin{ottdefnblock}[#1]{$ \Gamma \vdash \ottnt{v} : \ottnt{A} $}{}
|
|
\ottusedrule{\ottdruleTXXVar{}}
|
|
\ottusedrule{\ottdruleTXXUnit{}}
|
|
\ottusedrule{\ottdruleTXXInl{}}
|
|
\ottusedrule{\ottdruleTXXInr{}}
|
|
\ottusedrule{\ottdruleTXXThunk{}}
|
|
\end{ottdefnblock}}
|
|
|
|
%% defn ComWt
|
|
\newcommand{\ottdruleTXXForce}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \Gamma \vdash \ottnt{v} : \kw{U} \gap \ottnt{B} }%
|
|
}{
|
|
\Gamma \vdash \kw{force} \gap \ottnt{v} : \ottnt{B} }{%
|
|
{\ottdrulename{T\_Force}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleTXXLam}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \Gamma , \ottmv{x} \mathbin{:} \ottnt{A} \vdash \ottnt{m} : \ottnt{B} }%
|
|
}{
|
|
\Gamma \vdash \lambda \ottmv{x} \mathpunct{.} \ottnt{m} : \ottnt{A} \rightarrow \ottnt{B} }{%
|
|
{\ottdrulename{T\_Lam}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleTXXApp}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \Gamma \vdash \ottnt{m} : \ottnt{A} \rightarrow \ottnt{B} }%
|
|
\ottpremise{ \Gamma \vdash \ottnt{v} : \ottnt{A} }%
|
|
}{
|
|
\Gamma \vdash \ottnt{m} \gap \ottnt{v} : \ottnt{B} }{%
|
|
{\ottdrulename{T\_App}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleTXXRet}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \Gamma \vdash \ottnt{v} : \ottnt{A} }%
|
|
}{
|
|
\Gamma \vdash \kw{return} \gap \ottnt{v} : \kw{F} \gap \ottnt{A} }{%
|
|
{\ottdrulename{T\_Ret}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleTXXLet}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \Gamma \vdash \ottnt{m} : \kw{F} \gap \ottnt{A} }%
|
|
\ottpremise{ \Gamma , \ottmv{x} \mathbin{:} \ottnt{A} \vdash \ottnt{n} : \ottnt{B} }%
|
|
}{
|
|
\Gamma \vdash \kw{let} \gap \ottmv{x} \leftarrow \ottnt{m} \gap \kw{in} \gap \ottnt{n} : \ottnt{B} }{%
|
|
{\ottdrulename{T\_Let}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleTXXCase}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \Gamma \vdash \ottnt{v} : \ottnt{A_{{\mathrm{1}}}} + \ottnt{A_{{\mathrm{2}}}} }%
|
|
\ottpremise{ \Gamma , \ottmv{y} \mathbin{:} \ottnt{A_{{\mathrm{1}}}} \vdash \ottnt{m} : \ottnt{B} }%
|
|
\ottpremise{ \Gamma , \ottmv{z} \mathbin{:} \ottnt{A_{{\mathrm{2}}}} \vdash \ottnt{n} : \ottnt{B} }%
|
|
}{
|
|
\Gamma \vdash \kw{case} \gap \ottnt{v} \gap \kw{of} \gap \lbrace \kw{inl} \gap \ottmv{y} \Rightarrow \ottnt{m} \mathrel{;} \kw{inr} \gap \ottmv{z} \Rightarrow \ottnt{n} \rbrace : \ottnt{B} }{%
|
|
{\ottdrulename{T\_Case}}{}%
|
|
}}
|
|
|
|
\newcommand{\ottdefnComWt}[1]{\begin{ottdefnblock}[#1]{$ \Gamma \vdash \ottnt{m} : \ottnt{B} $}{}
|
|
\ottusedrule{\ottdruleTXXForce{}}
|
|
\ottusedrule{\ottdruleTXXLam{}}
|
|
\ottusedrule{\ottdruleTXXApp{}}
|
|
\ottusedrule{\ottdruleTXXRet{}}
|
|
\ottusedrule{\ottdruleTXXLet{}}
|
|
\ottusedrule{\ottdruleTXXCase{}}
|
|
\end{ottdefnblock}}
|
|
|
|
|
|
\newcommand{\ottdefnsTyping}{
|
|
\ottdefnValWt{}\ottdefnComWt{}}
|
|
|
|
% defns Red
|
|
%% defn StepVal
|
|
|
|
\newcommand{\ottdefnStepVal}[1]{\begin{ottdefnblock}[#1]{$ \ottnt{v} \rightsquigarrow \ottnt{w} $}{}
|
|
\end{ottdefnblock}}
|
|
|
|
%% defn StepCom
|
|
|
|
\newcommand{\ottdefnStepCom}[1]{\begin{ottdefnblock}[#1]{$ \ottnt{m} \rightsquigarrow \ottnt{n} $}{}
|
|
\end{ottdefnblock}}
|
|
|
|
%% defn StepVals
|
|
|
|
\newcommand{\ottdefnStepVals}[1]{\begin{ottdefnblock}[#1]{$ \ottnt{v} \rightsquigarrow^* \ottnt{w} $}{}
|
|
\end{ottdefnblock}}
|
|
|
|
%% defn StepComs
|
|
|
|
\newcommand{\ottdefnStepComs}[1]{\begin{ottdefnblock}[#1]{$ \ottnt{m} \rightsquigarrow^* \ottnt{n} $}{}
|
|
\end{ottdefnblock}}
|
|
|
|
|
|
\newcommand{\ottdefnsRed}{
|
|
\ottdefnStepVal{}\ottdefnStepCom{}\ottdefnStepVals{}\ottdefnStepComs{}}
|
|
|
|
% defns sn
|
|
%% defn snVal
|
|
\newcommand{\ottdrulesnXXVal}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \forall \ottnt{w} \mathpunct{.} \ottnt{v} \rightsquigarrow \ottnt{w} \Rightarrow \ottnt{w} \in \kw{sn} }%
|
|
}{
|
|
\ottnt{v} \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_Val}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesnXXForceXXinv}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \kw{force} \gap \ottnt{v} \in \kw{sn} }%
|
|
}{
|
|
\ottnt{v} \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_Force\_inv}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesnXXAppXXinvTwo}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \gap \ottnt{v} \in \kw{sn} }%
|
|
}{
|
|
\ottnt{v} \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_App\_inv2}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesnXXVar}[1]{\ottdrule[#1]{%
|
|
}{
|
|
\ottmv{x} \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_Var}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesnXXUnit}[1]{\ottdrule[#1]{%
|
|
}{
|
|
\kw{unit} \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_Unit}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesnXXInl}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{v} \in \kw{sn} }%
|
|
}{
|
|
\kw{inl} \gap \ottnt{v} \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_Inl}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesnXXInr}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{v} \in \kw{sn} }%
|
|
}{
|
|
\kw{inr} \gap \ottnt{v} \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_Inr}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesnXXThunk}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \in \kw{sn} }%
|
|
}{
|
|
\kw{thunk} \gap \ottnt{m} \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_Thunk}}{}%
|
|
}}
|
|
|
|
\newcommand{\ottdefnsnVal}[1]{\begin{ottdefnblock}[#1]{$ \ottnt{v} \in \kw{sn} $}{}
|
|
\ottusedrule{\ottdrulesnXXVal{}}
|
|
\ottusedrule{\ottdrulesnXXForceXXinv{}}
|
|
\ottusedrule{\ottdrulesnXXAppXXinvTwo{}}
|
|
\ottusedrule{\ottdrulesnXXVar{}}
|
|
\ottusedrule{\ottdrulesnXXUnit{}}
|
|
\ottusedrule{\ottdrulesnXXInl{}}
|
|
\ottusedrule{\ottdrulesnXXInr{}}
|
|
\ottusedrule{\ottdrulesnXXThunk{}}
|
|
\end{ottdefnblock}}
|
|
|
|
%% defn snCom
|
|
\newcommand{\ottdrulesnXXCom}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \forall \ottnt{n} \mathpunct{.} \ottnt{m} \rightsquigarrow \ottnt{n} \Rightarrow \ottnt{n} \in \kw{sn} }%
|
|
}{
|
|
\ottnt{m} \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_Com}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesnXXAppXXinvOne}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \gap \ottnt{v} \in \kw{sn} }%
|
|
}{
|
|
\ottnt{m} \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_App\_inv1}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesnXXLetXXinvOne}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \kw{let} \gap \ottmv{x} \leftarrow \ottnt{m} \gap \kw{in} \gap \ottnt{n} \in \kw{sn} }%
|
|
}{
|
|
\ottnt{m} \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_Let\_inv1}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesnXXLetXXinvTwo}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \kw{let} \gap \ottmv{x} \leftarrow \ottnt{m} \gap \kw{in} \gap \ottnt{n} \in \kw{sn} }%
|
|
}{
|
|
\ottnt{n} \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_Let\_inv2}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesnXXantisubst}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} [ \ottmv{x} \mapsto \ottnt{v} ] \in \kw{sn} }%
|
|
\ottpremise{ \ottnt{v} \in \kw{sn} }%
|
|
}{
|
|
\ottnt{m} \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_antisubst}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesnXXForceXXThunk}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \in \kw{sn} }%
|
|
}{
|
|
\kw{force} \gap ( \kw{thunk} \gap \ottnt{m} ) \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_Force\_Thunk}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesnXXAppXXLam}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{v} \in \kw{sn} }%
|
|
\ottpremise{ \ottnt{m} [ \ottmv{x} \mapsto \ottnt{v} ] \in \kw{sn} }%
|
|
}{
|
|
( \lambda \ottmv{x} \mathpunct{.} \ottnt{m} ) \gap \ottnt{v} \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_App\_Lam}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesnXXLetXXRet}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{v} \in \kw{sn} }%
|
|
\ottpremise{ \ottnt{m} [ \ottmv{x} \mapsto \ottnt{v} ] \in \kw{sn} }%
|
|
}{
|
|
\kw{let} \gap \ottmv{x} \leftarrow ( \kw{return} \gap \ottnt{v} ) \gap \kw{in} \gap \ottnt{m} \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_Let\_Ret}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesnXXCaseXXInl}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{v} \in \kw{sn} }%
|
|
\ottpremise{ \ottnt{m} [ \ottmv{y} \mapsto \ottnt{v} ] \in \kw{sn} }%
|
|
\ottpremise{ \ottnt{n} \in \kw{sn} }%
|
|
}{
|
|
\kw{case} \gap ( \kw{inl} \gap \ottnt{v} ) \gap \kw{of} \gap \lbrace \kw{inl} \gap \ottmv{y} \Rightarrow \ottnt{m} \mathrel{;} \kw{inr} \gap \ottmv{z} \Rightarrow \ottnt{n} \rbrace \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_Case\_Inl}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesnXXCaseXXInr}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{v} \in \kw{sn} }%
|
|
\ottpremise{ \ottnt{m} \in \kw{sn} }%
|
|
\ottpremise{ \ottnt{n} [ \ottmv{z} \mapsto \ottnt{v} ] \in \kw{sn} }%
|
|
}{
|
|
\kw{case} \gap ( \kw{inr} \gap \ottnt{v} ) \gap \kw{of} \gap \lbrace \kw{inl} \gap \ottmv{y} \Rightarrow \ottnt{m} \mathrel{;} \kw{inr} \gap \ottmv{z} \Rightarrow \ottnt{n} \rbrace \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_Case\_Inr}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesnXXAppXXbwd}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \leadsto_{ \kw{sn} } \ottnt{n} }%
|
|
\ottpremise{ \ottnt{v} \in \kw{sn} }%
|
|
\ottpremise{ \ottnt{n} \gap \ottnt{v} \in \kw{sn} }%
|
|
}{
|
|
\ottnt{m} \gap \ottnt{v} \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_App\_bwd}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesnXXLetXXbwd}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \leadsto_{ \kw{sn} } \ottnt{m'} }%
|
|
\ottpremise{ \ottnt{n} \in \kw{sn} }%
|
|
\ottpremise{ \kw{let} \gap \ottmv{x} \leftarrow \ottnt{m'} \gap \kw{in} \gap \ottnt{n} \in \kw{sn} }%
|
|
}{
|
|
\kw{let} \gap \ottmv{x} \leftarrow \ottnt{m} \gap \kw{in} \gap \ottnt{n} \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_Let\_bwd}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesnXXclosure}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \leadsto_{ \kw{sn} } \ottnt{n} }%
|
|
\ottpremise{ \ottnt{n} \in \kw{sn} }%
|
|
}{
|
|
\ottnt{m} \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_closure}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesnXXForce}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{v} \in \kw{sn} }%
|
|
}{
|
|
\kw{force} \gap \ottnt{v} \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_Force}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesnXXLam}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \in \kw{sn} }%
|
|
}{
|
|
\lambda \ottmv{x} \mathpunct{.} \ottnt{m} \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_Lam}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesnXXRet}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{v} \in \kw{sn} }%
|
|
}{
|
|
\kw{return} \gap \ottnt{v} \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_Ret}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesnXXApp}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \in \kw{sne} }%
|
|
\ottpremise{ \ottnt{v} \in \kw{sn} }%
|
|
}{
|
|
\ottnt{m} \gap \ottnt{v} \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_App}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesnXXLet}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \in \kw{sne} }%
|
|
\ottpremise{ \ottnt{n} \in \kw{sn} }%
|
|
}{
|
|
\kw{let} \gap \ottmv{x} \leftarrow \ottnt{m} \gap \kw{in} \gap \ottnt{n} \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_Let}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesnXXCase}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{v} \in \kw{sne} }%
|
|
\ottpremise{ \ottnt{m} \in \kw{sn} }%
|
|
\ottpremise{ \ottnt{n} \in \kw{sn} }%
|
|
}{
|
|
\kw{case} \gap \ottnt{v} \gap \kw{of} \gap \lbrace \kw{inl} \gap \ottmv{y} \Rightarrow \ottnt{m} \mathrel{;} \kw{inr} \gap \ottmv{z} \Rightarrow \ottnt{n} \rbrace \in \kw{sn} }{%
|
|
{\ottdrulename{sn\_Case}}{}%
|
|
}}
|
|
|
|
\newcommand{\ottdefnsnCom}[1]{\begin{ottdefnblock}[#1]{$ \ottnt{m} \in \kw{sn} $}{}
|
|
\ottusedrule{\ottdrulesnXXCom{}}
|
|
\ottusedrule{\ottdrulesnXXAppXXinvOne{}}
|
|
\ottusedrule{\ottdrulesnXXLetXXinvOne{}}
|
|
\ottusedrule{\ottdrulesnXXLetXXinvTwo{}}
|
|
\ottusedrule{\ottdrulesnXXantisubst{}}
|
|
\ottusedrule{\ottdrulesnXXForceXXThunk{}}
|
|
\ottusedrule{\ottdrulesnXXAppXXLam{}}
|
|
\ottusedrule{\ottdrulesnXXLetXXRet{}}
|
|
\ottusedrule{\ottdrulesnXXCaseXXInl{}}
|
|
\ottusedrule{\ottdrulesnXXCaseXXInr{}}
|
|
\ottusedrule{\ottdrulesnXXAppXXbwd{}}
|
|
\ottusedrule{\ottdrulesnXXLetXXbwd{}}
|
|
\ottusedrule{\ottdrulesnXXclosure{}}
|
|
\ottusedrule{\ottdrulesnXXForce{}}
|
|
\ottusedrule{\ottdrulesnXXLam{}}
|
|
\ottusedrule{\ottdrulesnXXRet{}}
|
|
\ottusedrule{\ottdrulesnXXApp{}}
|
|
\ottusedrule{\ottdrulesnXXLet{}}
|
|
\ottusedrule{\ottdrulesnXXCase{}}
|
|
\end{ottdefnblock}}
|
|
|
|
%% defn sr
|
|
\newcommand{\ottdrulesrXXThunk}[1]{\ottdrule[#1]{%
|
|
}{
|
|
\kw{force} \gap ( \kw{thunk} \gap \ottnt{m} ) \leadsto_{ \kw{sn} } \ottnt{m} }{%
|
|
{\ottdrulename{sr\_Thunk}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesrXXLam}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{v} \in \kw{sn} }%
|
|
}{
|
|
( \lambda \ottmv{x} \mathpunct{.} \ottnt{m} ) \gap \ottnt{v} \leadsto_{ \kw{sn} } \ottnt{m} [ \ottmv{x} \mapsto \ottnt{v} ] }{%
|
|
{\ottdrulename{sr\_Lam}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesrXXRet}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{v} \in \kw{sn} }%
|
|
}{
|
|
\kw{let} \gap \ottmv{x} \leftarrow ( \kw{return} \gap \ottnt{v} ) \gap \kw{in} \gap \ottnt{m} \leadsto_{ \kw{sn} } \ottnt{m} [ \ottmv{x} \mapsto \ottnt{v} ] }{%
|
|
{\ottdrulename{sr\_Ret}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesrXXInl}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{v} \in \kw{sn} }%
|
|
\ottpremise{ \ottnt{n} \in \kw{sn} }%
|
|
}{
|
|
\kw{case} \gap ( \kw{inl} \gap \ottnt{v} ) \gap \kw{of} \gap \lbrace \kw{inl} \gap \ottmv{y} \Rightarrow \ottnt{m} \mathrel{;} \kw{inr} \gap \ottmv{z} \Rightarrow \ottnt{n} \rbrace \leadsto_{ \kw{sn} } \ottnt{m} [ \ottmv{y} \mapsto \ottnt{v} ] }{%
|
|
{\ottdrulename{sr\_Inl}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesrXXInr}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{v} \in \kw{sn} }%
|
|
\ottpremise{ \ottnt{m} \in \kw{sn} }%
|
|
}{
|
|
\kw{case} \gap ( \kw{inr} \gap \ottnt{v} ) \gap \kw{of} \gap \lbrace \kw{inl} \gap \ottmv{y} \Rightarrow \ottnt{m} \mathrel{;} \kw{inr} \gap \ottmv{z} \Rightarrow \ottnt{n} \rbrace \leadsto_{ \kw{sn} } \ottnt{n} [ \ottmv{z} \mapsto \ottnt{v} ] }{%
|
|
{\ottdrulename{sr\_Inr}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesrXXApp}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \leadsto_{ \kw{sn} } \ottnt{n} }%
|
|
}{
|
|
\ottnt{m} \gap \ottnt{v} \leadsto_{ \kw{sn} } \ottnt{n} \gap \ottnt{v} }{%
|
|
{\ottdrulename{sr\_App}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdrulesrXXLet}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \leadsto_{ \kw{sn} } \ottnt{m'} }%
|
|
}{
|
|
\kw{let} \gap \ottmv{x} \leftarrow \ottnt{m} \gap \kw{in} \gap \ottnt{n} \leadsto_{ \kw{sn} } \kw{let} \gap \ottmv{x} \leftarrow \ottnt{m'} \gap \kw{in} \gap \ottnt{n} }{%
|
|
{\ottdrulename{sr\_Let}}{}%
|
|
}}
|
|
|
|
\newcommand{\ottdefnsr}[1]{\begin{ottdefnblock}[#1]{$ \ottnt{m} \leadsto_{ \kw{sn} } \ottnt{n} $}{}
|
|
\ottusedrule{\ottdrulesrXXThunk{}}
|
|
\ottusedrule{\ottdrulesrXXLam{}}
|
|
\ottusedrule{\ottdrulesrXXRet{}}
|
|
\ottusedrule{\ottdrulesrXXInl{}}
|
|
\ottusedrule{\ottdrulesrXXInr{}}
|
|
\ottusedrule{\ottdrulesrXXApp{}}
|
|
\ottusedrule{\ottdrulesrXXLet{}}
|
|
\end{ottdefnblock}}
|
|
|
|
%% defn neVal
|
|
\newcommand{\ottdruleneXXVar}[1]{\ottdrule[#1]{%
|
|
}{
|
|
\ottmv{x} \in \kw{ne} }{%
|
|
{\ottdrulename{ne\_Var}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleneXXStepVal}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{v} \rightsquigarrow \ottnt{w} }%
|
|
\ottpremise{ \ottnt{v} \in \kw{ne} }%
|
|
}{
|
|
\ottnt{w} \in \kw{ne} }{%
|
|
{\ottdrulename{ne\_StepVal}}{}%
|
|
}}
|
|
|
|
\newcommand{\ottdefnneVal}[1]{\begin{ottdefnblock}[#1]{$ \ottnt{v} \in \kw{ne} $}{}
|
|
\ottusedrule{\ottdruleneXXVar{}}
|
|
\ottusedrule{\ottdruleneXXStepVal{}}
|
|
\end{ottdefnblock}}
|
|
|
|
%% defn neCom
|
|
\newcommand{\ottdruleneXXForce}[1]{\ottdrule[#1]{%
|
|
}{
|
|
\kw{force} \gap \ottmv{x} \in \kw{ne} }{%
|
|
{\ottdrulename{ne\_Force}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleneXXApp}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \in \kw{ne} }%
|
|
}{
|
|
\ottnt{m} \gap \ottnt{v} \in \kw{ne} }{%
|
|
{\ottdrulename{ne\_App}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleneXXLet}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \in \kw{ne} }%
|
|
}{
|
|
\kw{let} \gap \ottmv{x} \leftarrow \ottnt{m} \gap \kw{in} \gap \ottnt{n} \in \kw{ne} }{%
|
|
{\ottdrulename{ne\_Let}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleneXXCase}[1]{\ottdrule[#1]{%
|
|
}{
|
|
\kw{case} \gap \ottmv{x} \gap \kw{of} \gap \lbrace \kw{inl} \gap \ottmv{y} \Rightarrow \ottnt{m} \mathrel{;} \kw{inr} \gap \ottmv{z} \Rightarrow \ottnt{n} \rbrace \in \kw{ne} }{%
|
|
{\ottdrulename{ne\_Case}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleneXXStepCom}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \rightsquigarrow \ottnt{n} }%
|
|
\ottpremise{ \ottnt{n} \in \kw{ne} }%
|
|
}{
|
|
\ottnt{m} \in \kw{ne} }{%
|
|
{\ottdrulename{ne\_StepCom}}{}%
|
|
}}
|
|
|
|
|
|
\newcommand{\ottdruleneXXSNe}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \in \kw{SNe} }%
|
|
}{
|
|
\ottnt{m} \in \kw{ne} }{%
|
|
{\ottdrulename{ne\_SNe}}{}%
|
|
}}
|
|
|
|
\newcommand{\ottdefnneCom}[1]{\begin{ottdefnblock}[#1]{$ \ottnt{m} \in \kw{ne} $}{}
|
|
\ottusedrule{\ottdruleneXXForce{}}
|
|
\ottusedrule{\ottdruleneXXApp{}}
|
|
\ottusedrule{\ottdruleneXXLet{}}
|
|
\ottusedrule{\ottdruleneXXCase{}}
|
|
\ottusedrule{\ottdruleneXXStepCom{}}
|
|
\ottusedrule{\ottdruleneXXSNe{}}
|
|
\end{ottdefnblock}}
|
|
|
|
%% defn sneVal
|
|
\newcommand{\ottdrulesnevalXXsne}[1]{\ottdrule[#1]{%
|
|
}{
|
|
\ottmv{x} \in \kw{sne} }{%
|
|
{\ottdrulename{sneval\_sne}}{}%
|
|
}}
|
|
|
|
\newcommand{\ottdefnsneVal}[1]{\begin{ottdefnblock}[#1]{$ \ottnt{v} \in \kw{sne} $}{}
|
|
\ottusedrule{\ottdrulesnevalXXsne{}}
|
|
\end{ottdefnblock}}
|
|
|
|
%% defn sneCom
|
|
\newcommand{\ottdrulesnecomXXsne}[1]{\ottdrule[#1]{%
|
|
\ottpremise{ \ottnt{m} \in \kw{ne} }%
|
|
\ottpremise{ \ottnt{m} \in \kw{sn} }%
|
|
}{
|
|
\ottnt{m} \in \kw{sne} }{%
|
|
{\ottdrulename{snecom\_sne}}{}%
|
|
}}
|
|
|
|
\newcommand{\ottdefnsneCom}[1]{\begin{ottdefnblock}[#1]{$ \ottnt{m} \in \kw{sne} $}{}
|
|
\ottusedrule{\ottdrulesnecomXXsne{}}
|
|
\end{ottdefnblock}}
|
|
|
|
|
|
\newcommand{\ottdefnssn}{
|
|
\ottdefnsnVal{}\ottdefnsnCom{}\ottdefnsr{}\ottdefnneVal{}\ottdefnneCom{}\ottdefnsneVal{}\ottdefnsneCom{}}
|
|
|
|
\newcommand{\ottdefnss}{
|
|
\ottdefnsSN
|
|
\ottdefnsLR
|
|
\ottdefnsLRs
|
|
\ottdefnsSem
|
|
\ottdefnsTyping
|
|
\ottdefnsRed
|
|
\ottdefnssn
|
|
}
|
|
|
|
\newcommand{\ottall}{\ottmetavars\\[0pt]
|
|
\ottgrammar\\[5.0mm]
|
|
\ottdefnss}
|
|
|