Conditional Syntax

Stream: lean4

[Marcus Rossel]

How does one conditionally include/exclude parts in a quotation?
For example, given the following type:

inductive T | a | b | c

I want to write a macro to_option that takes a list t1, t2, ... of elements of T and generates the following function:

example : T → Option T
  | t1 => some t1
  | t2 => some t2
  ...
  | _ => none

Now the | _ => none clause only needs to be present if the given ts don't cover all cases.
For the purposes of this example, let's say we magically know whether this is the case (via needsNone).
(Also let's assume that we only get valid ts and no duplicates).
Then I'd write the macro as:

macro "to_option" cases:ident* : command => do
  let cases' := cases
  let needsNone := sorry
  `(
    example : T → Option T
      $[| $cases => some $cases']*
      | _ => none  -- ?
  )

How can I conditionally include the none clause here?

[Andrés Goens]

what's wrong with using an if? like

  if needsNone then
  `(
    example : T → Option T
      $[| $cases => some $cases']*
      | _ => none  -- ?
  )
  else
  `(
    example : T → Option T
      $[| $cases => some $cases']*
  )

[Marcus Rossel]

@Andrés Goens I've considered that option, but would just like to avoid the duplication (if easily possible).

[Mario Carneiro]

you can conditionally push to the array of arms before interpolating them in the syntax quotation

[Marcus Rossel]

(deleted)

[Mario Carneiro]

do you have a MWE?

[Mario Carneiro]

I would presume the answer to your question is cases.push (<- `(_))

[Marcus Rossel]

Mario Carneiro said:

do you have a MWE?

Sorry, I think I got it working now. Thanks!

[Marcus Rossel]

Follow-up for future readers:
The pattern I tend to use for conditional syntax now is:

macro "test" x:ident? : command => do
  let optionalSyntaxPart := match x with | none => #[] | some y => #[y]
  `(def mightNeedAParam := test $[ $optionalSyntaxPart ]*)

If optionalSyntaxPart is empty, the $[ $optionalSyntaxPart ]* seems to just disappear.
Feels kind of gross, but ¯\_(ツ)_/¯

[Jannis Limperg]

Why not $[$x]??

[Marcus Rossel]

Jannis Limperg said:

Why not $[$x]??

:scream: I didn't know that was a thing.