hax_lib_macros/
hax_paths.rs

1//! This module defines the `ImplFnDecoration` structure and utils
2//! around it.
3
4use syn::spanned::Spanned;
5use syn::*;
6
7fn expect_simple_path(path: &Path) -> Option<Vec<String>> {
8    let mut chunks = vec![];
9    if path.leading_colon.is_some() {
10        chunks.push(String::new())
11    }
12    for segment in &path.segments {
13        chunks.push(format!("{}", segment.ident));
14        if !matches!(segment.arguments, PathArguments::None) {
15            return None;
16        }
17    }
18    Some(chunks)
19}
20
21/// The various strings allowed as decoration kinds.
22pub const DECORATION_KINDS: &[&str] = &["decreases", "ensures", "requires"];
23
24/// Expects a `Path` to be a decoration kind: `::hax_lib::<KIND>`,
25/// `hax_lib::<KIND>` or `<KIND>` in (with `KIND` in
26/// `DECORATION_KINDS`).
27pub fn expects_path_decoration(path: &Path) -> Result<Option<String>> {
28    expects_hax_path(DECORATION_KINDS, path)
29}
30
31/// Expects a path to be `[[::]hax_lib]::refine`
32pub fn expects_refine(path: &Path) -> Result<Option<String>> {
33    expects_hax_path(&["refine"], path)
34}
35
36/// Expects a path to be `[[::]hax_lib]::order`
37pub fn expects_order(path: &Path) -> Result<Option<String>> {
38    expects_hax_path(&["order"], path)
39}
40
41/// Expects a `Path` to be a hax path: `::hax_lib::<KW>`,
42/// `hax_lib::<KW>` or `<KW>` in (with `KW` in `allowlist`).
43pub fn expects_hax_path(allowlist: &[&str], path: &Path) -> Result<Option<String>> {
44    let path_span = path.span();
45    let path = expect_simple_path(path)
46        .ok_or_else(|| Error::new(path_span, "Expected a simple path, with no `<...>`."))?;
47    Ok(
48        match path
49            .iter()
50            .map(|x| x.as_str())
51            .collect::<Vec<_>>()
52            .as_slice()
53        {
54            [kw] | ["", "hax_lib", kw] | ["hax_lib", kw] if allowlist.contains(kw) => {
55                Some(kw.to_string())
56            }
57            _ => None,
58        },
59    )
60}
hax_lib_macros/hax_paths.rs

hax_lib_macros/
hax_paths.rs
