Granule documentation

Module Vec

Meta-data

Description: Base library for operations on type-indexed vectors
Authors: Dominic Orchard, Vilem-Benjamin Liepelt
License: BSD3
Copyright: (c) Authors 2018
Issue-tracking: https://github.com/dorchard/granule/issues
Repository: https://github.com/dorchard/granule

data Vec (n : Nat) (t : Type) where
    Nil  : Vec 0 t
  ; Cons : t -> (Vec n t) -> Vec (n + 1) t

Sized vectors

length : forall {a : Type, n : Nat} 
       . (Vec n (a [0])) -> N n

Length of an indexed vector into an indexed nat discarding the elements

length' : forall {a : Type, n : Nat} 
        . (Vec n a) -> (N n, Vec n a)

map : forall {a : Type, b : Type, n : Nat} 
    . ((a -> b) [n]) -> (Vec n a) -> Vec n b

index : forall {a : Type, n : Nat, m : Nat} 
      . {m > n} =>
    (N n) -> ((Vec m a) [0..1]) -> a

Safe random-access indexing from a vector

foldr : forall {a : Type, b : Type, n : Nat} 
      . ((a -> b -> b) [n]) -> b -> (Vec n a) -> b

Right fold

foldr1 : forall {a : Type, n : Nat} 
       . ((a -> a -> a) [n]) -> (Vec (n + 1) a) -> a

Foldr1 (no need for an initial value as vector has at least one element)

foldl : forall {a : Type, b : Type, n : Nat} 
      . ((b -> a -> b) [n]) -> b -> (Vec n a) -> b

Left fold

append : forall {a : Type, m : Nat, n : Nat} 
       . (Vec n a) -> (Vec m a) -> Vec (n + m) a

Append two vectors

concat : forall {a : Type, m : Nat, n : Nat} 
       . (Vec n (Vec m a)) -> Vec (n * m) a

Concatenate a vector of vectors

dropElems : forall {a : Type, m : Nat, n : Nat} 
          . (N m) -> ((Vec n a) [0..1]) -> Vec (n - m) a

Drop the first m elements

take : forall {a : Type, m : Nat, n : Nat} 
     . (N m) -> ((Vec n a) [0..1]) -> Vec (n + (m - n)) a

Take the first m elements

head : forall {a : Type, n : Nat} 
     . ((Vec (n + 1) a) [0..1]) -> a

Return the first item (head) of the vector NB: non-linear in the vector

tail : forall {a : Type, n : Nat} 
     . ((Vec (n + 1) a) [0..1]) -> Vec n a

Return the vector with the first item removed NB: non-linear in the vector

uncons : forall {a : Type, n : Nat} 
       . (Vec (n + 1) a) -> (a, Vec n a)

Take a vector and return the head element paired with the tail

split : forall {a : Type, m : Nat, n : Nat} 
      . (N n) -> (Vec (n + m) a) -> (Vec n a, Vec m a)

Split a vector at position 'n'

sum : forall {n : Nat} 
    . (Vec n Int) -> Int

Sum a vector of integers (using foldr)

product : forall {n : Nat} 
        . (Vec n Int) -> Int

Product of a vector of integers (using foldr)

replicate : forall {a : Type, n : Nat} 
          . (N n) -> (a [n]) -> Vec n a

Replicate n x is a vector of length n with x the value of every element

range : forall {n : Nat} 
      . (N n) -> Vec n Int

Make a vector of length n with all integers from 0 to n-1 e.g. range (S (S (S (S Z)))) should yield Cons 0 (Cons 1 (Cons 2 (Cons 3 Nil)))

range' : forall {n : Nat} 
       . (N n) -> (Int [n]) -> Vec n Int

Make a vector of length n with all integers from start up until n + i - 1 e.g. range' (S (S (S (S Z)))) [-6] should yield Cons -6 (Cons -5 (Cons -4 (Cons -3 Nil)))

pullVec : forall {a : Type, s : Coeffect, k : s, n : Nat} 
        . (Vec n (a [k])) -> (Vec n a) [k]

pullVec pulls non linearity in elements into a non linearity on the whole vector

pushVec : forall {a : Type, s : Coeffect, k : s, n : Nat} 
        . {((1 : s)) ≤ k, Pushable k} =>
    ((Vec n a) [k]) -> Vec n (a [k])

pushVec pushes in non linearity of vector into the elements

copySpine : forall {a : Type, n : Nat} 
          . (Vec n a) -> (Vec n (), Vec n a)

Copy the spine of a vector

stringToVec : String -> exists {n : Nat} 
            . Vec n Char

Convert a string into a vector

Meta-data

Contents