json elaborator

Stream: lean4

[Patrick Massot]

ProofWidgets has a nice json% elaborator but it requires a open scoped Json that will break things, especially the words "true" and "false". Is there a way to get this elaborator without opening those scoped notations? Or is there a way to open it for one line of code in a function. @Wojciech Nawrocki

[Wojciech Nawrocki]

You can open it in the scope of a single command (e.g. a single def) using open scoped Json in def .., but afaik there is no way to open within just a single term. The issue with true/false is due to the token table being global, and I recall Sebastian mention he wanted to fix that at some point. Note also that json% isn't an elaborator, it is a macro.

[Patrick Massot]

Example:

import ProofWidgets.Data.Json

open Lean

open scoped ProofWidgets.Json in
def foo : Json := Id.run do
  -- let x := true -- cannot uncomment this line
  return json% {"x" : 1}

[Patrick Massot]

Yes, I know I can open it before def. But here I want to open it before return.

[Mario Carneiro]

open ... in works within terms, but it is possible that it doesn't work here because you can't change the parser mid-command

[Mario Carneiro]

does the json parser work if these are declared as &"true" and &"false"? Are other identifiers legal in that position?

[Patrick Massot]

Oh,

def foo : Json := Id.run do
  -- let x := true
  open scoped ProofWidgets.Json in
  return  json% {"x" : 1}

fails but

def foo' : Json := Id.run do
  let x := true
  return open scoped ProofWidgets.Json in json% {"x" : 1}

works!

[Patrick Massot]

I'll be able to re-re-rewrite my code!

[Patrick Massot]

I need to find out how to write a macro that expands to open scoped ProofWidgets.Json in json%

[Patrick Massot]

but this doesn't really feel right.

[Mario Carneiro]

this seems like leakage of macro internals, you shouldn't need to open anything for json% to do the right thing

[Mario Carneiro]

except possibly the json% macro itself, if it is scoped

[Wojciech Nawrocki]

Mario Carneiro said:

except possibly the json% macro itself, if it is scoped

Yeah, it's a scoped syntax. The issue is precisely the true/false thing: we don't want importing the macro definition to mess up parsing everywhere.

[Patrick Massot]

Mario, you can take a look at https://github.com/EdAyers/ProofWidgets4/blob/main/ProofWidgets/Data/Json.lean, it doesn't depend on anything else.

[Wojciech Nawrocki]

Mario Carneiro said:

does the json parser work if these are declared as &"true" and &"false"? Are other identifiers legal in that position?

Are there any resources for how to use the & parser? Declaring them as non-keywords breaks matching in macro_rules:

declare_syntax_cat cat
syntax &"dogcow" : cat

macro_rules
  | `(cat| dogcow) => `(37) -- expected cat

[Patrick Massot]

import ProofWidgets.Data.Json

macro "Json%" x:jso : term => `(open scoped ProofWidgets.Json in json% $x)

def foo' : Json := Id.run do
  let x := true
  return Json% {"x" : 1}

doesn't work :sad: I'm out of hack ideas.

[Wojciech Nawrocki]

@Patrick Massot I think the issue is that to parse your Json% blah, the scoped syntaxes that make up blah need to already be open.

[Patrick Massot]

Yes, I understand, but I'm still out of ideas.

[Mario Carneiro]

this seems to work @Wojciech Nawrocki:

declare_syntax_cat cat (behavior := symbol)
syntax "dogcow" : cat

macro_rules
  | `(cat| dogcow) => `(37)

#check fun dogcow => dogcow

[Patrick Massot]

Maybe a stop gap would be to drop support of true and false and use $(true) and $(false).

[Mario Carneiro]

I'm not sure if this suffices for the json parser, but I would guess it does since true can only appear at a json object node

[Mario Carneiro]

I'm not sure why I'm getting strange reactions on that post

[Wojciech Nawrocki]

Mario Carneiro said:

I'm not sure why I'm getting strange reactions on that post

Mine was because the option is not documented on declare_syntax_cat and I had not seen it before. But one can get to its documentation by following the parser trail.

[James Gallicchio]

it's giving dark metamagic

[James Gallicchio]

(not opposed)

[Wojciech Nawrocki]

Okay, released new PW4 in which

open scoped ProofWidgets.Json in
def foo : Json := Id.run do
  let x := true
  return json% {"x" : 1}

should work thanks to Mario's metaprogramming investigations.

[Patrick Massot]

Great! Next question is: do we dare trying to bump PW4 in mathlib or will this break the cache?

[Mario Carneiro]

all bumps break the cache

[Patrick Massot]

By the way Mario, don't you want https://github.com/EdAyers/ProofWidgets4/blob/main/ProofWidgets/Data/Json.lean in Std anyway?

[Patrick Massot]

Mario Carneiro said:

all bumps break the cache

What should we do then?

[Mario Carneiro]

bump anyway

[Ruben Van de Velde]

Do you mean "invalidate" rather than "break"?

[Mario Carneiro]

I mean invalidate, not sure whether patrick does

[Mario Carneiro]

Patrick Massot said:

By the way Mario, don't you want https://github.com/EdAyers/ProofWidgets4/blob/main/ProofWidgets/Data/Json.lean in Std anyway?

PRs welcome

[Patrick Massot]

I'm referring the the week of debugging that followed my previous PW bump attempt. I opened #7258 anyway.

[Patrick Massot]

I opened std4#267. I hope @Wojciech Nawrocki and @Edward Ayers are ok. The only differences with the version at ProofWidgets4 are docstrings and tests.

[Mac Malone]

@Wojciech Nawrocki I am curious why jso_ident and jso_field are syntax categories rather than just syntax abbreviations. That is, the following should work

syntax jsoSubst := "$(" term ")"
syntax jsoIdent := ident <|> str <|> jsoSubst
syntax jsoField := jsoIdent ": " jso

[Mac Malone]

syntax categories are generally only used for recursive or extensible syntax kinds.

[Wojciech Nawrocki]

I'm afraid the answer is that I was sadly never able to understand the intricacies of Lean syntax extensions! I can confirm that after removing the two categories it still works.

However this does not fix the real issue. To remove the need for scoped, the task is to come up with a syntax extension which makes macro_rules work while also not breaking quotation patterns. Here is a minimal example:

import Lean
open Lean

-- Challenge: devise the syntax so that at least one of the `macro_rules`,
-- as well as the `#check` below succeed;
-- or explain why this is not possible.
declare_syntax_cat dog (behavior := symbol)
syntax "$(" term ")" : dog
syntax "dog% " dog : term

