module _ where
open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
open import Agda.Builtin.Unit
open import Agda.Builtin.Nat hiding (_==_)
open import Agda.Builtin.List
open import Agda.Builtin.Equality
Tactic = Term → TC ⊤
macro
-- Get the (first) constructor of a data or record type
`con : Name → Tactic
`con x hole = getDefinition x >>= λ where
(data-type _ (c ∷ _)) → unify hole (lit (name c))
(record-type c fs) → unify hole (lit (name c))
_ → typeError (strErr "bad" ∷ [])
-- Look up the name of a name
`typeOf : Name → Tactic
`typeOf x hole = getType x >>= unify hole
-- Some convenience function
data ⊥ : Set where
infix 0 _∋_
_∋_ : ∀ {a} (A : Set a) → A → A
A ∋ x = x
_≢_ : ∀ {a} {A : Set a} → A → A → Set a
x ≢ y = x ≡ y → ⊥
-- If we put a data type and a record type in a parameterised module
module Param (A : Set) where
data Data : Set where
mkData : A → Data
record Record : Set where
constructor mkRecord
field getField : A
-- and then apply the module to some argument
open Param Nat
-- getDefinition Data behaves as expected, returning a definition with a constructor
-- Data.mkData : Nat → Data
_ = `con Data ≡ quote Data.mkData ∋ refl
_ = `typeOf Data.mkData ≡ (Nat → Data) ∋ refl
-- Although it's interesting that we get Data.mkData and not mkData (and that these are
-- not the same).
_ = quote Data.mkData ≢ quote mkData ∋ λ ()
-- But, we don't get `Param.mkData : {A : Set} → A → Param.Data A`
_ = `con Data ≢ quote Param.mkData ∋ λ ()
_ = `typeOf Param.mkData ≡ ({A : Set} → A → Param.Data A) ∋ refl
-- For the record type, however, that is exactly what we get
_ = `con Record ≡ quote Param.mkRecord ∋ refl
_ = `typeOf Param.mkRecord ≡ ({A : Set} → A → Param.Record A) ∋ refl
-- What we should get is `mkRecord`
_ = `con Record ≢ quote mkRecord ∋ λ ()
_ = `typeOf mkRecord ≡ (Nat → Record) ∋ refl
-- The fact that we get `Data.mkData` and not `mkData` is a clue to the problem. There
-- is no equivalent of `Data.mkData` for the record type: record constructors are not
-- part of the record module.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4