Additions to fix-import (#497)

**Changes:**
- Sort by namespace first (i.e. `foundation` before `foundation-core`)
- Add line break between namespaces
- Remove repeat imports
- Remove redundant submodule imports if entire namespace is imported
- Remove `foundation-core` imports if the corresponding `foundation`
module is imported.

hooks/fix-imports.py

@@ -2,48 +2,79 @@
 # Run this script:
 # $ python3 hooks/fix-imports.py fileName.lagda.md
 
+from collections import defaultdict
 import sys
 import utils
 
 status = 0
 
+def normalize_imports(imports):
+    # Subdivide imports into namespaces
+    namespaces = defaultdict(set)
+    for statement in imports:
+        namespace_start = statement.index("open import") + len("open import") + 1
+        module = statement[namespace_start:]
+        try:
+            namespace = module[:module.rindex(".")]
+            namespaces[namespace].add(module)
+        except ValueError:
+            namespaces[module].add(module)
+
+    # If the entire namespace is imported, no further imports from that namespace are needed
+    for k in namespaces.keys():
+        if k in namespaces[k]:
+            namespaces[k] = {k}
+
+    for statement in namespaces["foundation"]:
+        submodule_start = statement.index(".")
+        namespaces["foundation-core"].discard("foundation-core" + statement[submodule_start:])
+
+    # Remove any namespaces that ended up being empty
+    namespaces = dict(filter(lambda kv: len(kv[1]) > 0, namespaces.items()))
+
+    # Join together with the appropriate line separations
+    blocks = ("\n".join(map(lambda module: "open import " + module, sorted(namespace_imports))) for namespace, namespace_imports in sorted(namespaces.items()))
+
+    return "\n\n".join(blocks)
+
 for fpath in utils.agdaFiles(sys.argv[1:]):
     with open(fpath, 'r', encoding='UTF-8') as file:
         contents = file.read()
         start = contents.find('<details>')
         end = contents.find('</details>')
         if start != -1 and end != -1:
             block = contents[start:end]
-            newBlock = filter(lambda l: l.strip() != '', block.split('\n'))
-            publicImports = []
-            nonPublicImports = []
-            otherStuff = []
+            # Strip all lines. There should not be any indentation in this block
+            newBlock = filter(lambda l: l != '', map(lambda l: l.strip(), block.split('\n')))
+
+            # Don't want repeat import statements
+            publicImports = set()
+            nonPublicImports = set()
+            openStatements = []
 
             for l in newBlock:
-                if l.startswith('```') or len(l.strip()) == 0:
+                if  len(l) == 0 or l.startswith('```') or '<details>' in l or '</details>' in l:
                     continue
                 if l.startswith('module') or l.startswith('{-# OPTIONS'):
                     print(
                         'Error: module decl./pragmas can not be in the details import block\n\
-                        Please put it in the first Agda block after the first header\n')
+                        Please put it in the first Agda block after the first header:\n\t' + str(fpath))
                     sys.exit(1)
                 elif 'open import' in l:
                     if l.endswith('public'):
-                        publicImports.append(l)
+                        publicImports.add(l)
                     else:
-                        nonPublicImports.append(l)
+                        nonPublicImports.add(l)
                 elif 'open' in l:
-                    otherStuff.append(l)
-
-            if len(otherStuff) > 0:
-
+                    openStatements.append(l)
+                else:
+                    print('Error: unknown statement in details import block:\n\t' + str(fpath))
+            if len(openStatements) > 0:
                 print(
-                    'Warning: Please review the imports block, it contains non-imports statements:\n\t' + str(fpath) )
-            imports = '\n'.join(
-                map(lambda ls: '\n'.join(sorted(ls)),
-                    filter(lambda ls: len(ls) > 0,
-                           [
-                        publicImports, nonPublicImports, otherStuff])))
+                    'Warning: Please review the imports block, it contains non-import statements:\n\t' + str(fpath))
+            imports = '\n\n'.join(
+                filter(lambda ls: len(ls) > 0,
+                    [normalize_imports(publicImports), normalize_imports(nonPublicImports), '\n'.join(sorted(openStatements))]))
 
             importBlock = '<details><summary>Imports</summary>\n' + \
                 '\n```agda\n' +\
@@ -56,8 +87,9 @@
             with open(fpath, 'w') as file:
                 file.write(newContent)
         else:
-            agdaBlockStart = utils.find_index(contents,'```agda')
+            agdaBlockStart = utils.find_index(contents, '```agda')
             if len(agdaBlockStart) > 1:
-                print('Warning: No Agda import block found inside <details> block in:\n\t' + str(fpath))
+                print(
+                    'Warning: No Agda import block found inside <details> block in:\n\t' + str(fpath))
                 status = 1
 sys.exit(status)

src/category-theory/adjunctions-large-precategories.lagda.md

