flux_syntax/
symbols.rs

1use flux_macros::symbols;
2use rustc_span::{Symbol, edition::Edition};
3
4symbols! {
5    Keywords {
6        Bitvec: "bitvec",
7        Hrn: "hrn",
8        Hdl: "hdl",
9        Requires: "requires",
10        Ensures: "ensures",
11        Property: "property",
12        Qualifier: "qualifier",
13        Sort: "sort",
14        Strg: "strg",
15        Trusted: "trusted",
16        Reft: "reft",
17        Invariant: "invariant",
18        RefinedBy: "refined_by",
19        Axiom: "axiom",
20    }
21
22    Symbols {
23        Map,
24        Set,
25        addr,
26        base,
27        cast,
28        int,
29        no_panic,
30        no_panic_if,
31        real,
32    }
33}
34
35/// All Rust keywords plus extra Flux keywords.
36pub mod kw {
37    #![allow(non_upper_case_globals)]
38
39    use rustc_span::Symbol;
40    pub use rustc_span::symbol::kw::*;
41
42    pub use super::kw_generated::*;
43
44    // Predefined symbols in rustc that are not Rust keywords but are Flux keywords.
45    // Update this in tandem with `is_flux_reserved`
46    pub const Opaque: Symbol = rustc_span::symbol::sym::opaque;
47    pub const Local: Symbol = rustc_span::symbol::sym::local;
48    pub const Exists: Symbol = rustc_span::symbol::sym::exists;
49    pub const Forall: Symbol = rustc_span::symbol::sym::forall;
50}
51
52pub mod sym {
53    pub use rustc_span::sym::*;
54
55    pub use super::sym_generated::*;
56}
57
58pub fn is_reserved(sym: Symbol, edition: Edition) -> bool {
59    // FIXME: We should treat these as reserved and adjust the parser to be consistent with Rust.
60    if sym == kw::SelfLower || sym == kw::SelfUpper || sym == kw::Crate || sym == kw::Super {
61        return false;
62    }
63    sym.is_reserved(|| edition) || is_flux_reserved(sym)
64}
65
66// Update in tandem with predefined non-keyword symbols in `kw`
67fn is_flux_reserved(sym: Symbol) -> bool {
68    (kw::Bitvec <= sym && sym <= kw::Strg)
69        || sym == kw::Opaque
70        || sym == kw::Local
71        || sym == kw::Exists
72        || sym == kw::Forall
73}
flux_syntax/symbols.rs

flux_syntax/
symbols.rs
