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

{-# OPTIONS --cubical-compatible --safe #-}

module Reflection.AST.Definition where

import Data.List.Properties as List                    using (≡-dec)
import Data.Nat.Properties as                         using (_≟_)
open import Data.Product.Base                          using (_×_; <_,_>; uncurry)
open import Relation.Nullary.Decidable.Core            using (map′; _×-dec_; yes; no)
open import Relation.Binary.Definitions                using (DecidableEquality)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)

import Reflection.AST.Argument as Arg
import Reflection.AST.Name     as Name
import Reflection.AST.Term     as Term

------------------------------------------------------------------------
-- Re-exporting type publically

open import Agda.Builtin.Reflection public
  using    ( Definition
           ; function
           ; data-type
           ; axiom
           )
  renaming ( record-type to record′
           ; data-cons   to constructor′
           ; prim-fun    to primitive′ )

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

function-injective :  {cs cs′}  function cs  function cs′  cs  cs′
function-injective refl = refl

data-type-injective₁ :  {pars pars′ cs cs′}  data-type pars cs  data-type pars′ cs′  pars  pars′
data-type-injective₁ refl = refl

data-type-injective₂ :  {pars pars′ cs cs′}  data-type pars cs  data-type pars′ cs′  cs  cs′
data-type-injective₂ refl = refl

data-type-injective :  {pars pars′ cs cs′}  data-type pars cs  data-type pars′ cs′  pars  pars′ × cs  cs′
data-type-injective = < data-type-injective₁ , data-type-injective₂ >

record′-injective₁ :  {c c′ fs fs′}  record′ c fs  record′ c′ fs′  c  c′
record′-injective₁ refl = refl

record′-injective₂ :  {c c′ fs fs′}  record′ c fs  record′ c′ fs′  fs  fs′
record′-injective₂ refl = refl

record′-injective :  {c c′ fs fs′}  record′ c fs  record′ c′ fs′  c  c′ × fs  fs′
record′-injective = < record′-injective₁ , record′-injective₂ >

constructor′-injective :  {c c′}  constructor′ c  constructor′ c′  c  c′
constructor′-injective refl = refl

infix 4 _≟_

_≟_ : DecidableEquality Definition
function cs        function cs′        =
  map′ (cong function) function-injective (cs Term.≟-Clauses cs′)
data-type pars cs  data-type pars′ cs′ =
  map′ (uncurry (cong₂ data-type)) data-type-injective
           (pars ℕ.≟ pars′ ×-dec List.≡-dec Name._≟_ cs cs′)
record′ c fs       record′ c′ fs′      =
  map′ (uncurry (cong₂ record′)) record′-injective
           (c Name.≟ c′ ×-dec List.≡-dec (Arg.≡-dec Name._≟_) fs fs′)
constructor′ d     constructor′ d′     =
  map′ (cong constructor′) constructor′-injective (d Name.≟ d′)
axiom              axiom               = yes refl
primitive′         primitive′          = yes refl

-- antidiagonal
function cs  data-type pars cs₁ = no  ())
function cs  record′ c fs = no  ())
function cs  constructor′ d = no  ())
function cs  axiom = no  ())
function cs  primitive′ = no  ())
data-type pars cs  function cs₁ = no  ())
data-type pars cs  record′ c fs = no  ())
data-type pars cs  constructor′ d = no  ())
data-type pars cs  axiom = no  ())
data-type pars cs  primitive′ = no  ())
record′ c fs  function cs = no  ())
record′ c fs  data-type pars cs = no  ())
record′ c fs  constructor′ d = no  ())
record′ c fs  axiom = no  ())
record′ c fs  primitive′ = no  ())
constructor′ d  function cs = no  ())
constructor′ d  data-type pars cs = no  ())
constructor′ d  record′ c fs = no  ())
constructor′ d  axiom = no  ())
constructor′ d  primitive′ = no  ())
axiom  function cs = no  ())
axiom  data-type pars cs = no  ())
axiom  record′ c fs = no  ())
axiom  constructor′ d = no  ())
axiom  primitive′ = no  ())
primitive′  function cs = no  ())
primitive′  data-type pars cs = no  ())
primitive′  record′ c fs = no  ())
primitive′  constructor′ d = no  ())
primitive′  axiom = no  ())