Add Show class

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"

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.Write using (Write)
+
 instance
   ℤ-≡-isDecEquivalence = isDecEquivalence _≡?_
   ℤ-≤-isDecTotalOrder = ≤-isDecTotalOrder
+
+instance
+  open Write
+  IntWrite : Write ℤ
+  IntWrite .writesPrecList _ i str = toList (showℤ i) ++ str

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)
@@ -22,13 +22,15 @@ 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 (NatWrite)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 open import Relation.Binary.PropositionalEquality.Properties
   using (isDecEquivalence)
 open import Relation.Binary.TypeClasses
   using (IsDecTotalOrder; IsDecEquivalence; _≈?_)
+open import Text.Write
 
 private
   variable
@@ -58,3 +60,22 @@ instance
                              → {{IsDecTotalOrder _≈_ _≼_}}
                              → IsDecTotalOrder (Pointwise _≈_) (Lex-≤ _≈_ _≼_)
   List-Lex-≤-isDecTotalOrder {{≼-isDecTotalOrder}} = ≤-isDecTotalOrder ≼-isDecTotalOrder
+
+------------------------------------------------------------------------
+-- List write
+
+open Write {{...}}
+
+instance
+  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 '['
+      listWrite' : {{ Write A }} → Precedence → List Char → List A → List Char
+      listWrite' prec str = foldr (λ x str → ',' ∷ writesPrecList prec x str) (']' ∷ str)
+
+-- some examples to write the instances working
+private
+  test[ℕ] : String
+  test[ℕ] = write (5 ∷ 2 ∷ 12 ∷ 42 ∷ [])

src/Data/List/Unsafe/Instances.agda

@@ -0,0 +1,27 @@
+------------------------------------------------------------------------
+-- 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
+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))

src/Data/Maybe/Unsafe/Instances.agda

@@ -0,0 +1,24 @@
+------------------------------------------------------------------------
+-- 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
+open import Level using (Level)
+
+private
+  variable
+    a : Level
+    A : Set a
+
+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"

src/Data/Nat/Instances.agda

@@ -8,10 +8,32 @@
 
 module Data.Nat.Instances where
 
+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 (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
   ℕ-≡-isDecEquivalence = isDecEquivalence _≡?_
   ℕ-≤-isDecTotalOrder = ≤-isDecTotalOrder
+
+instance
+  open Write
+  NatWrite : Write ℕ
+  NatWrite .writesPrecList _ n str = (toList (showℕ n)) ++ str
+
+instance
+  open Read {{...}}
+  NatRead : Read ℕ
+  NatRead .readsPrecList prec str = do
+    let (digits , leftover) = spanᵇ isDigit str
+    num ← readMaybe 10 (fromList digits)
+    just (num , leftover)

src/Data/Nat/Unsafe/Instances.agda

@@ -0,0 +1,18 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Unsafe instances for Nat
+------------------------------------------------------------------------
+
+{-# OPTIONS --with-K #-}
+
+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)

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,20 @@ 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
+
+  pretty : A → String
+  pretty = render ∘ pPrint

src/Text/Read.agda

@@ -0,0 +1,41 @@
+------------------------------------------------------------------------
+-- 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; 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; _$_; id)
+open import Level using (Level)
+
+private
+  variable
+    a : Level
+    A : Set a
+
+record Read (A : Set a) : Set a where
+  field
+    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

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
+

src/Text/Write.agda

@@ -0,0 +1,45 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Write class
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe  #-}
+
+module Text.Write 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; 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)
+open import Function.Base using (_∘_; const; _$_)
+open import Level using (Level)
+
+private
+  variable
+    a : Level
+    A : Set a
+
+record Write (A : Set a) :  Set a where
+  field
+    writesPrecList :  Precedence → A → List Char → List Char
+
+  writePrecList : Precedence → A → List Char
+  writePrecList prec x =  writesPrecList prec x []
+
+  writesPrec : Precedence → A → String → String
+  writesPrec prec x str = fromList (writesPrecList prec x (toList str))
+
+  writePrec : Precedence → A → String
+  writePrec prec x = fromList (writesPrecList prec x [])
+
+  write : A → String
+  write = writePrec Precedence.unrelated
+
+  writeMaybe : Maybe A → String
+  writeMaybe nothing = ""
+  writeMaybe (just x) = write x