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

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

module Reflection.AST.Abstraction where

open import Data.String.Base as String                 using (String)
open import Data.String.Properties as String           using (_≟_)
open import Data.Product.Base                          using (_×_; <_,_>; uncurry)
open import Level using (Level)
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₂)

private
  variable
    a b : Level
    A B : Set a
    s t : String
    x y : A

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

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

open Abs public

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

map : (A → B) → Abs A → Abs B
map f (abs s x) = abs s (f x)

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

abs-injective₁ : abs s x ≡ abs t y → s ≡ t
abs-injective₁ refl = refl

abs-injective₂ : abs s x ≡ abs t y → x ≡ y
abs-injective₂ refl = refl

abs-injective : abs s x ≡ abs t y → s ≡ t × x ≡ y
abs-injective = < abs-injective₁ , abs-injective₂ >

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

unAbs : Abs A → A
unAbs (abs s a) = a

unAbs-dec : {abs1 abs2 : Abs A} → Dec (unAbs abs1 ≡ unAbs abs2) → Dec (abs1 ≡ abs2)
unAbs-dec {abs1 = abs s a} {abs t a′} a≟a′ =
  map′ (uncurry (cong₂ abs)) abs-injective (s String.≟ t ×-dec a≟a′)

≡-dec : DecidableEquality A → DecidableEquality (Abs A)
≡-dec _≟_ x y = unAbs-dec (unAbs x ≟ unAbs y)