module powerofpi where
open import Data.Nat
open import Data.Vec hiding(_++_ ; take ; drop ; split ; [_] ; concat)
open import Data.List hiding(take ; drop ; concat; [_])
open import Relation.Binary.PropositionalEquality hiding ([_])
open ≡-Reasoning

-- Based on:
-- Oury and Swierstra: The power of Pi.


----------------------------------------------
---Part I: A simple example for a view--------
----------------------------------------------

--snocView is a datatype indexed by (List A)'s
--i.e. for every list of type List A, there is a corresponding snocView
--The snocView makes the last element in the List available for pattern-matching

data snocView {A : Set} : List A → Set where
  -- ⟨⟩ is the snocView of the empty list
  ⟨⟩ : snocView []
  -- snoc takes a list xs of type (List A) and an element x of type A and gives back a snocView of (xs ++ (x :: [])
  _snoc_ : (xs : List A) → (x : A) → snocView ( xs ++ (x ∷ []))

--Having defined a view for List, we now need a function that constructs the snocView for us
--The function view takes a list and gives back a snocView of that list
view : {A : Set} → (xs : List A) → snocView xs
view [] = ⟨⟩
view (x ∷ xs) with view xs
view (x ∷ .[]) | ⟨⟩
  = [] snoc x
view (x ∷ .(ys ++ (y ∷ []))) | ys snoc y
  = (x ∷ ys) snoc y

--Let's see this for some examples
list1 : List ℕ
list1 = 1 ∷ 2 ∷ 3 ∷ 4 ∷ []

snoclist1 : snocView list1
snoclist1 = view list1

list2 : List ℕ
list2 = []

snoclist2 : snocView list2
snoclist2 = view list2

--We can use our newly defined view to pattern-match on the last element of a list
--We use this in the function rotateright
rotateright : {A : Set} → List A → List A
rotateright xs with view xs
rotateright .[] | ⟨⟩
  = []
rotateright .(ys ++ (y ∷ [])) | ys snoc y
  = y ∷ ys

--Let's test this function
rotatedlist1 : List ℕ
rotatedlist1 = rotateright (rotateright list1)

-------------------------------------------------------------------
-----Part II: A more involved example: Cryptol---------------------
-------------------------------------------------------------------

--We have a type for Bits (0 and 1 dont work...)
data Bit : Set where
  O : Bit
  I : Bit

--And a type for Bit-Words of constant length
Word : ℕ → Set
Word n = Vec Bit n


--Now for some auxillary functions on Vectors and matrices

--The function "take" takes the first n bits of a vector and cuts of the rest
take : ∀ { m}{A : Set} → (n : ℕ) → Vec A (n + m) → Vec A n
take zero xs = []
take (suc n) (x ∷ xs) = x ∷ take n xs

--The function "drop" drops the first n bits of a vector and keeps the rest
drop : ∀ {m}{A : Set} → (n : ℕ) → Vec A (n + m) → Vec A m
drop zero xs = xs
drop (suc n) (x ∷ xs) = drop n xs

--The function "split" takes a vector of length n*m and makes it into a matrix of dimensions n*m
split : {A : Set} → (n : ℕ) → (m : ℕ) → Vec A (m * n) → Vec (Vec A n) m 
split n zero [] = []
split n (suc m) x = take n x ∷ split n m (drop n x)

--The function "_app_" appends to Vectors
_app_ : ∀ {m n}{A : Set} → Vec A m → Vec A n → Vec A (m + n)
[] app ys = ys
(x ∷ xs) app ys = x ∷ (xs app ys)

--The function "concat" takes a matrix of dimension n*m and returns a "flattened" vector of length n*m
concat : ∀ {A n m} → Vec (Vec A n) m → Vec A (m * n)
concat [] = []
concat (x ∷ x₁) = x app (concat x₁)

--Lemma 1: Take drop Lemma
takeDropLemma : ∀ {A : Set}{ n m} → (xs : Vec A (n + m)) → (take n xs) app (drop n xs) ≡ xs
takeDropLemma {A} {zero} {m} xs = refl
takeDropLemma {A} {suc n} {m}(x ∷ xs) = cong (λ l → x ∷ l) (takeDropLemma {n = n} {m = m} xs)


--Lemma 2: Split Concat Lemma
--We show in a Lemma that first splitting a Vector and then flattening it does not change anything in the vector
splitConcatLemma : ∀ {A n m} → (xs : Vec A (m * n)) → concat (split n m xs) ≡ xs
splitConcatLemma {A} {n} {zero} [] = refl
--splitConcatLemma {A} {zero} {suc m} xs = splitConcatLemma {m = m} xs
splitConcatLemma {A}{n = n} {suc m} xs =
  begin
    take n xs app concat (split n m (drop n xs))
    ≡⟨ cong (λ l → take n xs app l) (splitConcatLemma {n = n} {m = m}(drop n xs)) ⟩
    take n xs app drop n xs
    ≡⟨ takeDropLemma {n = n} {m = m * n} xs ⟩
    xs
  ∎

--Now to the SplitView datatype
data SplitView {A : Set} : {n : ℕ} → (m : ℕ) → Vec A (m * n) → Set where
  [_] : ∀ {m n} → (xss : Vec (Vec A n) m) → SplitView m (concat xss)

--Now let's define the view function that takes a Matrix and gives back a SplitView
splitview : {A : Set} → (n : ℕ) → (m : ℕ) → (xs : Vec A (m * n)) → SplitView m xs
splitview n m xs with concat (split n m xs ) | [ split n m xs ] | splitConcatLemma {n = n} {m = m} xs
splitview n m xs | .xs | v | refl = v

--Now let's implement the function
swab : Word 16 → Word 16
swab xs with splitview 4 4 xs
swab ._ | [ a ∷ b ∷ c ∷ d ∷ [] ] 
  = concat (b ∷ a ∷ d ∷ c ∷ [])

--Now let's test the function
testword : Word 16
testword = O ∷ O ∷ O ∷ O ∷ I ∷ I ∷ I ∷ I ∷ O ∷ O ∷ I ∷ I ∷ I ∷ I ∷ O ∷ O ∷ []

testsplit : SplitView 4 testword 
testsplit = splitview 4 4 testword

swabword : Word 16
swabword = swab testword