Can we write EBNF for djot?

[shi-yan]

I have a n00b question that if we can write EBNF for djot.

I want to use djot as the file format for my notebook app. But I need to extend djot's syntax to support more features. I looked at some of the djot implementations, they are too obscured to modify. I hence wanted to write one from scratch.

I'm not experienced in parsing. Previously I have used some parser generators briefly. I understand one design goal of djot is making parsing easier, I'm wondering if we can write EBNF for djot? (if so I will consider using tree-sitter to create a parser)

thanks,

[matklad]

Practically, my gut feeling is that a grammar won’t be very useful for djot (or in general for light markup languages). The structure is much more shallow (few distinct syntactic constructs), any input should have a parse tree, and there are a bunch of 2D rules (indentation, block quotes). So I’d probably recommend doing what djot.JS implementation does (parse blocks using sort-of-recusive descent maintaining a stack of blocks, witching each block parse inlines maintaining a map of potential openners).

Theoretically, I think djot isn’t LL(k) (because of attributes and rules for emphasis), but it might be LR or PEG.

But I need to extend djot's syntax to support more features

Could you tell which features exactly do you need? One big idea of djot is that you shouldn’t need to extend its syntax, as div, spans, and attributes should be enough to express any custom functionality within djot’s syntax.

[bpj]

I don’t know how relevant it is but in lpeg-re you can match such a construct by constraining the match for a character/byte between the delimiters with a negative lookahead for the closing delimiter before the pattern to match that character/byte. It may be that this is specific to lpeg-re/lpeg (although it alao works in regex dialects which support negative lookahead and quantified groups). This is what it looks like in lpeg-re:

match_str_pat = re.compile(
  [==[ -- start-re
    input <- {| ( plain / verb )* !. |}
    plain <- { [^`]+ }
    verb <- {|
      -- nam3d capture for opening delimitwr
      {:verb_del: '`'+ :} -- opening delimiter
      %s* -- optional whitespace
      {:verb: {~
        -- one or more bytes which are
        -- not at the start of the closing delimiter
        (
          -- negative lookahead for closing delimiter
          -- =NAME matches what {:NAME: ... :} matched
          !( %s* =verb_del )
          -- a single byte
          .
        )+ -- repeated one or more times
      ~} :}
      -- the closing delimiter
      %s* =verb_del
    |}
  ]==]
)

The construct is a bit slow because the engine has to make two matching attempt for every byte it advances within the delimiters but at least it makes variable length delimiters possible.

If something like this is possible in more regular PEG engines it will solve the problem.

In the above example I only matched non-delimited and delimited portions to demonstrate how it works. Of course you can contrast it with most anything if you want to!

[xxxserxxx]

That's one thing I noticed: there was a tendency to "drop into a programming language" when dealing with ambiguity. Which may be all you can do. My desire for determinism and a PL-decoupled specification is resisting what appears to be an inevitable conclusion.

[dereuromark]

Concretely EBNF? I am fairly certain it is possible.
I did it for carve which is basically Djot merged with Markdown, so a bit more rules and complex.

So yeah, doable for sure. And recommended to make it in general a bit more "serious" I would say.
Probably also makes it more machine readable, the rules.

[jgm]

Well, what you have for Carve is a formal-looking spec that actually relies on a lot of English prose in comments. That is not at all the same as a machine-interpretable formal grammar.

[dereuromark]

OK, maybe a bit overstated as a whole for this early draft.
At that point it was a formal EBNF skeleton sitting on top of a normative prose spec. My thinking was that if you strip the normative prose, the remaining productions give you a basic EBNF for the core elements - untested and unverified at the time. You could not feed the file to tree-sitter or a parser generator and get a working parser out of it; the context-free surface transcribes, but indentation, the 2D block structure, fence-length counting, emphasis precedence and reference resolution all live outside what plain EBNF can say.

(As an aside: once you count LLMs as consumers, even the prose becomes machine-interpretable in a looser sense :) Not a formal argument, but in practice it may soon be good enough for implementations at a high accuracy.)

That said, having the EBNF scaffold at all was worth it for Carve. It forced the context-free structure to be explicit and consistent, it made the prose constraints easy to locate (each production points at the specific rule that governs it), and it caught real ambiguities during design. I would recommend that much to any markup-language author regardless of where one lands on the formality question.

Your comment did inspire me to go deeper, and the result is further than I expected to get:

• The spec is now layered, each layer in a declared formalism: EBNF for the skeleton, guard predicates for the counting rules, a line automaton for the 2D parts, and a two-pass over declared symbol tables for the references.
• Each layer exists as a directly runnable artifact: an Ohm/PEG grammar for the inline layer, plus two small modules that are 1:1 transcriptions of the automaton and the resolution rules. For that verification I had to create a .ohm file, since EBNF is not directly executable as is.
• A CI gate renders the entire conformance corpus through this executable spec and requires byte-identical HTML with the reference implementation - currently 388/388 pairs, plus a differential run over generated off-corpus inputs with zero divergences.

Two honest limits, which I think are the real answer to the question this thread started with:

• The written grammar file still carries prose for some of the operational rules; the claim is not "zero English in the spec text" but "every pinned behavior also exists in an executable formalism, and CI proves the two agree".
• At that point the executable spec IS code - effectively another reference implementation. That is what machine-interpretable means at the limit. The difference from an ordinary implementation is traceability: each module transcribes one declared formal layer, and the byte-parity gate keeps it honest. The 2D and context-sensitive parts of any light markup language resist a single-grammar formalization, exactly as noted earlier in this thread.

In case it is useful as a comparison point for djot, here is a first sketch of the same exercise applied to djot's syntax, with an explicit section on what a context-free grammar cannot capture and which formalism would:
djot-grammar.ebnf.txt
Djot's syntax is cleaner than Carve's superset, so the same split (layout automaton, guarded PEG inlines, resolution pass) should need strictly less machinery.