Permalink
Browse files

Added a fromℕ using Data.Digits. If you value your time, don't ask it…

… to convert large naturals
  • Loading branch information...
1 parent 58ddfe4 commit 046f93a31ecd35fd2d41b4e3f9e111168ed9c8bc @copumpkin committed Sep 20, 2010
Showing with 22 additions and 1 deletion.
  1. +22 −1 Data/BitVector/Peano.agda
View
@@ -3,8 +3,13 @@ module Data.BitVector.Peano where
open import Data.BitVector
open import Algebra.FunctionProperties.Core
open import Data.Nat hiding (pred) renaming (suc to Nsuc; zero to Nzero)
-open import Data.Vec
+open import Data.Vec hiding (fromList)
open import Relation.Binary.PropositionalEquality
+
+open import Data.Digit hiding (Bit)
+open import Data.Fin using () renaming (zero to Fzero; suc to Fsuc)
+open import Data.List
+
suc : {n} Op₁ (BitVector n)
suc [] = []
suc (0# ∷ xs) = 1# ∷ xs
@@ -64,3 +69,19 @@ induction P z s x = peanoInduction (λ {x} _ → P x) z s (toPeano x)
toℕ : {n} BitVector n
toℕ = induction _ 0 Nsuc
+
+fromDigit : Digit 2 Bit
+fromDigit Fzero = 0#
+fromDigit (Fsuc Fzero) = 1#
+fromDigit (Fsuc (Fsuc ()))
+
+fromList : {n} List (Digit 2) BitVector n
+fromList [] = zero _
+fromList {Nzero} (x ∷ xs) = []
+fromList {Nsuc n} (x ∷ xs) = fromDigit x ∷ fromList xs
+
+fromℕ : {n} BitVector n
+fromℕ n with toDigits 2 n
+fromℕ .(fromDigits ds) | digits ds = fromList ds
+
+-- TODO: the terrifying proofs that toℕ and fromℕ are inverses

0 comments on commit 046f93a

Please sign in to comment.