From d01fd7f2aaa4731e8fa21d4cea61df763d95d514 Mon Sep 17 00:00:00 2001
From: Silas Hayes-Williams <silas.hayes.williams@gmail.com>
Date: Thu, 30 Jul 2026 15:36:11 -0400
Subject: [PATCH 01/24] Add show class

---
 src/Text/Show.agda | 71 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 71 insertions(+)
 create mode 100644 src/Text/Show.agda

diff --git a/src/Text/Show.agda b/src/Text/Show.agda
new file mode 100644
index 0000000000..1144145c99
--- /dev/null
+++ b/src/Text/Show.agda
@@ -0,0 +1,71 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Show class
+------------------------------------------------------------------------
+
+{-# OPTIONS --with-K #-}
+
+module Text.Show where
+
+-- should builtin be used?
+open import Agda.Builtin.Reflection using (Precedence)
+open import Agda.Builtin.Int
+open import Agda.Builtin.String using (primShowNat)
+open import Data.Bool.Base using (Bool)
+open import Data.Char.Base using (Char)
+open import Data.List.Base using (List; []; _++_; _∷_)
+open import Data.Nat.Base using (ℕ)
+open import Data.String.Base using (String; fromList; toList)
+open import Function.Base using (_∘_; const; _$_)
+open import Level using (Level)
+
+private
+  variable
+    a : Level
+    A : Set a
+
+record Show {α} (A : Set α) :  Set α
+  where
+  constructor show′
+
+  field  showsPrecList :  Precedence → A → List Char → List Char
+
+  showPrecList : Precedence → A → List Char
+  showPrecList prec a =  showsPrecList prec a []
+
+  showsPrec : Precedence → A → String → String
+  showsPrec prec a str = fromList (showsPrecList prec a (toList str))
+
+  showPrec : Precedence → A → String
+  showPrec prec a = fromList (showsPrecList prec a [])
+
+  show : A → String
+  show = showPrec Precedence.unrelated
+
+open Show {{...}}
+
+-- NOTE: could/should be moved into respective modules, e.g. Data.List.Show
+instance
+  IntShow : Show Int
+  IntShow .Show.showsPrecList _ i str = toList (primShowInteger i) ++ str
+
+instance
+  NatShow : Show ℕ
+  NatShow .Show.showsPrecList _ n str = (toList (primShowNat n)) ++ str
+
+instance
+  ListShow : {{ Show A }} → Show (List A)
+  ListShow .Show.showsPrecList prec [] str = '[' ∷ (']' ∷ str)
+  ListShow .Show.showsPrecList prec (x ∷ xs) str = '[' ∷ listShow' prec x xs str
+    where
+      -- after the first call, don't prepend '['
+      -- and don't call on [], hence head taken as its own argument
+      listShow' : {{ Show A }} → Precedence → A → List A → List Char → List Char
+      listShow' prec x [] str = showsPrecList prec x (']' ∷ str)
+      listShow' prec x (x₁ ∷ xs) str = showsPrecList prec x (',' ∷ (listShow' prec x₁ xs str))
+
+-- some examples to show the instances working
+private
+  test : String
+  test = show (5 ∷ 2 ∷ [])

From 32907bae1d432bdd4184ab20eee567be5cfaf56f Mon Sep 17 00:00:00 2001
From: Silas Hayes-Williams <silas.hayes.williams@gmail.com>
Date: Thu, 30 Jul 2026 16:35:57 -0400
Subject: [PATCH 02/24] Cleanup code

---
 src/Text/Show.agda | 32 ++++++++++++++++++++------------
 1 file changed, 20 insertions(+), 12 deletions(-)

diff --git a/src/Text/Show.agda b/src/Text/Show.agda
index 1144145c99..2268c364df 100644
--- a/src/Text/Show.agda
+++ b/src/Text/Show.agda
@@ -4,18 +4,19 @@
 -- Show class
 ------------------------------------------------------------------------
 
-{-# OPTIONS --with-K #-}
+{-# OPTIONS --without-K --safe  #-}
 
 module Text.Show where
 
 -- should builtin be used?
 open import Agda.Builtin.Reflection using (Precedence)
-open import Agda.Builtin.Int
-open import Agda.Builtin.String using (primShowNat)
 open import Data.Bool.Base using (Bool)
 open import Data.Char.Base using (Char)
 open import Data.List.Base using (List; []; _++_; _∷_)
 open import Data.Nat.Base using (ℕ)
+open import Data.Nat.Show using () renaming (show to showℕ)
+open import Data.Integer.Base using (ℤ)
+open import Data.Integer.Show using () renaming (show to showℤ)
 open import Data.String.Base using (String; fromList; toList)
 open import Function.Base using (_∘_; const; _$_)
 open import Level using (Level)
@@ -25,34 +26,41 @@ private
     a : Level
     A : Set a
 
-record Show {α} (A : Set α) :  Set α
+record Show (A : Set a) :  Set a
   where
   constructor show′
 
   field  showsPrecList :  Precedence → A → List Char → List Char
 
   showPrecList : Precedence → A → List Char
-  showPrecList prec a =  showsPrecList prec a []
+  showPrecList prec x =  showsPrecList prec x []
 
   showsPrec : Precedence → A → String → String
-  showsPrec prec a str = fromList (showsPrecList prec a (toList str))
+  showsPrec prec x str = fromList (showsPrecList prec x (toList str))
 
   showPrec : Precedence → A → String
-  showPrec prec a = fromList (showsPrecList prec a [])
+  showPrec prec x = fromList (showsPrecList prec x [])
 
   show : A → String
   show = showPrec Precedence.unrelated
 
 open Show {{...}}
 
--- NOTE: could/should be moved into respective modules, e.g. Data.List.Show
+-- NOTE: could/should be moved into respective modules, e.g. Data.List.Show, Data.Nat.Show, etc...
+
+------------------------------------------------------------------------
+-- Primitive show instances
+
 instance
-  IntShow : Show Int
-  IntShow .Show.showsPrecList _ i str = toList (primShowInteger i) ++ str
+  IntShow : Show ℤ
+  IntShow .Show.showsPrecList _ i str = toList (showℤ i) ++ str
 
 instance
   NatShow : Show ℕ
-  NatShow .Show.showsPrecList _ n str = (toList (primShowNat n)) ++ str
+  NatShow .Show.showsPrecList _ n str = (toList (showℕ n)) ++ str
+
+------------------------------------------------------------------------
+-- List show
 
 instance
   ListShow : {{ Show A }} → Show (List A)
@@ -63,7 +71,7 @@ instance
       -- and don't call on [], hence head taken as its own argument
       listShow' : {{ Show A }} → Precedence → A → List A → List Char → List Char
       listShow' prec x [] str = showsPrecList prec x (']' ∷ str)
-      listShow' prec x (x₁ ∷ xs) str = showsPrecList prec x (',' ∷ (listShow' prec x₁ xs str))
+      listShow' prec x (y ∷ ys) str = showsPrecList prec x (',' ∷ (listShow' prec y ys str))
 
 -- some examples to show the instances working
 private

From 8776f8e9081d49b1d8315cf4dc0d18dc0fdc69da Mon Sep 17 00:00:00 2001
From: Silas Hayes-Williams <silas.hayes.williams@gmail.com>
Date: Thu, 30 Jul 2026 16:50:12 -0400
Subject: [PATCH 03/24] Cleanup code

---
 src/Text/Show.agda | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/src/Text/Show.agda b/src/Text/Show.agda
index 2268c364df..11959cb8d0 100644
--- a/src/Text/Show.agda
+++ b/src/Text/Show.agda
@@ -26,11 +26,9 @@ private
     a : Level
     A : Set a
 
-record Show (A : Set a) :  Set a
-  where
-  constructor show′
-
-  field  showsPrecList :  Precedence → A → List Char → List Char
+record Show (A : Set a) :  Set a where
+  field
+    showsPrecList :  Precedence → A → List Char → List Char
 
   showPrecList : Precedence → A → List Char
   showPrecList prec x =  showsPrecList prec x []

From befbdf1b731fd1c82ac56a520e21268a110f3683 Mon Sep 17 00:00:00 2001
From: Silas Hayes-Williams <silas.hayes.williams@gmail.com>
Date: Fri, 31 Jul 2026 10:42:53 -0400
Subject: [PATCH 04/24] Move List Show instance to .Instances module

---
 src/Data/List/Instances.agda | 25 ++++++++++++++++++++++++-
 src/Text/Show.agda           | 26 ++++----------------------
 2 files changed, 28 insertions(+), 23 deletions(-)

diff --git a/src/Data/List/Instances.agda b/src/Data/List/Instances.agda
index 3f28c89185..57a7495338 100644
--- a/src/Data/List/Instances.agda
+++ b/src/Data/List/Instances.agda
@@ -8,7 +8,7 @@
 
 module Data.List.Instances where
 
-open import Data.List.Base using (List; []; _∷_)
+open import Data.List.Base using (List; []; _∷_; foldr)
 open import Data.List.Effectful
   using (functor; applicative; applicativeZero; alternative; monad
         ; monadZero; monadPlus)
@@ -29,6 +29,8 @@ open import Relation.Binary.PropositionalEquality.Properties
   using (isDecEquivalence)
 open import Relation.Binary.TypeClasses
   using (IsDecTotalOrder; IsDecEquivalence; _≈?_)
+open import Text.Show
+open Show {{...}}
 
 private
   variable
@@ -58,3 +60,24 @@ instance
                              → {{IsDecTotalOrder _≈_ _≼_}}
                              → IsDecTotalOrder (Pointwise _≈_) (Lex-≤ _≈_ _≼_)
   List-Lex-≤-isDecTotalOrder {{≼-isDecTotalOrder}} = ≤-isDecTotalOrder ≼-isDecTotalOrder
