Merge pull request #26 from Certora/panic_in_the_display

Panic! in the Display

Author: pickx

.gitignore

@@ -3,3 +3,4 @@
 **/.DS_Store
 BUGS
 **/python_wrapper/.env
+**/tests

CHANGELOG.md

@@ -1,6 +1,12 @@
 # Changelog
+<<<<<<< HEAD
+## [0.6.5] - 2023-01-09 
+### Fixed
+- Use span-based capturing for `Definition`
+=======
 ## [1.0.0] - 2022-12-20
 - Release Candidate for first public version
+>>>>>>> master
 
 ## [0.6.4] - 2022-12-14
 ### Fixed

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "cvldoc_parser_core"
-version = "1.0.0"
+version = "0.6.5"
 edition = "2021"
 
 [dependencies]

src/parse/builder.rs

@@ -298,6 +298,8 @@ impl<'src> Builder<'src> {
                 returns,
                 definition,
             } => {
+                let definition = self.owned_slice(definition);
+
                 let ast = Ast::Definition {
                     name,
                     params,

src/parse/mod.rs

@@ -273,7 +273,7 @@ fn decl_parser() -> impl Parser<Token, Intermediate, Error = Simple<Token>> {
         let rhs = none_of(Token::Semicolon)
             .at_least_once()
             .then_ignore(just(Token::Semicolon))
-            .map(String::from_iter);
+            .map_with_span(|_, span| span);
 
         just(Token::Definition)
             .ignore_then(ident())

src/parse/types.rs

@@ -41,36 +41,41 @@ pub enum Token {
 
 impl Display for Token {
     fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
-        let s = match self {
-            Token::Ghost => "ghost",
-            Token::Definition => "definition",
-            Token::Rule => "rule",
-            Token::Invariant => "invariant",
-            Token::Methods => "methods",
-            Token::Function => "function",
-            Token::Mapping => "mapping",
-            Token::Returns => "returns",
-            Token::Filtered => "filtered",
-            Token::Ident(data) | Token::Other(data) | Token::Number(data) => data.as_str(),
-            Token::RoundOpen => "(",
-            Token::RoundClose => ")",
-            Token::SquareOpen => "[",
-            Token::SquareClose => "]",
-            Token::CurlyOpen => "{",
-            Token::CurlyClose => "}",
-            Token::Dot => ".",
-            Token::Comma => ",",
-            Token::Semicolon => ";",
-            Token::Equals => "=",
-            Token::Arrow => "=>",
-            Token::Axiom => "axiom",
-            Token::Using => "using",
-            Token::Hook => "hook",
-            Token::Preserved => "preserved",
-            _ => panic!("{self:?}"),
-        };
+        match self {
+            Token::Ghost => write!(f, "ghost"),
+            Token::Definition => write!(f, "definition"),
+            Token::Rule => write!(f, "rule"),
+            Token::Invariant => write!(f, "invariant"),
+            Token::Methods => write!(f, "methods"),
+            Token::Function => write!(f, "function"),
+            Token::Mapping => write!(f, "mapping"),
+            Token::Returns => write!(f, "returns"),
+            Token::Filtered => write!(f, "filtered"),
+            Token::RoundOpen => write!(f, "("),
+            Token::RoundClose => write!(f, ")"),
+            Token::SquareOpen => write!(f, "["),
+            Token::SquareClose => write!(f, "]"),
+            Token::CurlyOpen => write!(f, "{{"),
+            Token::CurlyClose => write!(f, "}}"),
+            Token::Dot => write!(f, "."),
+            Token::Comma => write!(f, ","),
+            Token::Semicolon => write!(f, ";"),
+            Token::Equals => write!(f, "="),
+            Token::Arrow => write!(f, "=>"),
+            Token::Axiom => write!(f, "axiom"),
+            Token::Using => write!(f, "using"),
+            Token::Hook => write!(f, "hook"),
+            Token::Preserved => write!(f, "preserved"),
 
-        write!(f, "{s}")
+            Token::Ident(data) | Token::Other(data) | Token::Number(data) => write!(f, "{data}"),
+
+            Token::CvlDocSlashed
+            | Token::CvlDocStarred
+            | Token::FreeFormSlashed
+            | Token::FreeFormStarred
+            | Token::SingleLineComment
+            | Token::MultiLineComment => write!(f, "{self:?}"),
+        }
     }
 }
 
@@ -112,7 +117,7 @@ pub enum Intermediate {
         name: String,
         params: Vec<(String, Option<String>)>,
         returns: String,
-        definition: String,
+        definition: Span,
     },
     Invariant {
         name: String,

src/python_wrapper/CHANGELOG.md

@@ -1,6 +1,7 @@
 # Changelog
-## [1.0.0] - 2022-12-20
-- Release Candidate for first public version
+## [0.6.5] - 2023-01-09 
+### Fixed
+- Bugfix in core
 
 ## [0.6.4] - 2022-12-14
 ### Fixed

src/python_wrapper/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "cvldoc_parser_py"
-version = "1.0.0"
+version = "0.6.5"
 edition = "2021"
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

src/python_wrapper/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "maturin"
 
 [project]
 name = "cvldoc_parser"
-version = "1.0.0"
+version = "0.6.5"
 requires-python = ">=3.7"
 classifiers = [
     "Programming Language :: Rust",