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

module OWL2.Foundation.List where

open import Agda.Primitive using (_⊔_)
open import Cubical.Data.Nat.Base using (zero; suc)
open import OWL2.Prelude

listCount : ∀ {ℓ} {A : Type ℓ} → List A → ℕ
listCount [] =
  zero
listCount (x ∷ xs) =
  suc (listCount xs)

isEmpty? : ∀ {ℓ} {A : Type ℓ} → List A → Bool
isEmpty? [] =
  true
isEmpty? (x ∷ xs) =
  false

Empty : ∀ {ℓ} {A : Type ℓ} → List A → Type₀
Empty [] =
  Unit
Empty (x ∷ xs) =
  ⊥

NonEmpty : ∀ {ℓ} {A : Type ℓ} → List A → Type₀
NonEmpty [] =
  ⊥
NonEmpty (x ∷ xs) =
  Unit

singleton : ∀ {ℓ} {A : Type ℓ} → A → List A
singleton x =
  x ∷ []

head? : ∀ {ℓ} {A : Type ℓ} → List A → Optional A
head? [] =
  absent
head? (x ∷ xs) =
  present x

tail? : ∀ {ℓ} {A : Type ℓ} → List A → Optional (List A)
tail? [] =
  absent
tail? (x ∷ xs) =
  present xs

concatMap :
  ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} →
  (A → List B) → List A → List B
concatMap f [] =
  []
concatMap f (x ∷ xs) =
  f x ++ concatMap f xs

data All {ℓ ℓ'} {A : Type ℓ}
  (P : A → Type ℓ') : List A → Type (ℓ ⊔ ℓ') where
  all[] :
    All P []
  all∷ :
    ∀ {x xs} → P x → All P xs → All P (x ∷ xs)

allAppend :
  ∀ {ℓ ℓ'} {A : Type ℓ} {P : A → Type ℓ'} {xs ys : List A} →
  All P xs → All P ys → All P (xs ++ ys)
allAppend {xs = []} all[] pys =
  pys
allAppend {xs = x ∷ xs} (all∷ px pxs) pys =
  all∷ px (allAppend pxs pys)

allAppendLeft :
  ∀ {ℓ ℓ'} {A : Type ℓ} {P : A → Type ℓ'} {xs ys : List A} →
  All P (xs ++ ys) → All P xs
allAppendLeft {xs = []} proof =
  all[]
allAppendLeft {xs = x ∷ xs} (all∷ px proof) =
  all∷ px (allAppendLeft proof)

allAppendRight :
  ∀ {ℓ ℓ'} {A : Type ℓ} {P : A → Type ℓ'} {xs ys : List A} →
  All P (xs ++ ys) → All P ys
allAppendRight {xs = []} proof =
  proof
allAppendRight {xs = x ∷ xs} (all∷ px proof) =
  allAppendRight proof

allAppendSplit :
  ∀ {ℓ ℓ'} {A : Type ℓ} {P : A → Type ℓ'} {xs ys : List A} →
  All P (xs ++ ys) → All P xs × All P ys
allAppendSplit proof =
  allAppendLeft proof , allAppendRight proof

data Any {ℓ ℓ'} {A : Type ℓ}
  (P : A → Type ℓ') : List A → Type (ℓ ⊔ ℓ') where
  here :
    ∀ {x xs} → P x → Any P (x ∷ xs)
  there :
    ∀ {x xs} → Any P xs → Any P (x ∷ xs)