logicaffeine_language/
teach.rs

1//! The one teaching truth for LOGOS constructs: every lesson a surface shows
2//! — LSP hover, completion documentation, the REPL's `:explain` — comes from
3//! THIS table, so the editor and the terminal always teach the same thing.
4//!
5//! A [`ConstructDoc`] is complete by construction: the type has no optional
6//! teaching fields, so an entry cannot exist without a plain-English
7//! sentence, a runnable example, and a socratic question or tip. The
8//! `doc_for` match is wildcard-free (the `token_class` idiom): adding a
9//! `TokenType` variant does not compile until someone decides whether it
10//! deserves a lesson — the decision lives here, next to the enum, not in an
11//! editor plugin. `doc_for_block` is total: every `##` block type teaches.
12
13use crate::token::{BlockType, TokenType};
14
15/// A complete lesson for one construct. Every field is required by the TYPE —
16/// an entry cannot exist without a plain sentence, a runnable example, and a
17/// socratic question or tip. Clear-and-easy is structural, not aspirational.
18pub struct ConstructDoc {
19    /// The construct's display name ("Give", "Main", "Seq").
20    pub name: &'static str,
21    /// ONE plain sentence: what it does. Kept under 90 characters by the
22    /// teach lock — if it needs more, the rest belongs in the question/tip.
23    pub what: &'static str,
24    /// A runnable snippet (code-block body, no fences). Must lex.
25    pub example: &'static str,
26    /// The socratic seat: a guiding question (contains `?`) or an explicit
27    /// `Tip:` — it leads the reader to the next insight, never just restates.
28    pub question_or_tip: &'static str,
29    /// A LOGOS_QUICKGUIDE.md heading slug for "read more", when one fits.
30    pub guide_anchor: Option<&'static str>,
31}
32
33const fn lesson(
34    name: &'static str,
35    what: &'static str,
36    example: &'static str,
37    question_or_tip: &'static str,
38    guide_anchor: Option<&'static str>,
39) -> ConstructDoc {
40    ConstructDoc { name, what, example, question_or_tip, guide_anchor }
41}
42
43// ---------------------------------------------------------------------------
44// Statement keywords
45// ---------------------------------------------------------------------------
46
47static LET: ConstructDoc = lesson(
48    "Let",
49    "Declares a new variable.",
50    "Let x be 5.\nLet name: Text be \"Alice\".",
51    "Will the value change later? Then declare it `Let mutable x be 5.` — plain `Let` is immutable.",
52    Some("2-variables--mutation"),
53);
54
55static SET_KW: ConstructDoc = lesson(
56    "Set",
57    "Updates an existing mutable variable.",
58    "Set x to 10.",
59    "Was `x` declared with `Let mutable`? Only mutable bindings can be `Set`.",
60    Some("2-variables--mutation"),
61);
62
63static RETURN: ConstructDoc = lesson(
64    "Return",
65    "Hands a value back from the current function.",
66    "Return x.",
67    "Does the value's type match the function's declared `-> Type`? `Return.` alone returns nothing.",
68    Some("6-control-flow"),
69);
70
71static IF: ConstructDoc = lesson(
72    "If",
73    "Runs a block only when its condition holds.",
74    "If x > 0:\n    Show x.\nOtherwise:\n    Show 0.",
75    "What should happen when the condition is false — nothing, an `Otherwise:` branch, or an `elif`?",
76    Some("6-control-flow"),
77);
78
79static WHILE: ConstructDoc = lesson(
80    "While",
81    "Repeats a block as long as its condition stays true.",
82    "While x > 0:\n    Set x to x - 1.",
83    "Does the body change the condition? A body that never does loops forever — `(decreasing e)` proves termination.",
84    Some("6-control-flow"),
85);
86
87static REPEAT: ConstructDoc = lesson(
88    "Repeat",
89    "Walks a collection, binding each element in turn.",
90    "Repeat for item in items:\n    Show item.",
91    "Need positions instead of elements? Count with `for i from 1 to n:` — LOGOS is 1-based.",
92    Some("5-collections"),
93);
94
95static SHOW: ConstructDoc = lesson(
96    "Show",
97    "Displays a value while only borrowing it — you keep ownership.",
98    "Show x.",
99    "Need the value afterward? `Show` lends; `Give` transfers — pick by who owns it next.",
100    Some("13-output"),
101);
102
103static GIVE: ConstructDoc = lesson(
104    "Give",
105    "Transfers ownership of a value to a new owner.",
106    "Give x to processor.",
107    "Who should own this value afterward — you, or the receiver? Keep it by giving `a copy of x`.",
108    Some("13-output"),
109);
110
111static PUSH: ConstructDoc = lesson(
112    "Push",
113    "Appends a value to the end of a sequence.",
114    "Push 5 to items.",
115    "Tip: `Push` grows a Seq by one; for Sets use `Add v to s.` — sets have no order to push onto.",
116    Some("5-collections"),
117);
118
119static INSPECT: ConstructDoc = lesson(
120    "Inspect",
121    "Pattern-matches a value, running one branch per variant.",
122    "Inspect shape:\n    When Circle (r):\n        Show r.\n    Otherwise:\n        Show \"other\".",
123    "Is every variant handled? `Otherwise:` catches the rest — or list each `When` and let the checker verify.",
124    Some("6-control-flow"),
125);
126
127static CALL: ConstructDoc = lesson(
128    "Call",
129    "Invokes a function as a statement.",
130    "Call process with data.",
131    "Tip: in expressions call directly — `add(3, 7)`; `Call f with a and b.` is the statement form.",
132    Some("7-functions--closures"),
133);
134
135static NEW: ConstructDoc = lesson(
136    "New",
137    "Creates a struct or variant instance with named field values.",
138    "Let p be a new Point with x 10 and y 20.",
139    "Tip: fields are set by name — `with x 10 and y 20` — so argument order never bites.",
140    Some("8-structs-enums--field-access"),
141);
142
143static ESCAPE: ConstructDoc = lesson(
144    "Escape",
145    "Embeds raw foreign code, skipping every LOGOS checker.",
146    "Escape to Rust:\n    println!(\"hello\");",
147    "Could plain LOGOS express this? Escaped code is invisible to the ownership and type checkers.",
148    None,
149);
150
151static CHECK: ConstructDoc = lesson(
152    "Check",
153    "Enforces a security capability at runtime — a mandatory gate.",
154    "Check that balance is at least amount.",
155    "What may this code path do, and who says so? `## Policy` blocks define the capabilities.",
156    Some("10-contracts-refinement-assert-trust-check"),
157);
158
159static POP: ConstructDoc = lesson(
160    "Pop",
161    "Removes the last element of a sequence.",
162    "Pop from xs.\nPop from xs into y.",
163    "Need the popped value? `Pop from xs into y.` binds it; plain `Pop` discards it.",
164    Some("5-collections"),
165);
166
167static ADD: ConstructDoc = lesson(
168    "Add",
169    "Inserts a value into a set.",
170    "Add v to s.",
171    "Tip: sets keep one of each value — adding a duplicate changes nothing, and order is not kept.",
172    Some("5-collections"),
173);
174
175static REMOVE: ConstructDoc = lesson(
176    "Remove",
177    "Deletes a value from a set.",
178    "Remove v from s.",
179    "Tip: removing a value that isn't present is a quiet no-op — test `s contains v` when it matters.",
180    Some("5-collections"),
181);
182
183static BREAK: ConstructDoc = lesson(
184    "Break",
185    "Exits the innermost loop immediately.",
186    "While true:\n    Break.",
187    "Which loop should stop? `Break.` only leaves the innermost one.",
188    Some("6-control-flow"),
189);
190
191static ASSERT: ConstructDoc = lesson(
192    "Assert",
193    "Checks a condition at runtime, failing loudly when it is false.",
194    "Assert that x is equal to 42.",
195    "Is this a debugging aid or a security rule? Debug checks `Assert`; mandatory gates use `Check`.",
196    Some("10-contracts-refinement-assert-trust-check"),
197);
198
199static TRUST: ConstructDoc = lesson(
200    "Trust",
201    "States a justified assumption, carrying its reason.",
202    "Trust that x is greater than 0 because \"set to 10\".",
203    "Why is this safe? The `because` reason is required — future readers hold you to it.",
204    Some("10-contracts-refinement-assert-trust-check"),
205);
206
207static INCREASE: ConstructDoc = lesson(
208    "Increase",
209    "Grows a shared CRDT counter field — merges without conflicts.",
210    "Increase c's points by 10.",
211    "Tip: `Increase` is for `Shared` CRDT fields; plain integers update with `Set i to i + 1.`",
212    Some("12-distributed-crdt-concurrency-networking-zones"),
213);
214
215static DECREASE: ConstructDoc = lesson(
216    "Decrease",
217    "Shrinks a shared CRDT counter field — merges without conflicts.",
218    "Decrease g's score by 30.",
219    "Tip: `Decrease` is for `Shared` CRDT fields; plain integers update with `Set i to i - 1.`",
220    Some("12-distributed-crdt-concurrency-networking-zones"),
221);
222
223static SPAWN: ConstructDoc = lesson(
224    "Spawn",
225    "Starts an agent — an independent concurrent actor.",
226    "Spawn an EchoAgent called \"echo\".",
227    "How will you reach it later? The `called \"name\"` handle is how messages find the agent.",
228    Some("12-distributed-crdt-concurrency-networking-zones"),
229);
230
231static MERGE: ConstructDoc = lesson(
232    "Merge",
233    "Folds one CRDT replica into another without conflicts.",
234    "Merge remote into local.",
235    "Tip: merge order never matters — replicas converge to the same state either way.",
236    Some("12-distributed-crdt-concurrency-networking-zones"),
237);
238
239// ---------------------------------------------------------------------------
240// Block headers
241// ---------------------------------------------------------------------------
242
243static BLOCK_MAIN: ConstructDoc = lesson(
244    "Main",
245    "The program's entry point — statements here run top to bottom.",
246    "## Main\nShow \"Hello, World!\".",
247    "Tip: one `## Main` per program; everything else is definitions it can call.",
248    Some("1-program-structure"),
249);
250
251static BLOCK_FUNCTION: ConstructDoc = lesson(
252    "To",
253    "Defines a function; parameters and return type live in the header.",
254    "## To add (a: Int, b: Int) -> Int:\n    Return a + b.",
255    "What does it give back? `-> Type` declares it; omit the arrow for a procedure.",
256    Some("7-functions--closures"),
257);
258
259static BLOCK_THEOREM: ConstructDoc = lesson(
260    "Theorem",
261    "Declares a proposition to be proved.",
262    "## Theorem: Socrates\nGiven: All men are mortal. Socrates is a man.\nProve: Socrates is mortal.\nProof: Auto.",
263    "What structure does the claim have — universal, implication, equality? The proof strategy follows it.",
264    Some("1-program-structure"),
265);
266
267static BLOCK_PROOF: ConstructDoc = lesson(
268    "Proof",
269    "Holds the proof steps for the theorem above it.",
270    "Proof: Auto.",
271    "Stuck? Start with `Auto.` — the prover reports what it can and cannot discharge.",
272    None,
273);
274
275static BLOCK_DEFINITION: ConstructDoc = lesson(
276    "Definition",
277    "Introduces new terminology for later sentences to use.",
278    "## Definition: A bachelor is an unmarried man.",
279    "Tip: `## Definition` explains terms; executable data shapes live in `## A ... has:` blocks.",
280    None,
281);
282
283static BLOCK_DEFINE: ConstructDoc = lesson(
284    "Define",
285    "Mints a predicate the prover can unfold by definition.",
286    "## Define: A number is tiny if it is less than 10.",
287    "Tip: proofs may unfold this exactly — the prover substitutes the body for the name.",
288    None,
289);
290
291static BLOCK_AXIOM: ConstructDoc = lesson(
292    "Axiom",
293    "Declares a named formal axiom as a shared premise.",
294    "## Axiom cong_refl: for all a b, Cong(a,b,b,a).",
295    "Tip: axioms are believed, not proved — keep them few and inspectable.",
296    None,
297);
298
299static BLOCK_THEORY: ConstructDoc = lesson(
300    "Theory",
301    "Names a development grouping the axioms and theorems after it.",
302    "## Theory Tarski",
303    "Tip: a theory bundles `## Axiom`s with the `## Theorem`s proved from them.",
304    None,
305);
306
307static BLOCK_TYPEDEF: ConstructDoc = lesson(
308    "TypeDef",
309    "Defines a struct or enum type in English.",
310    "## A Point has:\n    An x: Int.\n    A y: Int.",
311    "One thing with fields, or one of several shapes? `has:` makes a struct; `is one of:` an enum.",
312    Some("8-structs-enums--field-access"),
313);
314
315static BLOCK_POLICY: ConstructDoc = lesson(
316    "Policy",
317    "Defines the security rules that `Check` statements enforce.",
318    "## Policy\nUsers can read public files.",
319    "Who may do what? Policies name capabilities; `Check that ...` gates on them.",
320    Some("10-contracts-refinement-assert-trust-check"),
321);
322
323static BLOCK_LOGIC: ConstructDoc = lesson(
324    "Logic",
325    "Holds direct logical notation instead of English.",
326    "## Logic\nforall x. Man(x) -> Mortal(x)",
327    "Tip: use it when symbols say it better — English and notation share one prover.",
328    None,
329);
330
331static BLOCK_EXAMPLE: ConstructDoc = lesson(
332    "Example",
333    "Shows an illustrative example the compiler treats as documentation.",
334    "## Example\nShow 42.",
335    "Tip: examples read as prose — the highlighter fades them so code stands out.",
336    None,
337);
338
339static BLOCK_NOTE: ConstructDoc = lesson(
340    "Note",
341    "Documentation prose the compiler skips and the highlighter fades.",
342    "## Note\nThis module parses dates.",
343    "Tip: a `## Note` right above a definition becomes that definition's documentation.",
344    None,
345);
346
347static BLOCK_REQUIRES: ConstructDoc = lesson(
348    "Requires",
349    "Declares external crate dependencies for escaped code.",
350    "## Requires\nserde",
351    "Tip: only `Escape` blocks need this — pure LOGOS programs never do.",
352    None,
353);
354
355static BLOCK_HARDWARE: ConstructDoc = lesson(
356    "Hardware",
357    "Declares hardware signals for verification.",
358    "## Hardware\nclk is a signal.",
359    "What are the inputs and state bits? Properties below verify against exactly these signals.",
360    None,
361);
362
363static BLOCK_PROPERTY: ConstructDoc = lesson(
364    "Property",
365    "States temporal assertions about hardware signals.",
366    "## Property\nThe counter is eventually zero.",
367    "Always or eventually? Temporal words carry the meaning — the prover checks every cycle.",
368    None,
369);
370
371static BLOCK_NO: ConstructDoc = lesson(
372    "No",
373    "Turns one optimization off for the code that follows.",
374    "## No Memo",
375    "Tip: use it to pin a benchmark or dodge a pathological case — semantics never change.",
376    None,
377);
378
379static BLOCK_TIER: ConstructDoc = lesson(
380    "Tier",
381    "Pins the hotness tier at which an optimization runs.",
382    "## Tier Memo eager",
383    "Tip: `eager`, `t1`–`t3`, or `never` — this tunes WHEN the optimizer fires, not correctness.",
384    None,
385);
386
387static BLOCK_SUSPECTED_TYPO: ConstructDoc = lesson(
388    "Unknown header",
389    "An unknown header that looks like a typo of a real one.",
390    "## Mian",
391    "Did you mean the suggested header? Unknown `##` headers otherwise read as prose.",
392    None,
393);
394
395// ---------------------------------------------------------------------------
396// Primitive and built-in generic types
397// ---------------------------------------------------------------------------
398
399static TY_INT: ConstructDoc = lesson(
400    "Int",
401    "A whole number.",
402    "Let n: Int be 42.",
403    "Tip: `/` divides and `%` takes the remainder — `x is divisible by n` reads best in conditions.",
404    Some("3-arithmetic-comparison-logic-bitwise"),
405);
406
407static TY_NAT: ConstructDoc = lesson(
408    "Nat",
409    "A whole number that can never be negative.",
410    "Let count: Nat be 0.",
411    "Can this value ever go below zero? If subtraction might take it there, use Int instead.",
412    None,
413);
414
415static TY_TEXT: ConstructDoc = lesson(
416    "Text",
417    "A string of characters.",
418    "Let name: Text be \"Alice\".",
419    "Tip: build strings by interpolation — `\"Hello, {name}!\"` — or `a combined with b`.",
420    Some("4-strings"),
421);
422
423static TY_BOOL: ConstructDoc = lesson(
424    "Bool",
425    "Either true or false.",
426    "Let ready: Bool be true.",
427    "Tip: `and`/`or`/`not` short-circuit and return Bool; 0 and empty collections count as false.",
428    Some("3-arithmetic-comparison-logic-bitwise"),
429);
430
431static TY_FLOAT: ConstructDoc = lesson(
432    "Float",
433    "A floating-point number for fractional values.",
434    "Let pi: Float be 3.14159.",
435    "Tip: floats round — format output with `\"{pi:.2}\"`, and avoid them for money.",
436    Some("3-arithmetic-comparison-logic-bitwise"),
437);
438
439static TY_UNIT: ConstructDoc = lesson(
440    "Unit",
441    "The empty value — what procedures return.",
442    "## To greet (name: Text):\n    Show name.",
443    "Tip: you rarely write Unit; a function without `-> Type` returns it implicitly.",
444    None,
445);
446
447static TY_CHAR: ConstructDoc = lesson(
448    "Char",
449    "A single character.",
450    "Let c: Char be 'a'.",
451    "Tip: Text is a sequence of Chars — one Char is the unit you get when you walk it.",
452    None,
453);
454
455static TY_BYTE: ConstructDoc = lesson(
456    "Byte",
457    "A single byte — a whole number from 0 to 255.",
458    "Let b: Byte be 255.",
459    "Tip: bytes are the unit of binary data; whole numbers past 255 need Int.",
460    None,
461);
462
463static TY_LIST: ConstructDoc = lesson(
464    "List",
465    "An ordered, growable collection (another name for Seq).",
466    "Let xs be a new List of Int.",
467    "Tip: `[1, 2, 3]` is the literal form; `Push` appends; indexing is 1-based.",
468    Some("5-collections"),
469);
470
471static TY_SEQ: ConstructDoc = lesson(
472    "Seq",
473    "An ordered, growable collection — the canonical list type.",
474    "Let xs: Seq of Int be [1, 2, 3].",
475    "Tip: `item 1 of xs` is the FIRST element — LOGOS indexing is 1-based.",
476    Some("5-collections"),
477);
478
479static TY_MAP: ConstructDoc = lesson(
480    "Map",
481    "A dictionary from keys to values.",
482    "Let m be a new Map of Text to Int.\nSet m at \"a\" to 1.",
483    "Tip: read with `item k of m` and write with `Set m at k to v.`",
484    Some("5-collections"),
485);
486
487static TY_SET: ConstructDoc = lesson(
488    "Set",
489    "An unordered collection holding each value once.",
490    "Let s be a new Set of Int.\nAdd 3 to s.",
491    "Tip: on sets `&`/`|`/`^` are intersection/union/symmetric-difference; `a without b` subtracts.",
492    Some("5-collections"),
493);
494
495static TY_OPTION: ConstructDoc = lesson(
496    "Option",
497    "A value that is either present or absent.",
498    "Let maybe be some 30.\nInspect maybe:\n    When OptionSome (v):\n        Show v.\n    When OptionNone:\n        Show \"nothing\".",
499    "What happens when the value is absent? `Inspect` makes you answer both ways.",
500    Some("9-options--pattern-matching"),
501);
502
503static TY_RESULT: ConstructDoc = lesson(
504    "Result",
505    "A success value or an error value — one or the other.",
506    "## To native read (path: Text) -> Result of Text and Text",
507    "Which side is which? `Result of Ok and Err` — handle both with `Inspect`.",
508    None,
509);
510
511/// Every lesson, for parity ratchets and the REPL's suggestion list.
512pub static ALL_DOCS: &[&ConstructDoc] = &[
513    // keywords
514    &LET, &SET_KW, &RETURN, &IF, &WHILE, &REPEAT, &SHOW, &GIVE, &PUSH, &INSPECT, &CALL, &NEW,
515    &ESCAPE, &CHECK, &POP, &ADD, &REMOVE, &BREAK, &ASSERT, &TRUST, &INCREASE, &DECREASE, &SPAWN,
516    &MERGE,
517    // block headers
518    &BLOCK_MAIN, &BLOCK_FUNCTION, &BLOCK_THEOREM, &BLOCK_PROOF, &BLOCK_DEFINITION, &BLOCK_DEFINE,
519    &BLOCK_AXIOM, &BLOCK_THEORY, &BLOCK_TYPEDEF, &BLOCK_POLICY, &BLOCK_LOGIC, &BLOCK_EXAMPLE,
520    &BLOCK_NOTE, &BLOCK_REQUIRES, &BLOCK_HARDWARE, &BLOCK_PROPERTY, &BLOCK_NO, &BLOCK_TIER,
521    &BLOCK_SUSPECTED_TYPO,
522    // types
523    &TY_INT, &TY_NAT, &TY_TEXT, &TY_BOOL, &TY_FLOAT, &TY_UNIT, &TY_CHAR, &TY_BYTE, &TY_LIST,
524    &TY_SEQ, &TY_MAP, &TY_SET, &TY_OPTION, &TY_RESULT,
525];
526
527/// The lesson for a statement keyword, when the token deserves one.
528///
529/// Wildcard-free: a new `TokenType` variant does not compile until someone
530/// decides whether it teaches (a lesson arm) or not (the grouped `None` arm).
531pub fn doc_for(kind: &TokenType) -> Option<&'static ConstructDoc> {
532    match kind {
533        TokenType::Let => Some(&LET),
534        TokenType::Set => Some(&SET_KW),
535        TokenType::Return => Some(&RETURN),
536        TokenType::If => Some(&IF),
537        TokenType::While => Some(&WHILE),
538        TokenType::Repeat => Some(&REPEAT),
539        TokenType::Show => Some(&SHOW),
540        TokenType::Give => Some(&GIVE),
541        TokenType::Push => Some(&PUSH),
542        TokenType::Inspect => Some(&INSPECT),
543        TokenType::Call => Some(&CALL),
544        TokenType::New => Some(&NEW),
545        TokenType::Escape => Some(&ESCAPE),
546        TokenType::Check => Some(&CHECK),
547        TokenType::Pop => Some(&POP),
548        TokenType::Add => Some(&ADD),
549        TokenType::Remove => Some(&REMOVE),
550        TokenType::Break => Some(&BREAK),
551        TokenType::Assert => Some(&ASSERT),
552        TokenType::Trust => Some(&TRUST),
553        TokenType::Increase => Some(&INCREASE),
554        TokenType::Decrease => Some(&DECREASE),
555        TokenType::Spawn => Some(&SPAWN),
556        TokenType::Merge => Some(&MERGE),
557
558        // No lesson (yet): block headers teach through `doc_for_block`;
559        // everything else is either structural, symbolic, or a word whose
560        // meaning the sentence around it carries.
561        TokenType::BlockHeader { .. }
562        | TokenType::All
563        | TokenType::No
564        | TokenType::Some
565        | TokenType::Any
566        | TokenType::Both
567        | TokenType::Most
568        | TokenType::Few
569        | TokenType::Many
570        | TokenType::Cardinal(_)
571        | TokenType::AtLeast(_)
572        | TokenType::AtMost(_)
573        | TokenType::Anything
574        | TokenType::Anyone
575        | TokenType::Nothing
576        | TokenType::Nobody
577        | TokenType::NoOne
578        | TokenType::Nowhere
579        | TokenType::Ever
580        | TokenType::Never
581        | TokenType::And
582        | TokenType::Or
583        | TokenType::Then
584        | TokenType::Not
585        | TokenType::Iff
586        | TokenType::Because
587        | TokenType::Although
588        | TokenType::Until
589        | TokenType::Release
590        | TokenType::WeakUntil
591        | TokenType::Implies
592        | TokenType::Must
593        | TokenType::Shall
594        | TokenType::Should
595        | TokenType::Can
596        | TokenType::May
597        | TokenType::Cannot
598        | TokenType::Would
599        | TokenType::Could
600        | TokenType::Might
601        | TokenType::Had
602        | TokenType::Be
603        | TokenType::For
604        | TokenType::In
605        | TokenType::From
606        | TokenType::Require
607        | TokenType::Requires
608        | TokenType::Ensures
609        | TokenType::Otherwise
610        | TokenType::Else
611        | TokenType::Elif
612        | TokenType::Either
613        | TokenType::Native
614        | TokenType::EscapeBlock(_)
615        | TokenType::Given
616        | TokenType::Prove
617        | TokenType::Auto
618        | TokenType::Read
619        | TokenType::Write
620        | TokenType::Console
621        | TokenType::File
622        | TokenType::Copy
623        | TokenType::Through
624        | TokenType::Length
625        | TokenType::At
626        | TokenType::Contains
627        | TokenType::Union
628        | TokenType::Intersection
629        | TokenType::Inside
630        | TokenType::Zone
631        | TokenType::Called
632        | TokenType::Size
633        | TokenType::Mapped
634        | TokenType::Attempt
635        | TokenType::Following
636        | TokenType::Simultaneously
637        | TokenType::Send
638        | TokenType::Await
639        | TokenType::Portable
640        | TokenType::Manifest
641        | TokenType::Chunk
642        | TokenType::Shared
643        | TokenType::Tally
644        | TokenType::SharedSet
645        | TokenType::SharedSequence
646        | TokenType::CollaborativeSequence
647        | TokenType::SharedMap
648        | TokenType::Divergent
649        | TokenType::Append
650        | TokenType::Resolve
651        | TokenType::RemoveWins
652        | TokenType::AddWins
653        | TokenType::YATA
654        | TokenType::Values
655        | TokenType::Listen
656        | TokenType::NetConnect
657        | TokenType::Sleep
658        | TokenType::Sync
659        | TokenType::Mount
660        | TokenType::Persistent
661        | TokenType::Combined
662        | TokenType::Followed
663        | TokenType::Launch
664        | TokenType::Task
665        | TokenType::Pipe
666        | TokenType::Receive
667        | TokenType::Stop
668        | TokenType::Try
669        | TokenType::Into
670        | TokenType::First
671        | TokenType::After
672        | TokenType::Colon
673        | TokenType::Indent
674        | TokenType::Dedent
675        | TokenType::Newline
676        | TokenType::Noun(_)
677        | TokenType::Adjective(_)
678        | TokenType::NonIntersectiveAdjective(_)
679        | TokenType::Adverb(_)
680        | TokenType::ScopalAdverb(_)
681        | TokenType::TemporalAdverb(_)
682        | TokenType::Verb { .. }
683        | TokenType::ProperName(_)
684        | TokenType::Ambiguous { .. }
685        | TokenType::Performative(_)
686        | TokenType::Exclamation
687        | TokenType::Article(_)
688        | TokenType::Auxiliary(_)
689        | TokenType::Is
690        | TokenType::Are
691        | TokenType::Was
692        | TokenType::Were
693        | TokenType::That
694        | TokenType::Who
695        | TokenType::What
696        | TokenType::Where
697        | TokenType::Whose
698        | TokenType::When
699        | TokenType::Why
700        | TokenType::Does
701        | TokenType::Do
702        | TokenType::Identity
703        | TokenType::Equals
704        | TokenType::Reflexive
705        | TokenType::Reciprocal
706        | TokenType::Respectively
707        | TokenType::Pronoun { .. }
708        | TokenType::Preposition(_)
709        | TokenType::Particle(_)
710        | TokenType::Comparative(_)
711        | TokenType::Superlative(_)
712        | TokenType::Than
713        | TokenType::To
714        | TokenType::PresupTrigger(_)
715        | TokenType::Focus(_)
716        | TokenType::Measure(_)
717        | TokenType::Number(_)
718        | TokenType::MoneyLiteral { .. }
719        | TokenType::DurationLiteral { .. }
720        | TokenType::DateLiteral { .. }
721        | TokenType::TimeLiteral { .. }
722        | TokenType::CalendarUnit(_)
723        | TokenType::Ago
724        | TokenType::Hence
725        | TokenType::Before
726        | TokenType::StringLiteral(_)
727        | TokenType::InterpolatedString(_)
728        | TokenType::CharLiteral(_)
729        | TokenType::Item
730        | TokenType::Items
731        | TokenType::Possessive
732        | TokenType::LParen
733        | TokenType::RParen
734        | TokenType::LBracket
735        | TokenType::RBracket
736        | TokenType::LBrace
737        | TokenType::Amp
738        | TokenType::VBar
739        | TokenType::Tilde
740        | TokenType::Caret
741        | TokenType::RBrace
742        | TokenType::Comma
743        | TokenType::Period
744        | TokenType::Dot
745        | TokenType::Xor
746        | TokenType::Shifted
747        | TokenType::Plus
748        | TokenType::Minus
749        | TokenType::Star
750        | TokenType::Slash
751        | TokenType::Percent
752        | TokenType::PlusEq
753        | TokenType::MinusEq
754        | TokenType::StarEq
755        | TokenType::SlashEq
756        | TokenType::PercentEq
757        | TokenType::StarStar
758        | TokenType::SlashSlash
759        | TokenType::Lt
760        | TokenType::Gt
761        | TokenType::LtEq
762        | TokenType::GtEq
763        | TokenType::EqEq
764        | TokenType::NotEq
765        | TokenType::Arrow
766        | TokenType::Assign
767        | TokenType::Mut
768        | TokenType::Identifier
769        | TokenType::EOF => None,
770    }
771}
772
773/// The lesson for a `##` block header. TOTAL — every block type teaches, and
774/// a new `BlockType` variant does not compile until it gets a lesson.
775pub fn doc_for_block(block: &BlockType) -> &'static ConstructDoc {
776    match block {
777        BlockType::SuspectedTypo { .. } => &BLOCK_SUSPECTED_TYPO,
778        BlockType::Theorem => &BLOCK_THEOREM,
779        BlockType::Main => &BLOCK_MAIN,
780        BlockType::Definition => &BLOCK_DEFINITION,
781        BlockType::Define => &BLOCK_DEFINE,
782        BlockType::Axiom => &BLOCK_AXIOM,
783        BlockType::Theory => &BLOCK_THEORY,
784        BlockType::Proof => &BLOCK_PROOF,
785        BlockType::Example => &BLOCK_EXAMPLE,
786        BlockType::Logic => &BLOCK_LOGIC,
787        BlockType::Note => &BLOCK_NOTE,
788        BlockType::Function => &BLOCK_FUNCTION,
789        BlockType::TypeDef => &BLOCK_TYPEDEF,
790        BlockType::Policy => &BLOCK_POLICY,
791        BlockType::Requires => &BLOCK_REQUIRES,
792        BlockType::Hardware => &BLOCK_HARDWARE,
793        BlockType::Property => &BLOCK_PROPERTY,
794        BlockType::No => &BLOCK_NO,
795        BlockType::Tier => &BLOCK_TIER,
796    }
797}
798
799/// The lesson for a primitive or built-in generic type name.
800pub fn doc_for_primitive(name: &str) -> Option<&'static ConstructDoc> {
801    match name {
802        "Int" => Some(&TY_INT),
803        "Nat" => Some(&TY_NAT),
804        "Text" => Some(&TY_TEXT),
805        "Bool" => Some(&TY_BOOL),
806        "Float" => Some(&TY_FLOAT),
807        "Unit" => Some(&TY_UNIT),
808        "Char" => Some(&TY_CHAR),
809        "Byte" => Some(&TY_BYTE),
810        "List" => Some(&TY_LIST),
811        "Seq" => Some(&TY_SEQ),
812        "Map" => Some(&TY_MAP),
813        "Set" => Some(&TY_SET),
814        "Option" => Some(&TY_OPTION),
815        "Result" => Some(&TY_RESULT),
816        _ => None,
817    }
818}
819
820// ---------------------------------------------------------------------------
821// Literate-doc extraction — the prose → documentation pipeline
822// ---------------------------------------------------------------------------
823
824/// One documented definition pulled from a literate LOGOS module.
825pub struct LiterateDoc {
826    /// The defined name (`read`, `Point`).
827    pub name: String,
828    /// The full `##` header line, verbatim.
829    pub signature: String,
830    /// The body of the `## Note` block directly above the header, when one
831    /// exists. Notes are the ONLY per-definition doc carrier — bare prose
832    /// between sections is not literate LOGOS.
833    pub doc: Option<String>,
834}
835
836/// The module-level documentation: the prose between the `# Title` line and
837/// the first `##` section (the region the lexer skips).
838pub fn module_doc(source: &str) -> Option<String> {
839    let first_section = if source.starts_with("## ") {
840        0
841    } else {
842        source.find("\n## ").map(|i| i + 1).unwrap_or(source.len())
843    };
844    let prose: Vec<&str> = source[..first_section]
845        .lines()
846        .map(str::trim)
847        .filter(|l| !l.is_empty() && !l.starts_with('#'))
848        .collect();
849    (!prose.is_empty()).then(|| prose.join("\n"))
850}
851
852/// The documentation for the `##` header starting at `header_start`: the body
853/// of a `## Note` block IMMEDIATELY above it (the nearest preceding header
854/// must be the Note — any other header in between means no doc).
855pub fn doc_for_header_at(source: &str, header_start: usize) -> Option<String> {
856    let head = source.get(..header_start)?;
857    let mut nearest_header: Option<usize> = None;
858    let mut offset = 0;
859    for line in head.split_inclusive('\n') {
860        if line.trim_start().starts_with("## ") {
861            nearest_header = Some(offset);
862        }
863        offset += line.len();
864    }
865    let note_start = nearest_header?;
866    let note_line_end = note_start + head[note_start..].find('\n')?;
867    if head[note_start..note_line_end].trim() != "## Note" {
868        return None;
869    }
870    let body = head[note_line_end + 1..].trim();
871    (!body.is_empty()).then(|| body.to_string())
872}
873
874/// Every `## To …` / `## A … ` definition in a literate module, with its
875/// `## Note` documentation attached where one sits directly above. Types
876/// declared inside a `## Definition` body inherit the block's Note.
877pub fn extract_literate_docs(source: &str) -> Vec<LiterateDoc> {
878    let mut docs = Vec::new();
879    let mut offset = 0;
880    let mut definition_doc: Option<Option<String>> = None;
881    for line in source.split_inclusive('\n') {
882        let header = line.trim_end().trim_start();
883        if header.starts_with("## ") {
884            definition_doc =
885                (header == "## Definition").then(|| doc_for_header_at(source, offset));
886        }
887        if let Some(name) = literate_definition_name(header) {
888            docs.push(LiterateDoc {
889                name,
890                signature: header.to_string(),
891                doc: doc_for_header_at(source, offset),
892            });
893        } else if let Some(block_doc) = &definition_doc {
894            if let Some(name) = definition_body_type_name(header) {
895                docs.push(LiterateDoc {
896                    name,
897                    signature: header.to_string(),
898                    doc: block_doc.clone(),
899                });
900            }
901        }
902        offset += line.len();
903    }
904    docs
905}
906
907/// The type a `## Definition` BODY line declares: `A <Name> has …` /
908/// `A <Name> is …` (mirrors the loader's type-header rule).
909fn definition_body_type_name(line: &str) -> Option<String> {
910    let rest = line.strip_prefix("A ").or_else(|| line.strip_prefix("An "))?;
911    let word = rest.split(|c: char| c == '(' || c == '.' || c.is_whitespace()).next()?;
912    if !word.chars().next().is_some_and(|c| c.is_ascii_uppercase()) {
913        return None;
914    }
915    let tail = rest[word.len()..].trim_start();
916    (tail.starts_with("has") || tail.starts_with("is") || tail.starts_with("of"))
917        .then(|| word.to_string())
918}
919
920/// The name a `##` definition header defines, mirroring the loader's
921/// trigger-name rules: `## To [native] <name>` and `## A/An <TypeName> …`.
922fn literate_definition_name(header: &str) -> Option<String> {
923    if let Some(rest) = header.strip_prefix("## To ") {
924        let rest = rest.strip_prefix("native ").unwrap_or(rest);
925        let name = rest.split(|c: char| c == '(' || c.is_whitespace()).next()?;
926        return (!name.is_empty()).then(|| name.to_string());
927    }
928    let rest = header.strip_prefix("## A ").or_else(|| header.strip_prefix("## An "))?;
929    let word = rest
930        .split(|c: char| c == '(' || c == '.' || c == ':' || c.is_whitespace())
931        .next()?;
932    word.chars()
933        .next()
934        .is_some_and(|c| c.is_ascii_uppercase())
935        .then(|| word.to_string())
936}
937
938/// Every lesson whose name matches the word, case-insensitively — a word can
939/// name more than one construct (`Set` the statement, `Set` the type), and an
940/// honest teacher shows both.
941pub fn docs_for_word(word: &str) -> Vec<&'static ConstructDoc> {
942    ALL_DOCS
943        .iter()
944        .filter(|doc| doc.name.eq_ignore_ascii_case(word))
945        .copied()
946        .collect()
947}
948
949/// The first lesson whose name matches the word, case-insensitively.
950pub fn doc_for_word(word: &str) -> Option<&'static ConstructDoc> {
951    docs_for_word(word).into_iter().next()
952}
logicaffeine_language/teach.rs

logicaffeine_language/
teach.rs
