Added function to show Rational at a decimal precision

CHANGELOG.md

@@ -266,8 +266,8 @@ Additions to existing modules
   filter-swap : filter P? ∘ filter Q? ≗ filter Q? ∘ filter P?
   ```
 
-* In `Data.Nat.Divisiblity`:
-  ```agad
+* In `Data.Nat.Divisibility`:
+  ```agda
   m∣n⇒m^o∣n^o : ∀ o → m ∣ n → m ^ o ∣ n ^ o
   n≤o⇒m^n∣m^o : ∀ m → .(n ≤ o) → m ^ n ∣ m ^ o
   ```
@@ -313,13 +313,24 @@ Additions to existing modules
   p*q≢0⇒q≢0     : p * q ≢ 0ℚ → q ≢ 0ℚ
   ```
 
+* In `Data.Rational.Show`:
+  ```agda
+  atPrecision : (n : ℕ) → ℚ → ℤ × Vec ℕ n
+  showAtPrecision : ℕ → ℚ → String
+  ```
+
 * In `Data.Rational.Unnormalised.Properties`:
   ```agda
   p*q≃0⇒p≃0∨q≃0 : p * q ≃ 0ℚᵘ → p ≃ 0ℚᵘ ⊎ q ≃ 0ℚᵘ
   p*q≄0⇒p≄0     : p * q ≄ 0ℚᵘ → p ≄ 0ℚᵘ
   p*q≢0⇒q≢0     : p * q ≄ 0ℚᵘ → q ≄ 0ℚᵘ
   ```
 
+* In `Data.Rational.Unnormalised.Show`:
+  ```agda
+  showAtPrecision : ℕ → ℚᵘ → String
+  ```
+
 * In `Data.Vec.Properties`:
   ```agda
   map-removeAt : ∀ (f : A → B) (xs : Vec A (suc n)) (i : Fin (suc n)) →

src/Data/Rational/Show.agda

@@ -8,9 +8,33 @@
 
 module Data.Rational.Show where
 
+open import Data.Integer.Base using (ℤ; +_; ∣_∣)
 import Data.Integer.Show as ℤ using (show)
-open import Data.Rational.Base using (ℚ; ↥_; ↧_)
+open import Data.Nat.Base using (ℕ; zero; suc)
+open import Data.Nat.Show using (toDigitChar)
+open import Data.Product.Base using (_×_; _,_)
+open import Data.Rational.Base
+  using (ℚ; ↥_; ↧_; _/_; _*_; truncate; fracPart)
 open import Data.String.Base using (String; _++_)
+open import Data.String using (fromVec)
+open import Data.Vec.Base using (Vec; []; _∷_; map)
 
 show : ℚ → String
 show p = ℤ.show (↥ p) ++ "/" ++ ℤ.show (↧ p)
+
+-- The integer part of q,
+-- followed by the first n digits of its decimal representation
+atPrecision : (n : ℕ) → ℚ → ℤ × Vec ℕ n
+atPrecision n q = (truncate q , decimalPart n ((+ 10 / 1) * (fracPart q)))
+  where
+  decimalPart : (n : ℕ) → ℚ → Vec ℕ n
+  decimalPart zero q = []
+-- fracPart q is a (non-negative) proper fraction,
+-- and 0 ≤ num < den implies 0 ≤ 10 num/den < 10,
+-- so everything but position 0 is a proper digit
+  decimalPart (suc n) q
+    = ∣ truncate q ∣ ∷ decimalPart n ((+ 10 / 1) * (fracPart q))
+
+showAtPrecision : ℕ → ℚ → String
+showAtPrecision n q with atPrecision n q
+... | (int , dec) = ℤ.show int ++ "." ++ (fromVec (map toDigitChar dec))

src/Data/Rational/Unnormalised/Show.agda

@@ -9,8 +9,15 @@
 module Data.Rational.Unnormalised.Show where
 
 import Data.Integer.Show as ℤ using (show)
-open import Data.Rational.Unnormalised.Base using (ℚᵘ; ↥_; ↧_)
+open import Data.Nat.Base using (ℕ)
+open import Data.Rational.Base using (fromℚᵘ)
+import Data.Rational.Show as ℚ using (showAtPrecision)
+open import Data.Rational.Unnormalised.Base
+  using (ℚᵘ; ↥_; ↧_)
 open import Data.String.Base using (String; _++_)
 
 show : ℚᵘ → String
 show p = ℤ.show (↥ p) ++ "/" ++ ℤ.show (↧ p)
+
+showAtPrecision : ℕ → ℚᵘ → String
+showAtPrecision n q = ℚ.showAtPrecision n (fromℚᵘ q)