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} +