Lean4 lambda calculus DSL macro

Question

I would like to define a DSL for writing lambda terms in Lean using macros a la the arithmetic example. I want to support syntax for multiple arguments in the lambda, and left-associativity. Thus far, I have come up with the following code:

inductive Λ where
 | var : String → Λ
 | apl : Λ → Λ → Λ
 | abstr : String → Λ → Λ
declare_syntax_cat lcplus
syntax ident : lcplus
syntax lcplus lcplus+ : lcplus
syntax "(λ" ident+ "." lcplus ")" : lcplus
syntax "(" lcplus ")" : lcplus
syntax "<[" term "]>" : lcplus
syntax "`[λ+| " lcplus "]" : term
macro_rules
 | `(`[λ+| $x:ident]) => `(Λ.var $(Lean.quote (toString x.getId)))
 | `(`[λ+| $x:lcplus $xs:lcplus*]) => do
 let mut acc <- `(`[λ+| $x])
 for x' in xs do
 acc <- `(Λ.apl $acc `[λ+| $x'])
 return acc
 | `(`[λ+| (λ $xs:ident* . $body:lcplus)]) => do
 let mut acc <- `(`[λ+| $body])
 for x in xs.reverse do
 acc <- `(Λ.abstr $(Lean.quote (toString x.getId)) $acc)
 return acc
 --xs.foldrM (init := `(`[λ+| $body])) λ x acc =>
 -- `(Λ.abstr $(Lean.quote (toString x.getId)) $acc) -- Type mismatch $acc, is Syntax, expected TSyntax `term
 | `(`[λ+| ($x:lcplus)]) => `(`[λ+| $x])
 | `(`[λ+| <[$e:term]>]) => pure e
 
#check `[λ+| (λ x y. x) a b ]

The issue is that `[λ+| (λ x y. x) a b ] parses as

Λ.apl (Λ.abstr "x" (Λ.abstr y (Λ.var "x"))) (Λ.apl (Λ.var "a") (Λ.var "b"))

while I would want it to parse as

Λ.apl (Λ.apl (Λ.abstr "x" (Λ.abstr y (Λ.var "x"))) (Λ.var "a")) (Λ.var "b")

i.e. it seems to be right-associative.

I suspect the issue lies in the syntax declaration

syntax lcplus lcplus+ : lcplus

and not in the macro itself, as I suspect that lcplus+ parses the rest of the lambda terms as another application rather than an array of lambda terms. I don't really know how to get around this, as my knowledge of Lean syntax and macros, and Lean in general, isn't great, and my knowledge of parsers is very rusty.

On another note, I could not figure out how to use a fold rather than do notation, as that is essentially what we are doing.

I would be grateful if someone could help me.

Answer 1

I figured it out.

First off, since the parser is already recursively using this rule:

syntax lcplus lcplus+ : lcplus

there is no point in the extra +. After closer inspection of the aforementioned arithmetic example, I figured out I should change this rule to the following:

syntax:60 lcplus:60 lcplus:61 : lcplus

to make it left-associative by specifying precedence.

I guess the question why the fold did not work still stands though.