← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to test/epic/Prelude/Vec.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
test/epic/Prelude/Vec.agda
1
 
module Prelude.Vec where
2
 
 
3
 
open import Prelude.Nat
4
 
open import Prelude.Fin
5
 
open import Prelude.Unit
6
 
open import Prelude.List using (List ; [] ; _::_)
7
 
infixr 40 _::_
8
 
 
9
 
data Vec (A : Set) :  Nat -> Set where
10
 
  _::_ : forall {n} -> A -> Vec A n -> Vec A (S n)
11
 
  []   : Vec A Z
12
 
 
13
 
infixr 30 _++_
14
 
 
15
 
_++_ : {A : Set}{m n : Nat} -> Vec A m -> Vec A n -> Vec A (m + n)
16
 
[]        ++ ys = ys
17
 
(x :: xs) ++ ys = x :: (xs ++ ys) 
18
 
 
19
 
snoc : {A : Set}{n : Nat} -> Vec A n -> A -> Vec A (S n)
20
 
snoc []        e = e :: []
21
 
snoc (x :: xs) e = x :: snoc xs e
22
 
 
23
 
length : {A : Set}{n : Nat} -> Vec A n -> Nat
24
 
length [] = Z
25
 
length (x :: xs) = 1 + length xs
26
 
 
27
 
length' : {A : Set}{n : Nat} -> Vec A n -> Nat
28
 
length' {n = n} _ = n
29
 
 
30
 
zipWith3 : ∀ {A B C D n} -> (A -> B -> C -> D) -> Vec A n -> Vec B n -> Vec C n -> Vec D n
31
 
zipWith3 f []        []        []        = []
32
 
zipWith3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: zipWith3 f xs ys zs
33
 
 
34
 
zipWith : ∀ {A B C n} -> (A -> B -> C) -> Vec A n -> Vec B n -> {u : Unit} -> Vec C n
35
 
zipWith _ [] [] = []
36
 
zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys {u = unit}
37
 
 
38
 
_!_ : ∀ {A n} -> Vec A n -> Fin n -> A
39
 
x :: xs ! fz = x
40
 
_ :: xs ! fs n = xs ! n
41
 
[] ! ()
42
 
 
43
 
_[_]=_ : {A : Set}{n : Nat} -> Vec A n -> Fin n -> A -> Vec A n
44
 
(a :: as) [ fz ]= e = e :: as
45
 
(a :: as) [ fs n ]= e = a :: (as [ n ]= e)
46
 
[] [ () ]= e
47
 
 
48
 
map : ∀ {A B n}(f : A -> B)(xs : Vec A n) -> Vec B n
49
 
map f []        = []
50
 
map f (x :: xs) = f x :: map f xs
51
 
 
52
 
forgetL : {A : Set}{n : Nat} -> Vec A n -> List A
53
 
forgetL [] = []
54
 
forgetL (x :: xs) = x :: forgetL xs
55
 
 
56
 
rem : {A : Set}(xs : List A) -> Vec A (Prelude.List.length xs)
57
 
rem [] = []
58
 
rem (x :: xs) = x :: rem xs
 
 
b'\\ No newline at end of file'