Hax_engine.Phasesinclude sig ... endmodule 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_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 Trivialize_assign_lhs = Phase_trivialize_assign_lhs.Makemodule Reconstruct_while_loops = Phase_reconstruct_while_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 Reconstruct_asserts = Phase_reconstruct_asserts.MakeThis phase recognizes desugared `assert!(...)` to rewrite into `hax_lib::assert(..)`.
module Reconstruct_for_index_loops = Phase_reconstruct_for_index_loops.Makemodule Drop_blocks = Phase_drop_blocks.Makemodule Cf_into_monads = Phase_cf_into_monads.Makemodule Drop_references = Phase_drop_references.Makemodule Transform_hax_lib_inline = Phase_transform_hax_lib_inline.MakeThis phase transforms nodes like:
module Direct_and_mut = Phase_direct_and_mut.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 Drop_match_guards = Phase_drop_match_guards.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 Local_mutation = Phase_local_mutation.Makemodule Simplify_match_return = Phase_simplify_match_return.MakeThis phase rewrites `let pat = match ... ... => ..., ... => return ... ; e` into `match ... ... => let pat = ...; e`.
module And_mut_defsite = Phase_and_mut_defsite.Makemodule Simplify_hoisting = Phase_simplify_hoisting.MakeThis phase rewrites `let pat = match ... ... => ..., ... => return ... ; e` into `match ... ... => let pat = ...; e`.
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 Reorder_fields = Phase_reorder_fields.MakeThis phase re-order fields in structs according to the attribute AttrPayload::Order (if any).
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 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 Functionalize_loops = Phase_functionalize_loops.Makemodule 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 Newtype_as_refinement = Phase_newtype_as_refinement.MakeThis phase transforms annotated struct definitions into (refined) type aliases.
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 Reject = Phase_reject