[wip] uninterp marker on uniterpreted spec fns

verus-lang · Feb 27, 2025 · 4c45266 · 4c45266
1 parent 65f122f
commit 4c45266
Show file tree

Hide file tree

Showing 19 changed files with 249 additions and 26 deletions.
diff --git a/dependencies/syn/src/gen/clone.rs b/dependencies/syn/src/gen/clone.rs
diff --git a/dependencies/syn/src/gen/debug.rs b/dependencies/syn/src/gen/debug.rs
diff --git a/dependencies/syn/src/gen/eq.rs b/dependencies/syn/src/gen/eq.rs
diff --git a/dependencies/syn/src/gen/fold.rs b/dependencies/syn/src/gen/fold.rs
diff --git a/dependencies/syn/src/gen/hash.rs b/dependencies/syn/src/gen/hash.rs
diff --git a/dependencies/syn/src/gen/token.css b/dependencies/syn/src/gen/token.css
diff --git a/dependencies/syn/src/gen/visit.rs b/dependencies/syn/src/gen/visit.rs
diff --git a/dependencies/syn/src/gen/visit_mut.rs b/dependencies/syn/src/gen/visit_mut.rs
diff --git a/dependencies/syn/src/lib.rs b/dependencies/syn/src/lib.rs
@@ -559,7 +559,7 @@ pub use crate::verus::{
     InvariantNameSetNone, ItemBroadcastGroup, MatchesOpExpr, MatchesOpToken, Mode, ModeExec,
     ModeGhost, ModeProof, ModeSpec, ModeSpecChecked, ModeTracked, Open, OpenRestricted, Prover,
     Publish, Recommends, Requires, Returns, RevealHide, SignatureDecreases, SignatureInvariants,
-    SignatureSpec, SignatureSpecAttr, SignatureUnwind, Specification, TypeFnSpec, View,
+    SignatureSpec, SignatureSpecAttr, SignatureUnwind, Specification, TypeFnSpec, Uninterp, View,
 };
 
 #[rustfmt::skip] // https://github.com/rust-lang/rustfmt/issues/6176

diff --git a/dependencies/syn/src/token.rs b/dependencies/syn/src/token.rs
@@ -748,6 +748,7 @@ define_keywords! {
     "exec"        pub struct Exec
     "open"        pub struct Open
     "closed"      pub struct Closed
+    "uninterp"    pub struct Uninterp
     "ghost"       pub struct Ghost
     "tracked"     pub struct Tracked
     "requires"    pub struct Requires
@@ -1031,6 +1032,7 @@ macro_rules! Token {
     [exec]        => { $crate::token::Exec };
     [open]        => { $crate::token::Open };
     [closed]      => { $crate::token::Closed };
+    [uninterp]    => { $crate::token::Uninterp };
     [ghost]       => { $crate::token::Ghost };
     [tracked]     => { $crate::token::Tracked };
     [requires]    => { $crate::token::Requires };

diff --git a/dependencies/syn/src/verus.rs b/dependencies/syn/src/verus.rs
@@ -7,6 +7,7 @@ ast_enum_of_structs! {
         Closed(Closed),
         Open(Open),
         OpenRestricted(OpenRestricted),
+        Uninterp(Uninterp),
         Default,
     }
 }
@@ -32,6 +33,12 @@ ast_struct! {
     }
 }
 
+ast_struct! {
+    pub struct Uninterp {
+        pub token: Token![uninterp],
+    }
+}
+
 ast_enum_of_structs! {
     pub enum Mode {
         Spec(ModeSpec),
@@ -503,6 +510,9 @@ pub mod parsing {
                 } else {
                     Ok(Publish::Open(Open { token }))
                 }
+            } else if input.peek(Token![uninterp]) {
+                let token = input.parse::<Token![uninterp]>()?;
+                Ok(Publish::Uninterp(Uninterp { token }))
             } else {
                 Ok(Publish::Default)
             }
@@ -1414,6 +1424,12 @@ mod printing {
         }
     }
 
+    impl ToTokens for Uninterp {
+        fn to_tokens(&self, tokens: &mut TokenStream) {
+            self.token.to_tokens(tokens);
+        }
+    }
+
     #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))]
     impl ToTokens for ModeSpec {
         fn to_tokens(&self, tokens: &mut TokenStream) {

diff --git a/dependencies/syn/syn.json b/dependencies/syn/syn.json
diff --git a/dependencies/syn/tests/debug/gen.rs b/dependencies/syn/tests/debug/gen.rs
diff --git a/source/builtin_macros/src/rustdoc.rs b/source/builtin_macros/src/rustdoc.rs
@@ -185,6 +185,7 @@ fn fn_mode_to_string(mode: &FnMode, publish: &Publish) -> String {
             Publish::OpenRestricted(res) => {
                 "open(".to_string() + &module_path_to_string(&res.path) + ") spec"
             }
+            Publish::Uninterp(_) => "uninterp".to_string(),
             Publish::Default => "spec".to_string(),
         },
         FnMode::Proof(_) => "proof".to_string(),