Skip to main content

Module ast_span

Module ast_span 

Source
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§

AstSpanError

Functions§

render_from_ast
Reconstruct source from the AST’s byte spans plus the lexer’s trivia.