Correct declarations

src/diagnostics.rs

@@ -1,33 +1,39 @@
-use crate::{AssociatedElement, DeclarationKind, DocumentationTag, NatSpec, Tag};
+use crate::{AssociatedElement, NatSpec, Tag};
 use lsp_types::{Diagnostic, DiagnosticSeverity, Range};
 
-impl Tag {
-    fn supported_declarations(&self) -> &[DeclarationKind] {
-        use DeclarationKind::*;
+impl AssociatedElement {
+    fn supported_tags(&self) -> &[Tag] {
+        use Tag::*;
         match self {
-            Tag::Title => &[Rule, Invariant],
-            Tag::Notice => &[Rule, Invariant, Function, Definition, Ghost, Methods],
-            Tag::Dev => &[Rule, Invariant, Function, Definition, Ghost, Methods],
-            Tag::Param => &[Rule, Invariant, Function, Definition, Ghost],
-            Tag::Return => &[Function, Definition, Ghost],
-            Tag::Formula => &[Rule],
-            _ => &[],
+            AssociatedElement::Rule { .. } => &[Title, Notice, Dev, Param, Formula],
+            AssociatedElement::Invariant { .. } => &[Title, Notice, Dev, Param],
+            AssociatedElement::Function { .. } => &[Notice, Dev, Param, Return],
+            AssociatedElement::Definition { .. } => &[Notice, Dev, Param, Return],
+            AssociatedElement::Ghost { .. } | AssociatedElement::GhostMapping { .. } => {
+                &[Notice, Dev, Param, Return]
+            }
+            AssociatedElement::Methods { .. } => &[Notice, Dev],
         }
     }
 
-    fn supports(&self, declaration_kind: DeclarationKind) -> bool {
-        self.supported_declarations().contains(&declaration_kind)
+    fn supports(&self, tag: &Tag) -> bool {
+        self.supported_tags().contains(tag)
     }
-}
 
-impl AssociatedElement {
     fn defines_param(&self, param: &str) -> bool {
-        self.params.iter().any(|(_, name)| name == param)
+        match self {
+            AssociatedElement::Rule { params, .. }
+            | AssociatedElement::Invariant { params, .. }
+            | AssociatedElement::Function { params, .. }
+            | AssociatedElement::Definition { params, .. } => params
+                .iter()
+                .filter_map(|(_, name)| name.as_ref())
+                .any(|name| name == param),
+            _ => false,
+        }
     }
 }
 
-impl DocumentationTag {}
-
 impl NatSpec {
     pub fn enumerate_diagnostics(&self) -> Vec<Diagnostic> {
         let mut warnings = Vec::new();
@@ -72,10 +78,9 @@ impl NatSpec {
                     }
                 }
 
-                let decl_kind = associated.kind;
                 for tag in tags {
-                    if !tag.kind.supports(decl_kind) {
-                        let error_desc = format!("this tag is unsupported for {decl_kind} blocks");
+                    if !associated.supports(&tag.kind) {
+                        let error_desc = format!("this tag is unsupported for {associated} blocks");
                         add(error_desc, tag.range, ERROR);
                     }
                 }

src/lib.rs

@@ -31,54 +31,49 @@ pub enum NatSpec {
     },
 }
 
-#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
-pub struct AssociatedElement {
-    pub kind: DeclarationKind,
-    pub name: String,
-    pub params: Vec<(String, String)>,
-    pub block: Option<String>,
-}
-
-#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
-pub enum DeclarationKind {
-    Rule,
-    Invariant,
-    Function,
-    Definition,
-    Ghost,
-    Methods,
-}
-
-impl Display for DeclarationKind {
-    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        let kind = match self {
-            DeclarationKind::Rule => "rule",
-            DeclarationKind::Invariant => "invariant",
-            DeclarationKind::Function => "function",
-            DeclarationKind::Definition => "definition",
-            DeclarationKind::Ghost => "ghost",
-            DeclarationKind::Methods => "methods",
-        };
-        write!(f, "{kind}")
-    }
-}
-
-impl TryFrom<&str> for DeclarationKind {
-    type Error = color_eyre::Report;
+pub type Ty = String;
+pub type Param = (Ty, Option<String>);
 
-    fn try_from(kw: &str) -> Result<Self, Self::Error> {
-        use DeclarationKind::*;
-
-        match kw {
-            "rule" => Ok(Rule),
-            "invariant" => Ok(Invariant),
-            "function" => Ok(Function),
-            "definition" => Ok(Definition),
-            "ghost" => Ok(Ghost),
-            "methods" => Ok(Methods),
-            _ => bail!("unrecognized declaration keyword: {kw}"),
-        }
-    }
+#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
+pub enum AssociatedElement {
+    Rule {
+        name: String,
+        params: Vec<Param>,
+        filters: Option<String>,
+        block: String,
+    },
+    Invariant {
+        name: String,
+        params: Vec<Param>,
+        invariant: String,
+        block: String,
+    },
+    Function {
+        name: String,
+        params: Vec<Param>,
+        returns: Option<String>,
+        block: String,
+    },
+    Definition {
+        name: String,
+        params: Vec<Param>,
+        returns: String,
+        definition: String,
+    },
+    Ghost {
+        name: String,
+        ty_list: Vec<Ty>,
+        returns: String,
+        block: Option<String>,
+    },
+    GhostMapping {
+        name: String,
+        mapping: String,
+        block: Option<String>,
+    },
+    Methods {
+        block: String,
+    },
 }
 
 impl NatSpec {
@@ -110,10 +105,16 @@ impl NatSpec {
 
     pub fn auto_generated_title(&self) -> Result<String, Report> {
         match self {
-            NatSpec::Documentation { associated, .. } => associated
-                .as_ref()
-                .map(|element| element.name.clone())
-                .ok_or_else(|| eyre!("documentation has no associated syntactic element")),
+            NatSpec::Documentation { associated, .. } => {
+                let associated = associated
+                    .as_ref()
+                    .ok_or_else(|| eyre!("documentation has no associated syntactic element"))?;
+
+                associated
+                    .name()
+                    .map(|name| name.to_string())
+                    .ok_or_else(|| eyre!("element has no name"))
+            }
             _ => bail!("free form comments have no associated syntactic element"),
         }
     }
@@ -216,3 +217,72 @@ impl From<&str> for Tag {
         }
     }
 }
+
+impl Display for AssociatedElement {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        let kind = match self {
+            AssociatedElement::Rule { .. } => "rule",
+            AssociatedElement::Invariant { .. } => "invariant",
+            AssociatedElement::Function { .. } => "function",
+            AssociatedElement::Definition { .. } => "definition",
+            AssociatedElement::Ghost { .. } | AssociatedElement::GhostMapping { .. } => "ghost",
+            AssociatedElement::Methods { .. } => "methods",
+        };
+
+        write!(f, "{kind}")
+    }
+}
+
+impl AssociatedElement {
+    pub fn name(&self) -> Option<&str> {
+        match self {
+            AssociatedElement::Rule { name, .. }
+            | AssociatedElement::Invariant { name, .. }
+            | AssociatedElement::Function { name, .. }
+            | AssociatedElement::Definition { name, .. }
+            | AssociatedElement::Ghost { name, .. }
+            | AssociatedElement::GhostMapping { name, .. } => Some(name.as_str()),
+            _ => None,
+        }
+    }
+
+    pub fn params(&self) -> Option<&[Param]> {
+        match self {
+            AssociatedElement::Rule { params, .. }
+            | AssociatedElement::Invariant { params, .. }
+            | AssociatedElement::Function { params, .. }
+            | AssociatedElement::Definition { params, .. } => Some(params),
+            _ => None,
+        }
+    }
+
+    pub fn block(&self) -> Option<&str> {
+        match self {
+            AssociatedElement::Rule { block, .. }
+            | AssociatedElement::Invariant { block, .. }
+            | AssociatedElement::Function { block, .. }
+            | AssociatedElement::Methods { block } => Some(block.as_str()),
+
+            AssociatedElement::Ghost { block, .. }
+            | AssociatedElement::GhostMapping { block, .. } => block.as_ref().map(String::as_str),
+
+            AssociatedElement::Definition { .. } => None, //TODO: return definition?
+        }
+    }
+
+    pub fn returns(&self) -> Option<&str> {
+        match self {
+            AssociatedElement::Function { returns, .. } => returns.as_ref().map(String::as_str),
+            AssociatedElement::Definition { returns, .. }
+            | AssociatedElement::Ghost { returns, .. } => Some(returns.as_str()),
+            _ => None,
+        }
+    }
+
+    pub fn ty_list(&self) -> Option<&[Ty]> {
+        match self {
+            AssociatedElement::Ghost { ty_list, .. } => Some(ty_list),
+            _ => None,
+        }
+    }
+}