Hax_engine.Phasesinclude sig ... endmodule Simplify_question_marks = Phase_simplify_question_marks.MakeIn THIR, there are no construct for question marks. Instead, Rustc desugars `e?` into the following:
module Local_mutation = Phase_local_mutation.Makemodule Specialize = Phase_specialize.MakeThis phase specializes certain specific method applications (according to their name and the type it is being used on) into plain functions.
module Newtype_as_refinement = Phase_newtype_as_refinement.MakeThis phase transforms annotated struct definitions into (refined) type aliases.
module Traits_specs = Phase_traits_specs.MakeThis phase adds specification to traits. For each method `f` in a trait, we add a `f_pre` and a `f_post`.
module Reconstruct_while_loops = Phase_reconstruct_while_loops.Makemodule Functionalize_loops = Phase_functionalize_loops.Makemodule Simplify_match_return = Phase_simplify_match_return.MakeThis phase rewrites `let pat = match ... ... => ..., ... => return ... ; e` into `match ... ... => let pat = ...; e`.
module Simplify_hoisting = Phase_simplify_hoisting.MakeThis phase rewrites `let pat = match ... ... => ..., ... => return ... ; e` into `match ... ... => let pat = ...; e`.
module Bundle_cycles = Phase_bundle_cycles.MakeThis 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 Rewrite_control_flow = Phase_rewrite_control_flow.MakeThis 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 Drop_match_guards = Phase_drop_match_guards.Makemodule Drop_references = Phase_drop_references.Makemodule Hoist_disjunctive_patterns = Phase_hoist_disjunctive_patterns.MakeThis phase eliminates nested disjunctive patterns (leaving only shallow disjunctions). It moves the disjunctions up to the top-level pattern.
module Drop_sized_trait = Phase_drop_sized_trait.MakeThis 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 Reconstruct_for_loops = Phase_reconstruct_for_loops.Makemodule Reconstruct_question_marks = Phase_reconstruct_question_marks.MakeIn THIR, there are no construct for question marks. Instead, Rustc desugars `e?` into the following:
module Reconstruct_asserts = Phase_reconstruct_asserts.MakeThis phase recognizes desugared `assert!(...)` to rewrite into `hax_lib::assert(..)`.
module And_mut_defsite = Phase_and_mut_defsite.Makemodule Drop_blocks = Phase_drop_blocks.Makemodule Trivialize_assign_lhs = Phase_trivialize_assign_lhs.Makemodule Cf_into_monads = Phase_cf_into_monads.Makemodule Reconstruct_for_index_loops = Phase_reconstruct_for_index_loops.Makemodule Direct_and_mut = Phase_direct_and_mut.Makemodule Transform_hax_lib_inline = Phase_transform_hax_lib_inline.MakeThis phase transforms nodes like:
module Drop_return_break_continue = Phase_drop_return_break_continue.MakeThis 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 Reject = Phase_reject