Module Pinterp_core.Value

module Value: sig .. end

(Mutable) values used in Pinterp

type float_mode = Why3deps.Mlmpfr_wrapper.mpfr_rnd_t

type big_float = Why3deps.Mlmpfr_wrapper.mpfr_float

type value = private {

	`v_desc : value_desc;`
	`v_ty : Why3.Ty.ty;`

}

type field

type value_desc =

`\|`	`Vconstr of Why3.Expr.rsymbol option * Why3.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 Why3.BigInt.t`	`(*`	Any integer number	`*)`
`\|`	`Vreal of Why3.Big_real.real`
`\|`	`Vfloat_mode of float_mode`
`\|`	`Vfloat of big_float`
`\|`	`Vstring of string`
`\|`	`Vbool of bool`
`\|`	`Vproj of Why3.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 Why3.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 Why3.Term.Mvs.t * Why3.Term.vsymbol * Why3.Expr.expr`	`(*`	A function value	`*)`
`\|`	`Vterm of Why3.Term.term`	`(*`	The result of a pure expression	`*)`
`\|`	`Vundefined`	`(*`	An undefined value; unreducible	`*)`