logicaffeine_lsp/
code_lens.rs

1use tower_lsp::lsp_types::{CodeLens, Command, Range};
2
3use logicaffeine_language::token::BlockType;
4
5use crate::document::DocumentState;
6
7/// Handle code lens request.
8///
9/// Shows "Run" above ## Main blocks and "Verify" above ## Theorem blocks.
10/// Commands include the block name as an argument for the editor extension.
11pub fn code_lenses(doc: &DocumentState, uri: &tower_lsp::lsp_types::Url) -> Vec<CodeLens> {
12    let mut lenses = Vec::new();
13
14    for (name, block_type, span) in &doc.symbol_index.block_spans {
15        let range = Range {
16            start: doc.line_index.position(span.start),
17            end: doc.line_index.position(span.start),
18        };
19
20        let args = Some(vec![
21            serde_json::Value::String(uri.to_string()),
22            serde_json::Value::String(name.clone()),
23        ]);
24
25        match block_type {
26            BlockType::Main => {
27                lenses.push(CodeLens {
28                    range,
29                    command: Some(Command {
30                        title: "Run".to_string(),
31                        command: "logicaffeine.run".to_string(),
32                        arguments: args,
33                    }),
34                    data: None,
35                });
36            }
37            BlockType::Theorem => {
38                lenses.push(CodeLens {
39                    range,
40                    command: Some(Command {
41                        title: "Verify".to_string(),
42                        command: "logicaffeine.verify".to_string(),
43                        arguments: args.clone(),
44                    }),
45                    data: None,
46                });
47                lenses.push(CodeLens {
48                    range,
49                    command: Some(Command {
50                        title: "Prove".to_string(),
51                        command: "logicaffeine.prove".to_string(),
52                        arguments: args,
53                    }),
54                    data: None,
55                });
56            }
57            BlockType::Proof => {
58                lenses.push(CodeLens {
59                    range,
60                    command: Some(Command {
61                        title: "Check Proof".to_string(),
62                        command: "logicaffeine.checkProof".to_string(),
63                        arguments: args,
64                    }),
65                    data: None,
66                });
67            }
68            _ => {}
69        }
70    }
71
72    lenses
73}
74
75#[cfg(test)]
76mod tests {
77    use super::*;
78    use crate::document::DocumentState;
79
80    fn make_doc(source: &str) -> DocumentState {
81        DocumentState::new(source.to_string(), 1)
82    }
83
84    fn test_uri() -> tower_lsp::lsp_types::Url {
85        tower_lsp::lsp_types::Url::parse("file:///test.logos").unwrap()
86    }
87
88    #[test]
89    fn code_lens_for_main_block() {
90        let doc = make_doc("## Main\n    Let x be 5.\n");
91        let lenses = code_lenses(&doc, &test_uri());
92        let run_lenses: Vec<_> = lenses.iter().filter(|l| {
93            l.command.as_ref().map(|c| c.command == "logicaffeine.run").unwrap_or(false)
94        }).collect();
95        assert_eq!(run_lenses.len(), 1, "Expected exactly one 'Run' lens for ## Main");
96        assert_eq!(run_lenses[0].command.as_ref().unwrap().title, "Run");
97    }
98
99    #[test]
100    fn code_lens_empty_for_no_blocks() {
101        let doc = make_doc("");
102        let lenses = code_lenses(&doc, &test_uri());
103        assert!(lenses.is_empty(), "Empty doc should have no lenses");
104    }
105
106    #[test]
107    fn code_lens_note_block_no_lenses() {
108        let doc = make_doc("## Note: readme\n    Some docs here.\n");
109        let lenses = code_lenses(&doc, &test_uri());
110        let run_or_verify: Vec<_> = lenses.iter().filter(|l| {
111            l.command.as_ref().map(|c|
112                c.command == "logicaffeine.run" || c.command == "logicaffeine.verify"
113            ).unwrap_or(false)
114        }).collect();
115        assert!(run_or_verify.is_empty(),
116            "Note block should not have Run or Verify lenses, got {:?}",
117            run_or_verify.iter().map(|l| &l.command).collect::<Vec<_>>());
118    }
119
120    #[test]
121    fn code_lens_positioned_at_block_start() {
122        let doc = make_doc("## Main\n    Let x be 5.\n");
123        let lenses = code_lenses(&doc, &test_uri());
124        assert!(!lenses.is_empty());
125        assert_eq!(lenses[0].range.start.line, 0, "Lens should be on the block header line");
126    }
127
128    #[test]
129    fn code_lens_theorem_has_verify_and_prove() {
130        let doc = make_doc("## Theorem: all humans are mortal\n    All humans are mortal.\n");
131        let lenses = code_lenses(&doc, &test_uri());
132        let verify_lenses: Vec<_> = lenses.iter().filter(|l| {
133            l.command.as_ref().map(|c| c.command == "logicaffeine.verify").unwrap_or(false)
134        }).collect();
135        let prove_lenses: Vec<_> = lenses.iter().filter(|l| {
136            l.command.as_ref().map(|c| c.command == "logicaffeine.prove").unwrap_or(false)
137        }).collect();
138        assert_eq!(verify_lenses.len(), 1, "Theorem should have 'Verify' lens");
139        assert_eq!(prove_lenses.len(), 1, "Theorem should have 'Prove' lens");
140    }
141
142    #[test]
143    fn code_lens_proof_block_has_check() {
144        let doc = make_doc("## Proof\n    By assumption.\n");
145        let lenses = code_lenses(&doc, &test_uri());
146        let check_lenses: Vec<_> = lenses.iter().filter(|l| {
147            l.command.as_ref().map(|c| c.command == "logicaffeine.checkProof").unwrap_or(false)
148        }).collect();
149        assert_eq!(check_lenses.len(), 1, "Proof block should have 'Check Proof' lens");
150        assert_eq!(
151            check_lenses[0].command.as_ref().unwrap().title,
152            "Check Proof"
153        );
154    }
155
156    #[test]
157    fn run_lens_has_arguments() {
158        let doc = make_doc("## Main\n    Let x be 5.\n");
159        let uri = test_uri();
160        let lenses = code_lenses(&doc, &uri);
161        let run_lens = lenses.iter().find(|l| {
162            l.command.as_ref().map(|c| c.command == "logicaffeine.run").unwrap_or(false)
163        }).expect("Should have Run lens");
164        let args = run_lens.command.as_ref().unwrap().arguments.as_ref();
165        assert!(args.is_some(), "Run lens should have arguments");
166        let args = args.unwrap();
167        assert_eq!(args.len(), 2, "Should have URI and block name arguments");
168        assert_eq!(args[0].as_str().unwrap(), uri.as_str());
169    }
170}
logicaffeine_lsp/code_lens.rs

logicaffeine_lsp/
code_lens.rs
