module Example where

open import Data.List
open import Data.Maybe
open import Data.Nat hiding (_⊔_ ; fold ; suc)
open import Data.Product
open import Function
open import Level
open import Relation.Binary.PropositionalEquality using (_≡_)


record MapClass {κ ν ℓ : Level} (K : Set κ) : Set (suc (κ ⊔ ν ⊔ ℓ)) where

  field
    Map : (V : K → Set ν) → Set ℓ
    nonempty! : {V : K → Set ν} → Map V → Set ℓ
    size : {V : K → Set ν} → Map V → ℕ
    lookup : {V : K → Set ν} → Map V → (k : K) → Maybe (V k)
    mapfilter : {V V′ : K → Set ν} → ((k : K) → V k → Maybe (V′ k)) → Map V → Map V′
    lookup-mapfilter : {V V′ : K → Set ν} (f : (k : K) → V k → Maybe (V′ k)) (M : Map V) (k : K) → lookup (mapfilter f M) k ≡ maybe′ (f k) nothing (lookup M k)
    fold : {V : K → Set ν} {A : Set (κ ⊔ ν)} (z : A) (s : Σ K V → A → A) → Map V → A
    -- In real life, some other data and specifications go here

  toList  : {V : K → Set ν} → Map V → List (Σ K V)
  toList = fold [] _∷_
  -- In real life, lots more standard utilities and properties go here


module PrefixMap {κ ν : Level} {K : Set κ} (NodeMap : MapClass {κ} {κ ⊔ suc ν} {κ ⊔ suc ν} K) where
  module N where
    open MapClass NodeMap public

  mutual
    Child : (V : List K → Set ν) → K → Set ?
    Child V k = PMap-nonempty (V ∘ (_∷_ k))

    -- "not strictly positive" :-(
    data PMap-nonempty (V : List K → Set ν) : Set (κ ⊔ suc ν) where
      node-✓ : V [] → N.Map (Child V) → PMap-nonempty V
      node-× : (C : N.Map (Child V)) → N.nonempty! C → PMap-nonempty V

  data PMap : (List K → Set ν) → Set {!!} where
    empty : (V : List K → Set ν) → PMap V
    nonempty : (V : List K → Set ν) → PMap-nonempty V → PMap V

  prefixmap : MapClass (List K)
  prefixmap = record {
    Map = PMap } -- In real life, we'd define and then specify the other fields, too...