bluespec-docs/content/chapter4/page7.md
2025-02-12 15:54:12 -05:00

3.2 KiB
Raw Permalink Blame History

+++ title = "Value definitions" weight = 1 +++

A value definition defines the value of an identifier (which could be a function). Value definitions are the meat of a BH program.

Value definitions consist of a type signature followed immediately by one or more defining clauses:

topDefn   ::= valueDefn
valueDefn ::= varId :: ctxType ;
              {clause ; }
clause    ::= varId
              {apat }[ when guard ]= exp

The first line of a value definition is the type signature--- it simply specifies that the identifier varId has the type ctxType. Subsequent lines define the value, one clause at a time. The varId's on the left-hand side of the type signature and on the left-hand side of each clause must all be the same, i.e., they collectively define a single varId.

Each clause defines part of the value, using pattern matching and guards. If there are patterns (apat's) present, then the varId being defined is a function, and the patterns represent arguments to the function. The guard is a list of arbitrary predicates that may use identifiers bound in the patterns (see Section 7).

The clause should be read as follows: if the function varId is applied to arguments that match the corresponding apat's (in which case, identifiers in the apat's are bound to the corresponding components of the arguments), and if the predicates in the guard are true, then the function returns the value of the expression exp.

Example:

wordSize :: Integer
wordSize = 16

This simply defines the identifier wordSize to have type Integer and value 16.

Example:

not :: Bool -> Bool
not True = False
not False = True

This defines the classical Boolean negation function. The type signature specifies that not is a function with argument type Bool and result type Bool. After that, the first clause specifies that if the argument matches the value True (i.e., it is the value True), then it returns False. The final clause specifies that if the argument is False it returns True.

Example:

f :: Maybe Int -> Int -> Int
f (Just x) y when x > 10, Just y <- g y = x + y'
f _        _                             = 0

(If necessary, please first remember the definition of the Maybe type, introduced in section 4.1). The first line specifies that f is a function of two arguments, of type Maybe Int and Int, respectively, and that its result has type Int. The second line specifies that if the first argument has the form Just x (in which case let us call its component x), if the second argument is anything (let us call it y), if x's value is greater than 10, if the result of applying g to y has the form Just y (in which case let us call the component y), then the result is the value of x + y. In all other cases, the result is the value 0. The bare underscores in the second line are wild-card patterns that match anything (described in section 6.1).

Clauses are attempted in order, from top to bottom, proceeding to the next clause only if the pattern matching and guard evaluation fail. Within each clause, pattern matching and guard evaluation are attempted from left to right. If no clause succeeds, then the system will raise a "pattern matching error".