[ refactor ] Clean up the dependency graph (agda#1435)

* [ refactor ] Clean up the dependency graph

Author: gallais

.gitignore

@@ -5,6 +5,7 @@
 *.hi
 *.lagda.el
 *.o
+*.svg
 *.tix
 *.vim
 *~

CHANGELOG.md

@@ -6,6 +6,10 @@ The library has been tested using Agda 2.6.1 and 2.6.1.1.
 Highlights
 ----------
 
+* Drastically reorganised the module hierarchy in the dependency graph of
+  the `IO` module so that we may compile a program as simple as hello world
+  without pulling upwards of 130 modules.
+
 * First verified implementation of a sorting algorithm (available from `Data.List.Sort`).
 
 Bug-fixes
@@ -14,6 +18,16 @@ Bug-fixes
 Non-backwards compatible changes
 --------------------------------
 
+* `Data.List.Relation.Binary.Lex.Core` has been thinned to minimise its
+  dependencies. The more complex properties (`transitive`, `respects₂`,
+  `[]<[]-⇔`, `∷<∷-⇔`, and `decidable`) have been moved to
+  `Data.List.Relation.Binary.Lex`.
+
+* `Data.String.Base` has been thinned to minimise its dependencies. The more
+  complex functions (`parensIfSpace`, `wordsBy`, `words`, `linesBy`, `lines`,
+  `rectangle`, `rectangleˡ`, `rectangleʳ`, `rectangleᶜ`) have been moved to
+  `Data.String`.
+
 Deprecated modules
 ------------------
 
@@ -116,6 +130,30 @@ New modules
   Data.Nat.PseudoRandom.LCG
   ```
 
+* Broke up `Data.List.Relation.Binary.Pointwise` and introduced:
+  ```
+  Data.List.Relation.Binary.Pointwise.Base
+  Data.List.Relation.Binary.Pointwise.Properties
+  ```
+
+* Broke up `Codata.Musical.Colist` into a multitude of modules:
+  ```
+  Codata.Musical.Colist.Base
+  Codata.Musical.Colist.Properties
+  Codata.Musical.Colist.Bisimilarity
+  Codata.Musical.Colist.Relation.Unary.All
+  Codata.Musical.Colist.Relation.Unary.All.Properties
+  Codata.Musical.Colist.Relation.Unary.Any
+  Codata.Musical.Colist.Relation.Unary.Any.Properties
+  ```
+
+* Broke up `IO` into a many smaller modules:
+  ```
+  IO.Base
+  IO.Finite
+  IO.Infinite
+  ```
+
 * Instantiate a homogeneously indexed bundle at a particular index
   ```
   Relation.Binary.Indexed.Homogeneous.Construct.At
@@ -130,6 +168,11 @@ New modules
 Other minor additions
 ---------------------
 
+* Added new function in `Data.Char.Base`:
+  ```agda
+  _≈ᵇ_ : (c d : Char) → Bool
+  ```
+
 * Added new proofs in `Algebra.Morphism.GroupMonomorphism`:
   ```agda
   ⁻¹-distrib-∙ : ((x ◦ y) ⁻¹₂ ≈₂ (x ⁻¹₂) ◦ (y ⁻¹₂)) → ((x ∙ y) ⁻¹₁ ≈₁ (x ⁻¹₁) ∙ (y ⁻¹₁))
@@ -370,7 +413,7 @@ Other minor additions
 
 * Added new proofs to `Data.List.Relation.Binary.Pointwise`:
   ```agda
-  foldr⁺  : (R w x → R y z → R (w • y) (x ◦ z)) → 
+  foldr⁺  : (R w x → R y z → R (w • y) (x ◦ z)) →
             R e f → Pointwise R xs ys → R (foldr _•_ e xs) (foldr _◦_ f ys)
   lookup⁻ : length xs ≡ length ys →
             (toℕ i ≡ toℕ j → R (lookup xs i) (lookup ys j)) →

GNUmakefile

@@ -23,8 +23,7 @@ Everything.agda:
 # command `cabal install` is needed by cabal-install <= 2.4.*. I did
 # not found any problem running both commands with different versions
 # of cabal-install. See Issue #1001.
-	cabal clean && cabal build && cabal install
-	cabal exec -- GenerateEverything
+	cabal run GenerateEverything
 
 .PHONY: listings
 listings: Everything.agda

GenerateEverything.hs

@@ -26,6 +26,13 @@ unsafeModules :: [FilePath]
 unsafeModules = map modToFile
   [ "Codata.Musical.Cofin"
   , "Codata.Musical.Colist"
+  , "Codata.Musical.Colist.Base"
+  , "Codata.Musical.Colist.Properties"
+  , "Codata.Musical.Colist.Bisimilarity"
+  , "Codata.Musical.Colist.Relation.Unary.All"
+  , "Codata.Musical.Colist.Relation.Unary.All.Properties"
+  , "Codata.Musical.Colist.Relation.Unary.Any"
+  , "Codata.Musical.Colist.Relation.Unary.Any.Properties"
   , "Codata.Musical.Colist.Infinite-merge"
   , "Codata.Musical.Conat"
   , "Codata.Musical.Costring"
@@ -39,7 +46,12 @@ unsafeModules = map modToFile
   , "Foreign.Haskell.Maybe"
   , "Foreign.Haskell.Pair"
   , "IO"
+  , "IO.Base"
+  , "IO.Infinite"
+  , "IO.Finite"
   , "IO.Primitive"
+  , "IO.Primitive.Infinite"
+  , "IO.Primitive.Finite"
   , "Relation.Binary.PropositionalEquality.TrustMe"
   , "System.Environment"
   , "System.Environment.Primitive"

README/Debug/Trace.agda

@@ -59,10 +59,11 @@ div m n    = just (go m m) where
 open import Level using (0ℓ)
 open import IO
 
+main : Main
 main =
   let r = trace "Call to div" (div 4 2)
       j = λ n → trace "Forcing the result wrapped in just." (putStrLn (show n)) in
-  run {a = 0ℓ} (maybe′ j (return _) r)
+  run (maybe′ j (return _) r)
 
 -- We get the following trace where we can see that checking that the
 -- maybe-solution is just-headed does not force the natural number. Once forced,

README/IO.agda

@@ -11,7 +11,7 @@ module README.IO where
 open import Level
 open import Data.Nat.Base
 open import Data.Nat.Show using (show)
-open import Data.String.Base using (String; _++_; lines)
+open import Data.String using (String; _++_; lines)
 open import Data.Unit.Polymorphic
 open import IO
 

graph.sh

@@ -0,0 +1,32 @@
+#!/bin/sh
+
+### You can call this script like so to generate a dependency graph
+### of the `Data.List.Base` module:
+### ./graph.sh src/Data/List/Base.agda
+
+### Allow users to pick the agda executable they want by prefixing
+### the call with `AGDA=agda-X.Y.Z` and default to agda in case
+### nothing was picked
+AGDA=${AGDA:-"agda"}
+
+### Grab the directory and name of the target agda file
+DIR=$(dirname $1)
+BASE=$(basename $1 ".agda")
+FILE=_build/${DIR}/${BASE}
+
+### Prepare the directory for the dot & tmp files
+mkdir -p _build/$DIR
+
+### Generate the dot file for the target agda file
+${AGDA} -i. -isrc/ --dependency-graph=${FILE}.dot $1
+
+### Trim the graph to remove transitive dependencies. Without that the
+### graphs get too big too quickly and are impossible to render
+tred ${FILE}.dot > ${FILE}2.dot
+mv ${FILE}2.dot ${FILE}.dot
+
+### Generate an svg representation of the graph
+dot -Tsvg ${FILE}.dot > ${FILE}.svg
+
+### Add a symlink to it in the base directory
+ln -is ${FILE}.svg ${BASE}.svg

src/Codata/Colist.agda

@@ -10,16 +10,16 @@ module Codata.Colist where
 
 open import Level using (Level)
 open import Size
-open import Data.Unit
+open import Data.Unit.Base
 open import Data.Nat.Base
 open import Data.Product using (_×_ ; _,_)
 open import Data.These.Base using (These; this; that; these)
 open import Data.Maybe.Base using (Maybe; nothing; just)
 open import Data.List.Base using (List; []; _∷_)
 open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
-open import Data.Vec.Bounded as Vec≤ using (Vec≤)
-open import Function
+open import Data.Vec.Bounded.Base as Vec≤ using (Vec≤)
+open import Function.Base using (_$′_; _∘′_; id; _∘_)
 
 open import Codata.Thunk using (Thunk; force)
 open import Codata.Conat as Conat using (Conat ; zero ; suc)

src/Codata/Cowriter.agda

@@ -17,15 +17,15 @@ open import Codata.Thunk using (Thunk; force)
 open import Codata.Conat
 open import Codata.Delay using (Delay; later; now)
 open import Codata.Stream as Stream using (Stream; _∷_)
-open import Data.Unit
+open import Data.Unit.Base
 open import Data.List.Base using (List; []; _∷_)
 open import Data.List.NonEmpty using (List⁺; _∷_)
 open import Data.Nat.Base as Nat using (ℕ; zero; suc)
 open import Data.Product as Prod using (_×_; _,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Data.Vec.Base using (Vec; []; _∷_)
-open import Data.Vec.Bounded as Vec≤ using (Vec≤; _,_)
-open import Function
+open import Data.Vec.Bounded.Base as Vec≤ using (Vec≤; _,_)
+open import Function.Base using (_$_; _∘′_; id)
 
 private
   variable

src/Codata/Delay.agda

@@ -19,7 +19,7 @@ open import Data.Maybe.Base hiding (map ; fromMaybe ; zipWith ; alignWith ; zip
 open import Data.Product as P hiding (map ; zip)
 open import Data.Sum.Base as S hiding (map)
 open import Data.These.Base as T using (These; this; that; these)
-open import Function
+open import Function.Base using (id)
 
 ------------------------------------------------------------------------
 -- Definition