Parser descriptor and orelse with two symbols

Stream: lean4

[Tomas Skrivan]

I want to define a macro that allows me to write

function_properties <function>
  linear <proof of linearity>
  smooth <proof of smoothness>

that then defines corresponding instances for each property.

In my attempt at such a macro, writing:

function_properties <function>
  linear <proof of linearity>

generates statement for smooth instead of for linear

Here is the code I tried:

class IsSmooth  (f : α → β) : Prop
class IsLin  (f : α → β) : Prop

syntax funProp := ("smooth" term) <|> ("linear" term)

syntax "function_properties " term funProp* : command

macro_rules
  | `(function_properties $f smooth $proof) =>
      dbg_trace "making smooth"
      `(instance function_is_smooth : IsSmooth $f := $proof)
  | `(function_properties $f linear $proof) =>
      dbg_trace "making linear"
      `(instance function_is_linear : IsLin $f := $proof)
  | `(function_properties $f $prop:funProp $props:funProp*) =>
      `(function_properties $f $prop
        function_properties $f $props*)

function_properties (@id Float)
  linear ⟨⟩

function_properties (@id Float)
  smooth ⟨⟩

example : IsSmooth (@id Float) := by infer_instance
example : IsLin (@id Float) := by infer_instance

And defining two properties at the same time fails completely

function_properties (@id Float)
  linear ⟨⟩
  smooth ⟨⟩

gives an error elaboration function for 'commandFunction_properties__' has not been implemented

[Tomas Skrivan]

Ughh changing the definition of the parser descriptor to

syntax smoothProp := "smooth" term
syntax linearProp := "linear" term
syntax funProp := smoothProp <|> linearProp

makes function_properties (@id Float) linear ⟨⟩ correctly define function_is_linear instance. Why is that?

Defining both properties at the same time still fails though.

[Arthur Paulino]

I'm not on my PC, but have you seen a definition of a function of type Macro? It can be useful to debug the syntax term that's being created. I believe that macro_rules is syntax sugar for creating such function

[Tomas Skrivan]

There is bunch of stuff like that in NotationExtra.lean I should look into it.