logicaffeine_tv/
parse.rs

1//! Parse a LOGOS source string into the arena-allocated AST and hand it to a
2//! callback, mirroring the front-end of `compile::compile_program_full`.
3//!
4//! The parser needs a bundle of bumpalo arenas whose lifetimes cannot escape the
5//! parsing scope, so access is given through a callback `f(&[Stmt], &Interner)`.
6//! Whatever the callback returns (typically a [`crate::symexec::SymSummary`], which
7//! holds only owned `VerifyExpr`s) outlives the arenas.
8
9use logicaffeine_compile::ast::{Expr, Stmt, TypeExpr};
10use logicaffeine_compile::drs::WorldState;
11use logicaffeine_compile::{Arena, AstContext, DiscoveryPass, Interner, Lexer, ParseError, Parser};
12
13/// Parse `source`, optionally run the production optimizer, and invoke `f` with the
14/// resulting statements and the interner used to intern their symbols.
15///
16/// When `optimize` is true the statements are passed through
17/// `optimize::optimize_program` — the same 14-pass pipeline the real compiler runs —
18/// so callers can validate the optimizer's output against the source.
19pub fn with_program<R>(
20    source: &str,
21    optimize: bool,
22    f: impl FnOnce(&[Stmt], &Interner) -> R,
23) -> Result<R, ParseError> {
24    let mut interner = Interner::new();
25    let mut lexer = Lexer::new(source, &mut interner);
26    let tokens = lexer.tokenize();
27
28    let type_registry = {
29        let mut discovery = DiscoveryPass::new(&tokens, &mut interner);
30        discovery.run_full().types
31    };
32
33    let mut world_state = WorldState::new();
34    let expr_arena = Arena::new();
35    let term_arena = Arena::new();
36    let np_arena = Arena::new();
37    let sym_arena = Arena::new();
38    let role_arena = Arena::new();
39    let pp_arena = Arena::new();
40    let stmt_arena: Arena<Stmt> = Arena::new();
41    let imperative_expr_arena: Arena<Expr> = Arena::new();
42    let type_expr_arena: Arena<TypeExpr> = Arena::new();
43
44    let ast_ctx = AstContext::with_types(
45        &expr_arena,
46        &term_arena,
47        &np_arena,
48        &sym_arena,
49        &role_arena,
50        &pp_arena,
51        &stmt_arena,
52        &imperative_expr_arena,
53        &type_expr_arena,
54    );
55
56    let mut parser = Parser::new(tokens, &mut world_state, &mut interner, ast_ctx, type_registry);
57    let stmts = parser.parse_program()?;
58    drop(parser);
59
60    let stmts = if optimize {
61        logicaffeine_compile::optimize::optimize_program(
62            stmts,
63            &imperative_expr_arena,
64            &stmt_arena,
65            &mut interner,
66            &logicaffeine_compile::optimization::OptimizationConfig::from_env(),
67        )
68    } else {
69        stmts
70    };
71
72    Ok(f(&stmts, &interner))
73}
logicaffeine_tv/parse.rs

logicaffeine_tv/
parse.rs
