Hax_engine.Phasesinclude sig ... endmodule Newtype_as_refinement = Phase_newtype_as_refinement.MakeThis phase transforms annotated struct definitions into (refined) type aliases.
module Transform_hax_lib_inline = Phase_transform_hax_lib_inline.MakeThis phase transforms nodes like:
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 Trivialize_assign_lhs = Phase_trivialize_assign_lhs.Makemodule And_mut_defsite = Phase_and_mut_defsite.Makemodule Drop_references = Phase_drop_references.Makemodule Cf_into_monads = Phase_cf_into_monads.Makemodule Drop_blocks = Phase_drop_blocks.Makemodule Reconstruct_while_loops = Phase_reconstruct_while_loops.Makemodule Simplify_hoisting = Phase_simplify_hoisting.MakeThis phase rewrites `let pat = match ... ... => ..., ... => return ... ; e` into `match ... ... => let pat = ...; e`.
module Reconstruct_asserts = Phase_reconstruct_asserts.MakeThis phase recognizes desugared `assert!(...)` to rewrite into `hax_lib::assert(..)`.
module Functionalize_loops = Phase_functionalize_loops.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 Direct_and_mut = Phase_direct_and_mut.Makemodule Local_mutation = Phase_local_mutation.Makemodule Simplify_question_marks = Phase_simplify_question_marks.MakeIn THIR, there are no construct for question marks. Instead, Rustc desugars `e?` into the following:
module Sort_items = Phase_sort_items.MakeThis 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 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 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 Reconstruct_for_index_loops = Phase_reconstruct_for_index_loops.Makemodule 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 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 Reconstruct_for_loops = Phase_reconstruct_for_loops.Makemodule 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 Simplify_match_return = Phase_simplify_match_return.MakeThis phase rewrites `let pat = match ... ... => ..., ... => return ... ; e` into `match ... ... => let pat = ...; e`.
module Reconstruct_question_marks = Phase_reconstruct_question_marks.MakeIn THIR, there are no construct for question marks. Instead, Rustc desugars `e?` into the following:
module Reject = Phase_reject