From bbc91efbc25f77f505d244e96cc566f63f6dc858 Mon Sep 17 00:00:00 2001
From: David Binder <david.binder@uni-tuebingen.de>
Date: Wed, 8 Jan 2025 19:11:50 +0100
Subject: [PATCH] Add spans to patterns (#438)

* Add spans to patterns in CST and AST

* Add hover for patterns

* Preserve spans during elaboration
---
 lang/ast/src/exp/case.rs                          |  5 +++--
 lang/backend/src/ast2ir/exprs.rs                  |  2 +-
 lang/driver/src/info/collect.rs                   | 15 +++++++++++++--
 lang/driver/src/info/data.rs                      | 15 +++++++++++++++
 lang/elaborator/src/normalizer/val.rs             |  1 +
 .../src/typechecker/exprs/local_comatch.rs        |  8 +++++++-
 .../src/typechecker/exprs/local_match.rs          |  7 ++++++-
 lang/lowering/src/lower/exp/mod.rs                | 15 +++++++++++++--
 lang/lsp/src/hover.rs                             | 11 +++++++++++
 lang/parser/src/cst/exp.rs                        |  2 ++
 lang/parser/src/grammar/cst.lalrpop               |  4 ++--
 lang/transformations/src/lifting/mod.rs           |  1 +
 lang/transformations/src/xfunc/matrix.rs          |  2 ++
 13 files changed, 77 insertions(+), 11 deletions(-)

diff --git a/lang/ast/src/exp/case.rs b/lang/ast/src/exp/case.rs
index b4334eed4a..7444e0d6d3 100644
--- a/lang/ast/src/exp/case.rs
+++ b/lang/ast/src/exp/case.rs
@@ -23,6 +23,7 @@ use super::{Exp, IdBound, Lvl, MetaVar, TelescopeInst};
 #[derive(Debug, Clone, Derivative)]
 #[derivative(Eq, PartialEq, Hash)]
 pub struct Pattern {
+    pub span: Option<Span>,
     pub is_copattern: bool,
     pub name: IdBound,
     pub params: TelescopeInst,
@@ -30,7 +31,7 @@ pub struct Pattern {
 
 impl Print for Pattern {
     fn print<'a>(&'a self, cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> {
-        let Pattern { is_copattern, name, params } = self;
+        let Pattern { span: _, is_copattern, name, params } = self;
         if *is_copattern {
             alloc.text(DOT).append(alloc.ctor(&name.id)).append(params.print(cfg, alloc))
         } else {
@@ -44,7 +45,7 @@ impl Zonk for Pattern {
         &mut self,
         meta_vars: &crate::HashMap<MetaVar, crate::MetaVarState>,
     ) -> Result<(), ZonkError> {
-        let Pattern { is_copattern: _, name: _, params } = self;
+        let Pattern { span: _, is_copattern: _, name: _, params } = self;
         params.zonk(meta_vars)
     }
 }
diff --git a/lang/backend/src/ast2ir/exprs.rs b/lang/backend/src/ast2ir/exprs.rs
index e70a611b7a..a562ae6636 100644
--- a/lang/backend/src/ast2ir/exprs.rs
+++ b/lang/backend/src/ast2ir/exprs.rs
@@ -154,7 +154,7 @@ impl ToIR for ast::Case {
 
     fn to_ir(&self) -> Result<Self::Target, BackendError> {
         let ast::Case { pattern, body, .. } = self;
-        let ast::Pattern { is_copattern, params, name } = pattern;
+        let ast::Pattern { span: _, is_copattern, params, name } = pattern;
 
         let params = params.to_ir()?;
 
diff --git a/lang/driver/src/info/collect.rs b/lang/driver/src/info/collect.rs
index eda44474b6..e32ba09eae 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 ed426a768f..c0a928438a 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/elaborator/src/normalizer/val.rs b/lang/elaborator/src/normalizer/val.rs
index 3e8316d4fa..c6ac35d29e 100644
--- a/lang/elaborator/src/normalizer/val.rs
+++ b/lang/elaborator/src/normalizer/val.rs
@@ -668,6 +668,7 @@ impl ReadBack for Case {
         Ok(ast::Case {
             span: *span,
             pattern: ast::Pattern {
+                span: None,
                 is_copattern: *is_copattern,
                 name: name.clone(),
                 params: params.clone(),
diff --git a/lang/elaborator/src/typechecker/exprs/local_comatch.rs b/lang/elaborator/src/typechecker/exprs/local_comatch.rs
index e34a446c6f..a371846694 100644
--- a/lang/elaborator/src/typechecker/exprs/local_comatch.rs
+++ b/lang/elaborator/src/typechecker/exprs/local_comatch.rs
@@ -118,7 +118,11 @@ impl WithExpectedType<'_> {
             let DtorMeta { self_param, ret_typ, params, .. } =
                 ctx.type_info_table.lookup_dtor(&case.pattern.name)?;
             let SelfParam { typ: TypCtor { args: def_args, .. }, .. } = self_param;
-            let Case { span, pattern: Pattern { name, params: params_inst, .. }, body } = &case;
+            let Case {
+                span,
+                pattern: Pattern { span: pattern_span, name, params: params_inst, .. },
+                body,
+            } = &case;
             // We are in the following situation:
             //
             // codata T(...) {  (self : T(.....)).d(...) : t, ...}
@@ -184,6 +188,7 @@ impl WithExpectedType<'_> {
                             let case_out = Case {
                                 span: *span,
                                 pattern: Pattern {
+                                    span: *pattern_span,
                                     is_copattern: true,
                                     name: name.clone(),
                                     params: args_out,
@@ -323,6 +328,7 @@ impl WithExpectedType<'_> {
                             let case_out = Case {
                                 span: *span,
                                 pattern: Pattern {
+                                    span: *pattern_span,
                                     is_copattern: true,
                                     name: name.clone(),
                                     params: args_out,
diff --git a/lang/elaborator/src/typechecker/exprs/local_match.rs b/lang/elaborator/src/typechecker/exprs/local_match.rs
index 20a147fe64..c36741f2f0 100644
--- a/lang/elaborator/src/typechecker/exprs/local_match.rs
+++ b/lang/elaborator/src/typechecker/exprs/local_match.rs
@@ -157,7 +157,11 @@ impl WithScrutineeType<'_> {
         let mut cases_out = Vec::new();
 
         for case in cases {
-            let Case { span, pattern: Pattern { name, params: args, .. }, body } = case;
+            let Case {
+                span,
+                pattern: Pattern { name, params: args, span: pattern_span, .. },
+                body,
+            } = case;
             let CtorMeta { typ: TypCtor { args: def_args, .. }, params, .. } =
                 ctx.type_info_table.lookup_ctor(&name)?;
             let TypCtor { args: on_args, .. } = &self.scrutinee_type;
@@ -296,6 +300,7 @@ impl WithScrutineeType<'_> {
                     let case_out = Case {
                         span,
                         pattern: Pattern {
+                            span: pattern_span,
                             is_copattern: false,
                             name: name.clone(),
                             params: args_out,
diff --git a/lang/lowering/src/lower/exp/mod.rs b/lang/lowering/src/lower/exp/mod.rs
index 7b33607e64..08e72050fe 100644
--- a/lang/lowering/src/lower/exp/mod.rs
+++ b/lang/lowering/src/lower/exp/mod.rs
@@ -248,7 +248,12 @@ impl Lower for cst::exp::Case<cst::exp::Pattern> {
             };
             Ok(ast::Case {
                 span: Some(*span),
-                pattern: ast::Pattern { is_copattern: false, name, params },
+                pattern: ast::Pattern {
+                    span: Some(pattern.span),
+                    is_copattern: false,
+                    name,
+                    params,
+                },
                 body: body.lower(ctx)?,
             })
         })
@@ -270,7 +275,12 @@ impl Lower for cst::exp::Case<cst::exp::Copattern> {
             };
             Ok(ast::Case {
                 span: Some(*span),
-                pattern: ast::Pattern { is_copattern: true, name, params },
+                pattern: ast::Pattern {
+                    span: Some(pattern.span),
+                    is_copattern: true,
+                    name,
+                    params,
+                },
                 body: body.lower(ctx)?,
             })
         })
@@ -543,6 +553,7 @@ impl Lower for cst::exp::Lam {
         let case = cst::exp::Case {
             span: *span,
             pattern: cst::exp::Copattern {
+                span: *span,
                 name: Ident { span: *span, id: "ap".to_owned() },
                 params: vec![
                     cst::exp::BindingSite::Wildcard { span: Default::default() },
diff --git a/lang/lsp/src/hover.rs b/lang/lsp/src/hover.rs
index cc08b942ec..34ab946e6b 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())])
diff --git a/lang/parser/src/cst/exp.rs b/lang/parser/src/cst/exp.rs
index 5717a8781a..570805f5d5 100644
--- a/lang/parser/src/cst/exp.rs
+++ b/lang/parser/src/cst/exp.rs
@@ -11,12 +11,14 @@ pub enum BindingSite {
 
 #[derive(Debug, Clone)]
 pub struct Pattern {
+    pub span: Span,
     pub name: Ident,
     pub params: Vec<BindingSite>,
 }
 
 #[derive(Debug, Clone)]
 pub struct Copattern {
+    pub span: Span,
     pub name: Ident,
     pub params: Vec<BindingSite>,
 }
diff --git a/lang/parser/src/grammar/cst.lalrpop b/lang/parser/src/grammar/cst.lalrpop
index 47334df507..2848c76433 100644
--- a/lang/parser/src/grammar/cst.lalrpop
+++ b/lang/parser/src/grammar/cst.lalrpop
@@ -201,11 +201,11 @@ Let: Let = <l: @L> <doc: DocComment?> <attr: OptAttributes> "let" <name: Ident><
 
 
 Pattern: Pattern = {
-  <name: Ident><params: OptTelescopeInst> => Pattern { name, params },
+  <l: @L><name: Ident><params: OptTelescopeInst><r: @R> => Pattern { span: span(l,r), name, params },
 }
 
 Copattern: Copattern = {
-  "." <name: Ident><params: OptTelescopeInst> => Copattern { name, params },
+  <l: @L> "." <name: Ident><params: OptTelescopeInst> <r: @R> => Copattern { span: span(l,r), name, params },
 }
 
 Case<P> : Case<P> = {
diff --git a/lang/transformations/src/lifting/mod.rs b/lang/transformations/src/lifting/mod.rs
index 57e0ae2bb8..e3ae89dca7 100644
--- a/lang/transformations/src/lifting/mod.rs
+++ b/lang/transformations/src/lifting/mod.rs
@@ -252,6 +252,7 @@ impl Lift for Case {
         pattern.params.lift_telescope(ctx, |ctx, params| Case {
             span: *span,
             pattern: Pattern {
+                span: None,
                 is_copattern: pattern.is_copattern,
                 name: pattern.name.clone(),
                 params,
diff --git a/lang/transformations/src/xfunc/matrix.rs b/lang/transformations/src/xfunc/matrix.rs
index 9676bc8e20..b97e3e79b4 100644
--- a/lang/transformations/src/xfunc/matrix.rs
+++ b/lang/transformations/src/xfunc/matrix.rs
@@ -198,6 +198,7 @@ impl XData {
                         body.map(|body| ast::Case {
                             span: None,
                             pattern: ast::Pattern {
+                                span: None,
                                 is_copattern: false,
                                 name: IdBound {
                                     span: None,
@@ -259,6 +260,7 @@ impl XData {
                         body.map(|body| ast::Case {
                             span: None,
                             pattern: ast::Pattern {
+                                span: None,
                                 is_copattern: true,
                                 name: IdBound {
                                     span: None,