Trouble writing a parser involving atoms

Stream: metaprogramming / tactics

[Robert Maxton]

I'm trying to define a syntax f ⇑(op) g, which expands to fun x => op (f x) (g x). Unfortunately, it seems very difficult to work with atoms in syntax. So far, I've come up with

def liftFun (op : μ → ν → β) (f : α → μ) (g : α → ν) : α → β := λ x => op (f x) (g x)

macro (name := coe_liftFun) f:term " ⇑" op:(noWs atom) g:term : term => withFreshMacroScope do
  let cdot := Syntax.mkLit `Lean.Parser.Term.cdot "·"
  let oparen := Syntax.mkLit `Lean.Parser.Term.parenLeft "("
  let cparen := Syntax.mkLit `Lean.Parser.Term.parenRight ")"
  let opfun := TSyntax.mk <| Syntax.node5 (SourceInfo.fromRef op) `term oparen cdot op cdot cparen
  ``(liftFun $opfun $f $g)

which at least compiles, but it doesn't work:

#check (λ x => x) ⇑+ (λ x => x) --unexpected token '+'; expected string literal or term

Suggestions?

[Mac Malone]

@Robert Maxton What is atom in your example (in op:(noWs atom))? That is not a parser/syntax in the Lean core. Could you produce a richer #mwe?

[Robert Maxton]

Mac Malone said:

Robert Maxton What is atom in your example (in op:(noWs atom))? That is not a parser/syntax in the Lean core. Could you produce a richer #mwe?

Lean.Parser.Syntax.atom ?

[Robert Maxton]

There honestly isn't much more MWE I can give, the entire section aside from imports is just

section «notation»
open Lean Parser Syntax

def liftFun (op : μ → ν → β) (f : α → μ) (g : α → ν) : α → β := λ x => op (f x) (g x)

set_option trace.Elab.definition true in
macro (name := coe_liftFun) f:term " ⟰" op:(noWs atom) g:term : term => withFreshMacroScope do
  let cdot := Syntax.mkLit `Lean.Parser.Term.cdot "·"
  let oparen := Syntax.mkLit `Lean.Parser.Term.parenLeft "("
  let cparen := Syntax.mkLit `Lean.Parser.Term.parenRight ")"
  let opfun := TSyntax.mk <| Syntax.node5 (SourceInfo.fromRef op) `term oparen cdot op cdot cparen
  ``(liftFun $opfun $f $g)


#check (λ x => x) ⟰+ (λ x => x) --unexpected token '+'; expected string literal
end «notation»

I changed from ⇑ to ⟰ to avoid collision with CoeFn; the new error message (which now insists on a string literal specifically) is a hint, I think.

[Kyle Miller]

It looks like the definition of atom is strLit, so it would be expecting (λ x => x) ⟰"+" (λ x => x).

I don't think you can get this syntax to work the way you expect it to work. Best I can think of is either have it take a term and then you write something like (λ x => x) ⟰(·+·) (λ x => x), or you define a ⟰+ type of operator for each operator you want to lift.

[Kyle Miller]

The issue is that you need to somehow map the token + to the right syntax kind. The Syntax.node5 you have won't produce a + node.

Take a look at this:

def foo : Lean.MacroM Lean.Syntax := `(1 + 2)
#print foo
/-
...
Lean.Syntax.node3 info `term_+_ (Lean.Syntax.node1 info `num (Lean.Syntax.atom info "1"))
  (Lean.Syntax.atom info "+") (Lean.Syntax.node1 info `num (Lean.Syntax.atom info "2"))
...
-/

The kind happens to be called term_+_, not term. That name is generated by the notation command, and it's not something you're supposed to refer to in user code.

[Robert Maxton]

I mean, I think that bit is soluble? Worst case I can produce and then parse a string or a quotation or something, I think?

The bigger issue is that Lean won't even recognize ⟰+ correctly to begin with; I'd need some way of matching "a ⟰ followed by any number of any non-whitespace characters followed by a whitespace", which I was hoping atom would do but apparently not.

