From e5c0950befae64abbdd81367bf180a849597e7f6 Mon Sep 17 00:00:00 2001 From: Jonathan Chan Date: Fri, 18 Apr 2025 16:48:40 -0400 Subject: [PATCH] Final project files --- .gitattributes | 1 + .gitignore | 4 +- Makefile | 47 ++ README.md | 3 +- cbpv.bib | 0 cbpv.mng | 650 ++++++++++++++++ cbpv.ott | 791 ++++++++++++++++++++ cbpv.pdf | 3 + cbpv.tex | 650 ++++++++++++++++ latexrun | 1938 ++++++++++++++++++++++++++++++++++++++++++++++++ listproc.sty | 349 +++++++++ ottalt.sty | 328 ++++++++ rules.tex | 1273 +++++++++++++++++++++++++++++++ 13 files changed, 6035 insertions(+), 2 deletions(-) create mode 100644 .gitattributes create mode 100644 Makefile create mode 100644 cbpv.bib create mode 100644 cbpv.mng create mode 100644 cbpv.ott create mode 100644 cbpv.pdf create mode 100644 cbpv.tex create mode 100755 latexrun create mode 100644 listproc.sty create mode 100644 ottalt.sty create mode 100644 rules.tex diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 0000000..cd6acc3 --- /dev/null +++ b/.gitattributes @@ -0,0 +1 @@ +cbpv.pdf filter=lfs diff=lfs merge=lfs -text diff --git a/.gitignore b/.gitignore index d163863..a3f47e9 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,3 @@ -build/ \ No newline at end of file +build/ +latex.out/ +.vscode/ \ No newline at end of file diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..024eb02 --- /dev/null +++ b/Makefile @@ -0,0 +1,47 @@ +MAIN := cbpv +RULES := rules +OLD := old +DIFF := diff + +LATEX_FLAGS := -jobname=$(MAIN) -shell-escape +LATEXRUN := ./latexrun -Wall --latex-cmd lualatex --latex-args "$(LATEX_FLAGS)" +LATEXDIFF := latexdiff +BIBTEX := bibtex + +OTT = ott +OTTFILES = $(MAIN).ott +OTT_FLAGS = -tex_wrap false -tex_show_meta false -merge true $(OTTFILES) + +MAKEDEPS := Makefile +LATEXDEPS := $(MAIN).bib +MOREDEPS := listproc.sty ottalt.sty +GENERATED := $(RULES).tex $(MAIN).tex + +all: $(MAIN).pdf + +$(RULES).tex: $(OTTFILES) + $(OTT) -o $(RULES).tex $(OTT_FLAGS) + +$(MAIN).tex: $(RULES).tex $(MAIN).mng + $(OTT) -tex_filter $(MAIN).mng $(MAIN).tex $(OTT_FLAGS) + +.PHONY: FORCE +$(MAIN).pdf: $(MAIN).tex $(LATEXDEPS) + $(LATEXRUN) $(MAIN).tex + +$(DIFF).pdf: $(RULES).tex $(MAIN).mng + $(LATEXDIFF) $(OLD).mng $(MAIN).mng > $(DIFF).mng + $(OTT) -tex_filter $(DIFF).mng $(DIFF).tex $(OTT_FLAGS) + $(LATEXRUN) -o $(DIFF).pdf $(DIFF).tex + rm $(DIFF).mng $(DIFF).tex + +.PHONY: zip +zip: $(MAIN).pdf + cp latex.out/$(MAIN).bbl $(MAIN).bbl + zip -o submit.zip $(MAIN).bbl $(LATEXDEPS) $(MOREDEPS) $(GENERATED) + rm $(MAIN).bbl + +.PHONY: clean +clean: + $(LATEXRUN) --clean-all + rm -f $(GENERATED) \ No newline at end of file diff --git a/README.md b/README.md index 46551c5..59eb55d 100644 --- a/README.md +++ b/README.md @@ -12,4 +12,5 @@ Exercise numbers refer to TAPL. | 4 | 13.3.1, 13.5.8 | 19 Feburary | | 5 | 15.3.6, 16.1.3, 16.2.5, 16.2.6, 16.3.2 | 24 Feburary | | 6 | Barendregt's or Gallier's normalization proof | 5 March | -| 7 | 22.3.9, 22.3.10, 22.4.6, 22.5.5 | 17 March | \ No newline at end of file +| 7 | 22.3.9, 22.3.10, 22.4.6, 22.5.5 | 17 March | +| 8 | 26.3.5, 26.4.11, 28.2.3, 28.7.1 | 26 March | \ No newline at end of file diff --git a/cbpv.bib b/cbpv.bib new file mode 100644 index 0000000..e69de29 diff --git a/cbpv.mng b/cbpv.mng new file mode 100644 index 0000000..399482c --- /dev/null +++ b/cbpv.mng @@ -0,0 +1,650 @@ +\documentclass{article} + +\usepackage[supertabular]{ottalt} +\let\newlist\relax +\let\renewlist\relax +\usepackage[T1]{fontenc} +\usepackage{mlmodern} +\usepackage[margin=1in]{geometry} +\usepackage{enumitem,float,booktabs,xspace,doi} +\usepackage{amsmath,amsthm,amssymb} +\usepackage[capitalize,nameinlink]{cleveref} +\usepackage{mathpartir,mathtools,stmaryrd} + +\setlist{nosep} +\hypersetup{ + colorlinks=true, + urlcolor=blue, + linkcolor=magenta, + citecolor=teal +} +\urlstyle{tt} + +\newtheorem{theorem}{Theorem} +\newtheorem{lemma}[theorem]{Lemma} +\newtheorem{corollary}[theorem]{Corollary} +\theoremstyle{definition} +\newtheorem{definition}{Definition} + +\newcommand{\ie}{\textit{i.e.}\@\xspace} +\newcommand{\ala}{\textit{\`a la}\@\xspace} +\newcommand{\apriori}{\textit{a priori}\@\xspace} +\newcommand{\aposteriori}{\textit{a posteriori}\@\xspace} + +\title{Strong Normalization for \\ Simply Typed Call-by-Push-Value} +\author{Jonathan Chan} +\date{} + +\inputott{rules} + +\begin{document} +\maketitle + +\section{Introduction} + +The goal of this project is to mechanize a proof of strong normalization for call-by-push-value (CBPV). +It follows work by Forster, Sch\"afer, Spies, and Stark (TODO: cite) on mechanizing the metatheory of CBPV in Rocq, +but instead adapts the proof technique from POPLMark Reloaded (TODO: cite). + +Both proofs, and mine, follow the same sequence of steps: +we define a logical relation that semantically interpret types as sets of terms, +show that these sets are backward closed by reduction and that they contain only strongly normalizing terms, +prove a fundamental soundness theorem that places well typed terms in the semantic interpretations of their types, +and conclude that well typed terms must be strongly normalizing. +The difference lies in \emph{how strong normalization} (and reduction) is defined. +The Rocq mechanization uses a traditional definition of strong normalization as an accessibility relation, +while POPLMark Reloaded and this project use an inductive characterization of strong normalization, +then prove it sound with respect to the traditional definition. + +In contrast to both prior works, which use Rocq, Agda, or Beluga, +this project is mechanized in Lean. +A secondary purpose of this project is to assess the capabilities of Lean for PL metatheory, +especially when making heavy use of mutually defined inductive types. +I have implemented a mutual induction tactic for Lean (TODO: link), +and the mutual values and computations of CBPV, +combined with the even more complex mutual inductives from POPLMark Reloaded, +make it an attractive test case to test the tactic's robustness. + +This report is divided in roughly the same shape as the proof development. +\Cref{sec:syntax} introduces the syntax and the typing rules for CBPV (\texttt{Syntax.lean}, \texttt{Typing.lean}). +Then the inductive characterization of strong normalization is defined in \cref{sec:sn-ind} (\texttt{NormalInd.lean}), +followed by the logical relation in \cref{sec:lr} (\texttt{OpenSemantics.lean}). +The central theorem of strong normalization is proven in \cref{sec:soundness} +as a corollary of the fundamental theorem for the logical relation (\texttt{Soundness.lean}, \texttt{Normalization.lean}). +To ensure that the inductive characterization is correct, +\cref{sec:sn-acc} shows that it implies the traditional definition of strong normalization (\texttt{NormalAcc.lean}). +This latter definition and proof depends on small-step reduction on open terms, +whose properties are omitted here (\texttt{Reduction.lean}). +In general, I gloss over details about substitution and reduction, +since I'm interested in presenting the structure of the strong normalization proof +and not the minutiae of syntax and binding. +Finally, I discuss the merits of this proof technique +and the challenges posed by using Lean in \cref{sec:discussion}. + +\section{Syntax and Typing} \label{sec:syntax} + +\begin{align*} + [[A]] &\Coloneqq [[Unit]] \mid [[A1 + A2]] \mid [[U B]] & \textit{value types} \\ + [[B]] &\Coloneqq [[A → B]] \mid [[F A]] & \textit{computation types} \\ + [[v]], [[w]] &\Coloneqq [[x]] \mid [[unit]] \mid [[inl v]] \mid [[inr v]] \mid [[thunk m]] & \textit{values} \\ + [[m]], [[n]] &\Coloneqq [[force v]] \mid [[λx. m]] \mid [[m v]] \mid [[ret v]] & \textit{computations} \\ + & \mid [[let x m n]] \\ + & \mid [[case v | y.m | z.n]] \\ + [[G]] &\Coloneqq [[•]] \mid [[G, x : A]] & \textit{typing contexts} \\ + [[s]] &\Coloneqq [[•]] \mid [[s, x ↦ v]] & \textit{simultaneous substitutions} +\end{align*} + +The grammar of the CBPV for this project is given above. +Terms and their types are divided between \emph{values} and \emph{computations}. +Values are variables, unit, injections into a sum type, or a thunked computation, +while computations are forcing thunks, +functions, applications, returning values, binding returned values, +and case analysis on sums. +There are only value variables and no computation variables, +since they represent terms that require no more work to be done on them ready to be substituted in, +and typing contexts similarly only contain value types. +I use $t$ to refer to terms that may be either values or computations. + +Although the syntax is presented nominally, +the mechanization uses an unscoped de Bruijn indexed representation of variables, +along with simultaneous substitutions $[[s]]$ mapping variables to values, +with $[[•]]$ as the identity substitution. +Applying a substitution is represented as $[[v{s}]]$ and $[[m{s}]]$, +and implemented in terms of renamings, +which are mappings from variables to other variables. + +This is not the usual complete CBPV language, +since it's missing both value tuples and computation tuples. +I exclude them because they are syntactically not much more interesting than returns, +whose eliminator is shaped like pattern matching on a singleton value tuple, +and than thunks, +whose eliminator is shaped like projection on a singleton computation tuple. +In contrast, I do include sums, which represent the only way a computation can branch. + +The typing rules below are standard for the values and computations included. +The judgements for values and computations are defined mutually, +just as are the types and the terms. + +\drules[T]{$[[G ⊢ v : A]]$}{value typing}{Var,Unit,Inl,Inr,Thunk} +\drules[T]{$[[G ⊢ m : B]]$}{computation typing}{Force,Lam,App,Ret,Let,Case} + +\section{Strong Normalization as an Inductive Definition} \label{sec:sn-ind} + +The idea behind the inductive characterization of strong normalization +is to describe case by case when a term is strongly normal, +rather than showing \aposteriori which terms are strongly normal. +This is done in conjunction with defining strongly neutral terms, +which are blocked from $\beta$-reduction, +and strong head reduction, +which expands the set from normal forms +to terms which must reduce to normal forms. + +The general recipe for defining these for CBPV is as follows: +\begin{itemize}[rightmargin=\leftmargin] + \item The only strongly neutral values are variables. + \item Strongly neutral computations are eliminators + whose head positions are strongly neutral, + while all other subterms are strongly normal. + \item Strongly normal values are constructors + whose subterms are strongly normal, + or strongly neutral values, \ie variables. + \item Strongly normal computations are constructors + whose subterms are strongly normal, + or strongly neutral computations, + or computations which reduce to strongly normal computations + (backward closure). + \item Strong head reduction consists of $\beta$ reductions + for all eliminators around the corresponding constructors, + and congruent reductions in head positions. +\end{itemize} + +Additionally, strong reduction requires premises asserting that +the subterms that may ``disappear'' after reduction be strongly normal +so that backward closure actually closes over strongly normal terms. +These subterms are the values that get substituted into a computation, +which may disappear if the computation never actually uses the binding, +as well as computation branches not taken. + +Because we're dealing with CBPV, values have no $\beta$ reductions, +so there's no need for head reduction of values as there are no heads. +Furthermore, there is only one strongly neutral value, +so we inline the definition as a variable where needed, +but also write it as $[[v ∈ SNe]]$ for symmetry as appropriate. +Otherwise, the remaining four judgements are defined mutually below. + +\drules[SNe]{$[[m ∈ SNe]]$}{strongly neutral computations}{Force,App,Let,Case} +\drules[SN]{$[[v ∈ SN]]$}{strongly normal values}{Var,Unit,Inl,Inr,Thunk} +\drules[SN]{$[[m ∈ SN]]$}{strongly normal computations}{Lam,Ret,SNe,Red} +\drules[SR]{$[[m ⤳ n]]$}{strong head reduction}{Thunk,Lam,Ret,Inl,Inr,App,Let} +\drules[SRs]{$[[m ⤳* n]]$}{reflexive, transitive closure of head reduction}{Refl,Trans} + +We also need the reflexive, transitive closure of head reduction, +defined as a separate inductive above. +Now we show a few simple lemmas about it, +along with an inversion lemma for forcing +(other inversion lemmas hold, but this is the only one we need). +I present them below as judgement pseudorules +using a dashed line to indicate that they are admissible rules. +These are all proven either by construction +or by induction on the first premise. + +\begin{mathpar} +\mprset{fraction={-~}{-~}{-}} +\drule[]{SRs-Once} +\drule[]{SRs-TransPP} +\drule[]{SRs-App} +\drule[]{SRs-Let} +\drule[]{SN-Reds} +\drule[]{SN-Force-inv} +\end{mathpar} + +The most important property of strongly normal terms that we need is antirenaming, +which states that undoing a renaming does not change the term's +normalization or reduction behaviour. +A crucial property that follows is extensionality of applications, +which is an inversion lemma specifically when the application argument is a variable. + +\begin{lemma}[Antirenaming] \label{thm:antisubst} + Let $[[s]]$ be a renaming, + \ie a substitution mapping variables to variables. + Then the following hold: + \begin{enumerate} + \item If $[[m{s} ∈ SNe]]$ then $[[m ∈ SNe]]$. + \item If $[[v{s} ∈ SN]]$ then $[[v ∈ SN]]$. + \item If $[[m{s} ∈ SN]]$ then $[[m ∈ SN]]$. + \item If $[[m{s} ⤳ n]]$ then there exists some $[[n']]$ + such that $[[n]] = [[n'{s}]]$ and $[[m ⤳ n']]$. + \end{enumerate} +\end{lemma} + +\begin{proof} + By mutual induction on the four derivations of + $[[m{s} ∈ SNe]]$, $[[v{s} ∈ SN]]$, $[[m{s} ∈ SN]]$, and $[[m{s} ⤳ n]]$. +\end{proof} + +\begin{corollary}[Extensionality] \label{cor:ext} + If $[[m x ∈ SN]]$ then $[[m ∈ SN]]$. +\end{corollary} + +\begin{proof} + By induction on the derivation of strongly normal values. + The possible cases are \rref*{SN-SNe,SN-Red}. + Destructing the premise of the former gives $[[m ∈ SNe]]$, + and we conclude using \rref{SN-SNe} again. + In the latter case, we have $[[m x ⤳ n]]$ and $[[n ∈ SN]]$; + destructing on the reduction yields the possible cases + \rref{SR-Lam,SR-App}. + In the first case, we have $[[m{x ↦ v} ∈ SN]]$, + so the goal holds by \nameref{thm:antisubst}. + In the second case, we have $[[m ⤳ n]]$ and $[[n x ∈ SN]]$, + so by the induction hypothesis, we have $[[n ∈ SN]]$, + and we conclude using \rref{SN-Red}. +\end{proof} + +\section{Logical Relation on Open Terms} \label{sec:lr} + +The next step is to define a logical relation that semantically interprets types +as sets of open terms. +The key property we need from these sets is that they contain only strongly normal terms. +Because we are working with open terms to prove normalization +and not just termination of evaluation of closed terms, +we need to consider variables and strongly neutral terms. +Having no other information about them other than their strong neutrality, +we require that the interpretation sets always contain all strongly neutral terms. + +The logical relation on simple types can be defined by induction on the structure of the type. +However, I want to maximize the amount of mutual inductives used in this project, +so we instead define the logical relation as an inductive binary relation +between the type and the set of terms of its interpretation, +denoted as $[[⟦A⟧ ↘ P]]$ and $[[⟦B⟧ ↘ P]]$ below. +I use set builder notation to define the sets and set membership, +but they are implemented in the mechanization as functions +that take terms and return propositions and as function applications. +Here, the conjunctions ($\wedge$), disjunctions ($\vee$), equalities ($=$), implications ($\Rightarrow$), +and universal ($\forall$) and existential ($\exists$) quantifiers +are part of the metatheory, not part of the object language. + +\drules[LR]{$[[⟦A⟧ ↘ P]]$}{semantic interpretation of value types}{Unit,U,Sum} +\drules[LR]{$[[⟦B⟧ ↘ P]]$}{semantic interpretation of computation types}{F,Arr} + +The terms in the interpretation of a type can be characterized in two different ways: +by what constructor of that type they reduce to, +or by how they act when eliminated by an eliminator for that type. +For the former, we need to explicitly include the possibility of the term being strongly neutral. +I chose the following characterizations because they seemed the simplest to me, +but the alternate choices likely work as well. + +\begin{itemize}[noitemsep,rightmargin=\leftmargin] + \item Values in the interpretation of the unit type + are either variables or the unit value. + \item Values are in the interpretation of the $[[U B]]$ type + if they can be forced to computations in the interpretation of the $[[B]]$ type. + \item Values in the interpretation of the sum type $[[A1 + A2]]$ are either variables, + left injections whose values are in the interpretation of $[[A1]]$, + or right injections whose values are in that of $[[A2]]$. + \item Computations in the interpretation of the $[[F A]]$ type + reduce to either a neutral computation + or a return whose value is in the interpretation of $[[A]]$. + \item Computations are in the interpretation of the function type $[[A → B]]$ + if applying them to values in the interpretation of $[[A]]$ + yields computations in the interpretation of $[[B]]$. +\end{itemize} + +By this description, it sounds like the logical relation can be presented +directly as a relation between a type and a term; +this presentation is given in \cref{fig:lr-alt}. +Unfortunately, this is not well defined, +since the logical relation appears in a negative position +(to the left of an implication) in the premise of \rref{LRPP-Arr}. +The alternate presentation can be interpreted as a function +match on the term and the type and returning the conjunction of its premises, +but I wanted to use a mutually defined inductive definition. + +\begin{figure}[H] +\fbox{$[[v ∈ ⟦A⟧]]$} \quad \fbox{$[[m ∈ ⟦B⟧]]$} \hfill \textit{} \\ +\begin{mathpar} +\drule[]{LRPP-Unit-var} +\drule[]{LRPP-Unit-unit} +\drule[]{LRPP-Sum-var} +\drule[]{LRPP-Sum-inl} +\drule[]{LRPP-Sum-inr} +\drule[]{LRPP-Force} +\drule[]{LRPP-F-var} +\drule[]{LRPP-F-ret} +\drule[]{LRPP-Arr} +\end{mathpar} +\caption{Alternate presentation of the logical relation} +\label{fig:lr-alt} +\end{figure} + +Using the inductive presentation of the logical relation, +there are three easy properties to show: +interpretability, which states that all types have an interpretation; +determinism, which states that the interpretation indeed behaves like a function +from types to sets of terms; +and backward closure, which states that the interpretations of computation types +are backward closed under multi-step head reduction. +The last property is why \rref{LRPP-F-var} needs to include +computations that \emph{reduce to} strongly neutral terms or returns, +not merely ones that are such terms. + +\begin{lemma}[Interpretability] \label{lem:interp} \leavevmode + \begin{enumerate} + \item Given $[[A]]$, there exists $[[P]]$ such that $[[⟦A⟧ ↘ P]]$. + \item Given $[[B]]$, there exists $[[P]]$ such that $[[⟦B⟧ ↘ P]]$. + \end{enumerate} +\end{lemma} + +\begin{proof} + By mutual induction on the types $[[A]]$ and $[[B]]$. +\end{proof} + +\begin{lemma}[Determinism] \label{lem:det} \leavevmode + \begin{enumerate} + \item If $[[⟦A⟧ ↘ P]]$ and $[[⟦A⟧ ↘ Q]]$ then $[[P]] = [[Q]]$. + \item If $[[⟦B⟧ ↘ P]]$ and $[[⟦B⟧ ↘ Q]]$ then $[[P]] = [[Q]]$. + \end{enumerate} +\end{lemma} + +\begin{proof} + By mutual induction on the first derivations of the logical relation, + then by cases on the second derivations. +\end{proof} + +\begin{lemma}[Backward closure] \label{lem:closure} + Given $[[⟦B⟧ ↘ P]]$ and $[[m ⤳* n]]$, + if $[[n ∈ P]]$ then $[[m ∈ P]]$. +\end{lemma} + +\begin{proof} + By induction on the derivation of the logical relation. +\end{proof} + +The final key property is adequacy, +which states that the interpretations of types +must contain all strongly neutral terms +and must contain only strongly normal terms. +Such sets are said to be \emph{reducibility candidates}. + +\begin{definition}[Reducibility candidates] + A reducibility candidate is a set of terms $[[P]]$ where, + given a term $[[t]]$, + if $[[t ∈ SNe]]$ then $[[t ∈ P]]$, and + if $[[t ∈ P]]$ then $[[t ∈ SN]]$. +\end{definition} + +\begin{lemma}[Adequacy] \label{lem:adequacy} \leavevmode + \begin{enumerate} + \item If $[[⟦A⟧ ↘ P]]$ then $[[P]]$ is a reducibility candidate. + \item If $[[⟦B⟧ ↘ P]]$ then $[[P]]$ is a reducibility candidate. + \end{enumerate} +\end{lemma} + +\begin{proof} + By mutual induction on the derivations of the logical relation. + \Rref{SN-Force-inv} is used in the \rref*{S-U} case, + while \rref{SN-Reds} is used in the \rref{S-F} case. + In the \rref*{S-Arr} case on $[[A → B]]$, + where $[[⟦A⟧ ↘ P]]$ and $[[⟦B⟧ ↘ Q]]$, + to show the second part of its interpretation being a reducibility candidate, + we are given $[[m]]$ such that for every $[[v ∈ P]]$, $[[m v ∈ Q]]$, + and the goal is to show that $[[m ∈ SN]]$. + By the induction hypotheses, picking an arbitrary variable $[[x]]$, + we have that $[[x ∈ P]]$ (since it is neutral) and that $[[m x ∈ SN]]$. + Then the goal holds by \nameref{cor:ext}. +\end{proof} + +\section{Semantic Typing and the Fundamental Theorem} \label{sec:soundness} + +Now that we know that the interpretations contain only strongly normal terms, +our goal is to show that well typed terms inhabit the interpretations of their types. +We first define what it means for a substitution to be +semantically well formed with respect to a context. + +\begin{definition}[Semantic well-formedness of substitutions] + A substitution $[[s]]$ is well formed with respect to a context $[[G]]$, + written $[[G ⊧ s]]$, if for every $[[x : A ∈ G]]$ and $[[⟦A⟧ ↘ P]]$, + we have $[[x{s} ∈ P]]$. + In short, the substitution maps variables in the context + to values in the interpretations of their types. +\end{definition} + +These judgements can be built up inductively, +as demonstrated by the below admissible rules, +which are proven by cases. + +{\mprset{fraction={-~}{-~}{-}} +\drules[S]{$[[G ⊧ s]]$}{admissible semantic substitution well-formedness}{Nil,Cons} +} + +Then we can define semantic typing in terms of the logical relation, +using semantic well formedness of substitutions to handle the context. + +\begin{definition}[Semantic typing] + \begin{enumerate}[rightmargin=\leftmargin] \leavevmode + \item $[[v]]$ semantically has type $[[A]]$ under context $[[G]]$, + written $[[G ⊧ v : A]]$, if for every $[[s]]$ such that $[[G ⊧ s]]$, + there exists an interpretation $[[⟦A⟧ ↘ P]]$ such that $[[v{s} ∈ P]]$. + \item $[[m]]$ semantically has type $[[B]]$ under context $[[G]]$, + written $[[G ⊧ m : B]]$, if for every $[[s]]$ such that $[[G ⊧ s]]$, + there exists an interpretation $[[⟦B⟧ ↘ P]]$ such that $[[m{s} ∈ P]]$. + \end{enumerate} +\end{definition} + +Semantic typing follows exactly the same shape of rules as syntactic typing, +so I present them here as admissible rules. +All the hard work happens in these lemmas; +the fundamental theorem of soundness of syntactic typing with respect to semantic typing +then follows directly. +Normalization holds as an easy corollary. + +{\mprset{fraction={-~}{-~}{-}} +\drules[S]{$[[G ⊧ v : A]]$}{admissible semantic value typing}{Var,Unit,Inl,Inr,Thunk} +\drules[S]{$[[G ⊧ m : B]]$}{admissible semantic computation typing}{Force,Arr,App,Ret,Let,Case} +} + +\begin{proof} + By construction using prior lemmas, + in particular \rref{SRs-Let} in case \rref*{S-Let}; + \nameref{lem:interp} in cases \rref*{S-Var,S-Inl,S-Inr,S-Lam}; + \nameref{lem:det} in cases \rref*{S-Lam,S-App}; + \nameref{lem:closure} in cases \rref*{S-Thunk,S-Lam,S-Let,S-Case}; and + \nameref{lem:adequacy} in cases \rref*{S-Lam,S-Let,S-Case}. +\end{proof} + +\begin{theorem}[Soundness] \label{thm:soundness} \leavevmode + \begin{enumerate} + \item If $[[G ⊢ v : A]]$ then $[[G ⊧ v : A]]$. + \item If $[[G ⊢ m : B]]$ then $[[G ⊧ m : B]]$. + \end{enumerate} +\end{theorem} + +\begin{proof} + By mutual induction on the syntactic typing derivations, + using the admissible semantic typing rules. +\end{proof} + +\begin{corollary}[Normalization] \leavevmode + \begin{enumerate} + \item If $[[G ⊢ v : A]]$ then $[[v ∈ SN]]$. + \item If $[[G ⊢ m : B]]$ then $[[m ∈ SN]]$. + \end{enumerate} +\end{corollary} + +\begin{proof} + By \nameref{thm:soundness}, + using the identity substitution and \rref{S-Nil}, + the well typed terms inhabit the semantic interpretations of their types. + Then by \nameref{lem:adequacy}, + they are also strongly normalizing. +\end{proof} + +\section{Strong Normalization as an Accessibility Relation} \label{sec:sn-acc} + +\drules[sn]{$[[v ∈ sn]], [[m ∈ sn]]$}{strongly normalizing terms}{Val,Com} +\drules[sr]{$[[m ⤳' n]]$}{strong head reduction}{Thunk,Lam,Ret,Inl,Inr,App,Let} +\drules[ne]{$[[m ∈ ne]]$}{neutral computations}{Force,App,Let,Case} + +\begin{mathpar} +\mprset{fraction={-~}{-~}{-}} +\drule[]{sn-App-invOne} +\drule[]{sn-App-invTwo} +\drule[]{sn-Let-invOne} +\drule[]{sn-Let-invTwo} +\end{mathpar} + +\begin{proof} + By induction on the premises of strongly normal terms, + using congruence of single-step reduction. +\end{proof} + +\begin{definition}[Neutral values] + A value is neutral, written $[[v ∈ ne]]$, if it is a variable. +\end{definition} + +\begin{lemma}[Preservation] \label{lem:preservation} \leavevmode + \begin{enumerate} + \item If $[[v ⇝ w]]$ and $[[v ∈ ne]]$ then $[[w ∈ ne]]$. + \item If $[[m ⇝ n]]$ and $[[m ∈ ne]]$ then $[[n ∈ ne]]$. + \end{enumerate} +\end{lemma} + +\begin{proof} + By mutual induction on the single-step reductions. +\end{proof} + +\begin{definition}[Strongly neutral computations] + A strongly neutral computation, written $[[m ∈ sne]]$, + is a computation that is both neutral and strongly normalizing, + \ie $[[m ∈ ne]]$ and $[[m ∈ sn]]$. +\end{definition} + +{\mprset{fraction={-~}{-~}{-}} +\drules[sn]{$[[v ∈ sn]]$}{admissible strongly normal values}{Var,Unit,Inl,Inr,Thunk} +\drules[sn]{$[[m ∈ sn]]$}{admissible strongly normal computations}{Lam,Ret,Force,App,Let,Case} +} + +\begin{proof} + \Rref{sn-App,sn-Let,sn-Case} are proven by double induction + on the two derivations of strongly normal terms. + Intuitively, we want to show that if the conclusion steps, + then it steps to a strongly normal term, + knowing by the induction hypotheses that if their subterms reduce, + then they also reduce to strongly normal terms. + Neutrality of the term in head position eliminates cases where the conclusion $\beta$-reduces, + leaving only the congruent reductions. + Because single-step reduction only steps in one subterm, + we only need the induction hypothesis for that reducing subterm, + so the double induction is really a lexicographic induction on the two derivations. + We additionally require \nameref{lem:preservation} to carry along neutrality + when the heads reduce in cases \rref*{sn-App,sn-Let}. + All other cases are direct by construction + or by induction on their sole premise. +\end{proof} + +% admissible rules missing backward closure \rref{SN-Red} + +\begin{lemma}[Antisubstitution (\textsf{sn})] \label{lem:antisubst-sn} + If $[[m{x ↦ v} ∈ sn]]$ and $[[v ∈ sn]]$ then $[[m ∈ sn]]$. +\end{lemma} + +\begin{proof} + By induction on the derivation of $[[m{x ↦ v} ∈ sn]]$. +\end{proof} + +{\mprset{fraction={-~}{-~}{-}} +\drules[sn]{$[[m ∈ sn]]$}{head expansion}{Force-Thunk,App-Lam,Let-Ret,Case-Inl,Case-Inr} +} + +\begin{proof} + \Rref{sn-Force-Thunk} holds directly by induction on the premise; + the remaining proofs are more complex. + First, given the premise $[[m{x ↦ v} ∈ sn]]$ (or $[[n{z ↦ v}]]$), + use \nameref{lem:antisubst-sn} to obtain $[[m ∈ sn]]$. + Then proceed by double (or triple) induction on the derivations of + $[[v ∈ sn]]$ and $[[m ∈ sn]]$ (and $[[n ∈ sn]]$ for the case rules). + Similarly to the admissible strongly normal rules, + these are lexicographic inductions, + except $[[m{x ↦ v} ∈ sn]]$ (or $[[n{z ↦ v}]]$) + is used to satisfy the $\beta$-reduction cases. +\end{proof} + +\begin{lemma}[Confluence] \label{lem:confluence} + If $[[m ⇝ n1]]$ and $[[m ⤳' n2]]$, then either $[[n1]] = [[n2]]$, + or there exists some $[[m']]$ such that + $[[n1 ⤳' m']]$ and $[[n2 ⇝ m']]$. +\end{lemma} + +\begin{proof} + By induction on the derivation of $[[m ⤳' n2]]$, + then by cases on the derivation of $[[m ⇝ n1]]$. +\end{proof} + +\begin{mathpar} +\mprset{fraction={-~}{-~}{-}} +\fbox{$[[m ∈ sn]]$} \hfill \textit{backward closure in head position} \\ +\drule[width=0.45\textwidth]{sn-App-bwd} +\drule[width=0.55\textwidth]{sn-Let-bwd} +\end{mathpar} + +\begin{proof} + First, use \rref{sn-App-inv,sn-Let-inv} to obtain $[[m ∈ sn]]$. + Then proceed by double induction on the derivations of + $[[m ∈ sn]]$ and $[[v ∈ sn]]$/$[[n ∈ sn]]$, + again as lexicographic induction. + We want to show that if the conclusion steps, + then it steps to a strongly normal term. + Strong reduction of the head position eliminates the cases of $\beta$-reduction, + leaving the cases where the head position steps or the other position steps. + If the head position steps, we use \nameref{lem:confluence} + to join the strong reduction and the single-step reduction together, + then use the first induction hypothesis. + Otherwise, we use the second induction hypothesis. + We need the last premise to step through either of the subterms, + since we have no congruence rule for when the head position is not neutral. +\end{proof} + +\begin{lemma}[Backward closure] \label{lem:closure} + If $[[m ⤳' n]]$ and $[[n ∈ sn]]$ then $[[m ∈ sn]]$. +\end{lemma} + +\begin{proof} + By induction on the derivation of $[[m ⤳' n]]$. + The cases correspond exactly to each of + \rref{sn-Force-Thunk,sn-App-Lam,sn-Let-Ret,sn-Case-Inl,sn-Case-Inr,sn-App-bwd,sn-Let-bwd}. +\end{proof} + +\begin{lemma}[Soundness (\textsf{SNe})] \label{lem:sound-sne} + If $[[m ∈ SNe]]$ then $[[m ∈ ne]]$. +\end{lemma} + +\begin{proof} + By induction on the derivation of $[[m ∈ SNe]]$. +\end{proof} + +\begin{theorem}[Soundness (\textsf{SN})] \leavevmode + \begin{enumerate} + \item If $[[m ∈ SNe]]$ then $[[m ∈ sn]]$. + \item If $[[v ∈ SN]]$ then $[[v ∈ sn]]$. + \item If $[[m ∈ SN]]$ then $[[m ∈ sn]]$. + \item If $[[m ⤳ n]]$ then $[[m ⤳' n]]$. + \end{enumerate} +\end{theorem} + +\begin{proof} + By mutual induction on the derivations of + $[[m ∈ SNe]]$, $[[v ∈ SN]]$, $[[m ∈ SN]]$, and $[[m ⤳ n]]$. + The cases for the first three correspond to the admissible strongly normal rules, + using \nameref{lem:sound-sne} as needed, + except for the \rref*{SN-Red} case, which uses \nameref{lem:closure}. + The cases for strong reduction hold by construction. +\end{proof} + +\begin{corollary} + If $[[G ⊢ v : A]]$ then $[[v ∈ sn]]$, + and if $[[G ⊢ m : B]]$ then $[[m ∈ sn]]$. +\end{corollary} + +\section{Discussion} \label{sec:discussion} + +\end{document} \ No newline at end of file diff --git a/cbpv.ott b/cbpv.ott new file mode 100644 index 0000000..6a38bf2 --- /dev/null +++ b/cbpv.ott @@ -0,0 +1,791 @@ +embed + {{ tex-preamble + \newcommand{\gap}{\:} + \newcommand{\kw}[1]{ \mathsf{#1} } + }} + +metavar x, y, z ::= + {{ com term variables }} + {{ lex alphanum }} + +grammar + +v, w :: 'val_' ::= {{ com values }} + | x :: :: Var + | unit :: :: Unit + {{ tex \kw{unit} }} + | inl v :: :: Inl + {{ tex \kw{inl} \gap [[v]] }} + | inr v :: :: Inr + {{ tex \kw{inr} \gap [[v]] }} + | thunk m :: :: Thunk + {{ tex \kw{thunk} \gap [[m]] }} + | ( v ) :: S :: Parens + {{ com parentheses }} + {{ tex ([[v]]) }} + | v { s } :: S :: Subst + {{ tex [[v]][ [[s]] ]}} + +m, n :: 'com_' ::= {{ com computations }} + | force v :: :: Force + {{ tex \kw{force} \gap [[v]] }} + | λ x . m :: :: Lam + (+ bind x in m +) + {{ tex \lambda [[x]] \mathpunct{.} [[m]] }} + | m v :: :: App + {{ tex [[m]] \gap [[v]] }} + | ret v :: :: Ret + {{ tex \kw{return} \gap [[v]] }} + | let x m n :: :: Let + (+ bind x in n +) + {{ tex \kw{let} \gap [[x]] \leftarrow [[m]] \gap \kw{in} \gap [[n]] }} + | case v | y . m | z . n :: :: Case + (+ bind y in m +) + (+ bind z in n +) + {{ tex \kw{case} \gap [[v]] \gap \kw{of} \gap \lbrace \kw{inl} \gap [[y]] \Rightarrow [[m]] \mathrel{;} \kw{inr} \gap [[z]] \Rightarrow [[n]] \rbrace }} + | ( m ) :: S :: Parens + {{ com parentheses }} + {{ tex ([[m]]) }} + | m { s } :: S :: Subst + {{ tex [[m]][ [[s]] ]}} + +A :: 'valtype_' ::= {{ com value types }} + | Unit :: :: Unit + {{ tex \kw{Unit} }} + | A1 + A2 :: :: Sum + {{ tex [[A1]] + [[A2]] }} + | U B :: :: U + {{ tex \kw{U} \gap [[B]] }} + +B :: 'comtype_' ::= {{ com computation types }} + | F A :: :: F + {{ tex \kw{F} \gap [[A]] }} + | A → B :: :: Arr + {{ tex [[A]] \rightarrow [[B]] }} + +s {{ tex \sigma }} :: 'subst_' ::= {{ com substitutions }} + | • :: :: Nil + {{ com identity substitution }} + {{ tex \cdot }} + | s , x ↦ v :: :: Cons + {{ com substitution extension }} + {{ tex [[s]], [[x]] \mapsto [[v]] }} + | x ↦ v :: S :: Single + {{ com single substitution }} + {{ tex [[x]] \mapsto [[v]] }} + | ⇑ s :: :: Lift + {{ com lifting substitution }} + {{ tex \mathop{\Uparrow} [[s]] }} + +G {{ tex \Gamma }}, D {{ tex \Delta }} :: 'ctxt_' ::= {{ com contexts }} + | • :: :: Nil + {{ com empty context }} + {{ tex \cdot }} + | G , x : A :: :: Cons + {{ com context extension }} + {{ tex [[G]], [[x]] \mathbin{:} [[A]] }} + +P, Q :: 'set_' ::= + | { v | formula } :: :: valset + {{ tex \lbrace [[v]] \mid [[formula]] \rbrace }} + | { m | formula } :: :: comset + {{ tex \lbrace [[m]] \mid [[formula]] \rbrace }} + +formula :: 'formula_' ::= + | judgement :: :: judgement + | formula1 ∧ formula2 :: :: and + {{ tex [[formula1]] \wedge [[formula2]] }} + | formula1 ∨ formula2 :: :: or + {{ tex [[formula1]] \vee [[formula2]] }} + | formula1 ⇒ formula2 :: :: implies + {{ tex [[formula1]] \Rightarrow [[formula2]] }} + | x : A ∈ G :: :: in + {{ tex [[x]] : [[A]] \in [[G]] }} + | v = w :: :: equals + {{ tex [[v]] = [[w]] }} + | v ∈ P :: :: valin + {{ tex [[v]] \in [[P]] }} + | m ∈ P :: :: comin + {{ tex [[m]] \in [[P]] }} + | ∀ v . formula :: :: valforall + {{ tex \forall [[v]] \mathpunct{.} [[formula]] }} + | ∀ m . formula :: :: comforall + {{ tex \forall [[m]] \mathpunct{.} [[formula]] }} + | ∃ v . formula :: :: valexists + {{ tex \exists [[v]] \mathpunct{.} [[formula]] }} + | ∃ m . formula :: :: comexists + {{ tex \exists [[m]] \mathpunct{.} [[formula]] }} + | ( formula ) :: :: parentheses + {{ tex ( [[formula ]] ) }} + | (# formula #) :: :: sparentheses + {{ tex [[formula]] }} + +%% Inductive definition of strong normalization %% + +defns +SN :: '' ::= + +defn + v ∈ SNe :: :: SNeVal :: 'SNe_' + {{ tex [[v]] \in \kw{SNe} }} +by + +------- :: Var +x ∈ SNe + +defn + m ∈ SNe :: :: SNeCom :: 'SNe_' + {{ tex [[m]] \in \kw{SNe} }} +by + +------------- :: Force +force x ∈ SNe + +m ∈ SNe +v ∈ SN +--------- :: App +m v ∈ SNe + +m ∈ SNe +n ∈ SN +--------------- :: Let +let x m n ∈ SNe + +m ∈ SN +n ∈ SN +------------------------ :: Case +case x | y.m | z.n ∈ SNe + +defn + v ∈ SN :: :: SNVal :: 'SN_' + {{ tex [[v]] \in \kw{SN} }} +by + +------ :: Var +x ∈ SN + +--------- :: Unit +unit ∈ SN + +v ∈ SN +---------- :: Inl +inl v ∈ SN + +v ∈ SN +---------- :: Inr +inr v ∈ SN + +m ∈ SN +------------ :: Thunk +thunk m ∈ SN + +% inversion + +force v ∈ SN +------------ :: Force_inv +v ∈ SN + +defn + m ∈ SN :: :: SNCom :: 'SN_' + {{ tex [[m]] \in \kw{SN} }} +by + +m ∈ SN +---------- :: Lam +λx. m ∈ SN + +v ∈ SN +---------- :: Ret +ret v ∈ SN + +m ∈ SNe +------- :: SNe +m ∈ SN + +m ⤳ n +n ∈ SN +------ :: Red +m ∈ SN + +% backward closure + +m ⤳* n +n ∈ SN +------- :: Reds +m ∈ SN + +% extensionality + +m x ∈ SN +-------- :: Ext +m ∈ SN + +% lifting + +G ⊧ s +G, x : A ⊧ m : B +---------------- :: Lift +m{⇑ s} ∈ SN + +defn + m ⤳ n :: :: SR :: 'SR_' + {{ tex [[m]] \leadsto [[n]] }} +by + +-------------------- :: Thunk +force (thunk m) ⤳ m + +v ∈ SN +--------------------- :: Lam +(λx. m) v ⤳ m{x ↦ v} + +v ∈ SN +--------------------------- :: Ret +let x (ret v) m ⤳ m{x ↦ v} + +v ∈ SN +n ∈ SN +------------------------------------ :: Inl +case (inl v) | y.m | z.n ⤳ m{y ↦ v} + +v ∈ SN +m ∈ SN +------------------------------------ :: Inr +case (inr v) | y.m | z.n ⤳ n{z ↦ v} + +m ⤳ n +---------- :: App +m v ⤳ n v + +m ⤳ m' +----------------------- :: Let +let x m n ⤳ let x m' n + +defn + m ⤳* n :: :: SRs :: 'SRs_' + {{ tex [[m]] \leadsto^* [[n]] }} +by + +------- :: Refl +m ⤳* m + +m ⤳ m' +m' ⤳* n +-------- :: Trans +m ⤳* n + +% admissible + +m ⤳ n +------- :: Once +m ⤳* n + +m ⤳* m' +m' ⤳* n +-------- :: Trans' +m ⤳* n + +% congruence rules + +m ⤳* n +----------- :: App +m v ⤳* n v + +m ⤳* m' +------------------------ :: Let +let x m n ⤳* let x m' n + +%% Logical relation and semantic typing %% + +defns +LR :: '' ::= + +defn + ⟦ A ⟧ ↘ P :: :: ValType :: 'LR_' + {{ tex \mathopen{\llbracket} [[A]] \mathclose{\rrbracket} \searrow [[P]] }} +by + +------------------------------------- :: Unit +⟦ Unit ⟧ ↘ { v | v ∈ SNe ∨ v = unit } + +⟦ A1 ⟧ ↘ P +⟦ A2 ⟧ ↘ Q +----------------------------------------------------------------------------------------------------------- :: Sum +⟦ A1 + A2 ⟧ ↘ { v | v ∈ SNe ∨ (# (∃w. (# v = inl w ∧ w ∈ P #)) ∨ (∃w. (# v = inr w ∧ w ∈ Q #)) #) } + +⟦ B ⟧ ↘ P +----------------------------- :: U +⟦ U B ⟧ ↘ { v | force v ∈ P } + +defn + ⟦ B ⟧ ↘ P :: :: ComType :: 'LR_' + {{ tex \mathopen{\llbracket} [[B]] \mathclose{\rrbracket} \searrow [[P]] }} +by + +⟦ A ⟧ ↘ P +--------------------------------------------------------------------------------- :: F +⟦ F A ⟧ ↘ { m | (∃n. (# m ⤳* n ∧ n ∈ SNe #)) ∨ (∃v. (# m ⤳* ret v ∧ v ∈ P #)) } + +⟦ A ⟧ ↘ P +⟦ B ⟧ ↘ Q +--------------------------------------------- :: Arr +⟦ A → B ⟧ ↘ { m | ∀v. (# v ∈ P ⇒ m v ∈ Q #) } + +defns +LRs :: '' ::= + +defn + v ∈ ⟦ A ⟧ :: :: ValTypes :: 'LR'_' + {{ tex [[v]] \in \mathopen{\llbracket} [[A]] \mathclose{\rrbracket} }} +by + +------------ :: Unit_var +x ∈ ⟦ Unit ⟧ + +--------------- :: Unit_unit +unit ∈ ⟦ Unit ⟧ + +--------------- :: Sum_var +x ∈ ⟦ A1 + A2 ⟧ + +v ∈ ⟦ A1 ⟧ +------------------- :: Sum_inl +inl v ∈ ⟦ A1 + A2 ⟧ + +v ∈ ⟦ A2 ⟧ +------------------- :: Sum_inr +inr v ∈ ⟦ A1 + A2 ⟧ + +force v ∈ ⟦ B ⟧ +--------------- :: Force +v ∈ ⟦ U B ⟧ + +defn + m ∈ ⟦ B ⟧ :: :: ComTypes :: 'LR'_' + {{ tex [[m]] \in \mathopen{\llbracket} [[B]] \mathclose{\rrbracket} }} +by + +m ⤳* n +n ∈ SNe +----------- :: F_var +m ∈ ⟦ F A ⟧ + +m ⤳* ret v +v ∈ ⟦ A ⟧ +----------- :: F_ret +m ∈ ⟦ F A ⟧ + +∀v. (# v ∈ ⟦ A ⟧ ⇒ m v ∈ ⟦ B ⟧ #) +--------------------------------- :: Arr +m ∈ ⟦ A → B ⟧ + +defns +Sem :: '' ::= + +defn + G ⊧ s :: :: SemCtxt :: 'S_' + {{ tex [[G]] \vDash [[s]] }} +by + +----- :: Nil +G ⊧ • + +G ⊧ s +⟦ A ⟧ ↘ P +v ∈ P +------------------- :: Cons +G, x : A ⊧ s, x ↦ v + +defn + G ⊧ v : A :: :: SemVal :: 'S_' + {{ tex [[G]] \vDash [[v]] : [[A]] }} +by + +x : A ∈ G +--------- :: Var +G ⊧ x : A + +--------------- :: Unit +G ⊧ unit : Unit + +G ⊧ v : A1 +------------------- :: Inl +G ⊧ inl v : A1 + A2 + +G ⊧ v : A2 +------------------- :: Inr +G ⊧ inr v : A1 + A2 + +G ⊧ m : B +----------------- :: Thunk +G ⊧ thunk m : U B + +defn + G ⊧ m : B :: :: SemCom :: 'S_' + {{ tex [[G]] \vDash [[m]] : [[B]] }} +by + +G ⊧ v : U B +--------------- :: Force +G ⊧ force v : B + +G, x : A ⊧ m : B +----------------- :: Arr +G ⊧ λx. m : A → B + +G ⊧ m : A → B +G ⊧ v : A +-------------- :: App +G ⊧ m v : B + +G ⊧ v : A +---------------- :: Ret +G ⊧ ret v : F A + +G ⊧ m : F A +G, x : A ⊧ n : B +----------------- :: Let +G ⊧ let x m n : B + +G ⊧ v : A1 + A2 +G, y : A1 ⊧ m : B +G, z : A2 ⊧ n : B +-------------------------- :: Case +G ⊧ case v | y.m | z.n : B + +%% Syntactic typing %% + +defns +Typing :: '' ::= + +defn + G ⊢ v : A :: :: ValWt :: 'T_' + {{ tex [[G]] \vdash [[v]] : [[A]] }} +by + +x : A ∈ G +--------- :: Var +G ⊢ x : A + +--------------- :: Unit +G ⊢ unit : Unit + +G ⊢ v : A1 +------------------- :: Inl +G ⊢ inl v : A1 + A2 + +G ⊢ v : A2 +------------------- :: Inr +G ⊢ inr v : A1 + A2 + +G ⊢ m : B +----------------- :: Thunk +G ⊢ thunk m : U B + +defn + G ⊢ m : B :: :: ComWt :: 'T_' + {{ tex [[G]] \vdash [[m]] : [[B]] }} +by + +G ⊢ v : U B +--------------- :: Force +G ⊢ force v : B + +G, x : A ⊢ m : B +----------------- :: Lam +G ⊢ λx. m : A → B + +G ⊢ m : A → B +G ⊢ v : A +-------------- :: App +G ⊢ m v : B + +G ⊢ v : A +---------------- :: Ret +G ⊢ ret v : F A + +G ⊢ m : F A +G, x : A ⊢ n : B +----------------- :: Let +G ⊢ let x m n : B + +G ⊢ v : A1 + A2 +G, y : A1 ⊢ m : B +G, z : A2 ⊢ n : B +-------------------------- :: Case +G ⊢ case v | y.m | z.n : B + +%% Reduction %% + +defns + Red :: '' ::= + +defn + v ⇝ w :: :: StepVal :: 'StepVal_' + {{ tex [[v]] \rightsquigarrow [[w]] }} +by + +defn + m ⇝ n :: :: StepCom :: 'StepCom_' + {{ tex [[m]] \rightsquigarrow [[n]] }} +by + +defn + v ⇝* w :: :: StepVals :: 'StepVals_' + {{ tex [[v]] \rightsquigarrow^* [[w]] }} +by + +defn + m ⇝* n :: :: StepComs :: 'StepComs_' + {{ tex [[m]] \rightsquigarrow^* [[n]] }} +by + +%% Accessibility definition of strong normalization %% + +defns + sn :: '' ::= + +defn + v ∈ sn :: :: snVal :: 'sn_' + {{ tex [[v]] \in \kw{sn} }} +by + +∀w. (# v ⇝ w ⇒ w ∈ sn #) +------------------------ :: Val +v ∈ sn + +% inversion + +force v ∈ sn +------------ :: Force_inv +v ∈ sn + +m v ∈ sn +-------- :: App_inv2 +v ∈ sn + +% congruence + +------ :: Var +x ∈ sn + +--------- :: Unit +unit ∈ sn + +v ∈ sn +---------- :: Inl +inl v ∈ sn + +v ∈ sn +---------- :: Inr +inr v ∈ sn + +m ∈ sn +------------ :: Thunk +thunk m ∈ sn + +defn + m ∈ sn :: :: snCom :: 'sn_' + {{ tex [[m]] \in \kw{sn} }} +by + +∀n. (# m ⇝ n ⇒ n ∈ sn #) +------------------------ :: Com +m ∈ sn + +% inversion + +m v ∈ sn +-------- :: App_inv1 +m ∈ sn + +let x m n ∈ sn +-------------- :: Let_inv1 +m ∈ sn + +let x m n ∈ sn +-------------- :: Let_inv2 +n ∈ sn + +% antisubstitution + +m{x ↦ v} ∈ sn +v ∈ sn +------------- :: antisubst +m ∈ sn + +% expansion + +m ∈ sn +-------------------- :: Force_Thunk +force (thunk m) ∈ sn + +v ∈ sn +m{x ↦ v} ∈ sn +-------------- :: App_Lam +(λx. m) v ∈ sn + +v ∈ sn +m{x ↦ v} ∈ sn +-------------------- :: Let_Ret +let x (ret v) m ∈ sn + +v ∈ sn +m{y ↦ v} ∈ sn +n ∈ sn +----------------------------- :: Case_Inl +case (inl v) | y.m | z.n ∈ sn + +v ∈ sn +m ∈ sn +n{z ↦ v} ∈ sn +----------------------------- :: Case_Inr +case (inr v) | y.m | z.n ∈ sn + +% closure + +m ⤳' n +v ∈ sn +n v ∈ sn +-------- :: App_bwd +m v ∈ sn + +m ⤳' m' +n ∈ sn +let x m' n ∈ sn +--------------- :: Let_bwd +let x m n ∈ sn + +m ⤳' n +n ∈ sn +------- :: closure +m ∈ sn + +% congruence + +v ∈ sn +------------ :: Force +force v ∈ sn + +m ∈ sn +---------- :: Lam +λx. m ∈ sn + +v ∈ sn +---------- :: Ret +ret v ∈ sn + +m ∈ sne +v ∈ sn +-------- :: App +m v ∈ sn + +m ∈ sne +n ∈ sn +-------------- :: Let +let x m n ∈ sn + +v ∈ sne +m ∈ sn +n ∈ sn +----------------------- :: Case +case v | y.m | z.n ∈ sn + +defn + m ⤳' n :: :: sr :: 'sr_' + {{ tex [[m]] \leadsto_{ \kw{sn} } [[n]] }} +by + +--------------------- :: Thunk +force (thunk m) ⤳' m + +v ∈ sn +---------------------- :: Lam +(λx. m) v ⤳' m{x ↦ v} + +v ∈ sn +---------------------------- :: Ret +let x (ret v) m ⤳' m{x ↦ v} + +v ∈ sn +n ∈ sn +------------------------------------- :: Inl +case (inl v) | y.m | z.n ⤳' m{y ↦ v} + +v ∈ sn +m ∈ sn +------------------------------------- :: Inr +case (inr v) | y.m | z.n ⤳' n{z ↦ v} + +m ⤳' n +----------- :: App +m v ⤳' n v + +m ⤳' m' +------------------------ :: Let +let x m n ⤳' let x m' n + +defn + v ∈ ne :: :: neVal :: 'ne_' + {{ tex [[v]] \in \kw{ne} }} +by + +------ :: Var +x ∈ ne + +% preservation + +v ⇝ w +v ∈ ne +------ :: StepVal +w ∈ ne + +defn + m ∈ ne :: :: neCom :: 'ne_' + {{ tex [[m]] \in \kw{ne} }} +by + +------------ :: Force +force x ∈ ne + +m ∈ ne +-------- :: App +m v ∈ ne + +m ∈ ne +-------------- :: Let +let x m n ∈ ne + +------------------ :: Case +case x | y.m | z.n ∈ ne + +% preservation + +m ⇝ n +n ∈ ne +------ :: StepCom +m ∈ ne + +% embedding + +m ∈ SNe +------- :: SNe +m ∈ ne + +defn + v ∈ sne :: :: sneVal :: 'sneval_' + {{ tex [[v]] \in \kw{sne} }} +by + +------- :: sne +x ∈ sne + +defn + m ∈ sne :: :: sneCom :: 'snecom_' + {{ tex [[m]] \in \kw{sne} }} +by + +m ∈ ne +m ∈ sn +------- :: sne +m ∈ sne diff --git a/cbpv.pdf b/cbpv.pdf new file mode 100644 index 0000000..16b0dcc --- /dev/null +++ b/cbpv.pdf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:78c4c356efb79eec148c56f072fe085288f4b09595c706789818f1bd09439a42 +size 262187 diff --git a/cbpv.tex b/cbpv.tex new file mode 100644 index 0000000..76fa25b --- /dev/null +++ b/cbpv.tex @@ -0,0 +1,650 @@ +\documentclass{article} + +\usepackage[supertabular]{ottalt} +\let\newlist\relax +\let\renewlist\relax +\usepackage[T1]{fontenc} +\usepackage{mlmodern} +\usepackage[margin=1in]{geometry} +\usepackage{enumitem,float,booktabs,xspace,doi} +\usepackage{amsmath,amsthm,amssymb} +\usepackage[capitalize,nameinlink]{cleveref} +\usepackage{mathpartir,mathtools,stmaryrd} + +\setlist{nosep} +\hypersetup{ + colorlinks=true, + urlcolor=blue, + linkcolor=magenta, + citecolor=teal +} +\urlstyle{tt} + +\newtheorem{theorem}{Theorem} +\newtheorem{lemma}[theorem]{Lemma} +\newtheorem{corollary}[theorem]{Corollary} +\theoremstyle{definition} +\newtheorem{definition}{Definition} + +\newcommand{\ie}{\textit{i.e.}\@\xspace} +\newcommand{\ala}{\textit{\`a la}\@\xspace} +\newcommand{\apriori}{\textit{a priori}\@\xspace} +\newcommand{\aposteriori}{\textit{a posteriori}\@\xspace} + +\title{Strong Normalization for \\ Simply Typed Call-by-Push-Value} +\author{Jonathan Chan} +\date{} + +\inputott{rules} + +\begin{document} +\maketitle + +\section{Introduction} + +The goal of this project is to mechanize a proof of strong normalization for call-by-push-value (CBPV). +It follows work by Forster, Sch\"afer, Spies, and Stark (TODO: cite) on mechanizing the metatheory of CBPV in Rocq, +but instead adapts the proof technique from POPLMark Reloaded (TODO: cite). + +Both proofs, and mine, follow the same sequence of steps: +we define a logical relation that semantically interpret types as sets of terms, +show that these sets are backward closed by reduction and that they contain only strongly normalizing terms, +prove a fundamental soundness theorem that places well typed terms in the semantic interpretations of their types, +and conclude that well typed terms must be strongly normalizing. +The difference lies in \emph{how strong normalization} (and reduction) is defined. +The Rocq mechanization uses a traditional definition of strong normalization as an accessibility relation, +while POPLMark Reloaded and this project use an inductive characterization of strong normalization, +then prove it sound with respect to the traditional definition. + +In contrast to both prior works, which use Rocq, Agda, or Beluga, +this project is mechanized in Lean. +A secondary purpose of this project is to assess the capabilities of Lean for PL metatheory, +especially when making heavy use of mutually defined inductive types. +I have implemented a mutual induction tactic for Lean (TODO: link), +and the mutual values and computations of CBPV, +combined with the even more complex mutual inductives from POPLMark Reloaded, +make it an attractive test case to test the tactic's robustness. + +This report is divided in roughly the same shape as the proof development. +\Cref{sec:syntax} introduces the syntax and the typing rules for CBPV (\texttt{Syntax.lean}, \texttt{Typing.lean}). +Then the inductive characterization of strong normalization is defined in \cref{sec:sn-ind} (\texttt{NormalInd.lean}), +followed by the logical relation in \cref{sec:lr} (\texttt{OpenSemantics.lean}). +The central theorem of strong normalization is proven in \cref{sec:soundness} +as a corollary of the fundamental theorem for the logical relation (\texttt{Soundness.lean}, \texttt{Normalization.lean}). +To ensure that the inductive characterization is correct, +\cref{sec:sn-acc} shows that it implies the traditional definition of strong normalization (\texttt{NormalAcc.lean}). +This latter definition and proof depends on small-step reduction on open terms, +whose properties are omitted here (\texttt{Reduction.lean}). +In general, I gloss over details about substitution and reduction, +since I'm interested in presenting the structure of the strong normalization proof +and not the minutiae of syntax and binding. +Finally, I discuss the merits of this proof technique +and the challenges posed by using Lean in \cref{sec:discussion}. + +\section{Syntax and Typing} \label{sec:syntax} + +\begin{align*} + \ottnt{A} &\Coloneqq \kw{Unit} \mid \ottnt{A_{{\mathrm{1}}}} + \ottnt{A_{{\mathrm{2}}}} \mid \kw{U} \gap \ottnt{B} & \textit{value types} \\ + \ottnt{B} &\Coloneqq \ottnt{A} \rightarrow \ottnt{B} \mid \kw{F} \gap \ottnt{A} & \textit{computation types} \\ + \ottnt{v}, \ottnt{w} &\Coloneqq \ottmv{x} \mid \kw{unit} \mid \kw{inl} \gap \ottnt{v} \mid \kw{inr} \gap \ottnt{v} \mid \kw{thunk} \gap \ottnt{m} & \textit{values} \\ + \ottnt{m}, \ottnt{n} &\Coloneqq \kw{force} \gap \ottnt{v} \mid \lambda \ottmv{x} \mathpunct{.} \ottnt{m} \mid \ottnt{m} \gap \ottnt{v} \mid \kw{return} \gap \ottnt{v} & \textit{computations} \\ + & \mid \kw{let} \gap \ottmv{x} \leftarrow \ottnt{m} \gap \kw{in} \gap \ottnt{n} \\ + & \mid \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 \\ + \Gamma &\Coloneqq \cdot \mid \Gamma , \ottmv{x} \mathbin{:} \ottnt{A} & \textit{typing contexts} \\ + \sigma &\Coloneqq \cdot \mid \sigma , \ottmv{x} \mapsto \ottnt{v} & \textit{simultaneous substitutions} +\end{align*} + +The grammar of the CBPV for this project is given above. +Terms and their types are divided between \emph{values} and \emph{computations}. +Values are variables, unit, injections into a sum type, or a thunked computation, +while computations are forcing thunks, +functions, applications, returning values, binding returned values, +and case analysis on sums. +There are only value variables and no computation variables, +since they represent terms that require no more work to be done on them ready to be substituted in, +and typing contexts similarly only contain value types. +I use $t$ to refer to terms that may be either values or computations. + +Although the syntax is presented nominally, +the mechanization uses an unscoped de Bruijn indexed representation of variables, +along with simultaneous substitutions $\sigma$ mapping variables to values, +with $ \cdot $ as the identity substitution. +Applying a substitution is represented as $ \ottnt{v} [ \sigma ] $ and $ \ottnt{m} [ \sigma ] $, +and implemented in terms of renamings, +which are mappings from variables to other variables. + +This is not the usual complete CBPV language, +since it's missing both value tuples and computation tuples. +I exclude them because they are syntactically not much more interesting than returns, +whose eliminator is shaped like pattern matching on a singleton value tuple, +and than thunks, +whose eliminator is shaped like projection on a singleton computation tuple. +In contrast, I do include sums, which represent the only way a computation can branch. + +The typing rules below are standard for the values and computations included. +The judgements for values and computations are defined mutually, +just as are the types and the terms. + +\drules[T]{$ \Gamma \vdash \ottnt{v} : \ottnt{A} $}{value typing}{Var,Unit,Inl,Inr,Thunk} +\drules[T]{$ \Gamma \vdash \ottnt{m} : \ottnt{B} $}{computation typing}{Force,Lam,App,Ret,Let,Case} + +\section{Strong Normalization as an Inductive Definition} \label{sec:sn-ind} + +The idea behind the inductive characterization of strong normalization +is to describe case by case when a term is strongly normal, +rather than showing \aposteriori which terms are strongly normal. +This is done in conjunction with defining strongly neutral terms, +which are blocked from $\beta$-reduction, +and strong head reduction, +which expands the set from normal forms +to terms which must reduce to normal forms. + +The general recipe for defining these for CBPV is as follows: +\begin{itemize}[rightmargin=\leftmargin] + \item The only strongly neutral values are variables. + \item Strongly neutral computations are eliminators + whose head positions are strongly neutral, + while all other subterms are strongly normal. + \item Strongly normal values are constructors + whose subterms are strongly normal, + or strongly neutral values, \ie variables. + \item Strongly normal computations are constructors + whose subterms are strongly normal, + or strongly neutral computations, + or computations which reduce to strongly normal computations + (backward closure). + \item Strong head reduction consists of $\beta$ reductions + for all eliminators around the corresponding constructors, + and congruent reductions in head positions. +\end{itemize} + +Additionally, strong reduction requires premises asserting that +the subterms that may ``disappear'' after reduction be strongly normal +so that backward closure actually closes over strongly normal terms. +These subterms are the values that get substituted into a computation, +which may disappear if the computation never actually uses the binding, +as well as computation branches not taken. + +Because we're dealing with CBPV, values have no $\beta$ reductions, +so there's no need for head reduction of values as there are no heads. +Furthermore, there is only one strongly neutral value, +so we inline the definition as a variable where needed, +but also write it as $ \ottnt{v} \in \kw{SNe} $ for symmetry as appropriate. +Otherwise, the remaining four judgements are defined mutually below. + +\drules[SNe]{$ \ottnt{m} \in \kw{SNe} $}{strongly neutral computations}{Force,App,Let,Case} +\drules[SN]{$ \ottnt{v} \in \kw{SN} $}{strongly normal values}{Var,Unit,Inl,Inr,Thunk} +\drules[SN]{$ \ottnt{m} \in \kw{SN} $}{strongly normal computations}{Lam,Ret,SNe,Red} +\drules[SR]{$ \ottnt{m} \leadsto \ottnt{n} $}{strong head reduction}{Thunk,Lam,Ret,Inl,Inr,App,Let} +\drules[SRs]{$ \ottnt{m} \leadsto^* \ottnt{n} $}{reflexive, transitive closure of head reduction}{Refl,Trans} + +We also need the reflexive, transitive closure of head reduction, +defined as a separate inductive above. +Now we show a few simple lemmas about it, +along with an inversion lemma for forcing +(other inversion lemmas hold, but this is the only one we need). +I present them below as judgement pseudorules +using a dashed line to indicate that they are admissible rules. +These are all proven either by construction +or by induction on the first premise. + +\begin{mathpar} +\mprset{fraction={-~}{-~}{-}} +\drule[]{SRs-Once} +\drule[]{SRs-TransPP} +\drule[]{SRs-App} +\drule[]{SRs-Let} +\drule[]{SN-Reds} +\drule[]{SN-Force-inv} +\end{mathpar} + +The most important property of strongly normal terms that we need is antirenaming, +which states that undoing a renaming does not change the term's +normalization or reduction behaviour. +A crucial property that follows is extensionality of applications, +which is an inversion lemma specifically when the application argument is a variable. + +\begin{lemma}[Antirenaming] \label{thm:antisubst} + Let $\sigma$ be a renaming, + \ie a substitution mapping variables to variables. + Then the following hold: + \begin{enumerate} + \item If $ \ottnt{m} [ \sigma ] \in \kw{SNe} $ then $ \ottnt{m} \in \kw{SNe} $. + \item If $ \ottnt{v} [ \sigma ] \in \kw{SN} $ then $ \ottnt{v} \in \kw{SN} $. + \item If $ \ottnt{m} [ \sigma ] \in \kw{SN} $ then $ \ottnt{m} \in \kw{SN} $. + \item If $ \ottnt{m} [ \sigma ] \leadsto \ottnt{n} $ then there exists some $\ottnt{n'}$ + such that $\ottnt{n} = \ottnt{n'} [ \sigma ] $ and $ \ottnt{m} \leadsto \ottnt{n'} $. + \end{enumerate} +\end{lemma} + +\begin{proof} + By mutual induction on the four derivations of + $ \ottnt{m} [ \sigma ] \in \kw{SNe} $, $ \ottnt{v} [ \sigma ] \in \kw{SN} $, $ \ottnt{m} [ \sigma ] \in \kw{SN} $, and $ \ottnt{m} [ \sigma ] \leadsto \ottnt{n} $. +\end{proof} + +\begin{corollary}[Extensionality] \label{cor:ext} + If $ \ottnt{m} \gap \ottmv{x} \in \kw{SN} $ then $ \ottnt{m} \in \kw{SN} $. +\end{corollary} + +\begin{proof} + By induction on the derivation of strongly normal values. + The possible cases are \rref*{SN-SNe,SN-Red}. + Destructing the premise of the former gives $ \ottnt{m} \in \kw{SNe} $, + and we conclude using \rref{SN-SNe} again. + In the latter case, we have $ \ottnt{m} \gap \ottmv{x} \leadsto \ottnt{n} $ and $ \ottnt{n} \in \kw{SN} $; + destructing on the reduction yields the possible cases + \rref{SR-Lam,SR-App}. + In the first case, we have $ \ottnt{m} [ \ottmv{x} \mapsto \ottnt{v} ] \in \kw{SN} $, + so the goal holds by \nameref{thm:antisubst}. + In the second case, we have $ \ottnt{m} \leadsto \ottnt{n} $ and $ \ottnt{n} \gap \ottmv{x} \in \kw{SN} $, + so by the induction hypothesis, we have $ \ottnt{n} \in \kw{SN} $, + and we conclude using \rref{SN-Red}. +\end{proof} + +\section{Logical Relation on Open Terms} \label{sec:lr} + +The next step is to define a logical relation that semantically interprets types +as sets of open terms. +The key property we need from these sets is that they contain only strongly normal terms. +Because we are working with open terms to prove normalization +and not just termination of evaluation of closed terms, +we need to consider variables and strongly neutral terms. +Having no other information about them other than their strong neutrality, +we require that the interpretation sets always contain all strongly neutral terms. + +The logical relation on simple types can be defined by induction on the structure of the type. +However, I want to maximize the amount of mutual inductives used in this project, +so we instead define the logical relation as an inductive binary relation +between the type and the set of terms of its interpretation, +denoted as $ \mathopen{\llbracket} \ottnt{A} \mathclose{\rrbracket} \searrow \ottnt{P} $ and $ \mathopen{\llbracket} \ottnt{B} \mathclose{\rrbracket} \searrow \ottnt{P} $ below. +I use set builder notation to define the sets and set membership, +but they are implemented in the mechanization as functions +that take terms and return propositions and as function applications. +Here, the conjunctions ($\wedge$), disjunctions ($\vee$), equalities ($=$), implications ($\Rightarrow$), +and universal ($\forall$) and existential ($\exists$) quantifiers +are part of the metatheory, not part of the object language. + +\drules[LR]{$ \mathopen{\llbracket} \ottnt{A} \mathclose{\rrbracket} \searrow \ottnt{P} $}{semantic interpretation of value types}{Unit,U,Sum} +\drules[LR]{$ \mathopen{\llbracket} \ottnt{B} \mathclose{\rrbracket} \searrow \ottnt{P} $}{semantic interpretation of computation types}{F,Arr} + +The terms in the interpretation of a type can be characterized in two different ways: +by what constructor of that type they reduce to, +or by how they act when eliminated by an eliminator for that type. +For the former, we need to explicitly include the possibility of the term being strongly neutral. +I chose the following characterizations because they seemed the simplest to me, +but the alternate choices likely work as well. + +\begin{itemize}[noitemsep,rightmargin=\leftmargin] + \item Values in the interpretation of the unit type + are either variables or the unit value. + \item Values are in the interpretation of the $ \kw{U} \gap \ottnt{B} $ type + if they can be forced to computations in the interpretation of the $\ottnt{B}$ type. + \item Values in the interpretation of the sum type $ \ottnt{A_{{\mathrm{1}}}} + \ottnt{A_{{\mathrm{2}}}} $ are either variables, + left injections whose values are in the interpretation of $\ottnt{A_{{\mathrm{1}}}}$, + or right injections whose values are in that of $\ottnt{A_{{\mathrm{2}}}}$. + \item Computations in the interpretation of the $ \kw{F} \gap \ottnt{A} $ type + reduce to either a neutral computation + or a return whose value is in the interpretation of $\ottnt{A}$. + \item Computations are in the interpretation of the function type $ \ottnt{A} \rightarrow \ottnt{B} $ + if applying them to values in the interpretation of $\ottnt{A}$ + yields computations in the interpretation of $\ottnt{B}$. +\end{itemize} + +By this description, it sounds like the logical relation can be presented +directly as a relation between a type and a term; +this presentation is given in \cref{fig:lr-alt}. +Unfortunately, this is not well defined, +since the logical relation appears in a negative position +(to the left of an implication) in the premise of \rref{LRPP-Arr}. +The alternate presentation can be interpreted as a function +match on the term and the type and returning the conjunction of its premises, +but I wanted to use a mutually defined inductive definition. + +\begin{figure}[H] +\fbox{$ \ottnt{v} \in \mathopen{\llbracket} \ottnt{A} \mathclose{\rrbracket} $} \quad \fbox{$ \ottnt{m} \in \mathopen{\llbracket} \ottnt{B} \mathclose{\rrbracket} $} \hfill \textit{} \\ +\begin{mathpar} +\drule[]{LRPP-Unit-var} +\drule[]{LRPP-Unit-unit} +\drule[]{LRPP-Sum-var} +\drule[]{LRPP-Sum-inl} +\drule[]{LRPP-Sum-inr} +\drule[]{LRPP-Force} +\drule[]{LRPP-F-var} +\drule[]{LRPP-F-ret} +\drule[]{LRPP-Arr} +\end{mathpar} +\caption{Alternate presentation of the logical relation} +\label{fig:lr-alt} +\end{figure} + +Using the inductive presentation of the logical relation, +there are three easy properties to show: +interpretability, which states that all types have an interpretation; +determinism, which states that the interpretation indeed behaves like a function +from types to sets of terms; +and backward closure, which states that the interpretations of computation types +are backward closed under multi-step head reduction. +The last property is why \rref{LRPP-F-var} needs to include +computations that \emph{reduce to} strongly neutral terms or returns, +not merely ones that are such terms. + +\begin{lemma}[Interpretability] \label{lem:interp} \leavevmode + \begin{enumerate} + \item Given $\ottnt{A}$, there exists $\ottnt{P}$ such that $ \mathopen{\llbracket} \ottnt{A} \mathclose{\rrbracket} \searrow \ottnt{P} $. + \item Given $\ottnt{B}$, there exists $\ottnt{P}$ such that $ \mathopen{\llbracket} \ottnt{B} \mathclose{\rrbracket} \searrow \ottnt{P} $. + \end{enumerate} +\end{lemma} + +\begin{proof} + By mutual induction on the types $\ottnt{A}$ and $\ottnt{B}$. +\end{proof} + +\begin{lemma}[Determinism] \label{lem:det} \leavevmode + \begin{enumerate} + \item If $ \mathopen{\llbracket} \ottnt{A} \mathclose{\rrbracket} \searrow \ottnt{P} $ and $ \mathopen{\llbracket} \ottnt{A} \mathclose{\rrbracket} \searrow \ottnt{Q} $ then $\ottnt{P} = \ottnt{Q}$. + \item If $ \mathopen{\llbracket} \ottnt{B} \mathclose{\rrbracket} \searrow \ottnt{P} $ and $ \mathopen{\llbracket} \ottnt{B} \mathclose{\rrbracket} \searrow \ottnt{Q} $ then $\ottnt{P} = \ottnt{Q}$. + \end{enumerate} +\end{lemma} + +\begin{proof} + By mutual induction on the first derivations of the logical relation, + then by cases on the second derivations. +\end{proof} + +\begin{lemma}[Backward closure] \label{lem:closure} + Given $ \mathopen{\llbracket} \ottnt{B} \mathclose{\rrbracket} \searrow \ottnt{P} $ and $ \ottnt{m} \leadsto^* \ottnt{n} $, + if $ \ottnt{n} \in \ottnt{P} $ then $ \ottnt{m} \in \ottnt{P} $. +\end{lemma} + +\begin{proof} + By induction on the derivation of the logical relation. +\end{proof} + +The final key property is adequacy, +which states that the interpretations of types +must contain all strongly neutral terms +and must contain only strongly normal terms. +Such sets are said to be \emph{reducibility candidates}. + +\begin{definition}[Reducibility candidates] + A reducibility candidate is a set of terms $\ottnt{P}$ where, + given a term $t$, + if $ t \in \kw{SNe} $ then $ t \in \ottnt{P} $, and + if $ t \in \ottnt{P} $ then $ t \in \kw{SN} $. +\end{definition} + +\begin{lemma}[Adequacy] \label{lem:adequacy} \leavevmode + \begin{enumerate} + \item If $ \mathopen{\llbracket} \ottnt{A} \mathclose{\rrbracket} \searrow \ottnt{P} $ then $\ottnt{P}$ is a reducibility candidate. + \item If $ \mathopen{\llbracket} \ottnt{B} \mathclose{\rrbracket} \searrow \ottnt{P} $ then $\ottnt{P}$ is a reducibility candidate. + \end{enumerate} +\end{lemma} + +\begin{proof} + By mutual induction on the derivations of the logical relation. + \Rref{SN-Force-inv} is used in the \rref*{S-U} case, + while \rref{SN-Reds} is used in the \rref{S-F} case. + In the \rref*{S-Arr} case on $ \ottnt{A} \rightarrow \ottnt{B} $, + where $ \mathopen{\llbracket} \ottnt{A} \mathclose{\rrbracket} \searrow \ottnt{P} $ and $ \mathopen{\llbracket} \ottnt{B} \mathclose{\rrbracket} \searrow \ottnt{Q} $, + to show the second part of its interpretation being a reducibility candidate, + we are given $\ottnt{m}$ such that for every $ \ottnt{v} \in \ottnt{P} $, $ \ottnt{m} \gap \ottnt{v} \in \ottnt{Q} $, + and the goal is to show that $ \ottnt{m} \in \kw{SN} $. + By the induction hypotheses, picking an arbitrary variable $\ottmv{x}$, + we have that $ \ottmv{x} \in \ottnt{P} $ (since it is neutral) and that $ \ottnt{m} \gap \ottmv{x} \in \kw{SN} $. + Then the goal holds by \nameref{cor:ext}. +\end{proof} + +\section{Semantic Typing and the Fundamental Theorem} \label{sec:soundness} + +Now that we know that the interpretations contain only strongly normal terms, +our goal is to show that well typed terms inhabit the interpretations of their types. +We first define what it means for a substitution to be +semantically well formed with respect to a context. + +\begin{definition}[Semantic well-formedness of substitutions] + A substitution $\sigma$ is well formed with respect to a context $\Gamma$, + written $ \Gamma \vDash \sigma $, if for every $ \ottmv{x} : \ottnt{A} \in \Gamma $ and $ \mathopen{\llbracket} \ottnt{A} \mathclose{\rrbracket} \searrow \ottnt{P} $, + we have $ \ottmv{x} [ \sigma ] \in \ottnt{P} $. + In short, the substitution maps variables in the context + to values in the interpretations of their types. +\end{definition} + +These judgements can be built up inductively, +as demonstrated by the below admissible rules, +which are proven by cases. + +{\mprset{fraction={-~}{-~}{-}} +\drules[S]{$ \Gamma \vDash \sigma $}{admissible semantic substitution well-formedness}{Nil,Cons} +} + +Then we can define semantic typing in terms of the logical relation, +using semantic well formedness of substitutions to handle the context. + +\begin{definition}[Semantic typing] + \begin{enumerate}[rightmargin=\leftmargin] \leavevmode + \item $\ottnt{v}$ semantically has type $\ottnt{A}$ under context $\Gamma$, + written $ \Gamma \vDash \ottnt{v} : \ottnt{A} $, if for every $\sigma$ such that $ \Gamma \vDash \sigma $, + there exists an interpretation $ \mathopen{\llbracket} \ottnt{A} \mathclose{\rrbracket} \searrow \ottnt{P} $ such that $ \ottnt{v} [ \sigma ] \in \ottnt{P} $. + \item $\ottnt{m}$ semantically has type $\ottnt{B}$ under context $\Gamma$, + written $ \Gamma \vDash \ottnt{m} : \ottnt{B} $, if for every $\sigma$ such that $ \Gamma \vDash \sigma $, + there exists an interpretation $ \mathopen{\llbracket} \ottnt{B} \mathclose{\rrbracket} \searrow \ottnt{P} $ such that $ \ottnt{m} [ \sigma ] \in \ottnt{P} $. + \end{enumerate} +\end{definition} + +Semantic typing follows exactly the same shape of rules as syntactic typing, +so I present them here as admissible rules. +All the hard work happens in these lemmas; +the fundamental theorem of soundness of syntactic typing with respect to semantic typing +then follows directly. +Normalization holds as an easy corollary. + +{\mprset{fraction={-~}{-~}{-}} +\drules[S]{$ \Gamma \vDash \ottnt{v} : \ottnt{A} $}{admissible semantic value typing}{Var,Unit,Inl,Inr,Thunk} +\drules[S]{$ \Gamma \vDash \ottnt{m} : \ottnt{B} $}{admissible semantic computation typing}{Force,Arr,App,Ret,Let,Case} +} + +\begin{proof} + By construction using prior lemmas, + in particular \rref{SRs-Let} in case \rref*{S-Let}; + \nameref{lem:interp} in cases \rref*{S-Var,S-Inl,S-Inr,S-Lam}; + \nameref{lem:det} in cases \rref*{S-Lam,S-App}; + \nameref{lem:closure} in cases \rref*{S-Thunk,S-Lam,S-Let,S-Case}; and + \nameref{lem:adequacy} in cases \rref*{S-Lam,S-Let,S-Case}. +\end{proof} + +\begin{theorem}[Soundness] \label{thm:soundness} \leavevmode + \begin{enumerate} + \item If $ \Gamma \vdash \ottnt{v} : \ottnt{A} $ then $ \Gamma \vDash \ottnt{v} : \ottnt{A} $. + \item If $ \Gamma \vdash \ottnt{m} : \ottnt{B} $ then $ \Gamma \vDash \ottnt{m} : \ottnt{B} $. + \end{enumerate} +\end{theorem} + +\begin{proof} + By mutual induction on the syntactic typing derivations, + using the admissible semantic typing rules. +\end{proof} + +\begin{corollary}[Normalization] \leavevmode + \begin{enumerate} + \item If $ \Gamma \vdash \ottnt{v} : \ottnt{A} $ then $ \ottnt{v} \in \kw{SN} $. + \item If $ \Gamma \vdash \ottnt{m} : \ottnt{B} $ then $ \ottnt{m} \in \kw{SN} $. + \end{enumerate} +\end{corollary} + +\begin{proof} + By \nameref{thm:soundness}, + using the identity substitution and \rref{S-Nil}, + the well typed terms inhabit the semantic interpretations of their types. + Then by \nameref{lem:adequacy}, + they are also strongly normalizing. +\end{proof} + +\section{Strong Normalization as an Accessibility Relation} \label{sec:sn-acc} + +\drules[sn]{$ \ottnt{v} \in \kw{sn} , \ottnt{m} \in \kw{sn} $}{strongly normalizing terms}{Val,Com} +\drules[sr]{$ \ottnt{m} \leadsto_{ \kw{sn} } \ottnt{n} $}{strong head reduction}{Thunk,Lam,Ret,Inl,Inr,App,Let} +\drules[ne]{$ \ottnt{m} \in \kw{ne} $}{neutral computations}{Force,App,Let,Case} + +\begin{mathpar} +\mprset{fraction={-~}{-~}{-}} +\drule[]{sn-App-invOne} +\drule[]{sn-App-invTwo} +\drule[]{sn-Let-invOne} +\drule[]{sn-Let-invTwo} +\end{mathpar} + +\begin{proof} + By induction on the premises of strongly normal terms, + using congruence of single-step reduction. +\end{proof} + +\begin{definition}[Neutral values] + A value is neutral, written $ \ottnt{v} \in \kw{ne} $, if it is a variable. +\end{definition} + +\begin{lemma}[Preservation] \label{lem:preservation} \leavevmode + \begin{enumerate} + \item If $ \ottnt{v} \rightsquigarrow \ottnt{w} $ and $ \ottnt{v} \in \kw{ne} $ then $ \ottnt{w} \in \kw{ne} $. + \item If $ \ottnt{m} \rightsquigarrow \ottnt{n} $ and $ \ottnt{m} \in \kw{ne} $ then $ \ottnt{n} \in \kw{ne} $. + \end{enumerate} +\end{lemma} + +\begin{proof} + By mutual induction on the single-step reductions. +\end{proof} + +\begin{definition}[Strongly neutral computations] + A strongly neutral computation, written $ \ottnt{m} \in \kw{sne} $, + is a computation that is both neutral and strongly normalizing, + \ie $ \ottnt{m} \in \kw{ne} $ and $ \ottnt{m} \in \kw{sn} $. +\end{definition} + +{\mprset{fraction={-~}{-~}{-}} +\drules[sn]{$ \ottnt{v} \in \kw{sn} $}{admissible strongly normal values}{Var,Unit,Inl,Inr,Thunk} +\drules[sn]{$ \ottnt{m} \in \kw{sn} $}{admissible strongly normal computations}{Lam,Ret,Force,App,Let,Case} +} + +\begin{proof} + \Rref{sn-App,sn-Let,sn-Case} are proven by double induction + on the two derivations of strongly normal terms. + Intuitively, we want to show that if the conclusion steps, + then it steps to a strongly normal term, + knowing by the induction hypotheses that if their subterms reduce, + then they also reduce to strongly normal terms. + Neutrality of the term in head position eliminates cases where the conclusion $\beta$-reduces, + leaving only the congruent reductions. + Because single-step reduction only steps in one subterm, + we only need the induction hypothesis for that reducing subterm, + so the double induction is really a lexicographic induction on the two derivations. + We additionally require \nameref{lem:preservation} to carry along neutrality + when the heads reduce in cases \rref*{sn-App,sn-Let}. + All other cases are direct by construction + or by induction on their sole premise. +\end{proof} + +% admissible rules missing backward closure \rref{SN-Red} + +\begin{lemma}[Antisubstitution (\textsf{sn})] \label{lem:antisubst-sn} + If $ \ottnt{m} [ \ottmv{x} \mapsto \ottnt{v} ] \in \kw{sn} $ and $ \ottnt{v} \in \kw{sn} $ then $ \ottnt{m} \in \kw{sn} $. +\end{lemma} + +\begin{proof} + By induction on the derivation of $ \ottnt{m} [ \ottmv{x} \mapsto \ottnt{v} ] \in \kw{sn} $. +\end{proof} + +{\mprset{fraction={-~}{-~}{-}} +\drules[sn]{$ \ottnt{m} \in \kw{sn} $}{head expansion}{Force-Thunk,App-Lam,Let-Ret,Case-Inl,Case-Inr} +} + +\begin{proof} + \Rref{sn-Force-Thunk} holds directly by induction on the premise; + the remaining proofs are more complex. + First, given the premise $ \ottnt{m} [ \ottmv{x} \mapsto \ottnt{v} ] \in \kw{sn} $ (or $ \ottnt{n} [ \ottmv{z} \mapsto \ottnt{v} ] $), + use \nameref{lem:antisubst-sn} to obtain $ \ottnt{m} \in \kw{sn} $. + Then proceed by double (or triple) induction on the derivations of + $ \ottnt{v} \in \kw{sn} $ and $ \ottnt{m} \in \kw{sn} $ (and $ \ottnt{n} \in \kw{sn} $ for the case rules). + Similarly to the admissible strongly normal rules, + these are lexicographic inductions, + except $ \ottnt{m} [ \ottmv{x} \mapsto \ottnt{v} ] \in \kw{sn} $ (or $ \ottnt{n} [ \ottmv{z} \mapsto \ottnt{v} ] $) + is used to satisfy the $\beta$-reduction cases. +\end{proof} + +\begin{lemma}[Confluence] \label{lem:confluence} + If $ \ottnt{m} \rightsquigarrow \ottnt{n_{{\mathrm{1}}}} $ and $ \ottnt{m} \leadsto_{ \kw{sn} } \ottnt{n_{{\mathrm{2}}}} $, then either $\ottnt{n_{{\mathrm{1}}}} = \ottnt{n_{{\mathrm{2}}}}$, + or there exists some $\ottnt{m'}$ such that + $ \ottnt{n_{{\mathrm{1}}}} \leadsto_{ \kw{sn} } \ottnt{m'} $ and $ \ottnt{n_{{\mathrm{2}}}} \rightsquigarrow \ottnt{m'} $. +\end{lemma} + +\begin{proof} + By induction on the derivation of $ \ottnt{m} \leadsto_{ \kw{sn} } \ottnt{n_{{\mathrm{2}}}} $, + then by cases on the derivation of $ \ottnt{m} \rightsquigarrow \ottnt{n_{{\mathrm{1}}}} $. +\end{proof} + +\begin{mathpar} +\mprset{fraction={-~}{-~}{-}} +\fbox{$ \ottnt{m} \in \kw{sn} $} \hfill \textit{backward closure in head position} \\ +\drule[width=0.45\textwidth]{sn-App-bwd} +\drule[width=0.55\textwidth]{sn-Let-bwd} +\end{mathpar} + +\begin{proof} + First, use \rref{sn-App-inv,sn-Let-inv} to obtain $ \ottnt{m} \in \kw{sn} $. + Then proceed by double induction on the derivations of + $ \ottnt{m} \in \kw{sn} $ and $ \ottnt{v} \in \kw{sn} $/$ \ottnt{n} \in \kw{sn} $, + again as lexicographic induction. + We want to show that if the conclusion steps, + then it steps to a strongly normal term. + Strong reduction of the head position eliminates the cases of $\beta$-reduction, + leaving the cases where the head position steps or the other position steps. + If the head position steps, we use \nameref{lem:confluence} + to join the strong reduction and the single-step reduction together, + then use the first induction hypothesis. + Otherwise, we use the second induction hypothesis. + We need the last premise to step through either of the subterms, + since we have no congruence rule for when the head position is not neutral. +\end{proof} + +\begin{lemma}[Backward closure] \label{lem:closure} + If $ \ottnt{m} \leadsto_{ \kw{sn} } \ottnt{n} $ and $ \ottnt{n} \in \kw{sn} $ then $ \ottnt{m} \in \kw{sn} $. +\end{lemma} + +\begin{proof} + By induction on the derivation of $ \ottnt{m} \leadsto_{ \kw{sn} } \ottnt{n} $. + The cases correspond exactly to each of + \rref{sn-Force-Thunk,sn-App-Lam,sn-Let-Ret,sn-Case-Inl,sn-Case-Inr,sn-App-bwd,sn-Let-bwd}. +\end{proof} + +\begin{lemma}[Soundness (\textsf{SNe})] \label{lem:sound-sne} + If $ \ottnt{m} \in \kw{SNe} $ then $ \ottnt{m} \in \kw{ne} $. +\end{lemma} + +\begin{proof} + By induction on the derivation of $ \ottnt{m} \in \kw{SNe} $. +\end{proof} + +\begin{theorem}[Soundness (\textsf{SN})] \leavevmode + \begin{enumerate} + \item If $ \ottnt{m} \in \kw{SNe} $ then $ \ottnt{m} \in \kw{sn} $. + \item If $ \ottnt{v} \in \kw{SN} $ then $ \ottnt{v} \in \kw{sn} $. + \item If $ \ottnt{m} \in \kw{SN} $ then $ \ottnt{m} \in \kw{sn} $. + \item If $ \ottnt{m} \leadsto \ottnt{n} $ then $ \ottnt{m} \leadsto_{ \kw{sn} } \ottnt{n} $. + \end{enumerate} +\end{theorem} + +\begin{proof} + By mutual induction on the derivations of + $ \ottnt{m} \in \kw{SNe} $, $ \ottnt{v} \in \kw{SN} $, $ \ottnt{m} \in \kw{SN} $, and $ \ottnt{m} \leadsto \ottnt{n} $. + The cases for the first three correspond to the admissible strongly normal rules, + using \nameref{lem:sound-sne} as needed, + except for the \rref*{SN-Red} case, which uses \nameref{lem:closure}. + The cases for strong reduction hold by construction. +\end{proof} + +\begin{corollary} + If $ \Gamma \vdash \ottnt{v} : \ottnt{A} $ then $ \ottnt{v} \in \kw{sn} $, + and if $ \Gamma \vdash \ottnt{m} : \ottnt{B} $ then $ \ottnt{m} \in \kw{sn} $. +\end{corollary} + +\section{Discussion} \label{sec:discussion} + +\end{document} \ No newline at end of file diff --git a/latexrun b/latexrun new file mode 100755 index 0000000..0533aff --- /dev/null +++ b/latexrun @@ -0,0 +1,1938 @@ +#!/usr/bin/env python3 + +# https://github.com/aclements/latexrun + +# Copyright (c) 2013, 2014 Austin Clements + +# Permission is hereby granted, free of charge, to any person obtaining a copy +# of this software and associated documentation files (the "Software"), to deal +# in the Software without restriction, including without limitation the rights +# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +# copies of the Software, and to permit persons to whom the Software is +# furnished to do so, subject to the following conditions: + +# The above copyright notice and this permission notice shall be included in +# all copies or substantial portions of the Software. + +# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN +# THE SOFTWARE. + +import sys +import os +import errno +import argparse +import shlex +import json +import subprocess +import re +import collections +import hashlib +import shutil +import curses +import filecmp +import io +import traceback +import time + +try: + import fcntl +except ImportError: + # Non-UNIX platform + fcntl = None + +def debug(string, *args): + if debug.enabled: + print(string.format(*args), file=sys.stderr) +debug.enabled = False + +def debug_exc(): + if debug.enabled: + traceback.print_exc() + +def main(): + # Parse command-line + arg_parser = argparse.ArgumentParser( + description='''A 21st century LaTeX wrapper, + %(prog)s runs latex (and bibtex) the right number of times so you + don't have to, + strips the log spew to make errors visible, + and plays well with standard build tools.''') + arg_parser.add_argument( + '-o', metavar='FILE', dest='output', default=None, + help='Output file name (default: derived from input file)') + arg_parser.add_argument( + '--latex-cmd', metavar='CMD', default='pdflatex', + help='Latex command (default: %(default)s)') + arg_parser.add_argument( + '--latex-args', metavar='ARGS', type=arg_parser_shlex, + help='Additional command-line arguments for latex.' + ' This will be parsed and split using POSIX shell rules.') + arg_parser.add_argument( + '--bibtex-cmd', metavar='CMD', default='bibtex', + help='Bibtex command (default: %(default)s)') + arg_parser.add_argument( + '--bibtex-args', metavar='ARGS', type=arg_parser_shlex, + help='Additional command-line arguments for bibtex') + arg_parser.add_argument( + '--max-iterations', metavar='N', type=int, default=10, + help='Max number of times to run latex before giving up' + ' (default: %(default)s)') + arg_parser.add_argument( + '-W', metavar='(no-)CLASS', + action=ArgParserWarnAction, dest='nowarns', default=set(['underfull']), + help='Enable/disable warning from CLASS, which can be any package name, ' + 'LaTeX warning class (e.g., font), bad box type ' + '(underfull, overfull, loose, tight), or "all"') + arg_parser.add_argument( + '-O', metavar='DIR', dest='obj_dir', default='latex.out', + help='Directory for intermediate files and control database ' + '(default: %(default)s)') + arg_parser.add_argument( + '--color', choices=('auto', 'always', 'never'), default='auto', + help='When to colorize messages') + arg_parser.add_argument( + '--verbose-cmds', action='store_true', default=False, + help='Print commands as they are executed') + arg_parser.add_argument( + '--debug', action='store_true', + help='Enable detailed debug output') + actions = arg_parser.add_argument_group('actions') + actions.add_argument( + '--clean-all', action='store_true', help='Delete output files') + actions.add_argument( + 'file', nargs='?', help='.tex file to compile') + args = arg_parser.parse_args() + if not any([args.clean_all, args.file]): + arg_parser.error('at least one action is required') + args.latex_args = args.latex_args or [] + args.bibtex_args = args.bibtex_args or [] + + verbose_cmd.enabled = args.verbose_cmds + debug.enabled = args.debug + + # A note about encodings: POSIX encoding is a mess; TeX encoding + # is a disaster. Our goal is to make things no worse, so we want + # byte-accurate round-tripping of TeX messages. Since TeX + # messages are *basically* text, we use strings and + # surrogateescape'ing for both input and output. I'm not fond of + # setting surrogateescape globally, but it's far easier than + # dealing with every place we pass TeX output through. + # Conveniently, JSON can round-trip surrogateescape'd strings, so + # our control database doesn't need special handling. + sys.stdout = io.TextIOWrapper( + sys.stdout.buffer, encoding=sys.stdout.encoding, + errors='surrogateescape', line_buffering=sys.stdout.line_buffering) + sys.stderr = io.TextIOWrapper( + sys.stderr.buffer, encoding=sys.stderr.encoding, + errors='surrogateescape', line_buffering=sys.stderr.line_buffering) + + Message.setup_color(args.color) + + # Open control database. + dbpath = os.path.join(args.obj_dir, '.latexrun.db') + if not os.path.exists(dbpath) and os.path.exists('.latexrun.db'): + # The control database used to live in the source directory. + # Support this for backwards compatibility. + dbpath = '.latexrun.db' + try: + db = DB(dbpath) + except (ValueError, OSError) as e: + print('error opening {}: {}'.format(e.filename if hasattr(e, 'filename') + else dbpath, e), + file=sys.stderr) + debug_exc() + sys.exit(1) + + # Clean + if args.clean_all: + try: + db.do_clean(args.obj_dir) + except OSError as e: + print(e, file=sys.stderr) + debug_exc() + sys.exit(1) + + # Build + if not args.file: + return + task_commit = None + try: + task_latex = LaTeX(db, args.file, args.latex_cmd, args.latex_args, + args.obj_dir, args.nowarns) + task_commit = LaTeXCommit(db, task_latex, args.output) + task_bibtex = BibTeX(db, task_latex, args.bibtex_cmd, args.bibtex_args, + args.nowarns, args.obj_dir) + tasks = [task_latex, task_commit, task_bibtex] + stable = run_tasks(tasks, args.max_iterations) + + # Print final task output and gather exit status + status = 0 + for task in tasks: + status = max(task.report(), status) + + if not stable: + print('error: files are still changing after {} iterations; giving up' + .format(args.max_iterations), file=sys.stderr) + status = max(status, 1) + except TaskError as e: + print(str(e), file=sys.stderr) + debug_exc() + status = 1 + + # Report final status, if interesting + fstatus = 'There were errors' if task_commit is None else task_commit.status + if fstatus: + output = args.output + if output is None: + if task_latex.get_outname() is not None: + output = os.path.basename(task_latex.get_outname()) + else: + output = 'output' + if Message._color: + terminfo.send('bold', ('setaf', 1)) + print('{}; {} not updated'.format(fstatus, output)) + if Message._color: + terminfo.send('sgr0') + sys.exit(status) + +def arg_parser_shlex(string): + """Argument parser for shell token lists.""" + try: + return shlex.split(string) + except ValueError as e: + raise argparse.ArgumentTypeError(str(e)) from None + +class ArgParserWarnAction(argparse.Action): + def __call__(self, parser, namespace, value, option_string=None): + nowarn = getattr(namespace, self.dest) + if value == 'all': + nowarn.clear() + elif value.startswith('no-'): + nowarn.add(value[3:]) + else: + nowarn.discard(value) + setattr(namespace, self.dest, nowarn) + +def verbose_cmd(args, cwd=None, env=None): + if verbose_cmd.enabled: + cmd = ' '.join(map(shlex.quote, args)) + if cwd is not None: + cmd = '(cd {} && {})'.format(shlex.quote(cwd), cmd) + if env is not None: + for k, v in env.items(): + if os.environ.get(k) != v: + cmd = '{}={} {}'.format(k, shlex.quote(v), cmd) + print(cmd, file=sys.stderr) +verbose_cmd.enabled = False + +def mkdir_p(path): + try: + os.makedirs(path) + except OSError as exc: + if exc.errno == errno.EEXIST and os.path.isdir(path): + pass + else: raise + +class DB: + """A latexrun control database.""" + + _VERSION = 'latexrun-db-v2' + + def __init__(self, filename): + self.__filename = filename + + # Make sure database directory exists + if os.path.dirname(self.__filename): + os.makedirs(os.path.dirname(self.__filename), exist_ok=True) + + # Lock the database if possible. We don't release this lock + # until the process exits. + lockpath = self.__filename + '.lock' + if fcntl is not None: + lockfd = os.open(lockpath, os.O_CREAT|os.O_WRONLY|os.O_CLOEXEC, 0o666) + # Note that this is actually an fcntl lock, not a lockf + # lock. Don't be fooled. + fcntl.lockf(lockfd, fcntl.LOCK_EX, 1) + + try: + fp = open(filename, 'r') + except FileNotFoundError: + debug('creating new database') + self.__val = {'version': DB._VERSION} + else: + debug('loading database') + self.__val = json.load(fp) + if 'version' not in self.__val: + raise ValueError('file exists, but does not appear to be a latexrun database'.format(filename)) + if self.__val['version'] != DB._VERSION: + raise ValueError('unknown database version {!r}' + .format(self.__val['version'])) + + def commit(self): + debug('committing database') + # Atomically commit database + tmp_filename = self.__filename + '.tmp' + with open(tmp_filename, 'w') as fp: + json.dump(self.__val, fp, indent=2, separators=(',', ': ')) + fp.flush() + os.fsync(fp.fileno()) + os.rename(tmp_filename, self.__filename) + + def get_summary(self, task_id): + """Return the recorded summary for the given task or None.""" + return self.__val.get('tasks', {}).get(task_id) + + def set_summary(self, task_id, summary): + """Set the summary for the given task.""" + self.__val.setdefault('tasks', {})[task_id] = summary + + def add_clean(self, filename): + """Add an output file to be cleaned. + + Unlike the output files recorded in the task summaries, + cleanable files strictly accumulate until a clean is + performed. + """ + self.__val.setdefault('clean', {})[filename] = hash_cache.get(filename) + + def do_clean(self, obj_dir=None): + """Remove output files and delete database. + + If obj_dir is not None and it is empty after all files are + removed, it will also be removed. + """ + + for f, want_hash in self.__val.get('clean', {}).items(): + have_hash = hash_cache.get(f) + if have_hash is not None: + if want_hash == have_hash: + debug('unlinking {}', f) + hash_cache.invalidate(f) + os.unlink(f) + else: + print('warning: {} has changed; not removing'.format(f), + file=sys.stderr) + self.__val = {'version': DB._VERSION} + try: + os.unlink(self.__filename) + except FileNotFoundError: + pass + if obj_dir is not None: + try: + os.rmdir(obj_dir) + except OSError: + pass + +class HashCache: + """Cache of file hashes. + + As latexrun reaches fixed-point, it hashes the same files over and + over, many of which never change. Since hashing is somewhat + expensive, we keep a simple cache of these hashes. + """ + + def __init__(self): + self.__cache = {} + + def get(self, filename): + """Return the hash of filename, or * if it was clobbered.""" + try: + with open(filename, 'rb') as fp: + st = os.fstat(fp.fileno()) + key = (st.st_dev, st.st_ino) + if key in self.__cache: + return self.__cache[key] + + debug('hashing {}', filename) + h = hashlib.sha256() + while True: + block = fp.read(256*1024) + if not len(block): + break + h.update(block) + self.__cache[key] = h.hexdigest() + return self.__cache[key] + except (FileNotFoundError, IsADirectoryError): + return None + + def clobber(self, filename): + """If filename's hash is not known, record an invalid hash. + + This can be used when filename was overwritten before we were + necessarily able to obtain its hash. filename must exist. + """ + st = os.stat(filename) + key = (st.st_dev, st.st_ino) + if key not in self.__cache: + self.__cache[key] = '*' + + def invalidate(self, filename): + try: + st = os.stat(filename) + except OSError as e: + # Pessimistically wipe the whole cache + debug('wiping hash cache ({})', e) + self.__cache.clear() + else: + key = (st.st_dev, st.st_ino) + if key in self.__cache: + del self.__cache[key] +hash_cache = HashCache() + +class _Terminfo: + def __init__(self): + self.__tty = os.isatty(sys.stdout.fileno()) + if self.__tty: + curses.setupterm() + self.__ti = {} + + def __ensure(self, cap): + if cap not in self.__ti: + if not self.__tty: + string = None + else: + string = curses.tigetstr(cap) + if string is None or b'$<' in string: + # Don't have this capability or it has a pause + string = None + self.__ti[cap] = string + return self.__ti[cap] + + def has(self, *caps): + return all(self.__ensure(cap) is not None for cap in caps) + + def send(self, *caps): + # Flush TextIOWrapper to the binary IO buffer + sys.stdout.flush() + for cap in caps: + # We should use curses.putp here, but it's broken in + # Python3 because it writes directly to C's buffered + # stdout and there's no way to flush that. + if isinstance(cap, tuple): + s = curses.tparm(self.__ensure(cap[0]), *cap[1:]) + else: + s = self.__ensure(cap) + sys.stdout.buffer.write(s) +terminfo = _Terminfo() + +class Progress: + _enabled = None + + def __init__(self, prefix): + self.__prefix = prefix + if Progress._enabled is None: + Progress._enabled = (not debug.enabled) and \ + terminfo.has('cr', 'el', 'rmam', 'smam') + + def __enter__(self): + self.last = '' + self.update('') + return self + + def __exit__(self, typ, value, traceback): + if Progress._enabled: + # Beginning of line and clear + terminfo.send('cr', 'el') + sys.stdout.flush() + + def update(self, msg): + if not Progress._enabled: + return + out = '[' + self.__prefix + ']' + if msg: + out += ' ' + msg + if out != self.last: + # Beginning of line, clear line, disable wrap + terminfo.send('cr', 'el', 'rmam') + sys.stdout.write(out) + # Enable wrap + terminfo.send('smam') + self.last = out + sys.stdout.flush() + +class Message(collections.namedtuple( + 'Message', 'typ filename lineno msg')): + def emit(self): + if self.filename: + if self.filename.startswith('./'): + finfo = self.filename[2:] + else: + finfo = self.filename + else: + finfo = '' + if self.lineno is not None: + finfo += ':' + str(self.lineno) + finfo += ': ' + if self._color: + terminfo.send('bold') + sys.stdout.write(finfo) + + if self.typ != 'info': + if self._color: + terminfo.send(('setaf', 5 if self.typ == 'warning' else 1)) + sys.stdout.write(self.typ + ': ') + if self._color: + terminfo.send('sgr0') + sys.stdout.write(self.msg + '\n') + + @classmethod + def setup_color(cls, state): + if state == 'never': + cls._color = False + elif state == 'always': + cls._color = True + elif state == 'auto': + cls._color = terminfo.has('setaf', 'bold', 'sgr0') + else: + raise ValueError('Illegal color state {:r}'.format(state)) + + +################################################################## +# Task framework +# + +terminate_task_loop = False +start_time = time.time() + +def run_tasks(tasks, max_iterations): + """Execute tasks in round-robin order until all are stable. + + This will also exit if terminate_task_loop is true. Tasks may use + this to terminate after a fatal error (even if that fatal error + doesn't necessarily indicate stability; as long as re-running the + task will never eliminate the fatal error). + + Return True if fixed-point is reached or terminate_task_loop is + set within max_iterations iterations. + """ + + global terminate_task_loop + terminate_task_loop = False + + nstable = 0 + for iteration in range(max_iterations): + for task in tasks: + if task.stable(): + nstable += 1 + if nstable == len(tasks): + debug('fixed-point reached') + return True + else: + task.run() + nstable = 0 + if terminate_task_loop: + debug('terminate_task_loop set') + return True + debug('fixed-point not reached') + return False + +class TaskError(Exception): + pass + +class Task: + """A deterministic computation whose inputs and outputs can be captured.""" + + def __init__(self, db, task_id): + self.__db = db + self.__task_id = task_id + + def __debug(self, string, *args): + if debug.enabled: + debug('task {}: {}', self.__task_id, string.format(*args)) + + def stable(self): + """Return True if running this task will not affect system state. + + Functionally, let f be the task, and s be the system state. + Then s' = f(s). If it must be that s' == s (that is, f has + reached a fixed point), then this function must return True. + """ + last_summary = self.__db.get_summary(self.__task_id) + if last_summary is None: + # Task has never run, so running it will modify system + # state + changed = 'never run' + else: + # If any of the inputs have changed since the last run of + # this task, the result may change, so re-run the task. + # Also, it's possible something else changed an output + # file, in which case we also want to re-run the task, so + # check the outputs, too. + changed = self.__summary_changed(last_summary) + + if changed: + self.__debug('unstable (changed: {})', changed) + return False + else: + self.__debug('stable') + return True + + def __summary_changed(self, summary): + """Test if any inputs changed from summary. + + Returns a string describing the changed input, or None. + """ + for dep in summary['deps']: + fn, args, val = dep + method = getattr(self, '_input_' + fn, None) + if method is None: + return 'unknown dependency method {}'.format(fn) + if method == self._input_unstable or method(*args) != val: + return '{}{}'.format(fn, tuple(args)) + return None + + def _input(self, name, *args): + """Register an input for this run. + + This calls self._input_(*args) to get the value of this + input. This function should run quickly and return some + projection of system state that affects the result of this + computation. + + Both args and the return value must be JSON serializable. + """ + method = getattr(self, '_input_' + name) + val = method(*args) + if [name, args, val] not in self.__deps: + self.__deps.append([name, args, val]) + return val + + def run(self): + # Before we run the task, pre-hash any files that were output + # files in the last run. These may be input by this run and + # then clobbered, at which point it will be too late to get an + # input hash. Ideally we would only hash files that were + # *both* input and output files, but latex doesn't tell us + # about input files that didn't exist, so if we start from a + # clean slate, we often require an extra run because we don't + # know a file is input/output until after the second run. + last_summary = self.__db.get_summary(self.__task_id) + if last_summary is not None: + for io_filename in last_summary['output_files']: + self.__debug('pre-hashing {}', io_filename) + hash_cache.get(io_filename) + + # Run the task + self.__debug('running') + self.__deps = [] + result = self._execute() + + # Clear cached output file hashes + for filename in result.output_filenames: + hash_cache.invalidate(filename) + + # If the output files change, then the computation needs to be + # re-run, so record them as inputs + for filename in result.output_filenames: + self._input('file', filename) + + # Update task summary in database + self.__db.set_summary(self.__task_id, + self.__make_summary(self.__deps, result)) + del self.__deps + + # Add output files to be cleaned + for f in result.output_filenames: + self.__db.add_clean(f) + + try: + self.__db.commit() + except OSError as e: + raise TaskError('error committing control database {}: {}'.format( + getattr(e, 'filename', ''), e)) from e + + def __make_summary(self, deps, run_result): + """Construct a new task summary.""" + return { + 'deps': deps, + 'output_files': {f: hash_cache.get(f) + for f in run_result.output_filenames}, + 'extra': run_result.extra, + } + + def _execute(self): + """Abstract: Execute this task. + + Subclasses should implement this method to execute this task. + This method must return a RunResult giving the inputs that + were used by the task and the outputs it produced. + """ + raise NotImplementedError('Task._execute is abstract') + + def _get_result_extra(self): + """Return the 'extra' result from the previous run, or None.""" + summary = self.__db.get_summary(self.__task_id) + if summary is None: + return None + return summary['extra'] + + def report(self): + """Report the task's results to stdout and return exit status. + + This may be called when the task has never executed. + Subclasses should override this. The default implementation + reports nothing and returns 0. + """ + return 0 + + # Standard input functions + + def _input_env(self, var): + return os.environ.get(var) + + def _input_file(self, path): + return hash_cache.get(path) + + def _input_unstable(self): + """Mark this run as unstable, regardless of other inputs.""" + return None + + def _input_unknown_input(self): + """An unknown input that may change after latexrun exits. + + This conservatively marks some unknown input that definitely + won't change while latexrun is running, but may change before + the user next runs latexrun. This allows the task to + stabilize during this invocation, but will cause the task to + re-run on the next invocation. + """ + return start_time + +class RunResult(collections.namedtuple( + 'RunResult', 'output_filenames extra')): + """The result of a single task execution. + + This captures all files written by the task, and task-specific + results that need to be persisted between runs (for example, to + enable reporting of a task's results). + """ + pass + +################################################################## +# LaTeX task +# + +def normalize_input_path(path): + # Resolve the directory of the input path, but leave the file + # component alone because it affects TeX's behavior. + head, tail = os.path.split(path) + npath = os.path.join(os.path.realpath(head), tail) + return os.path.relpath(path) + +class LaTeX(Task): + def __init__(self, db, tex_filename, cmd, cmd_args, obj_dir, nowarns): + super().__init__(db, 'latex::' + normalize_input_path(tex_filename)) + self.__tex_filename = tex_filename + self.__cmd = cmd + self.__cmd_args = cmd_args + self.__obj_dir = obj_dir + self.__nowarns = nowarns + + self.__pass = 0 + + def _input_args(self): + # If filename starts with a character the tex command-line + # treats specially, then tweak it so it doesn't. + filename = self.__tex_filename + if filename.startswith(('-', '&', '\\')): + filename = './' + filename + # XXX Put these at the beginning in case the provided + # arguments are malformed. Might want to do a best-effort + # check for incompatible user-provided arguments (note: + # arguments can be given with one or two dashes and those with + # values can use an equals or a space). + return [self.__cmd] + self.__cmd_args + \ + ['-interaction', 'nonstopmode', '-recorder', + '-output-directory', self.__obj_dir, filename] + + def _execute(self): + # Run latex + self.__pass += 1 + args = self._input('args') + debug('running {}', args) + try: + os.makedirs(self.__obj_dir, exist_ok=True) + except OSError as e: + raise TaskError('failed to create %s: ' % self.__obj_dir + str(e)) \ + from e + try: + verbose_cmd(args) + p = subprocess.Popen(args, + stdin=subprocess.DEVNULL, + stdout=subprocess.PIPE, + stderr=subprocess.STDOUT) + stdout, has_errors, missing_includes = self.__feed_terminal(p.stdout) + status = p.wait() + except OSError as e: + raise TaskError('failed to execute latex task: ' + str(e)) from e + + # Register environment variable inputs + for env_var in ['TEXMFOUTPUT', 'TEXINPUTS', 'TEXFORMATS', 'TEXPOOL', + 'TFMFONTS', 'PATH']: + self._input('env', env_var) + + jobname, outname = self.__parse_jobname(stdout) + inputs, outputs = self.__parse_recorder(jobname) + + # LaTeX overwrites its own inputs. Mark its output files as + # clobbered before we hash its input files. + for path in outputs: + # In some abort cases (e.g., >=100 errors), LaTeX claims + # output files that don't actually exist. + if os.path.exists(path): + hash_cache.clobber(path) + # Depend on input files. Task.run pre-hashed outputs from the + # previous run, so if this isn't the first run and as long as + # the set of outputs didn't change, we'll be able to get the + # input hashes, even if they were clobbered. + for path in inputs: + self._input('file', path) + + if missing_includes: + # Missing \includes are tricky. Ideally we'd depend on + # the absence of some file, but in fact we'd have to + # depend on the failure of a whole kpathsea lookup. + # Rather than try to be clever, just mark this as an + # unknown input so we'll run at least once on the next + # invocation. + self._input('unknown_input') + + if not self.__create_outdirs(stdout) and has_errors: + # LaTeX reported unrecoverable errors (other than output + # directory errors, which we just fixed). We could + # continue to stabilize the document, which may change + # some of the other problems reported (but not the + # unrecoverable errors), or we can just abort now and get + # back to the user quickly with the major errors. We opt + # for the latter. + global terminate_task_loop + terminate_task_loop = True + # This error could depend on something we failed to track. + # It would be really confusing if we continued to report + # the error after the user fixed it, so be conservative + # and force a re-run next time. + self._input('unknown_input') + + return RunResult(outputs, + {'jobname': jobname, 'outname': outname, + 'status': status}) + + def __feed_terminal(self, stdout): + prefix = 'latex' + if self.__pass > 1: + prefix += ' ({})'.format(self.__pass) + with Progress(prefix) as progress: + buf = [] + filt = LaTeXFilter() + while True: + # Use os.read to read only what's available on the pipe, + # without waiting to fill a buffer + data = os.read(stdout.fileno(), 4096) + if not data: + break + # See "A note about encoding" above + data = data.decode('ascii', errors='surrogateescape') + buf.append(data) + filt.feed(data) + file_stack = filt.get_file_stack() + if file_stack: + tos = file_stack[-1] + if tos.startswith('./'): + tos = tos[2:] + progress.update('>' * len(file_stack) + ' ' + tos) + else: + progress.update('') + + # Were there unrecoverable errors? + has_errors = any(msg.typ == 'error' for msg in filt.get_messages()) + + return ''.join(buf), has_errors, filt.has_missing_includes() + + def __parse_jobname(self, stdout): + """Extract the job name and output name from latex's output. + + We get these from latex because they depend on complicated + file name parsing rules, are affected by arguments like + -output-directory, and may be just "texput" if things fail + really early. The output name may be None if there were no + pages of output. + """ + jobname = outname = None + for m in re.finditer(r'^Transcript written on "?(.*)\.log"?\.$', stdout, + re.MULTILINE | re.DOTALL): + jobname = m.group(1).replace('\n', '') + if jobname is None: + print(stdout, file=sys.stderr) + raise TaskError('failed to extract job name from latex log') + for m in re.finditer(r'^Output written on "?(.*\.[^ ."]+)"? \([0-9]+ page', + stdout, re.MULTILINE | re.DOTALL): + outname = m.group(1).replace('\n', '') + if outname is None and not \ + re.search(r'^No pages of output\.$|^! Emergency stop\.$' + r'|^! ==> Fatal error occurred, no output PDF file produced!$', + stdout, re.MULTILINE): + print(stdout, file=sys.stderr) + raise TaskError('failed to extract output name from latex log') + + # LuaTeX (0.76.0) doesn't include the output directory in the + # logged transcript or output file name. + if os.path.basename(jobname) == jobname and \ + os.path.exists(os.path.join(self.__obj_dir, jobname + '.log')): + jobname = os.path.join(self.__obj_dir, jobname) + if outname is not None: + outname = os.path.join(self.__obj_dir, outname) + + return jobname, outname + + def __parse_recorder(self, jobname): + """Parse file recorder output.""" + # XXX If latex fails because a file isn't found, that doesn't + # go into the .fls file, but creating that file will affect + # the computation, so it should be included as an input. + # Though it's generally true that files can be added earlier + # in search paths and will affect the output without us knowing. + # + # XXX This is a serious problem for bibtex, since the first + # run won't depend on the .bbl file! But maybe the .aux file + # will always cause a re-run, at which point the .bbl will + # exist? + filename = jobname + '.fls' + try: + recorder = open(filename) + except OSError as e: + raise TaskError('failed to open file recorder output: ' + str(e)) \ + from e + pwd, inputs, outputs = '', set(), set() + for linenum, line in enumerate(recorder): + parts = line.rstrip('\n').split(' ', 1) + if parts[0] == 'PWD': + pwd = parts[1] + elif parts[0] in ('INPUT', 'OUTPUT'): + if parts[1].startswith('/'): + path = parts[1] + else: + # Try to make "nice" paths, especially for clean + path = os.path.relpath(os.path.join(pwd, parts[1])) + if parts[0] == 'INPUT': + inputs.add(path) + else: + outputs.add(path) + else: + raise TaskError('syntax error on line {} of {}' + .format(linenum, filename)) + # Ironically, latex omits the .fls file itself + outputs.add(filename) + return inputs, outputs + + def __create_outdirs(self, stdout): + # In some cases, such as \include'ing a file from a + # subdirectory, TeX will attempt to create files in + # subdirectories of the output directory that don't exist. + # Detect this, create the output directory, and re-run. + m = re.search('^! I can\'t write on file `(.*)\'\\.$', stdout, re.M) + if m and m.group(1).find('/') > 0 and '../' not in m.group(1): + debug('considering creating output sub-directory for {}'. + format(m.group(1))) + subdir = os.path.dirname(m.group(1)) + newdir = os.path.join(self.__obj_dir, subdir) + if os.path.isdir(subdir) and not os.path.isdir(newdir): + debug('creating output subdirectory {}'.format(newdir)) + try: + mkdir_p(newdir) + except OSError as e: + raise TaskError('failed to create output subdirectory: ' + + str(e)) from e + self._input('unstable') + return True + + def report(self): + extra = self._get_result_extra() + if extra is None: + return 0 + + # Parse the log + logfile = open(extra['jobname'] + '.log', 'rt', errors='surrogateescape') + for msg in self.__clean_messages( + LaTeXFilter(self.__nowarns).feed( + logfile.read(), True).get_messages()): + msg.emit() + + # Return LaTeX's exit status + return extra['status'] + + def __clean_messages(self, msgs): + """Make some standard log messages more user-friendly.""" + have_undefined_reference = False + for msg in msgs: + if msg.msg == '==> Fatal error occurred, no output PDF file produced!': + msg = msg._replace(typ='info', + msg='Fatal error (no output file produced)') + if msg.msg.startswith('[LaTeX] '): + # Strip unnecessary package name + msg = msg._replace(msg=msg.msg.split(' ', 1)[1]) + if re.match(r'Reference .* undefined', msg.msg): + have_undefined_reference = True + if have_undefined_reference and \ + re.match(r'There were undefined references', msg.msg): + # LaTeX prints this at the end so the user knows it's + # worthwhile looking back at the log. Since latexrun + # makes the earlier messages obvious, this is + # redundant. + continue + yield msg + + def get_tex_filename(self): + return self.__tex_filename + + def get_jobname(self): + extra = self._get_result_extra() + if extra is None: + return None + return extra['jobname'] + + def get_outname(self): + extra = self._get_result_extra() + if extra is None: + return None + return extra['outname'] + + def get_status(self): + extra = self._get_result_extra() + if extra is None: + return None + return extra['status'] + +class LaTeXCommit(Task): + def __init__(self, db, latex_task, output_path): + super().__init__(db, 'latex_commit::' + + normalize_input_path(latex_task.get_tex_filename())) + self.__latex_task = latex_task + self.__output_path = output_path + self.status = 'There were errors' + + def _input_latex(self): + return self.__latex_task.get_status(), self.__latex_task.get_outname() + + def _execute(self): + self.status = 'There were errors' + + # If latex succeeded with output, atomically commit the output + status, outname = self._input('latex') + if status != 0 or outname is None: + debug('not committing (status {}, outname {})', status, outname) + if outname is None: + self.status = 'No pages of output' + return RunResult([], None) + + commit = self.__output_path or os.path.basename(outname) + if os.path.abspath(commit) == os.path.abspath(outname): + debug('skipping commit (outname is commit name)') + self.status = None + return RunResult([], None) + + try: + if os.path.exists(commit) and filecmp.cmp(outname, commit): + debug('skipping commit ({} and {} are identical)', + outname, commit) + # To avoid confusion, touch the output file + open(outname, 'r+b').close() + else: + debug('commiting {} to {}', outname, commit) + shutil.copy(outname, outname + '~') + os.rename(outname + '~', commit) + except OSError as e: + raise TaskError('error committing latex output: {}'.format(e)) from e + self._input('file', outname) + self.status = None + return RunResult([commit], None) + +class LaTeXFilter: + TRACE = False # Set to enable detailed parse tracing + + def __init__(self, nowarns=[]): + self.__data = '' + self.__restart_pos = 0 + self.__restart_file_stack = [] + self.__restart_messages_len = 0 + self.__messages = [] + self.__first_file = None + self.__fatal_error = False + self.__missing_includes = False + self.__pageno = 1 + self.__restart_pageno = 1 + + self.__suppress = {cls: 0 for cls in nowarns} + + def feed(self, data, eof=False): + """Feed LaTeX log data to the parser. + + The log data can be from LaTeX's standard output, or from the + log file. If there will be no more data, set eof to True. + """ + + self.__data += data + self.__data_complete = eof + + # Reset to last known-good restart point + self.__pos = self.__restart_pos + self.__file_stack = self.__restart_file_stack.copy() + self.__messages = self.__messages[:self.__restart_messages_len] + self.__lstart = self.__lend = -1 + self.__pageno = self.__restart_pageno + + # Parse forward + while self.__pos < len(self.__data): + self.__noise() + + # Handle suppressed warnings + if eof: + msgs = ['%d %s warning%s' % (count, cls, "s" if count > 1 else "") + for cls, count in self.__suppress.items() if count] + if msgs: + self.__message('info', None, + '%s not shown (use -Wall to show them)' % + ', '.join(msgs), filename=self.__first_file) + + if eof and len(self.__file_stack) and not self.__fatal_error: + # Fatal errors generally cause TeX to "succumb" without + # closing the file stack, so don't complain in that case. + self.__message('warning', None, + "unbalanced `(' in log; file names may be wrong") + return self + + def get_messages(self): + """Return a list of warning and error Messages.""" + return self.__messages + + def get_file_stack(self): + """Return the file stack for the data that has been parsed. + + This results a list from outermost file to innermost file. + The list may be empty. + """ + + return self.__file_stack + + def has_missing_includes(self): + """Return True if the log reported missing \\include files.""" + return self.__missing_includes + + def __save_restart_point(self): + """Save the current state as a known-good restart point. + + On the next call to feed, the parser will reset to this point. + """ + self.__restart_pos = self.__pos + self.__restart_file_stack = self.__file_stack.copy() + self.__restart_messages_len = len(self.__messages) + self.__restart_pageno = self.__pageno + + def __message(self, typ, lineno, msg, cls=None, filename=None): + if cls is not None and cls in self.__suppress: + self.__suppress[cls] += 1 + return + filename = filename or (self.__file_stack[-1] if self.__file_stack + else self.__first_file) + self.__messages.append(Message(typ, filename, lineno, msg)) + + def __ensure_line(self): + """Update lstart and lend.""" + if self.__lstart <= self.__pos < self.__lend: + return + self.__lstart = self.__data.rfind('\n', 0, self.__pos) + 1 + self.__lend = self.__data.find('\n', self.__pos) + 1 + if self.__lend == 0: + self.__lend = len(self.__data) + + @property + def __col(self): + """The 0-based column number of __pos.""" + self.__ensure_line() + return self.__pos - self.__lstart + + @property + def __avail(self): + return self.__pos < len(self.__data) + + def __lookingat(self, needle): + return self.__data.startswith(needle, self.__pos) + + def __lookingatre(self, regexp, flags=0): + return re.compile(regexp, flags=flags).match(self.__data, self.__pos) + + def __skip_line(self): + self.__ensure_line() + self.__pos = self.__lend + + def __consume_line(self, unwrap=False): + self.__ensure_line() + data = self.__data[self.__pos:self.__lend] + self.__pos = self.__lend + if unwrap: + # TeX helpfully wraps all terminal output at 79 columns + # (max_print_line). If requested, unwrap it. There's + # simply no way to do this perfectly, since there could be + # a line that happens to be 79 columns. + # + # We check for >=80 because a bug in LuaTeX causes it to + # wrap at 80 columns instead of 79 (LuaTeX #900). + while self.__lend - self.__lstart >= 80: + if self.TRACE: print('<{}> wrapping'.format(self.__pos)) + self.__ensure_line() + data = data[:-1] + self.__data[self.__pos:self.__lend] + self.__pos = self.__lend + return data + + # Parser productions + + def __noise(self): + # Most of TeX's output is line noise that combines error + # messages, warnings, file names, user errors and warnings, + # and echos of token lists and other input. This attempts to + # tease these apart, paying particular attention to all of the + # places where TeX echos input so that parens in the input do + # not confuse the file name scanner. There are three + # functions in TeX that echo input: show_token_list (used by + # runaway and show_context, which is used by print_err), + # short_display (used by overfull/etc h/vbox), and show_print + # (used in issue_message and the same places as + # show_token_list). + lookingat, lookingatre = self.__lookingat, self.__lookingatre + if self.__col == 0: + # The following messages are always preceded by a newline + if lookingat('! '): + return self.__errmessage() + if lookingat('!pdfTeX error: '): + return self.__pdftex_fail() + if lookingat('Runaway '): + return self.__runaway() + if lookingatre(r'(Overfull|Underfull|Loose|Tight) \\[hv]box \('): + return self.__bad_box() + if lookingatre('(Package |Class |LaTeX |pdfTeX )?(\\w+ )?warning: ', re.I): + return self.__generic_warning() + if lookingatre('No file .*\\.tex\\.$', re.M): + # This happens with \includes of missing files. For + # whatever reason, LaTeX doesn't consider this even + # worth a warning, but I do! + self.__message('warning', None, + self.__simplify_message( + self.__consume_line(unwrap=True).strip())) + self.__missing_includes = True + return + # Other things that are common and irrelevant + if lookingatre(r'(Package|Class|LaTeX) (\w+ )?info: ', re.I): + return self.__generic_info() + if lookingatre(r'(Document Class|File|Package): '): + # Output from "\ProvidesX" + return self.__consume_line(unwrap=True) + if lookingatre(r'\\\w+=\\[a-z]+\d+\n'): + # Output from "\new{count,dimen,skip,...}" + return self.__consume_line(unwrap=True) + + # print(self.__data[self.__lstart:self.__lend].rstrip()) + # self.__pos = self.__lend + # return + + # Now that we've substantially reduced the spew and hopefully + # eliminated all input echoing, we're left with the file name + # stack, page outs, and random other messages from both TeX + # and various packages. We'll assume at this point that all + # parentheses belong to the file name stack or, if they're in + # random other messages, they're at least balanced and nothing + # interesting happens between them. For page outs, ship_out + # prints a space if not at the beginning of a line, then a + # "[", then the page number being shipped out (this is + # usually, but not always, followed by "]"). + m = re.compile(r'[(){}\n]|(?<=[\n ])\[\d+', re.M).\ + search(self.__data, self.__pos) + if m is None: + self.__pos = len(self.__data) + return + self.__pos = m.start() + 1 + ch = self.__data[m.start()] + if ch == '\n': + # Save this as a known-good restart point for incremental + # parsing, since we definitely didn't match any of the + # known message types above. + self.__save_restart_point() + elif ch == '[': + # This is printed at the end of a page, so we're beginning + # page n+1. + self.__pageno = int(self.__lookingatre(r'\d+').group(0)) + 1 + elif ((self.__data.startswith('`', m.start() - 1) or + self.__data.startswith('`\\', m.start() - 2)) and + self.__data.startswith('\'', m.start() + 1)): + # (, ), {, and } sometimes appear in TeX's error + # descriptions, but they're always in `'s (and sometimes + # backslashed) + return + elif ch == '(': + # XXX Check that the stack doesn't drop to empty and then re-grow + first = self.__first_file is None and self.__col == 1 + filename = self.__filename() + self.__file_stack.append(filename) + if first: + self.__first_file = filename + if self.TRACE: + print('<{}>{}enter {}'.format( + m.start(), ' '*len(self.__file_stack), filename)) + elif ch == ')': + if len(self.__file_stack): + if self.TRACE: + print('<{}>{}exit {}'.format( + m.start(), ' '*len(self.__file_stack), + self.__file_stack[-1])) + self.__file_stack.pop() + else: + self.__message('warning', None, + "extra `)' in log; file names may be wrong ") + elif ch == '{': + # TeX uses this for various things we want to ignore, like + # file names and print_mark. Consume up to the '}' + epos = self.__data.find('}', self.__pos) + if epos != -1: + self.__pos = epos + 1 + else: + self.__message('warning', None, + "unbalanced `{' in log; file names may be wrong") + elif ch == '}': + self.__message('warning', None, + "extra `}' in log; file names may be wrong") + + def __filename(self): + initcol = self.__col + first = True + name = '' + # File names may wrap, but if they do, TeX will always print a + # newline before the open paren + while first or (initcol == 1 and self.__lookingat('\n') + and self.__col >= 79): + if not first: + self.__pos += 1 + m = self.__lookingatre(r'[^(){} \n]*') + name += m.group() + self.__pos = m.end() + first = False + return name + + def __simplify_message(self, msg): + msg = re.sub(r'^(?:Package |Class |LaTeX |pdfTeX )?([^ ]+) (?:Error|Warning): ', + r'[\1] ', msg, flags=re.I) + msg = re.sub(r'\.$', '', msg) + msg = re.sub(r'has occurred (while \\output is active)', r'\1', msg) + return msg + + def __errmessage(self): + # Procedure print_err (including \errmessage, itself used by + # LaTeX's \GenericError and all of its callers), as well as + # fatal_error. Prints "\n! " followed by error text + # ("Emergency stop" in the case of fatal_error). print_err is + # always followed by a call to error, which prints a period, + # and a newline... + msg = self.__consume_line(unwrap=True)[1:].strip() + is_fatal_error = (msg == 'Emergency stop.') + msg = self.__simplify_message(msg) + # ... and then calls show_context, which prints the input + # stack as pairs of lines giving the context. These context + # lines are truncated so they never wrap. Each pair of lines + # will start with either " " if the context is a + # token list, "<*> " for terminal input (or command line), + # "" for stream reads, something like "\macroname + # #1->" for macros (though everything after \macroname is + # subject to being elided as "..."), or "l.[0-9]+ " if it's a + # file. This is followed by the errant input with a line + # break where the error occurred. + lineno = None + found_context = False + stack = [] + while self.__avail: + m1 = self.__lookingatre(r'<([a-z ]+|\*|read [^ >]*)> |\\.*(->|...)') + m2 = self.__lookingatre('l\\.[0-9]+ ') + if m1: + found_context = True + pre = self.__consume_line().rstrip('\n') + stack.append(pre) + elif m2: + found_context = True + pre = self.__consume_line().rstrip('\n') + info, rest = pre.split(' ', 1) + lineno = int(info[2:]) + stack.append(rest) + elif found_context: + # Done with context + break + if found_context: + # Consume the second context line + post = self.__consume_line().rstrip('\n') + # Clean up goofy trailing ^^M TeX sometimes includes + post = re.sub(r'\^\^M$', '', post) + if post[:len(pre)].isspace() and not post.isspace(): + stack.append(len(stack[-1])) + stack[-2] += post[len(pre):] + else: + # If we haven't found the context, skip the line. + self.__skip_line() + stack_msg = '' + for i, trace in enumerate(stack): + stack_msg += ('\n ' + (' ' * trace) + '^' + if isinstance(trace, int) else + '\n at ' + trace.rstrip() if i == 0 else + '\n from ' + trace.rstrip()) + + if is_fatal_error: + # fatal_error always prints one additional line of message + info = self.__consume_line().strip() + if info.startswith('*** '): + info = info[4:] + msg += ': ' + info.lstrip('(').rstrip(')') + + self.__message('error', lineno, msg + stack_msg) + self.__fatal_error = True + + def __pdftex_fail(self): + # Procedure pdftex_fail. Prints "\n!pdfTeX error: ", the + # message, and a newline. Unlike print_err, there's never + # context. + msg = self.__consume_line(unwrap=True)[1:].strip() + msg = self.__simplify_message(msg) + self.__message('error', None, msg) + + def __runaway(self): + # Procedure runaway. Prints "\nRunaway ...\n" possibly + # followed by token list (user text). Always followed by a + # call to print_err, so skip lines until we see the print_err. + self.__skip_line() # Skip "Runaway ...\n" + if not self.__lookingat('! ') and self.__avail: + # Skip token list, which is limited to one line + self.__skip_line() + + def __bad_box(self): + # Function hpack and vpack. hpack prints a warning, a + # newline, then a short_display of the offending text. + # Unfortunately, there's nothing indicating the end of the + # offending text, but it should be on one (possible wrapped) + # line. vpack prints a warning and then, *unless output is + # active*, a newline. The missing newline is probably a bug, + # but it sure makes our lives harder. + origpos = self.__pos + msg = self.__consume_line() + m = re.search(r' in (?:paragraph|alignment) at lines ([0-9]+)--([0-9]+)', msg) or \ + re.search(r' detected at line ([0-9]+)', msg) + if m: + # Sometimes TeX prints crazy line ranges like "at lines + # 8500--250". The lower number seems roughly sane, so use + # that. I'm not sure what causes this, but it may be + # related to shipout routines messing up line registers. + lineno = min(int(m.group(1)), int(m.groups()[-1])) + msg = msg[:m.start()] + else: + m = re.search(r' while \\output is active', msg) + if m: + lineno = None + msg = msg[:m.end()] + else: + self.__message('warning', None, + 'malformed bad box message in log') + return + # Back up to the end of the known message text + self.__pos = origpos + m.end() + if self.__lookingat('\n'): + # We have a newline, so consume it and look for the + # offending text. + self.__pos += 1 + # If there is offending text, it will start with a font + # name, which will start with a \. + if 'hbox' in msg and self.__lookingat('\\'): + self.__consume_line(unwrap=True) + msg = self.__simplify_message(msg) + ' (page {})'.format(self.__pageno) + cls = msg.split(None, 1)[0].lower() + self.__message('warning', lineno, msg, cls=cls) + + def __generic_warning(self): + # Warnings produced by LaTeX's \GenericWarning (which is + # called by \{Package,Class}Warning and \@latex@warning), + # warnings produced by pdftex_warn, and other random warnings. + msg, cls = self.__generic_info() + # Most warnings include an input line emitted by \on@line + m = re.search(' on input line ([0-9]+)', msg) + if m: + lineno = int(m.group(1)) + msg = msg[:m.start()] + else: + lineno = None + msg = self.__simplify_message(msg) + self.__message('warning', lineno, msg, cls=cls) + + def __generic_info(self): + # Messages produced by LaTeX's \Generic{Error,Warning,Info} + # and things that look like them + msg = self.__consume_line(unwrap=True).strip() + # Package and class messages are continued with lines + # containing '(package name) ' + pkg_name = msg.split(' ', 2)[1] + prefix = '(' + pkg_name + ') ' + while self.__lookingat(prefix): + # Collect extra lines. It's important that we keep these + # because they may contain context information like line + # numbers. + extra = self.__consume_line(unwrap=True) + msg += ' ' + extra[len(prefix):].strip() + return msg, pkg_name.lower() + +################################################################## +# BibTeX task +# + +class BibTeX(Task): + def __init__(self, db, latex_task, cmd, cmd_args, nowarns, obj_dir): + super().__init__(db, 'bibtex::' + normalize_input_path( + latex_task.get_tex_filename())) + self.__latex_task = latex_task + self.__cmd = cmd + self.__cmd_args = cmd_args + self.__obj_dir = obj_dir + + def stable(self): + # If bibtex doesn't have its inputs, then it's stable because + # it has no effect on system state. + jobname = self.__latex_task.get_jobname() + if jobname is None: + # We don't know where the .aux file is until latex has run + return True + if not os.path.exists(jobname + '.aux'): + # Input isn't ready, so bibtex will simply fail without + # affecting system state. Hence, this task is trivially + # stable. + return True + if not self.__find_bib_cmds(os.path.dirname(jobname), jobname + '.aux'): + # The tex file doesn't refer to any bibliographic data, so + # don't run bibtex. + return True + + return super().stable() + + def __find_bib_cmds(self, basedir, auxname, stack=()): + debug('scanning for bib commands in {}'.format(auxname)) + if auxname in stack: + raise TaskError('.aux file loop') + stack = stack + (auxname,) + + try: + aux_data = open(auxname, errors='surrogateescape').read() + except FileNotFoundError: + # The aux file may not exist if latex aborted + return False + if re.search(r'^\\bibstyle\{', aux_data, flags=re.M) or \ + re.search(r'^\\bibdata\{', aux_data, flags=re.M): + return True + + if re.search(r'^\\abx@aux@cite\{', aux_data, flags=re.M): + # biber citation + return True + + # Recurse into included aux files (see aux_input_command), in + # case \bibliography appears in an \included file. + for m in re.finditer(r'^\\@input\{([^}]*)\}', aux_data, flags=re.M): + if self.__find_bib_cmds(basedir, os.path.join(basedir, m.group(1)), + stack): + return True + + return False + + def _input_args(self): + if self.__is_biber(): + aux_name = os.path.basename(self.__latex_task.get_jobname()) + else: + aux_name = os.path.basename(self.__latex_task.get_jobname()) + '.aux' + return [self.__cmd] + self.__cmd_args + [aux_name] + + def _input_cwd(self): + return os.path.dirname(self.__latex_task.get_jobname()) + + def _input_auxfile(self, auxname): + # We don't consider the .aux files regular inputs. + # Instead, we extract just the bit that BibTeX cares about + # and depend on that. See get_aux_command_and_process in + # bibtex.web. + debug('hashing filtered aux file {}', auxname) + try: + with open(auxname, 'rb') as aux: + h = hashlib.sha256() + for line in aux: + if line.startswith((b'\\citation{', b'\\bibdata{', + b'\\bibstyle{', b'\\@input{', + b'\\abx@aux@cite{')): + h.update(line) + return h.hexdigest() + except FileNotFoundError: + debug('{} does not exist', auxname) + return None + + def __path_join(self, first, rest): + if rest is None: + # Append ':' to keep the default search path + return first + ':' + return first + ':' + rest + + def __is_biber(self): + return "biber" in self.__cmd + + def _execute(self): + # This gets complicated when \include is involved. \include + # switches to a different aux file and records its path in the + # main aux file. However, BibTeX does not consider this path + # to be relative to the location of the main aux file, so we + # have to run BibTeX *in the output directory* for it to + # follow these includes (there's no way to tell BibTeX other + # locations to search). Unfortunately, this means BibTeX will + # no longer be able to find local bib or bst files, but so we + # tell it where to look by setting BIBINPUTS and BSTINPUTS + # (luckily we can control this search). We have to pass this + # same environment down to Kpathsea when we resolve the paths + # in BibTeX's log. + args, cwd = self._input('args'), self._input('cwd') + debug('running {} in {}', args, cwd) + + env = os.environ.copy() + env['BIBINPUTS'] = self.__path_join(os.getcwd(), env.get('BIBINPUTS')) + env['BSTINPUTS'] = self.__path_join(os.getcwd(), env.get('BSTINPUTS')) + + try: + verbose_cmd(args, cwd, env) + p = subprocess.Popen(args, cwd=cwd, env=env, + stdin=subprocess.DEVNULL, + stdout=subprocess.PIPE, + stderr=subprocess.STDOUT) + stdout = self.__feed_terminal(p.stdout) + status = p.wait() + except OSError as e: + raise TaskError('failed to execute bibtex task: ' + str(e)) from e + + inputs, auxnames, outbase = self.__parse_inputs(stdout, cwd, env) + if not inputs and not auxnames: + # BibTeX failed catastrophically. + print(stdout, file=sys.stderr) + raise TaskError('failed to execute bibtex task') + + # Register environment variable inputs + for env_var in ['TEXMFOUTPUT', 'BSTINPUTS', 'BIBINPUTS', 'PATH']: + self._input('env', env_var) + + # Register file inputs + for path in auxnames: + self._input('auxfile', path) + for path in inputs: + self._input('file', path) + + if self.__is_biber(): + outbase = os.path.join(cwd, outbase) + outputs = [outbase + '.bbl', outbase + '.blg'] + return RunResult(outputs, {'outbase': outbase, 'status': status, + 'inputs': inputs}) + + def __feed_terminal(self, stdout): + with Progress('bibtex') as progress: + buf, linebuf = [], '' + while True: + data = os.read(stdout.fileno(), 4096) + if not data: + break + # See "A note about encoding" above + data = data.decode('ascii', errors='surrogateescape') + buf.append(data) + linebuf += data + while '\n' in linebuf: + line, _, linebuf = linebuf.partition('\n') + if line.startswith('Database file'): + progress.update(line.split(': ', 1)[1]) + return ''.join(buf) + + def __parse_inputs(self, log, cwd, env): + # BibTeX conveniently logs every file that it opens, and its + # log is actually sensible (see calls to a_open_in in + # bibtex.web.) The only trick is that these file names are + # pre-kpathsea lookup and may be relative to the directory we + # ran BibTeX in. + # + # Because BibTeX actually depends on very little in the .aux + # file (and it's likely other things will change in the .aux + # file), we don't count the whole .aux file as an input, but + # instead depend only on the lines that matter to BibTeX. + kpathsea = Kpathsea('bibtex') + inputs = [] + auxnames = [] + outbase = None + for line in log.splitlines(): + m = re.match('(?:The top-level auxiliary file:' + '|A level-[0-9]+ auxiliary file:) (.*)', line) + if m: + auxnames.append(os.path.join(cwd, m.group(1))) + continue + m = re.match('(?:(The style file:)|(Database file #[0-9]+:)) (.*)', + line) + if m: + filename = m.group(3) + if m.group(1): + filename = kpathsea.find_file(filename, 'bst', cwd, env) + elif m.group(2): + filename = kpathsea.find_file(filename, 'bib', cwd, env) + + # If this path is relative to the source directory, + # clean it up for error reporting and portability of + # the dependency DB + if filename.startswith('/'): + relname = os.path.relpath(filename) + if '../' not in relname: + filename = relname + + inputs.append(filename) + + # biber output + m = re.search("Found BibTeX data source '(.*?)'", + line) + if m: + filename = m.group(1) + inputs.append(filename) + + m = re.search("Logfile is '(.*?)'", line) + if m: + outbase = m.group(1)[:-4] + + if outbase is None: + outbase = auxnames[0][:-4] + + return inputs, auxnames, outbase + + def report(self): + extra = self._get_result_extra() + if extra is None: + return 0 + + # Parse and pretty-print the log + log = open(extra['outbase'] + '.blg', 'rt').read() + inputs = extra['inputs'] + for msg in BibTeXFilter(log, inputs).get_messages(): + msg.emit() + + # BibTeX exits with 1 if there are warnings, 2 if there are + # errors, and 3 if there are fatal errors (sysdep.h). + # Translate to a normal UNIX exit status. + if extra['status'] >= 2: + return 1 + return 0 + +class BibTeXFilter: + def __init__(self, data, inputs): + self.__inputs = inputs + self.__key_locs = None + + self.__messages = [] + + prev_line = '' + for line in data.splitlines(): + msg = self.__process_line(prev_line, line) + if msg is not None: + self.__messages.append(Message(*msg)) + prev_line = line + + def get_messages(self): + """Return a list of warning and error Messages.""" + # BibTeX reports most errors in no particular order. Sort by + # file and line. + return sorted(self.__messages, + key=lambda msg: (msg.filename or '', msg.lineno or 0)) + + def __process_line(self, prev_line, line): + m = None + def match(regexp): + nonlocal m + m = re.match(regexp, line) + return m + + # BibTeX has many error paths, but luckily the set is closed, + # so we can find all of them. This first case is the + # workhorse format. + # + # AUX errors: aux_err/aux_err_return/aux_err_print + # + # BST errors: bst_ln_num_print/bst_err/ + # bst_err_print_and_look_for_blank_line_return/ + # bst_warn_print/bst_warn/ + # skip_token/skip_token_print/ + # bst_ext_warn/bst_ext_warn_print/ + # bst_ex_warn/bst_ex_warn_print/ + # bst_mild_ex_warn/bst_mild_ex_warn_print/ + # bst_string_size_exceeded + # + # BIB errors: bib_ln_num_print/ + # bib_err_print/bib_err/ + # bib_warn_print/bib_warn/ + # bib_one_of_two_expected_err/macro_name_warning/ + if match('(.*?)---?line ([0-9]+) of file (.*)'): + # Sometimes the real error is printed on the previous line + if m.group(1) == 'while executing': + # bst_ex_warn. The real message is on the previous line + text = prev_line + else: + text = m.group(1) or prev_line + typ, msg = self.__canonicalize(text) + return (typ, m.group(3), int(m.group(2)), msg) + + # overflow/print_overflow + if match('Sorry---you\'ve exceeded BibTeX\'s (.*)'): + return ('error', None, None, 'capacity exceeded: ' + m.group(1)) + # confusion/print_confusion + if match('(.*)---this can\'t happen$'): + return ('error', None, None, 'internal error: ' + m.group(1)) + # aux_end_err + if match('I found (no .*)---while reading file (.*)'): + return ('error', m.group(2), None, m.group(1)) + # bad_cross_reference_print/ + # nonexistent_cross_reference_error/ + # @ + # + # This is split across two lines. Match the second. + if match('^refers to entry "'): + typ, msg = self.__canonicalize(prev_line + ' ' + line) + msg = re.sub('^a (bad cross reference)', '\\1', msg) + # Try to give this key a location + filename = lineno = None + m2 = re.search(r'--entry "[^"]"', prev_line) + if m2: + filename, lineno = self.__find_key(m2.group(1)) + return (typ, filename, lineno, msg) + # print_missing_entry + if match('Warning--I didn\'t find a database entry for (".*")'): + return ('warning', None, None, + 'no database entry for ' + m.group(1)) + # x_warning + if match('Warning--(.*)'): + # Most formats give warnings about "something in ". + # Try to match it up. + filename = lineno = None + for m2 in reversed(list(re.finditer(r' in ([^, \t\n]+)\b', line))): + if m2: + filename, lineno = self.__find_key(m2.group(1)) + if filename: + break + return ('warning', filename, lineno, m.group(1)) + # @ + if match('Aborted at line ([0-9]+) of file (.*)'): + return ('info', m.group(2), int(m.group(1)), 'aborted') + + # biber type errors + if match('^.*> WARN - (.*)$'): + print ('warning', None, None, m.group(1)) + m2 = re.match("(.*) in file '(.*?)', skipping ...", m.group(1)) + if m2: + return ('warning', m2.group(2), "0", m2.group(1)) + return ('warning', None, None, m.group(1)) + + if match('^.*> ERROR - (.*)$'): + m2 = re.match("BibTeX subsystem: (.*?), line (\\d+), (.*)$", m.group(1)) + if m2: + return ('error', m2.group(1), m2.group(2), m2.group(3)) + return ('error', None, None, m.group(1)) + + + def __canonicalize(self, msg): + if msg.startswith('Warning'): + msg = re.sub('^Warning-*', '', msg) + typ = 'warning' + else: + typ = 'error' + msg = re.sub('^I(\'m| was)? ', '', msg) + msg = msg[:1].lower() + msg[1:] + return typ, msg + + def __find_key(self, key): + if self.__key_locs is None: + p = BibTeXKeyParser() + self.__key_locs = {} + for filename in self.__inputs: + data = open(filename, 'rt', errors='surrogateescape').read() + for pkey, lineno in p.parse(data): + self.__key_locs.setdefault(pkey, (filename, lineno)) + return self.__key_locs.get(key, (None, None)) + +class BibTeXKeyParser: + """Just enough of a BibTeX parser to find keys.""" + + def parse(self, data): + IDENT_RE = '(?![0-9])([^\x00-\x20\x80-\xff \t"#%\'(),={}]+)' + self.__pos, self.__data = 0, data + # Find the next entry + while self.__consume('[^@]*@[ \t\n]*'): + # What type of entry? + if not self.__consume(IDENT_RE + '[ \t\n]*'): + continue + typ = self.__m.group(1) + if typ == 'comment': + continue + start = self.__pos + if not self.__consume('([{(])[ \t\n]*'): + continue + closing, key_re = {'{' : ('}', '([^, \t\n}]*)'), + '(' : (')', '([^, \t\n]*)')}[self.__m.group(1)] + if typ not in ('preamble', 'string'): + # Regular entry; get key + if self.__consume(key_re): + yield self.__m.group(1), self.__lineno() + # Consume body of entry + self.__pos = start + self.__balanced(closing) + + def __consume(self, regexp): + self.__m = re.compile(regexp).match(self.__data, self.__pos) + if self.__m: + self.__pos = self.__m.end() + return self.__m + + def __lineno(self): + return self.__data.count('\n', 0, self.__pos) + 1 + + def __balanced(self, closing): + self.__pos += 1 + level = 0 + skip = re.compile('[{}' + closing + ']') + while True: + m = skip.search(self.__data, self.__pos) + if not m: + break + self.__pos = m.end() + ch = m.group(0) + if level == 0 and ch == closing: + break + elif ch == '{': + level += 1 + elif ch == '}': + level -= 1 + +class Kpathsea: + def __init__(self, program_name): + self.__progname = program_name + + def find_file(self, name, format, cwd=None, env=None): + """Return the resolved path of 'name' or None.""" + + args = ['kpsewhich', '-progname', self.__progname, '-format', format, + name] + try: + verbose_cmd(args, cwd, env) + path = subprocess.check_output( + args, cwd=cwd, env=env, universal_newlines=True).strip() + except subprocess.CalledProcessError as e: + if e.returncode != 1: + raise + return None + if cwd is None: + return path + return os.path.join(cwd, path) + +if __name__ == "__main__": + main() \ No newline at end of file diff --git a/listproc.sty b/listproc.sty new file mode 100644 index 0000000..5ad9ce9 --- /dev/null +++ b/listproc.sty @@ -0,0 +1,349 @@ +%% +%% This is file `listproc.sty', +%% generated with the docstrip utility. +%% +%% The original source files were: +%% +%% listproc.dtx (with options: `package') +%% +%% Copyright (C) 2011 by Jesse A. Tov +%% +%% This file may be distributed and/or modified under the conditions of the +%% LaTeX Project Public License, either version 1.2 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.2 or later is part of all distributions of LaTeX +%% version 1999/12/01 or later. +%% +\NeedsTeXFormat{LaTeX2e}[1999/12/01] +\ProvidesPackage{listproc}[2011/08/03 v0.2 (list processing)] +\newcommand\newlist{\@lstp@def{}\newcommand} +\newcommand\renewlist{\@lstp@def{}\renewcommand} +\newcommand\deflist{\@lstp@def{}\def} +\newcommand\gdeflist{\@lstp@def\global\def} +\newcommand\@lstp@def[4]{% + #2#3{}% + \@for\lstp@def@temp:=#4\do{% + \expandafter\SnocTo\expandafter{\lstp@def@temp}#3% + }% + #1\let#3#3% + \let\lstp@def@temp\@undefined +} +\newtoks\lstp@ta +\newtoks\lstp@tb +\newcommand\ConsTo{\@lstp@ConsTo\relax\def} +\newcommand\gConsTo{\@lstp@ConsTo\global\def} +\newcommand\eConsTo{\@lstp@ConsTo\relax\edef} +\newcommand\xConsTo{\@lstp@ConsTo\global\edef} +\newcommand\@lstp@ConsTo[4]{% + \long#2\lstp@temp{#3}% + \lstp@ta=\expandafter{\expandafter\listitem\expandafter{\lstp@temp}}% + \lstp@tb=\expandafter{#4}% + #1\edef#4{\the\lstp@ta\the\lstp@tb}% +} +\newcommand\SnocTo{\@lstp@SnocTo\relax\def} +\newcommand\gSnocTo{\@lstp@SnocTo\global\def} +\newcommand\eSnocTo{\@lstp@SnocTo\relax\edef} +\newcommand\xSnocTo{\@lstp@SnocTo\global\edef} +\newcommand\@lstp@SnocTo[4]{% + \long#2\lstp@temp{#3}% + \lstp@ta=\expandafter{\expandafter\listitem\expandafter{\lstp@temp}}% + \lstp@tb=\expandafter{#4}% + #1\edef#4{\the\lstp@tb\the\lstp@ta}% +} +\newcommand\AppendTo{\@lstp@AppendTo\relax} +\newcommand\gAppendTo{\@lstp@AppendTo\global} +\newcommand\@lstp@AppendTo[3]{% + \lstp@ta=\expandafter{#2}% + \lstp@tb=\expandafter{#3}% + #1\edef#3{\the\lstp@ta\the\lstp@tb}% +} +\long\def\@LopOff\listitem#1#2\@LopOff#3#4{% + #3{#1}% + #4{#2}% +} +\newcommand\@lstp@LopTo[4]{\expandafter\@LopOff#3\@LopOff{#1\def#4}{#2\def#3}} +\newcommand\@lstp@RestTo[3]{\expandafter\@LopOff#2\@LopOff{\@gobble}{#1\def#3}} +\newcommand\LopTo{\@lstp@LopTo\relax\relax} +\newcommand\gLopTo{\@lstp@LopTo\global\global} +\newcommand\glLopTo{\@lstp@LopTo\global\relax} +\newcommand\lgLopTo{\@lstp@LopTo\relax\global} +\newcommand\FirstTo{\@lstp@LopTo\relax\@gobblethree} +\newcommand\gFirstTo{\@lstp@LopTo\global\@gobblethree} +\newcommand\RestTo{\@lstp@RestTo\relax} +\newcommand\gRestTo{\@lstp@RestTo\global} +\newcommand*\IfList[1]{% + {% + \expandafter\@IfList#1\@IfList + }% +} +\def\@IfList#1#2\@IfList{% + \ifx\listitem#1\relax + \aftergroup\@firstoftwo + \else + \aftergroup\@secondoftwo + \fi +} +\def\@forList#1:=#2\do#3{% + \long\def\lstp@for@listitem##1{% + \long\def#1{##1}% + #3% + \let\listitem\lstp@for@listitem% + }% + \let\listitem\lstp@for@listitem% + #2% + \let\listitem\@undefined% +} +\newcommand\SetToListLength[2]{% + \lstp@length{#2}{\value{#1}}% +} +\newcommand\lstp@length[2]{% + #2=0 % + \long\def\listitem##1{\advance#2 by1 }% + #1\let\listitem\@undefined% +} +\newcommand\MapListTo{\@lstp@MapListTo\relax} +\newcommand\gMapListTo{\@lstp@MapListTo\global} +\newcommand\MapAndAppendTo{\@lstp@MapAndAppendTo\relax} +\newcommand\gMapAndAppendTo{\@lstp@MapAndAppendTo\global} +\newcommand\@lstp@MapListTo[4]{% + \let\lstp@map@temp#3% + #1\let#4\empty% + \@lstp@MapAndAppendTo{#1}{#2}\lstp@map@temp#4% + \let\lstp@map@temp\@undefined% +} +\newcommand\@lstp@MapAndAppendTo[4]{% + \long\def\listitem##1{\@lstp@SnocTo{#1}\def{#2}{#4}}% + #3% + \let\listitem\@undefined% +} +\newcommand\lstp@insert[3]{% + \edef\lstp@insert@temp@a{#2{#1}}% + \let\lstp@insert@temp@i#3% + \let#3\empty + \long\def\lstp@insert@listitem##1{% + \edef\lstp@insert@temp@b{#2{##1}}% + \ifnum\lstp@insert@temp@a<\lstp@insert@temp@b + \SnocTo{#1}{#3}% + \let\listitem\lstp@insert@listitem@done + \else + \let\listitem\lstp@insert@listitem + \fi + \SnocTo{##1}{#3}% + }% + \long\def\lstp@insert@listitem@done##1{\SnocTo{##1}{#3}}% + \let\listitem\lstp@insert@listitem + \lstp@insert@temp@i% + \ifx\listitem\lstp@insert@listitem% + \SnocTo{#1}{#3}% + \fi% + \let\lstp@insert@temp@i\@undefined% + \let\listitem\@undefined% +} +\providecommand\@apply@group[2]{#1#2} +\newcommand\SortList[2][\@apply@group{}]{% + \let\lstp@sort@temp@i#2% + \let#2\empty + \long\def\lstp@sort@listitem##1{% + \lstp@insert{##1}{#1}{#2}% + \let\listitem\lstp@sort@listitem + }% + \let\listitem\lstp@sort@listitem + \lstp@sort@temp@i + \let\lstp@sort@temp@i\@undefined + \let\listitem\@undefined +} +\newcounter{lstp@ifsucc} +\newcommand\lstp@ifsucc[2]{% + \setcounter{lstp@ifsucc}{#1}% + \addtocounter{lstp@ifsucc}{1}% + \ifnum#2=\value{lstp@ifsucc}% + \let\@lstp@ifsucc@kont\@firstoftwo + \else + \let\@lstp@ifsucc@kont\@secondoftwo + \fi + \@lstp@ifsucc@kont +} +\newcommand\CompressList[2][\@apply@group{}]{% + \let\lstp@compress@temp@i#2% + \let#2\empty + \def\lstp@compress@add@single{% + \expandafter\SnocTo\expandafter + {\expandafter\@single\expandafter{\lstp@compress@temp@a}}{#2}% + }% + \def\lstp@compress@add@range{% + \expandafter\expandafter\expandafter\SnocTo + \expandafter\expandafter\expandafter{% + \expandafter\expandafter\expandafter\@range + \expandafter\expandafter\expandafter{% + \expandafter\lstp@compress@temp@a\expandafter}% + \expandafter{\lstp@compress@temp@b}}#2% + }% + \long\def\lstp@compress@listitem@start##1{% + \def\lstp@compress@temp@a{##1}% + \edef\lstp@compress@temp@a@key{#1{##1}}% + \let\listitem\lstp@compress@listitem@single + }% + \long\def\lstp@compress@listitem@single##1{% + \def\lstp@compress@temp@b{##1}% + \edef\lstp@compress@temp@b@key{#1{##1}}% + \ifnum\lstp@compress@temp@a@key=\lstp@compress@temp@b@key + \let\listitem\lstp@compress@listitem@single + \else + \lstp@ifsucc{\lstp@compress@temp@a@key}{\lstp@compress@temp@b@key} + {\let\listitem\lstp@compress@listitem@range} + {\lstp@compress@add@single + \let\lstp@compress@temp@a\lstp@compress@temp@b + \let\lstp@compress@temp@a@key\lstp@compress@temp@b@key + \let\listitem\lstp@compress@listitem@single}% + \fi + }% + \long\def\lstp@compress@listitem@range##1{% + \def\lstp@compress@temp@c{##1}% + \edef\lstp@compress@temp@c@key{#1{##1}}% + \ifnum\lstp@compress@temp@b@key=\lstp@compress@temp@c@key + \let\listitem\lstp@compress@listitem@range + \else + \lstp@ifsucc{\lstp@compress@temp@b@key}{\lstp@compress@temp@c@key} + {% + \let\lstp@compress@temp@b\lstp@compress@temp@c + \let\lstp@compress@temp@b@key\lstp@compress@temp@c@key + \let\listitem\lstp@compress@listitem@range + } + {% + \lstp@compress@add@range + \let\lstp@compress@temp@a\lstp@compress@temp@c + \let\lstp@compress@temp@a@key\lstp@compress@temp@c@key + \let\listitem\lstp@compress@listitem@single + }% + \fi + }% + \let\listitem\lstp@compress@listitem@start + \lstp@compress@temp@i + \ifx\listitem\lstp@compress@listitem@single + \lstp@compress@add@single + \else + \ifx\listitem\lstp@compress@listitem@range + \lstp@compress@add@range + \fi + \fi + \let\lstp@compress@temp@a\@undefined + \let\lstp@compress@temp@b\@undefined + \let\lstp@compress@temp@c\@undefined + \let\lstp@compress@temp@a@key\@undefined + \let\lstp@compress@temp@b@key\@undefined + \let\lstp@compress@temp@c@key\@undefined + \let\lstp@compress@temp@i\@undefined + \let\listitem\@undefined +} +\newcommand\FormatListSepTwo{ and } +\newcommand\FormatListSepMore{, } +\newcommand\FormatListSepLast{, and } +\newcounter{lstp@FormatList@length} +\newcounter{lstp@FormatList@posn} +\newcommand\FormatList[4]{{% + \deflist\lstp@FormatList@list{#4}% + \SetToListLength{lstp@FormatList@length}\lstp@FormatList@list% + \setcounter{lstp@FormatList@posn}{0}% + \ifnum\value{lstp@FormatList@length}=1% + #1% + \else% + #2% + \fi% + \def\listitem##1{% + \addtocounter{lstp@FormatList@posn}{1}% + \ifnum1<\value{lstp@FormatList@posn}% + \ifnum2=\value{lstp@FormatList@length}% + \FormatListSepTwo + \else + \ifnum\value{lstp@FormatList@length}=\value{lstp@FormatList@posn}% + \FormatListSepLast + \else + \FormatListSepMore + \fi + \fi + \fi + #3{##1}% + }% + \lstp@FormatList@list +}} +\newcommand\ListExpr[1]{\@lstp@ListExpr{#1}\relax} +\newcommand\ListExprTo[2]{\@lstp@ListExpr{#1}{\def#2}} +\newcommand\gListExprTo[2]{\@lstp@ListExpr{#1}{\gdef#2}} +\newcommand\@lstp@defbinop[2]{% + \newcommand#1[2]{% + \Eval{##1}\let\@lstp@tmp\@lstp@acc + {\Eval{##2}}% + #2\@lstp@tmp\@lstp@acc + }% +} +\newcommand\@lstp@defunop[2]{% + \newcommand#1[1]{% + \Eval{##1}% + #2\@lstp@acc\@lstp@acc + }% +} +\newcommand\@lstp@definplaceunopopt[3][]{% + \newcommand#2[2][#1]{% + \Eval{##2}% + #3[##1]\@lstp@acc + \global\let\@lstp@acc\@lstp@acc + }% +} +\newcommand\@lstp@ListExpr[2]{% + {% + \gdef\@lstp@acc{}% + \def\Eval##1{% + \IfList{##1}{% + \global\let\@lstp@acc##1% + }{% + \@lstp@ifListOp##1\@lstp@ifListOp{% + ##1% + }{% + \xdef\@lstp@acc{##1}% + }% + }% + }% + \def\Q##1{\gdef\@lstp@acc{##1}}% + \def\Nil{\global\let\@lstp@acc\empty}% + \def\List##1{\gdeflist\@lstp@acc{##1}}% + \@lstp@defbinop\Cons\xConsTo + \@lstp@defbinop\Snoc\xSnocTo + \@lstp@defunop\First\gFirstTo + \@lstp@defunop\Rest\gRestTo + \@lstp@defbinop\Append\gAppendTo + \@lstp@definplaceunopopt[\@apply@group{}]\Sort\SortList + \@lstp@definplaceunopopt[\@apply@group{}]\Compress\CompressList + \newcommand\Map[2]{% + \Eval{##2}% + \gMapListTo{##1}\@lstp@acc\@lstp@acc + }% + \Eval{#1}% + }% + \def\@lstp@finish##1{#2{##1}}% + \expandafter\@lstp@finish\expandafter{\@lstp@acc}% +} +\def\@lstp@ifListOp#1#2\@lstp@ifListOp{% + \@lstp@ifInToks#1{ + \Q\Nil\List\Cons\Snoc\Append + \First\Rest\Sort\Compress\Map + } +} +\newcommand\@lstp@ifInToks[2]{% + {% + \def\@tester##1#1##2\@tester{% + \ifx\@notfound##2\relax + \aftergroup\@secondoftwo + \else + \aftergroup\@firstoftwo + \fi + }% + \@tester#2\@lstp@ifInToks#1\@notfound\@tester + }% +} +\endinput +%% +%% End of file `listproc.sty'. \ No newline at end of file diff --git a/ottalt.sty b/ottalt.sty new file mode 100644 index 0000000..d74d7e5 --- /dev/null +++ b/ottalt.sty @@ -0,0 +1,328 @@ +%% +%% This is file `ottalt.sty', +%% generated with the docstrip utility. +%% +%% The original source files were: +%% +%% ottalt.dtx (with options: `package') +%% +%% Copyright (C) 2011 by Jesse A. Tov +%% +%% This file may be distributed and/or modified under the conditions of the +%% LaTeX Project Public License, either version 1.2 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.2 or later is part of all distributions of LaTeX +%% version 1999/12/01 or later. +%% +\NeedsTeXFormat{LaTeX2e}[1999/12/01] +\ProvidesPackage{ottalt} + [2013/03/14 v0.11 alternate Ott layout style] +\RequirePackage{mathpartir} +\RequirePackage{ifthen} +\RequirePackage{keyval} +\RequirePackage{listproc} +\DeclareOption{implicitPremiseBreaks}{ + \renewcommand\ottaltpremisesep{\\} + \renewcommand\ottaltpremisebreak{\\} +} +\DeclareOption{lineBreakHack}{ + \renewcommand\ottaltpremisesep{\mpr@andcr} + \renewcommand\ottaltpremisebreak{\\\\} +} +\DeclareOption{implicitLineBreakHack}{ + \renewcommand\ottaltpremisesep{\\} + \renewcommand\ottaltpremisebreak{\\\\} +} +\DeclareOption{alternateNonterms}{ + \let\ifnotalternateNonterms\@secondoftwo +} +\DeclareOption{supertabular}{ + \ottalt@supertabulartrue +} +\newcommand\ottaltpremisesep{\\} +\newcommand\ottaltpremisebreak{\\} +\let\ifnotalternateNonterms\@firstoftwo +\newif\ifottalt@supertabular +\ProcessOptions +\ifottalt@supertabular + \RequirePackage{supertabular} +\fi +\newcommand\inputott[2][ott]{ + \input{#2} + \renewottcommands[#1] +} +\newcommand\ottaltcurrentprefix{ott} +\newcommand\renewottcommands[1][ott]{ + \renewcommand\ottaltcurrentprefix{#1} + \def\renewottcomm@nd##1{ + \expandafter\renewcommand\csname #1##1\endcsname + } + \renewottcomm@nd{drule}[4][]{ + \def\ottalt@nextpremise{} + \ottalt@premisetoks={ } + ##2 + \expandafter\ottalt@inferrule\expandafter + {\the\ottalt@premisetoks}{##3}{##4}{##1} + } + \renewottcomm@nd{premise}[1]{% + \ottalt@premisetoks= + \expandafter\expandafter\expandafter + {\expandafter\the\expandafter\ottalt@premisetoks + \ottalt@nextpremise##1} + \ottalt@iflinebreakhack##1\ottlinebreakhack\ottalt@iflinebreakhack{ + \let\ottalt@nextpremise\ottaltpremisebreak + }{ + \let\ottalt@nextpremise\ottaltpremisesep + } + } + \renewottcomm@nd{usedrule}[1]{% + \ifottalt@firstrule + \ottalt@firstrulefalse + \else + %\and + %% sigart.cls uses \and for the title and mangles it horribly + %% so we cannot use it here. Instead, we drop down to what + %% mathpartir wants to redefine the \and command to be anyways + \mpr@andcr + %%\quad + \fi + \ensuremath{##1} + } + \renewenvironment{#1defnblock}[3][] + {\begin{drulepar}{##2}{##3}} + {\end{drulepar}} + \renewottcomm@nd{drulename}[1]{% + \ottalt@replace@cs\ranchor\_-{}##1\\ + } + \renewottcomm@nd{prodline}[6]{ + \ifthenelse{\equal{##3}{}}{ + \\ & & $##1$ & $##2$ & & $##5$ & $##6$ + }{} + } + \renewottcomm@nd{prodnewline}{\relax} + \renewottcomm@nd{grammartabular}[1]{% + \begin{ottaltgrammar}##1\end{ottaltgrammar}% + } +} +\newcommand*\drule@h@lper[3]{% + \expandafter\ifx\csname\ottaltcurrentprefix drule#3\endcsname\relax + \PackageWarning{ottalt}{Unknown ott rule: #3}% + \mbox{\textbf{(#2?)}}% + \else + \csname\ottaltcurrentprefix usedrule\endcsname + {\csname\ottaltcurrentprefix drule#3\endcsname{#1}}% + \fi +} +\newcommand*\nonterm@h@lper[1]{\csname\ottaltcurrentprefix#1\endcsname} +\newcommand\rrefruletext{rule} +\newcommand\Rrefruletext{\expandafter\MakeUppercase\rrefruletext} +\newcommand\rrefrulestext{\rrefruletext s} +\newcommand\Rrefrulestext{\Rrefruletext s} +\newcommand\rrefstyle{\normalfont\scshape} +\newcommand\ranchorstyle{\rrefstyle} +\providecommand\wraparoundrref{\relax} +\newcommand*\rref{% + \@ifnextchar* + {\rref@star} + {\rref@with\rrefruletext\rrefrulestext}} +\newcommand*\Rref{% + \@ifnextchar* + {\rref@star} + {\rref@with\Rrefruletext\Rrefrulestext}} +\newcommand*\rref@with[2]{\FormatList{#1~}{#2~}{\one@rref}} +\newcommand*\rref@star[1]{\FormatList{}{}{\one@rref}} +\newcommand*\@one@rref@nohyper[1]{\wraparoundrref{{\rrefstyle{#1}}}} +\newcommand*\@ranchor@nohyper[1]{{\ranchorstyle{#1}}} +\AtBeginDocument{ + \ifcsname hypertarget\endcsname + \newcommand*\one@rref[1]{% + \hyperlink + {ottalt:rule:\ottaltcurrentprefix:#1} + {\@one@rref@nohyper{#1}}% + } + \newcommand*\ranchor[1]{% + \hypertarget + {ottalt:rule:\ottaltcurrentprefix:#1} + {\@ranchor@nohyper{#1}}% + } + \else + \newcommand\one@rref{\@one@rref@nohyper} + \newcommand\ranchor{\@ranchor@nohyper} + \fi +} +\newcommand*{\drules}[4][\relax]{% + \begin{drulepar}[#1]{#2}{#3} + \@for\@ottalt@each:=#4\do{% + \expandafter\drule\expandafter{\@ottalt@each} + } + \end{drulepar}% +} +\newenvironment{drulepar}[3][\relax] + {\begin{rulesection}[#1]{#2}{#3}% + \begin{mathparpagebreakable}} + {\end{mathparpagebreakable}% + \end{rulesection}} +\newenvironment{drulepar*}[3][\relax] + {\begin{rulesection*}[#1]{#2}{#3}% + \begin{mathparpagebreakable}} + {\end{mathparpagebreakable}% + \end{rulesection*}} +\newenvironment{rulesection}[3][\relax] + {\trivlist\item + \ifx#1\relax\else\def\ottalt@rulesection@prefix{#1-}\fi + \drulesectionhead{#2}{#3}% + \nopagebreak[4]% + \noindent} + {\endtrivlist} +\newenvironment{rulesection*}[3][\relax] + {\trivlist\item + \ifx#1\relax\else\def\ottalt@rulesection@prefix{#1-}\fi + \drulesectionhead*{#2}{#3}% + \nopagebreak[4]% + \noindent} + {\endtrivlist} +\newcommand\ottalt@rulesection@prefix{} +\newcommand*{\drulesectionhead}{% + \@ifnextchar *{\drulesectionheadMany}{\drulesectionheadOne}% +} +\newcommand*{\drulesectionheadOne}[2]{% + \FormatDruleSectionHead{#1}% + \hfill\FormatDruleSectionHeadRight{#2}% + \par +} +\newcommand*{\drulesectionheadMany}[3]{% + {% + \let\FormatListSepTwo\FormatDruleSepTwo + \let\FormatListSepMore\FormatDruleSepMore + \let\FormatListSepLast\FormatDruleSepLast + \FormatList{}{}{\FormatDruleSectionHeads}{#2}% + }% + \hfill\FormatDruleSectionHeadRight{#3}% + \par +} +\newcommand*\FormatDruleSepTwo{\,,~} +\newcommand*\FormatDruleSepMore{\FormatDruleSepTwo} +\newcommand*\FormatDruleSepLast{\FormatDruleSepTwo} +\newcommand*\FormatDruleSectionHead[1]{\fbox{#1}} +\newcommand*\FormatDruleSectionHeads[1]{\fbox{\strut#1}} +\newcommand*\FormatDruleSectionHeadRight[1]{\emph{#1}} +\newcommand*\drule[2][]{% + \expandafter\drule@helper\expandafter{\ottalt@rulesection@prefix}{#1}{#2}% +} +\newcommand*\drule@helper[3]{% + \ottalt@replace@cs{\drule@h@lper{#2}{#1#3}}-{XX}{}#1#3\\ +} +\newcommand\ottaltinferrule[4]{ + \inferrule*[narrower=0.3,lab=#1,#2] + {#3} + {#4} +} +\newcommand\ottalt@inferrule[4]{ + \ottaltinferrule{#3}{#4}{#1}{#2} +} +\newif\ifottalt@firstrule \ottalt@firstruletrue +\newcommand{\ottalt@nextpremise}{\relax} +\newtoks\ottalt@premisetoks +\newcommand{\ottlinebreakhack}{\relax} +\def\ottalt@iflinebreakhack#1\ottlinebreakhack #2\ottalt@iflinebreakhack{% + \ifthenelse{\equal{#2}{}}\@secondoftwo\@firstoftwo +} +\newcommand\ottalt@replace@cs[5]{% + \ifx\\#5\relax + \def\ottalt@replace@cs@kont{#1{#4}}% + \else + \ifx#2#5\relax + \def\ottalt@replace@cs@kont{\ottalt@replace@cs{#1}{#2}{#3}{#4#3}}% + \else + \def\ottalt@replace@cs@kont{\ottalt@replace@cs{#1}{#2}{#3}{#4#5}}% + \fi + \fi + \ottalt@replace@cs@kont +} +\newcommand*\nonterms[2][8pt]{ + \begin{ottaltgrammar}[#1] + \@for\@ottalt@each:=#2\do{% + \expandafter\nt\expandafter{\@ottalt@each} + } + \end{ottaltgrammar} +} +\newenvironment{ottaltgrammar}[1][8pt]{% + \begingroup + \trivlist\item + \def\OTTALTNEWLINE{\\[#1]}% + \def\nt##1{\OTTALTNEWLINE\relax\nonterm@h@lper{##1}\ignorespaces}% + \newcommand\ottaltintertext[2]{% + \multicolumn{8}{l}{% + \begin{minipage}{##1}% + ##2% + \end{minipage}% + }% + }% + \ifottalt@supertabular + \begin{supertabular}{llcllllll} + \else + \begin{tabular}{llcllllll} + \fi + \let\OTTALTNEWLINE\relax + \ignorespaces +} +{% + \@ifundefined{ottafterlastrule}{\\}{\ottafterlastrule}% + \ifottalt@supertabular + \end{supertabular} + \else + \end{tabular} + \fi + \endtrivlist + \endgroup + \ignorespaces +} +\newcommand\newNTclass[2][\ifnotalternateNonterms]{ + \expandafter\newcommand\csname new#2s\endcsname[4][]{ + #1{ + \expandafter\newcommand\csname ottalt@NT@#2@##2\endcsname{##1{##3}} + }{ + \expandafter\newcommand\csname ottalt@NT@#2@##2\endcsname{##4} + } + } + \expandafter\newcommand\csname new#2\endcsname[3][]{ + \csname new#2s\endcsname[##1]{##2}{##3}{##3} + } + \expandafter\newcommand\csname #2\endcsname[1]{% + \csname ottalt@NT@#2@##1\endcsname + } +} +\providecommand\@ifToif[1]{% + #1\iftrue\iffalse +} +\providecommand\ifTo@if[1]{% + #1% + \expandafter\@firstoftwo + \else + \expandafter\@secondoftwo + \fi +} +\newcommand\NTOVERLINE{\NTCAPTURE\overline} +\newcommand\NTUNDERLINE{\NTCAPTURE\underline} +\newcommand\NTTEXTCOLOR[1]{\NTCAPTURE{\textcolor{#1}}} +\newcommand\NTCAPTURE[1]{\NTCAPTURELOW{\NTCAPTURE@FINISH{#1}}} +\newcommand\NTCAPTURE@FINISH[4]{#1{#2_{#3}#4}} +\newcommand\NTCAPTURELOW[2]{\NT@CAPTURE@LOOP{#1}{#2}\relax\relax} +\newcommand\NT@CAPTURE@LOOP[4]{% + \@ifnextchar _{% + \NT@CAPTURE@SUB{#1}{#2}{#3}{#4}% + }{\@ifnextchar '{% + \NT@CAPTURE@PRIME{#1}{#2}{#3}{#4}% + }{% + {#1{#2}{#3}{#4}}% + }}% +} +\def\NT@CAPTURE@SUB#1#2#3#4_#5{\NT@CAPTURE@LOOP{#1}{#2}{#3#5}{#4}} +\def\NT@CAPTURE@PRIME#1#2#3#4'{\NT@CAPTURE@LOOP{#1}{#2}{#3}{#4'}} +\endinput +%% +%% End of file `ottalt.sty'. \ No newline at end of file diff --git a/rules.tex b/rules.tex new file mode 100644 index 0000000..6b13bb7 --- /dev/null +++ b/rules.tex @@ -0,0 +1,1273 @@ +% 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} +