cade21 paper macro question

Stream: lean4

[Dan W.]

Hello, I'm reasonably new to lean (dabbled with lean 2 for a few months when it came out awhile back). I have a question on how to modify the boolean expression language example given in the recent CADE 21' lean 4 paper. Here is a link to the original code from that paper that I've been using as a reference: https://github.com/leanprover/lean4/blob/cade2021/doc/BoolExpr.lean

Basically, I want a Doc (document) datatype that just holds a List (or array -- if you that's more advisable) of another inductive datatype: Cmnd that can either be a No-op or some kind of constant (right now its restricted to be just a nullary boolean constant).

Anyways, I'm having trouble getting the Array Cmnd built up in the last macro_rules part. I've been trying to use a .map on mx, but am unclear on whether I want this to be $mx, etc. Further, mapping over the mx like so: mx.map (fun x => ``[Cmnd| x]) doesn't seem to work since x in the passed function has type Syntax (not the custom syntactic category: cmnd). This kind of confuses me since I said mx:cmnd (as opposed to mx:ident, etc.). No doubt I'm missing something here.

Here's a mwe (including the imports -- so it should just be able to be dropped into a .lean file).

import Std
open Std
open Lean

inductive BoolExpr where
  | var (name : String)
  | val (b : Bool)
  deriving Repr, BEq, DecidableEq

syntax "`[BExpr|" term "]" : term
macro_rules
 | `(`[BExpr| true])     => `(val true)
 | `(`[BExpr| false])    => `(val false)
 | `(`[BExpr| $x:ident]) => `(var $(quote x.getId.toString))

inductive Cmnd : Type
  | const (name : String) --(definiens : BoolExpr)
  | noop : Cmnd
declare_syntax_cat cmnd

inductive Doc where
  | doc (Δ : Array Cmnd)

-- will eventually add to this and replace the ..
syntax "Def." ident "::" "Boolean" "≜" ".." : cmnd
syntax "Noop."                              : cmnd

syntax "`[Cmnd|" cmnd "]" : term -- gives back the usual lean term
macro_rules
  | `(`[Cmnd| Def. $x:ident :: Boolean ≜ ..]) => `(Cmnd.const $(quote x.getId.toString))
  | `(`[Cmnd| Noop.]) => `(Cmnd.noop)

syntax "`[MyScript|" cmnd* "]" : term
macro_rules
  | `(`[MyScript| $[$mx:cmnd]* ]) =>
    `(Doc.doc (#[mx.map (fun x => `[BExpr| x])])) -- <-- ??

def ex1 := `[MyScript|
  Noop.
]

def ex2 := `[MyScript|
  Noop.
]

def ex3 := `[MyScript| ]

#print ex1

[Henrik Böving]

If you are getting into macro based meta programming you can check out the WIP documentation we are writing for it right now, specifically the syntax and macro chapters in your case, they should be helpful in understanding the general system: github.com/arthurpaulino/lean4-metaprogramming-book/

To answer your questions:

1. Array is mostly used for performance, as long as you want proofs Lists will suffice
2. The $mx vs regular mx is covered in detail in the book, i will not reproduce it here
3. regarding your confusion as to Syntax, every syntax including user defined one will have the type Syntax if you match on it this way, what you affect by declaring a concrete syntax category or parser is the SyntaxNodeKind that the syntax you are matching on will have.

[Henrik Böving]

Also if you find anything confusing or not nicely understandable in those chapters please do tell us, we are eager to improve the explanations.

[Dan W.]

Thanks! This book looks like exactly what I was looking for. I'll post here again if I can't get the example above working or if I need some clarification on a section of the book.