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

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

    module Reflection.AST.Argument where

    open import Data.List.Base as List using (List; []; _∷_)
    open import Data.Product.Base using (_×_; <_,_>; uncurry)
    open import Relation.Nullary.Decidable.Core using (Dec; map′; _×-dec_)
    open import Relation.Binary.Definitions using (DecidableEquality)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
    open import Level using (Level)
    open import Reflection.AST.Argument.Visibility
    open import Reflection.AST.Argument.Relevance
    open import Reflection.AST.Argument.Quantity
    open import Reflection.AST.Argument.Modality
    open import Reflection.AST.Argument.Information as Information

    private
      variable
        a b : Level
        A B : Set a
        i j : ArgInfo
        x y : A

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

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

    -- Pattern synonyms

    pattern defaultModality = modality relevant quantity-ω

    pattern vArg ty = arg (arg-info visible   defaultModality) ty
    pattern hArg ty = arg (arg-info hidden    defaultModality) ty
    pattern iArg ty = arg (arg-info instance′ defaultModality) ty

    ------------------------------------------------------------------------
    -- Lists of arguments

    Args : (A : Set a) → Set a
    Args A = List (Arg A)

    -- Pattern for appending a visible argument
    infixr 5 _⟨∷⟩_
    pattern _⟨∷⟩_ x args = vArg x ∷ args

    -- Pattern for appending a hidden argument
    infixr 5 _⟅∷⟆_
    pattern _⟅∷⟆_ x args = hArg x ∷ args

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

    map : (A → B) → Arg A → Arg B
    map f (arg i x) = arg i (f x)

    map-Args : (A → B) → Args A → Args B
    map-Args f xs = List.map (map f) xs

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

    arg-injective₁ : arg i x ≡ arg j y → i ≡ j
    arg-injective₁ refl = refl

    arg-injective₂ : arg i x ≡ arg j y → x ≡ y
    arg-injective₂ refl = refl

    arg-injective : arg i x ≡ arg j y → i ≡ j × x ≡ y
    arg-injective = < arg-injective₁ , arg-injective₂ >

    -- We often need decidability of equality for Arg A when implementing it
    -- for A. Unfortunately ≡-dec makes the termination checker unhappy.
    -- Instead, we can match on both Arg A and use unArg-dec for an
    -- obviously decreasing recursive call.

    unArg : Arg A → A
    unArg (arg i a) = a

    unArg-dec : {arg1 arg2 : Arg A} → Dec (unArg arg1 ≡ unArg arg2) → Dec (arg1 ≡ arg2)
    unArg-dec {arg1 = arg i x} {arg j y} arg1≟arg2 =
      map′ (uncurry (cong₂ arg)) arg-injective (i Information.≟ j ×-dec arg1≟arg2)

    ≡-dec : DecidableEquality A → DecidableEquality (Arg A)
    ≡-dec _≟_ x y = unArg-dec (unArg x ≟ unArg y)