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        RefinedBy: "refined_by",
18        Axiom: "axiom",
19    }
20
21    Symbols {
22        Map,
23        Set,
24        addr,
25        base,
26        cast,
27        int,
28        no_panic,
29        no_panic_if,
30        real,
31    }
32}
33
34/// All Rust keywords plus extra Flux keywords.
35pub mod kw {
36    #![allow(non_upper_case_globals)]
37
38    use rustc_span::Symbol;
39    pub use rustc_span::symbol::kw::*;
40
41    pub use super::kw_generated::*;
42
43    // Predefined symbols in rustc that are not Rust keywords but are Flux keywords.
44    // Update this in tandem with `is_flux_reserved`
45    pub const Opaque: Symbol = rustc_span::symbol::sym::opaque;
46    pub const Local: Symbol = rustc_span::symbol::sym::local;
47    pub const Exists: Symbol = rustc_span::symbol::sym::exists;
48    pub const Forall: Symbol = rustc_span::symbol::sym::forall;
49
50    // Predefined symbols in rustc that are Flux keywords but are not reserved.
51    pub const Invariant: Symbol = rustc_span::symbol::sym::invariant;
52}
53
54pub mod sym {
55    pub use rustc_span::sym::*;
56
57    pub use super::sym_generated::*;
58}
59
60pub fn is_reserved(sym: Symbol, edition: Edition) -> bool {
61    // FIXME: We should treat these as reserved and adjust the parser to be consistent with Rust.
62    if sym == kw::SelfLower || sym == kw::SelfUpper || sym == kw::Crate || sym == kw::Super {
63        return false;
64    }
65    sym.is_reserved(|| edition) || is_flux_reserved(sym)
66}
67
68// Update in tandem with predefined non-keyword symbols in `kw`
69fn is_flux_reserved(sym: Symbol) -> bool {
70    (kw::Bitvec <= sym && sym <= kw::Strg)
71        || sym == kw::Opaque
72        || sym == kw::Local
73        || sym == kw::Exists
74        || sym == kw::Forall
75}
flux_syntax/symbols.rs

flux_syntax/
symbols.rs
