← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/Data/Vec.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2013-04-10 10:30:20 UTC
  • mfrom: (2.1.7 experimental)
  • Revision ID: package-import@ubuntu.com-20130410103020-bcspfz3whyy5iafu
Tags: 0.7-1
* [6d52289] Imported Upstream version 0.7
* [54104d0] Update Depends and Build-Depends for this version, compatible
  with Agda 2.3.2
* [b3ddce4] No need for the .install file to be executable (thanks lintian)
* [a9a6cb7] Standards-Version → 3.9.4, no changes required

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Vec.agda
10
10
open import Data.Nat
11
11
open import Data.Fin using (Fin; zero; suc)
12
12
open import Data.List as List using (List)
13
 
open import Data.Product using (∃; ∃₂; _×_; _,_)
 
13
open import Data.Product as Prod using (∃; ∃₂; _×_; _,_)
14
14
open import Function
15
15
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
16
16
 
84
84
      Vec A n → Vec B n → Vec (A × B) n
85
85
zip = zipWith _,_
86
86
 
 
87
unzip : ∀ {a b n} {A : Set a} {B : Set b} →
 
88
        Vec (A × B) n → Vec A n × Vec B n
 
89
unzip []              = [] , []
 
90
unzip ((x , y) ∷ xys) = Prod.map (_∷_ x) (_∷_ y) (unzip xys)
 
91
 
87
92
foldr : ∀ {a b} {A : Set a} (B : ℕ → Set b) {m} →
88
93
        (∀ {n} → A → B n → B (suc n)) →
89
94
        B zero →
135
140
group (suc n) k .(ys ++ concat zss) | (ys , ._ , refl) | (zss , refl) =
136
141
  ((ys ∷ zss) , refl)
137
142
 
 
143
-- Splits a vector into two "halves".
 
144
 
 
145
split : ∀ {a n} {A : Set a} → Vec A n → Vec A ⌈ n /2⌉ × Vec A ⌊ n /2⌋
 
146
split []           = ([]     , [])
 
147
split (x ∷ [])     = (x ∷ [] , [])
 
148
split (x ∷ y ∷ xs) = Prod.map (_∷_ x) (_∷_ y) (split xs)
 
149
 
138
150
reverse : ∀ {a n} {A : Set a} → Vec A n → Vec A n
139
151
reverse {A = A} = foldl (Vec A) (λ rev x → x ∷ rev) []
140
152