first commit
This commit is contained in:
commit
13c1ed7b2a
35 changed files with 3330 additions and 0 deletions
3
content/_index.md
Normal file
3
content/_index.md
Normal file
|
@ -0,0 +1,3 @@
|
|||
+++
|
||||
redirect_to = "chapter1"
|
||||
+++
|
152
content/chapter1/_index.md
Normal file
152
content/chapter1/_index.md
Normal file
|
@ -0,0 +1,152 @@
|
|||
+++
|
||||
title = "Introduction"
|
||||
weight = 1
|
||||
sort_by = "weight"
|
||||
insert_anchor_links = "right"
|
||||
+++
|
||||
|
||||
BH (Bluespec Haskell/Classic) is a language for hardware design. The
|
||||
language borrows its notation, type and package system from an existing
|
||||
general-purpose functional programming language called Haskell
|
||||
[@haskell12] where those constructs have been well tested for over a
|
||||
decade. Unlike Haskell, BH is meant solely for hardware design--- a BH
|
||||
program represents a circuit. The abstract model for these circuits is a
|
||||
Term Rewriting System (TRS); details about using TRSs for describing
|
||||
circuits, and compiling these descriptions to real hardware, may be
|
||||
found in James Hoe's thesis [@jhoe]. BH has several restrictions and
|
||||
extensions relative to Haskell, arising out of this hardware focus.
|
||||
|
||||
|
||||
This document is not meant as a tutorial on BH (separate documents exist
|
||||
for that purpose). Nevertheless, this document has numerous small
|
||||
examples to explicate BH notation.
|
||||
|
||||
|
||||
## Meta notation
|
||||
|
||||
|
||||
The grammar rules in the presentation below mostly follow the usual EBNF
|
||||
(Extended BNF) structure. Grammar alternatives are separated by
|
||||
"$\mid$". Items enclosed in \[ \] are optional. Items enclosed in { }
|
||||
can be repeated zero or more times. The last piece of notation is used
|
||||
sloppily; sometimes there must be at least one item, and also, the last
|
||||
terminal inside the { } is sometimes a separator rather than terminator.
|
||||
|
||||
|
||||
## Identifiers and the rôle of upper and lower case
|
||||
|
||||
|
||||
An identifier in BH consists of a letter followed by zero or more
|
||||
letters, digits, underscores and single quotes. Identifiers are case
|
||||
sensitive: `glurph`, `gluRph` and `Glurph` are three distinct
|
||||
identifiers.
|
||||
|
||||
|
||||
The case of the first letter in an identifier is very important. If the
|
||||
first letter is lower case, the identifier is a "variable identifier",
|
||||
referred to in the grammar rules as a *varId*. If the first letter is
|
||||
upper case, the identifier is a "constructor identifier", referred to in
|
||||
the grammar rules as a *conId*.
|
||||
|
||||
|
||||
In BH, package names (*packageId*), type names (*tycon*) and value
|
||||
constructor names are all constructor identifiers. (Ordinary) variables,
|
||||
field names and type variables are all variable identifiers.
|
||||
|
||||
|
||||
A lone underscore, "` `", is treated as a special identifier--- it is
|
||||
used as a "don't care" pattern or expression (more details in Sections
|
||||
[5.10](fixme) and
|
||||
[6.1](fixme)).
|
||||
|
||||
|
||||
## The Standard Prelude
|
||||
|
||||
|
||||
The Standard Prelude is a predefined package that is imported implicitly
|
||||
into every BH package. It contains a number of useful predefined
|
||||
entities (types, values/functions, classes, instances, etc.). It is
|
||||
somewhat analogous to the combination of various ".h" files and standard
|
||||
libraries in C, except that in BH no special action is needed to import
|
||||
the prelude or to link it in. We will refer to the prelude periodically
|
||||
in the following sections, and there are more details in appendix
|
||||
[15](fixme).
|
||||
|
||||
|
||||
## Lexical syntax/layout
|
||||
|
||||
|
||||
In BH, there are various syntactic constructs that involve zero or more
|
||||
items enclosed in braces and separated by semicolons: These braces and semicolons can be omitted
|
||||
entirely if the components are laid out with proper indentation.
|
||||
|
||||
|
||||
Suppose the parser discovers a missing open brace (e.g., after the
|
||||
keywords `where`, `let`, `do` and `of`). Then, the indentation of the
|
||||
next lexical element is remembered (and the missing open brace is
|
||||
implicitly inserted before it). For each subsequent line, if it contains
|
||||
only whitespace or is indented more, then it is treated as a
|
||||
continuation of the current item. If it is indented the same amount, it
|
||||
is treated as the beginning of the next item (*i.e.,* a semicolon is
|
||||
inserted implicitly before the item). If it is indented less, then the
|
||||
list of items is considered to be complete (*i.e.,* a closing brace is
|
||||
implicitly inserted). An explicit brace is never matched against an
|
||||
implicit one. Thus, while using the layout rule, if the parser
|
||||
encounters an explicit open brace, then it does not resume using the
|
||||
layout rule for this list of items until it has "emerged" past the
|
||||
explicit corresponding closing brace (a construct nested inside this
|
||||
list of items may still use the layout rule).
|
||||
|
||||
|
||||
## Comments in BH programs
|
||||
|
||||
|
||||
In a BH program, a *comment* is legal as whitespace, and may be
|
||||
introduced in two ways. An *ordinary comment* is introduced by a lexical
|
||||
token consisting of two or more consecutive dashes followed by a
|
||||
non-symbol, and extends up to and including the end of the line. (See
|
||||
Section
|
||||
[\[sec-infix-applications\]](fixme) for the list of symbols.) Note: the
|
||||
lexical token `—>` is a legal token in BH, and since it contains three
|
||||
consecutive dashes followed by a symbol, it does not begin a comment.
|
||||
|
||||
|
||||
A *nested comment* is introduced by the lexeme "`{-`" and extends until
|
||||
the next matching "`-}`", possibly spanning multiple lines. A nested
|
||||
comment can itself contain another nested comment; this nesting can be
|
||||
repeated to any depth.
|
||||
|
||||
|
||||
In an ordinary comment, the character sequences "`{-`" and "`-}`" have
|
||||
no special significance, and, in a nested comment, a sequence of dashes
|
||||
has no special significance.
|
||||
|
||||
|
||||
## General organization of this document
|
||||
|
||||
|
||||
A concept that is pervasive in BH is the notion of a *type*. Every value
|
||||
expression in BH, even a basic value identifier, has a type, and the
|
||||
compiler does extensive static type checking to rule out absurd use of
|
||||
values (such as taking the square root of an IP address). Types are
|
||||
discussed in section [2](fixme).
|
||||
|
||||
|
||||
A BH program consists of one or more packages. These outermost
|
||||
constructs are described in section
|
||||
[3](fixme). As
|
||||
explained later, a BH package is a linguistic namespace-management
|
||||
mechanism and does not have any direct correlation with any hardware
|
||||
module being described by the program. Hardware modules correspond to
|
||||
*modules*, a particular type of value in BH.
|
||||
|
||||
|
||||
Within each package is a collection of top-level definitions. These are
|
||||
described in section [4](fixme).
|
||||
|
||||
|
||||
Amongst the top-level definitions are *value definitions* (section
|
||||
[4.7](fixme)),
|
||||
which constitute the actual meat of the code. Value definitions are
|
||||
built around *expressions*, which are described in section
|
||||
[5](fixme).
|
103
content/chapter2/_index.md
Normal file
103
content/chapter2/_index.md
Normal file
|
@ -0,0 +1,103 @@
|
|||
+++
|
||||
title = "Types"
|
||||
weight = 2
|
||||
sort_by = "weight"
|
||||
insert_anchor_links = "right"
|
||||
+++
|
||||
|
||||
Every value expression and, in particular, every value identifier in BH
|
||||
has a *type*. In some cases the programmer must supply a *type
|
||||
signature* specifying this and in many cases the compiler infers it
|
||||
automatically. The BH programmer should be aware of types at all times.
|
||||
|
||||
```
|
||||
type ::= btype [ "->" type ]
|
||||
btype ::= [ btype ] atype
|
||||
atype ::= tycon | tyvar | ( { type , } )
|
||||
tycon ::= conId
|
||||
```
|
||||
|
||||
|
||||
Most type expressions have the form: *TypeConstructor* $t_1$ $\cdots$
|
||||
$t_n$ where $t_1$ $\cdots$ $t_n$ are themselves type expressions, and $n
|
||||
{\geq} 0$. The $t_1$ $\cdots$ $t_n$ are referred to as the *type
|
||||
arguments* to the type constructor. $n$ is also called the *arity* of
|
||||
the type constructor.
|
||||
|
||||
|
||||
Familiar basic types have zero-arity type constructors (no type
|
||||
arguments, $n = 0$). Examples:
|
||||
|
||||
- `Integer`
|
||||
- `Bool`
|
||||
- `String`
|
||||
- `Action`
|
||||
|
||||
Other type constructors have arity $n > 0$; these are also known as
|
||||
*parameterized types*.
|
||||
|
||||
Examples:
|
||||
|
||||
- `List Bool`
|
||||
- `List (List Bool)`
|
||||
- `Array Integer String`
|
||||
- `Maybe Integer`
|
||||
|
||||
These represent the types of lists of
|
||||
Booleans, lists of lists of Booleans, arrays indexed by integers and
|
||||
containing strings, and an optional result possibly containing an
|
||||
integer.
|
||||
|
||||
|
||||
A type can be *polymorphic*, indicated using type variables. Examples:
|
||||
|
||||
- `List a`
|
||||
- `List (Llist b)`
|
||||
- `Array i (List String)`
|
||||
|
||||
|
||||
These represent lists of things of some unknown type "`a`", lists of
|
||||
lists of things of some unknown type "`b`", and arrays indexed by some
|
||||
unknown type "`i`" and containing lists of strings.
|
||||
|
||||
|
||||
One type constructor is given special status in the syntax. The type of
|
||||
functions from arguments of type $t_1$ to results of type $t_2$ could
|
||||
have been written as:
|
||||
|
||||
Function $t_1$ $t_2$
|
||||
|
||||
but in BH we write the constructor as an infix arrow:
|
||||
|
||||
$t_1$ -\> $t_2$
|
||||
|
||||
These associate to the right, *i.e.,*
|
||||
|
||||
$t_1$ -\> $\cdots$ -\> $t_{n-1}$ -\> $t_n$ $\equiv$ $t_1$
|
||||
-\> ($\cdots$ -\> ($t_{n-1}$ -\> $t_n$))
|
||||
|
||||
|
||||
There is one particular set of niladic type constructors that look like
|
||||
numbers. These are used to represent certain "sizes". For example, the
|
||||
type:
|
||||
|
||||
`Bit 16`
|
||||
|
||||
consists of the unary type constructor `Bit` applied to type represented
|
||||
by the niladic type constructor "`16`". The type as a whole represents
|
||||
bit vectors of length 16 bits. Similarly the type
|
||||
|
||||
`UInt 32`
|
||||
|
||||
|
||||
represents the type of unsigned integers that can be represented in 32
|
||||
bits. These numeric types are said to have kind `#`, rather than kind
|
||||
`*` for value types.
|
||||
|
||||
|
||||
Strings can also be used as type, having kind `$`. This is less common,
|
||||
but string types are quite useful in the generics library, described in
|
||||
the *Libraries Reference Guide*. Examples:
|
||||
|
||||
- `MetaData#("Prelude","Maybe",PrimUnit,2)`
|
||||
- `MetaConsNamed#("Valid",1,1)`
|
108
content/chapter2/page1.md
Normal file
108
content/chapter2/page1.md
Normal file
|
@ -0,0 +1,108 @@
|
|||
+++
|
||||
title = "Type classes and overloading"
|
||||
weight = 1
|
||||
+++
|
||||
|
||||
BH's `class` and `instance` mechanisms form a systematic way to do
|
||||
*overloading* (the approach has been well tested in Haskell).
|
||||
|
||||
|
||||
Overloading is a way to use a common name to refer to a set of
|
||||
operations at different types. For example, we may want to use the "`<`"
|
||||
operator name for the integer comparison operation, the floating-point
|
||||
comparison operation, the vector comparison operation and the matrix
|
||||
comparison operation. Note that this is not the same as polymorphism: a
|
||||
polymorphic function is a *single* function that is meaningful at an
|
||||
infinity of types (*i.e.,* at every possible instantiation of the type
|
||||
variables in its type). An overloaded identifier, on the other hand,
|
||||
usually uses a common name to refer to a (usually) small set of distinct
|
||||
operations.
|
||||
|
||||
|
||||
Further, it may make sense to have "`<=`", "`>`" and "`>=`" operations
|
||||
wherever there is a "`<`" operation, on integers, floating points
|
||||
numbers, vectors and matrices. Rather than handle these separately, we
|
||||
say:
|
||||
|
||||
|
||||
- there is class of types which we will call `Ord` (for "ordered types"),
|
||||
- that the integer, floating point, vector and matrix types are members
|
||||
(or "instances") of this class, and
|
||||
- that all types that are members of this class have appropriate
|
||||
definitions for the "`<`", "`<=`", "`>`" and "`>=`" operations. We also
|
||||
say that these operations are *overloaded* across these instance types,
|
||||
and we refer to these operations as the *methods* of this class.
|
||||
|
||||
|
||||
Another example: we could use a class `Hashable` with an operation
|
||||
called `hash` to represent those types $T$ for which we can and do
|
||||
define a hashing function. Each such type $T$ has to specify how to
|
||||
compute the `hash` function at that type.
|
||||
|
||||
|
||||
Classes, and the membership of a type in a class, do not come into
|
||||
existence by magic. Every class is created explicitly using a class
|
||||
declaration, described in section
|
||||
[4.5](fixme).
|
||||
A type must explicitly be made an instance of a class and the
|
||||
corresponding class methods have to be provided explicitly; this is
|
||||
described in [4.6](fixme).
|
||||
|
||||
|
||||
### Context-qualified types
|
||||
|
||||
|
||||
Consider the following type declaration:
|
||||
|
||||
```hs
|
||||
sort :: (Ord a) => List a -> List a
|
||||
```
|
||||
|
||||
|
||||
It expresses the idea that a sorting function takes an (unsorted) input
|
||||
list of items and produces a (sorted) output list of items, but it is
|
||||
only meaningful for those types of items ("`a`") for which the ordering
|
||||
functions (such as "`<`") are defined. Thus, it is ok to apply `sort` to
|
||||
lists of `Integer`'s or lists of `Bool`'s, because those types are
|
||||
instances of `Ord`, but it is not ok to apply `sort` to a list of, say,
|
||||
`Counter`'s (assuming `Counter` is not an instance of the `Ord` class).
|
||||
|
||||
|
||||
In the type of `sort` above, the part before "`=>`" is called a
|
||||
*context*. A context expresses constraints on one or more type
|
||||
variables--- in the above example, the constraint is that any actual
|
||||
type "`a`" must be an instance of the `Ord` class.
|
||||
|
||||
|
||||
A context-qualified type has the following grammar:
|
||||
|
||||
```
|
||||
ctxType ::= [ context => ] type
|
||||
context ::= ( {classId { varId }, })
|
||||
classId ::= conId
|
||||
```
|
||||
|
||||
In the above example, the class `Ord` had only one type parameter
|
||||
(*i.e.,* it constrains a single type) but, in general, a type class can
|
||||
have multiple type parameters. For example, in BH we frequently use the
|
||||
class "`Bits a n`" which constrains the type represented by `a` to be
|
||||
representable in bit strings of length represented by the type `n`.
|
||||
|
||||
|
||||
> **NOTE:**
|
||||
>
|
||||
> When using an overloaded identifier `x` there is always a question of
|
||||
> whether or not there is enough type information available to the
|
||||
> compiler to determine which of the overloaded `x`'s you mean. For
|
||||
> example, if `read` is an overloaded function that takes strings to
|
||||
> integers or Booleans, and `show` is an overloaded function that takes
|
||||
> integers or Booleans to strings, then the expression `show (read s)` is
|
||||
> ambiguous--- is the thing to be read an integer or a Boolean?
|
||||
>
|
||||
> In such ambiguous situations, the compiler will so notify you, and you
|
||||
> may need to give it a little help by inserting an explicit type
|
||||
> signature, e.g.,
|
||||
>
|
||||
> ```hs
|
||||
> show ((read s) :: Bool)
|
||||
> ```
|
82
content/chapter3/_index.md
Normal file
82
content/chapter3/_index.md
Normal file
|
@ -0,0 +1,82 @@
|
|||
+++
|
||||
title = "Packages"
|
||||
weight = 3
|
||||
sort_by = "weight"
|
||||
insert_anchor_links = "right"
|
||||
+++
|
||||
|
||||
Packages are the outermost constructs in BH--- all BH code must be
|
||||
inside packages. There should be one package per file. A BH package is a
|
||||
linguistic device for namespace control, and is particularly useful for
|
||||
programming-in-the-large. A package does not directly correspond to
|
||||
hardware modules. (Hardware modules correspond to BH modules, described
|
||||
in section [5.13](fixme))
|
||||
|
||||
|
||||
A BH package consists of the package header, import declarations, and
|
||||
top level definitions. The package header indicates which names defined
|
||||
in this package are exported, *i.e.,* available for import into other
|
||||
packages.
|
||||
|
||||
```
|
||||
packageDefn ::= package packageId ( exportDecl ) where {
|
||||
{ importDecl ; }
|
||||
{ fixityDecl ; }
|
||||
{ topDefn ; }
|
||||
}
|
||||
exportDecl ::= varId |typeId [ conList ]
|
||||
conList ::= (..)
|
||||
importDecl ::= import [ qualified ] packageId
|
||||
fixityDecl ::= fixity integer varId
|
||||
fixity ::= infix |infixl |infixr
|
||||
packageId ::= conId
|
||||
```
|
||||
|
||||
Example:
|
||||
|
||||
```hs
|
||||
package Foo (x, y) where
|
||||
import Bar
|
||||
import Glurph
|
||||
|
||||
-- top level definition ...
|
||||
-- top level definition ...
|
||||
-- top level definition ...
|
||||
```
|
||||
|
||||
Here, `Foo` is the name of this package, `x` and `y`
|
||||
are names exported from this package (they will be defined amongst the
|
||||
top level definitions in this package), and `Bar` and `Glurph` are the
|
||||
names of package being imported (for use in this package).
|
||||
|
||||
|
||||
The export list is a list of identifiers, each optionally followed by
|
||||
`(..)`. Each identifier in the list will be visible outside the package.
|
||||
If the exported identifier is the name of `data`, `struct`, or
|
||||
`interface`, then the constructors or fields of the type will be visible
|
||||
only if `(..)` is used. Otherwise, if you export only the name of a type
|
||||
without the `(..)` suffix, the type is an abstract (opaque) data type
|
||||
outside the package. The list of identifiers may include identifiers
|
||||
defined in the package as well as identifiers imported from other
|
||||
packages.
|
||||
|
||||
|
||||
If the keyword `qualified` is present in the import declaration all the
|
||||
imported entities from that package must be referred to by a qualified
|
||||
name.
|
||||
|
||||
|
||||
The fixity declaration can be used to give a precedence level to a
|
||||
user-defined infix operator. The `infixl` specifies a left associative
|
||||
operator, `infixr` a right associative operator, and `infix` a
|
||||
non-associative operator.
|
||||
|
||||
|
||||
## Name clashes and qualified names
|
||||
|
||||
|
||||
When used in any scope, a name must have an unambiguous meaning. If
|
||||
there is name clash for a name $x$ because it is defined in the current
|
||||
package and/or it is available from one or more imported packages, then
|
||||
the ambiguity can be resolved by using a qualified name of the form
|
||||
$M.x$ to refer to the version of $x$ contained in package $M$.
|
12
content/chapter4/_index.md
Normal file
12
content/chapter4/_index.md
Normal file
|
@ -0,0 +1,12 @@
|
|||
+++
|
||||
title = "Top Level Definitions"
|
||||
weight = 4
|
||||
sort_by = "weight"
|
||||
insert_anchor_links = "right"
|
||||
+++
|
||||
|
||||
# Top level definitions
|
||||
|
||||
|
||||
Top level definitions can be used only on the top level within a
|
||||
package.
|
146
content/chapter4/page1.md
Normal file
146
content/chapter4/page1.md
Normal file
|
@ -0,0 +1,146 @@
|
|||
+++
|
||||
title = "`data`"
|
||||
weight = 1
|
||||
+++
|
||||
|
||||
A `data` definition defines a brand new type, which is different from
|
||||
every primitive type and every other type defined using a `data`
|
||||
definition, even if they look structurally similar. The new type defined
|
||||
by a `data` definition is a "sum of products", or a "union of products".
|
||||
|
||||
```
|
||||
topDefn ::= data typeId {tyVarId } = {summand | }[ derive ]
|
||||
summand ::= conId {type }
|
||||
summand ::= conId { { fieldDef ; }}
|
||||
derive ::= deriving ( { classId , })
|
||||
fieldDef ::= fieldId :: type
|
||||
```
|
||||
|
||||
The *typeId* is the name of this new type. If the *tyVarId*'s exist,
|
||||
they are type parameters, thereby making this new type polymorphic. In
|
||||
each *summand*, the *conId* is called a "constructor". You can think of
|
||||
them as unique *tag*'s that identify each summand. Each *conId* is
|
||||
followed by a specification for the fields involved in that summand
|
||||
(*i.e.,* the fields are the "product" within the summand). In the first
|
||||
way of specifying a summand, the fields are just identified by position,
|
||||
hence we only specify the types of the fields. In the second way of
|
||||
specifying a summand, the fields are named, hence we specify the field
|
||||
names (*fieldId*'s) and their types.
|
||||
|
||||
|
||||
The same constructor name may occur in more than one type. The same
|
||||
field name can occur in more than one type. The same field name can
|
||||
occur in more than one summand within the same type, but the type of the
|
||||
field must be the same in each summand.
|
||||
|
||||
|
||||
The optional *derive* clause is used as a shorthand to make this new
|
||||
type an instance of the *classId*'s, instead of using a separate,
|
||||
full-blown `instance` declaration. This can only be done for certain
|
||||
predefined *classId*'s: `Bits`, `Eq`, and `Bounded`. The compiler
|
||||
automatically derives the operations corresponding to those classes
|
||||
(such as `pack` and `unpack` for the `Bits` class). Type classes,
|
||||
instances, and `deriving` are described in more detail in sections
|
||||
[2.1](fixme), [4.5](fixme) and [
|
||||
4.6](fixme).
|
||||
|
||||
To construct a value corresponding to some `data` definition $T$, one
|
||||
simply applies the constructor to the appropriate number of arguments
|
||||
(see section [5.3](fixme){reference-type="ref"
|
||||
reference="sec-exprs-constrs"}); the values of those arguments become
|
||||
the components/fields of the data structure.
|
||||
|
||||
|
||||
To extract a component/field from such a value, one uses pattern
|
||||
matching (see section [6](fixme){reference-type="ref"
|
||||
reference="sec-patterns"}).
|
||||
|
||||
|
||||
Example:
|
||||
|
||||
```hs
|
||||
data Bool = False | True
|
||||
```
|
||||
|
||||
|
||||
This is a "trivial" case of a `data` definition. The type is not
|
||||
polymorphic (no type parameters); there are two summands with
|
||||
constructors `False` and `True`, and neither constructor has any fields.
|
||||
It is a 2-way sum of empty products. A value of type `Bool` is either
|
||||
the value `False` or the value `True` Definitions like these correspond
|
||||
to an "enum" definition in C.
|
||||
|
||||
|
||||
Example:
|
||||
|
||||
```hs
|
||||
data Operand = Register (Bit 5)
|
||||
| Literal (Bit 22)
|
||||
| Indexed (Bit 5) (Bit 5)
|
||||
```
|
||||
|
||||
|
||||
Here, the first two summands have one field each; the third has two
|
||||
fields. The fields are positional (no field names). The field of a
|
||||
`Register` value must have type Bit 5. A value of type `Operand` is
|
||||
either a `Register` containing a 5-bit value, or a `Literal` containing
|
||||
a 22-bit value, or an `Indexed` containing two 5-bit values.
|
||||
|
||||
|
||||
Example:
|
||||
|
||||
```hs
|
||||
data Maybe a = Nothing | Just a
|
||||
deriving (Eq, Bits)
|
||||
```
|
||||
|
||||
This is a very useful and commonly used type. Consider a function that,
|
||||
given a key, looks up a table and returns some value associated with
|
||||
that key. Such a function can return either `Nothing`, if the table does
|
||||
not contain an entry for the given key, of `Just `$v$, if the table
|
||||
contains $v$ associated with the key. The type is polymorphic (type
|
||||
parameter "`a`") because it may be used with lookup functions for
|
||||
integer tables, string tables, IP address tables, etc., *i.e.,* we do
|
||||
not want here to over-specify the type of the value $v$ at which it may
|
||||
be used.
|
||||
|
||||
|
||||
Example:
|
||||
|
||||
```hs
|
||||
data Instruction = Immediate { op::Op; rs::Reg; rt::CPUReg; imm::UInt16; }
|
||||
| Jump { op::Op; target::UInt26; }
|
||||
```
|
||||
|
||||
|
||||
An `Instruction` is either an `Immediate` or a `Jump`. In the former
|
||||
case, it contains a field called `op` containing a value of type `Op`, a
|
||||
field called `rs` containing a value of type `Reg`, a field called `rt`
|
||||
containing a value of type `CPUReg`, and a field called `imm` containing
|
||||
a value of type `UInt16`. In the latter case, it contains a field called
|
||||
`op` containing a value of type `Op`, and a field called `target`
|
||||
containing a value of type `UInt26`.
|
||||
|
||||
> **NOTE:**
|
||||
>
|
||||
> Error messages involving data type definitions sometimes show traces of
|
||||
> how they are handled internally. Data type definitions are translated
|
||||
> into a data type where each constructor has exactly one argument. The
|
||||
> types above translate to:
|
||||
>
|
||||
> ```hs
|
||||
> data Bool = False PrimUnit | True PrimUnit
|
||||
>
|
||||
> data Operand = Register (Bit 5)
|
||||
> | Literal (Bit 22)
|
||||
> | Indexed Operand_$Indexed
|
||||
> struct Operand_$Indexed = { _1 :: Reg 5; _2 :: Reg 5 }
|
||||
>
|
||||
> data Maybe a = Nothing PrimUnit | Just a
|
||||
>
|
||||
> data Instruction = Immediate Instruction_$Immediate
|
||||
> | Register Instruction_$Register
|
||||
>
|
||||
> struct Instruction_$Immediate = { op::Op; rs::Reg; rt::CPUReg; imm::UInt16; }
|
||||
> struct Instruction_$Register = { op::Op; target::UInt26; }
|
||||
> ```
|
68
content/chapter4/page2.md
Normal file
68
content/chapter4/page2.md
Normal file
|
@ -0,0 +1,68 @@
|
|||
+++
|
||||
title = "`struct`"
|
||||
weight = 1
|
||||
+++
|
||||
|
||||
Defines a record type (a "pure product"). This is a specialized form of
|
||||
a `data` definition. The same field name may occur in more than one
|
||||
type.
|
||||
|
||||
```
|
||||
topDefn ::= struct typeId {tyVarId }= { { fieldDef ; }} [ derive ]
|
||||
fieldDef ::= fieldId :: type
|
||||
```
|
||||
|
||||
Example:
|
||||
|
||||
```
|
||||
struct Proc = { pc :: Addr; rf :: RegFile; mem :: Memory }
|
||||
struct Coord = { x :: Int; y :: Int }
|
||||
```
|
||||
|
||||
|
||||
Section [5.6](fixme) describes how to construct values of a
|
||||
`struct` type. A field of a `struct` type can be extracted either
|
||||
directly using "dot" notation (section
|
||||
[5.7](fixme)) or using pattern matching (section
|
||||
[6.3](fixme)).
|
||||
|
||||
|
||||
### Tuples {#sec-tuple-type}
|
||||
|
||||
|
||||
One way to group multiple values together is to use a `data` definition
|
||||
in which a constructor has multiple fields.
|
||||
|
||||
|
||||
However, there is a built-in notation for a common form of grouping,
|
||||
called "tuples". To group two (or more) values together the Prelude
|
||||
contains a type, `PrimPair`, for which there is syntactic sugar for type
|
||||
expressions, value expressions, and patterns.
|
||||
|
||||
The type has the following definition
|
||||
|
||||
```hs
|
||||
struct PrimPair a b = { fst :: a; snd :: b } deriving (Eq, Bits, Bounded)
|
||||
```
|
||||
|
||||
For type expressions the following shorthand can be used:
|
||||
|
||||
(a, b) $\equiv$ PrimPair a b
|
||||
|
||||
Or, more generally,
|
||||
|
||||
($t_1$, $t_2$, $\cdots$, $t_n$) $\equiv$ PrimPair $t_1$ (PrimPair $t_2$ ($\cdots$ $t_n$))
|
||||
|
||||
|
||||
There is a corresponding shorthand for value expressions and patterns:
|
||||
|
||||
(a, b) $\equiv$ PrimPair { fst = a; snd = b }
|
||||
|
||||
There is also special syntax for the empty tuple. It is written "`()`"
|
||||
for types, expressions, and patterns. The real type has the following
|
||||
definition
|
||||
|
||||
```hs
|
||||
struct PrimUnit = { } deriving (Eq, Bits, Bounded)
|
||||
```
|
||||
|
38
content/chapter4/page3.md
Normal file
38
content/chapter4/page3.md
Normal file
|
@ -0,0 +1,38 @@
|
|||
+++
|
||||
title = "`type`"
|
||||
weight = 1
|
||||
+++
|
||||
|
||||
Defines a type synonym. These are used purely for readability, *i.e.,* a
|
||||
type synonym can always be "expanded out" to its definition at any time.
|
||||
|
||||
```
|
||||
topDefn ::= type typeId {tyVarId }= type
|
||||
```
|
||||
|
||||
Examples:
|
||||
|
||||
```hs
|
||||
type Byte = Bit 8
|
||||
type Word = Bit 16
|
||||
type LongWord = Bit 32
|
||||
```
|
||||
|
||||
These provide commonly used names for certain bit lengths. In a
|
||||
specification of a processor:
|
||||
|
||||
```hs
|
||||
data RegName = R0 | R1 | ... | R31
|
||||
type Rdest = RegName
|
||||
type Rsrc = RegName
|
||||
data ArithInstr = Add Rdest Rsrc Rsrc
|
||||
| Sub Rdest Rsrc Rsrc
|
||||
```
|
||||
|
||||
the last two lines suggest the roles of the registers in the
|
||||
instructions, and is more readable than:
|
||||
|
||||
```hs
|
||||
data ArithInstr = Add RegName RegName RegName
|
||||
| Sub RegName RegName RegName
|
||||
```
|
43
content/chapter4/page4.md
Normal file
43
content/chapter4/page4.md
Normal file
|
@ -0,0 +1,43 @@
|
|||
+++
|
||||
title = "`interface`"
|
||||
weight = 1
|
||||
+++
|
||||
|
||||
Defines an interface for a hardware module (see section
|
||||
[5.13](fixme)). An
|
||||
interface is essentially a `struct`, but its components are restricted
|
||||
to those things that have a physical interpretation as wires in and out
|
||||
of a circuit. The types of fields in an interface are more likely to
|
||||
involve `Action`'s (see section
|
||||
[5.11](fixme)),
|
||||
which are typically interpreted as "enable signals" into a circuit. The
|
||||
fields of an interface are also known as *methods* (not to be confused
|
||||
with methods of a class, described in Sections
|
||||
[2.1](fixme) and
|
||||
[4.5](fixme)).
|
||||
|
||||
```
|
||||
topDefn ::= interface typeId {tyVarId }= { { fieldDef ; }}
|
||||
```
|
||||
|
||||
Example:
|
||||
|
||||
```hs
|
||||
interface Stack a =
|
||||
push :: a -> Action
|
||||
pop :: Action
|
||||
top :: Maybe a
|
||||
```
|
||||
|
||||
This describes a circuit that implements a stack (a LIFO) of items. This
|
||||
polymorphic definition does not specify the type of the contents of the
|
||||
stack, just that they have some type "`a`". Corresponding to the `push`
|
||||
method, the circuit will have input wires to carry a value of type
|
||||
"`a`", and a "push-enable" input wire that specifies when the value
|
||||
present on the input wires should be pushed on the stack. Corresponding
|
||||
to the `pop` component, the circuit will have a "pop-enable" input wire
|
||||
that specifies when a value should be popped off the stack.
|
||||
Corresponding to the `top` component, the circuit will have a set of
|
||||
output wires: if the stack is empty, the wires will represent the value
|
||||
`Nothing`, and if the stack is non-empty and $v$ is the value at the top
|
||||
of the stack, the wires will represent `Maybe` $v$.
|
86
content/chapter4/page5.md
Normal file
86
content/chapter4/page5.md
Normal file
|
@ -0,0 +1,86 @@
|
|||
+++
|
||||
title = "`class` declarations"
|
||||
weight = 1
|
||||
+++
|
||||
|
||||
The general concepts behind classes, instances, overloading etc. were
|
||||
introduced in section [2.1](fixme). A new class is declared using the
|
||||
following:
|
||||
|
||||
```
|
||||
topDefn ::= class [ context => ] classId {tyVarId }[ | funDep ] where {
|
||||
{varId :: ctxType ; }
|
||||
}
|
||||
```
|
||||
|
||||
|
||||
*classId* is the newly declared class. It can be polymorphic, if
|
||||
*tyVarId*'s exist; these are called the *parameters* of the type class.
|
||||
The *tyVarId*'s may themselves be constrained by *context*, in which
|
||||
case the classes named in *context* are called the "super-classes" of
|
||||
this class. The "*varId*`::`*ctxType*" list declares the class method
|
||||
names and their types.
|
||||
|
||||
Example (from the Prelude):
|
||||
|
||||
```hs
|
||||
class Literal a where
|
||||
fromInteger :: Integer -> a
|
||||
```
|
||||
|
||||
This defines the class `Literal`. It says that any type `a` in this
|
||||
class must have a method (a function) called `fromInteger` that converts
|
||||
an `Integer` value into the type `a`. In fact, this is the mechanism the
|
||||
BH uses to interpret literal constants, e.g., to resolve whether a
|
||||
literal like `6`847 is to be interpreted as a signed integer, an
|
||||
unsigned integer, a floating point number, a bit value of 10 bits, a bit
|
||||
value of 8 bits, etc. (This is described in more detail in Section
|
||||
[5.3](fixme).)
|
||||
|
||||
|
||||
Example (from the Prelude):
|
||||
|
||||
```hs
|
||||
class (Literal a) => Arith a where
|
||||
(+) :: a -> a -> a
|
||||
(-) :: a -> a -> a
|
||||
negate :: a -> a
|
||||
(*) :: a -> a -> a
|
||||
```
|
||||
|
||||
|
||||
This defines the class `Arith` with super-class `Literal`. It says that
|
||||
for any type `a` that is a member of the class `Arith`, it must also be
|
||||
a member of the class `Literal`, and it must have four methods with the
|
||||
given names and types. Said another way, an `Arith` type must have a way
|
||||
to convert integer literals into that type, and it must have addition,
|
||||
subtraction, negation and multiplication defined on it.
|
||||
|
||||
|
||||
The optional *funDep* section specifies *functional dependencies*
|
||||
between the parameters of the type class:
|
||||
|
||||
```
|
||||
funDep ::= { {tyVarId }-> {tyVarId }, }
|
||||
```
|
||||
|
||||
These declarations specify that a type parameter may be determined
|
||||
uniquely by certain other type parameters. For example:
|
||||
|
||||
```hs
|
||||
class Add x y z | x y -> z, y z -> x, z x -> y
|
||||
```
|
||||
|
||||
Here, the class declaration says that for any triple of types `x`, `y`
|
||||
and `z` that are in the class `Add`, any two of the types uniquely
|
||||
determines the remaining type, *i.e.,*
|
||||
|
||||
- x and y uniquely determine z,
|
||||
- y and z uniquely determine x, and
|
||||
- z and z uniquely determine y.
|
||||
|
||||
See section [8.1](fixme) for more detailed insights into
|
||||
the use of functional dependencies.
|
||||
|
||||
> **NOTE:**
|
||||
> Functional dependencies are not currently checked by the compiler.
|
113
content/chapter4/page6.md
Normal file
113
content/chapter4/page6.md
Normal file
|
@ -0,0 +1,113 @@
|
|||
+++
|
||||
title = "`instance` declarations"
|
||||
weight = 1
|
||||
+++
|
||||
|
||||
A type can be declared as an instance of a class in two ways. The
|
||||
general mechanism is the `instance` declaration; a convenient shortcut
|
||||
that can sometimes be used is the `deriving` mechanism.
|
||||
|
||||
The general `instance` declaration grammar is the following:
|
||||
|
||||
```
|
||||
topDefn ::= instance context => classId {type }where
|
||||
{ {localDefn ; }}
|
||||
```
|
||||
|
||||
This can be read as saying that the type *type* is an instance of class
|
||||
*classId*, provided the constraints of *context* hold, and where the
|
||||
*localDefn*'s specify the implementation of the methods of the class.
|
||||
|
||||
Sometimes, when a new type is defined using a `data` declaration, it can
|
||||
simultaneously be made a member of certain useful, predefined classes,
|
||||
allowing the compiler to choose the "obvious" implementation of the
|
||||
class methods. This is done using the `deriving` qualification to a
|
||||
`data` declaration (described in section
|
||||
[4.1](fixme)) or to a
|
||||
`struct` declaration (described in section
|
||||
[4.2](fixme)). The only classes for which `deriving` can
|
||||
be used for general types are `Bits`, `Eq` and `Bounded`. Furthermore,
|
||||
`deriving` can be used for any class if the type is a data type that is
|
||||
isomorphic to a type that has an instance for the derived class.
|
||||
|
||||
### Deriving `Bits` {#sec-deriving-Bits}
|
||||
|
||||
The instances derived for the `Bits` class can be described as follows:
|
||||
|
||||
- For a `struct` type it is simply the the concatenation of the bits for
|
||||
all the fields. The first field is in the leftmost (most significant)
|
||||
bits, and so on.
|
||||
- For a `data` type, all values of the type occupy the same number of
|
||||
bits, regardless of which disjunct (constructor) it belongs to. This
|
||||
size is determined by the largest disjunct. The leftmost (most
|
||||
significant) bits are a code (a tag) for the constructor. As few bits as
|
||||
possible are used for this. The first constructor in the definition is
|
||||
coded 0, the next constructor is coded 1, and so on. The size of the
|
||||
rest of the bits is determined by the largest numbers of bits needed to
|
||||
encode the fields for the constructors. For each constructor, the fields
|
||||
are laid out left to right, and the concatenated bits are stored right
|
||||
justified (*i.e.,* at the least significant bits). For disjuncts that
|
||||
are smaller than the largest one, the bits between the constructor code
|
||||
and the field bits, if any, are "don't care" bits.
|
||||
|
||||
Examples: The type
|
||||
|
||||
```hs
|
||||
data Bool = False | True
|
||||
```
|
||||
|
||||
uses one bit. `False` is represented by 0 and `True` by 1.
|
||||
|
||||
```hs
|
||||
struct Två = { första :: Bit 8; andra:: Bit 16 }
|
||||
```
|
||||
|
||||
uses 24 bits with `första` in the upper 8 bits and `andra`
|
||||
in the lower 16.
|
||||
|
||||
```hs
|
||||
data Maybe a = Nothing | Just
|
||||
```
|
||||
|
||||
a will use $1+n$ bits,
|
||||
where $n$ bits are needed to represent values of type `a`. The extra bit
|
||||
will be the most significant bit and it will be 0 (followed by $n$
|
||||
unspecified bits) for `Nothing` and 1 (followed by the $n$ bits for `a`)
|
||||
for `Just`.
|
||||
|
||||
|
||||
### Deriving `Eq`
|
||||
|
||||
|
||||
The instances derived for the `Eq` class is the natural equality for the
|
||||
type. For a struct all fields have to be equal, for a data type the
|
||||
constructors have to be equal and then all their parts.
|
||||
|
||||
|
||||
### Deriving `Bounded`
|
||||
|
||||
|
||||
An instance for `Bounded` can be derived for an enumeration type,
|
||||
*i.e.,* a data type where all constructors are niladic. The `minBound`
|
||||
will be the first constructor and the `maxBound` will be the last.
|
||||
|
||||
`Bounded` can also be derived for a `struct` type if all the field types
|
||||
of the struct are `Bounded`. The `minBound` will be the struct with all
|
||||
fields having their respective `minBound`, and correspondingly for
|
||||
`maxBound`.
|
||||
|
||||
### Deriving for isomorphic types
|
||||
|
||||
A data type with one constructor and one argument is isomorphic to its
|
||||
type argument. For such a type any one-parameter class can be used, in a
|
||||
`deriving`, for which there is an instance for the underlying type.
|
||||
|
||||
Example:
|
||||
|
||||
```hs
|
||||
data Apples = Apple (UInt 32) deriving (Literal, Arith)
|
||||
five :: Apples
|
||||
five = 5
|
||||
eatApple :: Apples -\> Apples
|
||||
eatApple n = n - 1
|
||||
```
|
94
content/chapter4/page7.md
Normal file
94
content/chapter4/page7.md
Normal file
|
@ -0,0 +1,94 @@
|
|||
+++
|
||||
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](fixme)).
|
||||
|
||||
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:
|
||||
|
||||
```hs
|
||||
wordSize :: Integer
|
||||
wordSize = 16
|
||||
```
|
||||
|
||||
|
||||
This simply defines the identifier `wordSize` to have type `Integer` and
|
||||
value 16.
|
||||
|
||||
|
||||
Example:
|
||||
|
||||
```hs
|
||||
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:
|
||||
|
||||
```hs
|
||||
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](fixme)). 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](fixme)).
|
||||
|
||||
|
||||
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".
|
46
content/chapter4/page8.md
Normal file
46
content/chapter4/page8.md
Normal file
|
@ -0,0 +1,46 @@
|
|||
+++
|
||||
title = "Calling foreign functions"
|
||||
weight = 1
|
||||
+++
|
||||
|
||||
A function can be declared to be foreign which means that its
|
||||
implementation is not in BH.
|
||||
|
||||
|
||||
```
|
||||
topDefn ::= foreign varId :: type [= string ] [ , ( {string }) ]
|
||||
```
|
||||
|
||||
The optional string gives the name of the external "function" to use. If
|
||||
no string is given the same name as the BH name is used. The optional
|
||||
strings in parentheses are the port names of the Verilog module that
|
||||
implements the function. Without port names positional arguments will be
|
||||
used.
|
||||
|
||||
Example:
|
||||
|
||||
```hs
|
||||
foreign countOnes :: Bit n -> Bit 32 = "pop_count"
|
||||
```
|
||||
|
||||
|
||||
A call to `countOnes` will instantiate the Verilog `pop`` ``count`
|
||||
module. It should have the same number of arguments (with the same type)
|
||||
as the BH function, *and* an additional trailing argument which is the
|
||||
result. If the function is (size) polymorphic the instantiated types
|
||||
will be used as Verilog parameters.
|
||||
|
||||
|
||||
Example: using the declaration above an action, with the type of `x`
|
||||
being `Bit 5`,
|
||||
|
||||
```hs
|
||||
y := countOnes x
|
||||
```
|
||||
|
||||
|
||||
will translate to something like
|
||||
|
||||
```hs
|
||||
pop_count #(5) ires1(R_x, I_y);
|
||||
```
|
21
content/preface/_index.md
Normal file
21
content/preface/_index.md
Normal file
|
@ -0,0 +1,21 @@
|
|||
+++
|
||||
title = "UNDER CONSTRUCTION ⚠️"
|
||||
weight = 5
|
||||
sort_by = "weight"
|
||||
insert_anchor_links = "right"
|
||||
+++
|
||||
|
||||
> Note that these docs are under construction and may not be finished
|
||||
> until summer 2025!
|
||||
> There are several chapters remaining to complete!
|
||||
|
||||
This is a largely manual attempt(with much assistance from
|
||||
[Pandoc][pandoc]) to convert the
|
||||
[Bluespec Haskell/Classic LaTeX docs][bhdocs] to an online
|
||||
readable markdown format.
|
||||
|
||||
If you find any errors, please reach out to me at
|
||||
[yehowshua@joyofhardware.com](mailto:yehowshua@joyofhardware.com)
|
||||
|
||||
[pandoc]: https://pandoc.org
|
||||
[bhdocs]: https://github.com/B-Lang-org/bsc/tree/main/doc/BH_ref_guide
|
Loading…
Add table
Add a link
Reference in a new issue