|
| |||||
| 9.7 Value expressions | ||||||
The RSL value literals are accepted.
A value name translates as a name.
Not accepted.
The only basic expression in RSLSML is skip.
A product expression translates to an SML product expression.
Enumerated and ranged set expressions are accepted.
A comprehended set expression can only be translated if it takes one of the forms
| { e | b : T • b ∈ slm } | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| or | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| { e | b : T • b ∈ slm ∧ p } | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
where b is a binding, T is a type, e is a translatable expression, slm is a translatable expression of set, list, or map type, and p is a translatable expression of type Bool.
Enumerated and ranged list expressions are accepted.
A comprehended list expression can only be translated if it takes one of the forms
| 〈 e | b in l 〉 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| or | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| 〈 e | b in l • p 〉 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
where b is a binding, e is a translatable expression, l is a translatable expression of list type, and p is a translatable expression of type Bool.
Enumerated map expressions are accepted.
A comprehended map expression can only be translated if it takes one of the forms
| [ e1 ↦ e2 | b :T • b ∈ slm ] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| or | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| [ e1 ↦ e2 | b :T • b ∈ slm ∧ p] | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
where b is a binding, e1 and e2 are translatable expressions, T is a type, slm is a translatable expression of set, list, or map type, and p is a translatable expression of type Bool.
Function expressions are accepted.
An application expression may be translated to a function call, a list application or a map application.
Quantified expressions can only be translated if they take one of the following forms:
| ∀ b : T • b ∈ slm | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ∀ b : T • b ∈ slm ⇒ p | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ∀ b : T • b ∈ slm ∧ p ⇒ q | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ∃ b : T • b ∈ slm | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ∃ b : T • b ∈ slm ∧ p | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ∃! b : T • b ∈ slm | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ∃! b : T • b ∈ slm ∧ p | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
where b is a binding, T is a type, slm is a translatable expression of set, list or map type, and p and q are translatable expressions of type Bool.
Not accepted.
Not accepted.
A disambiguation expression translates as its constituent value expression.
A bracketed expression translates to a bracketed expression.
An infix expression translates to the corresponding SML expression.
A prefix expression translates to the corresponding SML expression.
A universal prefix expression (□) is not accepted.
Not accepted.
An assignment expression translates to an assignment expression.
Not accepted.
Not accepted.
Local expressions are accepted.
Explicit let expressions are accepted, subject to the restrictions on patterns listed in section 9.7.25.
An implicit let expression can only be translated if it has one of the forms
| let b : T • b ∈ slm in ... end | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| or | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| let b : T • b ∈ slm ∧ p in ... end | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
where b is a binding, T a type, slm a translatable expression of set, list, or map type, and p a translatable expression of type Bool.
An if expression translates to an if expression.
Case expressions are accepted subject to some restrictions on possible patterns when the case is over a variant or record type and involves a function constructor:
The function must be the constructor of a record or variant.
Int, Real and Text literal patterns are not accepted.
Equality patterns are not accepted.
While expressions are accepted.
Until expressions are accepted.
For expressions are accepted.
| 9.7 Value expressions | ||||||
|
| |||||