@@ -8,9 +8,11 @@ module category-theory.adjunctions-large-precategories where
 
 ```agda
 open import Agda.Primitive using (Setω)
+
 open import category-theory.functors-large-precategories
 open import category-theory.large-precategories
 open import category-theory.natural-transformations-large-precategories
+
 open import foundation.commuting-squares-of-maps
 open import foundation.equivalences
 open import foundation.identity-types

src/category-theory/anafunctors.lagda.md

@@ -11,6 +11,7 @@ open import category-theory.categories
 open import category-theory.functors-precategories
 open import category-theory.isomorphisms-precategories
 open import category-theory.precategories
+
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.existential-quantification

src/category-theory/categories.lagda.md

@@ -9,6 +9,7 @@ module category-theory.categories where
 ```agda
 open import category-theory.isomorphisms-precategories
 open import category-theory.precategories
+
 open import foundation.1-types
 open import foundation.contractible-types
 open import foundation.dependent-pair-types

src/category-theory/coproducts-precategories.lagda.md

@@ -8,6 +8,7 @@ module category-theory.coproducts-precategories where
 
 ```agda
 open import category-theory.precategories
+
 open import foundation.cartesian-product-types
 open import foundation.contractible-types
 open import foundation.dependent-pair-types

src/category-theory/discrete-precategories.lagda.md

@@ -10,6 +10,7 @@ module category-theory.discrete-precategories where
 open import category-theory.functors-precategories
 open import category-theory.natural-transformations-precategories
 open import category-theory.precategories
+
 open import foundation.dependent-pair-types
 open import foundation.function-extensionality
 open import foundation.identity-types

src/category-theory/endomorphisms-of-objects-categories.lagda.md

@@ -8,10 +8,12 @@ module category-theory.endomorphisms-of-objects-categories where
 
 ```agda
 open import category-theory.categories
+
 open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.sets
 open import foundation.universe-levels
+
 open import group-theory.monoids
 open import group-theory.semigroups
 ```

src/category-theory/epimorphisms-large-precategories.lagda.md

@@ -9,6 +9,7 @@ module category-theory.epimorphisms-large-precategories where
 ```agda
 open import category-theory.isomorphisms-large-precategories
 open import category-theory.large-precategories
+
 open import foundation.embeddings
 open import foundation.equivalences
 open import foundation.identity-types

src/category-theory/equivalences-categories.lagda.md

@@ -10,6 +10,7 @@ module category-theory.equivalences-categories where
 open import category-theory.categories
 open import category-theory.equivalences-precategories
 open import category-theory.functors-categories
+
 open import foundation.universe-levels
 ```
 

src/category-theory/equivalences-large-precategories.lagda.md

@@ -8,9 +8,11 @@ module category-theory.equivalences-large-precategories where
 
 ```agda
 open import Agda.Primitive using (Setω)
+
 open import category-theory.functors-large-precategories
 open import category-theory.large-precategories
 open import category-theory.natural-isomorphisms-large-precategories
+
 open import foundation.universe-levels
 ```
 

src/category-theory/equivalences-precategories.lagda.md

@@ -10,6 +10,7 @@ module category-theory.equivalences-precategories where
 open import category-theory.functors-precategories
 open import category-theory.natural-isomorphisms-precategories
 open import category-theory.precategories
+
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.universe-levels

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

@@ -9,10 +9,12 @@ module category-theory.exponential-objects-precategories where
 ```agda
 open import category-theory.precategories
 open import category-theory.products-precategories
-open import foundation-core.identity-types
+
 open import foundation.dependent-pair-types
 open import foundation.unique-existence
 open import foundation.universe-levels
+
+open import foundation-core.identity-types
 ```
 
 </details>

src/category-theory/functors-categories.lagda.md

@@ -9,6 +9,7 @@ module category-theory.functors-categories where
 ```agda
 open import category-theory.categories
 open import category-theory.functors-precategories
+
 open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.universe-levels

src/category-theory/functors-large-precategories.lagda.md

@@ -8,7 +8,9 @@ module category-theory.functors-large-precategories where
 
 ```agda
 open import Agda.Primitive using (Setω)
+
 open import category-theory.large-precategories
+
 open import foundation.functions
 open import foundation.identity-types
 open import foundation.universe-levels

src/category-theory/functors-precategories.lagda.md

@@ -8,6 +8,7 @@ module category-theory.functors-precategories where
 
 ```agda
 open import category-theory.precategories
+
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.functions

src/category-theory/groupoids.lagda.md

@@ -14,6 +14,7 @@ open import category-theory.isomorphisms-categories
 open import category-theory.isomorphisms-precategories
 open import category-theory.precategories
 open import category-theory.pregroupoids
+
 open import foundation.1-types
 open import foundation.contractible-types
 open import foundation.dependent-pair-types

src/category-theory/homotopies-natural-transformations-large-precategories.lagda.md

@@ -8,9 +8,11 @@ module category-theory.homotopies-natural-transformations-large-precategories wh
 
 ```agda
 open import Agda.Primitive using (Setω)
+
 open import category-theory.functors-large-precategories
 open import category-theory.large-precategories
 open import category-theory.natural-transformations-large-precategories
+
 open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.universe-levels

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

@@ -8,10 +8,12 @@ module category-theory.initial-objects-precategories where
 
 ```agda
 open import category-theory.precategories
