------------------------------------------------------------------------
-- The Agda standard library
--
-- Keys for AVL trees -- the original key type extended with a new
-- minimum and maximum.
------------------------------------------------------------------------

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

open import Relation.Binary.Bundles
  using (StrictTotalOrder; StrictPartialOrder)

module Data.Tree.AVL.Key
  {a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂)
  where

open import Level using (Level; _⊔_)
open import Data.Product.Base using (_×_; _,_)
open import Relation.Binary.Definitions using (Reflexive)
open import Relation.Binary.PropositionalEquality.Core using (_≡_ ; refl)
open import Relation.Nullary.Negation.Core using (¬_)
open import Relation.Nullary.Construct.Add.Extrema
  as AddExtremaToSet using (_±)
import Relation.Binary.Construct.Add.Extrema.Equality
  as AddExtremaToEquality
import Relation.Binary.Construct.Add.Extrema.Strict
  as AddExtremaToOrder

open StrictTotalOrder sto renaming (Carrier to Key)
  using (_≈_; _<_; trans; irrefl; module Eq)

------------------------------------------------------------------------
-- Keys are augmented with new extrema (i.e. an artificial minimum and
-- maximum)

Key⁺ : Set a
Key⁺ = Key ±

open AddExtremaToSet public
  using ([_]; [_]-injective)
  renaming
  ( ⊥± to ⊥⁺
  ; ⊤± to ⊤⁺
  )

------------------------------------------------------------------------
-- The equality is extended in a corresponding manner

open AddExtremaToEquality _≈_ public
  using ()
  renaming
  ( _≈±_ to _≈⁺_
  ; [_]  to [_]ᴱ
  )

------------------------------------------------------------------------
-- The order is extended in a corresponding manner

open AddExtremaToOrder _<_ public
  using () renaming
  (_<±_    to _<⁺_
  ; [_]    to [_]ᴿ
  ; ⊥±<⊤±  to ⊥⁺<⊤⁺
  ; [_]<⊤± to [_]<⊤⁺
  ; ⊥±<[_] to ⊥⁺<[_]
  )

-- A pair of ordering constraints.

infix  _<_<_

_<_<_ : Key⁺ → Key → Key⁺ → Set (a ⊔ ℓ₂)
l < x < u = l <⁺ [ x ] × [ x ] <⁺ u

-- Properties

⊥⁺<[_]<⊤⁺ : ∀ k → ⊥⁺ < k < ⊤⁺
⊥⁺<[ k ]<⊤⁺ = ⊥⁺<[ k ] , [ k ]<⊤⁺

refl⁺ : Reflexive _≈⁺_
refl⁺ = AddExtremaToEquality.≈±-refl _≈_ Eq.refl

sym⁺ : ∀ {l u} → l ≈⁺ u → u ≈⁺ l
sym⁺ = AddExtremaToEquality.≈±-sym _≈_ Eq.sym

trans⁺ : ∀ l {m u} → l <⁺ m → m <⁺ u → l <⁺ u
trans⁺ l = AddExtremaToOrder.<±-trans _<_ trans

irrefl⁺ : ∀ k → ¬ (k <⁺ k)
irrefl⁺ k = AddExtremaToOrder.<±-irrefl _<_ irrefl refl⁺

-- Bundle

strictPartialOrder : StrictPartialOrder _ _ _
strictPartialOrder = record
  { isStrictPartialOrder = AddExtremaToOrder.<±-isStrictPartialOrder STO._<_ STO.isStrictPartialOrder
  } where module STO = StrictTotalOrder sto

strictTotalOrder : StrictTotalOrder _ _ _
strictTotalOrder = record
  { isStrictTotalOrder = AddExtremaToOrder.<±-isStrictTotalOrder STO._<_ STO.isStrictTotalOrder
  } where module STO = StrictTotalOrder sto