Side_effect_utils.MakeSI
module F :
Features.T
with type monadic_binding = Features.Off.monadic_binding
and type for_index_loop = Features.Off.for_index_loop
module AST : sig ... end
module U : sig ... end
include module type of struct include Ast end
type todo = Prelude.string
val pp_todo :
Ppx_deriving_runtime.Format.formatter ->
todo ->
Ppx_deriving_runtime.unit
val show_todo : todo -> Ppx_deriving_runtime.string
val todo_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> todo
val yojson_of_todo : todo -> Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_todo : todo -> todo -> Prelude.int
val todo_of_sexp : Sexplib0.Sexp.t -> todo
val sexp_of_todo : todo -> Sexplib0.Sexp.t
val hash_fold_todo :
Ppx_hash_lib.Std.Hash.state ->
todo ->
Ppx_hash_lib.Std.Hash.state
val hash_todo : todo -> Ppx_hash_lib.Std.Hash.hash_value
type span = Span.t
val pp_span :
Ppx_deriving_runtime.Format.formatter ->
span ->
Ppx_deriving_runtime.unit
val show_span : span -> Ppx_deriving_runtime.string
val span_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> span
val yojson_of_span : span -> Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_span : span -> span -> Prelude.int
val span_of_sexp : Sexplib0.Sexp.t -> span
val sexp_of_span : span -> Sexplib0.Sexp.t
val hash_fold_span :
Ppx_hash_lib.Std.Hash.state ->
span ->
Ppx_hash_lib.Std.Hash.state
val hash_span : span -> Ppx_hash_lib.Std.Hash.hash_value
type concrete_ident = Concrete_ident.t
val pp_concrete_ident :
Ppx_deriving_runtime.Format.formatter ->
concrete_ident ->
Ppx_deriving_runtime.unit
val show_concrete_ident : concrete_ident -> Ppx_deriving_runtime.string
val equal_concrete_ident :
concrete_ident ->
concrete_ident ->
Ppx_deriving_runtime.bool
val concrete_ident_of_yojson :
Ppx_yojson_conv_lib.Yojson.Safe.t ->
concrete_ident
val yojson_of_concrete_ident :
concrete_ident ->
Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_concrete_ident : concrete_ident -> concrete_ident -> Prelude.int
val concrete_ident_of_sexp : Sexplib0.Sexp.t -> concrete_ident
val sexp_of_concrete_ident : concrete_ident -> Sexplib0.Sexp.t
val hash_fold_concrete_ident :
Ppx_hash_lib.Std.Hash.state ->
concrete_ident ->
Ppx_hash_lib.Std.Hash.state
val hash_concrete_ident : concrete_ident -> Ppx_hash_lib.Std.Hash.hash_value
val pp_logical_op :
Ppx_deriving_runtime.Format.formatter ->
logical_op ->
Ppx_deriving_runtime.unit
val show_logical_op : logical_op -> Ppx_deriving_runtime.string
val pp_primitive_ident :
Ppx_deriving_runtime.Format.formatter ->
primitive_ident ->
Ppx_deriving_runtime.unit
val show_primitive_ident : primitive_ident -> Ppx_deriving_runtime.string
val equal_logical_op : logical_op -> logical_op -> Ppx_deriving_runtime.bool
val equal_primitive_ident :
primitive_ident ->
primitive_ident ->
Ppx_deriving_runtime.bool
val logical_op_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> logical_op
val primitive_ident_of_yojson :
Ppx_yojson_conv_lib.Yojson.Safe.t ->
primitive_ident
val yojson_of_logical_op : logical_op -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_primitive_ident :
primitive_ident ->
Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_logical_op : logical_op -> logical_op -> Prelude.int
val compare_primitive_ident : primitive_ident -> primitive_ident -> Prelude.int
val logical_op_of_sexp : Sexplib0.Sexp.t -> logical_op
val primitive_ident_of_sexp : Sexplib0.Sexp.t -> primitive_ident
val sexp_of_logical_op : logical_op -> Sexplib0.Sexp.t
val sexp_of_primitive_ident : primitive_ident -> Sexplib0.Sexp.t
val hash_fold_logical_op :
Ppx_hash_lib.Std.Hash.state ->
logical_op ->
Ppx_hash_lib.Std.Hash.state
val hash_fold_primitive_ident :
Ppx_hash_lib.Std.Hash.state ->
primitive_ident ->
Ppx_hash_lib.Std.Hash.state
val hash_logical_op : logical_op -> Ppx_hash_lib.Std.Hash.hash_value
val hash_primitive_ident : primitive_ident -> Ppx_hash_lib.Std.Hash.hash_value
module Global_ident = Ast.Global_ident
type global_ident = Global_ident.t
val pp_global_ident :
Ppx_deriving_runtime.Format.formatter ->
global_ident ->
Ppx_deriving_runtime.unit
val show_global_ident : global_ident -> Ppx_deriving_runtime.string
val equal_global_ident :
global_ident ->
global_ident ->
Ppx_deriving_runtime.bool
val global_ident_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> global_ident
val yojson_of_global_ident : global_ident -> Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_global_ident : global_ident -> global_ident -> Prelude.int
val global_ident_of_sexp : Sexplib0.Sexp.t -> global_ident
val sexp_of_global_ident : global_ident -> Sexplib0.Sexp.t
val hash_fold_global_ident :
Ppx_hash_lib.Std.Hash.state ->
global_ident ->
Ppx_hash_lib.Std.Hash.state
val hash_global_ident : global_ident -> Ppx_hash_lib.Std.Hash.hash_value
type attr_kind = Ast.attr_kind =
| Tool of {
path : Prelude.string;
tokens : Prelude.string;
}
| DocComment of {
kind : doc_comment_kind;
body : Prelude.string;
}
and attrs = attr Prelude.list
val pp_attr_kind :
Ppx_deriving_runtime.Format.formatter ->
attr_kind ->
Ppx_deriving_runtime.unit
val show_attr_kind : attr_kind -> Ppx_deriving_runtime.string
val pp_attr :
Ppx_deriving_runtime.Format.formatter ->
attr ->
Ppx_deriving_runtime.unit
val show_attr : attr -> Ppx_deriving_runtime.string
val pp_doc_comment_kind :
Ppx_deriving_runtime.Format.formatter ->
doc_comment_kind ->
Ppx_deriving_runtime.unit
val show_doc_comment_kind : doc_comment_kind -> Ppx_deriving_runtime.string
val pp_attrs :
Ppx_deriving_runtime.Format.formatter ->
attrs ->
Ppx_deriving_runtime.unit
val show_attrs : attrs -> Ppx_deriving_runtime.string
val equal_doc_comment_kind :
doc_comment_kind ->
doc_comment_kind ->
Ppx_deriving_runtime.bool
val attr_kind_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> attr_kind
val attr_of_yojson : Yojson.Safe.t -> attr
val doc_comment_kind_of_yojson : Yojson.Safe.t -> doc_comment_kind
val attrs_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> attrs
val yojson_of_attr_kind : attr_kind -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_attr : attr -> Yojson.Safe.t
val yojson_of_doc_comment_kind :
doc_comment_kind ->
Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_attrs : attrs -> Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_attr_kind : attr_kind -> attr_kind -> Prelude.int
val compare_attr : attr -> attr -> Prelude.int
val compare_doc_comment_kind :
doc_comment_kind ->
doc_comment_kind ->
Prelude.int
val compare_attrs : attrs -> attrs -> Prelude.int
val attr_kind_of_sexp : Sexplib0__.Sexp.t -> attr_kind
val attr_of_sexp : Sexplib0.Sexp.t -> attr
val doc_comment_kind_of_sexp : Sexplib0__.Sexp.t -> doc_comment_kind
val attrs_of_sexp : Sexplib0.Sexp.t -> attrs
val sexp_of_attr_kind : attr_kind -> Sexplib0.Sexp.t
val sexp_of_attr : attr -> Sexplib0.Sexp.t
val sexp_of_doc_comment_kind : doc_comment_kind -> Sexplib0.Sexp.t
val sexp_of_attrs : attrs -> Sexplib0.Sexp.t
val hash_fold_attr_kind :
Ppx_hash_lib.Std.Hash.state ->
attr_kind ->
Ppx_hash_lib.Std.Hash.state
val hash_fold_attr :
Base__.Ppx_hash_lib.Std.Hash.state ->
attr ->
Base__.Ppx_hash_lib.Std.Hash.state
val hash_fold_doc_comment_kind :
Ppx_hash_lib.Std.Hash.state ->
doc_comment_kind ->
Ppx_hash_lib.Std.Hash.state
val hash_fold_attrs :
Ppx_hash_lib.Std.Hash.state ->
attrs ->
Ppx_hash_lib.Std.Hash.state
val hash_attr_kind : attr_kind -> Ppx_hash_lib.Std.Hash.hash_value
val hash_attr : attr -> Ppx_hash_lib.Std.Hash.hash_value
val hash_doc_comment_kind :
doc_comment_kind ->
Ppx_hash_lib.Std.Hash.hash_value
val hash_attrs : attrs -> Ppx_hash_lib.Std.Hash.hash_value
type local_ident = Local_ident.t
val pp_local_ident :
Ppx_deriving_runtime.Format.formatter ->
local_ident ->
Ppx_deriving_runtime.unit
val show_local_ident : local_ident -> Ppx_deriving_runtime.string
val equal_local_ident : local_ident -> local_ident -> Ppx_deriving_runtime.bool
val local_ident_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> local_ident
val yojson_of_local_ident : local_ident -> Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_local_ident : local_ident -> local_ident -> Prelude.int
val local_ident_of_sexp : Sexplib0.Sexp.t -> local_ident
val sexp_of_local_ident : local_ident -> Sexplib0.Sexp.t
val hash_fold_local_ident :
Ppx_hash_lib.Std.Hash.state ->
local_ident ->
Ppx_hash_lib.Std.Hash.state
val hash_local_ident : local_ident -> Ppx_hash_lib.Std.Hash.hash_value
val pp_size :
Ppx_deriving_runtime.Format.formatter ->
size ->
Ppx_deriving_runtime.unit
val show_size : size -> Ppx_deriving_runtime.string
val size_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> size
val yojson_of_size : size -> Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_size : size -> size -> Prelude.int
val size_of_sexp : Sexplib0.Sexp.t -> size
val sexp_of_size : size -> Sexplib0.Sexp.t
val hash_fold_size :
Ppx_hash_lib.Std.Hash.state ->
size ->
Ppx_hash_lib.Std.Hash.state
val hash_size : size -> Ppx_hash_lib.Std.Hash.hash_value
val int_of_size : size -> int option
val string_of_size : size -> string Hax_engine.Prelude.Option.t
val pp_signedness :
Ppx_deriving_runtime.Format.formatter ->
signedness ->
Ppx_deriving_runtime.unit
val show_signedness : signedness -> Ppx_deriving_runtime.string
val equal_signedness : signedness -> signedness -> Ppx_deriving_runtime.bool
val signedness_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> signedness
val yojson_of_signedness : signedness -> Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_signedness : signedness -> signedness -> Prelude.int
val signedness_of_sexp : Sexplib0.Sexp.t -> signedness
val sexp_of_signedness : signedness -> Sexplib0.Sexp.t
val hash_fold_signedness :
Ppx_hash_lib.Std.Hash.state ->
signedness ->
Ppx_hash_lib.Std.Hash.state
val hash_signedness : signedness -> Ppx_hash_lib.Std.Hash.hash_value
val pp_int_kind :
Ppx_deriving_runtime.Format.formatter ->
int_kind ->
Ppx_deriving_runtime.unit
val int_kind_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> int_kind
val yojson_of_int_kind : int_kind -> Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_int_kind : int_kind -> int_kind -> Prelude.int
val int_kind_of_sexp : Sexplib0.Sexp.t -> int_kind
val sexp_of_int_kind : int_kind -> Sexplib0.Sexp.t
val hash_fold_int_kind :
Ppx_hash_lib.Std.Hash.state ->
int_kind ->
Ppx_hash_lib.Std.Hash.state
val hash_int_kind : int_kind -> Ppx_hash_lib.Std.Hash.hash_value
val show_int_kind : int_kind -> Hax_engine.Prelude.String.t
val pp_float_kind :
Ppx_deriving_runtime.Format.formatter ->
float_kind ->
Ppx_deriving_runtime.unit
val equal_float_kind : float_kind -> float_kind -> Ppx_deriving_runtime.bool
val float_kind_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> float_kind
val yojson_of_float_kind : float_kind -> Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_float_kind : float_kind -> float_kind -> Prelude.int
val float_kind_of_sexp : Sexplib0.Sexp.t -> float_kind
val sexp_of_float_kind : float_kind -> Sexplib0.Sexp.t
val hash_fold_float_kind :
Ppx_hash_lib.Std.Hash.state ->
float_kind ->
Ppx_hash_lib.Std.Hash.state
val hash_float_kind : float_kind -> Ppx_hash_lib.Std.Hash.hash_value
val show_float_kind : float_kind -> string
type literal = Ast.literal =
| String of Prelude.string
| Char of Prelude.char
| Int of {
value : Prelude.string;
negative : Prelude.bool;
kind : int_kind;
}
| Float of {
value : Prelude.string;
negative : Prelude.bool;
kind : float_kind;
}
| Bool of Prelude.bool
val pp_literal :
Ppx_deriving_runtime.Format.formatter ->
literal ->
Ppx_deriving_runtime.unit
val show_literal : literal -> Ppx_deriving_runtime.string
val literal_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> literal
val yojson_of_literal : literal -> Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_literal : literal -> literal -> Prelude.int
val literal_of_sexp : Sexplib0.Sexp.t -> literal
val sexp_of_literal : literal -> Sexplib0.Sexp.t
val hash_fold_literal :
Ppx_hash_lib.Std.Hash.state ->
literal ->
Ppx_hash_lib.Std.Hash.state
val hash_literal : literal -> Ppx_hash_lib.Std.Hash.hash_value
val pp_mutability :
'mut_witness. (Ppx_deriving_runtime.Format.formatter ->
'mut_witness ->
Ppx_deriving_runtime.unit) ->
Ppx_deriving_runtime.Format.formatter ->
'mut_witness mutability ->
Ppx_deriving_runtime.unit
val show_mutability :
'mut_witness. (Ppx_deriving_runtime.Format.formatter ->
'mut_witness ->
Ppx_deriving_runtime.unit) ->
'mut_witness mutability ->
Ppx_deriving_runtime.string
val equal_mutability :
'mut_witness. ('mut_witness -> 'mut_witness -> Ppx_deriving_runtime.bool) ->
'mut_witness mutability ->
'mut_witness mutability ->
Ppx_deriving_runtime.bool
val mutability_of_yojson :
'mut_witness. (Ppx_yojson_conv_lib.Yojson.Safe.t -> 'mut_witness) ->
Ppx_yojson_conv_lib.Yojson.Safe.t ->
'mut_witness mutability
val yojson_of_mutability :
'mut_witness. ('mut_witness -> Ppx_yojson_conv_lib.Yojson.Safe.t) ->
'mut_witness mutability ->
Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_mutability :
'mut_witness. ('mut_witness -> 'mut_witness -> Prelude.int) ->
'mut_witness mutability ->
'mut_witness mutability ->
Prelude.int
val mutability_of_sexp :
'mut_witness. (Sexplib0.Sexp.t -> 'mut_witness) ->
Sexplib0.Sexp.t ->
'mut_witness mutability
val sexp_of_mutability :
'mut_witness. ('mut_witness -> Sexplib0.Sexp.t) ->
'mut_witness mutability ->
Sexplib0.Sexp.t
val hash_fold_mutability :
'mut_witness. (Ppx_hash_lib.Std.Hash.state ->
'mut_witness ->
Ppx_hash_lib.Std.Hash.state) ->
Ppx_hash_lib.Std.Hash.state ->
'mut_witness mutability ->
Ppx_hash_lib.Std.Hash.state
type item_kind = [
| `Fn
| `TyAlias
| `Type
| `IMacroInvokation
| `Trait
| `Impl
| `Alias
| `Use
| `Quote
| `HaxError
| `NotImplementedYet
]
Describes the (shallow) kind of an item.
val pp_item_kind :
Ppx_deriving_runtime.Format.formatter ->
item_kind ->
Ppx_deriving_runtime.unit
val show_item_kind : item_kind -> Ppx_deriving_runtime.string
val __item_kind_of_yojson__ : Ppx_yojson_conv_lib.Yojson.Safe.t -> item_kind
val item_kind_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> item_kind
val yojson_of_item_kind : item_kind -> Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_item_kind : item_kind -> item_kind -> Prelude.int
val __item_kind_of_sexp__ : Sexplib0.Sexp.t -> item_kind
val item_kind_of_sexp : Sexplib0.Sexp.t -> item_kind
val sexp_of_item_kind : item_kind -> Sexplib0.Sexp.t
val hash_fold_item_kind :
Ppx_hash_lib.Std.Hash.state ->
item_kind ->
Ppx_hash_lib.Std.Hash.state
val hash_item_kind : item_kind -> Ppx_hash_lib.Std.Hash.hash_value
type item_quote_origin = Ast.item_quote_origin = {
item_kind : item_kind;
item_ident : concrete_ident;
position : [ `Before | `After | `Replace ];
}
From where does a quote item comes from?
val pp_item_quote_origin :
Ppx_deriving_runtime.Format.formatter ->
item_quote_origin ->
Ppx_deriving_runtime.unit
val show_item_quote_origin : item_quote_origin -> Ppx_deriving_runtime.string
val equal_item_quote_origin :
item_quote_origin ->
item_quote_origin ->
Ppx_deriving_runtime.bool
val item_quote_origin_of_yojson :
Ppx_yojson_conv_lib.Yojson.Safe.t ->
item_quote_origin
val yojson_of_item_quote_origin :
item_quote_origin ->
Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_item_quote_origin :
item_quote_origin ->
item_quote_origin ->
Prelude.int
val item_quote_origin_of_sexp : Sexplib0.Sexp.t -> item_quote_origin
val sexp_of_item_quote_origin : item_quote_origin -> Sexplib0.Sexp.t
val hash_fold_item_quote_origin :
Ppx_hash_lib.Std.Hash.state ->
item_quote_origin ->
Ppx_hash_lib.Std.Hash.state
val hash_item_quote_origin :
item_quote_origin ->
Ppx_hash_lib.Std.Hash.hash_value
module Make = Ast.Make
module type T = Ast.T
module Rust = Ast.Rust
module Full = Ast.Full
include module type of struct include AST end
val pp_safety_kind :
Ppx_deriving_runtime.Format.formatter ->
safety_kind ->
Ppx_deriving_runtime.unit
val show_safety_kind : safety_kind -> Ppx_deriving_runtime.string
val equal_safety_kind : safety_kind -> safety_kind -> Ppx_deriving_runtime.bool
val safety_kind_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> safety_kind
val yojson_of_safety_kind : safety_kind -> Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_safety_kind : safety_kind -> safety_kind -> Prelude.int
val safety_kind_of_sexp : Sexplib0.Sexp.t -> safety_kind
val sexp_of_safety_kind : safety_kind -> Sexplib0.Sexp.t
val hash_fold_safety_kind :
Ppx_hash_lib.Std.Hash.state ->
safety_kind ->
Ppx_hash_lib.Std.Hash.state
val hash_safety_kind : safety_kind -> Ppx_hash_lib.Std.Hash.hash_value
val pp_borrow_kind :
Ppx_deriving_runtime.Format.formatter ->
borrow_kind ->
Ppx_deriving_runtime.unit
val show_borrow_kind : borrow_kind -> Ppx_deriving_runtime.string
val equal_borrow_kind : borrow_kind -> borrow_kind -> Ppx_deriving_runtime.bool
val borrow_kind_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> borrow_kind
val yojson_of_borrow_kind : borrow_kind -> Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_borrow_kind : borrow_kind -> borrow_kind -> Prelude.int
val borrow_kind_of_sexp : Sexplib0.Sexp.t -> borrow_kind
val sexp_of_borrow_kind : borrow_kind -> Sexplib0.Sexp.t
val hash_fold_borrow_kind :
Ppx_hash_lib.Std.Hash.state ->
borrow_kind ->
Ppx_hash_lib.Std.Hash.state
val hash_borrow_kind : borrow_kind -> Ppx_hash_lib.Std.Hash.hash_value
val pp_binding_mode :
Ppx_deriving_runtime.Format.formatter ->
binding_mode ->
Ppx_deriving_runtime.unit
val show_binding_mode : binding_mode -> Ppx_deriving_runtime.string
val equal_binding_mode :
binding_mode ->
binding_mode ->
Ppx_deriving_runtime.bool
val binding_mode_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> binding_mode
val yojson_of_binding_mode : binding_mode -> Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_binding_mode : binding_mode -> binding_mode -> Prelude.int
val binding_mode_of_sexp : Sexplib0.Sexp.t -> binding_mode
val sexp_of_binding_mode : binding_mode -> Sexplib0.Sexp.t
val hash_fold_binding_mode :
Ppx_hash_lib.Std.Hash.state ->
binding_mode ->
Ppx_hash_lib.Std.Hash.state
val hash_binding_mode : binding_mode -> Ppx_hash_lib.Std.Hash.hash_value
type ty =
| TBool
| TChar
| TStr
| TApp of {
ident : [ `Concrete of Concrete_ident.t
| `Primitive of Hax_engine__Ast.primitive_ident
| `TupleType of Prelude.int
| `TupleCons of Prelude.int
| `TupleField of Prelude.int * Prelude.int
| `Projector of
[ `Concrete of Concrete_ident.t
| `TupleField of Prelude.int * Prelude.int ] ];
args : generic_value Prelude.list;
}
| TArray of {
}
| TSlice of {
}
| TRawPointer of {
witness : F.raw_pointer;
}
| TParam of Local_ident.t
| TArrow of ty Prelude.list * ty
| TAssociatedType of {
impl : impl_expr;
item : Concrete_ident.t;
}
| TOpaque of Concrete_ident.t
| TDyn of {
witness : F.dyn;
goals : dyn_trait_goal Prelude.list;
}
and generic_value =
| GLifetime of {
lt : Prelude.string;
witness : F.lifetime;
}
| GType of ty
| GConst of expr
and impl_expr_kind =
| Self
| Concrete of trait_goal
| LocalBound of {
id : Prelude.string;
}
| Parent of {
impl : impl_expr;
ident : impl_ident;
}
| Projection of {
impl : impl_expr;
item : Concrete_ident.t;
ident : impl_ident;
}
| ImplApp of {
impl : impl_expr;
args : impl_expr Prelude.list;
}
| Dyn
| Builtin of trait_goal
and pat' =
| PWild
| PAscription of {
}
| PConstruct of {
constructor : [ `Concrete of Concrete_ident.t
| `Primitive of Hax_engine__Ast.primitive_ident
| `TupleType of Prelude.int
| `TupleCons of Prelude.int
| `TupleField of Prelude.int * Prelude.int
| `Projector of
[ `Concrete of Concrete_ident.t
| `TupleField of Prelude.int * Prelude.int ] ];
is_record : Prelude.bool;
is_struct : Prelude.bool;
fields : field_pat Prelude.list;
}
| POr of {
subpats : pat Prelude.list;
}
| PArray of {
args : pat Prelude.list;
}
| PDeref of {
subpat : pat;
witness : F.reference;
}
and field_pat = {
field : [ `Concrete of Concrete_ident.t
| `Primitive of Hax_engine__Ast.primitive_ident
| `TupleType of Prelude.int
| `TupleCons of Prelude.int
| `TupleField of Prelude.int * Prelude.int
| `Projector of
[ `Concrete of Concrete_ident.t
| `TupleField of Prelude.int * Prelude.int ] ];
pat : pat;
}
and expr' =
| If of {
cond : expr;
then_ : expr;
else_ : expr Prelude.option;
}
| App of {
f : expr;
args : expr Prelude.list;
generic_args : generic_value Prelude.list;
bounds_impls : impl_expr Prelude.list;
trait : (impl_expr * generic_value Prelude.list) Prelude.option;
}
| Array of expr Prelude.list
| Construct of {
constructor : [ `Concrete of Concrete_ident.t
| `Primitive of Hax_engine__Ast.primitive_ident
| `TupleType of Prelude.int
| `TupleCons of Prelude.int
| `TupleField of Prelude.int * Prelude.int
| `Projector of
[ `Concrete of Concrete_ident.t
| `TupleField of Prelude.int * Prelude.int ] ];
is_record : Prelude.bool;
is_struct : Prelude.bool;
fields : ([ `Concrete of Concrete_ident.t
| `Primitive of Hax_engine__Ast.primitive_ident
| `TupleType of Prelude.int
| `TupleCons of Prelude.int
| `TupleField of Prelude.int * Prelude.int
| `Projector of
[ `Concrete of Concrete_ident.t
| `TupleField of Prelude.int * Prelude.int ] ]
* expr)
Prelude.list;
base : (expr * F.construct_base) Prelude.option;
}
| Match of {
scrutinee : expr;
arms : arm Prelude.list;
}
| Let of {
monadic : (supported_monads * F.monadic_binding) Prelude.option;
lhs : pat;
rhs : expr;
body : expr;
}
| Block of {
e : expr;
safety_mode : safety_kind;
witness : F.block;
}
| LocalVar of Local_ident.t
| GlobalVar of [ `Concrete of Concrete_ident.t
| `Primitive of Hax_engine__Ast.primitive_ident
| `TupleType of Prelude.int
| `TupleCons of Prelude.int
| `TupleField of Prelude.int * Prelude.int
| `Projector of
[ `Concrete of Concrete_ident.t
| `TupleField of Prelude.int * Prelude.int ] ]
| Ascription of {
}
| MacroInvokation of {
macro : [ `Concrete of Concrete_ident.t
| `Primitive of Hax_engine__Ast.primitive_ident
| `TupleType of Prelude.int
| `TupleCons of Prelude.int
| `TupleField of Prelude.int * Prelude.int
| `Projector of
[ `Concrete of Concrete_ident.t
| `TupleField of Prelude.int * Prelude.int ] ];
args : Prelude.string;
witness : F.macro;
}
| Assign of {
lhs : lhs;
e : expr;
witness : F.mutable_variable;
}
| Loop of {
body : expr;
kind : loop_kind;
state : loop_state Prelude.option;
control_flow : (cf_kind * F.fold_like_loop) Prelude.option;
label : Prelude.string Prelude.option;
witness : F.loop;
}
| Break of {
e : expr;
acc : (expr * F.state_passing_loop) Prelude.option;
label : Prelude.string Prelude.option;
witness : F.break * F.loop;
}
| Return of {
e : expr;
witness : F.early_exit;
}
| QuestionMark of {
e : expr;
return_typ : ty;
witness : F.question_mark;
}
| Continue of {
acc : (expr * F.state_passing_loop) Prelude.option;
label : Prelude.string Prelude.option;
witness : F.continue * F.loop;
}
| Borrow of {
kind : borrow_kind;
e : expr;
witness : F.reference;
}
| Closure of {
params : pat Prelude.list;
body : expr;
captures : expr Prelude.list;
}
| EffectAction of {
action : F.monadic_action;
argument : expr;
}
| Quote of quote
and quote = {
contents : [ `Expr of expr
| `Pat of pat
| `Typ of ty
| `Verbatim of Prelude.string ]
Prelude.list;
witness : F.quote;
}
and loop_kind =
| UnconditionalLoop
| WhileLoop of {
condition : expr;
witness : F.while_loop;
}
| ForLoop of {
pat : pat;
it : expr;
witness : F.for_loop;
}
| ForIndexLoop of {
start : expr;
end_ : expr;
var : Local_ident.t;
var_typ : ty;
witness : F.for_index_loop;
}
and lhs =
| LhsLocalVar of {
var : Local_ident.t;
typ : ty;
}
| LhsArbitraryExpr of {
e : expr;
witness : F.arbitrary_lhs;
}
| LhsFieldAccessor of {
e : lhs;
typ : ty;
field : [ `Concrete of Concrete_ident.t
| `Primitive of Hax_engine__Ast.primitive_ident
| `TupleType of Prelude.int
| `TupleCons of Prelude.int
| `TupleField of Prelude.int * Prelude.int
| `Projector of
[ `Concrete of Concrete_ident.t
| `TupleField of Prelude.int * Prelude.int ] ];
witness : F.nontrivial_lhs;
}
| LhsArrayAccessor of {
e : lhs;
typ : ty;
index : expr;
witness : F.nontrivial_lhs;
}
val pp_ty :
Ppx_deriving_runtime.Format.formatter ->
ty ->
Ppx_deriving_runtime.unit
val show_ty : ty -> Ppx_deriving_runtime.string
val pp_generic_value :
Ppx_deriving_runtime.Format.formatter ->
generic_value ->
Ppx_deriving_runtime.unit
val show_generic_value : generic_value -> Ppx_deriving_runtime.string
val pp_impl_expr :
Ppx_deriving_runtime.Format.formatter ->
impl_expr ->
Ppx_deriving_runtime.unit
val show_impl_expr : impl_expr -> Ppx_deriving_runtime.string
val pp_impl_expr_kind :
Ppx_deriving_runtime.Format.formatter ->
impl_expr_kind ->
Ppx_deriving_runtime.unit
val show_impl_expr_kind : impl_expr_kind -> Ppx_deriving_runtime.string
val pp_trait_goal :
Ppx_deriving_runtime.Format.formatter ->
trait_goal ->
Ppx_deriving_runtime.unit
val show_trait_goal : trait_goal -> Ppx_deriving_runtime.string
val pp_dyn_trait_goal :
Ppx_deriving_runtime.Format.formatter ->
dyn_trait_goal ->
Ppx_deriving_runtime.unit
val show_dyn_trait_goal : dyn_trait_goal -> Ppx_deriving_runtime.string
val pp_impl_ident :
Ppx_deriving_runtime.Format.formatter ->
impl_ident ->
Ppx_deriving_runtime.unit
val show_impl_ident : impl_ident -> Ppx_deriving_runtime.string
val pp_projection_predicate :
Ppx_deriving_runtime.Format.formatter ->
projection_predicate ->
Ppx_deriving_runtime.unit
val show_projection_predicate :
projection_predicate ->
Ppx_deriving_runtime.string
val pp_pat' :
Ppx_deriving_runtime.Format.formatter ->
pat' ->
Ppx_deriving_runtime.unit
val show_pat' : pat' -> Ppx_deriving_runtime.string
val pp_pat :
Ppx_deriving_runtime.Format.formatter ->
pat ->
Ppx_deriving_runtime.unit
val show_pat : pat -> Ppx_deriving_runtime.string
val pp_field_pat :
Ppx_deriving_runtime.Format.formatter ->
field_pat ->
Ppx_deriving_runtime.unit
val show_field_pat : field_pat -> Ppx_deriving_runtime.string
val pp_cf_kind :
Ppx_deriving_runtime.Format.formatter ->
cf_kind ->
Ppx_deriving_runtime.unit
val show_cf_kind : cf_kind -> Ppx_deriving_runtime.string
val pp_expr' :
Ppx_deriving_runtime.Format.formatter ->
expr' ->
Ppx_deriving_runtime.unit
val show_expr' : expr' -> Ppx_deriving_runtime.string
val pp_expr :
Ppx_deriving_runtime.Format.formatter ->
expr ->
Ppx_deriving_runtime.unit
val show_expr : expr -> Ppx_deriving_runtime.string
val pp_quote :
Ppx_deriving_runtime.Format.formatter ->
quote ->
Ppx_deriving_runtime.unit
val show_quote : quote -> Ppx_deriving_runtime.string
val pp_supported_monads :
Ppx_deriving_runtime.Format.formatter ->
supported_monads ->
Ppx_deriving_runtime.unit
val show_supported_monads : supported_monads -> Ppx_deriving_runtime.string
val pp_loop_kind :
Ppx_deriving_runtime.Format.formatter ->
loop_kind ->
Ppx_deriving_runtime.unit
val show_loop_kind : loop_kind -> Ppx_deriving_runtime.string
val pp_loop_state :
Ppx_deriving_runtime.Format.formatter ->
loop_state ->
Ppx_deriving_runtime.unit
val show_loop_state : loop_state -> Ppx_deriving_runtime.string
val pp_lhs :
Ppx_deriving_runtime.Format.formatter ->
lhs ->
Ppx_deriving_runtime.unit
val show_lhs : lhs -> Ppx_deriving_runtime.string
val pp_guard :
Ppx_deriving_runtime.Format.formatter ->
guard ->
Ppx_deriving_runtime.unit
val show_guard : guard -> Ppx_deriving_runtime.string
val pp_guard' :
Ppx_deriving_runtime.Format.formatter ->
guard' ->
Ppx_deriving_runtime.unit
val show_guard' : guard' -> Ppx_deriving_runtime.string
val pp_arm' :
Ppx_deriving_runtime.Format.formatter ->
arm' ->
Ppx_deriving_runtime.unit
val show_arm' : arm' -> Ppx_deriving_runtime.string
val pp_arm :
Ppx_deriving_runtime.Format.formatter ->
arm ->
Ppx_deriving_runtime.unit
val show_arm : arm -> Ppx_deriving_runtime.string
val equal_generic_value :
generic_value ->
generic_value ->
Ppx_deriving_runtime.bool
val equal_impl_expr_kind :
impl_expr_kind ->
impl_expr_kind ->
Ppx_deriving_runtime.bool
val equal_trait_goal : trait_goal -> trait_goal -> Ppx_deriving_runtime.bool
val equal_dyn_trait_goal :
dyn_trait_goal ->
dyn_trait_goal ->
Ppx_deriving_runtime.bool
val equal_impl_ident : impl_ident -> impl_ident -> Ppx_deriving_runtime.bool
val equal_projection_predicate :
projection_predicate ->
projection_predicate ->
Ppx_deriving_runtime.bool
val equal_supported_monads :
supported_monads ->
supported_monads ->
Ppx_deriving_runtime.bool
val equal_loop_state : loop_state -> loop_state -> Ppx_deriving_runtime.bool
val ty_of_yojson : Yojson.Safe.t -> ty
val generic_value_of_yojson : Yojson.Safe.t -> generic_value
val impl_expr_of_yojson : Yojson.Safe.t -> impl_expr
val impl_expr_kind_of_yojson :
Ppx_yojson_conv_lib.Yojson.Safe.t ->
impl_expr_kind
val trait_goal_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> trait_goal
val dyn_trait_goal_of_yojson : Yojson.Safe.t -> dyn_trait_goal
val impl_ident_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> impl_ident
val projection_predicate_of_yojson :
Ppx_yojson_conv_lib.Yojson.Safe.t ->
projection_predicate
val pat'_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> pat'
val pat_of_yojson : Yojson.Safe.t -> pat
val field_pat_of_yojson : Yojson.Safe.t -> field_pat
val cf_kind_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> cf_kind
val expr'_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> expr'
val expr_of_yojson : Yojson.Safe.t -> expr
val quote_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> quote
val supported_monads_of_yojson : Yojson.Safe.t -> supported_monads
val loop_kind_of_yojson : Yojson.Safe.t -> loop_kind
val loop_state_of_yojson : Yojson.Safe.t -> loop_state
val lhs_of_yojson : Yojson.Safe.t -> lhs
val guard_of_yojson : Yojson.Safe.t -> guard
val guard'_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> guard'
val arm'_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> arm'
val arm_of_yojson : Yojson.Safe.t -> arm
val yojson_of_ty : ty -> Yojson.Safe.t
val yojson_of_generic_value : generic_value -> Yojson.Safe.t
val yojson_of_impl_expr : impl_expr -> Yojson.Safe.t
val yojson_of_impl_expr_kind :
impl_expr_kind ->
Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_trait_goal : trait_goal -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_dyn_trait_goal : dyn_trait_goal -> Yojson.Safe.t
val yojson_of_impl_ident : impl_ident -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_projection_predicate :
projection_predicate ->
Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_pat' : pat' -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_pat : pat -> Yojson.Safe.t
val yojson_of_field_pat : field_pat -> Yojson.Safe.t
val yojson_of_cf_kind : cf_kind -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_expr' : expr' -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_expr : expr -> Yojson.Safe.t
val yojson_of_quote : quote -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_supported_monads :
supported_monads ->
Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_loop_kind : loop_kind -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_loop_state : loop_state -> Yojson.Safe.t
val yojson_of_lhs : lhs -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_guard : guard -> Yojson.Safe.t
val yojson_of_guard' : guard' -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_arm' : arm' -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_arm : arm -> Yojson.Safe.t
val compare_ty : ty -> ty -> Prelude.int
val compare_generic_value : generic_value -> generic_value -> Prelude.int
val compare_impl_expr : impl_expr -> impl_expr -> Prelude.int
val compare_impl_expr_kind : impl_expr_kind -> impl_expr_kind -> Prelude.int
val compare_trait_goal : trait_goal -> trait_goal -> Prelude.int
val compare_dyn_trait_goal : dyn_trait_goal -> dyn_trait_goal -> Prelude.int
val compare_impl_ident : impl_ident -> impl_ident -> Prelude.int
val compare_projection_predicate :
projection_predicate ->
projection_predicate ->
Prelude.int
val compare_pat' : pat' -> pat' -> Prelude.int
val compare_pat : pat -> pat -> Prelude.int
val compare_field_pat : field_pat -> field_pat -> Prelude.int
val compare_cf_kind : cf_kind -> cf_kind -> Prelude.int
val compare_expr' : expr' -> expr' -> Prelude.int
val compare_expr : expr -> expr -> Prelude.int
val compare_quote : quote -> quote -> Prelude.int
val compare_supported_monads :
supported_monads ->
supported_monads ->
Prelude.int
val compare_loop_kind : loop_kind -> loop_kind -> Prelude.int
val compare_loop_state : loop_state -> loop_state -> Prelude.int
val compare_lhs : lhs -> lhs -> Prelude.int
val compare_guard : guard -> guard -> Prelude.int
val compare_guard' : guard' -> guard' -> Prelude.int
val compare_arm' : arm' -> arm' -> Prelude.int
val compare_arm : arm -> arm -> Prelude.int
val ty_of_sexp : Sexplib0__.Sexp.t -> ty
val generic_value_of_sexp : Sexplib0.Sexp.t -> generic_value
val impl_expr_of_sexp : Sexplib0.Sexp.t -> impl_expr
val impl_expr_kind_of_sexp : Sexplib0__.Sexp.t -> impl_expr_kind
val trait_goal_of_sexp : Sexplib0__.Sexp.t -> trait_goal
val dyn_trait_goal_of_sexp : Sexplib0.Sexp.t -> dyn_trait_goal
val impl_ident_of_sexp : Sexplib0__.Sexp.t -> impl_ident
val projection_predicate_of_sexp : Sexplib0.Sexp.t -> projection_predicate
val pat'_of_sexp : Sexplib0__.Sexp.t -> pat'
val pat_of_sexp : Sexplib0__.Sexp.t -> pat
val field_pat_of_sexp : Sexplib0.Sexp.t -> field_pat
val cf_kind_of_sexp : Sexplib0.Sexp.t -> cf_kind
val expr'_of_sexp : Sexplib0__.Sexp.t -> expr'
val expr_of_sexp : Sexplib0__.Sexp.t -> expr
val quote_of_sexp : Sexplib0.Sexp.t -> quote
val supported_monads_of_sexp : Sexplib0.Sexp.t -> supported_monads
val loop_kind_of_sexp : Sexplib0__.Sexp.t -> loop_kind
val loop_state_of_sexp : Sexplib0.Sexp.t -> loop_state
val lhs_of_sexp : Sexplib0__.Sexp.t -> lhs
val guard_of_sexp : Sexplib0.Sexp.t -> guard
val guard'_of_sexp : Sexplib0__.Sexp.t -> guard'
val arm'_of_sexp : Sexplib0__.Sexp.t -> arm'
val arm_of_sexp : Sexplib0.Sexp.t -> arm
val sexp_of_ty : ty -> Sexplib0.Sexp.t
val sexp_of_generic_value : generic_value -> Sexplib0.Sexp.t
val sexp_of_impl_expr : impl_expr -> Sexplib0.Sexp.t
val sexp_of_impl_expr_kind : impl_expr_kind -> Sexplib0.Sexp.t
val sexp_of_trait_goal : trait_goal -> Sexplib0.Sexp.t
val sexp_of_dyn_trait_goal : dyn_trait_goal -> Sexplib0.Sexp.t
val sexp_of_impl_ident : impl_ident -> Sexplib0.Sexp.t
val sexp_of_projection_predicate : projection_predicate -> Sexplib0.Sexp.t
val sexp_of_pat' : pat' -> Sexplib0.Sexp.t
val sexp_of_pat : pat -> Sexplib0.Sexp.t
val sexp_of_field_pat : field_pat -> Sexplib0.Sexp.t
val sexp_of_cf_kind : cf_kind -> Sexplib0.Sexp.t
val sexp_of_expr' : expr' -> Sexplib0.Sexp.t
val sexp_of_expr : expr -> Sexplib0.Sexp.t
val sexp_of_quote : quote -> Sexplib0.Sexp.t
val sexp_of_supported_monads : supported_monads -> Sexplib0.Sexp.t
val sexp_of_loop_kind : loop_kind -> Sexplib0.Sexp.t
val sexp_of_loop_state : loop_state -> Sexplib0.Sexp.t
val sexp_of_lhs : lhs -> Sexplib0.Sexp.t
val sexp_of_guard : guard -> Sexplib0.Sexp.t
val sexp_of_guard' : guard' -> Sexplib0.Sexp.t
val sexp_of_arm' : arm' -> Sexplib0.Sexp.t
val sexp_of_arm : arm -> Sexplib0.Sexp.t
val hash_fold_ty :
Base__.Ppx_hash_lib.Std.Hash.state ->
ty ->
Base__.Ppx_hash_lib.Std.Hash.state
val hash_fold_generic_value :
Base__.Ppx_hash_lib.Std.Hash.state ->
generic_value ->
Base__.Ppx_hash_lib.Std.Hash.state
val hash_fold_impl_expr :
Base__.Ppx_hash_lib.Std.Hash.state ->
impl_expr ->
Base__.Ppx_hash_lib.Std.Hash.state
val hash_fold_impl_expr_kind :
Ppx_hash_lib.Std.Hash.state ->
impl_expr_kind ->
Ppx_hash_lib.Std.Hash.state
val hash_fold_trait_goal :
Ppx_hash_lib.Std.Hash.state ->
trait_goal ->
Ppx_hash_lib.Std.Hash.state
val hash_fold_dyn_trait_goal :
Base__.Ppx_hash_lib.Std.Hash.state ->
dyn_trait_goal ->
Base__.Ppx_hash_lib.Std.Hash.state
val hash_fold_impl_ident :
Ppx_hash_lib.Std.Hash.state ->
impl_ident ->
Ppx_hash_lib.Std.Hash.state
val hash_fold_projection_predicate :
Ppx_hash_lib.Std.Hash.state ->
projection_predicate ->
Ppx_hash_lib.Std.Hash.state
val hash_fold_pat' :
Ppx_hash_lib.Std.Hash.state ->
pat' ->
Ppx_hash_lib.Std.Hash.state
val hash_fold_pat :
Base__.Ppx_hash_lib.Std.Hash.state ->
pat ->
Base__.Ppx_hash_lib.Std.Hash.state
val hash_fold_field_pat :
Base__.Ppx_hash_lib.Std.Hash.state ->
field_pat ->
Base__.Ppx_hash_lib.Std.Hash.state
val hash_fold_cf_kind :
Ppx_hash_lib.Std.Hash.state ->
cf_kind ->
Ppx_hash_lib.Std.Hash.state
val hash_fold_expr' :
Ppx_hash_lib.Std.Hash.state ->
expr' ->
Ppx_hash_lib.Std.Hash.state
val hash_fold_expr :
Base__.Ppx_hash_lib.Std.Hash.state ->
expr ->
Base__.Ppx_hash_lib.Std.Hash.state
val hash_fold_quote :
Ppx_hash_lib.Std.Hash.state ->
quote ->
Ppx_hash_lib.Std.Hash.state
val hash_fold_supported_monads :
Ppx_hash_lib.Std.Hash.state ->
supported_monads ->
Ppx_hash_lib.Std.Hash.state
val hash_fold_loop_kind :
Ppx_hash_lib.Std.Hash.state ->
loop_kind ->
Ppx_hash_lib.Std.Hash.state
val hash_fold_loop_state :
Base__.Ppx_hash_lib.Std.Hash.state ->
loop_state ->
Base__.Ppx_hash_lib.Std.Hash.state
val hash_fold_lhs :
Ppx_hash_lib.Std.Hash.state ->
lhs ->
Ppx_hash_lib.Std.Hash.state
val hash_fold_guard :
Base__.Ppx_hash_lib.Std.Hash.state ->
guard ->
Base__.Ppx_hash_lib.Std.Hash.state
val hash_fold_guard' :
Ppx_hash_lib.Std.Hash.state ->
guard' ->
Ppx_hash_lib.Std.Hash.state
val hash_fold_arm' :
Ppx_hash_lib.Std.Hash.state ->
arm' ->
Ppx_hash_lib.Std.Hash.state
val hash_fold_arm :
Base__.Ppx_hash_lib.Std.Hash.state ->
arm ->
Base__.Ppx_hash_lib.Std.Hash.state
val hash_ty : ty -> Ppx_hash_lib.Std.Hash.hash_value
val hash_generic_value : generic_value -> Ppx_hash_lib.Std.Hash.hash_value
val hash_impl_expr : impl_expr -> Ppx_hash_lib.Std.Hash.hash_value
val hash_impl_expr_kind : impl_expr_kind -> Ppx_hash_lib.Std.Hash.hash_value
val hash_trait_goal : trait_goal -> Ppx_hash_lib.Std.Hash.hash_value
val hash_dyn_trait_goal : dyn_trait_goal -> Ppx_hash_lib.Std.Hash.hash_value
val hash_impl_ident : impl_ident -> Ppx_hash_lib.Std.Hash.hash_value
val hash_projection_predicate :
projection_predicate ->
Ppx_hash_lib.Std.Hash.hash_value
val hash_pat' : pat' -> Ppx_hash_lib.Std.Hash.hash_value
val hash_pat : pat -> Ppx_hash_lib.Std.Hash.hash_value
val hash_field_pat : field_pat -> Ppx_hash_lib.Std.Hash.hash_value
val hash_cf_kind : cf_kind -> Ppx_hash_lib.Std.Hash.hash_value
val hash_expr' : expr' -> Ppx_hash_lib.Std.Hash.hash_value
val hash_expr : expr -> Ppx_hash_lib.Std.Hash.hash_value
val hash_quote : quote -> Ppx_hash_lib.Std.Hash.hash_value
val hash_supported_monads :
supported_monads ->
Ppx_hash_lib.Std.Hash.hash_value
val hash_loop_kind : loop_kind -> Ppx_hash_lib.Std.Hash.hash_value
val hash_loop_state : loop_state -> Ppx_hash_lib.Std.Hash.hash_value
val hash_lhs : lhs -> Ppx_hash_lib.Std.Hash.hash_value
val hash_guard : guard -> Ppx_hash_lib.Std.Hash.hash_value
val hash_guard' : guard' -> Ppx_hash_lib.Std.Hash.hash_value
val hash_arm' : arm' -> Ppx_hash_lib.Std.Hash.hash_value
val hash_arm : arm -> Ppx_hash_lib.Std.Hash.hash_value
type generic_param = {
ident : Local_ident.t;
span : Span.t;
attrs : Hax_engine__Ast.attr Prelude.list;
kind : generic_param_kind;
}
and generic_constraint =
| GCLifetime of Prelude.string * F.lifetime
| GCType of impl_ident
| GCProjection of projection_predicate
val pp_generic_param :
Ppx_deriving_runtime.Format.formatter ->
generic_param ->
Ppx_deriving_runtime.unit
val show_generic_param : generic_param -> Ppx_deriving_runtime.string
val pp_generic_param_kind :
Ppx_deriving_runtime.Format.formatter ->
generic_param_kind ->
Ppx_deriving_runtime.unit
val show_generic_param_kind : generic_param_kind -> Ppx_deriving_runtime.string
val pp_generic_constraint :
Ppx_deriving_runtime.Format.formatter ->
generic_constraint ->
Ppx_deriving_runtime.unit
val show_generic_constraint : generic_constraint -> Ppx_deriving_runtime.string
val equal_generic_param :
generic_param ->
generic_param ->
Ppx_deriving_runtime.bool
val equal_generic_param_kind :
generic_param_kind ->
generic_param_kind ->
Ppx_deriving_runtime.bool
val equal_generic_constraint :
generic_constraint ->
generic_constraint ->
Ppx_deriving_runtime.bool
val generic_param_of_yojson :
Ppx_yojson_conv_lib.Yojson.Safe.t ->
generic_param
val generic_param_kind_of_yojson :
Ppx_yojson_conv_lib.Yojson.Safe.t ->
generic_param_kind
val generic_constraint_of_yojson :
Ppx_yojson_conv_lib.Yojson.Safe.t ->
generic_constraint
val yojson_of_generic_param :
generic_param ->
Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_generic_param_kind :
generic_param_kind ->
Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_generic_constraint :
generic_constraint ->
Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_generic_param : generic_param -> generic_param -> Prelude.int
val compare_generic_param_kind :
generic_param_kind ->
generic_param_kind ->
Prelude.int
val compare_generic_constraint :
generic_constraint ->
generic_constraint ->
Prelude.int
val generic_param_of_sexp : Sexplib0.Sexp.t -> generic_param
val generic_param_kind_of_sexp : Sexplib0__.Sexp.t -> generic_param_kind
val generic_constraint_of_sexp : Sexplib0.Sexp.t -> generic_constraint
val sexp_of_generic_param : generic_param -> Sexplib0.Sexp.t
val sexp_of_generic_param_kind : generic_param_kind -> Sexplib0.Sexp.t
val sexp_of_generic_constraint : generic_constraint -> Sexplib0.Sexp.t
val hash_fold_generic_param :
Ppx_hash_lib.Std.Hash.state ->
generic_param ->
Ppx_hash_lib.Std.Hash.state
val hash_fold_generic_param_kind :
Ppx_hash_lib.Std.Hash.state ->
generic_param_kind ->
Ppx_hash_lib.Std.Hash.state
val hash_fold_generic_constraint :
Ppx_hash_lib.Std.Hash.state ->
generic_constraint ->
Ppx_hash_lib.Std.Hash.state
val hash_generic_param : generic_param -> Ppx_hash_lib.Std.Hash.hash_value
val hash_generic_param_kind :
generic_param_kind ->
Ppx_hash_lib.Std.Hash.hash_value
val hash_generic_constraint :
generic_constraint ->
Ppx_hash_lib.Std.Hash.hash_value
type param = {
pat : pat;
typ : ty;
typ_span : Span.t Prelude.option;
attrs : Hax_engine__Ast.attr Prelude.list;
}
and variant = {
name : Concrete_ident.t;
arguments : (Concrete_ident.t * ty * Hax_engine__Ast.attr Prelude.list)
Prelude.list;
is_record : Prelude.bool;
attrs : Hax_engine__Ast.attr Prelude.list;
}
and item' =
| Fn of {
name : Concrete_ident.t;
generics : generics;
body : expr;
params : param Prelude.list;
safety : safety_kind;
}
| TyAlias of {
name : Concrete_ident.t;
generics : generics;
ty : ty;
}
| Type of {
name : Concrete_ident.t;
generics : generics;
variants : variant Prelude.list;
is_struct : Prelude.bool;
}
| IMacroInvokation of {
macro : Concrete_ident.t;
argument : Prelude.string;
span : Span.t;
witness : F.macro;
}
| Trait of {
name : Concrete_ident.t;
generics : generics;
items : trait_item Prelude.list;
safety : safety_kind;
}
| Impl of {
generics : generics;
self_ty : ty;
of_trait : Concrete_ident.t * generic_value Prelude.list;
items : impl_item Prelude.list;
parent_bounds : (impl_expr * impl_ident) Prelude.list;
safety : safety_kind;
}
| Alias of {
name : Concrete_ident.t;
item : Concrete_ident.t;
}
| Use of {
path : Prelude.string Prelude.list;
is_external : Prelude.bool;
rename : Prelude.string Prelude.option;
}
| HaxError of Prelude.string
| NotImplementedYet
and item = {
v : item';
span : Span.t;
ident : Concrete_ident.t;
attrs : Hax_engine__Ast.attr Prelude.list;
}
and impl_item' =
| IIType of {
typ : ty;
parent_bounds : (impl_expr * impl_ident) Prelude.list;
}
| IIFn of {
body : expr;
params : param Prelude.list;
}
and impl_item = {
ii_span : Span.t;
ii_generics : generics;
ii_v : impl_item';
ii_ident : Concrete_ident.t;
ii_attrs : Hax_engine__Ast.attr Prelude.list;
}
and trait_item' =
| TIType of impl_ident Prelude.list
| TIFn of ty
| TIDefault of {
params : param Prelude.list;
body : expr;
witness : F.trait_item_default;
}
and trait_item = {
ti_span : Span.t;
ti_generics : generics;
ti_v : trait_item';
ti_ident : Concrete_ident.t;
ti_attrs : Hax_engine__Ast.attr Prelude.list;
}
val pp_param :
Ppx_deriving_runtime.Format.formatter ->
param ->
Ppx_deriving_runtime.unit
val show_param : param -> Ppx_deriving_runtime.string
val pp_generics :
Ppx_deriving_runtime.Format.formatter ->
generics ->
Ppx_deriving_runtime.unit
val show_generics : generics -> Ppx_deriving_runtime.string
val pp_variant :
Ppx_deriving_runtime.Format.formatter ->
variant ->
Ppx_deriving_runtime.unit
val show_variant : variant -> Ppx_deriving_runtime.string
val pp_item' :
Ppx_deriving_runtime.Format.formatter ->
item' ->
Ppx_deriving_runtime.unit
val show_item' : item' -> Ppx_deriving_runtime.string
val pp_item :
Ppx_deriving_runtime.Format.formatter ->
item ->
Ppx_deriving_runtime.unit
val show_item : item -> Ppx_deriving_runtime.string
val pp_impl_item' :
Ppx_deriving_runtime.Format.formatter ->
impl_item' ->
Ppx_deriving_runtime.unit
val show_impl_item' : impl_item' -> Ppx_deriving_runtime.string
val pp_impl_item :
Ppx_deriving_runtime.Format.formatter ->
impl_item ->
Ppx_deriving_runtime.unit
val show_impl_item : impl_item -> Ppx_deriving_runtime.string
val pp_trait_item' :
Ppx_deriving_runtime.Format.formatter ->
trait_item' ->
Ppx_deriving_runtime.unit
val show_trait_item' : trait_item' -> Ppx_deriving_runtime.string
val pp_trait_item :
Ppx_deriving_runtime.Format.formatter ->
trait_item ->
Ppx_deriving_runtime.unit
val show_trait_item : trait_item -> Ppx_deriving_runtime.string
val equal_impl_item' : impl_item' -> impl_item' -> Ppx_deriving_runtime.bool
val equal_trait_item' : trait_item' -> trait_item' -> Ppx_deriving_runtime.bool
val equal_trait_item : trait_item -> trait_item -> Ppx_deriving_runtime.bool
val param_of_yojson : Yojson.Safe.t -> param
val generics_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> generics
val variant_of_yojson : Yojson.Safe.t -> variant
val item'_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> item'
val item_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> item
val impl_item'_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> impl_item'
val impl_item_of_yojson : Yojson.Safe.t -> impl_item
val trait_item'_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> trait_item'
val trait_item_of_yojson : Yojson.Safe.t -> trait_item
val yojson_of_param : param -> Yojson.Safe.t
val yojson_of_generics : generics -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_variant : variant -> Yojson.Safe.t
val yojson_of_item' : item' -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_item : item -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_impl_item' : impl_item' -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_impl_item : impl_item -> Yojson.Safe.t
val yojson_of_trait_item' : trait_item' -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_trait_item : trait_item -> Yojson.Safe.t
val compare_param : param -> param -> Prelude.int
val compare_generics : generics -> generics -> Prelude.int
val compare_variant : variant -> variant -> Prelude.int
val compare_item' : item' -> item' -> Prelude.int
val compare_item : item -> item -> Prelude.int
val compare_impl_item' : impl_item' -> impl_item' -> Prelude.int
val compare_impl_item : impl_item -> impl_item -> Prelude.int
val compare_trait_item' : trait_item' -> trait_item' -> Prelude.int
val compare_trait_item : trait_item -> trait_item -> Prelude.int
val param_of_sexp : Sexplib0.Sexp.t -> param
val generics_of_sexp : Sexplib0__.Sexp.t -> generics
val variant_of_sexp : Sexplib0.Sexp.t -> variant
val item'_of_sexp : Sexplib0__.Sexp.t -> item'
val item_of_sexp : Sexplib0.Sexp.t -> item
val impl_item'_of_sexp : Sexplib0__.Sexp.t -> impl_item'
val impl_item_of_sexp : Sexplib0.Sexp.t -> impl_item
val trait_item'_of_sexp : Sexplib0__.Sexp.t -> trait_item'
val trait_item_of_sexp : Sexplib0.Sexp.t -> trait_item
val sexp_of_param : param -> Sexplib0.Sexp.t
val sexp_of_generics : generics -> Sexplib0.Sexp.t
val sexp_of_variant : variant -> Sexplib0.Sexp.t
val sexp_of_item' : item' -> Sexplib0.Sexp.t
val sexp_of_item : item -> Sexplib0.Sexp.t
val sexp_of_impl_item' : impl_item' -> Sexplib0.Sexp.t
val sexp_of_impl_item : impl_item -> Sexplib0.Sexp.t
val sexp_of_trait_item' : trait_item' -> Sexplib0.Sexp.t
val sexp_of_trait_item : trait_item -> Sexplib0.Sexp.t
val hash_fold_param :
Base__.Ppx_hash_lib.Std.Hash.state ->
param ->
Base__.Ppx_hash_lib.Std.Hash.state
val hash_fold_generics :
Ppx_hash_lib.Std.Hash.state ->
generics ->
Ppx_hash_lib.Std.Hash.state
val hash_fold_variant :
Base__.Ppx_hash_lib.Std.Hash.state ->
variant ->
Base__.Ppx_hash_lib.Std.Hash.state
val hash_fold_item' :
Ppx_hash_lib.Std.Hash.state ->
item' ->
Ppx_hash_lib.Std.Hash.state
val hash_fold_item :
Ppx_hash_lib.Std.Hash.state ->
item ->
Ppx_hash_lib.Std.Hash.state
val hash_fold_impl_item' :
Ppx_hash_lib.Std.Hash.state ->
impl_item' ->
Ppx_hash_lib.Std.Hash.state
val hash_fold_impl_item :
Base__.Ppx_hash_lib.Std.Hash.state ->
impl_item ->
Base__.Ppx_hash_lib.Std.Hash.state
val hash_fold_trait_item' :
Ppx_hash_lib.Std.Hash.state ->
trait_item' ->
Ppx_hash_lib.Std.Hash.state
val hash_fold_trait_item :
Base__.Ppx_hash_lib.Std.Hash.state ->
trait_item ->
Base__.Ppx_hash_lib.Std.Hash.state
val hash_param : param -> Ppx_hash_lib.Std.Hash.hash_value
val hash_generics : generics -> Ppx_hash_lib.Std.Hash.hash_value
val hash_variant : variant -> Ppx_hash_lib.Std.Hash.hash_value
val hash_item' : item' -> Ppx_hash_lib.Std.Hash.hash_value
val hash_item : item -> Ppx_hash_lib.Std.Hash.hash_value
val hash_impl_item' : impl_item' -> Ppx_hash_lib.Std.Hash.hash_value
val hash_impl_item : impl_item -> Ppx_hash_lib.Std.Hash.hash_value
val hash_trait_item' : trait_item' -> Ppx_hash_lib.Std.Hash.hash_value
val hash_trait_item : trait_item -> Ppx_hash_lib.Std.Hash.hash_value
type modul = item Prelude.list
val make_hax_error_item : Span.t -> Concrete_ident.t -> Prelude.string -> item
module Visitors : sig ... end
module SideEffects : sig ... end
module Hoist : sig ... end