-open import foundation-core.identity-types
+
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.universe-levels
+
+open import foundation-core.identity-types
 ```
 
 </details>

src/category-theory/isomorphisms-categories.lagda.md

@@ -9,6 +9,7 @@ module category-theory.isomorphisms-categories where
 ```agda
 open import category-theory.categories
 open import category-theory.isomorphisms-precategories
+
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.equational-reasoning

src/category-theory/isomorphisms-large-precategories.lagda.md

@@ -8,6 +8,7 @@ module category-theory.isomorphisms-large-precategories where
 
 ```agda
 open import category-theory.large-precategories
+
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.identity-types

src/category-theory/isomorphisms-precategories.lagda.md

@@ -8,6 +8,7 @@ module category-theory.isomorphisms-precategories where
 
 ```agda
 open import category-theory.precategories
+
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.equational-reasoning

src/category-theory/large-categories.lagda.md

@@ -8,8 +8,10 @@ module category-theory.large-categories where
 
 ```agda
 open import Agda.Primitive using (Setω)
+
 open import category-theory.isomorphisms-large-precategories
 open import category-theory.large-precategories
+
 open import foundation.equivalences
 open import foundation.universe-levels
 ```

src/category-theory/large-precategories.lagda.md

@@ -8,6 +8,7 @@ module category-theory.large-precategories where
 
 ```agda
 open import Agda.Primitive using (Setω)
+
 open import foundation.functions
 open import foundation.identity-types
 open import foundation.sets

src/category-theory/monomorphisms-large-precategories.lagda.md

@@ -9,6 +9,7 @@ module category-theory.monomorphisms-large-precategories where
 ```agda
 open import category-theory.isomorphisms-large-precategories
 open import category-theory.large-precategories
+
 open import foundation.embeddings
 open import foundation.equivalences
 open import foundation.identity-types

src/category-theory/natural-isomorphisms-categories.lagda.md

@@ -11,6 +11,7 @@ open import category-theory.categories
 open import category-theory.functors-categories
 open import category-theory.natural-isomorphisms-precategories
 open import category-theory.natural-transformations-categories
+
 open import foundation.universe-levels
 ```
 

src/category-theory/natural-isomorphisms-large-precategories.lagda.md

@@ -11,6 +11,7 @@ open import category-theory.functors-large-precategories
 open import category-theory.isomorphisms-large-precategories
 open import category-theory.large-precategories
 open import category-theory.natural-transformations-large-precategories
+
 open import foundation.universe-levels
 ```
 

src/category-theory/natural-isomorphisms-precategories.lagda.md

@@ -11,6 +11,7 @@ open import category-theory.functors-precategories
 open import category-theory.isomorphisms-precategories
 open import category-theory.natural-transformations-precategories
 open import category-theory.precategories
+
 open import foundation.dependent-pair-types
 open import foundation.propositions
 open import foundation.universe-levels

src/category-theory/natural-numbers-object-precategories.lagda.md

@@ -9,6 +9,7 @@ module category-theory.natural-numbers-object-precategories where
 ```agda
 open import category-theory.precategories
 open import category-theory.terminal-objects-precategories
+
 open import foundation.cartesian-product-types
 open import foundation.dependent-pair-types
 open import foundation.identity-types

src/category-theory/natural-transformations-categories.lagda.md

@@ -10,6 +10,7 @@ module category-theory.natural-transformations-categories where
 open import category-theory.categories
 open import category-theory.functors-categories
 open import category-theory.natural-transformations-precategories
+
 open import foundation.universe-levels
 ```
 

src/category-theory/natural-transformations-large-precategories.lagda.md

@@ -9,6 +9,7 @@ module category-theory.natural-transformations-large-precategories where
 ```agda
 open import category-theory.functors-large-precategories
 open import category-theory.large-precategories
+
 open import foundation.identity-types
 open import foundation.universe-levels
 ```

src/category-theory/natural-transformations-precategories.lagda.md

@@ -9,6 +9,7 @@ module category-theory.natural-transformations-precategories where
 ```agda
 open import category-theory.functors-precategories
 open import category-theory.precategories
+
 open import foundation.dependent-pair-types
 open import foundation.embeddings
 open import foundation.equational-reasoning

src/category-theory/precategory-of-functors.lagda.md

@@ -10,6 +10,7 @@ module category-theory.precategory-of-functors where
 open import category-theory.functors-precategories
 open import category-theory.natural-transformations-precategories
 open import category-theory.precategories
+
 open import foundation.dependent-pair-types
 open import foundation.embeddings
 open import foundation.equational-reasoning

src/category-theory/pregroupoids.lagda.md

@@ -9,6 +9,7 @@ module category-theory.pregroupoids where
 ```agda
 open import category-theory.isomorphisms-precategories
 open import category-theory.precategories
+
 open import foundation.dependent-pair-types
 open import foundation.propositions
 open import foundation.universe-levels