Module Pinterp_core.Value

module Value: sig .. end

(Mutable) values used in Pinterp

type float_mode = Mlmpfr_wrapper.mpfr_rnd_t 
type big_float = Mlmpfr_wrapper.mpfr_float 
type value = private {
   v_desc : value_desc;
   v_ty : Ty.ty;
type field 
type value_desc = 
| Vconstr of Expr.rsymbol option * Expr.rsymbol list * field list (*

A constructor value (record or variant). The first argument is optional to handle records without constructors (e.g. when a type has an invariant, the constructor is not available to avoid creating an object that does not respect the invariant).

| Vnum of BigInt.t (*

Any integer number

| Vreal of Big_real.real
| Vfloat_mode of float_mode
| Vfloat of big_float
| Vstring of string
| Vbool of bool
| Vproj of Term.lsymbol * value (*

TODO/FIXME Was used to represent a model projection originating from a meta model_projection). Currently, projections are now handled using Vterm t with t an epsilon term.

| Varray of value array (*

An array created in code

| Vpurefun of Ty.ty * value Pinterp_core.Mv.t * value (*

TODO/FIXME Was used to represent arrays from the prover model. Currently, arrays are now handled using Vterm t with t a lambda term corresponding to the function defining the mapping of array elements.

| Vfun of value Term.Mvs.t * Term.vsymbol * Expr.expr (*

A function value

| Vterm of Term.term (*

The result of a pure expression

| Vundefined (*

An undefined value; unreducible