{-# 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
open import Agda.Builtin.Reflection public
using (Abs)
open Abs public
map : (A → B) → Abs A → Abs B
map f (abs s x) = abs s (f x)
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₂ >
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)