logicaffeine_lsp/
hover.rs

1use tower_lsp::lsp_types::{Hover, HoverContents, MarkupContent, MarkupKind, Position, Range};
2
3use logicaffeine_compile::analysis::VarState;
4use logicaffeine_language::token::{BlockType, TokenType};
5
6use crate::document::DocumentState;
7
8/// Handle hover request.
9///
10/// Shows type info, signatures, and keyword documentation depending on
11/// what's under the cursor.
12pub fn hover(doc: &DocumentState, position: Position) -> Option<Hover> {
13    let offset = doc.line_index.offset(position);
14
15    // Find the token at the cursor position
16    let token = doc.tokens.iter().find(|t| {
17        offset >= t.span.start && offset < t.span.end
18    })?;
19
20    let text = doc.source.get(token.span.start..token.span.end)?;
21
22    let content = match &token.kind {
23        // Block headers → the shared lesson table (total over BlockType),
24        // plus the socratic proof-strategy hint on theorems.
25        TokenType::BlockHeader { block_type } => {
26            let lesson = logicaffeine_language::teach::doc_for_block(block_type);
27            let mut result = crate::teach_md::block_hover_md(lesson);
28
29            if *block_type == BlockType::Theorem {
30                let hint = proof_strategy_hint_from_source(&doc.source, token.span.start);
31                result.push_str(&format!("\n\n---\n\n**Proof Strategy**: {}", hint));
32            }
33
34            Some(result)
35        }
36
37        // Taught keywords → the shared lesson table (one brain for hover,
38        // completion docs, and the REPL's :explain).
39        kind if logicaffeine_language::teach::doc_for(kind).is_some() => {
40            logicaffeine_language::teach::doc_for(kind).map(crate::teach_md::keyword_hover_md)
41        }
42
43        // Identifiers, proper names, adjectives, nouns → look up definition
44        // info first (detail + literate doc), then the stdlib registry.
45        TokenType::Identifier | TokenType::ProperName(_)
46        | TokenType::Adjective(_) | TokenType::Noun(_) => {
47            let defs = doc.symbol_index.definitions_of(text);
48            if let Some(def) = defs.first() {
49                definition_hover(def)
50            } else if let Some(entry) = crate::stdlib_docs::stdlib_doc(text) {
51                Some(crate::stdlib_docs::hover_md(text, entry))
52            } else {
53                // Fall back to token-specific info
54                match &token.kind {
55                    TokenType::Noun(sym) => {
56                        Some(format!("**Noun**: {}", doc.interner.resolve(*sym)))
57                    }
58                    TokenType::Adjective(sym) => {
59                        Some(format!("**Adjective**: {}", doc.interner.resolve(*sym)))
60                    }
61                    _ => None,
62                }
63            }
64        }
65
66        // Verbs → a defined function first (English-word function names lex
67        // as verbs), then the stdlib registry, then the verb-class display.
68        TokenType::Verb { lemma, time, aspect, class } => {
69            let defs = doc.symbol_index.definitions_of(text);
70            if let Some(def) = defs.first() {
71                definition_hover(def)
72            } else if let Some(entry) = crate::stdlib_docs::stdlib_doc(text) {
73                Some(crate::stdlib_docs::hover_md(text, entry))
74            } else {
75                let lemma_str = doc.interner.resolve(*lemma);
76                Some(format!(
77                    "**Verb**: {} ({}, {}, {})",
78                    lemma_str,
79                    verb_class_display(class),
80                    time_display(time),
81                    aspect_display(aspect),
82                ))
83            }
84        }
85
86        // Type names → look up in registry
87        _ => {
88            // Check if this is a type name
89            if let Some(sym) = doc.interner.lookup(text) {
90                if let Some(typedef) = doc.type_registry.get(sym) {
91                    Some(format_typedef(text, typedef, &doc.interner))
92                } else {
93                    None
94                }
95            } else {
96                None
97            }
98        }
99    };
100
101    let token_range = Range {
102        start: doc.line_index.position(token.span.start),
103        end: doc.line_index.position(token.span.end),
104    };
105
106    // Enrich with ownership state and diagnostics for variable-like tokens
107    let content = content.map(|mut c| {
108        if matches!(
109            &token.kind,
110            TokenType::Identifier | TokenType::ProperName(_)
111            | TokenType::Adjective(_) | TokenType::Noun(_)
112        ) {
113            // Ownership state
114            if let Some(state) = doc.ownership_states.get(text) {
115                let state_str = match state {
116                    VarState::Owned => "Owned",
117                    VarState::Moved => "Moved",
118                    VarState::MaybeMoved => "Maybe Moved",
119                    VarState::Borrowed => "Borrowed",
120                };
121                c.push_str(&format!("\n\n**Ownership**: {}", state_str));
122                match state {
123                    VarState::Moved => {
124                        c.push_str("\n\n*This variable has been given away and can no longer be used.*");
125                    }
126                    VarState::MaybeMoved => {
127                        c.push_str("\n\n*This variable might have been given away in a conditional branch.*");
128                    }
129                    _ => {}
130                }
131            }
132
133            // Diagnostics affecting this token
134            let affecting: Vec<_> = doc.diagnostics.iter()
135                .filter(|d| ranges_overlap(&token_range, &d.range))
136                .collect();
137            if !affecting.is_empty() {
138                c.push_str("\n\n---\n");
139                for diag in affecting.iter().take(3) {
140                    let first_line = diag.message.lines().next().unwrap_or(&diag.message);
141                    c.push_str(&format!("\n**Diagnostic**: {}", first_line));
142                }
143            }
144        }
145        c
146    });
147
148    content.map(|c| Hover {
149        contents: HoverContents::Markup(MarkupContent {
150            kind: MarkupKind::Markdown,
151            value: c,
152        }),
153        range: Some(token_range),
154    })
155}
156
157fn verb_class_display(class: &logicaffeine_language::lexicon::VerbClass) -> &'static str {
158    match class {
159        logicaffeine_language::lexicon::VerbClass::State => "state",
160        logicaffeine_language::lexicon::VerbClass::Activity => "activity",
161        logicaffeine_language::lexicon::VerbClass::Accomplishment => "accomplishment",
162        logicaffeine_language::lexicon::VerbClass::Achievement => "achievement",
163        logicaffeine_language::lexicon::VerbClass::Semelfactive => "semelfactive",
164    }
165}
166
167fn time_display(time: &logicaffeine_language::lexicon::Time) -> &'static str {
168    match time {
169        logicaffeine_language::lexicon::Time::Past => "past",
170        logicaffeine_language::lexicon::Time::Present => "present",
171        logicaffeine_language::lexicon::Time::Future => "future",
172        logicaffeine_language::lexicon::Time::None => "none",
173    }
174}
175
176fn aspect_display(aspect: &logicaffeine_language::lexicon::Aspect) -> &'static str {
177    match aspect {
178        logicaffeine_language::lexicon::Aspect::Simple => "simple",
179        logicaffeine_language::lexicon::Aspect::Progressive => "progressive",
180        logicaffeine_language::lexicon::Aspect::Perfect => "perfect",
181    }
182}
183
184/// A definition's hover: its signature detail plus its literate `## Note`
185/// documentation, when either exists.
186fn definition_hover(def: &crate::index::Definition) -> Option<String> {
187    match (&def.detail, &def.doc) {
188        (Some(detail), Some(doc)) => Some(format!("{detail}\n\n{doc}")),
189        (Some(detail), None) => Some(detail.clone()),
190        (None, Some(doc)) => Some(doc.clone()),
191        (None, None) => None,
192    }
193}
194
195fn ranges_overlap(a: &Range, b: &Range) -> bool {
196    !(a.end.line < b.start.line
197        || (a.end.line == b.start.line && a.end.character < b.start.character)
198        || b.end.line < a.start.line
199        || (b.end.line == a.start.line && b.end.character < a.start.character))
200}
201
202fn format_typedef(
203    name: &str,
204    typedef: &logicaffeine_language::analysis::TypeDef,
205    interner: &logicaffeine_base::Interner,
206) -> String {
207    match typedef {
208        logicaffeine_language::analysis::TypeDef::Struct { fields, .. } => {
209            let mut s = format!("**struct** {}\n\n", name);
210            for field in fields {
211                let field_name = interner.resolve(field.name);
212                let field_type = format_field_type(&field.ty, interner);
213                s.push_str(&format!("- `{}`: {}\n", field_name, field_type));
214            }
215            s
216        }
217        logicaffeine_language::analysis::TypeDef::Enum { variants, .. } => {
218            let mut s = format!("**enum** {}\n\n", name);
219            for variant in variants {
220                let variant_name = interner.resolve(variant.name);
221                if variant.fields.is_empty() {
222                    s.push_str(&format!("- `{}`\n", variant_name));
223                } else {
224                    let fields: Vec<String> = variant
225                        .fields
226                        .iter()
227                        .map(|f| {
228                            format!(
229                                "{}: {}",
230                                interner.resolve(f.name),
231                                format_field_type(&f.ty, interner)
232                            )
233                        })
234                        .collect();
235                    s.push_str(&format!("- `{}` with {}\n", variant_name, fields.join(", ")));
236                }
237            }
238            s
239        }
240        logicaffeine_language::analysis::TypeDef::Primitive => {
241            format!("**primitive** {}", name)
242        }
243        logicaffeine_language::analysis::TypeDef::Generic { param_count } => {
244            format!("**generic** {} (takes {} type parameter(s))", name, param_count)
245        }
246        logicaffeine_language::analysis::TypeDef::Alias { target } => {
247            format!("**alias** {} = {}", name, interner.resolve(*target))
248        }
249    }
250}
251
252#[cfg(test)]
253mod tests {
254    use super::*;
255    use crate::document::DocumentState;
256
257    fn make_doc(source: &str) -> DocumentState {
258        DocumentState::new(source.to_string(), 1)
259    }
260
261    #[test]
262    fn hover_on_keyword_shows_docs() {
263        let doc = make_doc("## Main\n    Let x be 5.\n");
264        // Position on "Let" (line 1, character 4)
265        let pos = Position { line: 1, character: 4 };
266        let result = hover(&doc, pos);
267        assert!(result.is_some(), "Expected hover info for 'Let'");
268        let h = result.unwrap();
269        match &h.contents {
270            HoverContents::Markup(m) => {
271                assert!(m.value.contains("Let"), "Hover should mention 'Let': {}", m.value);
272                assert!(m.value.contains("variable"), "Hover should describe variable declaration: {}", m.value);
273            }
274            _ => panic!("Expected markup content"),
275        }
276    }
277
278    #[test]
279    fn hover_on_variable_shows_definition() {
280        let doc = make_doc("## Main\n    Let x be 5.\n    Show x.\n");
281        let pos = Position { line: 2, character: 9 };
282        let result = hover(&doc, pos);
283        assert!(result.is_some(), "Expected hover info for variable 'x'");
284        let h = result.unwrap();
285        match &h.contents {
286            HoverContents::Markup(m) => {
287                assert!(m.value.contains("Let") || m.value.contains("x"),
288                    "Variable hover should contain 'Let' or 'x': {}", m.value);
289            }
290            _ => panic!("Expected markup content"),
291        }
292    }
293
294    #[test]
295    fn hover_on_block_header() {
296        let doc = make_doc("## Main\n    Let x be 5.\n");
297        let pos = Position { line: 0, character: 0 };
298        let result = hover(&doc, pos);
299        assert!(result.is_some(), "Expected hover for block header");
300        let h = result.unwrap();
301        match &h.contents {
302            HoverContents::Markup(m) => {
303                assert!(
304                    m.value.contains("Block Header") || m.value.contains("entry point"),
305                    "Expected block header info: {}",
306                    m.value
307                );
308            }
309            _ => panic!("Expected markup content"),
310        }
311    }
312
313    #[test]
314    fn hover_whitespace_returns_none() {
315        let doc = make_doc("## Main\n    Let x be 5.\n");
316        let pos = Position { line: 0, character: 50 };
317        let result = hover(&doc, pos);
318        assert!(result.is_none(), "Hover on whitespace/OOB should return None");
319    }
320
321    #[test]
322    fn hover_returns_correct_range() {
323        let doc = make_doc("## Main\n    Let x be 5.\n    Show x.\n");
324        let pos = Position { line: 2, character: 9 };
325        let result = hover(&doc, pos);
326        assert!(result.is_some());
327        let h = result.unwrap();
328        assert!(h.range.is_some(), "Hover should include a range");
329        let range = h.range.unwrap();
330        assert_eq!(range.start.line, 2, "Hover range should be on line 2");
331    }
332
333    #[test]
334    fn hover_verb_shows_lowercase_class() {
335        // Verb hover should show lowercase class/time/aspect, not Debug format
336        let _doc = make_doc("## Main\n    Let x be 5.\n");
337        assert_eq!(verb_class_display(&logicaffeine_language::lexicon::VerbClass::Activity), "activity");
338        assert_eq!(verb_class_display(&logicaffeine_language::lexicon::VerbClass::State), "state");
339        assert_eq!(verb_class_display(&logicaffeine_language::lexicon::VerbClass::Accomplishment), "accomplishment");
340        assert_eq!(verb_class_display(&logicaffeine_language::lexicon::VerbClass::Achievement), "achievement");
341        assert_eq!(verb_class_display(&logicaffeine_language::lexicon::VerbClass::Semelfactive), "semelfactive");
342        assert_eq!(time_display(&logicaffeine_language::lexicon::Time::Past), "past");
343        assert_eq!(time_display(&logicaffeine_language::lexicon::Time::Present), "present");
344        assert_eq!(time_display(&logicaffeine_language::lexicon::Time::Future), "future");
345        assert_eq!(time_display(&logicaffeine_language::lexicon::Time::None), "none");
346        assert_eq!(aspect_display(&logicaffeine_language::lexicon::Aspect::Simple), "simple");
347        assert_eq!(aspect_display(&logicaffeine_language::lexicon::Aspect::Progressive), "progressive");
348        assert_eq!(aspect_display(&logicaffeine_language::lexicon::Aspect::Perfect), "perfect");
349    }
350
351    #[test]
352    fn hover_set_keyword_docs() {
353        let doc = make_doc("## Main\n    Let x be 5.\n    Set x to 10.\n");
354        // Position on "Set" keyword (line 2, character 4)
355        let pos = Position { line: 2, character: 4 };
356        let result = hover(&doc, pos);
357        assert!(result.is_some(), "Expected hover for 'Set' keyword");
358        let h = result.unwrap();
359        match &h.contents {
360            HoverContents::Markup(m) => {
361                assert!(m.value.contains("Updates") || m.value.contains("Set"),
362                    "Set hover should contain 'Updates': {}", m.value);
363            }
364            _ => panic!("Expected markup content"),
365        }
366    }
367
368    #[test]
369    fn hover_shows_the_notes_prose_for_a_documented_function() {
370        let doc = make_doc(
371            "## Note\nDoubles a number.\n\n## To double (n: Int) -> Int:\n    Return n * 2.\n\n## Main\nLet x be double(3).\n",
372        );
373        // Hover over "double" at the call site (line 7).
374        let pos = Position { line: 7, character: 10 };
375        let result = hover(&doc, pos).expect("hover on documented call");
376        let HoverContents::Markup(m) = &result.contents else { panic!("expected markup") };
377        assert!(
378            m.value.contains("double"),
379            "the signature detail renders: {}",
380            m.value
381        );
382        assert!(
383            m.value.contains("Doubles a number."),
384            "the ## Note prose renders: {}",
385            m.value
386        );
387    }
388
389    #[test]
390    fn hover_teaches_stdlib_names_from_their_literate_docs() {
391        let doc = make_doc("## Main\nLet d be md5([1]).\n");
392        // Hover over "md5" (line 1, character 9).
393        let pos = Position { line: 1, character: 9 };
394        let result = hover(&doc, pos).expect("hover on a stdlib name");
395        let HoverContents::Markup(m) = &result.contents else { panic!("expected markup") };
396        assert!(m.value.contains("standard library"), "{}", m.value);
397        assert!(m.value.contains("MD5"), "the literate Note teaches: {}", m.value);
398    }
399
400    #[test]
401    fn hover_keyword_carries_the_full_lesson() {
402        let doc = make_doc("## Main\n    Let x be 5.\n    Let y be 0.\n    Give x to y.\n");
403        // Position on "Give" (line 3, character 4).
404        let pos = Position { line: 3, character: 4 };
405        let result = hover(&doc, pos).expect("hover on 'Give'");
406        let HoverContents::Markup(m) = &result.contents else { panic!("expected markup") };
407        let lesson = logicaffeine_language::teach::doc_for(&TokenType::Give)
408            .expect("Give is a taught keyword");
409        assert!(
410            m.value.contains(lesson.what),
411            "Give hover must carry the lesson's `what`: {}",
412            m.value
413        );
414        assert!(
415            m.value.contains(lesson.question_or_tip),
416            "Give hover must carry the socratic question: {}",
417            m.value
418        );
419        assert!(
420            m.value.contains("LOGOS_QUICKGUIDE.md#"),
421            "Give hover must link the quickguide anchor: {}",
422            m.value
423        );
424    }
425
426    #[test]
427    fn hover_covers_newly_taught_keywords() {
428        let doc = make_doc("## Main\n    While true:\n        Break.\n");
429        // Position on "Break" (line 2, character 8).
430        let pos = Position { line: 2, character: 8 };
431        let result = hover(&doc, pos).expect("hover on 'Break' — newly taught");
432        let HoverContents::Markup(m) = &result.contents else { panic!("expected markup") };
433        assert!(
434            m.value.contains("innermost"),
435            "Break hover must teach the innermost-loop rule: {}",
436            m.value
437        );
438    }
439
440    #[test]
441    fn hover_block_header_carries_the_lesson_question() {
442        let doc = make_doc("## Main\n    Let x be 5.\n");
443        let pos = Position { line: 0, character: 0 };
444        let result = hover(&doc, pos).expect("hover on ## Main");
445        let HoverContents::Markup(m) = &result.contents else { panic!("expected markup") };
446        let lesson = logicaffeine_language::teach::doc_for_block(
447            &logicaffeine_language::token::BlockType::Main,
448        );
449        assert!(
450            m.value.contains("Block Header"),
451            "block hover keeps the Block Header banner: {}",
452            m.value
453        );
454        assert!(
455            m.value.contains(lesson.question_or_tip),
456            "block hover must carry the lesson's question or tip: {}",
457            m.value
458        );
459    }
460
461    #[test]
462    fn hover_theorem_shows_proof_hint() {
463        let doc = make_doc("## Theorem: all humans are mortal\n    All humans are mortal.\n");
464        // Hover on the block header "##" (line 0, character 0)
465        let pos = Position { line: 0, character: 0 };
466        let result = hover(&doc, pos);
467        assert!(result.is_some(), "Expected hover for Theorem block header");
468        let h = result.unwrap();
469        match &h.contents {
470            HoverContents::Markup(m) => {
471                assert!(
472                    m.value.contains("Proof Strategy"),
473                    "Theorem hover should include proof strategy hint: {}",
474                    m.value
475                );
476                assert!(
477                    m.value.contains("universal"),
478                    "Theorem with 'all' should suggest universal proof strategy: {}",
479                    m.value
480                );
481            }
482            _ => panic!("Expected markup content"),
483        }
484    }
485
486    #[test]
487    fn hover_theorem_implication_shows_strategy() {
488        let doc = make_doc("## Theorem: if it rains then ground is wet\n    If it rains then the ground is wet.\n");
489        let pos = Position { line: 0, character: 0 };
490        let result = hover(&doc, pos);
491        assert!(result.is_some(), "Expected hover for Theorem block");
492        let h = result.unwrap();
493        match &h.contents {
494            HoverContents::Markup(m) => {
495                assert!(
496                    m.value.contains("implication"),
497                    "Theorem with 'if' should suggest implication strategy: {}",
498                    m.value
499                );
500            }
501            _ => panic!("Expected markup content"),
502        }
503    }
504
505    #[test]
506    fn hover_owned_variable_shows_owned() {
507        let doc = make_doc("## Main\n    Let x be 5.\n    Show x.\n");
508        // Hover on "x" in "Show x." (line 2, character 9)
509        let pos = Position { line: 2, character: 9 };
510        let result = hover(&doc, pos);
511        assert!(result.is_some(), "Expected hover for 'x'");
512        let h = result.unwrap();
513        match &h.contents {
514            HoverContents::Markup(m) => {
515                assert!(
516                    m.value.contains("Ownership") && m.value.contains("Owned")
517                    || m.value.contains("Borrowed"),
518                    "Hover should show ownership state: {}",
519                    m.value
520                );
521            }
522            _ => panic!("Expected markup content"),
523        }
524    }
525
526    #[test]
527    fn hover_moved_variable_shows_ownership_state() {
528        // After Give, x is Moved. The parser may emit use-after-move, but
529        // the ownership state should still be Moved on the checker.
530        let doc = make_doc("## Main\n    Let x be 5.\n    Let y be 0.\n    Give x to y.\n    Show x.\n");
531        // Check that x has Moved state in ownership_states
532        if let Some(state) = doc.ownership_states.get("x") {
533            assert!(
534                matches!(state, VarState::Moved),
535                "x should be Moved after Give, got: {:?}",
536                state
537            );
538        }
539    }
540
541    #[test]
542    fn hover_borrowed_variable_shows_borrowed() {
543        let doc = make_doc("## Main\n    Let x be 5.\n    Show x.\n");
544        // After Show, x should be Borrowed (or still Owned)
545        if let Some(state) = doc.ownership_states.get("x") {
546            assert!(
547                matches!(state, VarState::Borrowed | VarState::Owned),
548                "x should be Borrowed or Owned after Show, got: {:?}",
549                state
550            );
551        }
552    }
553}
554
555/// Analyze the source text of a Theorem block to suggest a proof strategy.
556///
557/// Scans the block's body text for structural keywords (quantifiers, connectives)
558/// and returns a Socratic hint guiding the user toward the right tactic.
559fn proof_strategy_hint_from_source(source: &str, block_start: usize) -> String {
560    let block_text = &source[block_start..];
561    let block_end = block_text.find("\n## ").unwrap_or(block_text.len());
562    let block_body = &block_text[..block_end].to_lowercase();
563
564    if block_body.contains("for all") || block_body.contains("every") || block_body.contains("all ") {
565        return "Your theorem involves a universal claim. To prove it, consider an arbitrary element and show the property holds.".to_string();
566    }
567    if block_body.contains("there exists") || block_body.contains("some ") {
568        return "Your theorem involves an existential claim. You need to find a specific witness that satisfies the property.".to_string();
569    }
570    if block_body.contains(" implies ") || block_body.contains("if ") {
571        return "Your theorem is an implication. Try assuming the antecedent and proving the consequent.".to_string();
572    }
573    if block_body.contains(" and ") {
574        return "Your theorem is a conjunction. You need to prove both parts separately.".to_string();
575    }
576    if block_body.contains(" or ") {
577        return "Your theorem is a disjunction. You only need to prove one of the alternatives.".to_string();
578    }
579    if block_body.contains("not ") || block_body.contains("no ") {
580        return "Your theorem involves negation. Try assuming the positive form and deriving a contradiction.".to_string();
581    }
582    if block_body.contains("equals") || block_body.contains(" = ") {
583        return "Your theorem is an equality. Can you rewrite one side to match the other, or use reflexivity?".to_string();
584    }
585
586    "What logical structure does your theorem have? Try breaking it down into simpler parts.".to_string()
587}
588
589pub fn format_field_type(
590    ty: &logicaffeine_language::analysis::FieldType,
591    interner: &logicaffeine_base::Interner,
592) -> String {
593    match ty {
594        logicaffeine_language::analysis::FieldType::Primitive(sym) => {
595            interner.resolve(*sym).to_string()
596        }
597        logicaffeine_language::analysis::FieldType::Named(sym) => {
598            interner.resolve(*sym).to_string()
599        }
600        logicaffeine_language::analysis::FieldType::Generic { base, params } => {
601            let base_name = interner.resolve(*base);
602            let param_strs: Vec<String> = params
603                .iter()
604                .map(|p| format_field_type(p, interner))
605                .collect();
606            format!("{} of {}", base_name, param_strs.join(", "))
607        }
608        logicaffeine_language::analysis::FieldType::TypeParam(sym) => {
609            interner.resolve(*sym).to_string()
610        }
611    }
612}
logicaffeine_lsp/hover.rs

logicaffeine_lsp/
hover.rs
