{-# OPTIONS --safe  #-}

open import Level
open import Data.Fin
open import Data.Fin.Properties using (suc-injective)
open import Data.List
open import Data.List.Relation.Unary.Any using (index)
import Data.List.Relation.Unary.Any as Any
open import Data.List.Relation.Unary.Any.Properties using (lookup-index)
open import Data.List.Membership.Propositional
open import Data.List.Membership.Propositional.Properties using (∈-map⁺; ∈-lookup)
open import Relation.Unary using (Pred)
open import Relation.Binary using (DecidableEquality)
open import Relation.Nullary.Decidable.Core

open import Relation.Binary.PropositionalEquality as ≡

open import Relation.Binary.PropositionalEquality.Core using (_≡_; sym; refl)

module Finite where

module MemberToIndex {ℓ : Level} {X : Set ℓ} where
  index-of-member : {x : X} (l : List X) → (x ∈ l) → Fin (length l)
  index-of-member .(_ ∷ _) (Any.here px) = Fin.zero
  index-of-member (._ ∷ l) (Any.there el) = Fin.suc (index-of-member l el)

  lookup-index-of-member : {x : X} (l : List X) → (el : x ∈ l) → lookup l (index-of-member l el) ≡ x
  lookup-index-of-member .(_ ∷ _) (Any.here refl) = refl
  lookup-index-of-member (x ∷ xs) (Any.there el) = lookup-index-of-member xs el

record FiniteType {ℓ : Level} (X : Set ℓ) : Set ℓ where
  -- the property of a type X being finite
  field
    elements : List X
    all-enumerated : ∀ (x : X) → x ∈ elements

  to-index : X → Fin (length elements)
  to-index x = index (all-enumerated x)

  from-index : Fin (length elements) → X
  from-index k = lookup elements k

  to-index-split : ∀ x → from-index (to-index x) ≡ x
  to-index-split x = sym (lookup-index (all-enumerated x))


-- Example of a finite type: Elements of a List:
record Element {a} {A : Set a} (l : List A) : Set a where
  -- The type compromised by the elements of a given list.
  constructor _∈⊣_ -- the first argument is for the 'l'
  field
    val : A
    contained : val ∈ l

  idx : Fin (length l)
  idx = MemberToIndex.index-of-member l contained

  idx-correct : lookup l idx ≡ val
  idx-correct = MemberToIndex.lookup-index-of-member l contained

Element-idx-injective : ∀ {a} {A : Set a} (l : List A) (x y : Element l) → (Element.idx x ≡ Element.idx y) → (x ≡ y)
Element-idx-injective .(_ ∷ _) (v1 ∈⊣ Any.here refl) (.v1 ∈⊣ Any.here refl) _ = refl
Element-idx-injective (x ∷ l) (v1 ∈⊣ Any.there e1) (v2 ∈⊣ Any.there e2) eq
  = goal
  where
    t1 : Element l
    t1 = (v1 ∈⊣ e1)
    t2 : Element l
    t2 = (v2 ∈⊣ e2)
    same-idx : Element.idx t1 ≡ Element.idx t2
    same-idx = suc-injective eq
    t1≡t2 : t1 ≡ t2
    t1≡t2 = Element-idx-injective l t1 t2 same-idx
    goal : (v1 ∈⊣ Any.there {x = x} e1) ≡ (v2 ∈⊣ Any.there e2)
    goal with t1≡t2
    ... | refl = refl

pattern _∈' val = val ∈⊣ _

ElementFromIndex : ∀ {a} {A : Set a} (l : List A) (idx : Fin (length l)) → Element l
ElementFromIndex l idx = lookup l idx ∈⊣ ∈-lookup idx

ElementFromIndex-correct1 : ∀ {a} {A : Set a} (l : List A) (idx : Fin (length l)) → Element.idx (ElementFromIndex l idx) ≡ idx
ElementFromIndex-correct1 (x ∷ l) Fin.zero = refl
ElementFromIndex-correct1 (x ∷ l) (Fin.suc idx) rewrite (ElementFromIndex-correct1 l idx) = refl

ElementFromIndex-correct2 : ∀ {a} {A : Set a} (l : List A) (e : Element l) → ElementFromIndex l (Element.idx e) ≡ e
ElementFromIndex-correct2 l e = Element-idx-injective l _ e (ElementFromIndex-correct1 l (Element.idx e))


record ElementIdx {a} {A : Set a} (l : List A) : Set 0ℓ where
  -- The type compromised by the elements of a given list.
  constructor element-by-idx
  field
    idx : Fin (length l)

  toElement : Element l
  toElement = ElementFromIndex l idx
  open Element toElement hiding (idx) public

module _ {a : Level} {A : Set a} where

  Element-∷ : ∀ {l : List A} {x} → Element l → Element (x ∷ l)
  Element-∷ (e ∈⊣ w) = e ∈⊣ Any.there w

  list-elements : ∀ (l : List A) → List (Element l)
  list-elements [] = []
  list-elements (x ∷ l) = (x ∈⊣ Any.here refl) ∷ map Element-∷ (list-elements l)


  double-elem : ∀ (l : List A) → (e : Element l) → e ∈ list-elements l
  double-elem .(_ ∷ _) (x ∈⊣ Any.here refl) = Any.here refl
  double-elem (_ ∷ l) (x ∈⊣ Any.there w) = Any.there (∈-map⁺ Element-∷ zzz) -- there {!!}
    where
      zzz : (x ∈⊣ w) ∈ list-elements l
      zzz = double-elem l (x ∈⊣ w) -- (x ∈⊣ w) l

  Element-Finite : ∀ {l : List A} → FiniteType (Element l)
  Element-Finite {l} =
    record
    { elements = list-elements l
    ; all-enumerated = double-elem l
    }

  -- regardless of A, the elements of a list always have decidable equality:
  same-element? : ∀ {l : List A} → DecidableEquality (Element l)
  same-element? {[]} () ()
  same-element? {x ∷ l} (.x ∈⊣ Any.here refl) (.x ∈⊣ Any.here refl) = yes refl
  same-element? {x ∷ l} (e1 ∈⊣ Any.here px) (e2 ∈⊣ Any.there c2) = no (λ ())
  same-element? {x ∷ l} (e1 ∈⊣ Any.there c1) (e2 ∈⊣ Any.here px) = no (λ ())
  same-element? {x ∷ l} (e1 ∈⊣ Any.there c1) (e2 ∈⊣ Any.there c2) =
    map′
      (λ {refl → refl }) (λ { refl → refl})
      (same-element? {l} (e1 ∈⊣ c1) (e2 ∈⊣ c2))

-- record FinitePred {a b : Level} {X : Set a} (P : Pred X b) : Set (a ⊔ b) where
--   -- the property of a predicate P holding for only finitely many
--   -- values
--   field
--     elements : List X
--     all-enumerated : ∀ (x : X) → P x → x ∈ elements