NameDateSize

..25-Jul-201970

binary_ieee.otdH A D25-Jul-2019210

binary_ieeeLib.sigH A D25-Jul-2019726

binary_ieeeLib.smlH A D25-Jul-201939.4 KiB

binary_ieeeScript.smlH A D25-Jul-2019146 KiB

binary_ieeeSyntax.sigH A D25-Jul-201910.6 KiB

binary_ieeeSyntax.smlH A D25-Jul-201912.7 KiB

fp-functor.smlH A D25-Jul-20194.7 KiB

fp-sig.smlH A D25-Jul-20196.4 KiB

fp16Syntax.smlH A D25-Jul-2019157

fp32Syntax.smlH A D25-Jul-2019157

fp64Syntax.smlH A D25-Jul-2019157

hol4-floating-point-unint.thyH A D25-Jul-2019376

hol4-floating-point.thyH A D25-Jul-2019465

HolmakefileH A D25-Jul-20191,010

lift_ieeeScript.smlH A D25-Jul-201964.7 KiB

lift_machine_ieeeScript.smlH A D25-Jul-201912.9 KiB

machine_ieeeLib.sigH A D25-Jul-2019110

machine_ieeeLib.smlH A D25-Jul-201921.9 KiB

machine_ieeeScript.smlH A D25-Jul-20194.5 KiB

machine_ieeeSyntax.sigH A D25-Jul-20192.4 KiB

machine_ieeeSyntax.smlH A D25-Jul-20192 KiB

native/H25-Jul-20196

READMEH A D25-Jul-20191.7 KiB

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