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
module Concrete_ident_generated : sig ... end
module Concrete_ident_sig : sig ... end
module Dependencies : sig ... end
module Diagnostics : sig ... end
module Feature_gate : sig ... end
module Features : sig ... end
module Function_dependency : sig ... end
module Generic_printer : sig ... end
module Generic_printer_base : sig ... end

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

module Hax_io : sig ... end
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_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_needless_returns : sig ... end

This phase transforms `return e` expressions into `e` when `return e` is on an exit position.

module Phase_drop_references : sig ... end
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_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 Side_effect_utils : sig ... end
module Span : sig ... end
module Subtype : sig ... end
module Types : sig ... end
module Utils : sig ... end