History log of /seL4-l4v-10.1.1/HOL4/src/floating-point/fp-functor.sml
Revision Date Author Comments
# 03e5e893 29-Nov-2017 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Update some floating-point syntax files.


# 037155db 12-Jul-2017 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Update floating-point theory to specify exception flags for some operations.

• The flags are: DivideByZero, InvalidOp, Overflow, Precision and Underflow.
• The arithmetic operations now return a pair (flags and result).
• Native (oracle) evaluation has been overhauled. It now only applies to some 64-bit machine_ieeeTheory operations directly.
• The L3 Importer has been updated.


# 161d7acc 02-Jul-2017 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Floating-point update.

• isSignallingNan predicate is added to machine_ieeeTheory.
• The RISC-V model is simplified in places (for DIV and REM).
• The L3 import is extended to cover more operations.


# 8c6fab69 22-Jun-2017 Ramana Kumar <ramana@member.fsf.org>

Remove float_negate1985 and float_abs1985

This seems to have been half done in
086cbeb857ffbcc88784f4f81db7626771ad8758


# 2fd5e05f 17-Dec-2015 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Add "fused multiply and subtract" floating-point operation


# bd1997ff 26-Nov-2015 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Update for latest version of L3.

Now supports floating-point square root and size conversions.


# 96edb9f3 20-Nov-2015 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Update for the latest version of L3, which has additional floating-point support.

Cover IEEE754:1985 behaviour for "abs" and "neg". Also adds support for "compare", "toInt" and "fromInt" at the machine level.


# ac817518 11-May-2015 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Modify the type of HolKernel.syntax_fns and add some documentation.

This is in response to issue #247.

The change to the type makes things a little more natural when using partial applications - for example, HolKernel.syntax_fns1 can be used to provide syntax support for regular unary operations.


# 52264b7d 01-May-2014 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Relocate examples/l3-machine-code/common/fp to src/floating-point.