I think it's harder because we are using the wrong tools, and have been doing so for a long time. We're documenting the reference under the illusion that Rust is in fact one language, but it is not. In observable terms, we have at minimum two languages, one syntactic and one semantic (and I think you're underestimating how much of AST validation we're not specifying at the moment even before the changes you've linked). But even so, I don't think it makes sense to e.g. document eventual borrow checking rules on something resembling HIR or HAIR; those can only be reasonably explained by something graph-like, e.g. like MIR (we did throw out ast_borrowck for a reason).

I also think it's not a good idea to document each concept, e.g. "if expressions" thoroughly from parsing to dynamic semantics. For a precise definition of the language, it's better to order explanations as a pipeline, taking one IR and transforming it down to another, as that is how any actual implementation, including for an interpreter, would be structured, even if it was a reference implementation in e.g. Agda. Then, in each part of the pipeline, you only explain what is needed in that pipe. This is what e.g. SML's spec does (see e.g. "bare language"), http://sml-family.org/sml97-defn.pdf, and CakeML goes even further, https://cakeml.org/.

So yes, I think we should give into having two "grammars" (where the latter is abstract syntax, not concrete) especially because a real formal specification without it has no hope of success. Transforming from the former to the latter can be explained using a denotational style (we can translate this fairly easily to inference rules as well for a more type-checking like style):

elab_slice_pats : [Syn.Pat] -> ([Abs.Pat], Option Abs.Pat, [Abs.Pat])
elab_slice_pats ([[ .. ]] :: ps) = ([], Some Wild, map elab_pat ps)
elab_slice_pats ([[ b @ .. ]] :: ps) = ([], Some (e_binding b Wild), map elab_pat ps)
elab_slice_pats (p :: ps) = (elab_pat p :: pre, mid, suf)
  where (pre, mid, suf) = elab_slice_pats ps

elab_pat : Syn.Pat -> Abs.Pat
elab_pat [[ .. ]] = error -- propagates implicitly; or we use monads if needed.
elab_pat [[ [ p0, ..., pn ] ]] = elab_slice_pats [[ [ p0, ..., pn] ]]
... -- more cases

Aside from introducing more syntactic shorthands, this is the tersest definition I can think of (way shorter than the actual Rust code, but it is still formal, and nearly executable). My initial versions of the slice patterns report had something like this. We can type set this appropriately and add comments where interesting things, e.g. not just identical structural transformations, happen. Auxiliary definitions can be defined and we can explain the syntactic conventions first.

However, you asked for a simple way, which I'm going to interpret as "don't rock the boat". To avoid doing so, I suppose we could add a chapter for "restrictions on syntax" where we say in a "declarative" way which productions would result in errors:

visit Trait => item_cx := Assoc(Trait) -- Implicitly following stack discipline.
visit Impl => item_cx := Assoc(Impl)
visit Statement | Module | Crate => item_cx := Free
visit ExternBlock => item_cx := Extern

error
  when item_cx == Extern
  on FunctionItem f where f.body != ";"

This is a sort of made up DSL for how AST validation behaves (not exactly a clean approach in my view; it's very much "validate" instead of "parse").

Description

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions