Expand description
AST byte-span losslessness oracle (render_from_ast): reconstruct source
from the parse tree to prove the tree lost nothing.
AST losslessness oracle for daml-fmt.
Every AST node carries a byte Span (see ast::Span). This module proves
those spans are faithful: it collects every node’s span, checks they form a
laminar family (each child contained in its parent, siblings ordered and
disjoint — ast::Span invariants), and reconstructs the file by tiling the
span forest with the verbatim source bytes that fall between sibling spans.
If the spans nest correctly and the module span covers the file, the reconstruction is byte-identical to the source. A parser that dropped a token’s bytes from every node span, or produced an overlap, fails here.
Enums§
Functions§
- render_
from_ ast - Reconstruct
sourcefrom the AST’s byte spans plus the lexer’strivia.