← Back to branch summary

~ubuntu-branches/ubuntu/precise/agda-stdlib/precise

« 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-02-25 22:28:40 UTC
  • mfrom: (1.1.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20110225222840-jt16gl302kca7h0g
Tags: 0.5-1~ubuntu1
https://launchpad.net/bugs/725364
http://bugs.debian.org/573807
http://bugs.debian.org/598708

* Upload to Ubuntu from Debian's VCS due to delays in unstable caused by
  the GHC 7 transition (LP: #725364)
* [ba20206] Make package architecture independent (Closes: #573807, #598708,
  #599958)
* [0fb0600] Standards-Version → 3.9.1, no changes required
* [d3f13b8] Update required Agda version to 2.2.8
* [cc1f5c8] Imported Upstream version 0.4
* [2c82171] Add watch file
* [9251e0b] Imported Upstream version 0.5
* [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

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))