------------------------------------------------------------------------
-- The Agda standard library
--
-- A universe for the types involved in the reflected syntax.
------------------------------------------------------------------------

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

module Reflection.AST.Universe where

open import Data.List.Base             using (List)
open import Data.String.Base           using (String)
open import Data.Product.Base          using (_×_)
open import Reflection.AST.Argument    using (Arg)
open import Reflection.AST.Abstraction using (Abs)
open import Reflection.AST.Term        using (Term; Pattern; Sort; Clause)

data Univ : Set where
  ⟨term⟩   : Univ
  ⟨pat⟩    : Univ
  ⟨sort⟩   : Univ
  ⟨clause⟩ : Univ
  ⟨list⟩   : Univ → Univ
  ⟨arg⟩    : Univ → Univ
  ⟨abs⟩    : Univ → Univ
  ⟨named⟩  : Univ → Univ

pattern ⟨tel⟩ = ⟨list⟩ (⟨named⟩ (⟨arg⟩ ⟨term⟩))

⟦_⟧ : Univ → Set
⟦ ⟨term⟩    ⟧ = Term
⟦ ⟨pat⟩     ⟧ = Pattern
⟦ ⟨sort⟩    ⟧ = Sort
⟦ ⟨clause⟩  ⟧ = Clause
⟦ ⟨list⟩ k  ⟧ = List ⟦ k ⟧
⟦ ⟨arg⟩ k   ⟧ = Arg ⟦ k ⟧
⟦ ⟨abs⟩ k   ⟧ = Abs ⟦ k ⟧
⟦ ⟨named⟩ k ⟧ = String × ⟦ k ⟧