Herbie plugins define new functions, add rewrite rules, and even implement number representations.
Herbie plugins are installed separately. Herbie then automatically loads and uses them.
The softposit-herbie plugin implements support for posit arithmetic. Install it with:
raco pkg install --auto softposit-herbie
This plugin uses the SoftPosit library, only supported on Linux.
Even then is reported to misbehave on some machines. The plugin
support arithmetic operations, sqrt
, and quires.
Once softposit-herbie is installed,
specify :precision posit16
to inform Herbie that it
should assume the core's inputs and outputs are posit numbers. Other
posit sizes (with 8 or 32 bits) and also quires (for 8, 16, and 32
bit posits) are available, but are poorly supported.
The complex-herbie plugin implements support for complex numbers. Install it with:
raco pkg install --auto complex-herbie
Herbie input parameters are always real numbers; complex
numbers must be constructed with complex
. The
functions re
, im
, and conj
are available on complex numbers, along with the arithmetic
operators, exp
, log
, pow
,
and sqrt
. Complex and real operations use the same
syntax, but cannot be mixed: (+ (complex 1 2) 1)
is not
valid. Herbie reports type errors in such situations.
Complex operations are implemented by Racket, so results may differ (slightly) from complex numbers in some other language, especially for non-finite complex numbers. In the future, we hope to support complex-number arguments and fully support all complex-number operations.
The following is a guide to creating a Herbie plugin. Plugins are considered experimental and may change considerably between releases. If you run into issues, please write to the mailing list.
First Steps
All plugins are implemented as Racket packages. The easiest way to
initialize a new Racket package is to run
raco pkg new pkg-namein a new folder. Make sure the folder name is the same as the package name! This will initialize a Racket package with all the necessary files. Read the official Racket documentation on the raco tool for more information.
A single entry needs to be added to the package manifest stored in info.rkt
, and
Add the following line at the bottom of the file (define herbie-plugin 'name)
where name is a unique symbol that doesn't conflict with other Herbie plugins.
As a suggestion, this should just be the package name.
Next, edit the main.rkt
file by erasing everything except the
language specifier on the first line, and add the line (require herbie/plugin)
.
This gives the package access to the Herbie plugin interface.
Optionally add the following for debugging purposes
(eprintf "Loading pkg-name support...\n")
.
Finally, run the following in the folder containing info.rkt
and main.rkt
:
raco pkg installThis should install your package and check for errors. Now everything is set up! Of course, your plugin is empty and doesn't add any useful features. If you added the debugging line in
main.rkt
, you should see the string
when you run Herbie.
Adding Features
Now that you have an empty plugin, you can begin adding new functions, rewrite
rules, and number representatons.
The procedures exported by the Herbie plugin interface can be roughly divided into
two categories: unique and parameterized.
Whether or not you use the unique or parameterized half of the interface
(or maybe both!) depends entirely on the number representation a feature is being
implemented for.
First, identify if your number representation is unique or parameterized.
For example, if you are adding features for double
precision
(or rather binary64
), the representation is unique.
If you are adding features for a generic floating point format, say
(float ebits nbits)
, then the representation is parameterized.
Plugin Interface (Unique)
The following are the signatures and descriptions of the
plugin procedures for unique representations.
These procedures should be called from the top-level of main.rkt
rather than inside a function.
(define-type name (exact? inexact?)
exact->inexact inexact->exact)
name
.
The arguments exact?
and inexact?
return true if a value is an exact or high-precision approximate representation.
For Herbie's real
type, exact?
is implemented
with real?
and inexact?
is implemented
with bigfloat?
. The procedures exact->inexact
and
inexact->exact
convert between exact?
and inexact?
values.
(define-representation (name type repr?)
bigfloat->repr
repr->bigfloat
ordinal->repr
repr->ordinal
width
special?)
name
.
The representation will inherit all rewrite rules defined for type
.
By default, Herbie defines two types: real
and bool
.
Your representation will most likely inherit from real
.
The width
argument should be the bitwidth of the representation,
e.g. 64 for binary64
.
The argument repr?
is a procedure that accepts any argument and returns
true if the argument is a value in the representation, e.g. an integer representation
should use Racket's integer?
, while special?
takes a
value in the representation and returns true if it is not finite, e.g. NaN or infinity.math/bigfloat
).
The last two convert between a value in your representation and its corresponding ordinal value.
Ordinal values for any representation must be within the interval [0, 2width - 1].
Check Racket's definition of
ordinals for floats.
Note that those ordinal values can be negative.
(define-operator (name itypes ...) otype
[bf bf-fn]
[ival ival-fn]
[nonffi nonffi-fn]
...)
+
or sin
.
The parameters itypes
and otype
are the input
type(s) and output type.
For example, +
takes two real
inputs and produces
one real
output.
The bf-fn
argument is the
bigfloat implementation of your operator.
The ival-fn
argument is the Rival
implementation of your operator. This is optional but improves the quality of Herbie's output.
If you don't want to implement this, set ival-fn
to false
.
The nonffi-fn
argument is the exact implementation of your operator
(see define-type
for a description of exact).
To define operators with an unknown number of arguments, e.g. comparators,
add the attribute [itype itype]
.
This will override the input types defined by itypes
.
(define-operator-impl (op name ireprs ...) orepr
[fl fl-fn]
...)
op
with input representation(s) ireprs
and output representation orepr
.
The field name
must be unique.
For example, Herbie implements +.f64
and +.f32
for double- and single-precision floats.
The argument fl-fn
is the actual procedure that does the computation.
Like define-operator
, the input representations can be
overridden with [itype irepr]
.
By default, the attributes bf
, ival
, and nonffi
are inherited from op
but can be overridden as previously
described.
(define-constant name [bf bf-thunk] [ival ival-thunk])
π
or e
.
The bf-fn
argument is a thunk that
returns the bigfloat
value of the constant.
The ival-fn
argument is a thunk
that returns the Rival
interval value of the constant.
(define-constant-impl (const name) repr
[fl fl-thunk]
...)
const
for the representation repr
.
The argument fl-thunk
is a thunk that returns the approximate
value of the constant in the representation repr
.
By default, the attributes bf
and ival
are inherited
from const
but can be overridden (see define-operator
or define-operator-impl
for overriding attributes).
(define-ruleset name (groups ...)
#:type ([var repr] ...)
[rule-name match replace]
...)
name
of the ruleset as well as each rule-name
must be a unique symbol.
Each ruleset must be marked with a set of groups
(read here on ruleset groups).
Each rewrite rule takes the form match ⇝ replace
where Herbie's rewriter
will replace match
with replace
(not vice-versa).
Each match
and replace
is an expression whose operators are
the names of operator implementations rather than pure mathematical operators.
Any variable must be listed in the type information with its associated representation.
See the softposit-herbie
plugin for a more concrete example.
(define-ruleset* name (groups ...)
#:type ([var type] ...)
[rule-name match replace]
...)
define-ruleset
, but it defines a ruleset for every representation that
inherits from type
.
Currently, every type
must be the same, e.g.
all real
, for this procedure to function correctly.
Unlike define-ruleset
, match
and replace
contain the names of operators rather than operator implementations.
Plugin Interface (Parameterized)
Defining operators, constants, and representations for parameterized functions requires
a generator procedure for just-in-time loading of features for a particular
representation.
When Herbie encounters a representation it does not recognize (not explicitly defined
using define-representation
) it queries a list of generators in case the
representation requires just-in-time loading.
The following procedure handles generators:
(register-generator! gen)
false
.
To actually add representations, operators, etc. within a generator procedure, you must use a set of alternate procedures.
(register-representation! name
type
repr?
bigfloat->repr
repr->bigfloat
ordinal->repr
repr->ordinal
width
special?)
define-representation
, but used within generators.(register-operator! op name itypes
otype attribs)
define-operator
, but used within generators.
The argument itypes
is a list of the input types
while the argument attribs
are the same attributes for
define-operator
, e.g. bf
.
In this case, attribs
is an association:
(list (cons 'bf bf-fn) ...)
.
(register-operator-impl! op name ireprs
orepr attribs)
define-operator-impl
, but used within generators.
See register-operator!
for a description of ireprs
and attribs
.
(register-constant! name attribs)
define-constant
, but used within generators.
The argument attribs
are the same attributes for
define-constant
.
In this case, attribs
is an association:
(list (cons 'bf bf-thunk) ...)
.
(register-constant-impl! const name type attribs)
define-constant-impl
, but used within generators.
See register-constant!
for a description of attribs
.
(register-ruleset! name groups var-reprs rules)
define-ruleset
, but used within generators.
In this case, groups
is a list of rule groups;
var-reprs
is an association
pairing each variable in the ruleset with its representation, e.g.
(list (cons 'x '(float 5 16)) ...)
;
and rules
is a list of rules of the following
form (list (list rule-name match replace) ...)
.