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