== Values

A *value* is one of the following:

* A primitive integer value

* An integer value

* A floating-point value

* A Boolean value

* A string value

* An abstract type value

* An anonymous array value

* An array value

* An enumeration value

* An anonymous struct value

* A struct value

Every value _v_ belongs to exactly one <<Types_Canonical-Types,canonical type>>
_T_, except that
every string value belongs to every string type.

Every value that belongs to type _T_ also belongs to every
<<Types_Alias-Types,alias type>> whose
<<Types_Underlying-Types,underlying type>> is _T_.

When a value _v_ belongs to a type _T_, we say that _v_ is a value
*of type _T_*.

In the following subsections, we describe each kind of value and
its associated canonical types.

=== Primitive Integer Values

A *primitive integer value* is an ordinary (mathematical) integer value
together with its canonical type, which is a
<<Types_Primitive-Integer-Types,primitive integer type>>. Formally, the set of
primitive integer values
is the disjoint union over the integer types of the values
represented by each type:

* An unsigned integer type of width stem:[w] represents integers in the
range stem:[[0, 2^w-1\]]. For example, `U8` represents the integers
stem:[[0, 255\]].

* A signed integer type of width stem:[w] represents integers in the range
stem:[[-2^(w-1), 2^(w-1)-1\]]. For example, `I8` represents the integers
stem:[[-128, 127\]].

We represent a primitive integer value as an expression followed by a colon and
a primitive integer type.
For example, we write the value 1 at type `U32` as `1: U32`. The value `1:
U32` is distinct from the value `1: U8`.

=== Integer Values

An *integer value* is an ordinary (mathematical) integer value.
Its canonical type is _Integer_.
We represent an integer value as an integer number, with no explicit type.
For example, `1` is an integer value.

=== Floating-Point Values

A *floating-point value* is an IEEE floating-point value of 4- or 8-byte
width. Formally, the set of floating-point values is the disjoint union
over the types `F32` and `F64` of the values represented by each type:

* The type `F32` represents all IEEE 4-byte floating-point values.

* The type `F64` represents all IEEE 8-byte floating-point values.

We write a floating-point values analogously to primitive integer values. For
example, we write the value 1.0 at type `F32` as `1.0: F32`.
The canonical type of a floating-point value is `F32` or `F64`.

=== Boolean Values

A *Boolean value* is one of the values `true` and `false`.
Its canonical type is `bool`.

=== String Values

A *string value* is a sequence of characters that can be
represented as a <<Expressions_String-Literals,string literal expression>>.
It is written in the same way as a string literal expression,
e.g., `"abc"`.
Every string value _v_ has a *length*, which is the number of
characters in the sequence.

A string value _v_ belongs to every string type.
Note that _v_ may have length _m_ and type `string size` _n_,
with stem:[m > n].
In this case, the behavior is defined by the code generation strategy.
In particular, when code is generated for the F Prime framework,
the value _v_ may be stored into a buffer that
can hold a maximum string length of _n_.
If this happens, the framework will *truncate* the value _v_
to _n_ characters before storing it.
That means that the first _n_ characters of _v_ are stored in the buffer.

=== Abstract Type Values

An *abstract type value* is a value associated with an abstract
type.
For each abstract type stem:[T], there is one
value with canonical type stem:[T].
This value is not represented explicitly in the model, but it
may be represented in the generated code, e.g., as an object
with default initialization.
We write the value `value of type` stem:[T].

=== Anonymous Array Values

An *anonymous array value* is a value associated with an anonymous
array type.
We write an anonymous array value similarly to an
<<Expressions_Array-Expressions,array expression>>:
an anonymous array value stem:[v] has the form `[` stem:[v_1] `,` stem:[...]
`,`
stem:[v_{n-1}] `]`, where

. stem:[n] is a positive integer called the *size* of the anonymous array
  value.

. For each stem:[i in [0,n-1]], stem:[v_i] is a value of type
stem:[T] for some <<Types_Canonical-Types,canonical type>> stem:[T].
The canonical type of stem:[v] is _[_ stem:[n] _]_ stem:[T].

Note that for an anonymous array value stem:[v] to be well-formed, the member
values must have identical types.
If an array expression appearing in the source syntax has
member values with non-identical types, then one or more members must be
converted to a different type before forming stem:[v].

=== Array Values

