From d92084e225279d0072e4cadf5cc3dee9c1021ce3 Mon Sep 17 00:00:00 2001
From: David Binder <david.binder@uni-tuebingen.de>
Date: Wed, 8 Jan 2025 17:04:14 +0100
Subject: [PATCH] Add hover for patterns

---
 lang/driver/src/info/collect.rs | 15 +++++++++++++--
 lang/driver/src/info/data.rs    | 15 +++++++++++++++
 lang/lsp/src/hover.rs           | 11 +++++++++++
 3 files changed, 39 insertions(+), 2 deletions(-)

diff --git a/lang/driver/src/info/collect.rs b/lang/driver/src/info/collect.rs
index eda44474b..e32ba09ea 100644
--- a/lang/driver/src/info/collect.rs
+++ b/lang/driver/src/info/collect.rs
@@ -16,7 +16,7 @@ use super::data::{
 };
 use super::item::Item;
 use super::lookup::{lookup_codef, lookup_ctor, lookup_decl, lookup_def, lookup_dtor, lookup_let};
-use super::CaseInfo;
+use super::{CaseInfo, PatternInfo};
 
 /// Traverse the program and collect information for the LSP server.
 #[allow(clippy::type_complexity)]
@@ -459,13 +459,24 @@ impl CollectInfo for LocalComatch {
     }
 }
 
+impl CollectInfo for Pattern {
+    fn collect_info(&self, _db: &Database, collector: &mut InfoCollector) {
+        let Pattern { span, name, is_copattern, .. } = self;
+        if let Some(span) = span {
+            let info = PatternInfo { is_copattern: *is_copattern, name: name.id.clone() };
+            collector.add_info(*span, info)
+        }
+    }
+}
+
 impl CollectInfo for Case {
     fn collect_info(&self, db: &Database, collector: &mut InfoCollector) {
-        let Case { body, span, .. } = self;
+        let Case { body, span, pattern, .. } = self;
         if let Some(span) = span {
             let info = CaseInfo {};
             collector.add_info(*span, info)
         }
+        pattern.collect_info(db, collector);
         body.collect_info(db, collector)
     }
 }
diff --git a/lang/driver/src/info/data.rs b/lang/driver/src/info/data.rs
index ed426a768..c0a928438 100644
--- a/lang/driver/src/info/data.rs
+++ b/lang/driver/src/info/data.rs
@@ -35,6 +35,7 @@ pub enum InfoContent {
     LocalComatchInfo(LocalComatchInfo),
     // Various
     CaseInfo(CaseInfo),
+    PatternInfo(PatternInfo),
     // Toplevel Declarations
     DataInfo(DataInfo),
     CtorInfo(CtorInfo),
@@ -247,6 +248,20 @@ impl From<AnnoInfo> for InfoContent {
         InfoContent::AnnoInfo(value)
     }
 }
+
+// Information for patterns and copatterns
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct PatternInfo {
+    pub name: String,
+    pub is_copattern: bool,
+}
+
+impl From<PatternInfo> for InfoContent {
+    fn from(value: PatternInfo) -> Self {
+        InfoContent::PatternInfo(value)
+    }
+}
+
 // Information for clauses in pattern and copattern matches
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub struct CaseInfo {}
diff --git a/lang/lsp/src/hover.rs b/lang/lsp/src/hover.rs
index cc08b942e..34ab946e6 100644
--- a/lang/lsp/src/hover.rs
+++ b/lang/lsp/src/hover.rs
@@ -93,6 +93,7 @@ impl ToHoverContent for InfoContent {
             InfoContent::LocalComatchInfo(i) => i.to_hover_content(),
             InfoContent::HoleInfo(i) => i.to_hover_content(),
             InfoContent::AnnoInfo(i) => i.to_hover_content(),
+            InfoContent::PatternInfo(i) => i.to_hover_content(),
             InfoContent::CaseInfo(i) => i.to_hover_content(),
             InfoContent::DataInfo(i) => i.to_hover_content(),
             InfoContent::CtorInfo(i) => i.to_hover_content(),
@@ -183,6 +184,16 @@ impl ToHoverContent for AnnoInfo {
     }
 }
 
+impl ToHoverContent for PatternInfo {
+    fn to_hover_content(self) -> HoverContents {
+        if self.is_copattern {
+            HoverContents::Array(vec![MarkedString::String(format!("Copattern: `{}`", self.name))])
+        } else {
+            HoverContents::Array(vec![MarkedString::String(format!("Pattern: `{}`", self.name))])
+        }
+    }
+}
+
 impl ToHoverContent for CaseInfo {
     fn to_hover_content(self) -> HoverContents {
         HoverContents::Array(vec![MarkedString::String("Clause".to_owned())])