------------------------------------------------------------------------
-- The Agda standard library
--
-- Names used in the reflection machinery
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Reflection.AST.Name where
 
open import Data.List.Base              using (List)
import Data.Product.Properties as Prodₚ using (≡-dec)
import Data.Word64.Properties as Wₚ       using (_≟_)
open import Function.Base               using (_on_)
open import Relation.Nullary.Decidable.Core            using (map′)
open import Relation.Binary.Core                       using (Rel)
open import Relation.Binary.Definitions                using (Decidable; DecidableEquality)
open import Relation.Binary.Construct.On               using (decidable)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
 
------------------------------------------------------------------------
-- Re-export built-ins
 
open import Agda.Builtin.Reflection public
  using (Name) renaming (primQNameToWord64s to toWords; primQNameEquality to _≡ᵇ_)
 
open import Agda.Builtin.Reflection.Properties public
  renaming (primQNameToWord64sInjective to toWords-injective)
 
------------------------------------------------------------------------
-- More definitions
------------------------------------------------------------------------
 
Names : Set
Names = List Name
 
------------------------------------------------------------------------
-- Decidable equality for names
------------------------------------------------------------------------
 
infix  _≈?_ _≟_ _≈_
 
_≈_ : Rel Name _
_≈_ = _≡_ on toWords
 
_≈?_ : Decidable _≈_
_≈?_ = decidable toWords _≡_ (Prodₚ.≡-dec Wₚ._≟_ Wₚ._≟_)
 
_≟_ : DecidableEquality Name
m ≟ n = map′ (toWords-injective _ _) (cong toWords) (m ≈? n)