logicaffeine_web/ui/pages/
studio_actions.rs

1//! What the Studio's toolbar actions can do for the file in the editor.
2//!
3//! Every mode has its buttons — Run, Compile and Debug in Code; Execute and Compile in Logic, Math
4//! and Hardware — but not every file can use every one: a Verilog design is already hardware, a
5//! grid puzzle has no Rust to extract, a program built on live networking cannot run in the
6//! browser. A button that can do nothing for the open file stays where it is, disabled, and says
7//! why in its tooltip. [`actions_for`] is the one place that decides; the toolbar draws from it.
8
9use crate::ui::state::StudioMode;
10
11/// Whether an action can do something for the open file — and why not, when it cannot.
12#[derive(Clone, Debug, PartialEq, Eq)]
13pub enum Offer {
14    Ready,
15    Unavailable(String),
16}
17
18impl Offer {
19    pub fn is_ready(&self) -> bool {
20        matches!(self, Offer::Ready)
21    }
22
23    /// Why the action is unavailable, for its tooltip.
24    pub fn reason(&self) -> Option<&str> {
25        match self {
26            Offer::Ready => None,
27            Offer::Unavailable(why) => Some(why),
28        }
29    }
30}
31
32/// The toolbar's actions for one file.
33#[derive(Clone, Debug, PartialEq, Eq)]
34pub struct Actions {
35    /// Run in Code mode; Execute in Logic, Math and Hardware.
36    pub run: Offer,
37    pub compile: Offer,
38    /// The Code debugger.
39    pub debug: Offer,
40}
41
42/// The actions the open file can take, from its mode, its path (the registry knows which shipped
43/// programs need the compiled runtime) and its text.
44pub fn actions_for(mode: StudioMode, path: Option<&str>, content: &str) -> Actions {
45    let unavailable = |why: &str| Offer::Unavailable(why.to_string());
46    if content.trim().is_empty() {
47        let empty = || unavailable("The editor is empty. Write something first.");
48        return Actions { run: empty(), compile: empty(), debug: empty() };
49    }
50    let only_code = || unavailable("The debugger steps through Code programs.");
51    match mode {
52        StudioMode::Code => {
53            let run = match path.and_then(crate::ui::examples::compiled_runtime_notice) {
54                Some(notice) => Offer::Unavailable(notice),
55                None => Offer::Ready,
56            };
57            Actions { debug: run.clone(), run, compile: Offer::Ready }
58        }
59        StudioMode::Logic => Actions {
60            run: Offer::Ready,
61            compile: match logicaffeine_compile::logic_compile_note(content) {
62                Some(note) => unavailable(note),
63                None => Offer::Ready,
64            },
65            debug: only_code(),
66        },
67        StudioMode::Math => Actions {
68            run: Offer::Ready,
69            compile: if is_theory(content) {
70                unavailable("A theory is certified by Execute. Compile turns Definitions and Inductives into Rust, and a theory declares none.")
71            } else if !declares_anything(content) {
72                unavailable("Compile turns Definitions and Inductives into Rust, and this file declares none. Execute runs its Checks and Evals.")
73            } else {
74                Offer::Ready
75            },
76            debug: only_code(),
77        },
78        StudioMode::Hardware => Actions {
79            run: Offer::Ready,
80            compile: match crate::ui::pages::hardware_report::kind_of(content)
81                .and_then(crate::ui::pages::hardware_report::nothing_to_compile)
82            {
83                Some(note) => unavailable(note),
84                None => Offer::Ready,
85            },
86            debug: only_code(),
87        },
88        StudioMode::Web => {
89            let live = || unavailable("The preview runs the app as you type.");
90            Actions { run: live(), compile: live(), debug: live() }
91        }
92    }
93}
94
95/// A `## Theory` development: axioms and cited theorems the multi-theorem driver certifies.
96fn is_theory(content: &str) -> bool {
97    content.lines().any(|line| line.trim_start().starts_with("## Theory"))
98}
99
100/// Whether a Math file declares anything extraction could turn into Rust — a statement in one of
101/// the kernel's defining forms (`command_parser::parse_command`), not a `Check` or an `Eval`.
102fn declares_anything(content: &str) -> bool {
103    crate::ui::pages::studio::parse_math_statements(content).iter().any(|statement| {
104        let s = statement.trim_start();
105        s.starts_with("Definition")
106            || s.starts_with("Inductive")
107            || s.starts_with("## To ")
108            || s.starts_with("## Theorem:")
109            || (s.starts_with("Let ") && s.contains(" be "))
110            || ((s.starts_with("A ") || s.starts_with("An ")) && s.contains(" is either"))
111    })
112}
113
114#[cfg(test)]
115#[path = "../../../../../crates/logicaffeine_tests/unit/logicaffeine_web/ui/pages/studio_actions/tests.rs"]
116mod tests;
logicaffeine_web/ui/pages/studio_actions.rs

logicaffeine_web/ui/pages/
studio_actions.rs
