README
1This directory contains a modernised version of src/float. The data
2representation has been updated to make use of HOL4 bit-vectors. There is also
3additional tool support, e.g. for relatively efficient evaluation of basic
4floating-point arithmetic operations.
5
6 * binary_ieeeTheory
7
8 Generic IEEE-754 floating-point theory. Introduces the type
9 ``:('t, 'w) float``, where ``:'t`` and ``:'w`` represent the sizes of the
10 significand and exponent respectively.
11
12 * lift_ieeeTheory and lift_machine_ieeeTheory
13
14 Error bound theorems for some roundTiesToEven floating-point operations.
15
16 * binary_ieeeSyntax
17
18 Syntax support for binary_ieeeTheory.
19
20 * binary_ieeeLib
21
22 Contains conversions for evaluating floating-point operations.
23
24 * native/native_ieeeLib (Poly/ML only)
25
26 Contains conversions for evaluating floating-point operations using the
27 native SML type "float". These generate oracle theorems.
28
29 * machine_ieeeLib
30
31 Supports building floating-point theories for particular bit-vector
32 encodings.
33
34 * machine_ieeeTheory
35
36 Uses machine_ieeeLib to build a theory covering 16-bit, 32-bit and 64-bit
37 floating-point encodings. For example, floating-point operations are defined
38 over the type ``:word16`` by using maps to and from the type
39 ``:(10, 5) float``, which is abbreviated to ``:half``. We also have
40 ``:single`` for ``:(23, 8) float`` and ``:double`` for ``:(52, 11) float``.
41
42 * fp16Syntax, fp32Syntax, fp64Syntax
43
44 These provide syntax support for the theory machine_ieeeTheory. They are
45 built using the functor in fp-functor.sml and signature in fp-sig.sml.
46
47 * machine_ieeeSyntax
48
49 Syntax support for floating-point operations that convert between single and
50 double precision values.
51