|
|
|---|
|
|
|
|---|
Value expressions and their evaluation.
In some contexts, we need to denote values via expressions that can be readily evaluated without the need for a dynamic environment. Thus, we introduce a notion of value expressions, as the expressions that can be evaluated in that way. These include literals (to denote primitive values), arithmetic negation applied to signed literals (to denote negative signed values), tuple expressions whose components are value expressions, and struct expressions whose components are value expressions.
The representation of values by value expressions is not unique. For example, the same field value may be denoted by infinite literals whose numerals differ by the prime.
Along with expression values, we also define their evaluation to values. We also define an inverse, namely a mapping from values to expression values that evaluate to the values. We pick a ``minimal'' such mapping: with reference to the non-uniqueness example above, we pick the smallest numeral for a field literal.