sig
  type float_mode = Why3deps.Mlmpfr_wrapper.mpfr_rnd_t
  type big_float = Why3deps.Mlmpfr_wrapper.mpfr_float
  type value = private {
    v_desc : Pinterp_core.Value.value_desc;
    v_ty : Why3.Ty.ty;
  }
  and field
  and value_desc =
      Vconstr of Why3.Expr.rsymbol option * Why3.Expr.rsymbol list *
        Pinterp_core.Value.field list
    | Vnum of Why3.BigInt.t
    | Vreal of Why3.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 Why3.Term.lsymbol * Pinterp_core.Value.value
    | Varray of Pinterp_core.Value.value array
    | Vpurefun of Why3.Ty.ty * Pinterp_core.Value.value Pinterp_core.Mv.t *
        Pinterp_core.Value.value
    | Vfun of Pinterp_core.Value.value Why3.Term.Mvs.t * Why3.Term.vsymbol *
        Why3.Expr.expr
    | Vterm of Why3.Term.term
    | Vundefined
end