Skip to main content

logicaffeine_web/ui/pages/guide/content/
mod.rs

1//! Embedded guide content for the Programmer's Guide page.
2//!
3//! Every section of the Programmer's Guide as Rust constants: WASM cannot read files at runtime,
4//! so the content is embedded at compile time.
5
6use crate::ui::components::code_editor::Language;
7
8/// Mode for code examples - determines how "Run" executes them
9#[derive(Clone, Copy, PartialEq, Eq, Debug)]
10pub enum ExampleMode {
11    /// Logic mode: compile to First-Order Logic (FOL)
12    Logic,
13    /// Imperative mode: execute via WASM interpreter
14    Imperative,
15    /// Theorem mode: run the proof engine (`compile_theorem_for_ui`) — the
16    /// output is the kernel-certified verdict.
17    Theorem,
18    /// Web mode: an LGX page compiled to WebAssembly in the browser and shown
19    /// live in a sandboxed frame — the preview the Studio's Web tab runs
20    /// (`web_host::assemble_preview`). A web example proves itself with its
21    /// own `## Test` blocks rather than with printed output.
22    Web,
23}
24
25impl ExampleMode {
26    /// The editor language the example is read in: LOGOS code (a program or a page), or the
27    /// English of sentences and theorems — as the Studio reads a `.logos` and a `.logic` file.
28    pub fn language(self) -> Language {
29        match self {
30            ExampleMode::Imperative | ExampleMode::Web => Language::Logos,
31            ExampleMode::Logic | ExampleMode::Theorem => Language::Logic,
32        }
33    }
34}
35
36/// How an example behaves in the browser playground. The single source of
37/// truth shared by the Run-button affordance, the badge, AND the test harness
38/// partition (`tests/guide_examples.rs`) — the three can never disagree.
39#[derive(Clone, Copy, PartialEq, Eq, Debug)]
40pub enum Runnability {
41    /// Executes in the browser playground.
42    Playground,
43    /// The runtime only exists in compiled Rust; the UI renders a badge with
44    /// the reason instead of a Run button that would fail.
45    CompiledOnly { reason: &'static str },
46    /// The example fails ON PURPOSE — the displayed Socratic error is the
47    /// content. The full diagnostic text is locked exactly.
48    ExpectedError { message: &'static str },
49}
50
51/// A code example within a section
52#[derive(Clone, Debug, PartialEq)]
53pub struct CodeExample {
54    pub id: &'static str,
55    pub label: &'static str,
56    pub mode: ExampleMode,
57    pub runnability: Runnability,
58    pub expected_output: Option<&'static str>,
59    /// Predict-before-reveal (Muller/POE): the block renders with its locked
60    /// expectation HIDDEN and asks the reader to commit first. Only legal with
61    /// something locked to predict (enforced by `guide_pedagogy.rs`).
62    pub predict_first: bool,
63    pub code: &'static str,
64}
65
66/// A section of the guide
67#[derive(Clone, Debug)]
68pub struct Section {
69    pub id: &'static str,
70    pub number: u8,
71    pub title: &'static str,
72    pub part: &'static str,
73    /// The headache before the aspirin (Meyer/Dewey): a concrete problem the
74    /// reader can't yet solve, rendered as the section's opener — before any
75    /// definition gets to speak. Empty until authored; teaching sections are
76    /// floor-ratcheted toward full coverage.
77    pub hook: &'static str,
78    /// "After this section you can …" — observable Bloom-verb behaviors
79    /// (Mager). 2..=5 once authored.
80    pub objectives: &'static [&'static str],
81    pub content: &'static str,
82    /// Imported beliefs confronted in the reader's voice, each backed by a
83    /// runnable evidence example in this same section (Muller).
84    pub misconceptions: &'static [Misconception],
85    pub examples: &'static [CodeExample],
86    pub exercises: &'static [Exercise],
87    /// End-of-section "Check yourself" free-recall questions, reveal-style
88    /// (Roediger & Karpicke). Self-marks feed the SM-2 review deck.
89    pub recap: &'static [RecapQuestion],
90}
91
92/// "Coming from X you'd expect A; LOGOS does B because C" — stated first in
93/// the reader's voice, then proven by a runnable example.
94#[derive(Clone, Debug, PartialEq)]
95pub struct Misconception {
96    pub id: &'static str,
97    /// The belief the reader arrives with, in their voice.
98    pub expectation: &'static str,
99    /// What LOGOS does and WHY (the because is not optional).
100    pub reality: &'static str,
101    /// Id of the evidence example IN THIS SECTION — predict-first or
102    /// ExpectedError, so the reader commits before the proof lands.
103    pub evidence: &'static str,
104}
105
106/// One end-of-section retrieval prompt: question → recall → reveal →
107/// self-mark. Free recall, never multiple-choice (recognition ≠ production).
108#[derive(Clone, Debug, PartialEq)]
109pub struct RecapQuestion {
110    pub id: &'static str,
111    pub question: &'static str,
112    pub answer: &'static str,
113}
114
115/// The rung an exercise occupies on the worked→completion→free ladder
116/// (Sweller/Renkl fading). Within a section, support only ever fades.
117#[derive(Clone, Copy, PartialEq, Eq, Debug)]
118pub enum ExerciseKind {
119    /// The worked solution minus 1–3 `HOLE_MARKER` holes — the faded middle
120    /// rung between reading an example and writing from scratch.
121    Completion,
122    /// Free practice of one (max two) concepts.
123    Practice,
124    /// Multi-concept stretch — also the checkpoint interleaving vehicle.
125    Challenge,
126}
127
128/// The canonical hole token for Completion starters: greppable, never valid
129/// LOGOS, unmistakably a blank to fill.
130pub const HOLE_MARKER: &str = "???";
131
132/// A "now you try" challenge: the reader writes code (Imperative — graded by
133/// exact program output), a page (Web — graded by its own `## Test` blocks)
134/// or FOL (Logic — graded structurally by the Learn grader), right in the guide.
135#[derive(Clone, Debug, PartialEq)]
136pub struct Exercise {
137    pub id: &'static str,
138    /// Where this sits on the fading ladder.
139    pub kind: ExerciseKind,
140    /// The LANGUAGE_SURFACE features this practices (deliberate practice
141    /// targets the hard part; checkpoints interleave via these).
142    pub concepts: &'static [&'static str],
143    /// The task, stated to the reader.
144    pub prompt: &'static str,
145    pub mode: ExampleMode,
146    /// The graded target: exact output lines (Imperative) or the expected FOL. Empty for a Web
147    /// exercise, which is graded by the `## Test` blocks its page carries.
148    pub expected: &'static str,
149    /// Pre-filled editor contents.
150    pub starter: &'static str,
151    /// 1–3 progressive hints, disclosed on demand: orient, then narrow —
152    /// never the answer (Bloom's corrective tutor).
153    pub hints: &'static [&'static str],
154    /// The hidden answer key — the self-check lock proves it grades correct.
155    pub reference: &'static str,
156}
157
158/// All guide sections organized by part
159mod part1;
160mod part2;
161mod part3;
162mod part4;
163mod part5;
164mod part6;
165mod part7;
166mod part8;
167
168use std::sync::LazyLock;
169
170/// All guide sections in display order, concatenated from the per-part modules.
171pub static SECTIONS: LazyLock<Vec<Section>> = LazyLock::new(|| {
172    [
173        part1::PART_1,
174        part2::PART_2,
175        part3::PART_3,
176        part4::PART_4,
177        part5::PART_5,
178        part6::PART_6,
179        part7::PART_7,
180        part8::PART_8,
181    ]
182    .concat()
183});