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

{-# OPTIONS --cubical-compatible --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)

------------------------------------------------------------------------
-- Re-exporting the builtin type and constructors

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

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

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