Use environment-based coderefs

Author: v--

packages/coderefs.sty

@@ -21,23 +21,9 @@
       }
   }
 
-\cs_new_protected:Nn \nb_coderef_write:n
+\NewDocumentCommand \ManualCodeRef {v}
   {
-    \begin{displayquote}
-      \small
-      \texttt{#1}
-      \normalsize
-    \end{displayquote}
-  }
-
-\NewDocumentCommand \WriteCodeRefText {v}
-  {
-    \nb_coderef_write:n {#1}
-  }
-
-\NewDocumentCommand \WriteCodeRef {m}
-  {
-    \nb_coderef_write:n {\GetCodeRef{#1}}
+    #1
   }
 
 \NewDocumentEnvironment {CodeRefDisplay} {}

text/binomial_coefficients.tex

@@ -430,7 +430,9 @@ \section{Binomial coefficients}\label{sec:binomial_coefficients}
 \end{definition}
 \begin{comments}
   \item These matrices are implemented in \cite{notebook:code}, in the module
-    \WriteCodeRefText{combinatorics.binomial}
+  \begin{CodeRefDisplay}
+    \ManualCodeRef{combinatorics.binomial}
+  \end{CodeRefDisplay}
 \end{comments}
 
 \begin{example}\label{ex:con:pascals_triangle}

text/boolean_functions.tex

@@ -114,7 +114,9 @@ \section{Boolean functions}\label{sec:boolean_functions}
 \end{algorithm}
 \begin{comments}
   \item This algorithm is implemented in \cite{notebook:code} as
-    \WriteCodeRef{alg:infer_zhegalkin_polynomial}
+  \begin{CodeRefDisplay}
+    \GetCodeRef{alg:infer_zhegalkin_polynomial}
+  \end{CodeRefDisplay}
 \end{comments}
 \begin{defproof}
   We will prove correctness by induction. The base case \( n = 0 \) is vacuous, so suppose that \( n > 0 \) and that the algorithm is correct for less than \( n \) variables.

text/curry_howard_correspondence.tex

@@ -652,7 +652,9 @@ \section{Curry-Howard correspondence}\label{sec:curry_howard_correspondence}
 \end{algorithm}
 \begin{comments}
   \item This algorithm is implemented in \cite{notebook:code} as
-    \WriteCodeRef{alg:type_derivation_to_proof_tree}
+  \begin{CodeRefDisplay}
+    \GetCodeRef{alg:type_derivation_to_proof_tree}
+  \end{CodeRefDisplay}
 
   \item When restricted to arrow types, this algorithm works just as well for \hyperref[def:lambda_term]{untyped} or even \hyperref[rem:mixed_lambda_term]{mixed} \( \muplambda \)-terms.
 \end{comments}
@@ -685,7 +687,9 @@ \section{Curry-Howard correspondence}\label{sec:curry_howard_correspondence}
 \end{algorithm}
 \begin{comments}
   \item This algorithm is implemented in \cite{notebook:code} as
-    \WriteCodeRef{alg:proof_tree_to_type_derivation}
+  \begin{CodeRefDisplay}
+    \GetCodeRef{alg:proof_tree_to_type_derivation}
+  \end{CodeRefDisplay}
 \end{comments}
 
 \begin{example}\label{ex:con:curry_howard_correspondence}

text/digit_based_operations.tex

@@ -50,7 +50,9 @@ \section{Digit-based operations}\label{sec:digit_based_operations}
 \end{algorithm}
 \begin{comments}
   \item This algorithm is implemented in \cite{notebook:code} as
-    \WriteCodeRef{alg:integer_radix_expansion}
+  \begin{CodeRefDisplay}
+    \GetCodeRef{alg:integer_radix_expansion}
+  \end{CodeRefDisplay}
 \end{comments}
 
 \paragraph{Digit-based integer arithmetic}
@@ -100,7 +102,9 @@ \section{Digit-based operations}\label{sec:digit_based_operations}
 \begin{comments}
   \item The term \( q_k \) \enquote{carries} either \( -1 \), \( 0 \) or \( 1 \) to be used in the next step.
   \item This algorithm is implemented in \cite{notebook:code} as
-    \WriteCodeRef{alg:addition_with_carrying}
+  \begin{CodeRefDisplay}
+    \GetCodeRef{alg:addition_with_carrying}
+  \end{CodeRefDisplay}
 \end{comments}
 \begin{defproof}
   \SubProof{Proof that \( q_k \) is either \( -1 \), \( 0 \) or \( 1 \)} We will show by induction on \( k \) that \( q_k \) is either \( -1 \), \( 0 \) or \( 1 \). Note that, since \( b \geq 2 \), we have
@@ -246,7 +250,9 @@ \section{Digit-based operations}\label{sec:digit_based_operations}
 \end{algorithm}
 \begin{comments}
   \item This algorithm is implemented in \cite{notebook:code} as
-    \WriteCodeRef{alg:single_digit_multiplication_with_carrying}
+  \begin{CodeRefDisplay}
+    \GetCodeRef{alg:single_digit_multiplication_with_carrying}
+  \end{CodeRefDisplay}
 \end{comments}
 \begin{defproof}
   The proof of correctness is similar, but much simpler than that of \fullref{alg:integer_radix_expansion}.
@@ -359,7 +365,9 @@ \section{Digit-based operations}\label{sec:digit_based_operations}
 \end{algorithm}
 \begin{comments}
   \item This algorithm is implemented in \cite{notebook:code} as
-    \WriteCodeRef{alg:multi_digit_multiplication_with_carrying}
+  \begin{CodeRefDisplay}
+    \GetCodeRef{alg:multi_digit_multiplication_with_carrying}
+  \end{CodeRefDisplay}
 \end{comments}
 
 \begin{algorithm}[Long division]\label{alg:long_integer_division}
@@ -423,7 +431,9 @@ \section{Digit-based operations}\label{sec:digit_based_operations}
 \end{algorithm}
 \begin{comments}
   \item This algorithm is implemented in \cite{notebook:code} as
-    \WriteCodeRef{alg:long_integer_division}
+  \begin{CodeRefDisplay}
+    \GetCodeRef{alg:long_integer_division}
+  \end{CodeRefDisplay}
 \end{comments}
 \begin{defproof}
   The guard steps \fullref{alg:long_integer_division/n_guard} and \fullref{alg:long_integer_division/m_guard} allow us to assume that \( n \geq 0 \) and \( m \geq 0 \).

text/first_order_logic.tex

@@ -133,10 +133,14 @@ \section{First-order logic}\label{sec:first_order_logic}
   \item We implicitly associate with each propositional formula an \hyperref[con:abstract_syntax_tree]{abstract syntax tree} --- see \cref{def:fol_term_ast}. The grammar of first-order terms is unambiguous as shown via \cref{thm:fol_term_grammar/unambiguous}, which makes it possible to perform proofs via \fullref{thm:induction_on_abstract_syntax}.
 
   \item First-order terms are implemented in \cite{notebook:code}, in the module
-    \WriteCodeRefText{logic.terms}
+  \begin{CodeRefDisplay}
+    \ManualCodeRef{logic.terms}
+  \end{CodeRefDisplay}
 
   A parser is implemented in
-    \WriteCodeRefText{logic.parsing}
+  \begin{CodeRefDisplay}
+    \ManualCodeRef{logic.parsing}
+  \end{CodeRefDisplay}
 \end{comments}
 
 \begin{remark}\label{rem:fol_application_notation}
@@ -232,7 +236,9 @@ \section{First-order logic}\label{sec:first_order_logic}
 \begin{comments}
   \item As discussed in \cref{rem:fol_application_notation}, we allow translation to change the notation of symbols.
   \item This algorithm is implemented in \cite{notebook:code} as
-    \WriteCodeRef{alg:fol_term_signature_translation}
+  \begin{CodeRefDisplay}
+    \GetCodeRef{alg:fol_term_signature_translation}
+  \end{CodeRefDisplay}
 \end{comments}
 
 \paragraph{First-order formulas}
@@ -267,10 +273,14 @@ \section{First-order logic}\label{sec:first_order_logic}
   \item Within the metalanguage, we will denote abstract formulas via \( \varphi \), \( \psi \), \( \theta \) and other letters in accordance with \cref{rem:mathematical_logic_conventions/greek_alphabet}. This convention will later lead us to a formal definition of formula schemas in \cref{def:fol_formula_schema}.
 
   \item First-order formulas are implemented in \cite{notebook:code}, in the module
-    \WriteCodeRefText{logic.formulas}
+  \begin{CodeRefDisplay}
+    \ManualCodeRef{logic.formulas}
+  \end{CodeRefDisplay}
 
   A parser is implemented in
-    \WriteCodeRefText{logic.parsing}
+  \begin{CodeRefDisplay}
+    \ManualCodeRef{logic.parsing}
+  \end{CodeRefDisplay}
 \end{comments}
 
 \begin{proposition}\label{thm:fol_formula_grammar}
@@ -384,7 +394,9 @@ \section{First-order logic}\label{sec:first_order_logic}
   \item As discussed in \cref{rem:fol_application_notation}, we allow exchanging prefix and infix symbols.
 
   \item This algorithm is implemented in \cite{notebook:code} as
-    \WriteCodeRef{alg:fol_formula_signature_translation}
+  \begin{CodeRefDisplay}
+    \GetCodeRef{alg:fol_formula_signature_translation}
+  \end{CodeRefDisplay}
 \end{comments}
 
 \paragraph{Variable binding}
@@ -545,7 +557,9 @@ \section{First-order logic}\label{sec:first_order_logic}
   \item The term \enquote{denotation} is inspired by Russell's theory of denotations discussed in \cref{con:denotation}. It is used inconsistently in the literature. See \cref{rem:model_theory_structure_terminology}.
 
   \item This algorithm is implemented in \cite{notebook:code} as
-    \WriteCodeRef{alg:fol_term_denotation}
+  \begin{CodeRefDisplay}
+    \GetCodeRef{alg:fol_term_denotation}
+  \end{CodeRefDisplay}
 \end{comments}
 
 \begin{definition}\label{def:fol_parameterized_term_denotation}
@@ -614,7 +628,9 @@ \section{First-order logic}\label{sec:first_order_logic}
   \item The term \enquote{denotation} is inspired by Russell's theory of denotations discussed in \cref{con:denotation}. It is used inconsistently in the literature. See \cref{rem:model_theory_structure_terminology}.
 
   \item This algorithm is implemented in \cite{notebook:code} as
-    \WriteCodeRef{alg:fol_formula_denotation}
+  \begin{CodeRefDisplay}
+    \GetCodeRef{alg:fol_formula_denotation}
+  \end{CodeRefDisplay}
 \end{comments}
 
 \begin{remark}\label{rem:fol_empty_universe/semantics}
@@ -715,7 +731,9 @@ \section{First-order logic}\label{sec:first_order_logic}
 \end{definition}
 \begin{comments}
   \item Structures are implemented in \cite{notebook:code}, in the module
-    \WriteCodeRefText{logic.structure}
+  \begin{CodeRefDisplay}
+    \ManualCodeRef{logic.structure}
+  \end{CodeRefDisplay}
 
   \item The definition is based on \bycite[def. 2.6.3]{Hinman2005Logic}, with small adjustments made for the intuitionistic treatment of formal equality.
 \end{comments}
@@ -734,7 +752,9 @@ \section{First-order logic}\label{sec:first_order_logic}
   \item Reducts are also compatible with \hyperref[def:fol_theory/morphism]{theory morphisms} --- see \cref{thm:def:fol_theory/theory_morphism_reduct}.
 
   \item Reducts are implemented in \cite{notebook:code}, in the module
-    \WriteCodeRefText{logic.structure.reduct}
+  \begin{CodeRefDisplay}
+    \ManualCodeRef{logic.structure.reduct}
+  \end{CodeRefDisplay}
 \end{comments}
 
 \begin{proposition}\label{thm:fol_structure_reduct_denotation}
@@ -890,7 +910,9 @@ \section{First-order logic}\label{sec:first_order_logic}
   \item Of course, this extension will only be valid when the propositional variables are in the domain of the atomic translation map.
 
   \item This algorithm is implemented in \cite{notebook:code} as
-    \WriteCodeRef{alg:fol_propositional_formula_translation}
+  \begin{CodeRefDisplay}
+    \GetCodeRef{alg:fol_propositional_formula_translation}
+  \end{CodeRefDisplay}
 \end{comments}
 
 \begin{proposition}\label{thm:fol_propositional_formula_translation_semantics}
@@ -940,7 +962,9 @@ \section{First-order logic}\label{sec:first_order_logic}
 \end{remark}
 \begin{comments}
   \item This is the approach we have used to implement propositional logic in \cite{notebook:code}, in the module
-    \WriteCodeRefText{logic.propositional}
+  \begin{CodeRefDisplay}
+    \ManualCodeRef{logic.propositional}
+  \end{CodeRefDisplay}
 \end{comments}
 
 \paragraph{Quantifier duality}
@@ -955,7 +979,9 @@ \section{First-order logic}\label{sec:first_order_logic}
 \end{algorithm}
 \begin{comments}
   \item This algorithm is implemented in \cite{notebook:code} as
-    \WriteCodeRef{alg:fol_formula_dualization}
+  \begin{CodeRefDisplay}
+    \GetCodeRef{alg:fol_formula_dualization}
+  \end{CodeRefDisplay}
 \end{comments}
 \begin{defproof}
   We will use \fullref{thm:induction_on_abstract_syntax} on \( \varphi \) to show that \( \Bracks{\oline{M}(\varphi)}_\mscrX^v = \oline{\Bracks{\varphi}_\mscrX^v} \) for every variable assignment \( v \) in every structure \( \mscrX = (X, I) \).

text/first_order_natural_deduction.tex

@@ -17,7 +17,9 @@ \section{First-order natural deduction}\label{sec:first_order_natural_deduction}
 \end{algorithm}
 \begin{comments}
   \item This algorithm is implemented in \cite{notebook:code} as
-    \WriteCodeRef{alg:fol_formula_substitution}
+  \begin{CodeRefDisplay}
+    \GetCodeRef{alg:fol_formula_substitution}
+  \end{CodeRefDisplay}
 
   \item This substitution is defined as to have the properties listed in \cref{rem:variable_binding_properties}; we elaborate on this in \fullref{thm:alg:fol_formula_substitution}.
 \end{comments}
@@ -394,7 +396,9 @@ \section{First-order natural deduction}\label{sec:first_order_natural_deduction}
 \end{definition}
 \begin{comments}
   \item Term schemas are implemented in \cite{notebook:code}, in the module
-    \WriteCodeRefText{logic.terms}
+  \begin{CodeRefDisplay}
+    \ManualCodeRef{logic.terms}
+  \end{CodeRefDisplay}
 \end{comments}
 
 \begin{definition}\label{def:fol_formula_schema}\mimprovised
@@ -418,7 +422,9 @@ \section{First-order natural deduction}\label{sec:first_order_natural_deduction}
   \item Small Greek identifiers are used for both term and formula placeholders, but in practice they do not cause confusion.
   \item First-order formula schemas directly extend their \hyperref[def:propositional_formula_schema]{propositional counterparts}.
   \item Formulas schemas are implemented in \cite{notebook:code}, in the module
-    \WriteCodeRefText{logic.formulas}
+  \begin{CodeRefDisplay}
+    \ManualCodeRef{logic.formulas}
+  \end{CodeRefDisplay}
 \end{comments}
 
 \begin{definition}\label{def:atomic_fol_instantiation}\mimprovised
@@ -438,7 +444,9 @@ \section{First-order natural deduction}\label{sec:first_order_natural_deduction}
 \begin{comments}
   \item Of course, an application of an instantiation is only valid if the placeholders are in its domain.
   \item This algorithm is implemented in \cite{notebook:code} as
-    \WriteCodeRef{alg:fol_term_schema_instantiation}
+  \begin{CodeRefDisplay}
+    \GetCodeRef{alg:fol_term_schema_instantiation}
+  \end{CodeRefDisplay}
 \end{comments}
 
 \begin{algorithm}[First-order formula instantiation]\label{alg:fol_formula_schema_instantiation}
@@ -464,7 +472,9 @@ \section{First-order natural deduction}\label{sec:first_order_natural_deduction}
   \item A variant of this algorithm, in which certain instantiations are considered invalid, is presented in \cref{rem:sequent_calculus_eigenvariables}.
 
   \item This algorithm is implemented in \cite{notebook:code} as
-    \WriteCodeRef{alg:fol_formula_schema_instantiation}
+  \begin{CodeRefDisplay}
+    \GetCodeRef{alg:fol_formula_schema_instantiation}
+  \end{CodeRefDisplay}
 \end{comments}
 
 \paragraph{Abstract natural deduction}
@@ -530,7 +540,9 @@ \section{First-order natural deduction}\label{sec:first_order_natural_deduction}
     Fix an \hyperref[def:atomic_fol_instantiation]{atomic schema instantiation} \( \BbbI \) and a list \( (P_1, \ldots, P_n) \) of proof trees such that, for \( i = 1, \ldots, n \), the conclusion of \( P_k \) is \( \Phi_k[\BbbI] \). As in the propositional case, for a suitable choice \( d \) of dischargeable assumptions, we have a unique rule application tree \( P_d \).
 
     Describing the eigenvariables of \( P_d \) requires additional coherence conditions. They are enforced programmatically in \cite{notebook:code}, in the function
-      \WriteCodeRef{def:fol_natural_deduction_proof_tree}
+    \begin{CodeDefDisplay}
+      \GetCodeRef{def:fol_natural_deduction_proof_tree}
+    \end{CodeDefDisplay}
 
     We also describe some of them below:
     \begin{thmenum}[series=def:fol_natural_deduction_proof_tree/application]
@@ -598,7 +610,9 @@ \section{First-order natural deduction}\label{sec:first_order_natural_deduction}
   Gentzen presents only two rules featuring eigenvariables, in which the variables must satisfy slightly differing constraints. We formalize Gentzen's rules in \cref{def:fol_natural_deduction} and adapt them for \hyperref[def:higher_order_logic]{higher-order logic} in \cref{def:hol_natural_deduction}.
 
   \item Natural deduction proof trees are implemented in \cite{notebook:code}, in the module
-    \WriteCodeRefText{logic.deduction}
+  \begin{CodeRefDisplay}
+    \ManualCodeRef{logic.deduction}
+  \end{CodeRefDisplay}
 \end{comments}
 
 \begin{proposition}\label{thm:def:fol_natural_deduction_proof_tree}
@@ -682,7 +696,9 @@ \section{First-order natural deduction}\label{sec:first_order_natural_deduction}
   \item We will use this algorithm to show compatibility of propositional and first-order derivation relations in \cref{thm:fol_propositional_formula_translation_entailment}.
 
   \item This algorithm is implemented in \cite{notebook:code} as
-    \WriteCodeRef{alg:fol_propositional_proof_tree_translation}
+  \begin{CodeRefDisplay}
+    \GetCodeRef{alg:fol_propositional_proof_tree_translation}
+  \end{CodeRefDisplay}
 \end{comments}
 
 \paragraph{Concrete natural deduction}
@@ -771,7 +787,9 @@ \section{First-order natural deduction}\label{sec:first_order_natural_deduction}
   \item The two equality rules are more concise and flexible, but less explicit than those from \cref{thm:fol_natural_deduction_equality}.
 
   \item These precise rules are used in \cite{notebook:code}, in the module
-    \WriteCodeRefText{logic.classical_logic}
+  \begin{CodeRefDisplay}
+    \ManualCodeRef{logic.classical_logic}
+  \end{CodeRefDisplay}
 \end{comments}
 
 \begin{example}\label{ex:def:fol_natural_deduction}
@@ -903,7 +921,9 @@ \section{First-order natural deduction}\label{sec:first_order_natural_deduction}
 \end{example}
 \begin{comments}
   \item Many of these examples are verified programmatically in \cite{notebook:code}, in the module
-    \WriteCodeRefText{logic.deduction.test_proof_tree}
+  \begin{CodeRefDisplay}
+    \ManualCodeRef{logic.deduction.test_proof_tree}
+  \end{CodeRefDisplay}
 \end{comments}
 
 \begin{remark}\label{rem:dependent_products_and_forall_quantifier_rules}