[ fix #667 ] add parsing and showing for numeric types

Author: gallais

CHANGELOG.md

@@ -146,6 +146,16 @@ Deprecated names
   filter⁺         ↦ filter-⊆
   ```
 
+* In `Data.Integer`:
+    ```agda
+  show ↦ Data.Integer.Show.show
+  ```
+
+* In `Data.Rational`:
+    ```agda
+  show ↦ Data.Rational.Show.show
+  ```
+
 New modules
 -----------
 
@@ -222,6 +232,13 @@ New modules
   System.Environment.Primitive
   ```
 
+* Added the following `Show` modules:
+  ```agda
+  Data.Fin.Show
+  Data.Integer.Show
+  Data.Rational.Show
+  ```
+
 * Added bindings for Haskell's `System.Exit`:
   ```
   System.Exit
@@ -486,6 +503,16 @@ Other minor additions
   lines   : String → List String
   ```
 
+* Added new function to `Data.Maybe.Base`:
+  ```agda
+  when : Bool → A → Maybe A
+  ```
+
+* Added new function to `Data.Nat.Show`:
+  ```agda
+  readMaybe : (base : ℕ) → {base≤16 : True (base ≤? 16)} → String → Maybe ℕ
+  ```
+
 * Added new functions to `Data.Tree.AVL`:
   ```agda
   foldr : (∀ {k} → Val k → A → A) → A → Tree V → A

src/Data/Fin/Show.agda

@@ -0,0 +1,28 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Showing finite numbers
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Fin.Show where
+
+open import Data.Fin.Base using (Fin; toℕ; fromℕ<)
+open import Data.Maybe.Base using (Maybe; nothing; just; _>>=_)
+open import Data.Nat as ℕ using (ℕ; _≤?_; _<?_)
+import Data.Nat.Show as ℕ
+open import Data.String.Base using (String)
+open import Function.Base
+open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Decidable using (True)
+
+show : ∀ {n} → Fin n → String
+show = ℕ.show ∘′ toℕ
+
+readMaybe : ∀ {n} base {base≤16 : True (base ≤? 16)} → String → Maybe (Fin n)
+readMaybe {n} base {pr} str = do
+  nat ← ℕ.readMaybe base {pr} str
+  case nat <? n of λ where
+    (yes pr) → just (fromℕ< pr)
+    (no ¬pr) → nothing

src/Data/Integer.agda

@@ -11,10 +11,6 @@
 
 module Data.Integer where
 
-import Data.Nat.Show as ℕ
-open import Data.Sign as Sign using (Sign)
-open import Data.String.Base using (String; _++_)
-
 ------------------------------------------------------------------------
 -- Re-export basic definition, operations and queries
 
@@ -23,7 +19,20 @@ open import Data.Integer.Properties public
   using (_≟_; _≤?_; _<?_)
 
 ------------------------------------------------------------------------
--- Conversions
+-- Deprecated
+
+-- Version 0.17
+
+open import Data.Integer.Properties public
+  using (◃-cong; drop‿+≤+; drop‿-≤-)
+  renaming (◃-inverse to ◃-left-inverse)
+
+-- Version 1.5
+-- Show
+
+import Data.Nat.Show as ℕ
+open import Data.Sign as Sign using (Sign)
+open import Data.String.Base using (String; _++_)
 
 show : ℤ → String
 show i = showSign (sign i) ++ ℕ.show ∣ i ∣
@@ -32,11 +41,7 @@ show i = showSign (sign i) ++ ℕ.show ∣ i ∣
   showSign Sign.- = "-"
   showSign Sign.+ = ""
 
-------------------------------------------------------------------------
--- Deprecated
-
--- Version 0.17
-
-open import Data.Integer.Properties public
-  using (◃-cong; drop‿+≤+; drop‿-≤-)
-  renaming (◃-inverse to ◃-left-inverse)
+{-# WARNING_ON_USAGE show
+"Warning: show was deprecated in v1.5.
+Please use Data.Integer.Show's show instead."
+#-}

src/Data/Integer/Show.agda

@@ -0,0 +1,24 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Showing integers
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Integer.Show where
+
+open import Data.Integer.Base using (ℤ; +_; -[1+_])
+open import Data.Nat.Base using (suc)
+open import Data.Nat.Show using () renaming (show to showℕ)
+open import Data.String.Base using (String; _++_)
+
+------------------------------------------------------------------------
+-- Show
+
+-- Decimal notation
+-- Time complexity is O(log₁₀(n))
+
+show : ℤ → String
+show (+ n)    = showℕ n
+show -[1+ n ] = "-" ++ showℕ (suc n)

src/Data/Maybe/Base.agda

@@ -106,6 +106,11 @@ _<∣>_ : Maybe A → Maybe A → Maybe A
 just x  <∣> my = just x
 nothing <∣> my = my
 
+-- Just when the boolean is true
+
+when : Bool → A → Maybe A
+when b c = map (const c) (boolToMaybe b)
+
 ------------------------------------------------------------------------
 -- Aligning and zipping
 

src/Data/Nat/Show.agda

@@ -8,42 +8,72 @@
 
 module Data.Nat.Show where
 
-open import Data.Char as Char using (Char)
+open import Data.Bool.Base using (_∧_)
+open import Data.Char.Base as Char using (Char)
 open import Data.Digit using (showDigit; toDigits; toNatDigits)
-open import Function.Base using (_∘_; _$_)
-open import Data.List.Base using (List; []; _∷_; map; reverse)
+open import Data.List.Base as List using (List; []; _∷_)
+open import Data.List.Categorical using (module TraversableA)
+open import Data.Maybe.Base as Maybe using (Maybe; nothing; _<∣>_; when)
+import Data.Maybe.Categorical as Maybe
 open import Data.Nat
 open import Data.Product using (proj₁)
 open import Data.String as String using (String)
+open import Function.Base
 open import Relation.Nullary.Decidable using (True)
 
 ------------------------------------------------------------------------
--- Conversion from unary representation to the representation by the
--- given base.
+-- Read
 
-toDigitChar : (n : ℕ) → Char
-toDigitChar n = Char.fromℕ (n + (Char.toℕ '0'))
+readMaybe : ∀ base {base≤16 : True (base ≤? 16)} → String → Maybe ℕ
+readMaybe _ "" = nothing
+readMaybe base = Maybe.map convert
+              ∘′ TraversableA.mapA Maybe.applicative readDigit
+              ∘′ String.toList
 
-toDecimalChars : ℕ → List Char
-toDecimalChars = map toDigitChar ∘ toNatDigits 10
+  where
+
+    convert : List ℕ → ℕ
+    convert = List.foldl (λ acc d → base * acc + d) 0
+
+    char0 = Char.toℕ '0'
+    char9 = Char.toℕ '9'
+    chara = Char.toℕ 'a'
+    charf = Char.toℕ 'f'
+
+    readDigit : Char → Maybe ℕ
+    readDigit c = digit Maybe.>>= λ n → when (n <ᵇ base) n where
+
+      charc = Char.toℕ c
+
+      dec = when ((char0 ≤ᵇ charc) ∧ (charc ≤ᵇ char9)) (charc ∸ char0)
+      hex = when ((chara ≤ᵇ charc) ∧ (charc ≤ᵇ charf)) (10 + charc ∸ chara)
+      digit = dec <∣> hex
 
 ------------------------------------------------------------------------
 -- Show
 
+-- Decimal notation
 -- Time complexity is O(log₁₀(n))
 
+toDigitChar : ℕ → Char
+toDigitChar n = Char.fromℕ (n + Char.toℕ '0')
+
+toDecimalChars : ℕ → List Char
+toDecimalChars = List.map toDigitChar ∘′ toNatDigits 10
+
 show : ℕ → String
 show = String.fromList ∘ toDecimalChars
 
+-- Arbitrary base betwen 2 & 16.
 -- Warning: when compiled the time complexity of `showInBase b n` is
 -- O(n) instead of the expected O(log(n)).
 
 charsInBase : (base : ℕ)
               {base≥2 : True (2 ≤? base)}
               {base≤16 : True (base ≤? 16)} →
               ℕ → List Char
-charsInBase base {base≥2} {base≤16} = map (showDigit {base≤16 = base≤16})
-                                    ∘ reverse
+charsInBase base {base≥2} {base≤16} = List.map (showDigit {base≤16 = base≤16})
+                                    ∘ List.reverse
                                     ∘ proj₁
                                     ∘ toDigits base {base≥2 = base≥2}
 

src/Data/Rational.agda

@@ -8,26 +8,30 @@
 
 module Data.Rational where
 
-open import Data.Integer as ℤ using (ℤ; +_)
-open import Data.String using (String; _++_)
-
 ------------------------------------------------------------------------
 -- Publicly re-export contents of core module and queries
 
 open import Data.Rational.Base public
 open import Data.Rational.Properties public
   using (_≟_; _≤?_; _<?_)
 
-------------------------------------------------------------------------
--- Method for displaying rationals
-
-show : ℚ → String
-show p = ℤ.show (↥ p) ++ "/" ++ ℤ.show (↧ p)
-
 ------------------------------------------------------------------------
 -- Deprecated
 
 -- Version 1.0
 
 open import Data.Rational.Properties public
   using (drop-*≤*; ≃⇒≡; ≡⇒≃)
+
+-- Version 1.5
+
+import Data.Integer.Show as ℤ
+open import Data.String using (String; _++_)
+
+show : ℚ → String
+show p = ℤ.show (↥ p) ++ "/" ++ ℤ.show (↧ p)
+
+{-# WARNING_ON_USAGE show
+"Warning: show was deprecated in v1.5.
+Please use Data.Rational.Show's show instead."
+#-}

src/Data/Rational/Show.agda

@@ -0,0 +1,16 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Showing rational numbers
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Rational.Show where
+
+import Data.Integer.Show as ℤ
+open import Data.Rational.Base
+open import Data.String.Base using (String; _++_)
+
+show : ℚ → String
+show p = ℤ.show (↥ p) ++ "/" ++ ℤ.show (↧ p)

src/Text/Printf.agda

@@ -20,10 +20,10 @@ open import Function.Nary.NonDependent
 open import Function
 open import Strict
 
-import Data.Char.Base as Cₛ
-import Data.Integer   as ℤₛ
-import Data.Float     as Fₛ
-import Data.Nat.Show  as ℕₛ
+import Data.Char.Base    as Cₛ
+import Data.Integer.Show as ℤₛ
+import Data.Float        as Fₛ
+import Data.Nat.Show     as ℕₛ
 
 open import Text.Format as Format hiding (Error)
 open import Text.Printf.Generic