← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda-stdlib/raring-proposed

« back to all changes in this revision

Viewing changes to src/Data/Product/N-ary.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2011-05-24 10:26:15 UTC
  • mfrom: (1.1.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20110524102615-9tontf43bq9ym690
Tags: 0.5-1
http://bugs.debian.org/573807
http://bugs.debian.org/598708
* [9251e0b] Imported Upstream version 0.5
* [ba20206] Make package architecture independent (Closes: #573807, #598708,
  #599958)
* [2c82171] Add watch file
* [0518fa6] No longer need procps | hurd BD as we no longer have the ticker
* [daf2445] Don't use upstream's make install — handled ourselves by
  dh_install
* [1b86533] Update watchfile to point at new location
* [637f47d] Remove debian/gbp.conf as we are no longer building for exp
* [cc88671] Require Agda 2.2.10
* [e99dab5] Set maximum stack size to 1G to prevent overflows in the build
* [251cd1d] Run the test suite manually
* [a7db697] Set the variable in the emacs loading script properly
* [540ca3f] Improve short description
* [6b3e794] Add dependencies on compatible versions of the Agda library
* [7127678] Standards-Version bump to 3.9.2, no changes required
* [9d0ae30] Update to use ghc instead of ghc6
* [3f6879a] Set Maintainer to my d.o email address

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Product/N-ary.agda
 
1
------------------------------------------------------------------------
 
2
-- N-ary products
 
3
------------------------------------------------------------------------
 
4
 
 
5
-- Vectors (as in Data.Vec) also represent n-ary products, so what is
 
6
-- the point of this module? The n-ary products below are intended to
 
7
-- be used with a fixed n, in which case the nil constructor can be
 
8
-- avoided: pairs are represented as pairs (x , y), not as triples
 
9
-- (x , y , unit).
 
10
 
 
11
{-# OPTIONS --universe-polymorphism #-}
 
12
 
 
13
module Data.Product.N-ary where
 
14
 
 
15
open import Data.Nat
 
16
open import Data.Product
 
17
open import Data.Unit
 
18
open import Data.Vec
 
19
open import Function.Inverse
 
20
open import Level
 
21
open import Relation.Binary.PropositionalEquality as P using (_≡_)
 
22
 
 
23
-- N-ary product.
 
24
 
 
25
infix 8 _^_
 
26
 
 
27
_^_ : ∀ {ℓ} → Set ℓ → ℕ → Set ℓ
 
28
A ^ 0           = Lift ⊤
 
29
A ^ 1           = A
 
30
A ^ suc (suc n) = A × A ^ suc n
 
31
 
 
32
-- Conversions.
 
33
 
 
34
⇿Vec : ∀ {a} {A : Set a} n → A ^ n ⇿ Vec A n
 
35
⇿Vec n = record
 
36
  { to         = P.→-to-⟶ (toVec n)
 
37
  ; from       = P.→-to-⟶ fromVec
 
38
  ; inverse-of = record
 
39
    { left-inverse-of  = fromVec∘toVec n
 
40
    ; right-inverse-of = toVec∘fromVec
 
41
    }
 
42
  }
 
43
  where
 
44
  toVec : ∀ {a} {A : Set a} n → A ^ n → Vec A n
 
45
  toVec 0             (lift tt) = []
 
46
  toVec 1             x         = [ x ]
 
47
  toVec (suc (suc n)) (x , xs)  = x ∷ toVec _ xs
 
48
 
 
49
  fromVec : ∀ {a} {A : Set a} {n} → Vec A n → A ^ n
 
50
  fromVec []           = lift tt
 
51
  fromVec (x ∷ [])     = x
 
52
  fromVec (x ∷ y ∷ xs) = (x , fromVec (y ∷ xs))
 
53
 
 
54
  fromVec∘toVec : ∀ {a} {A : Set a} n (xs : A ^ n) →
 
55
                  fromVec (toVec n xs) ≡ xs
 
56
  fromVec∘toVec 0                   (lift tt)    = P.refl
 
57
  fromVec∘toVec 1                   x            = P.refl
 
58
  fromVec∘toVec 2                   (x , y)      = P.refl
 
59
  fromVec∘toVec (suc (suc (suc n))) (x , y , xs) =
 
60
    P.cong (_,_ x) (fromVec∘toVec (suc (suc n)) (y , xs))
 
61
 
 
62
  toVec∘fromVec : ∀ {a} {A : Set a} {n} (xs : Vec A n) →
 
63
                  toVec n (fromVec xs) ≡ xs
 
64
  toVec∘fromVec []           = P.refl
 
65
  toVec∘fromVec (x ∷ [])     = P.refl
 
66
  toVec∘fromVec (x ∷ y ∷ xs) = P.cong (_∷_ x) (toVec∘fromVec (y ∷ xs))