update syntax for CVL2 changes

.circleci/config.yml

@@ -2,11 +2,11 @@ defines:
   smoke-test: &smoke-test
     name: Smoke test
     command: |
-      wget https://raw.githubusercontent.com/Certora/natspecTools/master/tests/basic_tests/definition_test.spec
+      wget https://raw.githubusercontent.com/Certora/cvldocTool/master/tests/basic_tests/definition_test.spec
 
       python -c "import cvldoc_parser
-      parsed = cvldoc_parser.parse([\"definition_test.spec\"])
-      assert len(parsed[0]) == 3, \"should parse to 3 elements\""
+      parsed = cvldoc_parser.parse(\"definition_test.spec\")
+      assert len(parsed) == 3, \"should parse to 3 elements\""
 
   store-and-persist:
     - store_artifacts: &store-wheel
@@ -23,7 +23,7 @@ orbs:
 jobs:
   unit-tests:
     docker:
-      - image: cimg/rust:1.65.0
+      - image: cimg/rust:1.72.0
     steps:
       - checkout
       - run:
@@ -49,9 +49,10 @@ jobs:
             PYPROJ_VER=$(rg '^version = "(.+)"$' -o -r '$1' ${PYTHON_MODULE_DIR}/pyproject.toml)
 
             [[ $CORE_CARGOTOML_VER == $LATEST_CHANGELOG_VER ]] || fail "Core Cargo.toml version (${CORE_CARGOTOML_VER}) doesn't match latest version in CHANGELOG (${CORE_LATEST_CHANGELOG_VER})"
-            [[ $MODULE_CARGOTOML_VER == $PYPROJ_VER ]] || fail "Python Module Cargo.toml version (${MODULE_CARGOTOML_VER}) doesn't match pyproject.toml version (${PYPROJ_VER})"
             [[ $CORE_CARGOTOML_VER == $MODULE_CARGOTOML_VER ]] || fail "Core Cargo.toml version (${CORE_CARGOTOML_VER}) doesn't match module Cargo.toml version (${MODULE_CARGOTOML_VER})"
 
+            # [[ $MODULE_CARGOTOML_VER == $PYPROJ_VER ]] || fail "Python Module Cargo.toml version (${MODULE_CARGOTOML_VER}) doesn't match pyproject.toml version (${PYPROJ_VER})"
+
             exit $status
       - run:
           name: Check code formatting
@@ -172,7 +173,7 @@ jobs:
           at: .
       - run: 
           name: Install dependencies
-          command: choco install wget
+          command: choco install wget -y
           shell: bash.exe
       - run:
           name: Install wheel

.gitignore

@@ -2,5 +2,4 @@
 **/Cargo.lock
 **/.DS_Store
 BUGS
-**/python_wrapper/.env
-**/tests
+**/.env

CHANGELOG.md

@@ -1,4 +1,13 @@
 # Changelog
+## [2.0.0] - 2023-09-13
+### Added
+- Support parsing of `hook`, `use`, `using`, `import` statements.
+- Python module API has been simplified.
+### Changed
+- CVL2 syntax is now enforced. Parsing of code which is not compliant with CVL2 has been removed.
+### Fixed
+- Some issues with `Invariant` parsing have been fixed.
+
 ## [1.0.3] - 2023-05-27
 ### Fixed
 - Fix issue that could cause infinite recursion on certain input

Cargo.toml

@@ -1,17 +1,17 @@
 [package]
 name = "cvldoc_parser_core"
-version = "1.0.3"
+version = "2.0.0"
 edition = "2021"
 
 [dependencies]
 assert_matches = "1.5.0"
 chumsky = "0.9.2"
 color-eyre = "0.6.2"
-indoc = "2.0.1"
-itertools = "0.10.5"
+indoc = "2"
+itertools = "0.11"
 lsp-types = "0.94.0"
 once_cell = "1.17.1"
-regex = "1.8.2"
+regex = "1"
 ropey = "1.6.0"
-serde = { version = "1.0.163", features = ["derive"] }
-tap = "1.0.1"
+serde = { version = "1", features = ["derive"] }
+tap = "1"

src/diagnostics.rs

@@ -10,32 +10,36 @@ impl Ast {
             Ast::Invariant { .. } => &[Title, Notice, Dev, Param],
             Ast::Function { .. } => &[Notice, Dev, Param, Return],
             Ast::Definition { .. } => &[Notice, Dev, Param, Return],
-            Ast::Ghost { .. } | Ast::GhostMapping { .. } => &[Notice, Dev, Param, Return],
+            Ast::GhostFunction { .. } | Ast::GhostMapping { .. } => &[Notice, Dev, Param, Return],
             Ast::Methods { .. } => &[Notice, Dev],
-            Ast::FreeFormComment { .. } => todo!(),
+            Ast::FreeFormComment { .. } => &[Notice, Dev],
+            Ast::Import { .. }
+            | Ast::Using { .. }
+            | Ast::UseRule { .. }
+            | Ast::UseBuiltinRule { .. }
+            | Ast::UseInvariant { .. }
+            | Ast::HookSload { .. }
+            | Ast::HookSstore { .. }
+            | Ast::HookCreate { .. }
+            | Ast::HookOpcode { .. } => &[Dev],
         }
     }
 
     fn supports(&self, tag: &TagKind) -> bool {
         self.supported_tags().contains(tag)
     }
 
-    fn defines_param(&self, param: &str) -> bool {
-        self.params()
-            .map(|params| {
-                params
-                    .iter()
-                    .filter_map(|(_ty, name)| name.as_ref())
-                    .any(|name| name == param)
-            })
-            .unwrap_or(false)
+    fn defines_param(&self, param_name: &str) -> bool {
+        if let Some(params) = self.params() {
+            params.iter().any(|param| param.name == param_name)
+        } else {
+            false
+        }
     }
 }
 
-const WARNING: DiagnosticSeverity = DiagnosticSeverity::WARNING;
-const ERROR: DiagnosticSeverity = DiagnosticSeverity::ERROR;
-
 enum DiagSpan<'a> {
+    #[allow(unused)]
     EntireDoc,
     SingleTag(&'a DocumentationTag),
 }
@@ -44,58 +48,52 @@ impl CvlElement {
     pub fn enumerate_diagnostics(&self, converter: RangeConverter) -> Vec<Diagnostic> {
         let mut diagnostics = Vec::new();
 
-        if let Some(doc) = &self.doc {
-            let mut add = |message, diag_span, severity| {
-                let span = match diag_span {
-                    DiagSpan::EntireDoc => self.element_span.clone(),
-                    DiagSpan::SingleTag(tag) => tag.span.clone(),
-                };
-
-                let diag = Diagnostic {
-                    range: converter.to_range(span),
-                    severity: Some(severity),
-                    message,
-                    ..Default::default()
-                };
-                diagnostics.push(diag);
+        let mut add = |message, diag_span, severity| {
+            let span = match diag_span {
+                DiagSpan::EntireDoc => self.element_span.clone(),
+                DiagSpan::SingleTag(tag) => tag.span.clone(),
             };
 
-            if doc.iter().all(|tag| tag.kind != TagKind::Notice) {
-                //Any applicable item is missing a notice
-                let message = "associated element is undocumented".to_string();
-                add(message, DiagSpan::EntireDoc, WARNING);
-            }
+            let diag = Diagnostic {
+                range: converter.to_range(span),
+                severity: Some(severity),
+                message,
+                ..Default::default()
+            };
+            diagnostics.push(diag);
+        };
 
-            let tags_with_params = doc.iter().filter_map(|tag| {
-                let param = tag.param_name()?;
-                Some((tag, param))
-            });
+        // disabled for now. this diagnostic is overly broad.
+        // if self.doc.iter().all(|tag| tag.kind != TagKind::Notice) {
+        //     //Any applicable item is missing a notice
+        //     let message = "associated element is undocumented".to_string();
+        //     add(message, DiagSpan::EntireDoc, WARNING);
+        // }
 
-            for (i, (tag, param)) in tags_with_params.enumerate() {
-                if !self.ast.defines_param(param) {
-                    //A @param is provided for a non-existent parameter
-                    let message = format!("no such parameter: {param}");
-                    add(message, DiagSpan::SingleTag(tag), ERROR);
-                } else if doc[..i].iter().any(|tag| tag.param_name() == Some(param)) {
-                    //Each parameter must be documented at most once
-                    let message = "parameter is already documented".to_string();
-                    add(message, DiagSpan::SingleTag(tag), ERROR);
-                }
-            }
+        let tags_with_params = self.doc.iter().filter_map(|tag| {
+            let param = tag.param_name()?;
+            Some((tag, param))
+        });
 
-            for tag in doc {
-                if !self.ast.supports(&tag.kind) {
-                    let message = format!("this tag is unsupported for {} blocks", self.ast);
-                    add(message, DiagSpan::SingleTag(tag), ERROR);
-                }
+        for (i, (tag, param)) in tags_with_params.enumerate() {
+            if !self.ast.defines_param(param) {
+                //A @param is provided for a non-existent parameter
+                let message = format!("no such parameter: {param}");
+                add(message, DiagSpan::SingleTag(tag), DiagnosticSeverity::ERROR);
+            } else if self.doc[..i]
+                .iter()
+                .any(|tag| tag.param_name() == Some(param))
+            {
+                //Each parameter must be documented at most once
+                let message = "parameter is already documented".to_string();
+                add(message, DiagSpan::SingleTag(tag), DiagnosticSeverity::ERROR);
             }
+        }
 
-            for tag in doc {
-                if let TagKind::Unexpected(unexpected_tag) = &tag.kind {
-                    //Unrecognized tags appear anywhere
-                    let message = format!("@{unexpected_tag} is unrecognized");
-                    add(message, DiagSpan::SingleTag(tag), WARNING);
-                }
+        for tag in &self.doc {
+            if !self.ast.supports(&tag.kind) {
+                let message = format!("this tag is unsupported for {} blocks", self.ast);
+                add(message, DiagSpan::SingleTag(tag), DiagnosticSeverity::ERROR);
             }
         }