module X4 where
----------------------------------------------------------------------
-- Exercise 4 : Views of Vectors --
----------------------------------------------------------------------
-- LIBRARY
data Zero : Set where
data One : Set where
void : One
data Sigma (S : Set)(T : S -> Set) : Set where
_,_ : (s : S)(t : T s) -> Sigma S T
_:*:_ : Set -> Set -> Set
S :*: T = Sigma S \ s -> T
data _:+:_ (S : Set)(T : Set) : Set where
inl : S -> S :+: T
inr : T -> S :+: T
data Nat : Set where
zero : Nat
suc : Nat -> Nat
data _^_ (X : Set) : Nat -> Set where
[] : X ^ zero
_::_ : {n : Nat} -> X -> X ^ n -> X ^ suc n
_+_ : Nat -> Nat -> Nat
zero + y = y
suc x + y = suc (x + y)
sum : {n : Nat} -> Nat ^ n -> Nat
sum [] = zero
sum (n :: ns) = n + sum ns
_++_ : {X : Set}{m n : Nat} -> X ^ m -> X ^ n -> X ^ (m + n)
[] ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)
-- EXERCISES
-- Hint: you will need to use the "dot patterns" as in the
-- allOrNothing example from lecture 6.
{- (4.1) Show that every vector of length (m + n) is made by
appending a vector of length m to a vector of length n. -}
data Split {X : Set}(m n : Nat) : X ^ (m + n) -> Set where
_+?+_ : (xs : X ^ m)(ys : X ^ n) -> Split m n (xs ++ ys)
split : {X : Set}(m n : Nat)(xs : X ^ (m + n)) -> Split m n xs
split m n zs = {! !}
{- (4.2) Define the "predicate transformer" (Everywhere P xs), which
collects a value in (P x) for each element x in xs -}
Everywhere : {n : Nat}{X : Set}(P : X -> Set)(xs : X ^ n) -> Set
Everywhere P xs = {! !}
{- (4.3) Show how to lift a function p which generates a P for each x
to a function which applies p everywhere. -}
everywhere : {n : Nat}{X : Set}(P : X -> Set)
(p : (x : X) -> P x) ->
(xs : X ^ n) -> Everywhere P xs
everywhere P p xs = {! !}
{- (4.4) Define a function which takes a vector of lengths and
some vectors of those lengths, then returns their concatenation. -}
concat : {X : Set}{m : Nat}(ns : Nat ^ m) ->
{! !} -> X ^ (sum ns)
concat ns xss = {! !}
{- (4.5*) Given a vector ns of lengths, use the same method as for
Split/split to show why every vector of length (sum ns) is given by
some (concat ns xss). -}