------------------------------------------------------------------------
-- The Agda standard library
--
-- Argument information used in the reflection machinery
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Reflection.AST.Argument.Information where
 
open import Data.Product.Base                          using (_×_; <_,_>; uncurry)
open import Relation.Nullary.Decidable.Core            using (map′; _×-dec_)
open import Relation.Binary.Definitions                using (DecidableEquality)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
 
open import Reflection.AST.Argument.Modality as Modality using (Modality)
open import Reflection.AST.Argument.Visibility as Visibility using (Visibility)
 
private
  variable
    v v′ : Visibility
    m m′ : Modality
 
------------------------------------------------------------------------
-- Re-exporting the builtins publicly
 
open import Agda.Builtin.Reflection public using (ArgInfo)
open ArgInfo public
 
------------------------------------------------------------------------
-- Operations
 
visibility : ArgInfo → Visibility
visibility (arg-info v _) = v
 
modality : ArgInfo → Modality
modality (arg-info _ m) = m
 
------------------------------------------------------------------------
-- Decidable equality
 
arg-info-injective₁ : arg-info v m ≡ arg-info v′ m′ → v ≡ v′
arg-info-injective₁ refl = refl
 
arg-info-injective₂ : arg-info v m ≡ arg-info v′ m′ → m ≡ m′
arg-info-injective₂ refl = refl
 
arg-info-injective : arg-info v m ≡ arg-info v′ m′ → v ≡ v′ × m ≡ m′
arg-info-injective = < arg-info-injective₁ , arg-info-injective₂ >
 
infix  _≟_
 
_≟_ : DecidableEquality ArgInfo
arg-info v m ≟ arg-info v′ m′ =
  map′
    (uncurry (cong₂ arg-info))
    arg-info-injective
    (v Visibility.≟ v′ ×-dec m Modality.≟ m′)