macro_rules
  | `(term| dog% $( $t:term )) => `(1337)

macro_rules
  | `(dog| $( $t:term )) => `(1337)

#check
  let a : Syntax := sorry
  if let `(calcStep| $(_) := $stx) := a then sorry else sorry

[Mac Malone]

@Wojciech Nawrocki I have two alternative suggestions:

• Just use parentheses without the $ (as they are otherwise not valid JSON).
• Use {{ ... }} like Moustache/Handlebars/GitHub actions (via atomic("{" noWs "{") / atomic("}" noWs "}") to avoid a new token).

The former is simpler that later is clearer for the user.

[Mac Malone]

I wonder if it would be a good idea to host some online (or even offline) workshops on some of the fine non-mathematical components of Lean 4 (and, in particular, the various aspects of metaprogramming).

[Wojciech Nawrocki]

I totally agree that a solution which does not clash with antiquotations is the pragmatic way to go. That said, I am interested in this puzzle because it seems intuitively wrong that adding parsers localized to a freshly defined category breaks the global syntax. This intuition might be incorrect, and in that case I would also be interested in learning why.

[Mac Malone]

@Wojciech Nawrocki The token trie is global. Every token reachable from command/term is in there. As json% makes jso reachable from term, its $( token breaks antiquotes.

[Wojciech Nawrocki]

Yep, you are right about that. Except that with antiquotations, because the token already exists, we can invent some hacks to make it work:

declare_syntax_cat dog
syntax "dog% " dog : term

macro_rules
  | `(term| dog% $stx) => do
    if stx.raw.getKind == `dog.pseudo.antiquot then
      return stx.raw[2][1]
    else
      Macro.throwUnsupported

/- 10 : Nat -/
#check dog% $(10)

#check
  let a : Syntax := sorry
  if let `(calcStep| $(_) := $stx) := a then sorry else sorry -- works

[Sebastian Ullrich]

Yes, this is in fact the reason I lifted the restriction of antiquotations only being allowed in quotations at some point. Ideally you should make use of functions isEscapedAntiquot etc. such that even `(dog% $$x) works (it should be a dog-level antiquotation, not a Syntax-level one)

[Sebastian Ullrich]

Actually that should work out of the box since it's the syntax quotation elaborator's job to strip off one $ here! You should only have to worry about that in your own quotation-like elaborator if other quotation-likes can be nested in it

[Wojciech Nawrocki]

Nice! The following seems to work as a fallback case handling antiquotations:

macro_rules
  | `(json% $stx)           =>
    if stx.raw.isAntiquot then
      let stx := ⟨stx.raw.getAntiquotTerm⟩
      `(Lean.toJson $stx)
    else
      Macro.throwUnsupported

...

def foo : Lean.Json := sorry
/- Lean.Json.mkObj [("abc", Lean.toJson foo), ("_def", Lean.toJson 10)] : Lean.Json -/
#check json% { abc: $foo, _def: $(10) }

[Mario Carneiro]

Mac Malone said:

I wonder if it would be a good idea to host some online (or even offline) workshops on some of the fine non-mathematical components of Lean 4 (and, in particular, the various aspects of metaprogramming).

This was actually the point of the ICERM 2022 after-party, it was a metaprogramming workshop to get people trained up to write missing tactics for mathlib4