hax_frontend_exporter_options/
lib.rs

1use hax_adt_into::derive_group;
2use schemars::JsonSchema;
3
4#[derive_group(Serializers)]
5#[derive(Debug, Clone, JsonSchema)]
6pub enum Glob {
7    One,  // *
8    Many, // **
9}
10
11impl ToString for Glob {
12    fn to_string(&self) -> String {
13        match self {
14            Self::One => "*",
15            Self::Many => "**",
16        }
17        .to_string()
18    }
19}
20
21#[derive_group(Serializers)]
22#[derive(Debug, Clone, JsonSchema)]
23pub enum NamespaceChunk {
24    Glob(Glob),
25    Exact(String),
26}
27
28impl ToString for NamespaceChunk {
29    fn to_string(&self) -> String {
30        match self {
31            Self::Glob(glob) => glob.to_string(),
32            Self::Exact(string) => string.to_string(),
33        }
34    }
35}
36
37impl std::convert::From<&str> for NamespaceChunk {
38    fn from(s: &str) -> Self {
39        match s {
40            "*" => NamespaceChunk::Glob(Glob::One),
41            "**" => NamespaceChunk::Glob(Glob::Many),
42            _ => NamespaceChunk::Exact(String::from(s)),
43        }
44    }
45}
46
47#[derive_group(Serializers)]
48#[derive(Debug, Clone, JsonSchema)]
49pub struct Namespace {
50    pub chunks: Vec<NamespaceChunk>,
51}
52
53impl ToString for Namespace {
54    fn to_string(&self) -> String {
55        self.chunks
56            .iter()
57            .map(NamespaceChunk::to_string)
58            .collect::<Vec<_>>()
59            .join("::")
60            .to_string()
61    }
62}
63
64impl std::convert::From<String> for Namespace {
65    fn from(s: String) -> Self {
66        Namespace {
67            chunks: s
68                .split("::")
69                .filter(|s| !s.is_empty())
70                .map(NamespaceChunk::from)
71                .collect(),
72        }
73    }
74}
75
76impl Namespace {
77    pub fn matches(&self, path: &Vec<String>) -> bool {
78        fn aux(pattern: &[NamespaceChunk], path: &[String]) -> bool {
79            match (pattern, path) {
80                ([], []) => true,
81                ([NamespaceChunk::Exact(x), pattern @ ..], [y, path @ ..]) => {
82                    x == y && aux(pattern, path)
83                }
84                ([NamespaceChunk::Glob(Glob::One), pattern @ ..], [_, path @ ..]) => {
85                    aux(pattern, path)
86                }
87                ([NamespaceChunk::Glob(Glob::Many), pattern @ ..], []) => aux(pattern, path),
88                ([NamespaceChunk::Glob(Glob::Many), pattern_tl @ ..], [_path_hd, path_tl @ ..]) => {
89                    aux(pattern_tl, path) || aux(pattern, path_tl)
90                }
91                _ => false,
92            }
93        }
94        aux(self.chunks.as_slice(), path.as_slice())
95    }
96}
97
98#[derive(Debug, Clone)]
99pub struct Options {
100    /// Whether we should evaluate and inline the value of anonymous constants (inline `const {}`
101    /// blocks or advanced constant expressions as in `[T; N+1]`), or refer to them as
102    /// `GlobalName`s.
103    pub inline_anon_consts: bool,
104    /// Options related to bounds.
105    pub bounds_options: BoundsOptions,
106}
107
108#[derive(Debug, Clone, Copy)]
109pub struct BoundsOptions {
110    /// Add `T: Drop` bounds to every type generic, so that we can build `ImplExpr`s to know what
111    /// code is run on drop.
112    pub resolve_drop: bool,
113    /// Prune `T: Sized` and `T: MetaSized` predicates.
114    pub prune_sized: bool,
115}
hax_frontend_exporter_options/lib.rs

hax_frontend_exporter_options/
lib.rs
