Add spans to patterns (#438)

* Add spans to patterns in CST and AST * Add hover for patterns * Preserve spans during elaboration
polarity-lang · Jan 8, 2025 · bbc91ef · bbc91ef
1 parent b60ce0a
commit bbc91ef
Show file tree

Hide file tree

Showing 13 changed files with 77 additions and 11 deletions.
diff --git a/lang/ast/src/exp/case.rs b/lang/ast/src/exp/case.rs
@@ -23,14 +23,15 @@ 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,
 }
 
 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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,