Can DSLs avoid collision with keywords ?

Stream: metaprogramming / tactics

[Ray Myers]

Hi all, this one might be easy for people who have made Elaborators but I'm stuck. I'm reading the Lean Metaprogramming book and making an S-expression DSL, and I'm trying to figure out how to define my own kind of identifier that behaves differently than Lean's built-in ident. For instance, - should be allowed within an identifier, and keywords like if can be identifiers.

Could someone point me in the right direction? Thanks!

import Lean

inductive Sexpr : Type where
  | list : List Sexpr → Sexpr
  | symbol : String → Sexpr

declare_syntax_cat sexpr
syntax str : sexpr
syntax "(" sexpr* ")" : sexpr
syntax ident : sexpr


open Lean Elab Meta in
partial def elabSexpr : Syntax → MetaM Expr
  | `(sexpr| $x:ident) => mkAppM ``Sexpr.symbol  #[mkStrLit x.getId.getString!]
  | `(sexpr| ( $xs:sexpr* )  ) => do
    let xsElab ← xs.mapM (fun x => elabSexpr x)
    mkAppM `Sexpr.list #[ ← mkListLit  (mkConst `Sexpr) xsElab.toList  ]
  | _ => throwUnsupportedSyntax

elab ">>" p:sexpr "<<" : term => elabSexpr p

#check >> (s a) <<

#check >> (if a b) <<
-- unexpected token 'if'; expected ')'

[Ray Myers]

Looks like this overlaps with this question as luck would have it...

#general > How can I parse custom tokens with the Lean Parser?

[Spanky]

I had quite a similar few days ago (the overlapping question you linked).

I found a few solutions:

1. You can roll your own parser for identifiers. It's fiddly and tedious and requires a lot of effort to work well, but it allows you to define identifiers exactly like you want them.
2. Instead of ident, use rawIdent (Lean.Parser.rawIdent) in your syntax declaration (but keep using ident in the syntax quotations). rawIdent is a similar to ident, but which ignores the registered tokens and that doesn't support namespacing. It doesn't give you full control over what's an allowed identifier, but it's perfect for prototyping.
3. Use «if» instead of if, that way the ident parser treats it as an identifier rather than a keyword.