flux_syntax/
symbols.rs

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

flux_syntax/
symbols.rs
