{-# OPTIONS --cubical-compatible --safe #-}
module Reflection.AST.Abstraction where
open import Data.Product using (_×_; <_,_>; uncurry)
open import Data.String as String using (String)
open import Level
open import Relation.Nullary.Decidable using (Dec; map′; _×-dec_)
open import Relation.Binary using (DecidableEquality)
open import Relation.Binary.PropositionalEquality 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)