 40 Chapter 3 Expressions
representation for 2-bit, binary zero. If the reset value is not high, the case
expression speciﬁes the value of the
if expression. The value resulting from eval-
uating the
if expressions constrains the value of current’ representing the value
of current in the next state.
Assuming that x is a natural number, the type of the case statement previously
EXAMPLE 3.5
Type Inference for Case
Expressions
deﬁned is natural:
case x is
0,1,2 -> x+1 |
3->0|
top -> 0
end case :: natural
3.6 Let Expressions
The let expression deﬁnes local items and their scopes. The expression:
let pi::real be 3.1415 in
end let;
evaluates to the area of a circle. The value of pi is deﬁned to be the real value
3.1415 in the scope of the
let expression.
The syntax of a let expression is:
let v
0
:: T
0
be e
0
[[ ; v
n
:: T
n
be e
n
]]
in
e
end let;
The let keyword is followed by a declar ative section where one or more local
items may be deﬁned. The syntax of local item declarations is identical to the
syntax of a traditional item declaration except that the keyword
is is replaced by
the keyword
be for readability. Semantically, declarations are identical. Like tra-
ditional item declarations,
let declarations are deﬁned by specify ing a name and
type using the type membership operator. The
be clause is required and speciﬁes
a value for the local item. Within the scope of the
let expressions, these items
same type may be speciﬁed using a comma-separated collection of item names in
the declaration. Within e, any variable deﬁned in the
let declaration section is
visible. For example, given area::boolean:
let pi::real be 3.14159 in
if area then pir^2 else 2pir end if
end let; 3.6 Let Expressions 41
deﬁnes a let expression that either calculates the area or radius of a circle. The let
expression declares and deﬁnes a local value, pi, that is visible in the if expression
used to calculate the indicated value.
Like all Rosetta expressions, the
let expression simpliﬁes to a value and has a
type. In the previous example, the
let expression’s value is the if expression in
the context of local variables. The
let expression’s type is the type of its encapsu-
lated expression with the types of local variables added to the expression’s context.
Let expressions may be nested in the traditional fashion. In the following spec-
iﬁcation, the variable x of type T
1
has the associated expression v
1
, while y of type
T
2
has the expression v
2
. Both may be referenced in the expression e:
let x::T
1
be v
1
in
let y::T
2
be v
2
in
e
end let
end let;
This expression may also be wr itten as:
let x::T
1
be v
1
; y::T
2
be v
2
in e end let;
Semantically, the let expression is actually a letrec expression. Languages such as
Scheme and Common Lisp provide separate let and letrec constructs. A traditional
let construct is not recursive. The deﬁned variable cannot be referenced in the
expression deﬁning its value. A letrec, traditionally deﬁned as a derived form of
let construct, is recursive and allows such references.
A key use for the
let expression is adding abst raction to deﬁnitions. Using the
EXAMPLE 3.6
Let Expressions and
Abstraction
let, new declarations speciﬁc to an expression deﬁne and name concepts. In the
following expression, a
let expression deﬁnes quantities for use in a deﬁnition:
let newx::real be x+dx; newy::real be y+dy in
update_position(newx,newy)
end let
Here the local variables newx and newy provide names for new values of an x
and y position, respectively. Although this is a trivial use of the
let expression, it
demonstrates an abstraction capability that will prove more useful when recursive
let applications and the ﬁxed point operator, fix, are introduced.
Thetypeofa
let expression is the same as the ty pe of its encapsulated
expression. If the expression is well-typed, so is the associated
let expression.
For the previously deﬁned
let expression, the encapsulated expression is real,
thus the
let expression is real:
let (pi::real be 3.14159) in
if area then pir^2 else 2pir end if
end let:: real

Get System Level Design with Rosetta now with O’Reilly online learning.

O’Reilly members experience live online training, plus books, videos, and digital content from 200+ publishers.