using indentation to resolve syntactic ambiguity

Stream: lean4

[Simon Hudon]

I'm building a DSL for writing context free grammars. I have the following syntactic rule and an example:

declare_syntax_cat rules
declare_syntax_cat rule
declare_syntax_cat symbol
syntax (ident <|> strLit) : symbol
syntax ident " ::= " (colGt symbol)* : rule
syntax rule* : rules
syntax(name := grammarCmd) "grammar " ident rules "end " ident : command

grammar foo

  foo ::= "(" foo ")"
  star ::= "." foo
  --   ^
  -- expected 'end'

end foo
-- invalid 'end', insufficient scopes

Clearly, the fact that I can have an identifier on either side of " ::= " makes this grammar ambiguous so I added colGt so that if I have a new line in the middle of a production rule, I have to indent it in order for it to be recognized as the continuation of the same rule. It doesn't seem to work that way. I also tried using notFollowedBy(" ::= ") after ident on the rhs of the production rule and that also doesn't work. How can I resolve this ambiguity?

[Leonardo de Moura]

@Simon Hudon colGt is the way to go, but you need to use withPosition to specify the column colGt is going to compare.

declare_syntax_cat rules
declare_syntax_cat rule
declare_syntax_cat symbol
syntax (ident <|> str) : symbol
syntax ident withPosition(" ::= " (colGt symbol)*) : rule
syntax rule* : rules
syntax(name := grammarCmd) "grammar " ident rules "end " ident : command

macro_rules
  | `(grammar $id1:ident $rules:rules end $id2:ident) => `(#print "hello")


grammar foo
  foo ::= "(" foo ")"
  star ::= "." foo

end foo

[Simon Hudon]

Ah! Nice! Thank you

[Arthur Paulino]

What does "colGt" mean? I keep reading "column greater than" in my mind but I'm not sure that makes sense

[Simon Hudon]

Leo just gave me the second part of this puzzle. withPosition marks a relative position and colGt is a match only if it appears at a column greater that the latest position recorded by withPosition