Module Ast_destruct.Make

Parameters

module F : Features.T

Signature

include sig ... end
type expr_If = {
  1. cond : Hax_engine__Ast.Make(F).expr;
  2. then_ : Hax_engine__Ast.Make(F).expr;
  3. else_ : Hax_engine__Ast.Make(F).expr Prelude.option;
}
val expr_If : Hax_engine__Ast.Make(F).expr -> expr_If Prelude.option
type expr_App = {
  1. f : Hax_engine__Ast.Make(F).expr;
  2. args : Hax_engine__Ast.Make(F).expr Prelude.list;
  3. generic_args : Hax_engine__Ast.Make(F).generic_value Prelude.list;
  4. bounds_impls : Hax_engine__Ast.Make(F).impl_expr Prelude.list;
  5. trait : (Hax_engine__Ast.Make(F).impl_expr * Hax_engine__Ast.Make(F).generic_value Prelude.list) Prelude.option;
}
val expr_App : Hax_engine__Ast.Make(F).expr -> expr_App Prelude.option
type expr_Literal = Ast.literal
val expr_Literal : Hax_engine__Ast.Make(F).expr -> expr_Literal Prelude.option
type expr_Array = Hax_engine__Ast.Make(F).expr Prelude.list
val expr_Array : Hax_engine__Ast.Make(F).expr -> expr_Array Prelude.option
type expr_Construct = {
  1. constructor : Ast.global_ident;
  2. is_record : Prelude.bool;
  3. is_struct : Prelude.bool;
  4. fields : (Ast.global_ident * Hax_engine__Ast.Make(F).expr) Prelude.list;
  5. base : (Hax_engine__Ast.Make(F).expr * F.construct_base) Prelude.option;
}
val expr_Construct : Hax_engine__Ast.Make(F).expr -> expr_Construct Prelude.option
type expr_Match = {
  1. scrutinee : Hax_engine__Ast.Make(F).expr;
  2. arms : Hax_engine__Ast.Make(F).arm Prelude.list;
}
val expr_Match : Hax_engine__Ast.Make(F).expr -> expr_Match Prelude.option
type expr_Let = {
  1. monadic : (Hax_engine__Ast.Make(F).supported_monads * F.monadic_binding) Prelude.option;
  2. lhs : Hax_engine__Ast.Make(F).pat;
  3. rhs : Hax_engine__Ast.Make(F).expr;
  4. body : Hax_engine__Ast.Make(F).expr;
}
val expr_Let : Hax_engine__Ast.Make(F).expr -> expr_Let Prelude.option
type expr_Block = {
  1. e : Hax_engine__Ast.Make(F).expr;
  2. safety_mode : Hax_engine__Ast.Make(F).safety_kind;
  3. witness : F.block;
}
val expr_Block : Hax_engine__Ast.Make(F).expr -> expr_Block Prelude.option
type expr_LocalVar = Ast.local_ident
val expr_LocalVar : Hax_engine__Ast.Make(F).expr -> expr_LocalVar Prelude.option
type expr_GlobalVar = Ast.global_ident
val expr_GlobalVar : Hax_engine__Ast.Make(F).expr -> expr_GlobalVar Prelude.option
type expr_Ascription = {
  1. e : Hax_engine__Ast.Make(F).expr;
  2. typ : Hax_engine__Ast.Make(F).ty;
}
val expr_Ascription : Hax_engine__Ast.Make(F).expr -> expr_Ascription Prelude.option
type expr_MacroInvokation = {
  1. macro : Ast.global_ident;
  2. args : Prelude.string;
  3. witness : F.macro;
}
val expr_MacroInvokation : Hax_engine__Ast.Make(F).expr -> expr_MacroInvokation Prelude.option
type expr_Assign = {
  1. lhs : Hax_engine__Ast.Make(F).lhs;
  2. e : Hax_engine__Ast.Make(F).expr;
  3. witness : F.mutable_variable;
}
val expr_Assign : Hax_engine__Ast.Make(F).expr -> expr_Assign Prelude.option
type expr_Loop = {
  1. body : Hax_engine__Ast.Make(F).expr;
  2. kind : Hax_engine__Ast.Make(F).loop_kind;
  3. state : Hax_engine__Ast.Make(F).loop_state Prelude.option;
  4. control_flow : (Hax_engine__Ast.Make(F).cf_kind * F.fold_like_loop) Prelude.option;
  5. label : Prelude.string Prelude.option;
  6. witness : F.loop;
}
val expr_Loop : Hax_engine__Ast.Make(F).expr -> expr_Loop Prelude.option
type expr_Break = {
  1. e : Hax_engine__Ast.Make(F).expr;
  2. acc : (Hax_engine__Ast.Make(F).expr * F.state_passing_loop) Prelude.option;
  3. label : Prelude.string Prelude.option;
  4. witness : F.break * F.loop;
}
val expr_Break : Hax_engine__Ast.Make(F).expr -> expr_Break Prelude.option
type expr_Return = {
  1. e : Hax_engine__Ast.Make(F).expr;
  2. witness : F.early_exit;
}
val expr_Return : Hax_engine__Ast.Make(F).expr -> expr_Return Prelude.option
type expr_QuestionMark = {
  1. e : Hax_engine__Ast.Make(F).expr;
  2. return_typ : Hax_engine__Ast.Make(F).ty;
  3. witness : F.question_mark;
}
val expr_QuestionMark : Hax_engine__Ast.Make(F).expr -> expr_QuestionMark Prelude.option
type expr_Continue = {
  1. acc : (Hax_engine__Ast.Make(F).expr * F.state_passing_loop) Prelude.option;
  2. label : Prelude.string Prelude.option;
  3. witness : F.continue * F.loop;
}
val expr_Continue : Hax_engine__Ast.Make(F).expr -> expr_Continue Prelude.option
type expr_Borrow = {
  1. kind : Hax_engine__Ast.Make(F).borrow_kind;
  2. e : Hax_engine__Ast.Make(F).expr;
  3. witness : F.reference;
}
val expr_Borrow : Hax_engine__Ast.Make(F).expr -> expr_Borrow Prelude.option
type expr_AddressOf = {
  1. mut : F.mutable_pointer Ast.mutability;
  2. e : Hax_engine__Ast.Make(F).expr;
  3. witness : F.raw_pointer;
}
val expr_AddressOf : Hax_engine__Ast.Make(F).expr -> expr_AddressOf Prelude.option
type expr_Closure = {
  1. params : Hax_engine__Ast.Make(F).pat Prelude.list;
  2. body : Hax_engine__Ast.Make(F).expr;
  3. captures : Hax_engine__Ast.Make(F).expr Prelude.list;
}
val expr_Closure : Hax_engine__Ast.Make(F).expr -> expr_Closure Prelude.option
type expr_EffectAction = {
  1. action : F.monadic_action;
  2. argument : Hax_engine__Ast.Make(F).expr;
}
val expr_EffectAction : Hax_engine__Ast.Make(F).expr -> expr_EffectAction Prelude.option
type expr_Quote
val expr_Quote : Hax_engine__Ast.Make(F).expr -> expr_Quote Prelude.option
type pat_PWild = Prelude.unit
val pat_PWild : Hax_engine__Ast.Make(F).pat -> pat_PWild Prelude.option
type pat_PAscription = {
  1. typ : Hax_engine__Ast.Make(F).ty;
  2. typ_span : Ast.span;
  3. pat : Hax_engine__Ast.Make(F).pat;
}
val pat_PAscription : Hax_engine__Ast.Make(F).pat -> pat_PAscription Prelude.option
type pat_PConstruct = {
  1. constructor : Ast.global_ident;
  2. is_record : Prelude.bool;
  3. is_struct : Prelude.bool;
  4. fields : Hax_engine__Ast.Make(F).field_pat Prelude.list;
}
val pat_PConstruct : Hax_engine__Ast.Make(F).pat -> pat_PConstruct Prelude.option
type pat_POr = {
  1. subpats : Hax_engine__Ast.Make(F).pat Prelude.list;
}
val pat_POr : Hax_engine__Ast.Make(F).pat -> pat_POr Prelude.option
type pat_PArray = {
  1. args : Hax_engine__Ast.Make(F).pat Prelude.list;
}
val pat_PArray : Hax_engine__Ast.Make(F).pat -> pat_PArray Prelude.option
type pat_PDeref = {
  1. subpat : Hax_engine__Ast.Make(F).pat;
  2. witness : F.reference;
}
val pat_PDeref : Hax_engine__Ast.Make(F).pat -> pat_PDeref Prelude.option
type pat_PConstant = {
  1. lit : Ast.literal;
}
val pat_PConstant : Hax_engine__Ast.Make(F).pat -> pat_PConstant Prelude.option
type pat_PBinding = {
  1. mut : F.mutable_variable Ast.mutability;
  2. mode : Hax_engine__Ast.Make(F).binding_mode;
  3. var : Ast.local_ident;
  4. typ : Hax_engine__Ast.Make(F).ty;
  5. subpat : (Hax_engine__Ast.Make(F).pat * F.as_pattern) Prelude.option;
}
val pat_PBinding : Hax_engine__Ast.Make(F).pat -> pat_PBinding Prelude.option
type item_Fn = {
  1. name : Ast.concrete_ident;
  2. generics : Hax_engine__Ast.Make(F).generics;
  3. body : Hax_engine__Ast.Make(F).expr;
  4. params : Hax_engine__Ast.Make(F).param Prelude.list;
  5. safety : Hax_engine__Ast.Make(F).safety_kind;
}
val item_Fn : Hax_engine__Ast.Make(F).item -> item_Fn Prelude.option
type item_TyAlias = {
  1. name : Ast.concrete_ident;
  2. generics : Hax_engine__Ast.Make(F).generics;
  3. ty : Hax_engine__Ast.Make(F).ty;
}
val item_TyAlias : Hax_engine__Ast.Make(F).item -> item_TyAlias Prelude.option
type item_Type = {
  1. name : Ast.concrete_ident;
  2. generics : Hax_engine__Ast.Make(F).generics;
  3. variants : Hax_engine__Ast.Make(F).variant Prelude.list;
  4. is_struct : Prelude.bool;
}
val item_Type : Hax_engine__Ast.Make(F).item -> item_Type Prelude.option
type item_IMacroInvokation = {
  1. macro : Ast.concrete_ident;
  2. argument : Prelude.string;
  3. span : Ast.span;
  4. witness : F.macro;
}
val item_IMacroInvokation : Hax_engine__Ast.Make(F).item -> item_IMacroInvokation Prelude.option
type item_Trait = {
  1. name : Ast.concrete_ident;
  2. generics : Hax_engine__Ast.Make(F).generics;
  3. items : Hax_engine__Ast.Make(F).trait_item Prelude.list;
  4. safety : Hax_engine__Ast.Make(F).safety_kind;
}
val item_Trait : Hax_engine__Ast.Make(F).item -> item_Trait Prelude.option
type item_Impl = {
  1. generics : Hax_engine__Ast.Make(F).generics;
  2. self_ty : Hax_engine__Ast.Make(F).ty;
  3. of_trait : Ast.concrete_ident * Hax_engine__Ast.Make(F).generic_value Prelude.list;
  4. items : Hax_engine__Ast.Make(F).impl_item Prelude.list;
  5. parent_bounds : (Hax_engine__Ast.Make(F).impl_expr * Hax_engine__Ast.Make(F).impl_ident) Prelude.list;
  6. safety : Hax_engine__Ast.Make(F).safety_kind;
}
val item_Impl : Hax_engine__Ast.Make(F).item -> item_Impl Prelude.option
type item_Alias = {
  1. name : Ast.concrete_ident;
  2. item : Ast.concrete_ident;
}
val item_Alias : Hax_engine__Ast.Make(F).item -> item_Alias Prelude.option
type item_Use = {
  1. path : Prelude.string Prelude.list;
  2. is_external : Prelude.bool;
  3. rename : Prelude.string Prelude.option;
}
val item_Use : Hax_engine__Ast.Make(F).item -> item_Use Prelude.option
type item_Quote = {
  1. quote : Hax_engine__Ast.Make(F).quote;
  2. origin : Ast.item_quote_origin;
}
val item_Quote : Hax_engine__Ast.Make(F).item -> item_Quote Prelude.option
type item_HaxError = Prelude.string
val item_HaxError : Hax_engine__Ast.Make(F).item -> item_HaxError Prelude.option
type item_NotImplementedYet = Prelude.unit
val item_NotImplementedYet : Hax_engine__Ast.Make(F).item -> item_NotImplementedYet Prelude.option
type guard_IfLet = {
  1. lhs : Hax_engine__Ast.Make(F).pat;
  2. rhs : Hax_engine__Ast.Make(F).expr;
  3. witness : F.match_guard;
}
val guard_IfLet : Hax_engine__Ast.Make(F).guard -> guard_IfLet Prelude.option
type trait_item_TIType = Hax_engine__Ast.Make(F).impl_ident Prelude.list
val trait_item_TIType : Hax_engine__Ast.Make(F).trait_item -> trait_item_TIType Prelude.option
type trait_item_TIFn
val trait_item_TIFn : Hax_engine__Ast.Make(F).trait_item -> trait_item_TIFn Prelude.option
type trait_item_TIDefault = {
  1. params : Hax_engine__Ast.Make(F).param Prelude.list;
  2. body : Hax_engine__Ast.Make(F).expr;
  3. witness : F.trait_item_default;
}
val trait_item_TIDefault : Hax_engine__Ast.Make(F).trait_item -> trait_item_TIDefault Prelude.option
type impl_expr_Self = Prelude.unit
val impl_expr_Self : Hax_engine__Ast.Make(F).impl_expr -> impl_expr_Self Prelude.option
type impl_expr_Concrete
val impl_expr_Concrete : Hax_engine__Ast.Make(F).impl_expr -> impl_expr_Concrete Prelude.option
type impl_expr_LocalBound = {
  1. id : Prelude.string;
}
val impl_expr_LocalBound : Hax_engine__Ast.Make(F).impl_expr -> impl_expr_LocalBound Prelude.option
type impl_expr_Parent = {
  1. impl : Hax_engine__Ast.Make(F).impl_expr;
  2. ident : Hax_engine__Ast.Make(F).impl_ident;
}
val impl_expr_Parent : Hax_engine__Ast.Make(F).impl_expr -> impl_expr_Parent Prelude.option
type impl_expr_Projection = {
  1. impl : Hax_engine__Ast.Make(F).impl_expr;
  2. item : Ast.concrete_ident;
  3. ident : Hax_engine__Ast.Make(F).impl_ident;
}
val impl_expr_Projection : Hax_engine__Ast.Make(F).impl_expr -> impl_expr_Projection Prelude.option
type impl_expr_ImplApp = {
  1. impl : Hax_engine__Ast.Make(F).impl_expr;
  2. args : Hax_engine__Ast.Make(F).impl_expr Prelude.list;
}
val impl_expr_ImplApp : Hax_engine__Ast.Make(F).impl_expr -> impl_expr_ImplApp Prelude.option
type impl_expr_Dyn = Prelude.unit
val impl_expr_Dyn : Hax_engine__Ast.Make(F).impl_expr -> impl_expr_Dyn Prelude.option
type impl_expr_Builtin
val impl_expr_Builtin : Hax_engine__Ast.Make(F).impl_expr -> impl_expr_Builtin Prelude.option
val list_0 : 'a list -> unit option
val list_1 : 'a list -> 'b option
val list_2 : 'a list -> ('b * 'c) option
val list_3 : 'a list -> ('b * 'c * 'd) option
val list_4 : 'a list -> ('b * 'c * 'd * 'e) option
val list_5 : 'a list -> ('b * 'c * 'd * 'e * 'f) option