An *array value* is a value associated with an array type.
We write an array value like an <<Values_Anonymous-Array-Values,anonymous array
value>>, except that the value is annotated with an
<<Types_Array-Types,array type>>.

An array value has the form `[` stem:[v_0] `,` stem:[...] `,`
stem:[v_{n-1}] `]` `:` stem:[Q],
where

. stem:[n] is a positive integer called the *size* of the array value.

. stem:[Q] is a
<<Scoping-of-Names_Qualified-Identifiers,qualified identifier>>
that refers to a
<<Definitions_Array-Definitions,array definition>>
with member type stem:[T].

. For each stem:[i in [0,n-1]], stem:[v_i] is a value of type stem:[T].
Note that stem:[T] need not be a canonical type.
For example, it is permissible for stem:[T] to be `T`, for
`T` to be an alias of `U32`, and for stem:[v] to be the value `[ 0: U32, 1: U32 ]`.
In this case `0: U32` and `1: U32` are values of type `T`, as required.

The canonical type of the value is stem:[Q].

=== Enumeration Values

An *enumeration value* is a value associated with an
<<Definitions_Enumerated-Constant-Definitions,enumerated constant definition>>.
It is a pair consisting of the name and the integer value
specified in the enumerated constant definition.
Its canonical type is the type associated with the
<<Definitions_Enum-Definitions,enum definition>> in which
the enumerated constant definition appears.

=== Anonymous Struct Values

An *anonymous struct value* is a value associated with an
<<Types_Internal-Types_Anonymous-Struct-Types,anonymous struct
type>>.
We write an anonymous struct value stem:[v] similarly to a
<<Expressions_Struct-Expressions,struct expression>>:
a struct value has the form `{` stem:[m_1] `=` stem:[v_1] `,` stem:[...] `,`
stem:[m_n] `=` stem:[v_n] `}`,
where for each stem:[i in [1,n]], stem:[v_i] is a value of type stem:[T_i].
The elements stem:[m_i] `=` stem:[v_i] are called the
*members* of the value.

Each type stem:[T_i] must be a <<Types_Canonical-Types,canonical type>>.
The canonical type of the value is _{_ stem:[m_1] _:_ stem:[T_1] _,_ stem:[...]
_,_ stem:[m_n] _:_ stem:[T_n] _}_.

=== Struct Values

A *struct value* is a value associated with a
<<Types_Struct-Types,struct type>>.
We write a struct value similarly to an
<<Values_Struct-Values,anonymous struct value>>,
except that we annotate the value with a struct type:
a struct value has the form `{` stem:[m_1] `:` stem:[v_1] `,` stem:[...] `,`
stem:[m_n] `:` stem:[v_n] `}` `:` stem:[Q],
where

. stem:[Q] is a
<<Scoping-of-Names_Qualified-Identifiers,qualified identifier>>
that refers to a
<<Definitions_Struct-Definitions,struct definition>>.

. The members of stem:[Q] are stem:[m_i] `:` stem:[T_i] for stem:[i in [1,n\]].

. For each stem:[i in [1,n]], stem:[v_i] is a value of type stem:[T_i].
Note that stem:[T_i] need not be a canonical type.
For example, it is permissible for stem:[T_1] to be `T`, for
`T` to be an alias of `U32`, and for stem:[v_1] to be the value `1: U32`.
In this case `1: U32` is a value of type `T`, as required.

Each member of the struct value must have an explicit value.
The canonical type of the struct value is stem:[Q].

=== Serialized Sizes

Every value _v_ of a <<Types_Displayable-Types,displayable type>>
has a *serialized size*.  This is the number of bytes required to represent _v_ 
in
the standard F Prime serialized format.  The serialized size _s_ of a value _v_
depends on the type _T_ of _v_:

* If _T_ is a
<<Types_String-Types,string type>>, then _s_ is the sum of the following two numbers:

** The serialized size of the
   <<Definitions_Framework-Definitions_Type-Definitions,framework type>>
`FwSizeStoreType`.  This is the space used to store the length of the string.

** The length of the string in characters.

* Otherwise if _v_ is an <<Types_Array-Types,array type>>, then _s_ is the sum
  of the serialized sizes of the elements of _v_.

* Otherwise if _v_ is a <<Types_Struct-Types,struct type>>, then _s_ is the sum
  of the serialized sizes of the members of _v_

* Otherwise _s_ is the <<Types_Serialized-Sizes,serialized size of the type _T_>>.
