------------------------------------------------------------------------
-- The Agda standard library
--
-- Modalities used in the reflection machinery
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Reflection.AST.Argument.Modality where

open import Data.Product.Base using (_×_; <_,_>; uncurry)
open import Relation.Nullary.Decidable.Core using (map′; _×?_)
open import Relation.Binary.Definitions using (DecidableEquality)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
open import Reflection.AST.Argument.Relevance as Relevance using (Relevance)
open import Reflection.AST.Argument.Quantity as Quantity using (Quantity)

private
  variable
    r r′ : Relevance
    q q′ : Quantity

------------------------------------------------------------------------
-- Re-exporting the builtins publicly

open import Agda.Builtin.Reflection public using (Modality)
open Modality public

------------------------------------------------------------------------
-- Operations

relevance : Modality → Relevance
relevance (modality r _) = r

quantity : Modality → Quantity
quantity (modality _ q) = q

------------------------------------------------------------------------
-- Decidable equality

modality-injective₁ : modality r q ≡ modality r′ q′ → r ≡ r′
modality-injective₁ refl = refl

modality-injective₂ : modality r q ≡ modality r′ q′ → q ≡ q′
modality-injective₂ refl = refl

modality-injective : modality r q ≡ modality r′ q′ → r ≡ r′ × q ≡ q′
modality-injective = < modality-injective₁ , modality-injective₂ >

infix  _≡?_

_≡?_ : DecidableEquality Modality
modality r q ≡? modality r′ q′ =
  map′
    (uncurry (cong₂ modality))
    modality-injective
    (r Relevance.≡? r′ ×? q Quantity.≡? q′)


------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 2.4

infix  _≟_

_≟_ = _≡?_
{-# WARNING_ON_USAGE _≟_
"Warning: _≟_ was deprecated in v2.4.
Please use _≡?_ instead."
#-}