diff --git a/Cargo.lock b/Cargo.lock index 27d7b99..afc44c1 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -751,6 +751,7 @@ version = "0.1.0" dependencies = [ "hexpr", "metacat", + "serde", "serde_json", "tokio", "tower-lsp", diff --git a/metacat-cli/src/main.rs b/metacat-cli/src/main.rs index da9eeba..1d6676f 100644 --- a/metacat-cli/src/main.rs +++ b/metacat-cli/src/main.rs @@ -143,7 +143,10 @@ fn check_one_theory(theory_id: &TheoryId, theory: &Theory) { log::info!("checking definitions in {}", theory_id); - for (operation, declaration) in arrows.iter().filter(|(_, arrow)| arrow.definition.is_some()) { + for (operation, declaration) in arrows + .iter() + .filter(|(_, arrow)| arrow.definition.is_some()) + { let mut term = declaration.definition.clone().unwrap(); let (source, target) = declaration.type_maps.clone(); log::info!("checking definition {} in {}", operation, theory_id); @@ -171,7 +174,10 @@ fn check_one_theory(theory_id: &TheoryId, theory: &Theory) { declaration.raw.type_maps.0, declaration.raw.type_maps.1 ); - println!("Checking '{} {}' failed: {}", theory_id, declaration.name, e); + println!( + "Checking '{} {}' failed: {}", + theory_id, declaration.name, e + ); } } } diff --git a/metacat-lsp/Cargo.toml b/metacat-lsp/Cargo.toml index 5ac6fef..32b0dc6 100644 --- a/metacat-lsp/Cargo.toml +++ b/metacat-lsp/Cargo.toml @@ -14,6 +14,7 @@ path = "src/main.rs" [dependencies] hexpr = { workspace = true } metacat = { version = "0.2.2", path = "../metacat" } +serde = { version = "1.0.228", features = ["derive"] } serde_json = "1.0.150" tokio = { workspace = true, features = ["io-std", "macros", "rt-multi-thread"] } tower-lsp = { workspace = true } diff --git a/metacat-lsp/src/analysis.rs b/metacat-lsp/src/analysis.rs index c6ca33e..824f218 100644 --- a/metacat-lsp/src/analysis.rs +++ b/metacat-lsp/src/analysis.rs @@ -1,6 +1,8 @@ use hexpr::Operation; -use metacat::check::check; -use metacat::theory::{Theory, TheoryId, TheorySet}; +use metacat::check::{check, eval_type}; +use metacat::theory::{Term, Theory, TheoryId, TheorySet}; +use metacat::{dual, tree::Tree}; +use std::collections::BTreeMap; use crate::syntax::PortSide; @@ -110,6 +112,137 @@ pub fn checked_definition_operation_label( )) } +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct ArrowSpanLabel { + pub source: String, + pub target: String, + pub source_metavariable_count: usize, + pub target_metavariable_count: usize, + pub error: Option, +} + +pub fn arrow_span_label( + theories: &TheorySet, + theory_name: &str, + arrow_name: &str, +) -> Option { + let theory_id = TheoryId(theory_name.parse().ok()?); + let theory = theories.theories.get(&theory_id)?; + let Theory::Theory { syntax, arrows } = theory else { + return None; + }; + let syntax_theory = theories.theories.get(syntax)?; + let arrow_op: Operation = arrow_name.parse().ok()?; + let declaration = arrows.get(&arrow_op)?; + let (source, target) = &declaration.type_maps; + + let source_metavariable_count = source.sources.len(); + let target_metavariable_count = target.sources.len(); + let error = (source_metavariable_count != target_metavariable_count).then(|| { + format!( + "Source and target terms have different metavariable counts: source has {}, target has {}.", + source_metavariable_count, target_metavariable_count + ) + }); + + Some(ArrowSpanLabel { + source: format_type_map_term(source, syntax_theory)?, + target: format_type_map_term(target, syntax_theory)?, + source_metavariable_count, + target_metavariable_count, + error, + }) +} + +fn format_type_map_term(term: &Term, syntax_theory: &Theory) -> Option { + let mut term = dual::into_fwd(term.clone()); + term.quotient().ok()?; + let targets = term.targets.iter().map(|node| node.0).collect::>(); + let sources = term.sources.iter().map(|node| node.0).collect::>(); + let labels = eval_type(term).ok()?; + let boundary = targets + .iter() + .map(|node| pretty_tree(labels.get(*node)?, syntax_theory)) + .collect::>>()?; + Some(replace_source_leaves( + &format_wire_list(&boundary), + &sources, + )) +} + +fn pretty_tree(tree: &Tree<(), Operation>, syntax_theory: &Theory) -> Option { + tree.try_pretty(Some(&|op: &Operation| { + syntax_theory.coarity_of(op).ok_or(()) + })) + .ok() +} + +fn replace_source_leaves(text: &str, sources: &[usize]) -> String { + let replacements = sources + .iter() + .enumerate() + .map(|(index, node)| (format!("x{}", node), format!("m{}", index))) + .collect::>(); + replace_tokens(text, &replacements) +} + +fn replace_tokens(text: &str, replacements: &BTreeMap) -> String { + let mut result = String::new(); + let mut offset = 0usize; + while offset < text.len() { + let Some(ch) = text.get(offset..).and_then(|slice| slice.chars().next()) else { + break; + }; + if !(ch == 'x' || ch == 'm') { + result.push(ch); + offset += ch.len_utf8(); + continue; + } + + let start = offset; + offset += ch.len_utf8(); + let digit_start = offset; + while offset < text.len() { + let Some(next) = text.get(offset..).and_then(|slice| slice.chars().next()) else { + break; + }; + if !next.is_ascii_digit() { + break; + } + offset += next.len_utf8(); + } + let candidate = &text[start..offset]; + if offset > digit_start + && is_pretty_token_start(text, start) + && is_pretty_token_end(text, offset) + && let Some(replacement) = replacements.get(candidate) + { + result.push_str(replacement); + } else { + result.push_str(candidate); + } + } + result +} + +fn is_pretty_token_start(text: &str, offset: usize) -> bool { + !text + .get(..offset) + .and_then(|prefix| prefix.chars().next_back()) + .is_some_and(is_pretty_token_char) +} + +fn is_pretty_token_end(text: &str, offset: usize) -> bool { + !text + .get(offset..) + .and_then(|suffix| suffix.chars().next()) + .is_some_and(is_pretty_token_char) +} + +fn is_pretty_token_char(ch: char) -> bool { + ch.is_ascii_alphanumeric() || matches!(ch, '_' | '-') +} + fn format_wire_list(labels: &[String]) -> String { match labels { [] => "1".to_string(), diff --git a/metacat-lsp/src/arrow_details.rs b/metacat-lsp/src/arrow_details.rs new file mode 100644 index 0000000..22fd721 --- /dev/null +++ b/metacat-lsp/src/arrow_details.rs @@ -0,0 +1,599 @@ +use std::collections::{BTreeMap, BTreeSet}; + +use hexpr::{Hexpr, Operation}; +use metacat::theory::ast::{RawTheory, RawTheorySet}; +use serde::{Deserialize, Serialize}; +use tower_lsp::lsp_types::{Position, Url}; + +use crate::analysis::{ArrowSpanLabel, arrow_span_label, theory_set_from_texts}; +use crate::syntax::{ + delimiter_stack_at, is_operation_char, matching_close_offset, offset_at_position, token_at, +}; + +#[derive(Clone, Debug, Deserialize)] +pub struct ArrowDetailsParams { + pub uri: Url, + pub position: Position, +} + +#[derive(Clone, Debug, Serialize)] +#[serde(rename_all = "camelCase")] +pub struct ArrowDetails { + pub declaration_kind: String, + pub name: String, + pub source: String, + pub target: String, + pub metavariables: Vec, + pub pretty_metavariables: Vec, + pub error: Option, +} + +#[derive(Clone, Debug)] +struct ArrowDeclaration { + start: usize, + end: usize, + declaration_kind: String, + theory: String, + name: crate::syntax::Token, + metavariables: Vec, + source_typevars: Vec, + target_typevars: Vec, +} + +pub fn arrow_details_at_position( + text: &str, + project_texts: &[String], + position: Position, +) -> Option { + let offset = offset_at_position(text, position)?; + let project_declarations = project_arrow_declarations(text, project_texts); + let declarations = scan_arrow_declarations(text); + let token = token_at(text, offset, is_operation_char); + let exact_declaration_name = declarations.iter().find(|declaration| { + token.as_ref().is_some_and(|token| { + token.text == declaration.name.text + && token.start >= declaration.name.start + && token.end <= declaration.name.end + }) + }); + let referenced_declaration = token + .as_ref() + .filter(|token| !matches!(token.text.as_str(), ":" | "->" | "=")) + .and_then(|token| { + definition_body_theory_at(text, token.start).and_then(|theory| { + project_declarations.iter().find(|declaration| { + declaration.theory == theory && declaration.name.text == token.text + }) + }) + }) + .or_else(|| { + declarations.iter().find(|declaration| { + token.as_ref().is_some_and(|token| { + token.text == declaration.name.text + && !matches!(token.text.as_str(), ":" | "->" | "=") + }) + }) + }); + let enclosing = declarations + .iter() + .find(|declaration| offset >= declaration.start && offset <= declaration.end); + let declaration = exact_declaration_name + .or(referenced_declaration) + .or(enclosing)?; + + let semantic = theory_set_from_texts(project_texts.iter().map(String::as_str)) + .and_then(|theories| { + arrow_span_label(&theories, &declaration.theory, &declaration.name.text) + }) + .or_else(|| partial_arrow_span_label(project_texts, declaration)); + let raw_error = raw_typevar_mismatch_error(declaration); + let span = semantic.or_else(|| raw_error.as_ref().map(|_| empty_span_label(declaration)))?; + let metavariable_count = span + .source_metavariable_count + .max(span.target_metavariable_count); + let metavariables = declaration + .metavariables + .iter() + .take(metavariable_count) + .cloned() + .collect::>(); + let pretty_metavariables = (0..metavariable_count) + .map(|index| format!("m{}", index)) + .collect::>(); + let error = raw_error.or(span.error); + + Some(ArrowDetails { + declaration_kind: declaration.declaration_kind.clone(), + name: declaration.name.text.clone(), + source: span.source, + target: span.target, + metavariables, + pretty_metavariables, + error, + }) +} + +fn partial_arrow_span_label( + project_texts: &[String], + declaration: &ArrowDeclaration, +) -> Option { + let raw = RawTheorySet::from_texts(project_texts.iter().map(String::as_str)).ok()?; + let raw = with_extensions_lossy(raw); + let theory: Operation = declaration.theory.parse().ok()?; + let arrow: Operation = declaration.name.text.parse().ok()?; + let mut needed = BTreeMap::>::new(); + let mut visiting = BTreeSet::<(Operation, Operation)>::new(); + collect_arrow_dependencies(&raw, &theory, &arrow, &mut needed, &mut visiting)?; + + let mut subset = RawTheorySet { + theories: BTreeMap::new(), + extensions: Vec::new(), + }; + for (theory_name, arrows) in needed { + let raw_theory = raw.theories.get(&theory_name)?; + let mut filtered_arrows = BTreeMap::new(); + for arrow_name in arrows { + let mut arrow = raw_theory.arrows.get(&arrow_name)?.clone(); + arrow.definition = None; + filtered_arrows.insert(arrow_name, arrow); + } + subset.theories.insert( + theory_name.clone(), + RawTheory { + name: raw_theory.name.clone(), + syntax_category: raw_theory.syntax_category.clone(), + arrows: filtered_arrows, + }, + ); + } + + let theories = match metacat::theory::TheorySet::from_raw(subset) { + Ok(theories) => theories, + Err(_) => return None, + }; + arrow_span_label(&theories, &declaration.theory, &declaration.name.text) +} + +fn empty_span_label(declaration: &ArrowDeclaration) -> ArrowSpanLabel { + ArrowSpanLabel { + source: String::new(), + target: String::new(), + source_metavariable_count: declaration.source_typevars.len(), + target_metavariable_count: declaration.target_typevars.len(), + error: None, + } +} + +fn raw_typevar_mismatch_error(declaration: &ArrowDeclaration) -> Option { + (!declaration.source_typevars.is_empty() + && !declaration.target_typevars.is_empty() + && declaration.source_typevars != declaration.target_typevars) + .then(|| { + format!( + "Source and target terms have different metavariables: source {{{}}}, target {{{}}}.", + declaration.source_typevars.join(", "), + declaration.target_typevars.join(", ") + ) + }) +} + +fn with_extensions_lossy(mut raw: RawTheorySet) -> RawTheorySet { + for extension in std::mem::take(&mut raw.extensions) { + let Some(theory) = raw.theories.get_mut(&extension.theory) else { + continue; + }; + for (name, arrow) in extension.arrows { + theory.arrows.entry(name).or_insert(arrow); + } + } + raw +} + +fn collect_arrow_dependencies( + raw: &RawTheorySet, + theory_name: &Operation, + arrow_name: &Operation, + needed: &mut BTreeMap>, + visiting: &mut BTreeSet<(Operation, Operation)>, +) -> Option<()> { + if !visiting.insert((theory_name.clone(), arrow_name.clone())) { + return Some(()); + } + + let theory = raw.theories.get(theory_name)?; + let arrow = theory.arrows.get(arrow_name)?; + needed + .entry(theory_name.clone()) + .or_default() + .insert(arrow_name.clone()); + + for operation in operations_in(&arrow.type_maps.0) + .into_iter() + .chain(operations_in(&arrow.type_maps.1)) + { + if should_skip_builtin_nat_operation(&theory.syntax_category, &operation) { + continue; + } + collect_arrow_dependencies(raw, &theory.syntax_category, &operation, needed, visiting)?; + } + + Some(()) +} + +fn operations_in(hexpr: &Hexpr) -> Vec { + let mut operations = Vec::new(); + collect_operations(hexpr, &mut operations); + operations +} + +fn collect_operations(hexpr: &Hexpr, operations: &mut Vec) { + match hexpr { + Hexpr::Composition(parts) | Hexpr::Tensor(parts) => { + for part in parts { + collect_operations(part, operations); + } + } + Hexpr::Frobenius { .. } => {} + Hexpr::Operation(operation) => operations.push(operation.clone()), + } +} + +fn should_skip_builtin_nat_operation(syntax_category: &Operation, operation: &Operation) -> bool { + operation.as_str() == "1" + || (syntax_category.as_str() == "nat" && operation.as_str().parse::().is_ok()) +} + +fn scan_arrow_declarations(text: &str) -> Vec { + let mut declarations = Vec::new(); + for (offset, ch) in text.char_indices() { + if ch != '(' { + continue; + } + let Some(end) = matching_close_offset(text, offset) else { + continue; + }; + if let Some(declaration) = parse_arrow_declaration(text, offset, end) { + declarations.push(declaration); + } + } + declarations +} + +fn project_arrow_declarations( + current_text: &str, + project_texts: &[String], +) -> Vec { + let mut declarations = Vec::new(); + for project_text in project_texts { + declarations.extend(scan_arrow_declarations(project_text)); + } + declarations.extend(scan_arrow_declarations(current_text)); + declarations +} + +fn parse_arrow_declaration(text: &str, start: usize, end: usize) -> Option { + let tokens = top_level_tokens(text, start + 1, end); + let kind = tokens.first()?.text.as_str(); + if !matches!(kind, "arr" | "def") { + return None; + } + + let colon_index = tokens.iter().position(|token| token.text == ":")?; + if colon_index < 2 { + return None; + } + + let name = tokens.get(colon_index - 1)?.clone(); + let theory = declaration_theory(text, start, end, &tokens, colon_index)?; + let arrow_index = tokens.iter().position(|token| token.text == "->")?; + let equal_index = tokens.iter().position(|token| token.text == "="); + let source_text = text.get(tokens.get(colon_index)?.end..tokens.get(arrow_index)?.start)?; + let target_end = equal_index + .and_then(|index| tokens.get(index).map(|token| token.start)) + .unwrap_or(end); + let target_text = text.get(tokens.get(arrow_index)?.end..target_end)?; + let source_typevars = leading_typevars_in(source_text); + let target_typevars = leading_typevars_in(target_text); + let metavariables = if source_typevars.is_empty() { + target_typevars.clone() + } else { + source_typevars.clone() + }; + + Some(ArrowDeclaration { + start, + end, + declaration_kind: kind.to_string(), + theory, + name, + metavariables, + source_typevars, + target_typevars, + }) +} + +fn definition_body_theory_at(text: &str, offset: usize) -> Option { + let definition = enclosing_arrow_declaration(text, offset)?; + if definition.declaration_kind != "def" + || offset < definition_body_start(text, definition.start, definition.end)? + { + return None; + } + Some(definition.theory) +} + +fn enclosing_arrow_declaration(text: &str, offset: usize) -> Option { + delimiter_stack_at(text, offset) + .iter() + .rev() + .filter(|delimiter| delimiter.char == '(') + .find_map(|delimiter| { + let end = matching_close_offset(text, delimiter.offset)?; + parse_arrow_declaration(text, delimiter.offset, end) + }) +} + +fn definition_body_start(text: &str, start: usize, end: usize) -> Option { + top_level_tokens(text, start + 1, end) + .into_iter() + .find(|token| token.text == "=") + .map(|token| token.end) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::syntax::position_at_offset; + + #[test] + fn arrow_details_returns_partial_semantic_profile_when_full_project_does_not_load() { + let text = r#"(theory fol.syntax nat { + (arr wff : 1 -> 1) + (arr |- : 1 -> 1) + (arr -> : 2 -> 1) +}) + +(theory fol.proof fol.syntax { + (arr broken : missing -> wff) + (arr ax : {wff wff} -> ([ph ps . ph ps] -> |-)) +})"#; + let offset = text.find("ax :").unwrap(); + let details = + arrow_details_at_position(text, &[text.to_string()], position_at_offset(text, offset)) + .unwrap(); + + assert_eq!(details.name, "ax"); + assert_eq!(details.source, "{wff(m0), wff(m1)}"); + assert_eq!(details.target, "|-(m0 -> m1)"); + assert_eq!(details.metavariables, ["ph", "ps"]); + assert_eq!(details.pretty_metavariables, ["m0", "m1"]); + assert_eq!(details.error, None); + } + + #[test] + fn arrow_details_uses_apex_metavariables_not_wire_names() { + let text = include_str!("../../fol.hex"); + let offset = text.find("ax-mp").unwrap(); + let details = + arrow_details_at_position(text, &[text.to_string()], position_at_offset(text, offset)) + .unwrap(); + + assert_eq!(details.name, "ax-mp"); + assert_eq!(details.source, "{|-(m0), |-(m0 -> m1)}"); + assert_eq!(details.target, "|-(m1)"); + assert_eq!(details.metavariables, ["ph", "ps"]); + assert_eq!(details.pretty_metavariables, ["m0", "m1"]); + assert_eq!(details.error, None); + } + + #[test] + fn arrow_details_on_definition_body_operation_reports_referenced_arrow() { + let text = include_str!("../../fol.hex"); + let definition_offset = text.find("(def id").unwrap(); + let body_arrow_offset = + text[definition_offset..].find("ax-mp").unwrap() + definition_offset; + let details = arrow_details_at_position( + text, + &[text.to_string()], + position_at_offset(text, body_arrow_offset), + ) + .unwrap(); + + assert_eq!(details.name, "ax-mp"); + assert_eq!(details.declaration_kind, "arr"); + assert_eq!(details.source, "{|-(m0), |-(m0 -> m1)}"); + assert_eq!(details.target, "|-(m1)"); + } + + #[test] + fn arrow_details_metavariables_for_ax5d_are_only_apex_typevars() { + let text = include_str!("../../fol.hex"); + let offset = text.find("ax5d").unwrap(); + let details = + arrow_details_at_position(text, &[text.to_string()], position_at_offset(text, offset)) + .unwrap(); + + assert_eq!(details.name, "ax5d"); + assert_eq!(details.metavariables, ["x", "ph", "ps"]); + assert_eq!(details.pretty_metavariables, ["m0", "m1", "m2"]); + assert!(details.source.contains("m1")); + assert!(details.source.contains("m2")); + assert!(details.target.contains("m0")); + assert!(details.target.contains("m1")); + assert!(details.target.contains("m2")); + assert!(!details.metavariables.contains(&"aps".to_string())); + assert!(!details.metavariables.contains(&"inner".to_string())); + } + + #[test] + fn arrow_details_reports_source_target_metavariable_mismatch() { + let text = r#"(theory fol.syntax nat { + (arr wff : 1 -> 1) +}) + +(theory fol.proof fol.syntax { + (arr bad : ([ph . ph] wff) -> ([ps . ps] wff)) +})"#; + let offset = text.find("bad :").unwrap(); + let details = + arrow_details_at_position(text, &[text.to_string()], position_at_offset(text, offset)) + .unwrap(); + + assert_eq!(details.source, "wff(m0)"); + assert_eq!(details.target, "wff(m0)"); + assert_eq!(details.metavariables, ["ph"]); + assert_eq!(details.pretty_metavariables, ["m0"]); + assert_eq!( + details.error.as_deref(), + Some("Source and target terms have different metavariables: source {ph}, target {ps}.") + ); + } +} + +fn declaration_theory( + text: &str, + start: usize, + end: usize, + tokens: &[crate::syntax::Token], + colon_index: usize, +) -> Option { + if tokens.first()?.text == "def" && colon_index >= 3 { + return Some(tokens.get(colon_index - 2)?.text.clone()); + } + + delimiter_stack_at(text, start) + .iter() + .rev() + .filter(|delimiter| delimiter.char == '(') + .find_map(|delimiter| { + let theory_end = matching_close_offset(text, delimiter.offset)?; + if theory_end < end { + return None; + } + let theory_tokens = top_level_tokens(text, delimiter.offset + 1, theory_end); + if theory_tokens.first()?.text == "theory" { + Some(theory_tokens.get(1)?.text.clone()) + } else { + None + } + }) +} + +fn top_level_tokens(text: &str, start: usize, end: usize) -> Vec { + let mut tokens = Vec::new(); + let mut offset = start; + while offset < end { + offset = skip_whitespace_and_comments(text, offset, end); + if offset >= end { + break; + } + + let Some(ch) = text.get(offset..).and_then(|slice| slice.chars().next()) else { + break; + }; + match ch { + '(' | '{' | '[' => { + offset = matching_close_offset(text, offset) + .map_or(offset + ch.len_utf8(), |end| end + 1); + } + _ if is_operation_char(ch) => { + if let Some(token) = token_at(text, offset, is_operation_char) { + offset = token.end; + tokens.push(token); + } else { + offset += ch.len_utf8(); + } + } + _ => offset += ch.len_utf8(), + } + } + tokens +} + +fn leading_typevars_in(text: &str) -> Vec { + let mut offset = 0usize; + while offset < text.len() { + let Some(ch) = text.get(offset..).and_then(|slice| slice.chars().next()) else { + break; + }; + match ch { + '[' => return source_variables_in_frobenius(text, offset).unwrap_or_default(), + '(' | '{' => { + let Some(end) = matching_close_offset(text, offset) else { + break; + }; + let nested = leading_typevars_in(&text[offset + ch.len_utf8()..end]); + if !nested.is_empty() { + return nested; + } + offset = end + 1; + } + _ => offset += ch.len_utf8(), + } + } + Vec::new() +} + +fn source_variables_in_frobenius(text: &str, start: usize) -> Option> { + let end = matching_close_offset(text, start)?; + let mut variables = Vec::new(); + let mut offset = start + 1; + while offset < end { + let Some(ch) = text.get(offset..).and_then(|slice| slice.chars().next()) else { + break; + }; + match ch { + '.' => break, + _ if is_variable_char(ch) => { + let start = offset; + offset += ch.len_utf8(); + while offset < text.len() { + let Some(next) = text.get(offset..).and_then(|slice| slice.chars().next()) + else { + break; + }; + if !is_variable_char(next) { + break; + } + offset += next.len_utf8(); + } + let variable = text[start..offset].to_string(); + if !variables.contains(&variable) { + variables.push(variable); + } + } + _ => offset += ch.len_utf8(), + } + } + Some(variables) +} + +fn is_variable_char(ch: char) -> bool { + ch.is_ascii_alphanumeric() || matches!(ch, '_' | '-') +} + +fn skip_whitespace_and_comments(text: &str, mut offset: usize, end: usize) -> usize { + while offset < end { + let Some(ch) = text.get(offset..).and_then(|slice| slice.chars().next()) else { + break; + }; + if ch.is_whitespace() { + offset += ch.len_utf8(); + continue; + } + if ch == '#' { + while offset < end { + let Some(ch) = text.get(offset..).and_then(|slice| slice.chars().next()) else { + break; + }; + offset += ch.len_utf8(); + if ch == '\n' { + break; + } + } + continue; + } + break; + } + offset +} diff --git a/metacat-lsp/src/main.rs b/metacat-lsp/src/main.rs index 78d28e7..ce5aecd 100644 --- a/metacat-lsp/src/main.rs +++ b/metacat-lsp/src/main.rs @@ -1,4 +1,5 @@ mod analysis; +mod arrow_details; mod capabilities; mod diagnostics; mod documents; @@ -15,6 +16,8 @@ async fn main() { let stdin = tokio::io::stdin(); let stdout = tokio::io::stdout(); - let (service, socket) = LspService::new(Backend::new); + let (service, socket) = LspService::build(Backend::new) + .custom_method("metacat/arrowDetails", Backend::arrow_details) + .finish(); Server::new(stdin, stdout, socket).serve(service).await; } diff --git a/metacat-lsp/src/server.rs b/metacat-lsp/src/server.rs index 76510ab..24443d4 100644 --- a/metacat-lsp/src/server.rs +++ b/metacat-lsp/src/server.rs @@ -1,3 +1,4 @@ +use crate::arrow_details::{ArrowDetails, ArrowDetailsParams, arrow_details_at_position}; use crate::capabilities::server_capabilities; use crate::diagnostics::diagnostics_for_document; use crate::documents::DocumentStore; @@ -30,6 +31,18 @@ impl Backend { .publish_diagnostics(uri, diagnostics_for_document(text, &project.texts), None) .await; } + + pub async fn arrow_details(&self, params: ArrowDetailsParams) -> Result> { + let Some(text) = self.documents.get(¶ms.uri).await else { + return Ok(None); + }; + let project = context_for_document(¶ms.uri, &text); + Ok(arrow_details_at_position( + &text, + &project.texts, + params.position, + )) + } } #[tower_lsp::async_trait] diff --git a/metacat-lsp/src/syntax.rs b/metacat-lsp/src/syntax.rs index b68e49f..ff29176 100644 --- a/metacat-lsp/src/syntax.rs +++ b/metacat-lsp/src/syntax.rs @@ -52,7 +52,7 @@ pub struct OperationElement { pub start: usize, } -#[derive(Debug)] +#[derive(Clone, Debug)] pub struct Token { pub text: String, pub start: usize, diff --git a/metacat-vscode/package.json b/metacat-vscode/package.json index a244a69..14dd062 100644 --- a/metacat-vscode/package.json +++ b/metacat-vscode/package.json @@ -13,14 +13,43 @@ ], "activationEvents": [ "onLanguage:metacat", - "onCommand:metacat.checkCurrentFile" + "onCommand:metacat.checkCurrentFile", + "onCommand:metacat.focusArrowPanel", + "onCommand:metacat.refreshArrowPanel", + "onView:metacat.project" ], "main": "./out/extension.js", "contributes": { + "viewsContainers": { + "activitybar": [ + { + "id": "metacat", + "title": "Metacat", + "icon": "resources/metacat-cat.svg" + } + ] + }, + "views": { + "metacat": [ + { + "id": "metacat.project", + "name": "Arrow", + "type": "webview" + } + ] + }, "commands": [ { "command": "metacat.checkCurrentFile", "title": "Metacat: Check Current File" + }, + { + "command": "metacat.focusArrowPanel", + "title": "Metacat: Focus Arrow Panel" + }, + { + "command": "metacat.refreshArrowPanel", + "title": "Metacat: Refresh Arrow Panel" } ], "configuration": { diff --git a/metacat-vscode/resources/metacat-cat.svg b/metacat-vscode/resources/metacat-cat.svg new file mode 100644 index 0000000..829af1d --- /dev/null +++ b/metacat-vscode/resources/metacat-cat.svg @@ -0,0 +1,4 @@ + + + + diff --git a/metacat-vscode/src/extension.ts b/metacat-vscode/src/extension.ts index 9933767..f25a99d 100644 --- a/metacat-vscode/src/extension.ts +++ b/metacat-vscode/src/extension.ts @@ -17,8 +17,20 @@ export function activate(context: vscode.ExtensionContext): void { context.subscriptions.push(outputChannel); startLanguageServer(context); + const projectPanel = new MetacatProjectPanelProvider(); + context.subscriptions.push( + projectPanel, + vscode.window.registerWebviewViewProvider('metacat.project', projectPanel), + ); + context.subscriptions.push( vscode.commands.registerCommand('metacat.checkCurrentFile', checkCurrentFile), + vscode.commands.registerCommand('metacat.focusArrowPanel', async () => { + await vscode.commands.executeCommand('workbench.view.extension.metacat').then(undefined, () => undefined); + await vscode.commands.executeCommand('metacat.project.focus').then(undefined, () => undefined); + projectPanel.refresh(); + }), + vscode.commands.registerCommand('metacat.refreshArrowPanel', () => projectPanel.refresh()), ); } @@ -138,3 +150,258 @@ function languageServerExecutable(context: vscode.ExtensionContext): string { function binaryName(name: string): string { return process.platform === 'win32' ? `${name}.exe` : name; } + +class MetacatProjectPanelProvider implements vscode.WebviewViewProvider, vscode.Disposable { + private readonly disposables: vscode.Disposable[]; + private updateVersion = 0; + private view: vscode.WebviewView | undefined; + + constructor() { + this.disposables = [ + vscode.window.onDidChangeActiveTextEditor(() => this.update()), + vscode.window.onDidChangeTextEditorSelection((event) => { + if (event.textEditor === vscode.window.activeTextEditor) { + this.update(); + } + }), + vscode.workspace.onDidChangeTextDocument((event) => { + if (event.document === vscode.window.activeTextEditor?.document) { + this.update(); + } + }), + ]; + } + + resolveWebviewView(view: vscode.WebviewView): void { + this.view = view; + view.webview.options = { enableScripts: false }; + this.update(); + } + + refresh(): void { + this.update(); + } + + private async update(): Promise { + if (!this.view) { + return; + } + const version = ++this.updateVersion; + + const editor = vscode.window.activeTextEditor; + if (!editor || editor.document.languageId !== 'metacat') { + this.view.webview.html = renderPanel({ kind: 'empty', message: 'Open a Metacat file.' }); + return; + } + + const details = await semanticArrowDetailsAt(editor.document, editor.selection.active); + if (version !== this.updateVersion) { + return; + } + this.view.webview.html = renderPanel(details ?? { + kind: 'empty', + message: 'Select an arrow name or an arrow declaration.', + }); + } + + dispose(): void { + for (const disposable of this.disposables) { + disposable.dispose(); + } + } +} + +type PanelModel = ArrowDetails | EmptyPanel; + +interface EmptyPanel { + kind: 'empty'; + message: string; +} + +interface ArrowDetails { + kind: 'arrow'; + declarationKind: 'arr' | 'def'; + name: string; + source: string; + target: string; + metavariables: string[]; + prettyMetavariables: string[]; + error?: string | null; +} + +interface SemanticArrowDetails { + declarationKind: 'arr' | 'def'; + name: string; + source: string; + target: string; + metavariables: string[]; + prettyMetavariables: string[]; + error?: string | null; +} + +async function semanticArrowDetailsAt( + document: vscode.TextDocument, + position: vscode.Position, +): Promise { + if (!languageClient) { + return undefined; + } + + try { + const details = await languageClient.sendRequest('metacat/arrowDetails', { + uri: document.uri.toString(), + position, + }); + if (!details) { + return undefined; + } + return { + kind: 'arrow', + ...details, + }; + } catch (error) { + const message = error instanceof Error ? error.message : String(error); + outputChannel.appendLine(`Failed to fetch Metacat arrow details: ${message}`); + return undefined; + } +} + +function renderPanel(model: PanelModel): string { + const body = model.kind === 'arrow' + ? renderArrowDetails(model) + : `

${escapeHtml(model.message)}

`; + + return ` + + + + + + +${body} +`; +} + +function renderArrowDetails(details: ArrowDetails): string { + const metavariables = details.metavariables.length > 0 + ? `
${details.metavariables.map((name) => `${escapeHtml(name)}`).join('')}
` + : '

None

'; + const error = details.error + ? `
+
Error
+
${escapeHtml(details.error)}
+
` + : ''; + + return `
${escapeHtml(details.name)} ${details.declarationKind}
+${error} +
+
Source
+ ${renderPrettyLabel(details.source, details.prettyMetavariables)} +
+
+
Target
+ ${renderPrettyLabel(details.target, details.prettyMetavariables)} +
+
+
Metavariables
+ ${metavariables} +
`; +} + +function renderPrettyLabel(text: string, metavariables: string[]): string { + const names = new Set(metavariables); + if (names.size === 0) { + return escapeHtml(text); + } + + const pattern = new RegExp(`\\b(${[...names].map(escapeRegExp).join('|')})\\b`, 'g'); + return text + .split(pattern) + .map((part) => { + const escaped = escapeHtml(part); + return names.has(part) ? `${escaped}` : escaped; + }) + .join(''); +} + +function escapeRegExp(value: string): string { + return value.replace(/[.*+?^${}()|[\]\\]/g, '\\$&'); +} + +function escapeHtml(value: string): string { + return value + .replace(/&/g, '&') + .replace(//g, '>') + .replace(/"/g, '"') + .replace(/'/g, '''); +} diff --git a/metacat/src/check.rs b/metacat/src/check.rs index e90e6bc..861688e 100644 --- a/metacat/src/check.rs +++ b/metacat/src/check.rs @@ -228,7 +228,9 @@ impl Functor<(), Operation, (), Dual> for AsType<'_> { fn project_check_error(err: Error, indices: &[usize]) -> Error { match err { - Error::PartialResult(partial) => Error::PartialResult(project_partial_result(partial, indices)), + Error::PartialResult(partial) => { + Error::PartialResult(project_partial_result(partial, indices)) + } other => other, } } diff --git a/metacat/src/theory/graph.rs b/metacat/src/theory/graph.rs index 4f47c06..bf590e5 100644 --- a/metacat/src/theory/graph.rs +++ b/metacat/src/theory/graph.rs @@ -66,9 +66,7 @@ pub fn syntax_dependency_graph(raw: &RawTheorySet) -> Result Result, GraphError> { +pub fn topological_order(graph: &SyntaxDependencyGraph) -> Result, GraphError> { #[derive(Clone, Copy, PartialEq, Eq)] enum Mark { Visiting, @@ -214,8 +212,8 @@ mod tests { } #[test] - fn subset_includes_transitive_dependencies_and_extensions( - ) -> Result<(), Box> { + fn subset_includes_transitive_dependencies_and_extensions() + -> Result<(), Box> { let raw = RawTheorySet::from_text( r#" (theory fol.syntax nat { diff --git a/metacat/src/tree.rs b/metacat/src/tree.rs index b9c6941..e714352 100644 --- a/metacat/src/tree.rs +++ b/metacat/src/tree.rs @@ -88,7 +88,11 @@ mod tests { "*", 0, vec![ - Tree::Node("+", 0, vec![Tree::Node("1", 0, vec![]), Tree::Node("1", 0, vec![])]), + Tree::Node( + "+", + 0, + vec![Tree::Node("1", 0, vec![]), Tree::Node("1", 0, vec![])], + ), Tree::Node("2", 0, vec![]), ], );