sending elaboration error to custom syntax category

Stream: lean4

[Tomas Skrivan]

I have a custom syntax category cexpr and I have a macro that turns it into syntax of type term. How can I correctly propagate elaboration errors back to cexpr?

import Lean

open Lean

declare_syntax_cat cexpr

syntax ident : cexpr
syntax cexpr "+" cexpr : cexpr
syntax "(" cexpr ")" : cexpr

syntax (name:=cexprStx) "cexpr% " cexpr : term

macro_rules (kind:=cexprStx)
| `(cexpr% $id:ident) => `(term| $id:ident)
| `(cexpr% $x:cexpr + $y:cexpr) => `(term| (cexpr% $x:cexpr) + (cexpr% $y:cexpr))
| `(cexpr% ( $x:cexpr )) => `(term| (cexpr% $x:cexpr))

variable (a b c : Float) (s : String)

#check a + (b + s)
#check cexpr% a + (b + s)

Is there a way to make the red squiggle to show under (b + s) in cexpr% a + (b + s) ?
image.png

[Aaron Liu]

while it's certainly possible (it's done for term after all) I can't think of any easy way to do it

[Aaron Liu]

oh I just thought of an easy way to do it (if it works)

[Aaron Liu]

oh it totally didn't work

[Tomas Skrivan]

Ahh what a shame :cry:

[Aaron Liu]

final product (failure)

import Mathlib.Util.WhatsNew
import Lean

open Lean

declare_syntax_cat cexpr

syntax ident : cexpr
syntax cexpr "+" hygieneInfo cexpr : cexpr
syntax "(" hygieneInfo cexpr ")" : cexpr

syntax (name:=cexprStx) "cexpr% " cexpr : term

whatsnew in
macro_rules (kind:=cexprStx)
| `(cexpr% $id:ident) => `(term| $id:ident)
| `(cexpr%%$cexpr $x:cexpr +%$add $hi:hygieneInfo $y:cexpr) => `(term| (%$add $hi:hygieneInfo cexpr%%$cexpr $x:cexpr)%$add +%$add (%$add $hi:hygieneInfo cexpr%%$cexpr $y:cexpr)%$add)
| `(cexpr%%$cexpr (%$lparen $hi:hygieneInfo $x:cexpr )%$rparen) => `(term| (%$lparen $hi:hygieneInfo cexpr%%$cexpr $x:cexpr)%$rparen)

variable (a b c : Float) (s : String)

#check a + (b + s)
#info_trees in
#check cexpr% a + (b + s)

[Aaron Liu]

all that syntax referencing didn't make a difference since I guess it just goes back to the place it entered term-land

[Aaron Liu]

oh maybe that's why "unsolved goals" highlights the entire tactic block

[Tomas Skrivan]

Very interesting attempt! Unfortunately I have no idea if it can be salvaged or not.

[Thomas Murrills]

I think all you need to do is attach the position info of the component syntax to the constructed syntax (via e.g. withRef) :)

import Lean

open Lean

declare_syntax_cat cexpr

syntax ident : cexpr
syntax cexpr "+" cexpr : cexpr
syntax "(" cexpr ")" : cexpr

syntax (name:=cexprStx) "cexpr% " cexpr : term

macro_rules (kind:=cexprStx)
| `(cexpr% $id:ident) => withRef id `(term| $id:ident)
| `(cexpr% $x:cexpr + $y:cexpr) => do
  let x ← withRef x `(term| (cexpr% $x:cexpr))
  let y ← withRef y `(term| (cexpr% $y:cexpr))
  `(term| $x + $y)
| `(cexpr% ( $x:cexpr )) => withRef x `(term| (cexpr% $x:cexpr))

variable (a b c : Float) (s : String)

#check a + (b + s)
#check cexpr% a + (b + s)

image.png

I haven't thought very hard about whether this could produce any unexpected behavior sometimes, though (or if each of these cases is exactly correct, especially the last). :thinking:

(The hygiene management might be interesting for other reasons...! :eyes:)

[Thomas Murrills]

To be slightly more careful (but still possibly not sufficiently careful!), I might rewrite the macro_rules above slightly to

code

macro_rules (kind := cexprStx)
| `(cexpr% $c:cexpr) => withRef c do
  match c with
  | `(cexpr| $id:ident) => withRef id `(term| $id:ident)
  | `(cexpr| $x:cexpr + $y:cexpr) => do
    let x ← withRef x `(term| cexpr% $x:cexpr)
    let y ← withRef y `(term| cexpr% $y:cexpr)
    `(term| $x + $y)
  | `(cexpr| ( $x:cexpr )) => withRef x `(term| cexpr% $x:cexpr)
  | _ => Macro.throwUnsupported

(the difference being mainly the position info of c appearing on the final + term)

[Tomas Skrivan]

Thanks, this works exactly as I want to. I need to test it also when I convert to doElem but I don't see a reason why it wouldn't work.