custom syntax outer conflicts

Stream: metaprogramming / tactics

[Mirek Olšák]

I got confused by the idea of a custom syntax category, with the examples such as
in the metaprogramming book, it looks like we are defining a local language only to be activated between >> and << in that example. However, once we add the true token to our syntax, we cannot use the standard Bool.true outside anymore

declare_syntax_cat imp_lit
syntax "true"    : imp_lit
#check true   -- :-( unexpected token 'true'; expected term

On the other hand, declaring tactic syntax does not collide with standard terms.

syntax "true"    : tactic
#check true   -- :-) Bool.true : Bool

Could I make a custom syntax category work like tactic in the sense, that it only gets activated in a specific environment, and doesn't mess up with usual term elaboration?

[Aaron Liu]

I think it was something like declare_syntax_cat (behavior := symbol) imp_lit

[Mirek Olšák]

Thanks,

declare_syntax_cat imp_lit  (behavior := symbol)

looks like doing something.
It doesn't seem to work for binary operators, but for them, even tactics declare a new token. I mean something like

syntax num "div" num : imp_lit

I suppose I could create a new category just for them...

[Robin Arnez]

Or use &"div"

[Mirek Olšák]

How does that work? I cannot match on it

declare_syntax_cat imp_lit (behavior := symbol)
syntax imp_lit &"div" imp_lit : imp_lit

open Lean in
def process (stx : TSyntax `imp_lit) : Elab.TermElabM Expr :=
  match stx with
  | `(imp_lit|$a:imp_lit div $b:imp_lit) => return default
  | _ => return default

[Robin Arnez]

Huh, I guess there are some subtleties when you try to use it as a binary operator?

[Robin Arnez]

This seems to work I guess

import Lean

open Lean Parser Elab

declare_syntax_cat imp_lit (behavior := symbol)

@[imp_lit_parser]
def impDiv : TrailingParser := trailing_parser
  nonReservedSymbol "div" true >> categoryParser `imp_lit 0

open Lean in
def process (stx : TSyntax `imp_lit) : Elab.TermElabM Expr :=
  match stx with
  | `(imp_lit| $a:imp_lit div $b:imp_lit) => return default
  | _ => return default

[Mirek Olšák]

magic :slight_smile: