mutually recursive syntax

Stream: lean4

[Andrés Goens]

Hi! I'm trying to define mutually recursive syntax and that seems to confuse the syntax extension algorithm:

declare_syntax_cat foo
declare_syntax_cat bar
syntax "fooval" : foo
--syntax bar : foo
syntax foo : bar
syntax "[bar|" bar "]": term
syntax "[foo|" foo "]": term

macro_rules
 | `([foo| fooval ]) => `(42)
 | `([bar| $x:foo]) => `([foo| $x])
-- | `([foo| $x:bar ]) => `([bar| $x])

#eval [bar| fooval ]

If I uncomment the first line here (syntax bar: foo), Lean gets stuck (emacs just hangs evaluating it, vscode says potentially a stack overflow), probably because it gets caught up in the recursion that foo : bar and bar : foo. In theory, with the line commented below in the macro rules, this should work well, as the delaborator would not get caught in an infinite loop if the mutual recursion is the last call. I guess if there's some syntax error then it could fall through the infinite loop...

Is there away around this? E.g. defining some custom parser combinator?

[Sébastien Michelland]

If you have syntax foo: bar and syntax bar: foo, then you really only have a single syntax category with two different names. Do you not have any guards around the sub-foo in bar and the sub-bar in foo in your use case?

[Andrés Goens]

oh, that's because I reduced my MWE, in the real example I really do have two distinct syntax categories with different syntax. I actually don't have any guards there, nope. To be concrete, I was trying to define CTL* syntax and there you don't really have guards either, would be pretty unnatural to have them

[Sébastien Michelland]

I can see in that piece of grammar that you have ϕ ::= Φ, but where do you have the other one? I can only see Φ ::= Aϕ | Eϕ, which has leading symbols A and E that would prevent the left recursion (acting as what I called guards).

[Henrik Böving]

As Sebastien said if you write this grammar down in Lean:

import Lean

mutual

inductive State where
  | bot : State
  | top : State
  | var : Lean.Name → State
  | neg : State → State
  | and : State → State → State
  | or : State → State → State
  | imp : State → State → State
  | iff : State → State → State
  | aPath : Path → State
  | ePath : Path → State

inductive Path where
  | state : State → Path
  | neg : Path → Path
  | and : Path → Path → Path
  | or : Path → Path → Path
  | imp : Path → Path → Path
  | iff : Path → Path → Path
  | x : Path → Path
  | f : Path → Path
  | g : Path → Path
  | u : Path → Path → Path
  | r : Path → Path → Path

end

declare_syntax_cat state
declare_syntax_cat path

syntax "⊥" : state
syntax "⊤" : state
syntax ident : state
syntax "¬" state : state
syntax state " ∧ " state : state
syntax state " ∨ " state : state
syntax state " → " state : state
syntax state " ↔ " state : state
syntax "A " path : state
syntax "E " path : state

syntax state : path
syntax "¬" path : path
syntax path " ∧ " path : path
syntax path " ∨ " path : path
syntax path " → " path : path
syntax path " ↔ " path : path
syntax "X " path : path
syntax "F " path : path
syntax "G " path : path
syntax path " U " path : path
syntax path " R " path : path

syntax "[state|" state "]" : term
syntax "[path|" path "]" : term

macro_rules
  | `([state| ⊥]) => `(State.bot)
  | `([state| ⊤]) => `(State.top)
  | `([state| $x:ident]) => `(State.var $x:ident)
  | `([state| ¬ $x:state]) => `(State.neg [state| $x:state])
  | `([state| $l:state ∧ $r:state]) => `(State.and [state| $l] [state| $r])
  | `([state| $l:state ∨ $r:state]) => `(State.or [state| $l] [state| $r])
  | `([state| $l:state → $r:state]) => `(State.imp [state| $l] [state| $r])
  | `([state| $l:state ↔ $r:state]) => `(State.iff [state| $l] [state| $r])
  | `([state| A $x:path]) => `(State.aPath [path| $x:path])
  | `([state| E $x:path]) => `(State.ePath [path| $x:path])
  | `([path| ¬ $x:path]) => `(State.neg [state| $x:state])
  | `([path| $l:path ∧ $r:path]) => `(Path.and [path| $l] [path| $r])
  | `([path| $l:path ∨ $r:path]) => `(Path.or [path| $l] [path| $r])
  | `([path| $l:path → $r:path]) => `(Path.imp [path| $l] [path| $r])
  | `([path| $l:path ↔ $r:path]) => `(Path.iff [path| $l] [path| $r])
  | `([path| X $x:path]) => `(Path.x [path| $x:path])
  | `([path| F $x:path]) => `(Path.f [path| $x:path])
  | `([path| $l:path U $r:path]) => `(Path.u [path| $l:path] [path| $r:path])
  | `([path| $l:path R $r:path]) => `(Path.r [path| $l:path] [path| $r:path])

I also can't quite see how the mechanism you demonstrated above would occur here.

[Andrés Goens]

Interesting, I was using the definition from somewhere else that did have that extra one, thanks for pointing that out! I'd still be curious wether it's possible (even if it won't matter for my concrete example)

[Andrés Goens]

(edited: I realized I just read it wrong)

[Mac]

Andrés Goens said:

Because it gets caught up in the recursion that foo : bar and bar : foo.

Yes, the parser looping indefinitely seems like the expected behavior here. How were you envisioning this working? :thinking:

[Andrés Goens]

Mac said:

Yes, the parser looping indefinitely seems like the expected behavior here. How were you envisioning this working? :thinking:

I didn't expect it to work 'out of the box', but I imagined I could have extended the parser to explicitly handle that case :thinking:

[Mac]

Andrés Goens said:

I imagined I could have extended the parser to explicitly handle that case

Sorry, that was kind of my question. How were you hoping to resolve the loop? That is, what extension did you want to write to solve it? I am having a hard time imagining what such a solution would look like.