Module ui_bridge

Expand description

UI bridge for web interface integration.

This module provides high-level, UI-friendly wrappers around the compilation pipeline, returning structured results suitable for display in the browser.

§Key Functions

Function	Purpose
`compile_for_ui`	Compile LOGOS to FOL (UI format)
`compile_for_proof`	Compile and search for proofs
`compile_theorem_for_ui`	Compile theorems with derivation trees
`verify_theorem`	Verify a theorem is provable
`interpret_for_ui`	Run imperative code and return output
`generate_rust_code`	Generate Rust source (requires `codegen` feature)

§Result Types

All functions return serializable result types:

CompileResult - Tokens, FOL, AST, errors
ProofCompileResult - FOL with proof search results
TheoremCompileResult - Theorem verification with derivation tree
InterpreterResult - Program output lines and errors

§Token Categories

The TokenCategory enum provides syntactic highlighting categories: Quantifier, Noun, Verb, Adjective, Connective, Determiner, etc.

Re-exports§

pub use crate::interpreter::InterpreterResult;

Structs§

AstNode: AST node for tree visualization in the UI.
CompileResult: Result of compiling English input to FOL with UI metadata.
GridColumn: One category column of a SolvedGrid.
ProofCompileResult: Result of compiling English to a proof expression.
SolvedGrid: A solved (or partially solved) logic grid: the row entities plus one column per declared category closure. Every filled cell is an entailment the no-Z3 certified prover (CDCL+RUP / kernel) closed, so the whole table is independently checkable.
TheoremCompileResult: Result of compiling and verifying a theorem block.
TheoremTrace: An English theorem proved, with its FOL and a human-readable PROOF TRACE — the “English in → proof out, see the trace” path. Parsing yields the premises and goal as FOL; the kernel-certified backward chainer yields the derivation, which renders as an indented step-by-step proof.
TheoryCompileResult: The result of compiling a program’s formal development — its ## Axiom declarations (a shared premise base) plus the theorems of its ## Theory block, each discharged in citation order and kernel-certified by the multi-theorem driver.
TheoryTheoremResult: A single theorem’s verdict within a compiled formal development.
TokenInfo: Token information for UI display with position and category.

Enums§

Engine: In-process execution tier. All choices consume the same optimized program.
TokenCategory: Syntactic category of a token for UI highlighting.

Functions§

