conflicting with Lean keywords

Stream: metaprogramming / tactics

[Arthur Paulino]

I have a DSL implemented in Lean, with a custom elaborator.
But Lean's syntax is interfering with it. For example, I can't have a variable called Type because Lean complains "unexpected token 'Type'" ("Type" glows blue).

Is there a way to disable Lean's syntax within my own syntactical scope?

[Robin Arnez]

You can write a docs#Lean.Parser.Parser but this is a bit hacky:

import Lean

declare_syntax_cat myCat

open Lean Parser
def myCatParser : Parser := withFn (p := categoryParser `myCat 0) <|
  adaptUncacheableContextFn fun ctx =>
    -- this makes "bad", "good" and "test" the only tokens
    let table : TokenTable := ["bad", "good", "test"].foldl (fun acc tk => acc.insert tk tk) {}
    { ctx with tokens := table }

elab "#test_me " stx:myCatParser : command => do
  Lean.logInfo stx

-- you can simply use Lean keywords in identifiers
syntax "test " ident : myCat

#test_me test Type
#test_me test let
#test_me test def

-- but oh no: it doesn't update the token table so
-- `term` is left with only the three tokens (see below)
syntax "bad " term : myCat

-- so if you want to transition, make sure to restore the token table
def restoreTermParser : Parser := withFn (p := termParser) <|
  adaptUncacheableContextFn fun ctx =>
    { ctx with tokens := getTokenTable ctx.env }

syntax "good " restoreTermParser : myCat

#test_me bad let a 5 Type oh no _ stop sorry do by -- interpreted as an application
#test_me good let a := 5; 5 -- correctly interpreted as let

[Robin Arnez]

You only need to use these special parsers on transition; and if you don't want to hardcode the token table, you can retrieve it from the environment:

import Lean

declare_syntax_cat myCat

open Lean Parser

def collectTokens (env : Environment) (cat : Name) (table : TokenTable) : TokenTable :=
  let state := parserExtension.getState env
  let cat := state.categories.find! cat
  let table := cat.tables.leadingParsers.foldl (init := table) fun acc (p, _) =>
    (p.info.collectTokens []).foldl (fun acc tk => acc.insert tk tk) acc
  let table := cat.tables.trailingParsers.foldl (init := table) fun acc (p, _) =>
    (p.info.collectTokens []).foldl (fun acc tk => acc.insert tk tk) acc
  let table := cat.tables.leadingTable.foldl (init := table) fun acc _ p =>
    p.foldl (init := acc) fun acc (p, _) =>
      (p.info.collectTokens []).foldl (fun acc tk => acc.insert tk tk) acc
  let table := cat.tables.trailingTable.foldl (init := table) fun acc _ p =>
    p.foldl (init := acc) fun acc (p, _) =>
      (p.info.collectTokens []).foldl (fun acc tk => acc.insert tk tk) acc
  table

def myCatParser : Parser := withFn (p := categoryParser `myCat 0) <|
  adaptUncacheableContextFn fun ctx =>
    let table : TokenTable := {}
    let table : TokenTable := collectTokens ctx.env `myCat table
    --let table : TokenTable := collectTokens ctx.env `myOtherCat table -- for any nested categories
    { ctx with tokens := table }

-- perfectly fine, since the token table is already updated
syntax myCat " + " myCat : myCat
...

[Arthur Paulino]

Thanks a lot for your answer!
So there's no principled solution to this issue

[Robin Arnez]

Yeah, parsing is currently not build to support multiple token tables