Matching if Statements of Another Syntax

Stream: new members

[Jack Hackshaw]

I'm trying to embed a language in Lean. It seems like there is a conflict between lean's syntax and my language. The if syntax for the language looks like this:

if x > 0 {
    return 1;
} else {
    return 0;
}

I've defined it like this:

declare_syntax_cat if_else
syntax "if" term "{" doSeq "}" "else" "{" doSeq "}" : if_else

And I try to translate it to Lean with the following macro rule:

macro_rules
 | `(if_else| if $cond {$a}{$if_body} else {$else_body}) =>
   `(if $cond then do $if_body else do $else_body)

Notice the {$a}. If I don't include it I get an error.a has the type TSyntax Lean.Parser.Term.structInstField`

Regardless, if I write an if statement in my language Lean complains about a missing then so obviously, the macro rule is not being applied.

[Jakub Nowak]

It seems like you're trying to parse your if in the context where lean expects term. You declared your if to belong to if_else category, which is not term.

[Jakub Nowak]

You might be interested in reading https://leanprover-community.github.io/lean4-metaprogramming-book/main/08_dsls.html.

[Kyle Miller]

A significant issue with this syntax is that terms can be followed by curly braces; for example f { return 2 } is valid as a term, because return 2 is a term and { ... } is a term (singleton set). It goes for the longest valid parse.

What MrQubo points out should not be a problem for the macro rule, just as long as you are aware this is in the if_else category, and that you might need to make an if_else macro expander (macros are not expanded automatically, each category writes its own hook for that), and that you'll definitely need to use the if_else category in some syntax available to terms/doElems/etc.

It's possible set forbidden tokens to get this to parse, though withForbidden doesn't appear to be available in syntax, only lower-level parsers. Another option might be to adjust the precedence, but it's not possible to disambiguate x > 0 { return 1 } that way. Easiest is to change your DSL to use C syntax, if (x > 0) { ... } else { ... }. Harder is to make your own term category from scratch with exactly the term syntaxes you want.

[Jack Hackshaw]

Unfortunately, changing the DSL is not an option.

I am not wedded to using syntax, if I can get the desired result with a lower level parser that allows withForbidden then that is an option. Otherwise I guess I will have to do it the hard way and implement my own term category.

Do you have a recommendation on where I might look to get started?