answer_question: ANSWER a wh-question theorem (“Given: … Prove: Who is a lawyer?”). A wh-goal converts to ∃x.φ(x); the ANSWER is the witness. We find it the same way the puzzle is meant to be solved — by the GENERAL kernel-certified prover, applied per candidate: enumerate the domain individuals named in the premises and prove each candidate goal φ(c); the c’s that prove are the answer (usually one, for a puzzle with a unique solution). No question-specific reasoning — every step is the same prove_certify_check that proves Socrates.
compile_for_proof: Compile English input to ProofExpr for the proof engine.
compile_for_ui: Compile English input to FOL with full UI metadata.
compile_theorem_for_ui: Compile a theorem block for UI display.
compile_theory_for_ui: Compile a program’s formal development end to end: collect every ## Axiom (a shared premise base) and every ## Theory block’s Axiom/Theorem declarations, then prove the theorems in citation order, each kernel-certified by the multi-theorem driver. This is the seam that turns a Tarski-style source file into a verified development.
expr_to_ast_node: Converts a logic expression to an AST node for tree visualization.
extract_logic_module: Like extract_logic_rust, but emits NO demo main — the linkable form bundled into an imperative program’s mod proven (which has its own main). Produces the World + holds (+ Monitor) library items only.
extract_logic_rust: Compile a Logic-mode input to runnable Rust.
extract_math_module: Extract every user-defined inductive/definition in ctx into one Rust module — types, functions, and check_* property fns from proven theorems — WITHOUT a demo main. This is the linkable artifact bundled into an imperative program’s mod proven; extract_math_rust wraps it with a self-verifying main for the standalone Math compile.
extract_math_module_from_source: Like extract_math_rust_from_source, but produces the main-less module (the linkable artifact bundled into an imperative program’s mod proven).
extract_math_rust: Extract every user-defined inductive and definition in ctx into one Rust module — the “compile my math to Rust” path for the Math studio. Shared and StandardLibrary dependencies are pulled in only when a user definition transitively needs them, and are emitted exactly once.
extract_math_rust_from_source: Compile a Math-mode SOURCE program (the editor text) to a Rust module: split it into vernacular statements, run them into a fresh kernel, then extract every user-defined inductive/definition. This is the exact pipeline the Studio’s Math “🦀 Compile” button drives, exposed as one function so it is testable.
failure_sites_of: Every Stmt::Site marker input parsed to, as the (span, component, action) FailureSite the marker’s id indexes — in the author’s own file coordinates, the implicit-## Main wrap and the stdlib-prelude splice already undone (matching lgx_findings_of/parse_error_of’s own treatment). The tree-walker’s current_site() and a compiled program’s site_at pc-lookup both answer an id into THIS SAME table; whoever renders a runtime failure looks it up here and calls FailureSite::render with the message.
generate_rust_code: Generate Rust code from LOGOS source — the Studio Code path. Mixed-document aware: a source interleaving imperative code with Coq-style math (Definition/## Theorem:/…) extracts the math into a bundled mod proven that the imperative half calls into. Pure imperative source is a no-op partition.
generate_rust_code_with_proven: generate_rust_code with an already-extracted proven module bundled in.
grounded_grid_problem: The GROUNDED, quantifier-free grid problem (solver_input, goal) for an Auto grid theorem — the EXACT problem compile_theorem_for_ui solves, exposed so the trust tiers (Untrusted CDCL / RUP / Kernel) and the benchmark all run the same input. None if the theorem is not an Auto finite-domain grid.
implicit_main: IMPLICIT MAIN: a source with no ## headers whose first non-blank line reads as an imperative statement runs as its own ## Main body, so a bare script runs rather than parsing as logic prose. Natural-language documents (no statement-keyword opening) are untouched. Returns the wrapped source, or None when the input is not a bare script.
interpret_for_ui
interpret_for_ui_baseline: Baseline-tier interpret for the interactive UI (the Studio) — the cold-start engine. Runs on the bytecode VM with NO run-path optimizer (with_parsed_program, not with_optimized_program) and NO oracle (compile_with_types, not compile_with_oracle), so there is no optimize/analysis latency before execution. largo run and the benchmarks keep interpret_for_ui, which optimizes ahead of execution for peak throughput. Output is identical — the VM is differentially gated against the tree-walker on the SAME parsed statements (see the debug shadow-oracle assert in interpret_for_ui_baseline_sync_with_args); only the startup latency differs. This is the baseline half of the EXODIA tier split; promoting hot code to the optimized path is a later step.
interpret_for_ui_baseline_sync_with_args: The synchronous baseline core: parse (UNoptimized) → bytecode VM (no oracle) → run. Mirrors interpret_for_ui_sync_with_args exactly, minus optimize_for_run and the oracle range analysis.
interpret_for_ui_baseline_with_args: Like interpret_for_ui_baseline, but supplies the program’s argument vector to the args() system native.
interpret_for_ui_sync: Interpret LOGOS imperative code synchronously (no async runtime needed).
interpret_for_ui_sync_with_args: Like interpret_for_ui_sync, but supplies the program’s argument vector to the args() system native. program_args is the full argv (index 0 is the program name), matching the compiled binary’s env::args() — this is what largo run --interpret N forwards so an args-driven main.lg runs the same on the VM/JIT as on the native binary.
interpret_for_ui_sync_with_args_scoped: Project-aware form of interpret_for_ui_sync_with_args. The scope gate consumes the AST this execution already parsed, so explicit VM/JIT runs do not pay for a separate front-end parse on every invocation.
interpret_for_ui_with_args: Like interpret_for_ui, but supplies the program’s argument vector to the args() system native. program_args is the full argv (index 0 is the program name), matching the compiled binary’s env::args().
interpret_streaming: Interpret LOGOS imperative code with streaming output.
interpret_streaming_with_vfs: Like interpret_streaming, but routes the interpreter’s file I/O (Write/Read/Mount) to vfs. The browser Studio passes its WebVfs here so the standard-library I/O vocabulary works against OPFS/IndexedDB; a None vfs leaves file I/O reporting “VFS not initialized” as before. The clone-per-task model means concurrent tasks inherit the same VFS handle.
interpret_streaming_with_vfs_observer: Like interpret_streaming_with_vfs, but also emits a logicaffeine_runtime::SchedSnapshot to observer after each scheduler slice — the Studio’s Tasks/Channels strip subscribes here to show a concurrent program’s live task and channel state as it runs.
interpret_unsatisfiable_require: The tree-walk interpreter (largo run --interpret) is the raw differential tier — it applies NO optimizations, so it cannot satisfy any ## Require <opt>. Returns the honest error for the first requirement (mirroring the compiled tiers’ message), or None when there is none.
lgx_findings_of: The accessibility and structure warnings lgx/check.rs computes for input.
logic_compile_note: Why Logic’s Compile has no Rust to give for input, or None when it has one: a finite-domain puzzle is solved by Execute, and extracting it would run the whole solver — the same test extract_logic_rust makes before it bails.
parse_error_of: The parse error for input, in the AUTHOR’s own file coordinates — the implicit-## Main wrap and the stdlib-prelude splice both undone, exactly as with_parsed_program_checked undoes them for its callers — or None when input parses. A pure parse check with no ## Require gate: a caller that wants to render its OWN caret block (largo run --interpret, matching what largo check already shows) takes the located error from here instead of formatting whatever Result::Err variant happened to reach it.
parse_math_statements: Split a Math-mode program into complete vernacular statements.
partition_mixed: Partition a possibly-MIXED document into its imperative and math streams.
program_required_opts: The ## Require <opt> demands declared in input (a lightweight parse via parse_seam). Empty for a program with no ## Require decorators.
prove_theorem_trace: Prove an English ## Theorem block and return its FOL plus a rendered PROOF TRACE. Unlike verify_theorem (which returns the raw kernel term), this surfaces the derivation tree so the proof steps are visible.
repl_global_bindings: Run a program on the synchronous tree-walker and return its global bindings as sorted (name, type, value) rows — the REPL’s :vars inspection. Returns None for programs the sync walker can’t host (async/concurrent) or that fail to parse or run.
run_treewalker_concurrent_seeded: Parse input and run its concurrent program on the tree-walker scheduler under an explicit seed — the seeded sibling of the default run_program_concurrent entry, used by the cross-tier seeded differential.
run_vm_concurrent: Run a concurrent program on the bytecode VM under the deterministic scheduler (T11): compile to opcodes, then drive the main Vm (and any spawned per-task VMs) through run_until_block via a VmTask. This is the VM analog of run_program_concurrent; the default routing still sends concurrent programs to the tree-walker, so this is the explicit VM entry used to exercise and (Phase 5c) differentially compare the VM concurrency tier.
run_vm_concurrent_seeded: run_vm_concurrent under an explicit scheduler seed — the VM sibling of run_treewalker_concurrent_seeded for the cross-tier seeded differential.
run_vm_concurrent_traced: run_vm_concurrent_seeded, also returning the recorded scheduling trace — the seam the .replay failure artifact captures its schedule through.
run_vm_concurrent_traced_with_config: run_vm_concurrent_traced under an explicit SchedulerConfig (the config-parameterized core both the default-config and knobbed entry points delegate to).
run_vm_concurrent_with_config: Run a concurrent program on the VM under an EXPLICIT SchedulerConfig — the same knob surface the AOT bytecode-walker’s stepped scheduler exposes (crate::codegen_c::concurrency::SchedulerKnobs). This is the oracle side of the cross-tier knob equivalence: AOT-at-knobs-K == VM-at-knobs-K. The default-config wrapper is run_vm_concurrent.
run_vm_io_async: Run an IO program (peer networking and/or tcp.lg sockets) on the BYTECODE VM (single task, no channels): drive the resumable VM and service each VmBlock::Net*/VmBlock::Tcp through the shared NetInbox/TcpRegistry — the SAME seams the tree-walker uses — so networking and sockets run byte-identically on both tiers. The cross-tier locks prove they agree.
run_vm_net_async: Run a peer-networking program on the BYTECODE VM — the historical name for run_vm_io_async, kept so existing locks keep reading naturally.
run_vm_workstealing_seeded: run_vm_concurrent_seeded under the work-stealing M:N driver: workers OS-thread workers poll task bodies in parallel while one coordinator owns the scheduler and applies channel ops + flushes output in deterministic pick order. The observable result is byte-identical to the cooperative driver at the same seed (diff_cooperative_eq_workstealing_seeded) — the difference is that task bodies genuinely run on multiple cores.
set_engine: Select the tier used by subsequent in-process runs on this thread.
set_pending_aot_natives: Queue compiled-native functions for the next VM run on this thread (HOTSWAP §Axis-3). Consumed by the next interpret_for_ui_* VM run.
solve_grid: SOLVE the whole grid for the studio (the form-recognized easter egg): re-parse the theorem and, if it is a finite-domain grid, fill every cell the certified prover can force. None for a non-grid theorem.
theorem_certificate: Build an INDEPENDENTLY RE-CHECKABLE certificate for a proved English ## Theorem.
theorem_dependency_graph: The uses dependency graph (Rung 0b) for an English document: its ## Define blocks plus the theorem’s premises and goal, lowered and analyzed. Each node is a definition or the theorem; each edge is a uses. This is the structure a mathscrapes node/edge compiles into.
theorem_proof_exprs: Parse a ## Theorem: block and convert its premises and goal to ProofExprs — the shared front half of verify_theorem and check_theorem_smt. Parse a ## Theorem document and convert its premises and goal to ProofExpr. Public so a puzzle solver can obtain the parsed-FOL premises (the Given clues/declarations) and feed them to the entailment oracle.
theorem_proof_exprs_with_defs: Like theorem_proof_exprs but also returns the document’s ## Define blocks (Rung 0a) lowered to proof-layer definitions, so the prover can δ-unfold them. This is the entry the kernel-certified theorem path uses.
tokenize_for_ui: Tokenizes input text and returns token information for UI display.
value_copy_findings_of: The value-semantics copy lint’s warnings for input — see logicaffeine_language::lint. Same shape as lgx_findings_of: computed on every parse, worth nothing until something reads it.
verify_theorem: Phase 78: Verify a theorem with full kernel certification.
vm_listing: The bytecode the VM runs for input, as largo run --interpret compiles it: the run path’s optimizer, the oracle and the VM compiler. One section per function, ## Main first, then ## To <name> in code order, each instruction at its pc. A source that does not parse, or that only the tree-walker runs, answers why.
with_monomorphic_program: with_parsed_program over the program’s monomorphic form (crate::monomorphize) — every generic function and applied generic type made concrete — for a backend that lowers only concrete code.
with_monomorphic_program_checked: with_parsed_program_checked over the program’s monomorphic form (crate::monomorphize) — every generic function and applied generic type made concrete — for a backend that lowers only concrete code.
with_optimized_program: with_parsed_program, but the statements pass through the RUN-PATH optimizer (EXODIA D1: the Futamura residual — PE, GVN, LICM, closed-form, deforestation, interval analysis, DCE) before reaching the closure. The live largo run engines consume this; the differential seams stay on the raw variant so optimizer correctness is itself differentially gated (optimized-VM vs raw-tree-walker).
with_optimized_program_scoped: with_optimized_program, with the assembled project’s file scope checked on the same parsed AST before it is optimized. Project runners use this to avoid assembling and parsing the entire project a second time merely to enforce import visibility.
with_optimized_program_tiered: with_optimized_program gated by an explicit hotness tier (HOTSWAP §4): the statements pass through crate::optimize::optimize_for_run_tiered at tier. Tier::T3 reproduces with_optimized_program exactly; Tier::T0 skips the optimizer (the baseline tier). The accumulator→loop TCO rewrite is a LANGUAGE SEMANTIC, not an optimization, so it runs at every tier — deep recursion stays constant-stack regardless of the optimization tier.
with_parsed_program: The execution front-end shared by every engine (see parse_seam): lex → MWE → discovery → parse, with the file’s ## No decorators installed as the active config. ## Require is NOT enforced here — this generic variant serves the differential-test seams and callers whose return type can’t carry a compile error; use with_parsed_program_checked for the emit paths that must fail an unfired ## Require.
with_parsed_program_checked: with_parsed_program for a Result-returning compile (the emit c/isa/wasm backends): installs ## No, opens a ## Require firing-trace around f, and after f succeeds fails the compile on any demanded optimization that did not fire — the honest answer when a backend (e.g. the VM tiers, which don’t memoize) cannot provide a required optimization. f’s own error propagates unchanged.
with_parsed_tensor_program: with_parsed_program that also hands over every tensor’s (rows, cols) — the shape table the parser keeps and the desugared statements do not (a declaration desugars to a flat Seq of rows · cols elements). The spatial walk reads it to declare each tensor in the shape the program gives it.
with_v2_optimized_program: Like with_optimized_program, but the program runs through the ARCHITECT pipeline (optimize_program_v2): equality saturation with kernel-certified rewrites in place of GVN + LICM + closed-form. The differential gates in phase_exodia_architect.rs hold this path to the raw tree-walker’s outcomes.

Type Aliases§

ObserverCallback: A snapshot sink for the Studio’s Tasks/Channels strip — invoked between scheduler slices with the live task/channel state.

Module ui_bridge

Module ui_bridge Copy item path

§Key Functions

§Result Types

§Token Categories

Re-exports§

Structs§

Enums§

Functions§

Type Aliases§

Module ui_bridge