sig
  module rec Value :
    sig
      type float_mode = Mlmpfr_wrapper.mpfr_rnd_t
      type big_float = Mlmpfr_wrapper.mpfr_float
      type value = private {
        v_desc : Pinterp_core.Value.value_desc;
        v_ty : Ty.ty;
      }
      and field
      and value_desc =
          Vconstr of Expr.rsymbol option * Expr.rsymbol list *
            Pinterp_core.Value.field list
        | Vnum of BigInt.t
        | Vreal of Big_real.real
        | Vfloat_mode of Pinterp_core.Value.float_mode
        | Vfloat of Pinterp_core.Value.big_float
        | Vstring of string
        | Vbool of bool
        | Vproj of Term.lsymbol * Pinterp_core.Value.value
        | Varray of Pinterp_core.Value.value array
        | Vpurefun of Ty.ty * Pinterp_core.Value.value Pinterp_core.Mv.t *
            Pinterp_core.Value.value
        | Vfun of Pinterp_core.Value.value Term.Mvs.t * Term.vsymbol *
            Expr.expr
        | Vterm of Term.term
        | Vundefined
    end
  and Mv :
    sig
      type key = Value.value
      type +'a t
      val empty : 'a t
      val is_empty : 'a t -> bool
      val mem : key -> 'a t -> bool
      val add : key -> 'a -> 'a t -> 'a t
      val singleton : key -> 'a -> 'a t
      val remove : key -> 'a t -> 'a t
      val merge :
        (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
      val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
      val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
      val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val for_all : (key -> 'a -> bool) -> 'a t -> bool
      val exists : (key -> 'a -> bool) -> 'a t -> bool
      val filter : (key -> 'a -> bool) -> 'a t -> 'a t
      val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
      val cardinal : 'a t -> int
      val bindings : 'a t -> (key * 'a) list
      val min_binding : 'a t -> key * 'a
      val max_binding : 'a t -> key * 'a
      val choose : 'a t -> key * 'a
      val split : key -> 'a t -> 'a t * 'a option * 'a t
      val find : key -> 'a t -> 'a
      val map : ('a -> 'b) -> 'a t -> 'b t
      val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
      val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
      val inter : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
      val diff : (key -> 'a -> 'b -> 'a option) -> 'a t -> 'b t -> 'a t
      val submap : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
      val disjoint : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
      val set_union : 'a t -> 'a t -> 'a t
      val set_inter : 'a t -> 'b t -> 'a t
      val set_diff : 'a t -> 'b t -> 'a t
      val set_submap : 'a t -> 'b t -> bool
      val set_disjoint : 'a t -> 'b t -> bool
      val set_compare : 'a t -> 'b t -> int
      val set_equal : 'a t -> 'b t -> bool
      val find_def : 'a -> key -> 'a t -> 'a
      val find_opt : key -> 'a t -> 'a option
      val find_exn : exn -> key -> 'a t -> 'a
      val map_filter : ('a -> 'b option) -> 'a t -> 'b t
      val mapi_filter : (key -> 'a -> 'b option) -> 'a t -> 'b t
      val mapi_fold :
        (key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
      val mapi_filter_fold :
        (key -> 'a -> 'acc -> 'acc * 'b option) ->
        'a t -> 'acc -> 'acc * 'b t
      val fold_left : ('b -> key -> 'a -> 'b) -> 'b -> 'a t -> 'b
      val fold2_inter :
        (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
      val fold2_union :
        (key -> 'a option -> 'b option -> 'c -> 'c) ->
        'a t -> 'b t -> 'c -> 'c
      val translate : (key -> key) -> 'a t -> 'a t
      val add_new : exn -> key -> 'a -> 'a t -> 'a t
      val replace : exn -> key -> 'a -> 'a t -> 'a t
      val keys : 'a t -> key list
      val values : 'a t -> 'a list
      val of_list : (key * 'a) list -> 'a t
      val contains : 'a t -> key -> bool
      val domain : 'a t -> unit t
      val subdomain : (key -> 'a -> bool) -> 'a t -> unit t
      val is_num_elt : int -> 'a t -> bool
      type 'a enumeration
      val val_enum : 'a enumeration -> (key * 'a) option
      val start_enum : 'a t -> 'a enumeration
      val next_enum : 'a enumeration -> 'a enumeration
      val start_ge_enum : key -> 'a t -> 'a enumeration
      val next_ge_enum : key -> 'a enumeration -> 'a enumeration
    end
  val print_value :
    Stdlib.Format.formatter -> Pinterp_core.Value.value -> unit
  val compare_values :
    Pinterp_core.Value.value -> Pinterp_core.Value.value -> int
  val v_ty : Pinterp_core.Value.value -> Ty.ty
  val v_desc : Pinterp_core.Value.value -> Pinterp_core.Value.value_desc
  val field : Pinterp_core.Value.value -> Pinterp_core.Value.field
  val field_get : Pinterp_core.Value.field -> Pinterp_core.Value.value
  val field_set :
    Pinterp_core.Value.field -> Pinterp_core.Value.value -> unit
  val bool_value : bool -> Pinterp_core.Value.value
  val int_value : BigInt.t -> Pinterp_core.Value.value
  val string_value : string -> Pinterp_core.Value.value
  val num_value : Ity.ity -> BigInt.t -> Pinterp_core.Value.value
  val float_value :
    Ity.ity -> Pinterp_core.Value.big_float -> Pinterp_core.Value.value
  val real_value : Big_real.real -> Pinterp_core.Value.value
  val constr_value :
    Ity.ity ->
    Expr.rsymbol option ->
    Expr.rsymbol list ->
    Pinterp_core.Value.value list -> Pinterp_core.Value.value
  val purefun_value :
    result_ity:Ity.ity ->
    arg_ity:Ity.ity ->
    Pinterp_core.Value.value Pinterp_core.Mv.t ->
    Pinterp_core.Value.value -> Pinterp_core.Value.value
  val unit_value : Pinterp_core.Value.value
  val range_value : Ity.ity -> BigInt.t -> Pinterp_core.Value.value
  val term_value : Ity.ity -> Term.term -> Pinterp_core.Value.value
  val snapshot : Pinterp_core.Value.value -> Pinterp_core.Value.value
  val snapshot_vsenv :
    Pinterp_core.Value.value Term.Mvs.t ->
    Pinterp_core.Value.value Term.Mvs.t
  val snapshot_oldies :
    Ity.pvsymbol Ity.Mpv.t ->
    Pinterp_core.Value.value Term.Mvs.t ->
    Pinterp_core.Value.value Term.Mvs.t
  module Log :
    sig
      type exec_mode = Exec_giant_steps | Exec_normal
      val pp_mode :
        Stdlib.Format.formatter -> Pinterp_core.Log.exec_mode -> unit
      type value_or_invalid = Value of Pinterp_core.Value.value | Invalid
      type log_entry_desc = private
          Val_assumed of (Ident.ident * Pinterp_core.Value.value)
        | Res_assumed of (Expr.rsymbol option * Pinterp_core.Value.value)
        | Const_init of Ident.ident
        | Exec_call of
            (Expr.rsymbol option * Pinterp_core.Value.value Term.Mvs.t *
             Pinterp_core.Log.exec_mode)
        | Exec_pure of (Term.lsymbol * Pinterp_core.Log.exec_mode)
        | Exec_any of
            (Expr.rsymbol option * Pinterp_core.Value.value Term.Mvs.t)
        | Iter_loop of Pinterp_core.Log.exec_mode
        | Exec_main of
            (Expr.rsymbol * Pinterp_core.Log.value_or_invalid Term.Mls.t *
             Pinterp_core.Value.value Term.Mvs.t *
             Pinterp_core.Log.value_or_invalid Expr.Mrs.t)
        | Exec_stucked of (string * Pinterp_core.Value.value Ident.Mid.t)
        | Exec_failed of (string * Pinterp_core.Value.value Ident.Mid.t)
        | Exec_ended
      type log_entry = private {
        log_desc : Pinterp_core.Log.log_entry_desc;
        log_loc : Loc.position option;
      }
      type exec_log
      type log_uc
      val log_val :
        Pinterp_core.Log.log_uc ->
        Ident.ident ->
        Pinterp_core.Value.value -> Loc.position option -> unit
      val log_const :
        Pinterp_core.Log.log_uc -> Ident.ident -> Loc.position option -> unit
      val log_call :
        Pinterp_core.Log.log_uc ->
        Expr.rsymbol option ->
        Pinterp_core.Value.value Term.Mvs.t ->
        Pinterp_core.Log.exec_mode -> Loc.position option -> unit
      val log_pure_call :
        Pinterp_core.Log.log_uc ->
        Term.lsymbol ->
        Pinterp_core.Log.exec_mode -> Loc.position option -> unit
      val log_any_call :
        Pinterp_core.Log.log_uc ->
        Expr.rsymbol option ->
        Pinterp_core.Value.value Term.Mvs.t -> Loc.position option -> unit
      val log_iter_loop :
        Pinterp_core.Log.log_uc ->
        Pinterp_core.Log.exec_mode -> Loc.position option -> unit
      val log_exec_main :
        Pinterp_core.Log.log_uc ->
        Expr.rsymbol ->
        Pinterp_core.Value.value Stdlib.Lazy.t Term.Mls.t ->
        Pinterp_core.Value.value Term.Mvs.t ->
        Pinterp_core.Value.value Stdlib.Lazy.t Expr.Mrs.t ->
        Loc.position option -> unit
      val log_failed :
        Pinterp_core.Log.log_uc ->
        string ->
        Pinterp_core.Value.value Ident.Mid.t -> Loc.position option -> unit
      val log_stucked :
        Pinterp_core.Log.log_uc ->
        string ->
        Pinterp_core.Value.value Ident.Mid.t -> Loc.position option -> unit
      val log_exec_ended :
        Pinterp_core.Log.log_uc -> Loc.position option -> unit
      val empty_log_uc : unit -> Pinterp_core.Log.log_uc
      val empty_log : Pinterp_core.Log.exec_log
      val get_log : Pinterp_core.Log.log_uc -> Pinterp_core.Log.exec_log
      val flush_log : Pinterp_core.Log.log_uc -> Pinterp_core.Log.exec_log
      val sort_log_by_loc :
        Pinterp_core.Log.exec_log ->
        Pinterp_core.Log.log_entry list Wstdlib.Mint.t Wstdlib.Mstr.t
      val json_log : Pinterp_core.Log.exec_log -> Json_base.json
      val print_log :
        ?verb_lvl:int -> json:bool -> Pinterp_core.Log.exec_log Pp.pp
      val get_exec_calls_and_loops :
        Env.env ->
        Pinterp_core.Log.exec_log -> Pinterp_core.Log.log_entry list
    end
  type premises
  val with_push_premises : Pinterp_core.premises -> (unit -> 'a) -> 'a
  val add_premises : Term.term list -> Pinterp_core.premises -> unit
  val fold_premises :
    ('a -> Term.term -> 'a) -> Pinterp_core.premises -> 'a -> 'a
  type env = {
    why_env : Env.env;
    pmodule : Pmodule.pmodule;
    funenv : (Expr.cexp * Expr.rec_defn list option) Expr.Mrs.t;
    vsenv : Pinterp_core.Value.value Term.Mvs.t;
    lsenv : Pinterp_core.Value.value Stdlib.Lazy.t Term.Mls.t;
    rsenv : Pinterp_core.Value.value Stdlib.Lazy.t Expr.Mrs.t;
    premises : Pinterp_core.premises;
    log_uc : Pinterp_core.Log.log_uc;
  }
  val mk_empty_env : Env.env -> Pmodule.pmodule -> Pinterp_core.env
  val get_vs : Pinterp_core.env -> Term.Mvs.key -> Pinterp_core.Value.value
  val get_pvs : Pinterp_core.env -> Ity.pvsymbol -> Pinterp_core.Value.value
  val bind_vs :
    Term.Mvs.key ->
    Pinterp_core.Value.value -> Pinterp_core.env -> Pinterp_core.env
  val bind_ls :
    Term.Mls.key ->
    Pinterp_core.Value.value Stdlib.Lazy.t ->
    Pinterp_core.env -> Pinterp_core.env
  val bind_rs :
    Expr.Mrs.key ->
    Pinterp_core.Value.value Stdlib.Lazy.t ->
    Pinterp_core.env -> Pinterp_core.env
  val bind_pvs :
    ?register:(Ident.ident -> Pinterp_core.Value.value -> unit) ->
    Ity.pvsymbol ->
    Pinterp_core.Value.value -> Pinterp_core.env -> Pinterp_core.env
  val multibind_pvs :
    ?register:(Ident.ident -> Pinterp_core.Value.value -> unit) ->
    Ity.pvsymbol list ->
    Pinterp_core.Value.value list -> Pinterp_core.env -> Pinterp_core.env
  exception Incomplete of string
  val incomplete :
    ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a
  val term_of_value :
    ?ty_mt:Ty.ty Ty.Mtv.t ->
    Pinterp_core.env ->
    (Term.vsymbol * Term.term) list ->
    Pinterp_core.Value.value -> (Term.vsymbol * Term.term) list * Term.term
  type compute_term = Pinterp_core.env -> Term.term -> Term.term
  val compute_term_dummy : Pinterp_core.compute_term
  val default_value_of_type :
    Pinterp_core.env -> Ity.ity -> Pinterp_core.Value.value
  type check_value = Ity.ity -> Pinterp_core.Value.value -> unit
  type oracle = {
    for_variable :
      Pinterp_core.env ->
      ?check:Pinterp_core.check_value ->
      loc:Loc.position option ->
      Ident.ident -> Ity.ity -> Pinterp_core.Value.value option;
    for_result :
      Pinterp_core.env ->
      ?check:Pinterp_core.check_value ->
      loc:Loc.position ->
      call_id:Expr.expr_id option ->
      Ity.ity -> Pinterp_core.Value.value option;
  }
  val oracle_dummy : Pinterp_core.oracle
  val register_used_value :
    Pinterp_core.env ->
    Loc.position option -> Ident.ident -> Pinterp_core.Value.value -> unit
  val register_res_value :
    Pinterp_core.env ->
    Loc.position -> Expr.rsymbol option -> Pinterp_core.Value.value -> unit
  val register_const_init :
    Pinterp_core.env -> Loc.position option -> Ident.ident -> unit
  val register_call :
    Pinterp_core.env ->
    Loc.position option ->
    Expr.rsymbol option ->
    Pinterp_core.Value.value Term.Mvs.t -> Pinterp_core.Log.exec_mode -> unit
  val register_pure_call :
    Pinterp_core.env ->
    Loc.position option -> Term.lsymbol -> Pinterp_core.Log.exec_mode -> unit
  val register_any_call :
    Pinterp_core.env ->
    Loc.position option ->
    Expr.rsymbol option -> Pinterp_core.Value.value Term.Mvs.t -> unit
  val register_iter_loop :
    Pinterp_core.env ->
    Loc.position option -> Pinterp_core.Log.exec_mode -> unit
  val register_exec_main : Pinterp_core.env -> Expr.rsymbol -> unit
  val register_failure :
    Pinterp_core.env ->
    Loc.position option ->
    string -> Pinterp_core.Value.value Ident.Mid.t -> unit
  val register_stucked :
    Pinterp_core.env ->
    Loc.position option ->
    string -> Pinterp_core.Value.value Ident.Mid.t -> unit
  val register_ended : Pinterp_core.env -> Loc.position option -> unit
  type cntr_ctx = {
    attr : Ident.attribute;
    desc : string option;
    loc : Loc.position option;
    attrs : Ident.Sattr.t;
    cntr_env : Pinterp_core.env;
    giant_steps : bool option;
  }
  val mk_cntr_ctx :
    Pinterp_core.env ->
    giant_steps:bool option ->
    ?loc:Loc.position ->
    ?attrs:Ident.Sattr.t ->
    ?desc:string -> Ident.attribute -> Pinterp_core.cntr_ctx
  val describe_cntr_ctx : Pinterp_core.cntr_ctx -> string
  val report_cntr_title : (Pinterp_core.cntr_ctx * string) Pp.pp
  val report_cntr_head : (Pinterp_core.cntr_ctx * string * Term.term) Pp.pp
  val report_cntr_body : (Pinterp_core.cntr_ctx * Term.term) Pp.pp
  val report_cntr : (Pinterp_core.cntr_ctx * string * Term.term) Pp.pp
  exception Fail of Pinterp_core.cntr_ctx * Term.term
  exception Stuck of Pinterp_core.cntr_ctx * Loc.position option * string
  val stuck :
    ?loc:Loc.position ->
    Pinterp_core.cntr_ctx ->
    ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a
  val stuck_for_fail :
    ?loc:Loc.position -> Pinterp_core.cntr_ctx -> Term.term -> 'a
  type check_term =
      ?vsenv:(Term.vsymbol * Term.term) list ->
      Pinterp_core.cntr_ctx -> Term.term -> unit
  val check_term_dummy : Pinterp_core.check_term
  type rac = {
    check_term : Pinterp_core.check_term;
    ignore_incomplete : bool;
  }
  val mk_rac :
    ?ignore_incomplete:bool -> Pinterp_core.check_term -> Pinterp_core.rac
  val rac_dummy : Pinterp_core.rac
  val check_term :
    Pinterp_core.rac ->
    ?vsenv:(Term.vsymbol * Term.term) list ->
    Pinterp_core.cntr_ctx -> Term.term -> unit
  val check_assume_term :
    Pinterp_core.rac -> Pinterp_core.cntr_ctx -> Term.term -> unit
  val check_terms :
    Pinterp_core.rac -> Pinterp_core.cntr_ctx -> Term.term list -> unit
  val check_assume_terms :
    Pinterp_core.rac -> Pinterp_core.cntr_ctx -> Term.term list -> unit
  val check_post :
    Pinterp_core.rac ->
    Pinterp_core.cntr_ctx -> Pinterp_core.Value.value -> Ity.post -> unit
  val check_posts :
    Pinterp_core.rac ->
    Pinterp_core.cntr_ctx ->
    Pinterp_core.Value.value -> Ity.post list -> unit
  val check_assume_posts :
    Pinterp_core.rac ->
    Pinterp_core.cntr_ctx ->
    Pinterp_core.Value.value -> Ity.post list -> unit
  val check_type_invs :
    Pinterp_core.rac ->
    ?loc:Loc.position ->
    giant_steps:bool ->
    Pinterp_core.env -> Ity.ity -> Pinterp_core.Value.value -> unit
  val check_assume_type_invs :
    Pinterp_core.rac ->
    ?loc:Loc.position ->
    giant_steps:bool ->
    Pinterp_core.env -> Ity.ity -> Pinterp_core.Value.value -> unit
  val oldify_varl :
    Pinterp_core.env ->
    (Term.term * Term.lsymbol option) list ->
    (Term.term * Term.lsymbol option) list *
    Pinterp_core.Value.value Term.Mvs.t
  val check_variant :
    Pinterp_core.rac ->
    Ident.Sattr.elt ->
    Loc.position option ->
    giant_steps:bool ->
    Pinterp_core.env ->
    (Term.term * Term.lsymbol option) list *
    Pinterp_core.Value.value Term.Mvs.t ->
    (Term.term * Term.lsymbol option) list -> unit
  val t_undefined : Ty.ty -> Term.term
  val ty_app_arg : Ty.tysymbol -> int -> Ty.ty -> Ty.ty
  val ity_components : Ity.ity -> Ity.itysymbol * Ity.ity list * Ity.ity list
  val is_range_ty : Ty.ty -> bool
  val debug_array_as_update_chains_not_epsilon : Debug.flag
  val undefined_value :
    Pinterp_core.env -> Ity.ity -> Pinterp_core.Value.value
  val debug_trace_exec : Debug.flag
  val pp_bindings :
    ?sep:unit Pp.pp ->
    ?pair_sep:unit Pp.pp ->
    ?delims:unit Pp.pp * unit Pp.pp ->
    'a Pp.pp -> 'b Pp.pp -> ('a * 'b) list Pp.pp
  val pp_env :
    'a Pp.pp -> 'b Pp.pp -> Stdlib.Format.formatter -> ('a * 'b) list -> unit
  val value :
    Ty.ty -> Pinterp_core.Value.value_desc -> Pinterp_core.Value.value
end