module Exercise1 where

{- The library is in the Library directory.

   To make the system find it do
     M-x customize-group
     agda2
     Add the Library directory (full path) to the Agda2 Include Dirs option
     Click Save for Future Sessions (or Set for Current Session, whichever you prefer)
-}

open import Data.Bool
open import Data.Vec
open import Data.List
open import Data.Nat
open import Data.Fin
open import Data.Function
open import Logic.Id

-- Exercise: Matrix transposition ---------------------------

-- Define a function to compute a constant vector
vec : {n : Nat}{A : Set} -> A -> Vec A n
vec {n} x = {! !}

-- Define point-wise application of function vectors and argument vectors
infixl 90 _$_
_$_ : {n : Nat}{A B : Set} -> Vec (A -> B) n -> Vec A n -> Vec B n
fs $ xs = {! !}

-- Use these two functions to implement matrix transposition
Matrix : Set -> Nat -> Nat -> Set
Matrix A n m = Vec (Vec A n) m

transpose : forall {A n m} -> Matrix A n m -> Matrix A m n
transpose xss = {! !}

-- Exercise: Vector lookup ----------------------------------

-- Remember tabulate and _!_ from the lecture. They're defined in Data.Vec.

-- Prove that they are each other's inverses.

-- Should be easy
lem-!-tab : forall {A n} (f : Fin n -> A)(i : Fin n) -> tabulate f ! i == f i
lem-!-tab f i = {! !}

-- Might be trickier
lem-tab-! : forall {A n} (xs : Vec A n) -> tabulate (_!_ xs) == xs
lem-tab-! xs = {! !}

-- Exercise: Sublists ---------------------------------------

-- From the lecture
data _⊆_ {A : Set} : List A -> List A -> Set where
  stop : [] ⊆ []
  drop : forall {x xs ys} -> xs ⊆ ys ->      xs ⊆ x :: ys
  keep : forall {x xs ys} -> xs ⊆ ys -> x :: xs ⊆ x :: ys

-- Prove some simple properties

⊆-refl : {A : Set}{xs : List A} -> xs ⊆ xs
⊆-refl {xs = xs} = {! !}

⊆-trans : {A : Set}{xs ys zs : List A} -> xs ⊆ ys -> ys ⊆ zs -> xs ⊆ zs
⊆-trans p q = {! !}

-- Another representation of sublists

infixr 30 _::_
data SubList {A : Set} : List A -> Set where
  []   : SubList []
  _::_ : forall x {xs} -> SubList xs -> SubList (x :: xs)
  skip : forall {x xs} -> SubList xs -> SubList (x :: xs)

-- Define a function to extract corresponing list from a sublist.
forget : {A : Set}{xs : List A} -> SubList xs -> List A
forget s = {! !}

-- Prove that a SubList is a sublist in the sense of _⊆_
lem-forget : {A : Set}{xs : List A}(zs : SubList xs) -> forget zs ⊆ xs
lem-forget zs = {! !}

-- Give an alternative definition of filter which satisfies the
-- sublist property by construction.
filter' : {A : Set} -> (A -> Bool) -> (xs : List A) -> SubList xs
filter' p xs = {! !}

-- Define the complement of a sublist
complement : {A : Set}{xs : List A} -> SubList xs -> SubList xs
complement zs = {! !}

-- Compute all sublists of a given list
sublists : {A : Set}(xs : List A) -> List (SubList xs)
sublists xs = {! !}

-- Exercise: Do something interesting -----------------------

-- Implement some interesting functions / datatypes.