What comes after macros?

Stream: lean4

[Marcus Rossel]

I'm struggling to understand how to expand custom syntax, when the syntactic transformation isn't super easy.
I'm trying to transform something like:

•••••••••▦▦•••••◎•••••••
•••••••••▦▦▦▦•••••••••••
•••••▦••••▦▦••••••••••••
•••••••▦••▦•••*•▦•••••••
••••╺━0•••▦•▦•••▦▦•••*••
•▦▦▦▦▦▦▦▦•••▦▦•••••••▦▦•
•▦▦▦▦▦▦▦▦▦▦▦▦▦▦▦▦▦▦▦▦▦▦•
•▦▦▦▦▦▦▦▦▦•▦▦▦▦▦▦▦▦▦▦▦••
••▦▦▦▦▦▦▦▦••▦▦▦▦▦▦▦▦▦▦••
∼∼∼∼∼∼∼∼∼∼∼∼∼∼∼∼∼∼∼∼∼∼∼∼

... into an instance of Game:

structure Game where
  map : Map
  snakes : List Snake

structure Map where
  goal  : Pos
  rocks : List Pos
  fruit : List Pos
  saws  : List Pos

structure Snake where
  head : Pos
  body : List Pos

structure Pos where
  x : Int
  y : Int

From what I've read on elaboration, I feel like it might play some role, but I don't know how or why.

[Gabriel Ebner]

You can also run Game.fromFields in the macro, and then quote the result of Game.fromFields (that is, the macro expands into {map := ..., snakes := ...} and not a call to Game.fromFields).

[Marcus Rossel]

Gabriel Ebner said:

You can also run Game.fromFields in the macro, and then quote the result of Game.fromFields (that is, the macro expands into [[air, ...], ...] and not a call to Game.fromFields).

How do I get a List (List Field) (to pass to Game.fromFields) inside the macro? Currently fields is an Array Syntax.

[Gabriel Ebner]

I don't see the whole code. From what I can tell you're producing the fields variable from rows and water; you can probably directly produce the List (List Field) instead.

[Marcus Rossel]

Gabriel Ebner said:

I don't see the whole code. From what I can tell you're producing the fields variable from rows and water; you can probably directly produce the List (List Field) instead.

Haha you're right :see_no_evil: Thanks!

[Marcus Rossel]

I am stuck on one step though. I have this transformation:

def fieldToTerm : Syntax → MacroM Field
  | `(map_field| •) => Field.air
  | `(map_field| ▦) => Field.rock
  | `(map_field| ✸) => Field.saw
  | `(map_field| ◎) => Field.goal
  | `(map_field| *) => Field.fruit
  ...
  | `(map_field| $n:numLit) => Field.snakeHead n -- This doesn't work because `n` isn't a `Nat`.
  | _ => Lean.Macro.throwError "Unknown map field."

And I'll need to turn n : Syntax into a Nat.

[Mario Carneiro]

The function Syntax.isNatLit? should work there

[Notification Bot]

Marcus Rossel has marked this topic as resolved.

[Notification Bot]

Marcus Rossel has marked this topic as unresolved.

[Marcus Rossel]

Gabriel Ebner said:

You can also run Game.fromFields in the macro, and then quote the result of Game.fromFields (that is, the macro expands into {map := ..., snakes := ...} and not a call to Game.fromFields).

I now have:

macro_rules
  | `($rows:map_row* $water:water_row) => do
    ...
    let g : Game ← Game.fromFields fields.data

How do I get a Syntax object from g though?

[Gabriel Ebner]

You need to implement a function Game → Syntax, this is the quote function from the Quote type class. At some point in the future this will be auto-derived, but for now you'll need to write it manually.

You can use Unhygienic.run `(....) to create syntax outside of the MacroM/TermElabM monads.