{-# OPTIONS --without-K --safe #-}
module Reflection.AST.Literal where
open import Data.Bool.Base using (Bool; true; false)
import Data.Char.Properties as Char
import Data.Float.Properties as Float
import Data.Nat.Properties as ℕ
import Data.String.Properties as String
import Data.Word64.Properties as Word64
import Reflection.AST.Meta as Meta
import Reflection.AST.Name as Name
open import Relation.Nullary.Decidable.Core using (yes; no; map′; isYes)
open import Relation.Binary.Definitions using (DecidableEquality)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
open import Agda.Builtin.Reflection public
using ( Literal )
open Literal public
meta-injective : ∀ {x y} → meta x ≡ meta y → x ≡ y
meta-injective refl = refl
nat-injective : ∀ {x y} → nat x ≡ nat y → x ≡ y
nat-injective refl = refl
word64-injective : ∀ {x y} → word64 x ≡ word64 y → x ≡ y
word64-injective refl = refl
float-injective : ∀ {x y} → float x ≡ float y → x ≡ y
float-injective refl = refl
char-injective : ∀ {x y} → char x ≡ char y → x ≡ y
char-injective refl = refl
string-injective : ∀ {x y} → string x ≡ string y → x ≡ y
string-injective refl = refl
name-injective : ∀ {x y} → name x ≡ name y → x ≡ y
name-injective refl = refl
infix 4 _≡?_
_≡?_ : DecidableEquality Literal
nat x ≡? nat x₁ = map′ (cong nat) nat-injective (x ℕ.≡? x₁)
nat x ≡? word64 x₁ = no (λ ())
nat x ≡? float x₁ = no (λ ())
nat x ≡? char x₁ = no (λ ())
nat x ≡? string x₁ = no (λ ())
nat x ≡? name x₁ = no (λ ())
nat x ≡? meta x₁ = no (λ ())
word64 x ≡? word64 x₁ = map′ (cong word64) word64-injective (x Word64.≡? x₁)
word64 x ≡? nat x₁ = no (λ ())
word64 x ≡? float x₁ = no (λ ())
word64 x ≡? char x₁ = no (λ ())
word64 x ≡? string x₁ = no (λ ())
word64 x ≡? name x₁ = no (λ ())
word64 x ≡? meta x₁ = no (λ ())
float x ≡? nat x₁ = no (λ ())
float x ≡? word64 x₁ = no (λ ())
float x ≡? float x₁ = map′ (cong float) float-injective (x Float.≡? x₁)
float x ≡? char x₁ = no (λ ())
float x ≡? string x₁ = no (λ ())
float x ≡? name x₁ = no (λ ())
float x ≡? meta x₁ = no (λ ())
char x ≡? nat x₁ = no (λ ())
char x ≡? word64 x₁ = no (λ ())
char x ≡? float x₁ = no (λ ())
char x ≡? char x₁ = map′ (cong char) char-injective (x Char.≡? x₁)
char x ≡? string x₁ = no (λ ())
char x ≡? name x₁ = no (λ ())
char x ≡? meta x₁ = no (λ ())
string x ≡? nat x₁ = no (λ ())
string x ≡? word64 x₁ = no (λ ())
string x ≡? float x₁ = no (λ ())
string x ≡? char x₁ = no (λ ())
string x ≡? string x₁ = map′ (cong string) string-injective (x String.≡? x₁)
string x ≡? name x₁ = no (λ ())
string x ≡? meta x₁ = no (λ ())
name x ≡? nat x₁ = no (λ ())
name x ≡? word64 x₁ = no (λ ())
name x ≡? float x₁ = no (λ ())
name x ≡? char x₁ = no (λ ())
name x ≡? string x₁ = no (λ ())
name x ≡? name x₁ = map′ (cong name) name-injective (x Name.≡? x₁)
name x ≡? meta x₁ = no (λ ())
meta x ≡? nat x₁ = no (λ ())
meta x ≡? word64 x₁ = no (λ ())
meta x ≡? float x₁ = no (λ ())
meta x ≡? char x₁ = no (λ ())
meta x ≡? string x₁ = no (λ ())
meta x ≡? name x₁ = no (λ ())
meta x ≡? meta x₁ = map′ (cong meta) meta-injective (x Meta.≡? x₁)
infix 4 _≡ᵇ_
_≡ᵇ_ : Literal → Literal → Bool
l ≡ᵇ l′ = isYes (l ≡? l′)
infix 4 _≟_
_≟_ = _≡?_
{-# WARNING_ON_USAGE _≟_
"Warning: _≟_ was deprecated in v2.4.
Please use _≡?_ instead."
#-}