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

Add some more float-to-float functions to machine_ieeeTheory.

Also add versions that output flags for the exception status.


# a279ce83 24-Jul-2017 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Improve floating-point rounding conversions.

The conversions should now work for more float types, e.g. evaluation for "(23, 8 + 1) float" was not working before.


# 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.


# 086cbeb8 22-Jun-2017 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Minor changes within floating-point theory.

• The operations float_negate1985 and float_abs1985 have been removed.
• Added a predicate float_is_signalling and renamed float_some_nan to float_some_qnan.
• Fixed problem with EQ_tm and GT_tm being swapped in binary_ieeeSyntax.


# 6ccca7af 16-Feb-2016 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Make more of the floating-point library available to Moscow ML users.

Evaluation now works under Poly/ML. However, Poly/ML is needed for evaluation
using native floats (which is controlled through the "native ieee" trace).


# c5580900 15-Feb-2016 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Ensure most of the "floating-point" development works with Moscow ML.


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

Add "fused multiply and subtract" floating-point operation


# 7a5f60ec 04-Dec-2015 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Provide support for evaluating float to int and real to int operations.

For example, the following weren't working before (with intLib and realLib loaded):

EVAL ``NUM_FLOOR (-0.5)``; (* |- flr (-0.5) = 0 *)
EVAL ``NUM_CEILING 0.5``; (* |- clg 0.5 = 1 *)
EVAL ``INT_FLOOR 0.5``; (* |- flr 0.5 = 0 *)
EVAL ``INT_CEILING 0.5``; (* |- clg 0.5 = 1 *)


# 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.


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

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