Module Hax_engine

module Analyses : sig ... end
module Ast : sig ... end
module Ast_builder : sig ... end
module Ast_builder_generated : sig ... end
module Ast_destruct : sig ... end
module Ast_destruct_generated : sig ... end
module Ast_utils : sig ... end
module Ast_visitors : sig ... end
module Attr_payloads : sig ... end
module Backend : sig ... end
module Concrete_ident : sig ... end

This module provides the global concrete identifiers.

module Concrete_ident_generated : sig ... end
module Concrete_ident_render_sig : sig ... end
module Concrete_ident_types : sig ... end
module Concrete_ident_view : sig ... end
module Concrete_ident_view_types : sig ... end

This modules defines what is the view over a concrete identifiers.

module Dependencies : sig ... end
module Deprecated_generic_printer : sig ... end
module Deprecated_generic_printer_base : sig ... end

Generic printer for the Ast ASTs. It uses the PPrint library, and additionally computes Annotation.t.

module Diagnostics : sig ... end
module Explicit_def_id : sig ... end

An ExplicitDefId.t is a Rust Types.def_id tagged with some diambiguation metadata. Explicit definition identifiers are used internally by the concrete names of hax.

module Feature_gate : sig ... end
module Features : sig ... end
module Function_dependency : sig ... end
module Generated_generic_printer_base : sig ... end
module Generic_printer : sig ... end
module Generic_printer_template : sig ... end
module Hax_io : sig ... end

This module helps communicating with `cargo-hax`.

module Impl_infos : sig ... end
module Import_thir : sig ... end
module Local_ident : sig ... end
module Mutable_variables : sig ... end
module Phase_and_mut_defsite : sig ... end
module Phase_bundle_cycles : sig ... end

This phase makes sure the items don't yield any cycle, namespace-wise. It does so by creating namespaces we call bundles, in which we regroup definitions that would otherwise yield cycles.

module Phase_cf_into_monads : sig ... end
module Phase_direct_and_mut : sig ... end
module Phase_drop_blocks : sig ... end
module Phase_drop_match_guards : sig ... end
module Phase_drop_references : sig ... end

This phase transforms `return e` expressions into `e` when `return e` is on an exit position. It should come after phase `RewriteControlFlow` and thus eliminate all `return`s. Inside loops it rewrites `return`, `break` and `continue` as their equivalent in terms of the `ControlFlow` wrapper that will be handled by the specific fold operators introduced by phase `FunctionalizeLoops`.

module Phase_drop_sized_trait : sig ... end

This phase remove any occurence to the `core::marker::sized` trait. This trait appears a lot, but is generally not very useful in our backends.

module Phase_functionalize_loops : sig ... end

This phase eliminates nested disjunctive patterns (leaving only shallow disjunctions). It moves the disjunctions up to the top-level pattern.

module Phase_local_mutation : sig ... end
module Phase_newtype_as_refinement : sig ... end

This phase transforms annotated struct definitions into (refined) type aliases.

module Phase_reconstruct_asserts : sig ... end

This phase recognizes desugared `assert!(...)` to rewrite into `hax_lib::assert(..)`.

module Phase_reconstruct_for_loops : sig ... end

In THIR, there are no construct for question marks. Instead, Rustc desugars `e?` into the following:

module Phase_reconstruct_while_loops : sig ... end
module Phase_reject : sig ... end
module Phase_rewrite_control_flow : sig ... end

This phase finds control flow expression (`if` or `match`) with a `return` expression in one of the branches. We replace them by replicating what comes after in all the branches. This allows the `return` to be eliminated by `drop_needless_returns`. This phase should come after `phase_local_mutation`.

module Phase_simplify_hoisting : sig ... end

This phase rewrites `let pat = match ... ... => ..., ... => return ... ; e` into `match ... ... => let pat = ...; e`.

module Phase_simplify_match_return : sig ... end

This phase rewrites `let pat = match ... ... => ..., ... => return ... ; e` into `match ... ... => let pat = ...; e`.

module Phase_simplify_question_marks : sig ... end

In THIR, there are no construct for question marks. Instead, Rustc desugars `e?` into the following:

module Phase_sort_items : sig ... end

This phase sorts items so that each item comes after the items it depends on. This is done by sorting namespaces with the same property, and then sorting items within each namespace, trying as much as possible to respect the original order.

module Phase_specialize : sig ... end

This phase specializes certain specific method applications (according to their name and the type it is being used on) into plain functions.

module Phase_traits_specs : sig ... end

This phase adds specification to traits. For each method `f` in a trait, we add a `f_pre` and a `f_post`.

module Phase_transform_hax_lib_inline : sig ... end

This phase transforms nodes like:

module Phase_trivialize_assign_lhs : sig ... end
module Phase_utils : sig ... end
module Phases : sig ... end
module Prelude : sig ... end
module Print_rust : sig ... end
module Profiling : sig ... end
module Side_effect_utils : sig ... end
module Span : sig ... end
module Subtype : sig ... end
module Thir_simple_types : sig ... end
module Types : sig ... end
module Utils : sig ... end