+
+------------------------------------------------------------------------
+-- List show
+
+instance
+  ListShow : {{ Show A }} → Show (List A)
+  ListShow .Show.showsPrecList prec [] str = '[' ∷ (']' ∷ str)
+  ListShow .Show.showsPrecList prec (x ∷ xs) str = '[' ∷ showsPrecList prec x (listShow' prec str xs)
+    where
+      -- after the first call, don't prepend '['
+      -- and don't call on [], hence head taken as its own argument
+      listShow' : {{ Show A }} → Precedence → List Char → List A → List Char
+      listShow' prec str = foldr (λ x str → ',' ∷ showsPrecList prec x str) (']' ∷ str)
+
+-- some examples to show the instances working
+private
+  test[ℕ] : String
+  test[ℕ] = show (5 ∷ 2 ∷ 12 ∷ 42 ∷ [])
+
+  meow : Set
+  meow = {!!}
diff --git a/src/Text/Show.agda b/src/Text/Show.agda
index 11959cb8d0..c5d2e0f0b6 100644
--- a/src/Text/Show.agda
+++ b/src/Text/Show.agda
@@ -9,15 +9,16 @@
 module Text.Show where
 
 -- should builtin be used?
-open import Agda.Builtin.Reflection using (Precedence)
+open import Agda.Builtin.Reflection using (Precedence) public
 open import Data.Bool.Base using (Bool)
-open import Data.Char.Base using (Char)
+open import Data.Char.Base using (Char) public
 open import Data.List.Base using (List; []; _++_; _∷_)
 open import Data.Nat.Base using (ℕ)
 open import Data.Nat.Show using () renaming (show to showℕ)
 open import Data.Integer.Base using (ℤ)
 open import Data.Integer.Show using () renaming (show to showℤ)
-open import Data.String.Base using (String; fromList; toList)
+open import Data.String.Base using (String) public
+open import Data.String.Base using (fromList; toList)
 open import Function.Base using (_∘_; const; _$_)
 open import Level using (Level)
 
@@ -56,22 +57,3 @@ instance
 instance
   NatShow : Show ℕ
   NatShow .Show.showsPrecList _ n str = (toList (showℕ n)) ++ str
-
-------------------------------------------------------------------------
--- List show
-
-instance
-  ListShow : {{ Show A }} → Show (List A)
-  ListShow .Show.showsPrecList prec [] str = '[' ∷ (']' ∷ str)
-  ListShow .Show.showsPrecList prec (x ∷ xs) str = '[' ∷ listShow' prec x xs str
-    where
-      -- after the first call, don't prepend '['
-      -- and don't call on [], hence head taken as its own argument
-      listShow' : {{ Show A }} → Precedence → A → List A → List Char → List Char
-      listShow' prec x [] str = showsPrecList prec x (']' ∷ str)
-      listShow' prec x (y ∷ ys) str = showsPrecList prec x (',' ∷ (listShow' prec y ys str))
-
--- some examples to show the instances working
-private
-  test : String
-  test = show (5 ∷ 2 ∷ [])

From e762d27d3fcb8d34cce7fa8ff05fed1b624cd24a Mon Sep 17 00:00:00 2001
From: Silas Hayes-Williams <silas.hayes.williams@gmail.com>
Date: Fri, 31 Jul 2026 10:52:24 -0400
Subject: [PATCH 05/24] Move instances to .Instances modules for Nat and
 Integer

---
 src/Data/Integer/Instances.agda | 11 +++++++++++
 src/Data/List/Instances.agda    | 12 +++++-------
 src/Data/Nat/Instances.agda     | 10 ++++++++++
 src/Text/Show.agda              | 19 -------------------
 4 files changed, 26 insertions(+), 26 deletions(-)

diff --git a/src/Data/Integer/Instances.agda b/src/Data/Integer/Instances.agda
index b43ad23e66..2e57880dec 100644
--- a/src/Data/Integer/Instances.agda
+++ b/src/Data/Integer/Instances.agda
@@ -8,10 +8,21 @@
 
 module Data.Integer.Instances where
 
+open import Data.Integer.Base using (ℤ)
 open import Data.Integer.Properties using (_≡?_; ≤-isDecTotalOrder)
+open import Data.Integer.Show using () renaming (show to showℤ)
+open import Data.List.Base using (_++_)
+open import Data.String.Base using (toList)
 open import Relation.Binary.PropositionalEquality.Properties
   using (isDecEquivalence)
 
+open import Text.Show using (Show)
+
 instance
   ℤ-≡-isDecEquivalence = isDecEquivalence _≡?_
   ℤ-≤-isDecTotalOrder = ≤-isDecTotalOrder
+
+instance
+  open Show
+  IntShow : Show ℤ
+  IntShow .showsPrecList _ i str = toList (showℤ i) ++ str
diff --git a/src/Data/List/Instances.agda b/src/Data/List/Instances.agda
index 57a7495338..4306a65c59 100644
--- a/src/Data/List/Instances.agda
+++ b/src/Data/List/Instances.agda
@@ -22,6 +22,7 @@ open import Data.List.Relation.Binary.Pointwise
   using (Pointwise)
 open import Data.List.Relation.Binary.Lex.NonStrict
   using (Lex-≤; ≤-isDecTotalOrder)
+open import Data.Nat.Instances using (NatShow)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
@@ -30,7 +31,6 @@ open import Relation.Binary.PropositionalEquality.Properties
 open import Relation.Binary.TypeClasses
   using (IsDecTotalOrder; IsDecEquivalence; _≈?_)
 open import Text.Show
-open Show {{...}}
 
 private
   variable
@@ -64,13 +64,14 @@ instance
 ------------------------------------------------------------------------
 -- List show
 
+open Show {{...}}
+
 instance
   ListShow : {{ Show A }} → Show (List A)
