anodized_core/annotate/
syntax.rs

1use syn::{
2    FieldValue, Ident, Member, Token,
3    parse::{Parse, ParseStream, Result},
4    punctuated::Punctuated,
5};
6
7/// Raw spec fields, i.e. as they appear in the `#[spec(...)]` proc macro invocation.
8///
9/// Represents a syntactically well-formed but otherwise unvalidated set of `spec` fields.
10///
11/// It reuses Rust's grammar of fields inside a `struct` expression. For reference, see:
12///
13/// <https://doc.rust-lang.org/reference/expressions/struct-expr.html#railroad-StructExprField>
14#[derive(Debug, Clone)]
15pub struct SpecFields {
16    pub fields: Punctuated<FieldValue, Token![,]>,
17}
18
19impl Parse for SpecFields {
20    fn parse(input: ParseStream) -> Result<Self> {
21        Ok(Self {
22            fields: Punctuated::<FieldValue, Token![,]>::parse_terminated(input)?,
23        })
24    }
25}
26
27impl SpecFields {
28    /// Check whether the spec fields are sorted correctly, ignoring unknown keywords.
29    pub fn is_sorted(&self) -> bool {
30        self.fields
31            .iter()
32            .map(|field| Keyword::from(&field.member))
33            .filter(|keyword| !matches!(keyword, Keyword::Unknown(_)))
34            .is_sorted()
35    }
36}
37
38#[derive(Debug, Clone, Eq, PartialEq, Ord, PartialOrd)]
39pub enum Keyword {
40    Unknown(Ident),
41    Functional,
42    Pure,
43    Total,
44    Deterministic,
45    Effectfree,
46    Infallible,
47    Terminating,
48    Requires,
49    Maintains,
50    Captures,
51    // TODO: Remove `binds` and `inspects` before v0.7.0 is released.
52    Binds,
53    Inspects,
54    Ensures,
55    Decreases,
56}
57
58impl From<&Member> for Keyword {
59    fn from(value: &Member) -> Self {
60        use Keyword::*;
61        match value {
62            Member::Named(ident) if ident == "functional" => Functional,
63            Member::Named(ident) if ident == "pure" => Pure,
64            Member::Named(ident) if ident == "total" => Total,
65            Member::Named(ident) if ident == "deterministic" => Deterministic,
66            Member::Named(ident) if ident == "effectfree" => Effectfree,
67            Member::Named(ident) if ident == "infallible" => Infallible,
68            Member::Named(ident) if ident == "terminating" => Terminating,
69            Member::Named(ident) if ident == "requires" => Requires,
70            Member::Named(ident) if ident == "maintains" => Maintains,
71            Member::Named(ident) if ident == "captures" => Captures,
72            Member::Named(ident) if ident == "binds" => Binds,
73            Member::Named(ident) if ident == "inspects" => Inspects,
74            Member::Named(ident) if ident == "ensures" => Ensures,
75            Member::Named(ident) if ident == "decreases" => Decreases,
76            Member::Named(ident) => Unknown(ident.clone()),
77            Member::Unnamed(index) => Unknown(Ident::new(&format!("{}", index.index), index.span)),
78        }
79    }
80}
81
82impl std::fmt::Display for Keyword {
83    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
84        match self {
85            Keyword::Unknown(ident) => write!(f, "{}", ident),
86            Keyword::Functional => write!(f, "functional"),
87            Keyword::Pure => write!(f, "pure"),
88            Keyword::Total => write!(f, "total"),
89            Keyword::Deterministic => write!(f, "deterministic"),
90            Keyword::Effectfree => write!(f, "effectfree"),
91            Keyword::Infallible => write!(f, "infallible"),
92            Keyword::Terminating => write!(f, "terminating"),
93            Keyword::Requires => write!(f, "requires"),
94            Keyword::Maintains => write!(f, "maintains"),
95            Keyword::Captures => write!(f, "captures"),
96            Keyword::Binds => write!(f, "binds"),
97            Keyword::Inspects => write!(f, "inspects"),
98            Keyword::Ensures => write!(f, "ensures"),
99            Keyword::Decreases => write!(f, "decreases"),
100        }
101    }
102}
anodized_core/annotate/syntax.rs

anodized_core/annotate/
syntax.rs
