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

{-# OPTIONS --without-K --safe #-}

module Reflection.Abstraction where

open import Data.List.Base as List using (List)
open import Data.Product using (_×_; _,_; uncurry; <_,_>)
import Data.String as String
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

private
  variable
    A B : Set

------------------------------------------------------------------------
-- Re-exporting the builtins publically

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

-- Pattern synonyms

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

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

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

abs-injective₁ :  {i i′} {a a′ : A}  abs i a  abs i′ a′  i  i′
abs-injective₁ refl = refl

abs-injective₂ :  {i i′} {a a′ : A}  abs i a  abs i′ a′  a  a′
abs-injective₂ refl = refl

abs-injective :  {i i′} {a a′ : A}  abs i a  abs i′ a′  i  i′ × a  a′
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 : {x y : Abs A}  Dec (unAbs x  unAbs y)  Dec (x  y)
unAbs-dec {x = abs i a} {abs i′ a′} a≟a′ =
  Dec.map′ (uncurry (cong₂ abs)) abs-injective ((i String.≟ i′) ×-dec a≟a′)

≡-dec : Decidable {A = A} _≡_  Decidable {A = Abs A} _≡_
≡-dec _≟_ x y = unAbs-dec (unAbs x  unAbs y)