Topic: Creating a DSL
Calvin Lee (Mar 20 2021 at 05:33):
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 (Mar 20 2021 at 13:32):
Calvin Lee (May 05 2021 at 18:18):
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 (May 05 2021 at 18:27):
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 (May 05 2021 at 18:34):
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?
@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
Calvin Lee (May 05 2021 at 19:41):
Is there any way to generate some identifier I can use that won't interfere with anything else?
Mario Carneiro (May 05 2021 at 20:45):
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
Last updated: May 18 2021 at 23:14 UTC