Module ui_bridge 

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

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.

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

Partition a possibly-MIXED document into its imperative and math streams.

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_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.

parse_math_statements

Split a Math-mode program into complete vernacular statements.

partition_mixed

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_net_async

Run a peer-networking program on the BYTECODE VM (single task, no channels): drive the resumable VM and service each VmBlock::Net* through the shared NetInbox — the SAME inbox the tree-walker uses — so Connect/Listen/Send/Stream/Await run byte-identically on both tiers. The VM analog of the tree-walker’s networking path; the cross-tier lock proves they agree.

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_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_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.

verify_theorem

Phase 78: Verify a theorem with full kernel certification.

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_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: lex → MWE → discovery → parse. The tree-walker and the bytecode VM MUST both come through here so they see the identical token stream, type registry, and policies — a differential test that parses differently per engine is comparing two different programs.

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.