Declare types programmatically, via elaborators

Stream: metaprogramming / tactics

[Spanky]

I'm trying to declare some types from an elaborator.
I believe this code should do the trick, but it doesn't work:

def typeName := mkIdent `MyType
def typeName2 := mkIdent `MyType2
def fieldName := mkIdent `myField

-- this attempt works:
open Lean.Elab.Command in run_cmd
  elabCommand $ ← `(inductive $typeName where | x : $typeName)
  elabCommand $ ← `(#print $typeName)

-- this part doesn't :(
open Lean.Elab.Command in run_cmd
  elabCommand $ ← `(inductive $typeName2 where | $fieldName : $typeName2)
  elabCommand $ ← `(#print $typeName2)

It looks that the problem lies within the use of $fieldName: everything works if I used a regular ident within the syntax quotation.
But I can't use the working elab: the x field would have a secret name that I can't access, due to macro hygiene.

I tried to look into the elaborators that implements the inductive command, to create a type manually without relying on existing elaborators, but that logic seems very complicated.
The same is true for structure and other types.

How can I declare types from my elaborators?

[Kyle Miller]

What does "doesn't work" mean? I'm just seeing a parse error in the quotation, is that the problem?

Often you need to add syntax type annotations to get these to parse.

open Lean.Elab.Command in run_cmd
  elabCommand $ ← `(inductive $typeName2 where | $fieldName:ident : $typeName2)
  elabCommand $ ← `(#print $typeName2)

[Spanky]

Yes, the issue was the parse error.
I couldn't figure out that a syntax annotation would fix the problem and couldn't find that suggestion anywhere.
Thank you!

[Spanky]

Got another related(ish) question about elabs.
I'm trying to define some new command within an elab, and then use that same command within the same elab:

import Lean
open Lean.Elab.Command (elabCommand)

def cmdCat := Lean.mkIdent `command

-- this works
run_cmd elabCommand $ ← `(elab "#X" : $cmdCat => IO.println "X")
run_cmd elabCommand $ ← `(#X)

-- this fails
run_cmd
  elabCommand $ ← `(elab "#Y" : $cmdCat => IO.println "Y")
  elabCommand $ ← `(#Y) -- error: unexpected token '#'; expected identifier or term

-- this fails too, with a different error (it's the same thing, but without `#`)
run_cmd -- error: unexpected command
  elabCommand $ ← `(elab "Y" : $cmdCat => IO.println "Y")
  elabCommand $ ← `(Y)

I get the same errors if I try to run a command (#Y or Y) that hasn't been created yet outside of elaborators.

It feels to me like the syntax quotation creates the second TSyntax `commands before elaborating the first. But that shouldn't happen, since the syntax quotation itself is a CommandElabM action.

Why does this happen, and how can I make it work?

[Eric Wieser]

You'll get a better error from

run_cmd
  elabCommand $ ← `(command| elab "#Y" : $cmdCat => IO.println "Y")
  elabCommand $ ← `(command| #Y)

[Eric Wieser]

(which is consistent with and without #)

[Eric Wieser]

This works, but is ugly:

run_cmd
  elabCommand $ ← `(command| elab "Y" : $cmdCat => IO.println "Y")
  let e ← IO.ofExcept <| Lean.Parser.runParserCategory (← Lean.getEnv) `command <|
    -- need to parse a string, otherwise the syntax is parsed before we run the above line
    "Y"
  elabCommand $ e

[Eric Wieser]

Spanky said:

But that shouldn't happen, since the syntax quotation itself is a CommandElabM action.

My understanding is that the monad is only used to attach source information to the syntax, not to influence the parsing itself.

[Spanky]

Eric Wieser said:

My understanding is that the monad is only used to attach source information to the syntax, not to influence the parsing itself.

Ohh, so the syntax quotation gets evaluated before the actions are executed?
That's a bummer.

I wonder if there are better ways to achieve the goal.
Otherwise I guess I'll introduce some term-elaborator to generate the string and the expression which parses it.

[Sebastian Ullrich]

I would be interested in hearing more about your use case. This is not something that should usually come up because for new syntax to be used in a quotation, it must be sufficiently static, while having it generated implies there must be some dynamic parts.

[Blue]

[I'm still OP. Using an account I created from my parents' computer when I had no access to my mail]

Sebastian Ullrich said:

I would be interested in hearing more about your use case.

I was trying to write a command which wraps a list of other commands and was surprised to see it misbehave:

elab "{" cmds:command* "}" : command => cmds.forM elabCommand

{
elab "#greet" : command => IO.println "Hi!"
#greet -- uh oh! :-(
}

I've seen how namespace avoids the problem: it doesn't handle the commands it contains. It rather modifies the env, and then the end command undoes the changes.
In my case I wanted to manipulate the commands (filter and/or print the command to be executed).

In any case, I'm not doing anything important. Just playing with the elaborator to understand the whole system better.

[Sebastian Ullrich]

Yes we don't currently have an abstraction for introducing such scoping commands