syntax/macros with iterated definitions

Stream: lean4

[Paul Chisholm]

I am trying to define some notation that is like the if-fi construct in Dijkstra's Guarded Command Language. I started with:

namespace syntax_version

scoped syntax " if " (term " ⟹ " term " ‖ ")+ " ⟹ " term " fi " : term

macro_rules
  | `(if $c₁ ⟹ $e₁ ‖ ⟹ $e₂ fi) =>
      `(ite $c₁ $e₁ $e₂)
  | `(if $c₁ ⟹ $e₁ ‖ $c₂ ⟹ $e₂ ‖ ⟹ $e₃ fi) =>
      `(ite $c₁ $e₁ (ite $c₂ $e₂ $e₃))

def select (n : Nat) : String :=
    if n == 0 ⟹ "zero"
     ‖ n == 1 ⟹ "one"
--     ‖ n == 2 ⟹ "two"
     ‖        ⟹ "> 2"
    fi

end syntax_version

which is fine as far as it goes but inadequate because you can't keep adding cases each time you need an extra branch (such as to handle the n == 2 case in the example). I can't see any way to handle the iterated syntax (+).

Syntax categories seem to be a step in the right direction so it became:

namespace syntax_category_version

declare_syntax_cat clause
declare_syntax_cat catchall

scoped syntax term " ⟹ " term  " ‖ " : clause
scoped syntax " ⟹ " term : catchall
scoped syntax (name := iffi) " if " clause+ catchall " fi " : term

macro_rules
  | ?

end syntax_category_version

I have tried to mimic what I see in the notation section of the manual but haven't been able to come up with the correct pattern. What do I need to do here to match the iterated clauses and translate to the corresponding ite calls?

[Mario Carneiro]

you use $(e)* to match an expression produced by stx+

[Paul Chisholm]

I had tried something along those lines. This sort of thing (ignoring the RHS for the moment):

macro_rules
  | `(catchall| ⟹ $e) => `(1)
  | `(clause| c ⟹ e ‖) => `(1)
  | `(iffi| if $cl $(cls)* $ca fi) => `(1)

I have tried various combinations but I always end up with the fi underlined and the error expected catchall.

[Paul Chisholm]

Actually, I missed a couple of $ above (in the clause case) which then has an error under the arrow of that case expected ')'.

[Sebastian Ullrich]

Using your original syntax:

scoped syntax " if " (term " ⟹ " term " ‖ ")+ " ⟹ " term " fi " : term

macro_rules
  | `(if $c₁ ⟹ $e₁ ‖ ⟹ $e₂ fi) =>
    `(ite $c₁ $e₁ $e₂)
  | `(if $c₁ ⟹ $e₁ ‖ $[$cs₁ ⟹ $es₁ ‖]* ⟹ $e₂ fi) =>
    `(ite $c₁ $e₁ (if $[$cs₁ ⟹ $es₁ ‖]* ⟹ $e₂ fi))

[Sebastian Ullrich]

Regarding your second approach, you need to resolve ambiguities around antiquotations manually: in clause| $c ..., c will default to being clause, which means you should use $c:term instead

[Paul Chisholm]

Thanks very much for the responses.

It is really nice the way the macro rules are just a kind of recursive definition. I just didn't see that before.

[Marcus Rossel]

@Paul Chisholm Are you planning on implementing some model checking related stuff?

[Paul Chisholm]

@Marcus Rossel I was really just experimenting with notation. The notation expands to the nested ites. What do you have in mind when you say model checking in this context.

[Marcus Rossel]

@Paul Chisholm I mean checking satisfiability of LTL and CTL formulas over a labeled transition system (a la Principles of Model Checking by Baier and Katoen).

[Paul Chisholm]

@Marcus Rossel Ok, I haven't come across that previously, though from a quick scan looks very interesting. However, I have no time to investigate further at this stage. (Lean is a personal interest activity for me away from work.)