hax_rust_engine/
names.rs

1//! This module provides a list of handy `DefId` for the engine.
2//! The list of `DefId`s comes from the crate `/engine/names`: any name mentionned
3//! in that crate will be provided here automatically.
4//!
5//! For example, to be able to resugar `std::ops::Add::add(x, y)` into `x + y`,
6//! we need to:
7//!  1. match on the expression `std::ops::Add::add(x, y)`, figure out it is the
8//!     application of the function denoted by the global identifier
9//!     `std::ops::Add::add` with arguments `x` and `y`.
10//!  2. check that global identifier `id: GlobalId` `std::ops::Add::add` is
11//!     indeed `std::ops::Add::add`.
12//!
13//! Point (2.) seems a bit tautological, but we need to write a comparison like
14//! `some_id == the_function_add`. This module basically provides such
15//! `the_function_add` symbols.
16//!
17//! As an example, the names `std::option::Option::Some` and `None` will be provided by this module as:
18//! ```rust,ignore
19//! mod std {
20//!     mod option {
21//!         mod Option {
22//!             fn Some() -> DefId { ... }
23//!             fn None() -> DefId { ... }
24//!         }
25//!     }
26//! }
27//! ```
28
29pub use crate::ast::identifiers::global_id::generated_names::{codegen, root::*};
hax_rust_engine/names.rs

hax_rust_engine/
names.rs
