{-# OPTIONS --safe --without-K #-}

module Reflection.Syntax where

open import Meta.Prelude

open import Reflection.AST.Argument public
  hiding (map)
open import Reflection.AST.Term public
  hiding (_≟_; getName)
open import Reflection.AST.Name public
  hiding (_≟_; _≡ᵇ_; _≈_; _≈?_)
open import Reflection.AST.Definition public
  hiding (_≟_)
open import Reflection.AST.Meta public
  hiding (_≟_; _≡ᵇ_; _≈_; _≈?_)
open import Reflection.AST.Abstraction public
  using (unAbs)

open import Agda.Builtin.Reflection public
  using (ArgInfo; Modality; Visibility; Literal; Meta)

open import Reflection.AST.Argument public
  using (Arg; arg)
open import Reflection.AST.Argument.Visibility public
  using (Visibility; visible; hidden; instance′)
open import Reflection.AST.Argument.Information public
  using (ArgInfo; arg-info)
open import Reflection.AST.Abstraction public
  using (Abs; abs; unAbs)
open import Reflection.AST.Argument public
  using (vArg; hArg; iArg; unArg; _⟨∷⟩_; map-Args)
open import Reflection public
  using ( Name; Meta; Literal; Pattern; Clause
        ; ErrorPart; strErr
        ; Term; Type; pi; var; con; def; lam; pat-lam; agda-sort; lit; meta; unknown
        ; Definition; data-cons; data-type; record-type
        )

open import Reflection using (hidden; instance′; TC)

-- ** Smart constructors

-- arguments
pattern hArg? = hArg unknown
pattern vArg? = vArg unknown
pattern iArg? = iArg unknown

-- variables
pattern ♯ n = var n []
pattern ♯_⟦_⟧ n x = var n (vArg x ∷ [])
pattern ♯_⟦_∣_⟧ n x y = var n (vArg x ∷ vArg y ∷ [])

-- patterns
pattern `_ x = Pattern.var x
pattern `∅   = Pattern.absurd 

-- clauses
pattern ⟦⦅_⦆∅⟧ tel = absurd-clause tel (vArg `∅ ∷ [])
pattern ⟦∅⟧ = absurd-clause [] (vArg `∅ ∷ [])

pattern ⟦⇒_⟧ k = clause [] [] k
pattern ⟦⦅_⦆⇒_⟧ tel k = clause tel [] k

pattern ⟦_⇒_⟧ x k = clause [] (vArg x ∷ []) k
pattern ⟦_⦅_⦆⇒_⟧ x tel k = clause tel (vArg x ∷ []) k

pattern ⟦_∣_⇒_⟧ x y k = clause [] (vArg x ∷ vArg y ∷ []) k
pattern ⟦_∣_⦅_⦆⇒_⟧ x y tel k = clause tel (vArg x ∷ vArg y ∷ []) k

pattern ⟦_∣_∣_⇒_⟧ x y z k = Clause.clause [] (vArg x ∷ vArg y ∷ vArg z ∷ []) k
pattern ⟦_∣_∣_⦅_⦆⇒_⟧ x y z tel k = Clause.clause tel (vArg x ∷ vArg y ∷ vArg z ∷ []) k

-- lambdas
pattern `λ_⇒_       x     k = lam visible (abs x k)
pattern `λ⟦_∣_⇒_⟧   x y   k = `λ x ⇒ `λ y ⇒ k
pattern `λ⟦_∣_∣_⇒_⟧ x y z k = `λ x ⇒ `λ y ⇒ `λ z ⇒ k

pattern `λ⟅_⟆⇒_     x k = lam hidden (abs x k)
pattern `λ⦃_⦄⇒_     x k = lam instance′ (abs x k)

pattern `λ⦅_⦆∅ tel = pat-lam (⟦⦅ tel ⦆∅⟧ ∷ []) []
pattern `λ∅ = pat-lam (⟦∅⟧ ∷ []) []

pattern `λ⟦_⇒_⟧ p k = pat-lam ($\begin{pmatrix} \,\href{Reflection.Syntax.html#2597}{\htmlId{2597}{\htmlClass{Bound}{\text{p}}}}\, \,\href{Reflection.Syntax.html#1829}{\htmlId{2599}{\htmlClass{InductiveConstructor Operator}{\text{⇒}}}}\, \,\href{Reflection.Syntax.html#2601}{\htmlId{2601}{\htmlClass{Bound}{\text{k}}}}\, \end{pmatrix}$ ∷ []) []
pattern `λ⟦_⦅_⦆⇒_⟧ p tel k = pat-lam ($\begin{pmatrix} \,\href{Reflection.Syntax.html#2654}{\htmlId{2654}{\htmlClass{Bound}{\text{p}}}}\, \,\href{Reflection.Syntax.html#1875}{\htmlId{2656}{\htmlClass{InductiveConstructor Operator}{\text{⦅}}}}\, \,\href{Reflection.Syntax.html#2658}{\htmlId{2658}{\htmlClass{Bound}{\text{tel}}}}\, \,\href{Reflection.Syntax.html#1875}{\htmlId{2662}{\htmlClass{InductiveConstructor Operator}{\text{⦆⇒}}}}\, \,\href{Reflection.Syntax.html#2665}{\htmlId{2665}{\htmlClass{Bound}{\text{k}}}}\, \end{pmatrix}$ ∷ []) []

pattern `λ⟦_⇒_∣_⇒_⟧ p₁ k₁ p₂ k₂ = pat-lam ($\begin{pmatrix} \,\href{Reflection.Syntax.html#2724}{\htmlId{2724}{\htmlClass{Bound}{\text{p₁}}}}\, \,\href{Reflection.Syntax.html#1829}{\htmlId{2727}{\htmlClass{InductiveConstructor Operator}{\text{⇒}}}}\, \,\href{Reflection.Syntax.html#2729}{\htmlId{2729}{\htmlClass{Bound}{\text{k₁}}}}\, \end{pmatrix}$ ∷ $\begin{pmatrix} \,\href{Reflection.Syntax.html#2738}{\htmlId{2738}{\htmlClass{Bound}{\text{p₂}}}}\, \,\href{Reflection.Syntax.html#1829}{\htmlId{2741}{\htmlClass{InductiveConstructor Operator}{\text{⇒}}}}\, \,\href{Reflection.Syntax.html#2743}{\htmlId{2743}{\htmlClass{Bound}{\text{k₂}}}}\, \end{pmatrix}$ ∷ []) []
pattern `λ⟦_⦅_⦆⇒_∣_⦅_⦆⇒_⟧ p₁ tel₁ k₁ p₂ tel₂ k₂ = pat-lam ($\begin{pmatrix} \,\href{Reflection.Syntax.html#2818}{\htmlId{2818}{\htmlClass{Bound}{\text{p₁}}}}\, \,\href{Reflection.Syntax.html#1875}{\htmlId{2821}{\htmlClass{InductiveConstructor Operator}{\text{⦅}}}}\, \,\href{Reflection.Syntax.html#2823}{\htmlId{2823}{\htmlClass{Bound}{\text{tel₁}}}}\, \,\href{Reflection.Syntax.html#1875}{\htmlId{2828}{\htmlClass{InductiveConstructor Operator}{\text{⦆⇒}}}}\, \,\href{Reflection.Syntax.html#2831}{\htmlId{2831}{\htmlClass{Bound}{\text{k₁}}}}\, \end{pmatrix}$ ∷ $\begin{pmatrix} \,\href{Reflection.Syntax.html#2840}{\htmlId{2840}{\htmlClass{Bound}{\text{p₂}}}}\, \,\href{Reflection.Syntax.html#1875}{\htmlId{2843}{\htmlClass{InductiveConstructor Operator}{\text{⦅}}}}\, \,\href{Reflection.Syntax.html#2845}{\htmlId{2845}{\htmlClass{Bound}{\text{tel₂}}}}\, \,\href{Reflection.Syntax.html#1875}{\htmlId{2850}{\htmlClass{InductiveConstructor Operator}{\text{⦆⇒}}}}\, \,\href{Reflection.Syntax.html#2853}{\htmlId{2853}{\htmlClass{Bound}{\text{k₂}}}}\, \end{pmatrix}$ ∷ []) []

-- function application
pattern _∙ n = def n []
pattern _∙⟦_⟧ n x = def n (vArg x ∷ [])
pattern _∙⟦_∣_⟧ n x y = def n (vArg x ∷ vArg y ∷ [])
pattern _∙⟦_∣_∣_⟧ n x y z = def n (vArg x ∷ vArg y ∷ vArg z ∷ [])
pattern _∙⟦_∣_∣_∣_⟧ n x y z w = def n (vArg x ∷ vArg y ∷ vArg z ∷ vArg w ∷ [])

pattern _◆ n = con n []
pattern _◆⟦_⟧ n x = con n (vArg x ∷ [])
pattern _◆⟦_∣_⟧ n x y = con n (vArg x ∷ vArg y ∷ [])

pattern _◇ n = Pattern.con n []
pattern _◇⟦_⟧ n x = Pattern.con n (vArg x ∷ [])
pattern _◇⟦_∣_⟧ n x y = Pattern.con n (vArg x ∷ vArg y ∷ [])

pattern `Set = agda-sort (set (quote 0ℓ ∙))

-- ** useful type aliases
PatTelescope = Telescope
Context      = Args Type
TTerm        = Term × Type
Hole         = Term
THole        = Hole × Type