Move Codata modules to Codata.Sized (agda#1699)

Author: MatthewDaggitt

CHANGELOG.md

@@ -50,6 +50,14 @@ Non-backwards compatible changes
 
 * All modules and names that were deprecated prior to v1.0 have been removed.
 
+#### Moved `Codata` modules to `Codata.Sized`
+
+* Due to the change in Agda 2.6.2 where sized types are no longer compatible
+  with the `--safe` flag, it has become clear that a third variant of codata
+  will be needed using coinductive records. Therefore all existing modules in
+  `Codata` which used sized types have been moved inside a new folder named
+  `Sized`, e.g. `Codata.Stream` has become `Codata.Sized.Stream`.
+
 ### Improvements to pretty printing and regexes
 
 * In `Text.Pretty`, `Doc` is now a record rather than a type alias. This

GenerateEverything.hs

@@ -113,36 +113,36 @@ isWithKModule =
 
 sizedTypesModules :: [FilePath]
 sizedTypesModules = map modToFile
-  [ "Codata.Cofin"
-  , "Codata.Cofin.Literals"
-  , "Codata.Colist"
-  , "Codata.Colist.Bisimilarity"
-  , "Codata.Colist.Categorical"
-  , "Codata.Colist.Properties"
-  , "Codata.Conat"
-  , "Codata.Conat.Bisimilarity"
-  , "Codata.Conat.Literals"
-  , "Codata.Conat.Properties"
-  , "Codata.Covec"
-  , "Codata.Covec.Bisimilarity"
-  , "Codata.Covec.Categorical"
-  , "Codata.Covec.Instances"
-  , "Codata.Covec.Properties"
-  , "Codata.Cowriter"
-  , "Codata.Cowriter.Bisimilarity"
-  , "Codata.Delay"
-  , "Codata.Delay.Bisimilarity"
-  , "Codata.Delay.Categorical"
-  , "Codata.Delay.Properties"
-  , "Codata.M"
-  , "Codata.M.Bisimilarity"
-  , "Codata.M.Properties"
-  , "Codata.Stream"
-  , "Codata.Stream.Bisimilarity"
-  , "Codata.Stream.Categorical"
-  , "Codata.Stream.Instances"
-  , "Codata.Stream.Properties"
-  , "Codata.Thunk"
+  [ "Codata.Sized.Cofin"
+  , "Codata.Sized.Cofin.Literals"
+  , "Codata.Sized.Colist"
+  , "Codata.Sized.Colist.Bisimilarity"
+  , "Codata.Sized.Colist.Categorical"
+  , "Codata.Sized.Colist.Properties"
+  , "Codata.Sized.Conat"
+  , "Codata.Sized.Conat.Bisimilarity"
+  , "Codata.Sized.Conat.Literals"
+  , "Codata.Sized.Conat.Properties"
+  , "Codata.Sized.Covec"
+  , "Codata.Sized.Covec.Bisimilarity"
+  , "Codata.Sized.Covec.Categorical"
+  , "Codata.Sized.Covec.Instances"
+  , "Codata.Sized.Covec.Properties"
+  , "Codata.Sized.Cowriter"
+  , "Codata.Sized.Cowriter.Bisimilarity"
+  , "Codata.Sized.Delay"
+  , "Codata.Sized.Delay.Bisimilarity"
+  , "Codata.Sized.Delay.Categorical"
+  , "Codata.Sized.Delay.Properties"
+  , "Codata.Sized.M"
+  , "Codata.Sized.M.Bisimilarity"
+  , "Codata.Sized.M.Properties"
+  , "Codata.Sized.Stream"
+  , "Codata.Sized.Stream.Bisimilarity"
+  , "Codata.Sized.Stream.Categorical"
+  , "Codata.Sized.Stream.Instances"
+  , "Codata.Sized.Stream.Properties"
+  , "Codata.Sized.Thunk"
   , "Data.Container.Fixpoints.Sized"
   , "Data.W.Sized"
   , "Data.Nat.PseudoRandom.LCG.Unsafe"

README.agda

@@ -70,7 +70,7 @@ import README.Axiom
 
 -- • Codata
 --     Coinductive data types and properties. There are two different
---     approaches taken. The `Codata` folder contains the new more
+--     approaches taken. The `Codata.Sized` folder contains the new more
 --     standard approach using sized types. The `Codata.Musical`
 --     folder contains modules using the old musical notation.
 
@@ -157,8 +157,8 @@ import Data.Vec      -- Fixed-length vectors.
 
 -- • Some co-inductive data types
 
-import Codata.Stream -- Streams.
-import Codata.Colist -- Colists.
+import Codata.Sized.Stream -- Streams.
+import Codata.Sized.Colist -- Colists.
 
 -- • Some types used to structure computations
 
@@ -202,7 +202,7 @@ import Data.Nat.Induction
 -- • Support for coinduction
 
 import Codata.Musical.Notation
-import Codata.Thunk
+import Codata.Sized.Thunk
 
 -- • IO
 

src/Codata/Musical/Conversion.agda

@@ -13,20 +13,20 @@
 module Codata.Musical.Conversion where
 
 open import Level using (Level)
-import Codata.Cofin as Sized
-import Codata.Colist as Sized
-import Codata.Conat as Sized
-import Codata.Covec as Sized
-import Codata.M
-import Codata.Stream as Sized
+import Codata.Sized.Cofin  as Sized
+import Codata.Sized.Colist as Sized
+import Codata.Sized.Conat  as Sized
+import Codata.Sized.Covec  as Sized
+import Codata.Sized.M      as Sized
+import Codata.Sized.Stream as Sized
+open import Codata.Sized.Thunk
 open import Codata.Musical.Cofin hiding (module Cofin)
 open import Codata.Musical.Colist hiding (module Colist)
 open import Codata.Musical.Conat
 open import Codata.Musical.Covec hiding (module Covec)
 open import Codata.Musical.M hiding (module M)
 open import Codata.Musical.Notation
 open import Codata.Musical.Stream hiding (module Stream)
-open import Codata.Thunk
 open import Data.Product
 open import Data.Container.Core as C using (Container)
 import Size
@@ -78,12 +78,12 @@ module Covec where
 
 module M {s p} {C : Container s p} where
 
-  fromMusical : ∀ {i} → M C → Codata.M.M C i
-  fromMusical (inf t) = Codata.M.inf (C.map rec t) where
+  fromMusical : ∀ {i} → M C → Sized.M C i
+  fromMusical (inf t) = Sized.M.inf (C.map rec t) where
     rec = λ x → λ where .force → fromMusical (♭ x)
 
-  toMusical : Codata.M.M C Size.∞ → M C
-  toMusical (Codata.M.inf (s , f)) = inf (s , λ p → ♯ toMusical (f p .force))
+  toMusical : Sized.M C Size.∞ → M C
+  toMusical (Sized.M.inf (s , f)) = inf (s , λ p → ♯ toMusical (f p .force))
 
 module Stream where
 

src/Codata/Cofin.agda renamed to src/Codata/Sized/Cofin.agda

@@ -6,13 +6,13 @@
 
 {-# OPTIONS --without-K --sized-types #-}
 
-module Codata.Cofin where
+module Codata.Sized.Cofin where
 
 open import Size
-open import Codata.Thunk
-open import Codata.Conat as Conat
+open import Codata.Sized.Thunk
+open import Codata.Sized.Conat as Conat
   using (Conat; zero; suc; infinity; _ℕ<_; sℕ≤s; _ℕ≤infinity)
-open import Codata.Conat.Bisimilarity as Bisim using (_⊢_≲_ ; s≲s)
+open import Codata.Sized.Conat.Bisimilarity as Bisim using (_⊢_≲_ ; s≲s)
 open import Data.Nat.Base
 open import Data.Fin.Base as Fin hiding (fromℕ; fromℕ≤; fromℕ<; toℕ)
 open import Function.Base using (_∋_)

src/Codata/Cofin/Literals.agda renamed to src/Codata/Sized/Cofin/Literals.agda

@@ -6,13 +6,13 @@
 
 {-# OPTIONS --without-K --sized-types #-}
 
-module Codata.Cofin.Literals where
+module Codata.Sized.Cofin.Literals where
 
 open import Data.Nat.Base
 open import Agda.Builtin.FromNat
-open import Codata.Conat
-open import Codata.Conat.Properties
-open import Codata.Cofin
+open import Codata.Sized.Conat
+open import Codata.Sized.Conat.Properties
+open import Codata.Sized.Cofin
 open import Relation.Nullary.Decidable
 
 number : ∀ n → Number (Cofin n)

src/Codata/Colist.agda renamed to src/Codata/Sized/Colist.agda

@@ -6,7 +6,7 @@
 
 {-# OPTIONS --without-K --sized-types #-}
 
-module Codata.Colist where
+module Codata.Sized.Colist where
 
 open import Level using (Level)
 open import Size
@@ -21,11 +21,11 @@ open import Data.Vec.Base as Vec using (Vec; []; _∷_)
 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)
-open import Codata.Cowriter as CW using (Cowriter; _∷_)
-open import Codata.Delay as Delay using (Delay ; now ; later)
-open import Codata.Stream using (Stream ; _∷_)
+open import Codata.Sized.Thunk using (Thunk; force)
+open import Codata.Sized.Conat as Conat using (Conat ; zero ; suc)
+open import Codata.Sized.Cowriter as CW using (Cowriter; _∷_)
+open import Codata.Sized.Delay as Delay using (Delay ; now ; later)
+open import Codata.Sized.Stream using (Stream ; _∷_)
 
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 

src/Codata/Colist/Bisimilarity.agda renamed to src/Codata/Sized/Colist/Bisimilarity.agda

@@ -6,12 +6,12 @@
 
 {-# OPTIONS --without-K --sized-types #-}
 
-module Codata.Colist.Bisimilarity where
+module Codata.Sized.Colist.Bisimilarity where
 
 open import Level using (Level; _⊔_)
 open import Size
-open import Codata.Thunk
-open import Codata.Colist
+open import Codata.Sized.Thunk
+open import Codata.Sized.Colist
 open import Data.List.Base using (List; []; _∷_)
 open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
 open import Data.List.NonEmpty as List⁺  using (List⁺; _∷_)

src/Codata/Colist/Categorical.agda renamed to src/Codata/Sized/Colist/Categorical.agda

@@ -6,10 +6,10 @@
 
 {-# OPTIONS --without-K --sized-types #-}
 
-module Codata.Colist.Categorical where
+module Codata.Sized.Colist.Categorical where
 
-open import Codata.Conat using (infinity)
-open import Codata.Colist
+open import Codata.Sized.Conat using (infinity)
+open import Codata.Sized.Colist
 open import Category.Functor
 open import Category.Applicative
 

src/Codata/Colist/Properties.agda renamed to src/Codata/Sized/Colist/Properties.agda

@@ -6,19 +6,19 @@
 
 {-# OPTIONS --without-K --sized-types #-}
 
-module Codata.Colist.Properties where
+module Codata.Sized.Colist.Properties where
 
 open import Level using (Level)
 open import Size
-open import Codata.Thunk as Thunk using (Thunk; force)
-open import Codata.Colist
-open import Codata.Colist.Bisimilarity
-open import Codata.Conat
-open import Codata.Conat.Bisimilarity as coℕᵇ using (zero; suc)
-import Codata.Conat.Properties as coℕₚ
-open import Codata.Cowriter as Cowriter using ([_]; _∷_)
-open import Codata.Cowriter.Bisimilarity as coWriterᵇ using ([_]; _∷_)
-open import Codata.Stream as Stream using (Stream; _∷_)
+open import Codata.Sized.Thunk as Thunk using (Thunk; force)
+open import Codata.Sized.Colist
+open import Codata.Sized.Colist.Bisimilarity
+open import Codata.Sized.Conat
+open import Codata.Sized.Conat.Bisimilarity as coℕᵇ using (zero; suc)
+import Codata.Sized.Conat.Properties as coℕₚ
+open import Codata.Sized.Cowriter as Cowriter using ([_]; _∷_)
+open import Codata.Sized.Cowriter.Bisimilarity as coWriterᵇ using ([_]; _∷_)
+open import Codata.Sized.Stream as Stream using (Stream; _∷_)
 open import Data.Vec.Bounded as Vec≤ using (Vec≤)
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_)

src/Codata/Conat.agda renamed to src/Codata/Sized/Conat.agda

@@ -6,10 +6,10 @@
 
 {-# OPTIONS --without-K --sized-types #-}
 
-module Codata.Conat where
+module Codata.Sized.Conat where
 
 open import Size
-open import Codata.Thunk
+open import Codata.Sized.Thunk
 
 open import Data.Nat.Base using (ℕ ; zero ; suc)
 open import Relation.Nullary

src/Codata/Conat/Bisimilarity.agda renamed to src/Codata/Sized/Conat/Bisimilarity.agda

@@ -6,12 +6,12 @@
 
 {-# OPTIONS --without-K --sized-types #-}
 
-module Codata.Conat.Bisimilarity where
+module Codata.Sized.Conat.Bisimilarity where
 
 open import Level using (0ℓ)
 open import Size
-open import Codata.Thunk
-open import Codata.Conat
+open import Codata.Sized.Thunk
+open import Codata.Sized.Conat
 open import Relation.Binary
 
 infix 1 _⊢_≈_

src/Codata/Conat/Literals.agda renamed to src/Codata/Sized/Conat/Literals.agda

@@ -6,11 +6,11 @@
 
 {-# OPTIONS --without-K --sized-types #-}
 
-module Codata.Conat.Literals where
+module Codata.Sized.Conat.Literals where
 
 open import Agda.Builtin.FromNat
 open import Data.Unit
-open import Codata.Conat
+open import Codata.Sized.Conat
 
 number : ∀ {i} → Number (Conat i)
 number = record

src/Codata/Conat/Properties.agda renamed to src/Codata/Sized/Conat/Properties.agda

@@ -6,13 +6,13 @@
 
 {-# OPTIONS --without-K --sized-types #-}
 
-module Codata.Conat.Properties where
+module Codata.Sized.Conat.Properties where
 
 open import Size
 open import Data.Nat.Base using (ℕ; zero; suc)
-open import Codata.Thunk
-open import Codata.Conat
-open import Codata.Conat.Bisimilarity
+open import Codata.Sized.Thunk
+open import Codata.Sized.Conat
+open import Codata.Sized.Conat.Bisimilarity
 open import Function.Base using (_∋_)
 open import Relation.Nullary
 open import Relation.Nullary.Decidable using (map′)

src/Codata/Covec.agda renamed to src/Codata/Sized/Covec.agda

@@ -6,17 +6,17 @@
 
 {-# OPTIONS --without-K --sized-types #-}
 
-module Codata.Covec where
+module Codata.Sized.Covec where
 
 open import Size
 
-open import Codata.Thunk using (Thunk; force)
-open import Codata.Conat as Conat
-open import Codata.Conat.Bisimilarity
-open import Codata.Conat.Properties
-open import Codata.Cofin as Cofin using (Cofin; zero; suc)
-open import Codata.Colist as Colist using (Colist ; [] ; _∷_)
-open import Codata.Stream as Stream using (Stream ; _∷_)
+open import Codata.Sized.Thunk using (Thunk; force)
+open import Codata.Sized.Conat as Conat
+open import Codata.Sized.Conat.Bisimilarity
+open import Codata.Sized.Conat.Properties
+open import Codata.Sized.Cofin as Cofin using (Cofin; zero; suc)
+open import Codata.Sized.Colist as Colist using (Colist ; [] ; _∷_)
+open import Codata.Sized.Stream as Stream using (Stream ; _∷_)
 open import Function.Base using (_∘′_)
 
 data Covec {ℓ} (A : Set ℓ) (i : Size) : Conat ∞ → Set ℓ where

src/Codata/Covec/Bisimilarity.agda renamed to src/Codata/Sized/Covec/Bisimilarity.agda

@@ -6,13 +6,13 @@
 
 {-# OPTIONS --without-K --sized-types #-}
 
-module Codata.Covec.Bisimilarity where
+module Codata.Sized.Covec.Bisimilarity where
 
 open import Level using (_⊔_)
 open import Size
-open import Codata.Thunk
-open import Codata.Conat hiding (_⊔_)
-open import Codata.Covec
+open import Codata.Sized.Thunk
+open import Codata.Sized.Conat hiding (_⊔_)
+open import Codata.Sized.Covec
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
 

src/Codata/Covec/Categorical.agda renamed to src/Codata/Sized/Covec/Categorical.agda

@@ -6,10 +6,10 @@
 
 {-# OPTIONS --without-K --sized-types #-}
 
-module Codata.Covec.Categorical where
+module Codata.Sized.Covec.Categorical where
 
-open import Codata.Conat
-open import Codata.Covec
+open import Codata.Sized.Conat
+open import Codata.Sized.Covec
 
 open import Category.Functor
 open import Category.Applicative