Zulip Chat Archive

Stream: new members

Topic: How do I write a "#check_syntax"?

Eduardo Ochs (May 16 2024 at 02:45):

Hi all,

I'm taking far too long to do this myself, so I decided to ask...

In the section "Free form syntax declarations" of the metaprogramming book there's an example - inside "namespace Playground2" - in which the command "#check_failure ⊥ OR (⊤ AND ⊥)" fails with the error "elaboration function for 'Playground2.term_OR_' has not been implemented". I only found that error message in two places in the source:

here in Lean/Elab/Command.lean, and
here in Lean/Elab/Term.lean,

but lots of things happen before that error message...

How do I write a variant of #check or #check_failure - let me call that variant "#check_syntax" - that parses the rest of the line like #check or #check_failure, i.e., like this,

@[builtin_command_parser] def check := leading_parser "#check " >> termParser

but that does not try to elaborate the result of "termParser"? I would like it to just print the resulting Syntax object...

Eric Wieser (May 16 2024 at 02:50):

I usually use #check `(my_custom_syntax) for this

Eduardo Ochs (May 16 2024 at 03:03):

Neat! If I run this,

#check `(42 + "foo")

then the output is:

do
  let info ← Lean.MonadRef.mkInfoFromRefPos
  let scp ← Lean.getCurrMacroScope
  let mainModule ← Lean.getMainModule
  pure
      {
        raw :=
          Lean.Syntax.node3 info `term_+_ (Lean.Syntax.node1 info `num (Lean.Syntax.atom info "42"))
            (Lean.Syntax.atom info "+")
            (Lean.Syntax.node1 info `str (Lean.Syntax.atom info "\"foo\"")) } : ?m.233 (Lean.TSyntax `term) (lsp)

Eduardo Ochs (May 16 2024 at 03:04):

I would still like to learn how to write a new command that works as the first half of #check, but that helps!

Kyle Miller (May 16 2024 at 03:08):

Here:

namespace Playground2

scoped syntax "⊥" : term -- ⊥ for false
scoped syntax "⊤" : term -- ⊤ for true
scoped syntax:40 term " OR " term : term
scoped syntax:50 term " AND " term : term

elab "#check_syntax " t:term : command => do
  Lean.logInfo m!"{t}"

#check_syntax ⊥ OR (⊤ AND ⊥)
-- ⊥ OR (⊤ AND ⊥)

end Playground2

Kyle Miller (May 16 2024 at 03:08):

It doesn't look like it's doing anything, but it's parsing the syntax (getting a Syntax) and then printing that Syntax back out.

Kyle Miller (May 16 2024 at 03:10):

If you change the logging line to Lean.logInfo m!"{repr t.raw}" you can see the structure of the Syntax.

Eduardo Ochs (May 16 2024 at 07:05):

Fantastic! Many thanks! :upside_down::upside_down::upside_down:
If anyone else is reading this, here is a version that is trivial to run:

import Lean.Elab.Command

namespace Playground2

scoped syntax "⊥" : term
scoped syntax "⊤" : term
scoped syntax:40 term " OR " term : term
scoped syntax:50 term " AND " term : term

elab "#check_syntax " t:term : command => do Lean.logInfo m!"{t}"
elab "#check_syntax " t:term : command => do Lean.logInfo m!"{repr t.raw}"

#check_syntax ⊥ OR (⊤ AND ⊥)

end Playground2

The definition of "#check_syntax" that holds is the last one - to change its behavior, reorder the "elab" lines.

Eduardo Ochs (May 17 2024 at 06:37):

(deleted)

Last updated: May 02 2025 at 03:31 UTC