Showcasing usage of declareData and defineData now being tested in Zekt/agda.

DeclareData.agda

{-# OPTIONS -v meta:5 #-}
--{-# OPTIONS -v tc.data.con:16 #-}
--{-# OPTIONS -v tc.unquote.def:11 #-}
--{-# OPTIONS -v tc.data.sort:21 #-}
--{-# OPTIONS -v tc.data.con.comp:6 #-}
--{-# OPTIONS -v tc.conv.term:21 #-}
--{-# OPTIONS -v scope.lhs:60 #-}
--{-# OPTIONS -v scope.operators:60 #-}

open import Reflection
open import Agda.Builtin.Reflection
import Reflection.Name
import Reflection.Term
import Level as Level
--open import Reflection.Clause
open import Tactic.MonoidSolver

open import Data.Unit
open import Data.Empty
open import Data.Bool
open import Data.Nat
open import Data.Nat.Show
open import Data.Nat.Properties
open import Data.List
open import Agda.Builtin.Sigma
open import Data.Product using (_×_; proj₁; proj₂)
open import Data.Bool
open import Data.String renaming (_++_ to _⧺_)
open import Function.Base
open import Relation.Nullary
import Data.Fin

open import Relation.Binary.PropositionalEquality
  using (_≡_;
 refl)

macro
  showTerm′ : Term → Term → TC ⊤
  showTerm′ t hole = do
    debugPrint "meta" 2 [ termErr t ]
    unify hole (quoteTerm tt)

macro
  showType : Name → Term → TC _
  showType t hole = do
               t2 ← getType t
               debugPrint "meta" 2 [ termErr t2 ]
               unify hole (quoteTerm tt)

showCs : List Name → TC ⊤
showCs [] = debugPrint "meta" 2 [ strErr "All constructors printed." ]
showCs (x ∷ l) = getType x >>= λ c →
  debugPrint "meta" 2 (strErr "Constructor "
                         ∷ nameErr x
                         ∷ strErr (" is defined as:\n" ⧺ (showTerm c))
                         ∷ []) >>
  showCs l

showDef′ : Name → TC _
showDef′ n = do
  getDefinition n >>= λ where
    d@(data-type _ cs) → do
      debugPrint "meta" 2 [ strErr (showDefinition d) ]
      showCs cs
    d → debugPrint "meta" 2 [ strErr (showDefinition d) ]
  getType n >>= λ x →
    debugPrint "meta" 2 (strErr "The type of the declared datatype '"
                        ∷ nameErr n
                        ∷ strErr "' is: "
                        ∷ termErr x
                        ∷ [])

newData : Name → ℕ → Type → List (Name × Type) → TC ⊤
newData n npars t cs = do
  declareData n npars t
  defineData n cs
  getType n >>= λ x →
    debugPrint "meta" 2 (strErr "The type of the declared datatype '"
                           ∷ nameErr n
                           ∷ strErr "' is: "
                           ∷ termErr x
                           ∷ [])
  --getDefinition n >>= λ where
  --  d → debugPrint "meta" 2 [ strErr (showDefinition d) ]
  --showDef′ n
  printDef "meta" 5 n

newtype′ : ℕ × Type
newtype′ = (1 , (quoteTerm ((idx : ℕ) → (A : Set) → List A → Set)))

newcon′ : Name → Term
newcon′ n = (pi (hArg (quoteTerm ℕ))
                (abs "idx" (pi (vArg (quoteTerm Set))
                               (abs "A" (pi (vArg (def (quote List) (vArg (var 0 []) ∷ [])))
                                            (abs "_" (def n (vArg (var 2 [])
                                                            ∷ vArg (var 1 [])
                                                            ∷ vArg (var 0 [])
                                                            ∷ []))))))))
unquoteDecl newtype conpi conpi₁ = do let (t₁ , t₂) = newtype′
                                      newData newtype t₁ t₂ ((conpi , newcon′ newtype)
                                                     ∷ (conpi₁ , newcon′ newtype)
                                                     ∷ [])