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});