-
Notifications
You must be signed in to change notification settings - Fork 0
/
vector.ya
64 lines (57 loc) · 2.21 KB
/
vector.ya
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
package vector
import natural
import maybe
import unit
import pair
import equal
import empty
where
type Vector (A: Type): ∀ (ω k: Natural) -> Type {
Nil: Vector A Natural.Z,
Cons (0 k: Natural) (x: A) (xs: Vector A k): Vector A (Natural.S k),
}
def Vector.head (0 A: Type) (k: Natural) (a : Vector A (Natural.S k)): A
= ((case a) (λ k' self => ∀ (Equal Natural (Natural.S k) k') -> A)
(λ e => Empty.absurd A (Natural.Z_isnt_S k e))
(λ k x xs e => x))
(Equal.Refl Natural (Natural.S k))
def Vector.tail (0 A: Type) (0 k: Natural) (a : Vector A k)
: Vector A (Natural.pred k)
= (case a) (λ k _ => Vector A (Natural.pred k))
(Vector.Nil A)
(λ _ x xs => xs)
def Vector.fill (0 A: Type) (n: Natural) (a: A): Vector A n
= (case n) (λ x => (Vector A x))
(Vector.Nil A)
(λ p => Vector.Cons A p a (Vector.fill A p a))
def Vector.extract (0 A: Type) (0 k: Natural) (xs: Vector A (Natural.S k))
: Pair A (Vector A k)
= (case xs)
(λ k _ => (case k) (λ _ => Type) Unit (λ pred => Pair A (Vector A pred)))
Unit.New
(λ k y ys => Pair.New A (Vector A k) y ys)
//
//def concat (0 A : Type) (0 sizeA sizeB : Nat) (a : Vector A sizeA) (b : Vector A sizeB): Vector A (Nat.add sizeA sizeB)
// = (case a) (λ sizeA _ => Vector A (Nat.add sizeA sizeB))
// b
// (λ sizeA head tail => cons A (Nat.add sizeA sizeB) head (concat A sizeA sizeB tail b))
//
//def at (A : Type) (0 size : Nat) (vec : Vector A size) (idx : Nat): Maybe A
// = (case idx) (λ _ => Maybe A)
// (head A size vec)
// (λ pred => at A size vec pred)
//
//def map (0 A B: Type) (0 size: Nat) (f: ∀ A -> B) (vec: Vector A size): Vector B size
// = (case vec) (λ k _ => Vector B k)
// (nil B)
// (λ size x xs => cons B size (f x) (map A B size f xs))
//
//def foldr (0 A B : Type) (0 size : Nat) (f: forall A B -> B) (b : B) (vec : Vector A size): B
// = (case vec) (λ _ _ => B)
// b
// (λ size head tail => f head (foldr A B size f b tail))
//
//def foldl (0 A B : Type) (0 size : Nat) (f: forall A B -> B) (b : B) (vec : Vector A size): B
// = (case vec) (λ _ _ => B)
// b
// (λ size head tail => (foldl A B size f (f head b) tail))