Definition Macro?

Stream: lean4

[Joseph O]

How could I make a macro in Lean such that

(define (add [x Nat] [y Nat]) (x + y))

expands into

def add (x : Nat) (y : Nat) := x + y

[Arthur Paulino]

syntax binder := "[" ident term "]"
syntax "(" "define" "(" ident binder* ")" term " : " term ")" : command

macro_rules
  | `((define ($f:ident [$nm:ident $ty:term]) $v:term : $ty':term)) =>
    `(def $f:ident : $ty → $ty' := fun $nm => $v:term)
  | `((define ($f:ident [$nm:ident $ty:term] $bs:binder*) $v:term : $ty':term)) =>
    `((define ($f:ident $bs:binder*) fun $nm => $v:term : $ty → $ty':term))

(define (add [x Nat] [y Nat]) x : Nat)

#eval add 3 5 -- 5

[Arthur Paulino]

Here's a fun idea:

syntax binder := "[" ident term "]"
syntax "(" "define" "(" "[" ident term "]" binder* ")" term ")" : command

macro_rules
  | `((define ([$f:ident $ty':term] [$nm:ident $ty:term]) $v:term)) =>
    `(def $f:ident : $ty:term → $ty':term := fun $nm:ident => $v:term)
  | `((define ([$f:ident $ty':term] [$nm:ident $ty:term] $bs:binder*) $v:term)) =>
    `((define ([$f:ident $ty:term → $ty':term] $bs:binder*) fun $nm => $v:term))

(define ([add Nat] [x Nat] [y Nat]) x)

#eval add 3 5 -- 5

[Joseph O]

Thanks!

[Arthur Paulino]

There's something wrong with my code tho

[Arthur Paulino]

(define ([add Nat] [x Nat] [bla Int]) x)

#eval add 3 5 -- 5

I would expect that to eval to 3, but it's being evaluated to 5. Maybe someone else might be able to help you

[Joseph O]

@Arthur Paulino I think its because the arguments are reversed

[Notification Bot]

Joseph O has marked this topic as unresolved.

[Joseph O]

Hm can someone explain this weird behavior?
image.png
image.png

[Arthur Paulino]

I can't understand what's wrong with those screenshots

[Joseph O]

For more context, here is test3

def test3 : List Nat :=
  let x := [1, 2], y := [3, 4] in x ++ y

[Arthur Paulino]

I believe you posted on the wrong thread

[Joseph O]

Arthur Paulino said:

I believe you posted on the wrong thread

I don't think so, because this has something to do with the definition macro

[Joseph O]

As when it is uncommented (the add function), it breaks test3

[Arthur Paulino]

#mwe please

[Joseph O]

Arthur Paulino said:

#mwe please

syntax binder := ident " := " term
syntax "let" binder,+ " in " term : term

macro_rules
  | `(let $name:ident := $v:term in $t:term) => `(let $name := $v; $t)
  | `(let $name:ident := $v:term, $bs:binder,* in $t:term) =>
    `(let $name := $v; let $bs:binder,* in $t:term)

syntax binder := "[" ident term "]"
syntax "(" "define" "(" binder+ ")" term ")" : command

macro_rules
  | `((define ([$f:ident $ty':term] [$nm:ident $ty:term]) $v:term)) =>
    `(def $f:ident : $ty:term → $ty':term := fun $nm:ident => $v:term)
  | `((define ([$f:ident $ty':term] [$nm:ident $ty:term] $bs:binder*) $v:term)) =>
    `((define ([$f:ident $ty:term → $ty':term] $bs:binder*) fun $nm => $v:term))

def test3 : List Nat :=
  let x := [1, 2], y := [3, 4] in x ++ y

#eval test3 -- [1, 2, 3, 4]

-- try commenting and uncommenting this line, and see what happens to the eval
(define ([add Nat] [x Nat] [y Nat]) x + y)

[Arthur Paulino]

There's a conflict with the declaration of binder

[Joseph O]

Arthur Paulino said:

There's a conflict with the declaration of binder

Oh I see

[Joseph O]

I renamed them and I still get the same error

[Raghuram]

Joseph O said:

Hm can someone explain this weird behavior?
image.png
image.png

I got similar errors. I think Lean is interpreting (define ...) as a term to which test3 is applied. See if the error goes away if you put section end between the #eval and (define ...).
As for how to make (define ...) recognised as a separate command, I don't know.

[Raghuram]

Wait; are you not getting any errors on the (define ...) line when it's uncommented? That's different from what I got.

[Arthur Paulino]

Apparently the parens from (define ⋯ is causing the confusion. This works:

syntax binder := ident " := " term
syntax "let " binder,+ " in " term : term

macro_rules
  | `(let $name:ident := $v:term in $t:term) => `(let $name := $v; $t)
  | `(let $name:ident := $v:term, $bs:binder,* in $t:term) =>
    `(let $name := $v; let $bs:binder,* in $t:term)

syntax binder' := "[" ident term "]"
syntax "⦃" "define" "(" binder'+ ")" term "⦄" : command

macro_rules
  | `(⦃define ([$f:ident $ty':term] [$nm:ident $ty:term]) $v:term⦄) =>
    `(def $f:ident : $ty:term → $ty':term := fun $nm:ident => $v:term)
  | `(⦃define ([$f:ident $ty':term] [$nm:ident $ty:term] $bs:binder'*) $v:term⦄) =>
    `(⦃define ([$f:ident $ty:term → $ty':term] $bs:binder'*) fun $nm => $v:term⦄)

def test3 : List Nat :=
  let x := [1, 2], y := [3, 4] in x ++ y

#eval test3 -- [1, 2, 3, 4] works

⦃define ([add Nat] [x Nat] [y Nat]) x + y⦄ -- works