Migrate to coderefs labels

Author: v--

packages/coderefs.sty

@@ -21,11 +21,16 @@
       }
   }
 
-\NewDocumentCommand \WriteCodeRef {m}
+\NewDocumentCommand \WriteCodeRefText {m}
   {
     \\[1ex]
     \hbox{\quad}
-    \texttt{\GetCodeRef{#1}}
+    \texttt{#1}
+  }
+
+\NewDocumentCommand \WriteCodeRef {m}
+  {
+    \WriteCodeRefText{\GetCodeRef{#1}}
   }
 
 \ExplSyntaxOff

src/notebook/commands/watcher/command.py

@@ -32,6 +32,7 @@ async def iter_build_file_changes(logger: loguru.Logger) -> AsyncIterator[TaskTr
         inotify.add_watch(ROOT_PATH / 'bibliography', MASK)
         inotify.add_watch(ROOT_PATH / 'asymptote', MASK)
         inotify.add_watch(ROOT_PATH / 'classes', MASK)
+        inotify.add_watch(ROOT_PATH / 'aux', MASK)
         inotify.add_watch(ROOT_PATH / 'output', MASK)
         logger.info('Started daemon and initialized watchers')
 
@@ -89,6 +90,7 @@ async def setup_watchers(manager: TaskRunner, base_logger: loguru.Logger, *, reb
                 path.match('bibliography/*.bib') or
                 path.match('text/*.tex') or
                 path.match('images/*') or
+                path.match('aux/coderefs.tex') or
                 (path.match('output/*') and not path.match('output/notebook.pdf')) or
                 path.match('packages/*.sty')
             ):

src/notebook/math/lambda_/hol/evaluation.py

@@ -4,6 +4,7 @@
 from typing import TYPE_CHECKING
 
 from ....exceptions import UnreachableException
+from ....support.coderefs import collector
 from ..alphabet import BinaryTypeConnective
 from ..assertions import VariableTypeAssertion
 from ..terms import Constant, TypedAbstraction, TypedApplication, TypedTerm, Variable
@@ -131,6 +132,7 @@ def evaluate_hol_term[T](  # noqa: C901
     raise UnreachableException
 
 
+@collector.ref('alg:hol_denotation')
 def evaluate_hol_expression[T](
     expression: HolExpression,
     structure: HolStructure[T],

src/notebook/math/lambda_/signature_translation.py

@@ -31,7 +31,7 @@ def visit_connective(self, type_: SimpleConnectiveType) -> SimpleConnectiveType:
         )
 
 
-@collector.ref('alg:fol_formula_signature_translation')
+@collector.ref('alg:simple_type_signature_translation')
 def translate_type(translation: SignatureMorphism, type_: SimpleType) -> SimpleType:
     return TypeTranslationVisitor(translation).visit(type_)
 
@@ -68,6 +68,6 @@ def visit_abstraction(self, term: TypedAbstraction) -> TypedAbstraction:
         )
 
 
-@collector.ref('alg:fol_term_signature_translation')
+@collector.ref('alg:simply_typed_term_signature_translation')
 def translate_term(translation: SignatureMorphism, term: TypedTerm) -> TypedTerm:
     return TermTranslationVisitor(translation).visit(term)

text/boolean_functions.tex

@@ -113,7 +113,8 @@ \section{Boolean functions}\label{sec:boolean_functions}
   \end{thmenum}
 \end{algorithm}
 \begin{comments}
-  \item This algorithm can be found as \identifier{math.polynomials.zhegalkin.infer_zhegalkin} in \cite{notebook:code}.
+  \item This algorithm is implemented in \cite{notebook:code} as
+    \WriteCodeRef{alg:infer_zhegalkin_polynomial}
 \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

@@ -651,7 +651,8 @@ \section{Curry-Howard correspondence}\label{sec:curry_howard_correspondence}
   \end{thmenum}
 \end{algorithm}
 \begin{comments}
-  \item This algorithm can be found as \identifier{math.lambda_.curry_howard.derivation_to_proof.type_derivation_to_proof_tree} in \cite{notebook:code}.
+  \item This algorithm is implemented in \cite{notebook:code} as
+    \WriteCodeRef{alg:type_derivation_to_proof_tree}
 
   \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}
@@ -683,7 +684,8 @@ \section{Curry-Howard correspondence}\label{sec:curry_howard_correspondence}
   \end{thmenum}
 \end{algorithm}
 \begin{comments}
-  \item This algorithm can be found as \identifier{math.lambda_.curry_howard.proof_to_derivation.proof_tree_to_type_derivation} in \cite{notebook:code}.
+  \item This algorithm is implemented in \cite{notebook:code} as
+    \WriteCodeRef{alg:proof_tree_to_type_derivation}
 \end{comments}
 
 \begin{example}\label{ex:con:curry_howard_correspondence}

text/digit_based_operations.tex

@@ -49,7 +49,8 @@ \section{Digit-based operations}\label{sec:digit_based_operations}
   \end{thmenum}
 \end{algorithm}
 \begin{comments}
-  \item This algorithm can be found as \identifier{math.arithmetic.bases.get_integer_expansion} in \cite{notebook:code}.
+  \item This algorithm is implemented in \cite{notebook:code} as
+    \WriteCodeRef{alg:integer_radix_expansion}
 \end{comments}
 
 \paragraph{Digit-based integer arithmetic}
@@ -98,7 +99,8 @@ \section{Digit-based operations}\label{sec:digit_based_operations}
 \end{algorithm}
 \begin{comments}
   \item The term \( q_k \) \enquote{carries} either \( -1 \), \( 0 \) or \( 1 \) to be used in the next step.
-  \item This algorithm can be found as \identifier{math.arithmetic.bases.add_with_carrying} in \cite{notebook:code}.
+  \item This algorithm is implemented in \cite{notebook:code} as
+    \WriteCodeRef{alg:addition_with_carrying}
 \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
@@ -243,7 +245,8 @@ \section{Digit-based operations}\label{sec:digit_based_operations}
   \end{thmenum}
 \end{algorithm}
 \begin{comments}
-  \item This algorithm can be found as \identifier{math.arithmetic.bases.single_digit_mult_with_carrying} in \cite{notebook:code}.
+  \item This algorithm is implemented in \cite{notebook:code} as
+    \WriteCodeRef{alg:single_digit_multiplication_with_carrying}
 \end{comments}
 \begin{defproof}
   The proof of correctness is similar, but much simpler than that of \fullref{alg:integer_radix_expansion}.
@@ -355,7 +358,8 @@ \section{Digit-based operations}\label{sec:digit_based_operations}
   \end{thmenum}
 \end{algorithm}
 \begin{comments}
-  \item This algorithm can be found as \identifier{math.arithmetic.bases.multi_digit_mult_with_carrying} in \cite{notebook:code}.
+  \item This algorithm is implemented in \cite{notebook:code} as
+    \WriteCodeRef{alg:multi_digit_multiplication_with_carrying}
 \end{comments}
 
 \begin{algorithm}[Long division]\label{alg:long_division}
@@ -418,7 +422,8 @@ \section{Digit-based operations}\label{sec:digit_based_operations}
   \end{thmenum}
 \end{algorithm}
 \begin{comments}
-  \item This algorithm can be found as \identifier{math.arithmetic.bases.long_integer_division} in \cite{notebook:code}.
+  \item This algorithm is implemented in \cite{notebook:code} as
+    \WriteCodeRef{alg:long_division}
 \end{comments}
 \begin{defproof}
   The guard steps \fullref{alg:long_division/n_guard} and \fullref{alg:long_division/m_guard} allow us to assume that \( n \geq 0 \) and \( m \geq 0 \).

text/first_order_logic.tex

@@ -227,7 +227,8 @@ \section{First-order logic}\label{sec:first_order_logic}
 \end{algorithm}
 \begin{comments}
   \item As discussed in \cref{rem:fol_application_notation}, we allow translation to change the notation of symbols.
-  \item This algorithm can be found as \identifier{math.logic.signature_translation.translate_term} in \cite{notebook:code}.
+  \item This algorithm is implemented in \cite{notebook:code} as
+    \WriteCodeRef{alg:fol_term_signature_translation}
 \end{comments}
 
 \paragraph{First-order formulas}
@@ -374,7 +375,8 @@ \section{First-order logic}\label{sec:first_order_logic}
 \begin{comments}
   \item As discussed in \cref{rem:fol_application_notation}, we allow exchanging prefix and infix symbols.
 
-  \item This algorithm can be found as \identifier{math.logic.signature_translation.translate_formula} in \cite{notebook:code}.
+  \item This algorithm is implemented in \cite{notebook:code} as
+    \WriteCodeRef{alg:fol_formula_signature_translation}
 \end{comments}
 
 \paragraph{Variable binding}
@@ -874,7 +876,8 @@ \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 can be found as \identifier{math.logic.propositional.apply_prop_formula_translation} in \cite{notebook:code}.
+  \item This algorithm is implemented in \cite{notebook:code} as
+    \WriteCodeRef{alg:fol_propositional_formula_translation}
 \end{comments}
 
 \begin{proposition}\label{thm:fol_propositional_formula_translation_semantics}

text/first_order_natural_deduction.tex

@@ -16,7 +16,8 @@ \section{First-order natural deduction}\label{sec:first_order_natural_deduction}
   where \( n = \sharp(\op*{Free}_\Bbbs(\varphi)) \).
 \end{algorithm}
 \begin{comments}
-  \item This algorithm can be found as \identifier{math.logic.substitution.apply_substitution_to_formula} in \cite{notebook:code}.
+  \item This algorithm is implemented in \cite{notebook:code} as
+    \WriteCodeRef{alg:fol_formula_substitution}
   \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}
 
@@ -433,7 +434,8 @@ \section{First-order natural deduction}\label{sec:first_order_natural_deduction}
 \end{algorithm}
 \begin{comments}
   \item Of course, an application of an instantiation is only valid if the placeholders are in its domain.
-  \item This algorithm can be found as \identifier{math.logic.instantiation.instantiate_term_schema} in \cite{notebook:code}.
+  \item This algorithm is implemented in \cite{notebook:code} as
+    \WriteCodeRef{alg:fol_term_schema_instantiation}
 \end{comments}
 
 \begin{algorithm}[First-order formula instantiation]\label{alg:fol_formula_schema_instantiation}
@@ -458,7 +460,8 @@ \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 can be found as \identifier{math.logic.instantiation.instantiate_substitution} in \cite{notebook:code}.
+  \item This algorithm is implemented in \cite{notebook:code} as
+    \WriteCodeRef{alg:fol_formula_schema_instantiation}
 \end{comments}
 
 \paragraph{Abstract natural deduction}
@@ -671,7 +674,8 @@ \section{First-order natural deduction}\label{sec:first_order_natural_deduction}
 \begin{comments}
   \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 can be found as \identifier{math.logic.propositional.apply_prop_proof_tree_translation} in \cite{notebook:code}.
+  \item This algorithm is implemented in \cite{notebook:code} as
+    \WriteCodeRef{alg:fol_propositional_proof_tree_translation}
 \end{comments}
 
 \paragraph{Concrete natural deduction}

text/first_order_theories.tex

@@ -981,7 +981,11 @@ \section{First-order theories}\label{sec:first_order_theories}
   \end{thmenum}
 \end{algorithm}
 \begin{comments}
-  \item This algorithm can be found as \identifier{math.logic.skolemization.formula_to_prenex_form} in \cite{notebook:code}. The bulk of the implementation is in the module \identifier{math.logic.transformation.pull_quantifiers}.
+  \item This algorithm is implemented in \cite{notebook:code} as
+    \WriteCodeRef{alg:fol_formula_to_prenex_normal_form}
+
+  The bulk of the implementation is in the module
+    \WriteCodeRefText{math.logic.transformation.pull_quantifiers}
 \end{comments}
 \begin{defproof}
   We can use induction on the \hyperref[def:graph_cardinality/order]{graph order} of the \hyperref[def:fol_formula_ast]{abstract syntax tree} of \( \varphi \) to show that \( M_{\logic{PNF}}(\varphi) \) is in prenex normal form. This is straightforward because, in every operation, we recursively \enquote{pull} quantifiers outwards.
@@ -1092,7 +1096,8 @@ \section{First-order theories}\label{sec:first_order_theories}
 \begin{comments}
   \item The overall premise of Skolemization is described in \cref{rem:definitional_extensions_and_skolemization} and \cref{thm:skolemization_equisatisfiability} (the latter leading to \fullref{thm:skolems_theorem}).
   \item There are two sources of ambiguity in the algorithm --- the choice of Skolem function symbols and the choice of the functions themselves. The disambiguation that we may find useful depends on the situation.
-  \item This algorithm can be found as \identifier{math.logic.skolemization.skolemize} in \cite{notebook:code}.
+  \item This algorithm is implemented in \cite{notebook:code} as
+    \WriteCodeRef{alg:fol_skolemization}
 \end{comments}
 
 \begin{proposition}\label{thm:skolemization_equisatisfiability}