------------------------------------------------------------------------
-- 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)