[Kyle Miller]

Parsing a non-whitespace characters is certainly possible, but before going down that path of constructing a string and then parsing something, do you have an idea of how wide of an array of binary operators you want to support?

If it's not many, I would go with ⟰+, ⟰-, ⟰*, ⟰/, and the others that come up.

It's also fairly straightforward to make a macro that generates notation, so you can declare_lift_op "+", declare_lift_op "-", etc.

[Kyle Miller]

import Lean

set_option autoImplicit true

def liftFun (op : μ → ν → β) (f : α → μ) (g : α → ν) : α → β := λ x => op (f x) (g x)

open Lean Macro

macro "declare_lift_op " op:str " => " t:term : command => do
  let op' := Syntax.mkStrLit s!" ⇑{op.getString} "
  `(notation f $op':str g => liftFun $t f g)

declare_lift_op "+" => (· + ·)
declare_lift_op "-" => (· - ·)

variable (φ ψ : Nat → Int)
#check φ ⇑+ ψ
-- liftFun (fun x x_1 ↦ x + x_1) φ ψ : Nat → Int

[Kyle Miller]

You could try synthesizing t from the op string by parsing s!"(· {op.getString} ·)" but that feels a little hacky to me.

[Kyle Miller]

With this, if you import Mathlib.Mathport.Notation, switch notation to notation3, and write declare_lift_op "+" => HAdd.hAdd, then φ ⇑+ ψ even pretty prints as φ ⇑+ ψ.

[Kyle Miller]

Here's another sort of solution:

import Lean

set_option autoImplicit true

def liftFun (op : μ → ν → β) (f : α → μ) (g : α → ν) : α → β := λ x => op (f x) (g x)

open Lean Macro

declare_syntax_cat binop
syntax "binop(" binop ")" : term

macro f:term " ⇑" op:binop g:term : term => `(liftFun binop($op) $f $g)

syntax "+" : binop
macro_rules | `(binop(+)) => `((· + ·))

syntax "-" : binop
macro_rules | `(binop(-)) => `((· - ·))

variable (φ ψ : Nat → Int)
#check φ ⇑+ ψ
-- liftFun (fun x x_1 ↦ x + x_1) φ ψ : Nat → Int

[Robert Maxton]

Hmmm... I sort of see. The issue is primarily that it's hard to even talk about the 'atom' part of the syntax in a way Lean will pay attention to.

Okay, I might end up resorting to one of those options, then. Thanks.

[Mario Carneiro]

I'm quite sure you can write a Parser that steals an atom off the syntax stack, but this is not something any existing parser does currently

[Mario Carneiro]

it would be somewhat abstraction breaking, e.g. you could pull a ( and then what?

[Robert Maxton]

Mm. Ideally, f ⇑(foo) g would act exactly like you typed liftFun (· (foo) ·) f g for any foo, but of course I see that that wouldn't be covered by my simplistic "just parse everything until the next whitespace" spec in the case of parenthesized operators. And of course "compound atoms" would be a horrible contradiction in terms on the syntax design level.

[Kyle Miller]

By the way, with this approach you can have it parse a term too:

syntax (priority := low) term:max : binop
macro_rules | `(binop($t:term)) => pure t

#check φ ⇑(· / ·) ψ

I made that low-priority because there's a source of ambiguity in ⇑-, whether the - is the beginning of a negation.

[Kyle Miller]

And one improvement to the syntax is

macro f:term " ⇑" noWs op:binop g:term : term => `(liftFun binop($op) $f $g)

The noWs ensures it can't be used with whitespace after ⇑.

[Mac Malone]

Robert Maxton said:

Lean.Parser.Syntax.atom ?

Oops! I missed that! For future reference, the atom here is the string literal in a syntax vommand. For example:

syntax "foo" : term
    -- ^^^^^ this is an `atom`