Creating a DSL

Stream: lean4

[Calvin Lee]

Hi, are there any tips on creating a DSL? other than creating a new syntax kind? Is do notation defined anywhere that I can take a look at?

[Julian Berman]

Parser here and elaborator here it'd seem, if you haven't found those already.

[Calvin Lee]

Hello! I'm working on creating a DSL using macros.
I haven't programmed in lean for awhile though, so I have a bit of a silly question to start out with: how do you create a new syntax category?

[Daniel Selsam]

declare_syntax_cat mycat

syntax ident  : mycat
syntax "(" mycat ")" : mycat

syntax "to_term"  mycat : term

macro_rules
  | `(to_term $a:ident)  => `($a)
  | `(to_term ($a))      => `(to_term $a)

syntax "`[mycat|" mycat "]" : term

macro_rules
  | `(`[mycat| $m]) => `(to_term $m)

#check `[mycat| ((Nat.add))]

[Calvin Lee]

Is there any way I can make my DSL translate into the do DSL?
i.e. instead of term i would translate into the do category?

[Mac]

@Daniel Selsam fyi,toTerm! should probably be to_term to fit with the new Lean 4 naming conventions, correct? ! is now only supposed to be used for functions that panic (see https://github.com/leanprover/lean4/issues/406); macro keywords use snake case now (like nat_lit) .

[Calvin Lee]

Is there any way to generate some identifier I can use that won't interfere with anything else?

[Mario Carneiro]

This is the default behavior if you use a variable name in a macro. This is called "macro hygiene" and is a major part of the lean 4 macro framework