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). -}