Generate module indexes (#501)

Automatically generate both namespace index modules and the main index
file (meaning the long list in `SUMMARY.md`) as part of `pre-commit`.

The namespace index modules are generated by
- Create a file if it does not exist
- If there is no title, use the namespace but capitalize the first word
and replace dashes with spaces. E.g. `orthogonal-factorization-systems`
becomes "Orthogonal factorization systems"
- If there is no Agda-block, create one, otherwise, capture the last
Agda block in the file. (this is to preserve possible `OPTION` pragmas
as in the case of `type-theories`.
- Declare the namespace module, and import all files in the namespace
folder publically and in alphabetic ordering.

This assures that if there is a custom title or other text in the
namespace index module from before (as in the case of
`univalent-combinatorics`), then this is preserved.

The main index file is generated as follows
- Overwrite the previous file
- Add title "Formalisation in Agda"
- Add entry lists for each namespace. The title of a module is used for
the entry, and the lists are sorted by title as well.

Resolves #448. 

Written in collaboration with @jonaprieto.

---------

Co-authored-by: Jonathan Cubides <jonaprieto@users.noreply.github.com>

.pre-commit-config.yaml

@@ -35,6 +35,27 @@ repos:
       args: []
       require_serial: false
 
+    - id: generate-namespace-index-modules
+      name: Generate Agda namespace index modules
+      entry: hooks/generate_namespace_index_modules.py
+      language: python
+      always_run: true
+      verbose: true
+      types_or: [markdown, text]
+      args: []
+      require_serial: false
+
+    - id: generate-main-index-file
+      name: Generate main index file
+      entry: hooks/generate_main_index_file.py
+      language: python
+      always_run: true
+      verbose: true
+      types_or: [markdown, text]
+      args: []
+      require_serial: false
+
+
 # - repo: https://github.com/pre-commit/mirrors-prettier
 #   rev: "v3.0.0-alpha.6"
 #   hooks:

hooks/generate_main_index_file.py

@@ -0,0 +1,79 @@
+#!/usr/bin/env python3
+# Run this script:
+# $ python3 hooks/generate_main_index_file.py
+
+import os
+import sys
+import utils
+
+STATUS_FLAG_NO_TITLE = 1
+STATUS_FLAG_DUPLICATE_TITLE = 2
+
+entry_template = '- [{title}]({mdfile})'
+
+def generate_namespace_entry_list(namespace):
+    status = 0
+    modules = sorted(os.listdir(os.path.join(root, namespace)))
+    module_titles = tuple(map(lambda m: utils.get_lagda_file_title(
+        os.path.join(root, namespace, m)), modules))
+    module_mdfiles = tuple(
+        map(lambda m: utils.get_module_mdfile(namespace, m), modules))
+
+    # Check for missing titles
+    for title, module in zip(module_titles, modules):
+        if title is None:
+            status |= STATUS_FLAG_NO_TITLE
+            print(f"WARNING! {namespace}.{module} no title was found")
+
+    # Check duplicate titles
+    equal_titles = utils.get_equivalence_classes(
+        lambda tf1, tf2: tf1[0] == tf2[0], zip(module_titles, modules))
+    equal_titles = tuple(filter(lambda ec: len(
+        ec) > 1 and ec[0][0] is not None, equal_titles))
+
+    if (len(equal_titles) > 0):
+        status |= STATUS_FLAG_DUPLICATE_TITLE
+        print(f"WARNING! Duplicate titles in {namespace}:")
+        for ec in equal_titles:
+            print(
+                f"  Title '{ec[0][0]}': {', '.join(m[1][:m.rfind('.lagda.md')] for m in ec)}")
+
+    module_titles_and_mdfiles = sorted(
+        zip(module_titles, module_mdfiles), key=lambda tm: (tm[0].casefold(), tm[1]))
+
+    entry_list = ('  ' + entry_template.format(title=t, mdfile=md)
+                  for t, md in module_titles_and_mdfiles)
+
+    namespace_title = utils.get_lagda_file_title(
+        os.path.join(root, namespace) + ".lagda.md")
+    namespace_entry = entry_template.format(
+        title=namespace_title, mdfile=namespace + ".md")
+
+    namespace_entry_list = namespace_entry + "\n" + "\n".join(entry_list)
+    return namespace_entry_list, status
+
+def generate_index(root, header):
+    status = 0
+    entry_lists = []
+    for namespace in sorted(utils.get_subdirectories_recursive(root)):
+        entry_list, s = generate_namespace_entry_list(namespace)
+        entry_lists.append(entry_list)
+        status |= s
+
+    index = f"{header}\n\n" + "\n\n".join(entry_lists) + "\n"
+    return index, status
+
+if __name__ == "__main__":
+
+    status = 0
+    root = "src"
+
+    index_path = "MODULE-INDEX.md"
+    index_header = "# Formalisation in Agda"
+
+    index_content, status = generate_index(root, index_header)
+
+    with open(index_path, "w") as index_file:
+        index_file.write(index_content)
+
+    sys.exit(status)

hooks/generate_namespace_index_modules.py

@@ -0,0 +1,79 @@
+#!/usr/bin/env python3
+# Run this script:
+# $ python3 hooks/generate_namespace_index_modules.py
+
+import os
+import pathlib
+import sys
+import utils
+
+def generate_title(namespace):
+    return "# " + namespace.capitalize().replace("-", " ") + "\n"
+
+def generate_imports(root, namespace):
+    namespace_path = os.path.join(root, namespace)
+    agda_file_filter = lambda f: utils.isAgdaFile(pathlib.Path(os.path.join(namespace_path, f)))
+    namespace_files = filter(agda_file_filter, os.listdir(namespace_path))
+
+    import_statements = (utils.get_import_statement(namespace, module_file, public=True) for module_file in namespace_files)
+    return "\n".join(sorted(import_statements))
+
+agda_block_template = \
+    '''```agda
+module {namespace} where
+
+{imports}
+```
+'''
+
+def generate_agda_block(root, namespace):
+    return agda_block_template.format(namespace=namespace, imports=generate_imports(root, namespace))
+
+if __name__ == "__main__":
+
+    status = 0
+    root = "src"
+
+    for namespace in utils.get_subdirectories_recursive(root):
+        namespace_filename = os.path.join(root, namespace) + ".lagda.md"
+        with open(namespace_filename, "a+") as namespace_file:
+            pass
+        with open(namespace_filename, "r+") as namespace_file:
+            contents = namespace_file.read()
+
+        oldcontents = contents
+
+        title_index = contents.find("# ")
+        if title_index > 0:
+            print(
+                f"Warning! Namespace file {namespace_filename} has title after first line.")
+        elif title_index == -1:  # Missing title. Generate it
+            contents = generate_title(namespace) + contents
+
+        agda_block_start = contents.rfind("```agda\n")
+
+        if agda_block_start == -1:
+            # Must add agda block
+            # Add at the end of the file
+            contents += "\n" + generate_agda_block(root, namespace)
+        else:
+            agda_block_end = contents.find(
+                "\n```\n", agda_block_start + len("```agda\n"))
+            generated_block = generate_agda_block(root, namespace)
+
+            if agda_block_end == -1:
+                # An agda block is opened but not closed.
+                # This is an error, but we can fix it
+                print(
+                    f"WARNING! agda-block was opened but not closed in {namespace_filename}.")
+                contents = contents[:agda_block_start] + generated_block
+            else:
+                agda_block_end += len("\n```\n")
+                contents = contents[:agda_block_start] + generated_block + contents[agda_block_end:]
+
+        if oldcontents != contents:
+            status |= 1
+            with open(namespace_filename, "w") as f:
+                f.write(contents)
+
+    sys.exit(status)

hooks/utils.py

@@ -1,7 +1,8 @@
 import pathlib as path
+import os
 
 def find_index(s : str, t : str) -> list[int]:
-    return [p for p, c in  enumerate(s) if c == t]
+    return [p for p, c in enumerate(s) if c == t]
 
 def isAgdaFile(f: path.Path) -> bool:
     return (f.match('*.lagda.md') and
@@ -11,3 +12,35 @@ def isAgdaFile(f: path.Path) -> bool:
 def agdaFiles(files: list[str]) -> list[path.Path]:
     return list(filter(isAgdaFile,
                        map(path.Path, files)))
+
+def get_subdirectories_recursive(startpath):
+    for root, dirs, files in os.walk(startpath):
+        yield from dirs
+
+def get_lagda_file_title(lagda_filepath):
+    with open(lagda_filepath, "r") as file:
+        contents = file.read()
+        title_index = contents.find("# ")
+        if title_index != 0:
+            return None
+
+        title_start = title_index + len("# ")
+        title_end = contents.find("\n", len("# "))
+        return contents[title_start:title_end]
+
+def get_import_statement(namespace, module_file, public=False):
+    return f"open import {namespace}.{module_file[:module_file.rfind('.lagda.md')]}{' public' * public}"
+
+def get_module_mdfile(namespace, module_file):
+    return namespace + "." + module_file.replace(".lagda.md", ".md")
+
+def get_equivalence_classes(equivalence_relation, iterable):
+    partitions = []  # Found partitions
+    for e in iterable:  # Loop over each element
+        for p in partitions:
+            if equivalence_relation(e, p[0]):  # Found a partition for it!
+                p.append(e)
+                break
+        else: # Make a new partition for it.
+            partitions.append([e])
+    return partitions

src/category-theory.lagda.md

@@ -9,6 +9,7 @@ open import category-theory.categories public
 open import category-theory.coproducts-precategories public
 open import category-theory.discrete-precategories public
 open import category-theory.endomorphisms-of-objects-categories public
+open import category-theory.epimorphisms-large-precategories public
 open import category-theory.equivalences-categories public
 open import category-theory.equivalences-large-precategories public
 open import category-theory.equivalences-precategories public

src/category-theory/exponential-objects-precategories.lagda.md

@@ -1,4 +1,4 @@
-# Products in precategories
+# Exponential objects in precategories
 
 ```agda
 module category-theory.exponential-objects-precategories where

src/elementary-number-theory.lagda.md

@@ -20,6 +20,7 @@ open import elementary-number-theory.commutative-ring-of-integers public
 open import elementary-number-theory.commutative-semiring-of-natural-numbers public
 open import elementary-number-theory.congruence-integers public
 open import elementary-number-theory.congruence-natural-numbers public
+open import elementary-number-theory.decidable-dependent-function-types public
 open import elementary-number-theory.decidable-types public
 open import elementary-number-theory.difference-integers public
 open import elementary-number-theory.dirichlet-convolution public
@@ -33,11 +34,13 @@ open import elementary-number-theory.equality-integers public
 open import elementary-number-theory.equality-natural-numbers public
 open import elementary-number-theory.euclidean-division-natural-numbers public
 open import elementary-number-theory.eulers-totient-function public
+open import elementary-number-theory.exponentiation-natural-numbers public
 open import elementary-number-theory.factorials public
 open import elementary-number-theory.falling-factorials public
 open import elementary-number-theory.fibonacci-sequence public
 open import elementary-number-theory.finitary-natural-numbers public
 open import elementary-number-theory.finitely-cyclic-maps public
+open import elementary-number-theory.fractions public
 open import elementary-number-theory.goldbach-conjecture public
 open import elementary-number-theory.greatest-common-divisor-integers public
 open import elementary-number-theory.greatest-common-divisor-natural-numbers public
@@ -50,13 +53,14 @@ open import elementary-number-theory.inequality-standard-finite-types public
 open import elementary-number-theory.infinitude-of-primes public
 open import elementary-number-theory.integer-partitions public
 open import elementary-number-theory.integers public
+open import elementary-number-theory.lower-bounds-natural-numbers public
 open import elementary-number-theory.maximum-natural-numbers public
 open import elementary-number-theory.maximum-standard-finite-types public
 open import elementary-number-theory.mersenne-primes public
 open import elementary-number-theory.minimum-natural-numbers public
 open import elementary-number-theory.minimum-standard-finite-types public
-open import elementary-number-theory.modular-arithmetic-standard-finite-types public
 open import elementary-number-theory.modular-arithmetic public
+open import elementary-number-theory.modular-arithmetic-standard-finite-types public
 open import elementary-number-theory.multiplication-integers public
 open import elementary-number-theory.multiplication-natural-numbers public
 open import elementary-number-theory.multiset-coefficients public
@@ -76,11 +80,14 @@ open import elementary-number-theory.retracts-of-natural-numbers public
 open import elementary-number-theory.square-free-natural-numbers public
 open import elementary-number-theory.stirling-numbers-of-the-second-kind public
 open import elementary-number-theory.strong-induction-natural-numbers public
+open import elementary-number-theory.sums-of-natural-numbers public
 open import elementary-number-theory.telephone-numbers public
 open import elementary-number-theory.triangular-numbers public
 open import elementary-number-theory.twin-prime-conjecture public
 open import elementary-number-theory.unit-elements-standard-finite-types public
 open import elementary-number-theory.unit-similarity-standard-finite-types public
 open import elementary-number-theory.universal-property-natural-numbers public
+open import elementary-number-theory.upper-bounds-natural-numbers public
 open import elementary-number-theory.well-ordering-principle-natural-numbers public
 open import elementary-number-theory.well-ordering-principle-standard-finite-types public
+```

src/finite-group-theory.lagda.md

@@ -2,6 +2,7 @@
 
 ```agda
 module finite-group-theory where
+
 open import finite-group-theory.abstract-quaternion-group public
 open import finite-group-theory.alternating-concrete-groups public
 open import finite-group-theory.alternating-groups public

src/foundation-core.lagda.md

@@ -31,6 +31,7 @@ open import foundation-core.equality-cartesian-product-types public
 open import foundation-core.equality-dependent-pair-types public
 open import foundation-core.equality-fibers-of-maps public
 open import foundation-core.equivalence-induction public
+open import foundation-core.equivalence-relations public
 open import foundation-core.equivalences public
 open import foundation-core.faithful-maps public
 open import foundation-core.fibers-of-maps public