Make (hax-engine.Hax_engine.Ast

Parameters

module F : Features.T

Signature

module AST : sig ... end

module TypedLocalIdent : sig ... end

module Visitors : sig ... end

module M : sig ... end

module D : sig ... end

module Expect : sig ... end

module Sets : sig ... end

val functions_of_item : 
  AST.item ->
  (Ast.concrete_ident * AST.expr) Prelude.list

module Mappers : sig ... end

module Reducers : sig ... end

val fresh_local_ident_in : 
  Ast.local_ident Prelude.list ->
  Prelude.string ->
  Local_ident.t

Produces a local identifier which is locally fresh **with respect to variables

ars}**.

val fresh_local_ident_in_expr : 
  AST.expr Prelude.list ->
  Prelude.string ->
  Local_ident.t

Produces a local identifier which is locally fresh **with respect to expressions xprs**.

val never_typ : AST.ty

val is_never_typ : AST.ty -> Prelude.bool

val unit_typ : AST.ty

val unit_expr : Span.t -> AST.expr

val remove_tuple1_pat : AST.pat -> AST.pat

val remove_tuple1 : AST.ty -> AST.ty

val remove_unsize : AST.expr -> AST.expr

val beta_reduce_closure_opt : AST.expr -> AST.expr Prelude.option

See beta_reduce_closure's documentation.

val beta_reduce_closure : AST.expr -> AST.expr

Reduces a (|x1, ..., xN| body)(e1, ..., eN) to body[x1/e1, ..., xN/eN]. This assumes the arities are right: (|x, y| ...)(e1).

val is_unit_typ : AST.ty -> Prelude.bool

val pat_is_expr : AST.pat -> AST.expr -> Ppx_deriving_runtime.bool

val make_let : AST.pat -> AST.expr -> AST.expr -> AST.expr

val make_lets : (AST.pat * AST.expr) Prelude.list -> AST.expr -> AST.expr

val make_var_pat : Ast.local_ident -> AST.ty -> Ast.span -> AST.pat

val ty_equality : AST.ty -> AST.ty -> Prelude.bool

val let_of_binding : (Ast.local_ident * AST.expr) -> AST.expr -> AST.expr

val lets_of_bindings : 
  (Ast.local_ident * AST.expr) Prelude.list ->
  AST.expr ->
  AST.expr

val make_tuple_typ' : AST.ty Prelude.list -> AST.ty

val make_tuple_typ : AST.ty Prelude.list -> AST.ty

val make_unit_param : Ast.span -> AST.param

val make_seq : AST.expr -> AST.expr -> AST.expr

val make_tuple_field_pat : 
  Prelude.int ->
  Prelude.int ->
  AST.pat ->
  AST.field_pat

val make_tuple_pat'' : Span.t -> AST.field_pat Prelude.list -> AST.pat

val make_tuple_pat' : AST.pat Prelude.list -> AST.pat

val make_tuple_pat : AST.pat Prelude.list -> AST.pat

val make_tuple_expr' : span:Ast.span -> AST.expr Prelude.list -> AST.expr

val make_tuple_expr : span:Ast.span -> AST.expr Prelude.list -> AST.expr

val call_Constructor' : 
  Ast.global_ident ->
  Prelude.bool ->
  AST.expr Prelude.list ->
  Span.t ->
  AST.ty ->
  AST.expr

val call_Constructor : 
  Concrete_ident.name ->
  Prelude.bool ->
  AST.expr Prelude.list ->
  Span.t ->
  AST.ty ->
  AST.expr

val call' : 
  ?impl:AST.impl_expr ->
  [ `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 ] ] ->
  ?generic_args:AST.generic_value Prelude.list ->
  ?impl_generic_args:AST.generic_value Prelude.list ->
  AST.expr Prelude.list ->
  Span.t ->
  AST.ty ->
  AST.expr

val call : 
  ?kind:Concrete_ident.Kind.t ->
  ?generic_args:AST.generic_value Prelude.list ->
  ?impl_generic_args:AST.generic_value Prelude.list ->
  ?impl:AST.impl_expr ->
  Concrete_ident.name ->
  AST.expr Prelude.list ->
  Span.t ->
  AST.ty ->
  AST.expr

val make_closure : AST.pat Prelude.list -> AST.expr -> Ast.span -> AST.expr

val string_lit : Span.t -> Prelude.string -> AST.expr

val hax_failure_expr' : 
  Span.t ->
  AST.ty ->
  (Diagnostics.Context.t * Diagnostics.kind) ->
  Prelude.string ->
  AST.expr

val hax_failure_expr : 
  Span.t ->
  AST.ty ->
  (Diagnostics.Context.t * Diagnostics.kind) ->
  Ast.Full.expr ->
  AST.expr

val hax_failure_typ : AST.ty

module LiftToFullAst : sig ... end

module Debug : sig ... end

val unbox_expr' : (AST.expr -> AST.expr) -> AST.expr -> AST.expr

val underef_expr' : (AST.expr -> AST.expr) -> AST.expr -> AST.expr

val unbox_expr : AST.expr -> AST.expr

val underef_expr : AST.expr -> AST.expr

val unbox_underef_expr : AST.expr -> AST.expr

val param_of_generic_const_param : 
  AST.generic_param ->
  AST.param Prelude.option

val kind_of_item : AST.item -> Ast.item_kind

val expr_of_lhs : Ast.span -> AST.lhs -> AST.expr

val collect_let_bindings' : 
  AST.expr ->
  (AST.pat * AST.expr * AST.ty) Prelude.list * AST.expr

val collect_let_bindings : 
  AST.expr ->
  (AST.pat * AST.expr) Prelude.list * AST.expr

val map_body_of_nested_lets : (AST.expr -> AST.expr) -> AST.expr -> AST.expr

val tuple_projector : 
  Span.t ->
  AST.ty ->
  Prelude.int ->
  Prelude.int ->
  AST.ty ->
  AST.expr

val project_tuple : 
  AST.expr ->
  Prelude.int ->
  Prelude.int ->
  AST.ty ->
  AST.expr

val concat_generics : AST.generics -> AST.generics -> AST.generics

Concatenates the generics g1 and g2, making sure lifetimes appear first

module Place : sig ... end

module StringList : sig ... end