------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to All
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Vec.Relation.Unary.All.Properties where

open import Data.Nat.Base using (; zero; suc; _+_)
open import Data.Fin.Base using (Fin; zero; suc)
open import Data.List.Base using ([]; _∷_)
open import Data.List.Relation.Unary.All as List using ([]; _∷_)
open import Data.Product as Prod using (_×_; _,_; uncurry; uncurry′)
open import Data.Vec.Base as Vec
import Data.Vec.Properties as Vecₚ
open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_)
open import Level using (Level)
open import Function.Base using (_∘_; id)
open import Function.Inverse using (_↔_; inverse)
open import Relation.Unary using (Pred) renaming (_⊆_ to _⋐_)
open import Relation.Binary as B using (REL)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; cong; cong₂; →-to-⟶)

private
  variable
    a b p q : Level
    A : Set a
    B : Set b
    P : Pred A p
    Q : Pred B q
    m n : 
    xs : Vec A n

------------------------------------------------------------------------
-- lookup

lookup⁺ : All P xs   i  P (Vec.lookup xs i)
lookup⁺ (px  _)  zero    = px
lookup⁺ (_  pxs) (suc i) = lookup⁺ pxs i

lookup⁻ : (∀ i  P (Vec.lookup xs i))  All P xs
lookup⁻ {xs = []}    pxs = []
lookup⁻ {xs = _  _} pxs = pxs zero  lookup⁻ (pxs  suc)

------------------------------------------------------------------------
-- map

map⁺ : {f : A  B}  All (P  f) xs  All P (map f xs)
map⁺ []         = []
map⁺ (px  pxs) = px  map⁺ pxs

map⁻ : {f : A  B}  All P (map f xs)  All (P  f) xs
map⁻ {xs = []}    []       = []
map⁻ {xs = _  _} (px  pxs) = px  map⁻ pxs

-- A variant of All.map

gmap : {f : A  B}  P  Q  f  All P {n}  All Q {n}  map f
gmap g = map⁺  All.map g

------------------------------------------------------------------------
-- _++_

++⁺ : {xs : Vec A m} {ys : Vec A n} 
      All P xs  All P ys  All P (xs ++ ys)
++⁺ []         pys = pys
++⁺ (px  pxs) pys = px  ++⁺ pxs pys

++ˡ⁻ : (xs : Vec A m) {ys : Vec A n} 
       All P (xs ++ ys)  All P xs
++ˡ⁻ []       _          = []
++ˡ⁻ (x  xs) (px  pxs) = px  ++ˡ⁻ xs pxs

++ʳ⁻ : (xs : Vec A m) {ys : Vec A n} 
       All P (xs ++ ys)  All P ys
++ʳ⁻ []       pys        = pys
++ʳ⁻ (x  xs) (px  pxs) = ++ʳ⁻ xs pxs

++⁻ : (xs : Vec A m) {ys : Vec A n} 
      All P (xs ++ ys)  All P xs × All P ys
++⁻ []       p          = [] , p
++⁻ (x  xs) (px  pxs) = Prod.map₁ (px ∷_) (++⁻ _ pxs)

++⁺∘++⁻ : (xs : Vec A m) {ys : Vec A n} 
          (p : All P (xs ++ ys)) 
          uncurry′ ++⁺ (++⁻ xs p)  p
++⁺∘++⁻ []       p          = refl
++⁺∘++⁻ (x  xs) (px  pxs) = cong (px ∷_) (++⁺∘++⁻ xs pxs)

++⁻∘++⁺ : {xs : Vec A m} {ys : Vec A n} 
          (p : All P xs × All P ys) 
          ++⁻ xs (uncurry ++⁺ p)  p
++⁻∘++⁺ ([]       , pys) = refl
++⁻∘++⁺ (px  pxs , pys) rewrite ++⁻∘++⁺ (pxs , pys) = refl

++↔ : {xs : Vec A m} {ys : Vec A n} 
      (All P xs × All P ys)  All P (xs ++ ys)
++↔ {xs = xs} = inverse (uncurry ++⁺) (++⁻ xs) ++⁻∘++⁺ (++⁺∘++⁻ xs)

------------------------------------------------------------------------
-- concat

concat⁺ : {xss : Vec (Vec A m) n} 
          All (All P) xss  All P (concat xss)
concat⁺ []           = []
concat⁺ (pxs  pxss) = ++⁺ pxs (concat⁺ pxss)

concat⁻ : (xss : Vec (Vec A m) n) 
          All P (concat xss)  All (All P) xss
concat⁻ []         []   = []
concat⁻ (xs  xss) pxss = ++ˡ⁻ xs pxss  concat⁻ xss (++ʳ⁻ xs pxss)

------------------------------------------------------------------------
-- swap

module _ {_~_ : REL A B p} where

  All-swap :  {n m xs ys} 
             All  x  All (x ~_) ys) {n} xs 
             All  y  All (_~ y) xs) {m} ys
  All-swap {ys = []}     _   = []
  All-swap {ys = y  ys} []  = All.universal  _  []) (y  ys)
  All-swap {ys = y  ys} ((x~y  x~ys)  pxs) =
    (x~y  (All.map All.head pxs)) 
    All-swap (x~ys  (All.map All.tail pxs))


------------------------------------------------------------------------
-- tabulate

module _ {P : A  Set p} where

  tabulate⁺ :  {n} {f : Fin n  A} 
              (∀ i  P (f i))  All P (tabulate f)
  tabulate⁺ {zero}  Pf = []
  tabulate⁺ {suc n} Pf = Pf zero  tabulate⁺ (Pf  suc)

  tabulate⁻ :  {n} {f : Fin n  A} 
              All P (tabulate f)  (∀ i  P (f i))
  tabulate⁻ (px  _) zero    = px
  tabulate⁻ (_  pf) (suc i) = tabulate⁻ pf i

------------------------------------------------------------------------
-- take and drop

drop⁺ :  m {xs}  All P {m + n} xs  All P {n} (drop m xs)
drop⁺ zero pxs = pxs
drop⁺ (suc m) {x  xs} (px  pxs)
  rewrite Vecₚ.unfold-drop m x xs = drop⁺ m pxs

take⁺ :  m {xs}  All P {m + n} xs  All P {m} (take m xs)
take⁺ zero pxs = []
take⁺ (suc m) {x  xs} (px  pxs)
  rewrite Vecₚ.unfold-take m x xs = px  take⁺ m pxs

------------------------------------------------------------------------
-- toList

module _ {P : Pred A p} where

  toList⁺ :  {n} {xs : Vec A n}  All P xs  List.All P (toList xs)
  toList⁺ []         = []
  toList⁺ (px  pxs) = px  toList⁺ pxs

  toList⁻ :  {n} {xs : Vec A n}  List.All P (toList xs)  All P xs
  toList⁻ {xs = []}     []         = []
  toList⁻ {xs = x  xs} (px  pxs) = px  toList⁻ pxs

------------------------------------------------------------------------
-- fromList

module _ {P : Pred A p} where

  fromList⁺ :  {xs}  List.All P xs  All P (fromList xs)
  fromList⁺ []         = []
  fromList⁺ (px  pxs) = px  fromList⁺ pxs

  fromList⁻ :  {xs}  All P (fromList xs)  List.All P xs
  fromList⁻ {[]}     []         = []
  fromList⁻ {x  xs} (px  pxs) = px  (fromList⁻ pxs)