Merge pull request #9 from Certora/fixed_invariants_and_types

Fixed invariants and types

Author: pickx

Cargo.toml

@@ -5,12 +5,14 @@ edition = "2021"
 
 [dependencies]
 chumsky = { git = "https://github.com/zesterer/chumsky" }
-clap = { version = "3.2.15", features = ["cargo", "derive"] }
+clap = { version = "3.2.17", features = ["cargo", "derive"] }
 color-eyre = "0.6.2"
-indoc = "1.0.6"
+indoc = "1.0.7"
 itertools = "0.10.3"
 lsp-types = "0.93.0"
+once_cell = "1.13.1"
+regex = "1.6.0"
 ropey = "1.5.0"
-serde = { version = "1.0.140", features = ["derive"] }
-serde_json = "1.0.82"
+serde = { version = "1.0.143", features = ["derive"] }
+serde_json = "1.0.83"
 tap = "1.0.1"

src/bin/main.rs

@@ -46,7 +46,8 @@ pub enum AssociatedElement {
         name: String,
         params: Vec<Param>,
         invariant: String,
-        block: String,
+        filters: Option<String>,
+        block: Option<String>,
     },
     Function {
         name: String,
@@ -259,11 +260,11 @@ impl AssociatedElement {
     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::Invariant { block, .. }
+            | AssociatedElement::Ghost { block, .. }
             | AssociatedElement::GhostMapping { block, .. } => block.as_ref().map(String::as_str),
 
             AssociatedElement::Definition { .. } => None, //TODO: return definition?
@@ -285,4 +286,33 @@ impl AssociatedElement {
             _ => None,
         }
     }
+
+    pub fn filters(&self) -> Option<&str> {
+        match self {
+            AssociatedElement::Rule { filters, .. }
+            | AssociatedElement::Invariant { filters, .. } => filters.as_ref().map(String::as_str),
+            _ => None,
+        }
+    }
+
+    pub fn invariant(&self) -> Option<&str> {
+        match self {
+            AssociatedElement::Invariant { invariant, .. } => Some(invariant.as_str()),
+            _ => None,
+        }
+    }
+
+    pub fn mapping(&self) -> Option<&str> {
+        match self {
+            AssociatedElement::GhostMapping { mapping, .. } => Some(mapping.as_str()),
+            _ => None,
+        }
+    }
+
+    pub fn definition(&self) -> Option<&str> {
+        match self {
+            AssociatedElement::Definition { definition, .. } => Some(definition.as_str()),
+            _ => None,
+        }
+    }
 }