[Agda] A question about the innards of C-c C-d

[Eduardo Ochs]

Hi list,

if we define the function eek in Elisp as:

  (defun eek (str)
    "Execute STR as a keyboard macro. See `edmacro-mode' for the exact
format.\n
  An example: (eek \"C-x 4 C-h\")"
    (interactive "sKeys: ")
    (execute-kbd-macro (read-kbd-macro str)))

and we create a file /tmp/test/T.agda containing this,

--snip--snip--
open import Level
MySet1 : Set₂
MySet1 = Set (Level.suc Level.zero)

postulate B₁ :                                              Set
postulate B₂ : (y₁ : B₁) →                                  Set
postulate A₁ : (y₁ : B₁) → (y₂ : B₂ y₁) →                   Set
postulate A₂ : (y₁ : B₁) → (y₂ : B₂ y₁) → (x₁ : A₁ y₁ y₂) → Set

record R (y₁ : B₁) (y₂ : B₂ y₁) : MySet1 where
  field
    x₁ : A₁ y₁ y₂
    x₂ : A₂ y₁ y₂ x₁

postulate ay₁ : B₁
postulate ay₂ : B₂ ay₁
postulate ax₁ : A₁ ay₁ ay₂
postulate ax₂ : A₂ ay₁ ay₂ ax₁
postulate ar  : R  ay₁ ay₂

-- (eek "C-a C-c C-d  R           RET")
-- (eek "C-a C-c C-d  R.x₁        RET")
-- (eek "C-a C-c C-d  R.x₂        RET")
-- (eek "C-a C-c C-d  ar          RET")
-- (eek "C-a C-c C-d  R.x₁ SPC ar RET")
--snip--snip--

then the sexps with "eek" work as buttons that can be executed with
C-e C-x C-e, and whose effects are to display the types of the
expressions "R", "R.x₁", "R.x₂", "ar", and "R.x₁ ar" in the second
window... note that the "R.x₁ SPC ar" in the last sexp was sort of
translated to "R.x₁ ar".

I am looking for a better way to do that, but I am having trouble to
understand the innards of the function bound to C-c C-d -
agda2-infer-type-maybe-toplevel - because it uses at least two levels
of macros...

So: suppose that I define foo as:

  (defun foo ()
    "Running M-x foo in agda2-mode should be equivalent to
     typing C-c C-d R.x₁ ar RET"
    (interactive)
    (bar "R.x₁ ar"))

what is the right way to define bar in a low-level way? Let's suppose
for simplicity that we just want to make this work in situations in
which agda2-infer-type-maybe-toplevel would run
agda2-infer-type-toplevel, and we don't care for the cases in which it
would run agda2-infer-type...

  Thanks in advance!
    Eduardo Ochs
    http://angg.twu.net/#eev
    http://angg.twu.net/eev-intros/find-eev-quick-intro.html#3
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20211227/b256d9e5/attachment-0001.html>