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

pi∗radius∗radius

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

behave as traditional items. Like traditional declarations, multiple items of the

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 pi∗r^2 else 2∗pi∗r 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

the traditional

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 pi∗r^2 else 2∗pi∗r 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.