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

module OWL2.Foundation.Fin where

open import OWL2.Prelude
open import OWL2.Foundation.List using (listCount)
open import Cubical.Data.FinData.Base public
  using (Fin)
  renaming (zero to fzero; suc to fsuc; toℕ to finToNat)

lookupFinBy :
  ∀ {ℓ} {A : Type ℓ} →
  (A → Bool) → (xs : List A) → Optional (Fin (listCount xs))
lookupFinBy p [] =
  absent
lookupFinBy p (x ∷ xs) with p x
... | true =
  present fzero
... | false with lookupFinBy p xs
...   | absent =
  absent
...   | present i =
  present (fsuc i)

lookupFin :
  ∀ {ℓ} {A : Type ℓ} →
  (A → A → Bool) → A → (xs : List A) → Optional (Fin (listCount xs))
lookupFin equal target xs =
  lookupFinBy (equal target) xs

lookupByFin :
  ∀ {ℓ} {A : Type ℓ} →
  (xs : List A) → Fin (listCount xs) → A
lookupByFin [] ()
lookupByFin (x ∷ xs) fzero =
  x
lookupByFin (x ∷ xs) (fsuc index) =
  lookupByFin xs index

injectLeftFin :
  ∀ {ℓ} {A : Type ℓ} →
  (left right : List A) →
  Fin (listCount left) →
  Fin (listCount (left ++ right))
injectLeftFin [] right ()
injectLeftFin (x ∷ left) right fzero =
  fzero
injectLeftFin (x ∷ left) right (fsuc index) =
  fsuc (injectLeftFin left right index)

injectRightFin :
  ∀ {ℓ} {A : Type ℓ} →
  (left right : List A) →
  Fin (listCount right) →
  Fin (listCount (left ++ right))
injectRightFin [] right index =
  index
injectRightFin (x ∷ left) right index =
  fsuc (injectRightFin left right index)

lookupByFinInjectLeft :
  ∀ {ℓ} {A : Type ℓ} →
  (left right : List A) →
  (index : Fin (listCount left)) →
  lookupByFin (left ++ right) (injectLeftFin left right index) ≡
  lookupByFin left index
lookupByFinInjectLeft [] right ()
lookupByFinInjectLeft (x ∷ left) right fzero =
  refl
lookupByFinInjectLeft (x ∷ left) right (fsuc index) =
  lookupByFinInjectLeft left right index

lookupByFinInjectRight :
  ∀ {ℓ} {A : Type ℓ} →
  (left right : List A) →
  (index : Fin (listCount right)) →
  lookupByFin (left ++ right) (injectRightFin left right index) ≡
  lookupByFin right index
lookupByFinInjectRight [] right index =
  refl
lookupByFinInjectRight (x ∷ left) right index =
  lookupByFinInjectRight left right index