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