sig
  val init_real : int * int * int -> unit
  type ctx
  val mk_empty_env : Env.env -> Pmodule.pmodule -> Pinterp_core.env
  val mk_rac :
    ?ignore_incomplete:bool -> Pinterp_core.check_term -> Pinterp_core.rac
  val mk_ctx :
    Pinterp_core.env ->
    limits:Call_provers.resource_limits ->
    ?giant_steps:bool ->
    ?do_rac:bool ->
    ?rac:Pinterp_core.rac ->
    ?oracle:Pinterp_core.oracle ->
    ?compute_term:(Pinterp_core.env -> Term.term -> Term.term) ->
    unit -> Pinterp.ctx
  val get_env : Pinterp.ctx -> Pinterp_core.env
  val get_do_rac : Pinterp.ctx -> bool
  val get_rac : Pinterp.ctx -> Pinterp_core.rac
  val get_giant_steps : Pinterp.ctx -> bool
  type result =
      Normal of Pinterp_core.Value.value
    | Excep of Ity.xsymbol * Pinterp_core.Value.value
    | Irred of Expr.expr
  val print_logic_result : Pinterp.result Pp.pp
  val exec_rs : Pinterp.ctx -> Expr.rsymbol -> Pinterp.result * Pinterp.ctx
  val exec_global_fundef :
    Pinterp.ctx ->
    (Expr.rsymbol * Expr.cexp) list ->
    Expr.rec_defn list option ->
    Expr.expr ->
    Pinterp.result * Pinterp_core.Value.value Term.Mvs.t *
    Pinterp_core.Value.value Stdlib.Lazy.t Expr.Mrs.t
  val report_eval_result :
    Expr.expr ->
    Stdlib.Format.formatter ->
    Pinterp.result * Pinterp_core.Value.value Term.Mvs.t *
    Pinterp_core.Value.value Stdlib.Lazy.t Expr.Mrs.t -> unit
  val report_cntr : (Pinterp_core.cntr_ctx * Term.term) Pp.pp
  val debug_disable_builtin_mach : Debug.flag
  val debug_rac_values : Debug.flag
end