logicaffeine_web/ui/pages/
studio_run.rs

1//! What Execute does with a Logic or a Math document, for every surface that runs one.
2//!
3//! A Logic document is a `## Theorem` block, compiled and handed to the prover, or plain English
4//! sentences, each read into logic. A Math document is a `## Theory` development, every theorem
5//! certified on its own, or kernel statements run in order from a fresh kernel, so each run
6//! replaces the last. The front page's mini Studio runs its examples through these, so it shows
7//! what the Studio shows; a Code program runs on `interpret_for_ui_baseline`, and a Hardware design
8//! is read by `hardware_report::analyze`.
9
10use logicaffeine_compile::{compile_for_proof, compile_for_ui, compile_theorem_for_ui, CompileResult, ProofCompileResult, TheoremCompileResult};
11use logicaffeine_kernel::interface::Repl;
12
13use crate::ui::pages::studio::parse_math_statements;
14use crate::ui::state::ReplLine;
15
16/// What running a Logic document produced.
17pub enum LogicRun {
18    /// A `## Theorem:` block: its compiled result, or why it did not compile.
19    Theorem(Result<TheoremCompileResult, String>),
20    /// Plain sentences: their readings, and the first of them compiled for the prover.
21    Sentences(CompileResult, ProofCompileResult),
22    /// Nothing but headers and comments.
23    Empty,
24}
25
26pub fn run_logic(text: &str) -> LogicRun {
27    if text.contains("## Theorem:") {
28        let result = compile_theorem_for_ui(text);
29        return LogicRun::Theorem(match result.error.clone() {
30            Some(error) => Err(error),
31            None => Ok(result),
32        });
33    }
34    // Plain English: markdown headers (#) and LOGOS comments (--) are not sentences.
35    let sentences: Vec<&str> = text
36        .lines()
37        .filter(|line| {
38            let trimmed = line.trim();
39            !trimmed.is_empty() && !trimmed.starts_with('#') && !trimmed.starts_with("--")
40        })
41        .collect();
42    match sentences.first() {
43        // The proof engine works on the first sentence.
44        Some(first) => LogicRun::Sentences(compile_for_ui(&sentences.join("\n")), compile_for_proof(first)),
45        None => LogicRun::Empty,
46    }
47}
48
49/// What running a Math document produced: a line per statement, and, when the statements ran
50/// through the kernel, the kernel they left behind, whose environment the Studio's Context panel
51/// lists. A `## Theory` development certifies its theorems on its own and leaves no kernel.
52pub struct MathRun {
53    pub lines: Vec<ReplLine>,
54    pub kernel: Option<Repl>,
55}
56
57/// Runs a Math document from a fresh kernel, so each run replaces the last rather than piling on.
58pub fn run_math(code: &str) -> MathRun {
59    if code.lines().any(|line| line.trim_start().starts_with("## Theory")) {
60        let theory = logicaffeine_compile::ui_bridge::compile_theory_for_ui(code);
61        let mut lines = Vec::new();
62        if let Some(error) = &theory.parse_error {
63            lines.push(ReplLine::error("## Theory".to_string(), error.clone()));
64        } else {
65            lines.push(ReplLine::success(
66                format!("Theory {} ({} axioms)", theory.theory_name.clone().unwrap_or_default(), theory.axiom_count),
67                format!("{} theorems checked", theory.theorems.len()),
68            ));
69            for theorem in &theory.theorems {
70                if theorem.verified {
71                    lines.push(ReplLine::success(format!("Theorem {}", theorem.name), "kernel-certified".to_string()));
72                } else {
73                    lines.push(ReplLine::error(
74                        format!("Theorem {}", theorem.name),
75                        theorem.error.clone().unwrap_or_else(|| "not certified".to_string()),
76                    ));
77                }
78            }
79        }
80        return MathRun { lines, kernel: None };
81    }
82
83    let mut kernel = Repl::new();
84    let lines = parse_math_statements(code)
85        .into_iter()
86        .map(|statement| match kernel.execute(&statement) {
87            Ok(output) => ReplLine::success(statement, output),
88            Err(error) => ReplLine::error(statement, error.to_string()),
89        })
90        .collect();
91    MathRun { lines, kernel: Some(kernel) }
92}
93
94#[cfg(test)]
95#[path = "../../../../../crates/logicaffeine_tests/unit/logicaffeine_web/ui/pages/studio_run/tests.rs"]
96mod tests;
logicaffeine_web/ui/pages/studio_run.rs

logicaffeine_web/ui/pages/
studio_run.rs