-  ListShow .Show.showsPrecList prec [] str = '[' ∷ (']' ∷ str)
-  ListShow .Show.showsPrecList prec (x ∷ xs) str = '[' ∷ showsPrecList prec x (listShow' prec str xs)
+  ListShow .showsPrecList prec [] str = '[' ∷ (']' ∷ str)
+  ListShow .showsPrecList prec (x ∷ xs) str = '[' ∷ showsPrecList prec x (listShow' prec str xs)
     where
       -- after the first call, don't prepend '['
-      -- and don't call on [], hence head taken as its own argument
       listShow' : {{ Show A }} → Precedence → List Char → List A → List Char
       listShow' prec str = foldr (λ x str → ',' ∷ showsPrecList prec x str) (']' ∷ str)
 
@@ -78,6 +79,3 @@ instance
 private
   test[ℕ] : String
   test[ℕ] = show (5 ∷ 2 ∷ 12 ∷ 42 ∷ [])
-
-  meow : Set
-  meow = {!!}
diff --git a/src/Data/Nat/Instances.agda b/src/Data/Nat/Instances.agda
index efe7e48d3e..fdf0b5c427 100644
--- a/src/Data/Nat/Instances.agda
+++ b/src/Data/Nat/Instances.agda
@@ -8,10 +8,20 @@
 
 module Data.Nat.Instances where
 
+open import Data.List.Base using (_++_)
+open import Data.Nat.Base using (ℕ)
 open import Data.Nat.Properties using (≤-isDecTotalOrder; _≡?_)
+open import Data.Nat.Show using () renaming (show to showℕ)
+open import Data.String.Base using (toList)
 open import Relation.Binary.PropositionalEquality.Properties
   using (isDecEquivalence)
+open import Text.Show using (Show)
 
 instance
   ℕ-≡-isDecEquivalence = isDecEquivalence _≡?_
   ℕ-≤-isDecTotalOrder = ≤-isDecTotalOrder
+
+instance
+  open Show
+  NatShow : Show ℕ
+  NatShow .showsPrecList _ n str = (toList (showℕ n)) ++ str
diff --git a/src/Text/Show.agda b/src/Text/Show.agda
index c5d2e0f0b6..c2a1200d55 100644
--- a/src/Text/Show.agda
+++ b/src/Text/Show.agda
@@ -10,13 +10,9 @@ module Text.Show where
 
 -- should builtin be used?
 open import Agda.Builtin.Reflection using (Precedence) public
-open import Data.Bool.Base using (Bool)
 open import Data.Char.Base using (Char) public
 open import Data.List.Base using (List; []; _++_; _∷_)
-open import Data.Nat.Base using (ℕ)
 open import Data.Nat.Show using () renaming (show to showℕ)
-open import Data.Integer.Base using (ℤ)
-open import Data.Integer.Show using () renaming (show to showℤ)
 open import Data.String.Base using (String) public
 open import Data.String.Base using (fromList; toList)
 open import Function.Base using (_∘_; const; _$_)
@@ -42,18 +38,3 @@ record Show (A : Set a) :  Set a where
 
   show : A → String
   show = showPrec Precedence.unrelated
-
-open Show {{...}}
-
--- NOTE: could/should be moved into respective modules, e.g. Data.List.Show, Data.Nat.Show, etc...
-
-------------------------------------------------------------------------
--- Primitive show instances
-
-instance
-  IntShow : Show ℤ
-  IntShow .Show.showsPrecList _ i str = toList (showℤ i) ++ str
-
-instance
-  NatShow : Show ℕ
-  NatShow .Show.showsPrecList _ n str = (toList (showℕ n)) ++ str

From 4c8232d07f66cb97b0d844751211fce0c30d7614 Mon Sep 17 00:00:00 2001
From: Silas Hayes-Williams <psysh13@nottingham.ac.uk>
Date: Fri, 14 Aug 2026 12:10:15 -0400
Subject: [PATCH 06/24] Rename Show to Write

---
 src/Data/List/Instances.agda       | 24 ++++++++++++------------
 src/Data/Nat/Instances.agda        |  8 ++++----
 src/Text/{Show.agda => Write.agda} | 22 +++++++++++-----------
 3 files changed, 27 insertions(+), 27 deletions(-)
 rename src/Text/{Show.agda => Write.agda} (58%)

diff --git a/src/Data/List/Instances.agda b/src/Data/List/Instances.agda
index 4306a65c59..b388cdb22d 100644
--- a/src/Data/List/Instances.agda
+++ b/src/Data/List/Instances.agda
@@ -22,7 +22,7 @@ open import Data.List.Relation.Binary.Pointwise
   using (Pointwise)
 open import Data.List.Relation.Binary.Lex.NonStrict
   using (Lex-≤; ≤-isDecTotalOrder)
-open import Data.Nat.Instances using (NatShow)
+open import Data.Nat.Instances using (NatWrite)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
@@ -30,7 +30,7 @@ open import Relation.Binary.PropositionalEquality.Properties
   using (isDecEquivalence)
 open import Relation.Binary.TypeClasses
   using (IsDecTotalOrder; IsDecEquivalence; _≈?_)
-open import Text.Show
+open import Text.Write
 
 private
   variable
@@ -48,7 +48,7 @@ instance
   listMonadPlus = monadPlus
   listIsString = isString
   -- ListT
-  listTFunctor = λ {f} {g} {M} {{inst}} → Trans.functor {f} {g} {M} inst
+    listTFunctor = λ {f} {g} {M} {{inst}} → Trans.functor {f} {g} {M} inst
   listTApplicative = λ {f} {g} {M} {{inst}} → Trans.applicative {f} {g} {M} inst
   listTMonad = λ {f} {g} {M} {{inst}} → Trans.monad {f} {g} {M} inst
   listTMonadT = λ {f} {g} {M} {{inst}} → Trans.monadT {f} {g} {M} inst
@@ -62,20 +62,20 @@ instance
   List-Lex-≤-isDecTotalOrder {{≼-isDecTotalOrder}} = ≤-isDecTotalOrder ≼-isDecTotalOrder
 
 ------------------------------------------------------------------------
--- List show
+-- List write
 
-open Show {{...}}
+open Write {{...}}
 
 instance
-  ListShow : {{ Show A }} → Show (List A)
-  ListShow .showsPrecList prec [] str = '[' ∷ (']' ∷ str)
-  ListShow .showsPrecList prec (x ∷ xs) str = '[' ∷ showsPrecList prec x (listShow' prec str xs)
+  ListWrite : {{ Write A }} → Write (List A)
+  ListWrite .writesPrecList prec [] str = '[' ∷ (']' ∷ str)
+  ListWrite .writesPrecList prec (x ∷ xs) str = '[' ∷ writesPrecList prec x (listWrite' prec str xs)
     where
       -- after the first call, don't prepend '['
-      listShow' : {{ Show A }} → Precedence → List Char → List A → List Char
-      listShow' prec str = foldr (λ x str → ',' ∷ showsPrecList prec x str) (']' ∷ str)
+      listWrite' : {{ Write A }} → Precedence → List Char → List A → List Char
+      listWrite' prec str = foldr (λ x str → ',' ∷ writesPrecList prec x str) (']' ∷ str)
 
--- some examples to show the instances working
+-- some examples to write the instances working
 private
   test[ℕ] : String
-  test[ℕ] = show (5 ∷ 2 ∷ 12 ∷ 42 ∷ [])
+  test[ℕ] = write (5 ∷ 2 ∷ 12 ∷ 42 ∷ [])
diff --git a/src/Data/Nat/Instances.agda b/src/Data/Nat/Instances.agda
index fdf0b5c427..36d80157d2 100644
--- a/src/Data/Nat/Instances.agda
+++ b/src/Data/Nat/Instances.agda
@@ -15,13 +15,13 @@ open import Data.Nat.Show using () renaming (show to showℕ)
 open import Data.String.Base using (toList)
 open import Relation.Binary.PropositionalEquality.Properties
   using (isDecEquivalence)
-open import Text.Show using (Show)
+open import Text.Write using (Write)
 
 instance
   ℕ-≡-isDecEquivalence = isDecEquivalence _≡?_
   ℕ-≤-isDecTotalOrder = ≤-isDecTotalOrder
 
 instance
-  open Show
-  NatShow : Show ℕ
-  NatShow .showsPrecList _ n str = (toList (showℕ n)) ++ str
+  open Write
+  NatWrite : Write ℕ
+  NatWrite .writesPrecList _ n str = (toList (showℕ n)) ++ str
diff --git a/src/Text/Show.agda b/src/Text/Write.agda
similarity index 58%
rename from src/Text/Show.agda
rename to src/Text/Write.agda
index c2a1200d55..4811a61151 100644
--- a/src/Text/Show.agda
+++ b/src/Text/Write.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --without-K --safe  #-}
 
-module Text.Show where
+module Text.Write where
 
 -- should builtin be used?
 open import Agda.Builtin.Reflection using (Precedence) public
@@ -23,18 +23,18 @@ private
     a : Level
     A : Set a
 
-record Show (A : Set a) :  Set a where
+record Write (A : Set a) :  Set a where
   field
-    showsPrecList :  Precedence → A → List Char → List Char
+    writesPrecList :  Precedence → A → List Char → List Char
 
-  showPrecList : Precedence → A → List Char
-  showPrecList prec x =  showsPrecList prec x []
+  writePrecList : Precedence → A → List Char
+  writePrecList prec x =  writesPrecList prec x []
 
-  showsPrec : Precedence → A → String → String
-  showsPrec prec x str = fromList (showsPrecList prec x (toList str))
+  writesPrec : Precedence → A → String → String
+  writesPrec prec x str = fromList (writesPrecList prec x (toList str))
 
-  showPrec : Precedence → A → String
-  showPrec prec x = fromList (showsPrecList prec x [])
+  writePrec : Precedence → A → String
+  writePrec prec x = fromList (writesPrecList prec x [])
 
-  show : A → String
-  show = showPrec Precedence.unrelated
+  write : A → String
+  write = writePrec Precedence.unrelated

From c9d932aa77e8db901c596dd516689f28f6b84cb1 Mon Sep 17 00:00:00 2001
From: Silas Hayes-Williams <psysh13@nottingham.ac.uk>
Date: Fri, 14 Aug 2026 14:05:59 -0400
Subject: [PATCH 07/24] Introduce Pretty, Write, Read, and ReadWrite

---
 src/Text/Pretty.agda    | 15 +++++++++++++++
 src/Text/Read.agda      | 29 +++++++++++++++++++++++++++++
 src/Text/ReadWrite.agda | 40 ++++++++++++++++++++++++++++++++++++++++
 src/Text/Write.agda     |  7 ++++++-
 4 files changed, 90 insertions(+), 1 deletion(-)
 create mode 100644 src/Text/Read.agda
 create mode 100644 src/Text/ReadWrite.agda

diff --git a/src/Text/Pretty.agda b/src/Text/Pretty.agda
index a9202b1f82..d3b22a6197 100644
--- a/src/Text/Pretty.agda
+++ b/src/Text/Pretty.agda
@@ -12,6 +12,7 @@ open import Data.Nat.Base using (ℕ)
 
 module Text.Pretty (width : ℕ) where
 
+open import Agda.Builtin.Reflection using (Precedence) public
 import Level
 open import Data.Char.Base using (Char)
 open import Data.List.Base
@@ -137,3 +138,17 @@ commaSep = foldDoc (λ d e → d <> comma <+> e)
 
 newline : Doc
 newline = flush empty
+
+------------------------------------------------------------------------
+-- Pretty class
+
+private
+  variable
+    a : Level.Level
+
+record Pretty (A : Set a) : Set a where
+  field
+    pPrintPrec : Precedence → A → Doc
+
+  pPrint : A → Doc
+  pPrint = pPrintPrec Precedence.unrelated
diff --git a/src/Text/Read.agda b/src/Text/Read.agda
new file mode 100644
index 0000000000..54e448d1df
--- /dev/null
+++ b/src/Text/Read.agda
@@ -0,0 +1,29 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Read class
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe  #-}
+
+module Text.Read where
+
+-- should builtin be used?
+open import Agda.Builtin.Reflection using (Precedence) public
+open import Data.Char.Base using (Char) public
+open import Data.List.Base using (List; []; _++_; _∷_)
+open import Data.Maybe.Base using (Maybe)
+open import Data.Nat.Show using () renaming (show to showℕ)
+open import Data.String.Base using (String) public
+open import Data.String.Base using (fromList; toList)
+open import Function.Base using (_∘_; const; _$_)
+open import Level using (Level)
+
+private
+  variable
+    a : Level
+    A : Set a
+
+record Read (A : Set a) :  Set a where
+  field
+    read : String → Maybe A
diff --git a/src/Text/ReadWrite.agda b/src/Text/ReadWrite.agda
new file mode 100644
index 0000000000..da8fff8cfb
--- /dev/null
+++ b/src/Text/ReadWrite.agda
@@ -0,0 +1,40 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- ReadWrite class
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe  #-}
+
+module Text.ReadWrite where
+
+-- should builtin be used?
+open import Agda.Builtin.Reflection using (Precedence) public
+open import Data.Char.Base using (Char) public
+open import Data.List.Base using (List; []; _++_; _∷_)
+open import Data.Nat.Show using () renaming (show to showℕ)
+open import Data.Maybe.Base using (just)
+open import Data.String.Base using (String) public
+open import Data.String.Base using (fromList; toList)
+open import Function.Base using (_∘_; const; _$_)
+open import Level using (Level)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Text.Write using (Write)
+open import Text.Read using (Read)
+
+private
+  variable
+    a : Level
+    A : Set a
+
+record ReadWrite (A : Set a) :  Set a where
+  open Read
+  open Write
+
+  field
+    reader : Read A
+    writer : Write A
+
+    readWrite : ∀ {x : A} → read reader (write writer x) ≡ (just x)
+    writeRead : ∀ {x : A} {s : String} → (read reader s) ≡ (just x) → writeMaybe writer (read reader s) ≡ s
+
diff --git a/src/Text/Write.agda b/src/Text/Write.agda
index 4811a61151..a117c1fbab 100644
--- a/src/Text/Write.agda
+++ b/src/Text/Write.agda
@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Show class
+-- Write class
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe  #-}
@@ -12,6 +12,7 @@ module Text.Write where
 open import Agda.Builtin.Reflection using (Precedence) public
 open import Data.Char.Base using (Char) public
 open import Data.List.Base using (List; []; _++_; _∷_)
+open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.Nat.Show using () renaming (show to showℕ)
 open import Data.String.Base using (String) public
 open import Data.String.Base using (fromList; toList)
@@ -38,3 +39,7 @@ record Write (A : Set a) :  Set a where
 
   write : A → String
   write = writePrec Precedence.unrelated
+
+  writeMaybe : Maybe A → String
+  writeMaybe nothing = ""
+  writeMaybe (just x) = write x

From a6496e13b9175d8d4af2b835cccdf35bb01874e3 Mon Sep 17 00:00:00 2001
From: Silas Hayes-Williams <psysh13@nottingham.ac.uk>
Date: Fri, 14 Aug 2026 14:58:38 -0400
Subject: [PATCH 08/24] Fix IntWrite

---
 src/Data/Integer/Instances.agda | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Data/Integer/Instances.agda b/src/Data/Integer/Instances.agda
index 2e57880dec..683668138e 100644
--- a/src/Data/Integer/Instances.agda
+++ b/src/Data/Integer/Instances.agda
@@ -16,13 +16,13 @@ open import Data.String.Base using (toList)
 open import Relation.Binary.PropositionalEquality.Properties
   using (isDecEquivalence)
 
-open import Text.Show using (Show)
+open import Text.Write using (Write)
 
 instance
   ℤ-≡-isDecEquivalence = isDecEquivalence _≡?_
   ℤ-≤-isDecTotalOrder = ≤-isDecTotalOrder
 
 instance
-  open Show
-  IntShow : Show ℤ
-  IntShow .showsPrecList _ i str = toList (showℤ i) ++ str
+  open Write
+  IntWrite : Write ℤ
+  IntWrite .writesPrecList _ i str = toList (showℤ i) ++ str

From fa521f3bdbceaf9bc2ed0b117b3c33e144f148d9 Mon Sep 17 00:00:00 2001
From: Silas Hayes-Williams <psysh13@nottingham.ac.uk>
Date: Fri, 14 Aug 2026 15:07:57 -0400
Subject: [PATCH 09/24] Remove accidental indent in Data.List.Instances

---
 src/Data/List/Instances.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/List/Instances.agda b/src/Data/List/Instances.agda
index b388cdb22d..cba8597ebc 100644
--- a/src/Data/List/Instances.agda
+++ b/src/Data/List/Instances.agda
@@ -48,7 +48,7 @@ instance
   listMonadPlus = monadPlus
   listIsString = isString
   -- ListT
-    listTFunctor = λ {f} {g} {M} {{inst}} → Trans.functor {f} {g} {M} inst
+  listTFunctor = λ {f} {g} {M} {{inst}} → Trans.functor {f} {g} {M} inst
   listTApplicative = λ {f} {g} {M} {{inst}} → Trans.applicative {f} {g} {M} inst
   listTMonad = λ {f} {g} {M} {{inst}} → Trans.monad {f} {g} {M} inst
   listTMonadT = λ {f} {g} {M} {{inst}} → Trans.monadT {f} {g} {M} inst

From 5986b9e390672ca6102b08199612a3da30c40d72 Mon Sep 17 00:00:00 2001
From: Silas Hayes-Williams <58709355+silas-hw@users.noreply.github.com>
Date: Mon, 17 Aug 2026 12:43:41 -0400
Subject: [PATCH 10/24] Fix typo

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
---
 src/Text/Read.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Text/Read.agda b/src/Text/Read.agda
index 54e448d1df..914cfa30fe 100644
--- a/src/Text/Read.agda
+++ b/src/Text/Read.agda
@@ -24,6 +24,6 @@ private
     a : Level
     A : Set a
 
-record Read (A : Set a) :  Set a where
+record Read (A : Set a) : Set a where
   field
     read : String → Maybe A

From 335dd51ecc2deaa665cebd447d8f4306e6a3efba Mon Sep 17 00:00:00 2001
From: Silas Hayes-Williams <psysh13@nottingham.ac.uk>
Date: Mon, 17 Aug 2026 13:16:41 -0400
Subject: [PATCH 11/24] Update Read interface

---
 src/Data/List/Unsafe/Instances.agda | 19 +++++++++++++++++++
 src/Text/Read.agda                  | 20 ++++++++++++++++----
 2 files changed, 35 insertions(+), 4 deletions(-)
 create mode 100644 src/Data/List/Unsafe/Instances.agda

diff --git a/src/Data/List/Unsafe/Instances.agda b/src/Data/List/Unsafe/Instances.agda
new file mode 100644
index 0000000000..47d7868a73
--- /dev/null
+++ b/src/Data/List/Unsafe/Instances.agda
@@ -0,0 +1,19 @@
+{-# OPTIONS --with-K #-}
+
+open import Data.List.Base
+open import Data.Nat.Base
+open import Data.Nat.Instances
+open import Level using (Level)
+open import Text.Write
+open import Text.Pretty 80
+
+private
+  variable
+    a : Level
+    A : Set a
+
+open Pretty {{...}}
+
+instance
+  ListPretty : {{ Pretty A }} → Pretty (List A)
+  ListPretty .pPrintPrec prec xs = parens (commaSep (map (pPrintPrec prec) xs))
diff --git a/src/Text/Read.agda b/src/Text/Read.agda
index 914cfa30fe..d600867240 100644
--- a/src/Text/Read.agda
+++ b/src/Text/Read.agda
@@ -12,11 +12,11 @@ module Text.Read where
 open import Agda.Builtin.Reflection using (Precedence) public
 open import Data.Char.Base using (Char) public
 open import Data.List.Base using (List; []; _++_; _∷_)
-open import Data.Maybe.Base using (Maybe)
-open import Data.Nat.Show using () renaming (show to showℕ)
+open import Data.Maybe.Base using (Maybe; just; nothing; map)
+open import Data.Product.Base using (_×_; _,_; proj₁) renaming (map to map×)
 open import Data.String.Base using (String) public
 open import Data.String.Base using (fromList; toList)
-open import Function.Base using (_∘_; const; _$_)
+open import Function.Base using (_∘_; const; _$_; id)
 open import Level using (Level)
 
 private
@@ -26,4 +26,16 @@ private
 
 record Read (A : Set a) : Set a where
   field
-    read : String → Maybe A
+    readsPrecList : Precedence → List Char → Maybe (A × List Char)
+
+  readPrecList : Precedence → List Char → Maybe A
+  readPrecList prec str = map proj₁ (readsPrecList prec str)
+  
+  readsPrec : Precedence → String → Maybe (A × String)
+  readsPrec prec str = map (map× id fromList) (readsPrecList prec (toList str))
+
+  readPrec : Precedence → String → Maybe A
+  readPrec prec = (readPrecList prec) ∘ toList
+
+  read : String → Maybe A
+  read = readPrec Precedence.unrelated

From 892fd98281f3ab8dec9144ecb80e041fa3d51dd9 Mon Sep 17 00:00:00 2001
From: Silas Hayes-Williams <psysh13@nottingham.ac.uk>
Date: Mon, 17 Aug 2026 13:36:49 -0400
Subject: [PATCH 12/24] Fix whitespace

---
 src/Text/Read.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Text/Read.agda b/src/Text/Read.agda
index d600867240..99bcde109e 100644
--- a/src/Text/Read.agda
+++ b/src/Text/Read.agda
@@ -30,7 +30,7 @@ record Read (A : Set a) : Set a where
 
   readPrecList : Precedence → List Char → Maybe A
   readPrecList prec str = map proj₁ (readsPrecList prec str)
-  
+
   readsPrec : Precedence → String → Maybe (A × String)
   readsPrec prec str = map (map× id fromList) (readsPrecList prec (toList str))
 

From fe50044af0934bbc619ddc575b9fe7ed7ca751e8 Mon Sep 17 00:00:00 2001
From: Silas Hayes-Williams <psysh13@nottingham.ac.uk>
Date: Mon, 17 Aug 2026 16:13:37 -0400
Subject: [PATCH 13/24] Add Maybe Pretty instance

---
 src/Data/Maybe/Unsafe/Instances.agda | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 src/Data/Maybe/Unsafe/Instances.agda

diff --git a/src/Data/Maybe/Unsafe/Instances.agda b/src/Data/Maybe/Unsafe/Instances.agda
new file mode 100644
index 0000000000..068c34041e
--- /dev/null
+++ b/src/Data/Maybe/Unsafe/Instances.agda
@@ -0,0 +1,15 @@
+
+open import Data.Maybe.Base
+open import Text.Pretty 80
+open import Level using (Level)
+
+private
+  variable
+    a : Level
+    A : Set a
+
+open Pretty {{...}}
+instance
+  MaybePretty : {{ Pretty A }} → Pretty (Maybe A)
+  MaybePretty .pPrintPrec prec (just x) = (text "just") <+> pPrintPrec prec x
+  MaybePretty .pPrintPrec prec nothing = text "nothing"

From b7823a09479b77ffe66eb48e0ce687169e97fd22 Mon Sep 17 00:00:00 2001
From: Silas Hayes-Williams <psysh13@nottingham.ac.uk>
Date: Mon, 17 Aug 2026 16:27:20 -0400
Subject: [PATCH 14/24] Add 'pretty' function to Pretty

---
 src/Text/Pretty.agda | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Text/Pretty.agda b/src/Text/Pretty.agda
index d3b22a6197..f305a3f4ec 100644
--- a/src/Text/Pretty.agda
+++ b/src/Text/Pretty.agda
@@ -152,3 +152,6 @@ record Pretty (A : Set a) : Set a where
 
   pPrint : A → Doc
   pPrint = pPrintPrec Precedence.unrelated
+
+  pretty : A → String
+  pretty = render ∘ pPrint

From 2c7c8af3a558b62d86ccba0e7f470e35dcda1a05 Mon Sep 17 00:00:00 2001
From: Silas Hayes-Williams <psysh13@nottingham.ac.uk>
Date: Mon, 17 Aug 2026 16:54:37 -0400
Subject: [PATCH 15/24] Add NatPretty instance

---
 src/Data/Maybe/Unsafe/Instances.agda | 11 ++++++++++-
 src/Data/Nat/Unsafe/Instances.agda   | 16 ++++++++++++++++
 2 files changed, 26 insertions(+), 1 deletion(-)
 create mode 100644 src/Data/Nat/Unsafe/Instances.agda

diff --git a/src/Data/Maybe/Unsafe/Instances.agda b/src/Data/Maybe/Unsafe/Instances.agda
index 068c34041e..1011efa9ef 100644
--- a/src/Data/Maybe/Unsafe/Instances.agda
+++ b/src/Data/Maybe/Unsafe/Instances.agda
@@ -1,3 +1,12 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Unsafe instances for Maybe
+------------------------------------------------------------------------
+
+{-# OPTIONS --with-K #-}
+
+module Data.Maybe.Unsafe.Instances where
 
 open import Data.Maybe.Base
 open import Text.Pretty 80
@@ -8,8 +17,8 @@ private
     a : Level
     A : Set a
 
-open Pretty {{...}}
 instance
+  open Pretty {{...}}
   MaybePretty : {{ Pretty A }} → Pretty (Maybe A)
   MaybePretty .pPrintPrec prec (just x) = (text "just") <+> pPrintPrec prec x
   MaybePretty .pPrintPrec prec nothing = text "nothing"
diff --git a/src/Data/Nat/Unsafe/Instances.agda b/src/Data/Nat/Unsafe/Instances.agda
new file mode 100644
index 0000000000..0c72aca9b3
--- /dev/null
+++ b/src/Data/Nat/Unsafe/Instances.agda
@@ -0,0 +1,16 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Unsafe instances for Nat
+------------------------------------------------------------------------
+
+module Data.Nat.Unsafe.Instances where
+
+open import Data.Nat.Base
+open import Data.Nat.Show using (show)
+open import Text.Pretty 80
+
+instance
+  open Pretty {{...}}
+  ℕPretty : Pretty ℕ
+  ℕPretty .pPrintPrec prec n = text (show n)

From fec6ee2b45d41e1c3b0faff8167c6daf101f3951 Mon Sep 17 00:00:00 2001
From: Silas Hayes-Williams <psysh13@nottingham.ac.uk>
Date: Mon, 17 Aug 2026 17:53:09 -0400
Subject: [PATCH 16/24] Add module header

---
 src/Data/List/Unsafe/Instances.agda |  8 +++++
 src/Text/Write/Deriving.agda        | 46 +++++++++++++++++++++++++++++
 2 files changed, 54 insertions(+)
 create mode 100644 src/Text/Write/Deriving.agda

diff --git a/src/Data/List/Unsafe/Instances.agda b/src/Data/List/Unsafe/Instances.agda
index 47d7868a73..39ee0cacd1 100644
--- a/src/Data/List/Unsafe/Instances.agda
+++ b/src/Data/List/Unsafe/Instances.agda
@@ -1,5 +1,13 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Unsafe instances for List
+------------------------------------------------------------------------
+
 {-# OPTIONS --with-K #-}
 
+module Data.List.Unsafe.Instances where
+
 open import Data.List.Base
 open import Data.Nat.Base
 open import Data.Nat.Instances
diff --git a/src/Text/Write/Deriving.agda b/src/Text/Write/Deriving.agda
new file mode 100644
index 0000000000..c112627cab
--- /dev/null
+++ b/src/Text/Write/Deriving.agda
@@ -0,0 +1,46 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Macro for deriving instances of Write
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Text.Write.Deriving where
+
+{-
+Should this be placed in Tactic.DerivingWrite?
+
+For now, some notes on design:
+
+Should print syntactically correct Agda that can be read by
+an also derived Read instance.
+
+Steps:
+1. Check term is actually a data/record definition, if not throw typecheck error?
+2. Get all parameters and attach required instances to the resulting function type
+
+   e.g. for something like
+
+   data MyData (A : Set) : Set where
+     ...
+
+   we would need
+
+   MyDataWrite : {A : Set} → {{ Write A }} → Write (MyData A)
+
+   but for somethin like
+
+   dat MyData' (x : ℕ) : Set where
+     ...
+
+   we instead need
+
+   MyData'Write : {{ Write ℕ }} → {x : ℕ} → Write (MyData x) 
+3. For records, print in record syntax (record { x = y, ... }), recursively
+   calling write on fields
+4. For data, get fixity of constructor and recursively call write, intertwining
+   parts of the constructors name in a way that properly aligns with fixity
+
+   (e.g. print x ∷ [] as "x ∷ []", not "_∷_ x []")
+-}

From b96a6a97772a97ebf78498b21a2ccc662c4f1632 Mon Sep 17 00:00:00 2001
From: Silas Hayes-Williams <psysh13@nottingham.ac.uk>
Date: Mon, 17 Aug 2026 20:02:13 -0400
Subject: [PATCH 17/24] Fix whitespace

---
 src/Text/Write/Deriving.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Text/Write/Deriving.agda b/src/Text/Write/Deriving.agda
index c112627cab..3b7bbe53f1 100644
--- a/src/Text/Write/Deriving.agda
+++ b/src/Text/Write/Deriving.agda
@@ -36,7 +36,7 @@ Steps:
 
    we instead need
 
-   MyData'Write : {{ Write ℕ }} → {x : ℕ} → Write (MyData x) 
+   MyData'Write : {{ Write ℕ }} → {x : ℕ} → Write (MyData x)
 3. For records, print in record syntax (record { x = y, ... }), recursively
    calling write on fields
 4. For data, get fixity of constructor and recursively call write, intertwining

From 87d7f8f82f55ccf68ee8797c24028689ffccb1d9 Mon Sep 17 00:00:00 2001
From: Silas Hayes-Williams <psysh13@nottingham.ac.uk>
Date: Tue, 18 Aug 2026 09:21:16 -0400
Subject: [PATCH 18/24] Add modules to unsafe and withK sets in
 GenerateEverything

---
 GenerateEverything.hs              | 6 ++++++
 src/Data/Nat/Unsafe/Instances.agda | 2 ++
 2 files changed, 8 insertions(+)

diff --git a/GenerateEverything.hs b/GenerateEverything.hs
index b4356c6bf0..4327bf3ba0 100644
--- a/GenerateEverything.hs
+++ b/GenerateEverything.hs
@@ -50,6 +50,9 @@ unsafeModules = map modToFile
   , "Data.Bytestring.IO"
   , "Data.Bytestring.IO.Primitive"
   , "Data.Bytestring.Primitive"
+  , "Data.List.Unsafe.Instances"
+  , "Data.Maybe.Unsafe.Instances"
+  , "Data.Nat.Unsafe.Instances"
   , "Data.Word8.Base"
   , "Data.Word8.Literals"
   , "Data.Word8.Primitive"
@@ -109,6 +112,9 @@ isUnsafeModule fp =
 withKModules :: [FilePath]
 withKModules = map modToFile
   [ "Axiom.Extensionality.Heterogeneous"
+  , "Data.List.Unsafe.Instances"
+  , "Data.Maybe.Unsafe.Instances"
+  , "Data.Nat.Unsafe.Instances"
   , "Data.Star.BoundedVec"
   , "Data.Star.Decoration"
   , "Data.Star.Environment"
diff --git a/src/Data/Nat/Unsafe/Instances.agda b/src/Data/Nat/Unsafe/Instances.agda
index 0c72aca9b3..1b0f89f14f 100644
--- a/src/Data/Nat/Unsafe/Instances.agda
+++ b/src/Data/Nat/Unsafe/Instances.agda
@@ -4,6 +4,8 @@
 -- Unsafe instances for Nat
 ------------------------------------------------------------------------
 
+{-# OPTIONS --with-K #-}
+
 module Data.Nat.Unsafe.Instances where
 
 open import Data.Nat.Base

From 35b27c28c413e1188c9dcf9f3eb3981cadcd08f5 Mon Sep 17 00:00:00 2001
From: Silas Hayes-Williams <psysh13@nottingham.ac.uk>
Date: Tue, 18 Aug 2026 10:58:53 -0400
Subject: [PATCH 19/24] Add NatRead instance

---
 src/Data/Nat/Instances.agda | 20 ++++++++++++++++----
 1 file changed, 16 insertions(+), 4 deletions(-)

diff --git a/src/Data/Nat/Instances.agda b/src/Data/Nat/Instances.agda
index 36d80157d2..2a49d8822d 100644
--- a/src/Data/Nat/Instances.agda
+++ b/src/Data/Nat/Instances.agda
@@ -8,13 +8,17 @@
 
 module Data.Nat.Instances where
 
-open import Data.List.Base using (_++_)
-open import Data.Nat.Base using (ℕ)
+open import Data.Char using (isDigit)
+open import Data.List.Base using (_++_; spanᵇ)
+open import Data.Maybe using (_>>=_; just)
+open import Data.Nat.Base using (ℕ; _≤ᵇ_)
 open import Data.Nat.Properties using (≤-isDecTotalOrder; _≡?_)
-open import Data.Nat.Show using () renaming (show to showℕ)
-open import Data.String.Base using (toList)
+open import Data.Nat.Show using (readMaybe) renaming (show to showℕ)
+open import Data.Product using (_,_)
+open import Data.String.Base using (toList; fromList)
 open import Relation.Binary.PropositionalEquality.Properties
   using (isDecEquivalence)
+open import Text.Read using (Read)
 open import Text.Write using (Write)
 
 instance
@@ -25,3 +29,11 @@ instance
   open Write
   NatWrite : Write ℕ
   NatWrite .writesPrecList _ n str = (toList (showℕ n)) ++ str
+
+instance
+  open Read {{...}}
+  NatRead : Read ℕ
+  NatRead .readsPrecList prec str = do
+    let (x , y) = spanᵇ isDigit str
+    num ← readMaybe 10 (fromList x)
+    just (num , y)

From 8d97b800163a47fb16dfd8b7b5d4bd4c36f0ad79 Mon Sep 17 00:00:00 2001
From: Silas Hayes-Williams <psysh13@nottingham.ac.uk>
Date: Tue, 18 Aug 2026 11:03:07 -0400
Subject: [PATCH 20/24] Rename variables

---
 src/Data/Nat/Instances.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Data/Nat/Instances.agda b/src/Data/Nat/Instances.agda
index 2a49d8822d..245151f83d 100644
--- a/src/Data/Nat/Instances.agda
+++ b/src/Data/Nat/Instances.agda
@@ -34,6 +34,6 @@ instance
   open Read {{...}}
   NatRead : Read ℕ
   NatRead .readsPrecList prec str = do
-    let (x , y) = spanᵇ isDigit str
-    num ← readMaybe 10 (fromList x)
-    just (num , y)
+    let (digits , leftover) = spanᵇ isDigit str
+    num ← readMaybe 10 (fromList digits)
+    just (num , leftover)

From 018720169435c4f48fd2ba86b3d3866e168e8342 Mon Sep 17 00:00:00 2001
From: Silas Hayes-Williams <psysh13@nottingham.ac.uk>
Date: Wed, 19 Aug 2026 18:01:01 -0400
Subject: [PATCH 21/24] Start on deriving macro

---
 src/Text/Write/Deriving.agda | 100 +++++++++++++++++++++++++++++++++++
 1 file changed, 100 insertions(+)

diff --git a/src/Text/Write/Deriving.agda b/src/Text/Write/Deriving.agda
index 3b7bbe53f1..ace0d90bd1 100644
--- a/src/Text/Write/Deriving.agda
+++ b/src/Text/Write/Deriving.agda
@@ -8,6 +8,17 @@
 
 module Text.Write.Deriving where
 
+open import Data.List.Base using (_∷_; []; List; concat; _++_; zip)
+open import Data.List.Effectful
+open import Data.Nat.Base using (ℕ)
+open TraversableM using (mapM)
+open import Data.Unit using (⊤)
+open import Data.Product.Base using (_×_; _,_; uncurry; proj₁; proj₂)
+open import Reflection
+open import Reflection.AST.Term using (Telescope; Clause)
+open import Reflection.TCM.Effectful using () renaming (monad to monadTCM)
+open import Text.Write
+
 {-
 Should this be placed in Tactic.DerivingWrite?
 
@@ -37,10 +48,99 @@ Steps:
    we instead need
 
    MyData'Write : {{ Write ℕ }} → {x : ℕ} → Write (MyData x)
+
 3. For records, print in record syntax (record { x = y, ... }), recursively
    calling write on fields
 4. For data, get fixity of constructor and recursively call write, intertwining
    parts of the constructors name in a way that properly aligns with fixity
 
    (e.g. print x ∷ [] as "x ∷ []", not "_∷_ x []")
+
+Reflection notes:
+- Prelude has a lot of machinery that should be moved over
+- Should derive *own* type so we know the exact order things are in
 -}
+
+------------------------------------------------------------------------
+-- Machinery for deriving things
+
+-- Derive the type of an instance for a given record type
+instanceArg : Arg Name
+instanceArg = arg (arg-info instance′ defaultModality) (quote Write)
+
+instanceType : Name → Name → TC Type
+instanceType = {!!}
+
+telView : Type → Telescope × Type
+telView (pi a (abs x b)) = ((x , a) ∷ (proj₁ telVb)) , proj₂ telVb
+  where
+    telVb : Telescope × Type
+    telVb = telView b
+telView a                = [] , a
+
+
+telStr : Telescope → List ErrorPart
+telStr [] = strErr "" ∷ []
+telStr ((nm , arg i t) ∷ xs) = strErr nm ∷ termErr t ∷ (telStr xs)
+
+------------------------------------------------------------------------
+-- Actual derive tactic for Write
+
+-- test implementation, no bracketing
+
+defStr : Definition → List ErrorPart
+defStr (function cs) = (strErr "function") ∷ []
+defStr (data-type pars cs) = (strErr "data-type") ∷ []
+defStr (record-type c fs) = (strErr "record-type") ∷ []
+defStr (data-cons d q) = strErr "data-cons" ∷ (nameErr d) ∷ []
+defStr axiom = (strErr "axiom") ∷ []
+defStr prim-fun = (strErr "prim-fun") ∷ []
+
+nameStr : (Name × Type) → List ErrorPart
+nameStr (nm , t) = (nameErr nm) ∷ (strErr " : ") ∷ (telStr (proj₁ (telView t)))
+
+vra : {A : Set} → A → Arg A
+vra = arg (arg-info visible (modality relevant quantity-0))
+
+vrv :  ℕ → List (Arg Term) → Arg Term
+vrv n args = arg (arg-info visible (modality relevant quantity-0)) (var n args)
+
+-- concat write calls to each argument in a telescope
+open Write
+telWrite : ℕ → Term
+telWrite ℕ.zero = con (quote List.[]) []
+telWrite (ℕ.suc n) = def (quote _++_) (vra (def (quote write) ((vrv (ℕ.suc n) []) ∷ [])) ∷ (vra (telWrite n)) ∷ [])
+-- telWrite 0 = con (quote (List.[])) []
+-- telWrite (suc n) = def (quote _++_) ({!!} ∷ {!!})
+
+-- derive the clause for a single constructor
+consClause : Name → Type → Clause
+consClause nm t with telView t
+... | tel , _ = Clause.clause tel [] (telWrite (Data.List.Base.length tel))
+
+deriveWriteFun : Name → Definition → Clause
+deriveWriteFun nm (Reflection.data-type pars cs) = {!!}
+deriveWriteFun nm (Reflection.record-type c fs) = {!!}
+deriveWriteFun _ _ = Clause.absurd-clause [] []
+
+-- cs in data-type contains actual constructor names
+-- 'name' in data-cons is just name of data type itself
+deriveWrite' : Definition → Term → TC ⊤
+deriveWrite' (Reflection.record-type c fs) met = {!!}
+deriveWrite' (data-type p cs) met = do
+  ts ← mapM monadTCM getType cs
+  let clauses = (Data.List.Base.map (uncurry consClause) (zip cs ts))
+      errs    = concat (Data.List.Base.map nameStr (zip cs ts))
+  let term = telWrite 5
+  {!!}
+  typeError errs
+deriveWrite' _ _ = typeError (strErr "Write instances can only be derived for data and record types" ∷ [])
+
+macro
+  deriveWrite : Name → Term → TC ⊤
+  deriveWrite nm met = do
+    d ← getDefinition nm
+    deriveWrite' d met
+
+data Test : Set where
+  a : ℕ → (a : ℕ) → ℕ → Test

From 16f07413eb6f9be33bfe6969c929ca1759a80cbe Mon Sep 17 00:00:00 2001
From: Silas Hayes-Williams <psysh13@nottingham.ac.uk>
Date: Thu, 20 Aug 2026 11:05:06 -0400
Subject: [PATCH 22/24] [skip ci] Add note

---
 src/Text/Write/Deriving.agda | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Text/Write/Deriving.agda b/src/Text/Write/Deriving.agda
index ace0d90bd1..e8af952dff 100644
--- a/src/Text/Write/Deriving.agda
+++ b/src/Text/Write/Deriving.agda
@@ -6,6 +6,8 @@
 
 {-# OPTIONS --without-K --safe #-}
 
+-- NOTE: still figuring things out, just pushing to get over to other device
+
 module Text.Write.Deriving where
 
 open import Data.List.Base using (_∷_; []; List; concat; _++_; zip)

From 876fc3c14c58d5e0aee5940fe34e1972f2bf6fc9 Mon Sep 17 00:00:00 2001
From: Silas Hayes-Williams <silas.hayes.williams@gmail.com>
Date: Thu, 20 Aug 2026 16:31:10 -0400
Subject: [PATCH 23/24] [skip ci] Add more stub methods to Write.Deriving and
 experiment with reflection

---
 src/Text/Write/Deriving.agda | 161 +++++++++++++++++++++++------------
 1 file changed, 108 insertions(+), 53 deletions(-)

diff --git a/src/Text/Write/Deriving.agda b/src/Text/Write/Deriving.agda
index e8af952dff..40335fbe53 100644
--- a/src/Text/Write/Deriving.agda
+++ b/src/Text/Write/Deriving.agda
@@ -10,16 +10,25 @@
 
 module Text.Write.Deriving where
 
+-- Much understanding and structure taken from
+--   ∙ https://github.com/UlfNorell/agda-prelude/blob/master/src/Tactic/Deriving/Eq.agda
+--   ∙ https://github.com/alhassy/gentle-intro-to-reflection
+
 open import Data.List.Base using (_∷_; []; List; concat; _++_; zip)
 open import Data.List.Effectful
-open import Data.Nat.Base using (ℕ)
+open import Data.Nat.Base using (ℕ; _+_)
+open import Data.Nat.Instances using (NatWrite)
 open TraversableM using (mapM)
 open import Data.Unit using (⊤)
 open import Data.Product.Base using (_×_; _,_; uncurry; proj₁; proj₂)
 open import Reflection
 open import Reflection.AST.Term using (Telescope; Clause)
+open import Reflection.TCM
 open import Reflection.TCM.Effectful using () renaming (monad to monadTCM)
-open import Text.Write
+open import Text.Write using (Write; Char; Precedence)
+
+data Test : Set where
+  a : ℕ → (x : ℕ) → ℕ → Test
 
 {-
 Should this be placed in Tactic.DerivingWrite?
@@ -33,23 +42,19 @@ Steps:
 1. Check term is actually a data/record definition, if not throw typecheck error?
 2. Get all parameters and attach required instances to the resulting function type
 
-   e.g. for something like
+   only need instances for types within constructors, e.g.
 
-   data MyData (A : Set) : Set where
-     ...
+   data {a : Level} {A : Set} → MyData A : Set a where
+     c : A → A → MyData A
 
-   we would need
+   needs to have
 
-   MyDataWrite : {A : Set} → {{ Write A }} → Write (MyData A)
+   {a : Level} {A : Set} {{ Write A }} → Write (List A)
 
-   but for somethin like
+   NOT
 
-   dat MyData' (x : ℕ) : Set where
-     ...
+   {a : Level} {A : Set} {{ Write a }} {{ Write A }} → Write (List A)
 
-   we instead need
-
-   MyData'Write : {{ Write ℕ }} → {x : ℕ} → Write (MyData x)
 
 3. For records, print in record syntax (record { x = y, ... }), recursively
    calling write on fields
@@ -61,45 +66,68 @@ Steps:
 Reflection notes:
 - Prelude has a lot of machinery that should be moved over
 - Should derive *own* type so we know the exact order things are in
+- Instance arguments MUST be included in telescope and argument patterns, and must be provided
+  to calls to writesPrecList, as opposed to say instance resolution within the definition.
+  (at least I think)
+- Clause takes telescope of arguments (i.e. the type of the given function without the return value)
+  AND a list of patterns applied to those arguments. If no pattern matching is applied, just the
+  deBruijin index within a var pattern should be given.
+
 -}
 
 ------------------------------------------------------------------------
 -- Machinery for deriving things
 
--- Derive the type of an instance for a given record type
-instanceArg : Arg Name
-instanceArg = arg (arg-info instance′ defaultModality) (quote Write)
-
-instanceType : Name → Name → TC Type
-instanceType = {!!}
-
 telView : Type → Telescope × Type
-telView (pi a (abs x b)) = ((x , a) ∷ (proj₁ telVb)) , proj₂ telVb
+telView (pi x (abs y b)) = ((y , x) ∷ (proj₁ telVb)) , proj₂ telVb
   where
     telVb : Telescope × Type
     telVb = telView b
-telView a                = [] , a
+{-# CATCHALL #-}
+telView x                = [] , x
 
+-- Construct a Type out of a Telescope and Core Type
+telToType : Telescope → Type → Type
+telToType tel core = {!!}
 
-telStr : Telescope → List ErrorPart
-telStr [] = strErr "" ∷ []
-telStr ((nm , arg i t) ∷ xs) = strErr nm ∷ termErr t ∷ (telStr xs)
+-- Return a list of all types that appear in the constructors
+-- or fields of a data or record type that aren't the type itself
+-- in order of appearance
+--
+-- e.g. for
+-- data X : Set where
+--   c₁ : ℕ → X
+--   c₂ : Bool → X → X
+--
+-- This should return ℕ, Bool
+consArgTypes : Type → List Type
+consArgTypes = {!!}
 
-------------------------------------------------------------------------
--- Actual derive tactic for Write
+instanceArg : Arg Name
+instanceArg = arg (arg-info instance′ defaultModality) (quote Write)
 
--- test implementation, no bracketing
+-- Derive the telescope for the type of an instance,
+--
+-- e.g. for Write List this returns
+--      {a : Level} {A : Set a} {{ Write A }}
+instanceTel : Name → Name → TC Telescope
+instanceTel = {!!}
 
-defStr : Definition → List ErrorPart
-defStr (function cs) = (strErr "function") ∷ []
-defStr (data-type pars cs) = (strErr "data-type") ∷ []
-defStr (record-type c fs) = (strErr "record-type") ∷ []
-defStr (data-cons d q) = strErr "data-cons" ∷ (nameErr d) ∷ []
-defStr axiom = (strErr "axiom") ∷ []
-defStr prim-fun = (strErr "prim-fun") ∷ []
+-- Derive the type of an instance for a given record type,
+-- prepending all required instances to the telescope
+--
+-- e.g. for Write (List), will give
+--      : {{ Write A }} → Write (List A)
+instanceType : Name → Name → TC Type
+instanceType cls inst = do
+  clsT ← getType cls
+  instT ← getType inst
+  tel ← instanceTel cls inst
+  pure (telToType tel {!!})
 
-nameStr : (Name × Type) → List ErrorPart
-nameStr (nm , t) = (nameErr nm) ∷ (strErr " : ") ∷ (telStr (proj₁ (telView t)))
+telStr : Telescope → List ErrorPart
+telStr [] = strErr "[]" ∷ []
+telStr ((nm , arg i t) ∷ xs) = strErr nm ∷ termErr t ∷ (telStr xs)
 
 vra : {A : Set} → A → Arg A
 vra = arg (arg-info visible (modality relevant quantity-0))
@@ -107,24 +135,54 @@ vra = arg (arg-info visible (modality relevant quantity-0))
 vrv :  ℕ → List (Arg Term) → Arg Term
 vrv n args = arg (arg-info visible (modality relevant quantity-0)) (var n args)
 
--- concat write calls to each argument in a telescope
-open Write
+vri : ℕ → Arg Term
+vri n = arg (arg-info instance′ (modality relevant quantity-0)) (var n [])
+
+vrv' : ℕ → Arg Term
+vrv' n = vrv n []
+
+------------------------------------------------------------------------
+-- Machinery specific to Write
+
+-- TODO: doc comment can be better
+-- given the telescope for a constructor, produce the whole telescope for
+-- its clause
+-- Precedence → A → List Char → List Char
+conTel : Telescope → Telescope
+conTel tel =  ("str" , (vra (quoteTerm (List Char)))) ∷ (tel ++ ("prec" , (vra (quoteTerm Precedence))) ∷ [])
+
+------------------------------------------------------------------------
+-- Derive macro for Write
+
+-- test implementation, no bracketing
+
+-- concat write calls to each argument in a telescope for Write
+-- suc suc N is used because we have Prec → A → List Char → List Char, so everything is one more away
+-- because of the List Char taken as an argument
+
 telWrite : ℕ → Term
 telWrite ℕ.zero = con (quote List.[]) []
-telWrite (ℕ.suc n) = def (quote _++_) (vra (def (quote write) ((vrv (ℕ.suc n) []) ∷ [])) ∷ (vra (telWrite n)) ∷ [])
+telWrite (ℕ.suc n) = def (quote _++_) (vra (def (quote Write.writesPrecList) (vri 5 ∷ vrv' 0 ∷ vrv' (1 + n) ∷ vrv' 4 ∷ [])) ∷ (vra (telWrite n)) ∷ [])
 -- telWrite 0 = con (quote (List.[])) []
 -- telWrite (suc n) = def (quote _++_) ({!!} ∷ {!!})
 
+varPat : ℕ → Arg Pattern
+varPat n = vra (Pattern.var n)
+
+telToVarPat : ℕ → List (Arg Pattern)
+telToVarPat 0 = []
+telToVarPat (ℕ.suc n) = telToVarPat n ++ (varPat (1 + n)) ∷ []
+
 -- derive the clause for a single constructor
 consClause : Name → Type → Clause
 consClause nm t with telView t
-... | tel , _ = Clause.clause tel [] (telWrite (Data.List.Base.length tel))
+... | tel , _ = Clause.clause (conTel tel) (varPat 0 ∷ (vra (Pattern.con nm (telToVarPat (Data.List.Base.length tel)))) ∷ varPat 4 ∷ []) (telWrite (Data.List.Base.length tel))
 
-deriveWriteFun : Name → Definition → Clause
-deriveWriteFun nm (Reflection.data-type pars cs) = {!!}
+deriveWriteFun : Name → Definition → Definition
+deriveWriteFun nm (Reflection.data-type pars cs) = function (Data.List.Base.map (uncurry consClause) {!!})
 deriveWriteFun nm (Reflection.record-type c fs) = {!!}
-deriveWriteFun _ _ = Clause.absurd-clause [] []
-
+{-# CATCHALL #-}
+deriveWriteFun _ _ = function []
 -- cs in data-type contains actual constructor names
 -- 'name' in data-cons is just name of data type itself
 deriveWrite' : Definition → Term → TC ⊤
@@ -132,17 +190,14 @@ deriveWrite' (Reflection.record-type c fs) met = {!!}
 deriveWrite' (data-type p cs) met = do
   ts ← mapM monadTCM getType cs
   let clauses = (Data.List.Base.map (uncurry consClause) (zip cs ts))
-      errs    = concat (Data.List.Base.map nameStr (zip cs ts))
-  let term = telWrite 5
-  {!!}
-  typeError errs
-deriveWrite' _ _ = typeError (strErr "Write instances can only be derived for data and record types" ∷ [])
+      term = telWrite 5
+  typeError (termErr (pat-lam clauses []) ∷ [])
+-- unify met (pat-lam clauses [])
+{-# CATCHALL #-}
+deriveWrite' _ _  = typeError (strErr "Write instances can only be derived for data and record types" ∷ [])
 
 macro
   deriveWrite : Name → Term → TC ⊤
   deriveWrite nm met = do
     d ← getDefinition nm
     deriveWrite' d met
-
-data Test : Set where
-  a : ℕ → (a : ℕ) → ℕ → Test

From adc9d592f34fe08200634f21fdaab56d38868572 Mon Sep 17 00:00:00 2001
From: Silas Hayes-Williams <psysh13@nottingham.ac.uk>
Date: Tue, 25 Aug 2026 17:08:49 -0400
Subject: [PATCH 24/24] [skip ci] Experiment more with reflection

---
 src/Text/Write.agda          |   1 +
 src/Text/Write/Deriving.agda | 360 ++++++++++++++++++++++++++++++-----
 2 files changed, 313 insertions(+), 48 deletions(-)

diff --git a/src/Text/Write.agda b/src/Text/Write.agda
index a117c1fbab..acfdf04866 100644
--- a/src/Text/Write.agda
+++ b/src/Text/Write.agda
@@ -25,6 +25,7 @@ private
     A : Set a
 
 record Write (A : Set a) :  Set a where
+  constructor mkWrite
   field
     writesPrecList :  Precedence → A → List Char → List Char
 
diff --git a/src/Text/Write/Deriving.agda b/src/Text/Write/Deriving.agda
index 40335fbe53..25a181084c 100644
--- a/src/Text/Write/Deriving.agda
+++ b/src/Text/Write/Deriving.agda
@@ -14,21 +14,35 @@ module Text.Write.Deriving where
 --   ∙ https://github.com/UlfNorell/agda-prelude/blob/master/src/Tactic/Deriving/Eq.agda
 --   ∙ https://github.com/alhassy/gentle-intro-to-reflection
 
-open import Data.List.Base using (_∷_; []; List; concat; _++_; zip)
+open import Data.Bool.Base using (Bool; false; true; if_then_else_)
+open import Data.Char.Properties using (_≡?_)
+open import Data.List.Base using (_∷_; []; [_]; List; concat; _++_; zip; wordsBy; length; map)
 open import Data.List.Effectful
-open import Data.Nat.Base using (ℕ; _+_)
-open import Data.Nat.Instances using (NatWrite)
+open import Data.Maybe.Base using (just; nothing; fromMaybe; Maybe) renaming (_>>=_ to _>>=Maybe_)
+open import Data.Nat.Base using (ℕ; _+_; ∣_-_∣′)
+open import Data.Nat.Instances
 open TraversableM using (mapM)
+open import Data.String.Base using (toList; fromList; String) renaming (_++_ to _++s_)
 open import Data.Unit using (⊤)
 open import Data.Product.Base using (_×_; _,_; uncurry; proj₁; proj₂)
+open import Function.Base using (_∘_)
 open import Reflection
-open import Reflection.AST.Term using (Telescope; Clause)
+open import Reflection.AST.Show using (showName)
+open import Reflection.AST.Term using (Telescope; Clause; unknown; getName)
+open import Reflection.AST.Meta using (showMeta)
+open import Reflection.AST.Name using (_≡ᵇ_)
+open import Reflection.AST.Argument using (iArg; unArg)
 open import Reflection.TCM
 open import Reflection.TCM.Effectful using () renaming (monad to monadTCM)
+open import Relation.Binary.PropositionalEquality using (_≡_)
 open import Text.Write using (Write; Char; Precedence)
 
+open import Level using (Level; suc; zero)
+  
 data Test : Set where
-  a : ℕ → (x : ℕ) → ℕ → Test
+  a_-_-_ : ℕ → ℕ → ℕ → Test
+  a' : Test
+  a'' : {!!}
 
 {-
 Should this be placed in Tactic.DerivingWrite?
@@ -55,10 +69,23 @@ Steps:
 
    {a : Level} {A : Set} {{ Write a }} {{ Write A }} → Write (List A)
 
+3. Create a pat-lam for the record field of Write, but use outer de Bruijn indices
+   to fetch write instances
 
-3. For records, print in record syntax (record { x = y, ... }), recursively
+   When writing values of a constructor, recursively call write on them. For
+   other types, use a map of instances for de Bruijn indices. But for the current type
+   (in the case of induction), the name of the defined function must be used.
+
+   NOTE: map return an arg instead of a nat 
+
+4. For data types, create a clause for each constructor and produce a pat-lam out of it
+
+OUTPUT:
+
+For records, print in record syntax (record { x = y, ... }), recursively
    calling write on fields
-4. For data, get fixity of constructor and recursively call write, intertwining
+
+For data, get fixity of constructor and recursively call write, intertwining
    parts of the constructors name in a way that properly aligns with fixity
 
    (e.g. print x ∷ [] as "x ∷ []", not "_∷_ x []")
@@ -66,15 +93,29 @@ Steps:
 Reflection notes:
 - Prelude has a lot of machinery that should be moved over
 - Should derive *own* type so we know the exact order things are in
-- Instance arguments MUST be included in telescope and argument patterns, and must be provided
-  to calls to writesPrecList, as opposed to say instance resolution within the definition.
-  (at least I think)
+- WRONG
 - Clause takes telescope of arguments (i.e. the type of the given function without the return value)
   AND a list of patterns applied to those arguments. If no pattern matching is applied, just the
   deBruijin index within a var pattern should be given.
+- Pat lam for pattern matching, lam for normal
+- Instances can't be handled as arguments in pat-lam, but can in lam
+- Recursion can't be done within a lam. Must define a top level name and refer to that
 
+Instance Notes:
+- Recursive calls have to be handled in a helper function, whose type signature
+  is the type of the field in Write. 
 -}
 
+------------------------------------------------------------------------
+-- List Char utils
+
+last : {a : Level} {A : Set a} → A → List A → A
+last x [] = x
+last x (y ∷ ys) = last y ys
+
+unqualify : List Char → List Char
+unqualify str = last str (wordsBy (_≡?_ '.') str)
+
 ------------------------------------------------------------------------
 -- Machinery for deriving things
 
@@ -86,22 +127,19 @@ telView (pi x (abs y b)) = ((y , x) ∷ (proj₁ telVb)) , proj₂ telVb
 {-# CATCHALL #-}
 telView x                = [] , x
 
+getTel : Type → Telescope
+getTel = proj₁ ∘ telView
+
+getCore : Type → Type
+getCore = proj₂ ∘ telView
+
 -- Construct a Type out of a Telescope and Core Type
 telToType : Telescope → Type → Type
 telToType tel core = {!!}
 
--- Return a list of all types that appear in the constructors
--- or fields of a data or record type that aren't the type itself
--- in order of appearance
---
--- e.g. for
--- data X : Set where
---   c₁ : ℕ → X
---   c₂ : Bool → X → X
---
--- This should return ℕ, Bool
-consArgTypes : Type → List Type
-consArgTypes = {!!}
+-- Return a list of all types that appear in a list of constructors in order of appearance
+conArgTypes : Type → List Type
+conArgTypes t = map (unArg ∘ proj₂) (getTel t)
 
 instanceArg : Arg Name
 instanceArg = arg (arg-info instance′ defaultModality) (quote Write)
@@ -111,7 +149,7 @@ instanceArg = arg (arg-info instance′ defaultModality) (quote Write)
 -- e.g. for Write List this returns
 --      {a : Level} {A : Set a} {{ Write A }}
 instanceTel : Name → Name → TC Telescope
-instanceTel = {!!}
+instanceTel cls inst = {!!}
 
 -- Derive the type of an instance for a given record type,
 -- prepending all required instances to the telescope
@@ -129,21 +167,43 @@ telStr : Telescope → List ErrorPart
 telStr [] = strErr "[]" ∷ []
 telStr ((nm , arg i t) ∷ xs) = strErr nm ∷ termErr t ∷ (telStr xs)
 
+-- NOTE: a lot of these are likely already defined somewhere
+
 vra : {A : Set} → A → Arg A
 vra = arg (arg-info visible (modality relevant quantity-0))
 
+hra : {A : Set} → A → Arg A
+hra = arg (arg-info hidden (modality relevant quantity-0))
+
 vrv :  ℕ → List (Arg Term) → Arg Term
 vrv n args = arg (arg-info visible (modality relevant quantity-0)) (var n args)
 
 vri : ℕ → Arg Term
 vri n = arg (arg-info instance′ (modality relevant quantity-0)) (var n [])
 
+vrit : {A : Set} → A → Arg A
+vrit = arg (arg-info instance′ (modality relevant quantity-0))
+
 vrv' : ℕ → Arg Term
 vrv' n = vrv n []
 
 ------------------------------------------------------------------------
 -- Machinery specific to Write
 
+-- Produce the type for the auxiliary function that does the
+-- actual writing (i.e. has the expanded type)
+--
+-- Example: writeAuxType List
+--          ↦ {a : Set} {A : Set a} → {{ Write A }} → Precedence → List A → List Char → List Char
+writeAuxType : Name → TC Type
+writeAuxType nm = {!!}
+
+-- Produce the type of a Write instance for a given class.
+--
+-- Example: writeType List ↦ {a : Set} {A : Set a} → {{ Write A }} → Write (List A) 
+writeType : Name → TC Type
+writeType nm = {!!}
+
 -- TODO: doc comment can be better
 -- given the telescope for a constructor, produce the whole telescope for
 -- its clause
@@ -151,53 +211,257 @@ vrv' n = vrv n []
 conTel : Telescope → Telescope
 conTel tel =  ("str" , (vra (quoteTerm (List Char)))) ∷ (tel ++ ("prec" , (vra (quoteTerm Precedence))) ∷ [])
 
+recTel : Type → Telescope
+recTel rec = conTel [ ("rec" , (vra rec)) ]
+
 ------------------------------------------------------------------------
 -- Derive macro for Write
 
--- test implementation, no bracketing
+-- NOTE: lots of experimenting
+
+next : List (List Char) → (List Char) × (List (List Char))
+next [] = [] , []
+next (x ∷ xs) = x , xs
+
+-- Take a list of terms and turn it into a term of a list of said terms
+quoteList : List Term → Term
+quoteList [] = con (quote List.[]) []
+quoteList (x ∷ xs) = con (quote _∷_) (vra x ∷ [ (vra (quoteList xs)) ])
+
+padSep : List Char → List Char
+padSep [] = []
+padSep xs@(_ ∷ _) = ' ' ∷ xs ++ [ ' ' ]
+
+open Write {{...}}
 
--- concat write calls to each argument in a telescope for Write
--- suc suc N is used because we have Prec → A → List Char → List Char, so everything is one more away
--- because of the List Char taken as an argument
+-- TODO: probably a better interface/function than this
+--         len ≥ length (tel)
+--         Between values    Inst Map    num vals  tel
+telWrite' : List (List Char) → ℕ → Telescope → List Term
+telWrite' seps len [] = [ con (quote List.[]) [] ]
+telWrite' seps len ((nm , typ) ∷ xs) = sepTerm ∷ pref ∷ 
+                                       (def (quote writesPrecList)
+                                       (prec ∷ conVal ∷ vra suff ∷ [])) ∷
+                                       (telWrite' seps' len xs)
+          where
 
-telWrite : ℕ → Term
-telWrite ℕ.zero = con (quote List.[]) []
-telWrite (ℕ.suc n) = def (quote _++_) (vra (def (quote Write.writesPrecList) (vri 5 ∷ vrv' 0 ∷ vrv' (1 + n) ∷ vrv' 4 ∷ [])) ∷ (vra (telWrite n)) ∷ [])
--- telWrite 0 = con (quote (List.[])) []
--- telWrite (suc n) = def (quote _++_) ({!!} ∷ {!!})
+            sepSeps : List Char × (List (List Char))
+            sepSeps = next seps
+
+            sep : List Char
+            sep = padSep (proj₁ sepSeps)
+
+            -- there must be a better way! maybe we should use strings
+            sepTerm : Term
+            sepTerm = def (quote toList) ((vra (lit (string (fromList sep)))) ∷ [])
+
+            seps' : List (List Char)
+            seps' = proj₂ sepSeps
+            
+            inst : Arg Term
+            inst = arg (arg-info instance′ (modality relevant quantity-0)) unknown
+
+            str : Arg Term
+            str = vrv' (len + 1)
+
+            pref : Term
+            pref = quoteTerm (toList "(")
+
+            suff : Term
+            suff = quoteTerm (toList ")")
+            
+            strBrack : Arg Term
+            strBrack = vra (def (quote _++_) (vra (quoteTerm (toList ") ")) ∷ [ str ]))
+
+            conVal : Arg Term
+            conVal = vrv' (∣ len - (length xs) ∣′)
+
+            prec : Arg Term
+            prec = vrv' 0
+
+telWrite : List (List Char) → ℕ → Telescope → Term
+telWrite seps n tel = def (quote concat) [ (vra (quoteList (telWrite' seps n tel))) ]
 
 varPat : ℕ → Arg Pattern
 varPat n = vra (Pattern.var n)
 
+insPat : ℕ → Arg Pattern
+insPat n = vrit (Pattern.var n)
+
 telToVarPat : ℕ → List (Arg Pattern)
 telToVarPat 0 = []
 telToVarPat (ℕ.suc n) = telToVarPat n ++ (varPat (1 + n)) ∷ []
 
+conNameTerm : Name → Term
+conNameTerm nm = def (quote unqualify) (vra (def (quote toList) (nmLit ∷ [])) ∷ [])
+  where
+    nmLit : Arg Term
+    nmLit = vra (lit (string (showName nm)))
+
+-- get a list of constructor seperators
+-- with an additional empty seperator
+-- if the constructor mixfix starts with a _
+conSeps : List Char → List (List Char)
+conSeps [] = []
+conSeps ('_' ∷ str) = [] ∷ conSeps str
+conSeps str@(_ ∷ _) = wordsBy (_≡?_ '_') str
+
+-- clause when the constructor of a data type is empty
+emptyCons : Name → Clause
+emptyCons nm = Clause.clause (conTel []) ((varPat 0) ∷ conPat ∷ ((varPat 1) ∷ [])) (conNameTerm nm)
+  where
+    conPat : Arg Pattern
+    conPat = vra (Pattern.con nm [])
+
 -- derive the clause for a single constructor
 consClause : Name → Type → Clause
 consClause nm t with telView t
-... | tel , _ = Clause.clause (conTel tel) (varPat 0 ∷ (vra (Pattern.con nm (telToVarPat (Data.List.Base.length tel)))) ∷ varPat 4 ∷ []) (telWrite (Data.List.Base.length tel))
+... | [] , _ = emptyCons nm
+... | tel@(_ ∷ _) , _ = Clause.clause (conTel tel) (varPat 0 ∷ conPat ∷ strPat ∷ []) writeTerm
+  where
+    precPat : Arg Pattern
+    precPat = varPat 0
+
+    telLen : ℕ
+    telLen = Data.List.Base.length tel
+    
+    conPat : Arg Pattern
+    conPat = vra (Pattern.con nm (telToVarPat telLen))
+
+    strPat : Arg Pattern
+    strPat = varPat (telLen + 1)
+
+    nmStr : List Char
+    nmStr = unqualify (toList (showName nm))
+
+    writeTerm : Term
+    writeTerm = telWrite (conSeps nmStr) telLen tel
+
+-- Prec → Rec → LC → LC
+recordOutputs : Name → List (Arg Name) → List Term
+recordOutputs nm [] = [ (quoteTerm (toList "}")) ]
+recordOutputs nm (x ∷ fs) = def (quote toList) [ vra (lit (string fieldName)) ] ∷
+                            (quoteTerm (toList " = ")) ∷
+                            def (quote writesPrecList) (vrv' 0 ∷ fieldArg ∷ vrv' 2 ∷ []) ∷
+                            (quoteTerm (toList "; ")) ∷
+                            recordOutputs nm fs
+  where
+    fieldArg : Arg Term
+    fieldArg = vra (def (unArg x) [ vrv' 1 ])
+
+    fieldName : String
+    fieldName = fromList (unqualify (toList (showName (unArg x))))
+    
+
+recordTerm : Name → List (Arg Name) → Term
+recordTerm nm fs = def (quote concat) [
+                   (vra (quoteList (prefix ∷ outs))) ]
+           where
+             prefix : Term
+             prefix = quoteTerm (toList "record { ")
+
+             outs : List Term
+             outs = recordOutputs nm fs
 
-deriveWriteFun : Name → Definition → Definition
-deriveWriteFun nm (Reflection.data-type pars cs) = function (Data.List.Base.map (uncurry consClause) {!!})
-deriveWriteFun nm (Reflection.record-type c fs) = {!!}
-{-# CATCHALL #-}
-deriveWriteFun _ _ = function []
 -- cs in data-type contains actual constructor names
 -- 'name' in data-cons is just name of data type itself
-deriveWrite' : Definition → Term → TC ⊤
-deriveWrite' (Reflection.record-type c fs) met = {!!}
-deriveWrite' (data-type p cs) met = do
+computeAuxWrite : Definition → TC (List Clause)
+computeAuxWrite (record-type c fs) = do
+  t ← getType c
+  let tel = recTel t
+      pats = varPat 0 ∷ varPat 1 ∷ varPat 2 ∷ []
+      body = recordTerm c fs
+      clause = Clause.clause tel pats body
+  -- typeError [ termErr (pat-lam [ clause ] []) ]
+  pure [ clause ]
+computeAuxWrite (data-type p cs) = do
   ts ← mapM monadTCM getType cs
+  let tels = Data.List.Base.map telView ts
   let clauses = (Data.List.Base.map (uncurry consClause) (zip cs ts))
-      term = telWrite 5
-  typeError (termErr (pat-lam clauses []) ∷ [])
--- unify met (pat-lam clauses [])
+  -- typeError (termErr (pat-lam clauses []) ∷ [])
+  pure clauses
 {-# CATCHALL #-}
-deriveWrite' _ _  = typeError (strErr "Write instances can only be derived for data and record types" ∷ [])
+computeAuxWrite _  = typeError (strErr "Write instances can only be derived for data and record types" ∷ [])
 
 macro
-  deriveWrite : Name → Term → TC ⊤
-  deriveWrite nm met = do
+  deriveWriteDef : Name → Term → TC ⊤
+  deriveWriteDef nm met = do
     d ← getDefinition nm
-    deriveWrite' d met
+    writeClauses ← computeAuxWrite d
+    unify met (pat-lam writeClauses [])
+
+-- Declare a Write instance with a given name for a given
+-- type.
+--
+-- e.g.
+-- declareWriteInstance 'ListWrite' (quote List)
+-- ↦
+-- ListWrite : {a : Level} {A : Set a} {{Write A}} → Write (List A)
+declareWriteInstance : Name → Name → TC ⊤
+declareWriteInstance fnm class = do
+  t ← writeType class
+  declareDef (iArg fnm) t
+
+-- Define the Write instance of a given name for a given
+-- type.
+--
+-- The instance must already be declared, e.g. via declareWriteInstance.
+-- This also declares another top-level name with the 'expanded' type of Write
+-- (Precedence → A → List Char → List Char), and attaches the 'actual' definition to that.
+-- For a type T, the name of this auxillary function is "write[T]".
+-- 
+-- The instance then simply constructs a record of Write out of it. This is to allow
+-- for the definition to recurse on itself.
+defineWriteInstance : Name → Name → TC ⊤
+defineWriteInstance inm class = do
+  fnm ← freshName ("write[" ++s showName inm ++s "]")
+  ft ← writeAuxType class
+  
+  declareDef (vra fnm) ft
+ 
+  defineFun inm (Clause.clause [] [] (con (quote Text.Write.mkWrite) [ vra (def fnm []) ]) ∷ [])
+
+  classDef ← getDefinition class
+  clauses ← computeAuxWrite classDef
+  defineFun fnm clauses
+  
+  pure _
+
+-- Usage (example for List):
+--  unquoteDecl ListWrite = deriveWriteI ListWrite (quote List)
+deriveWriteI : Name → Name → TC ⊤
+deriveWriteI iname typ = (declareWriteInstance iname typ) >> (defineWriteInstance iname typ)
+
+record Test' : Set where
+  field
+    a : ℕ
+    b : ℕ
+    
+g : Precedence → Test' → List Char → List Char
+g = deriveWriteDef Test'
+
+test' : Test'
+test' .Test'.a = 5
+test' .Test'.b = 99
+f : String
+f = fromList (g unrelated test' [])
+
+{-
+λ { prec (a _ - _ - _) str
+      → concat
+        (toList " a " ∷
+         toList "(" ∷
+         .Write.writesPrecList prec _ (toList ")") ∷
+         concat
+         (toList " - " ∷
+          toList "(" ∷
+          .Write.writesPrecList prec _ (toList ")") ∷
+          concat
+          (toList " - " ∷
+           toList "(" ∷ .Write.writesPrecList prec _ (toList ")") ∷ [] ∷ [])
+          ∷ [])
+         ∷ [])
+  ; prec a' str → unqualify (toList "Text.Write.Deriving.Test.a'")
+  ; prec a'' str → unqualify (toList "Text.Write.Deriving.Test.a''")
+  }
+-}