Abstract
This entry makes machine words and machine arithmetic available for code generation from Isabelle/HOL. It provides a common abstraction that hides the differences between the different target languages. The code generator maps these operations to the APIs of the target languages. Apart from that, we extend the available bit operations on types int and integer, and map them to the operations in the target languages.
License
History
- July 15, 2018
- added cast operators for default-size words (revision fc1f1fb8dd30)
- September 2, 2017
- added 64-bit words (revision c89f86244e3c)
- October 6, 2014
- proper test setup with compilation and execution of tests in all target languages
(revision 5d7a1c9ae047)
- March 31, 2014
- added words of default size in the target language (by Peter Lammich)
(revision 25caf5065833)
- November 6, 2013
- added conversion function between native words and characters
(revision fd23d9a7fe3a)
Topics
Session Native_Word
- Code_Target_Word_Base
- Word_Type_Copies
- Code_Int_Integer_Conversion
- Code_Target_Integer_Bit
- Uint64
- Uint32
- Uint16
- Uint8
- Uint
- Native_Cast
- Native_Cast_Uint
- Native_Word_Imperative_HOL
- Native_Word_Test
- Code_Target_Int_Bit
- Native_Word_Test_Emu
- Native_Word_Test_PolyML
- Native_Word_Test_PolyML2
- Native_Word_Test_PolyML64
- Native_Word_Test_Scala
- Native_Word_Test_GHC
- Native_Word_Test_MLton
- Native_Word_Test_MLton2
- Native_Word_Test_OCaml
- Native_Word_Test_OCaml2
- Native_Word_Test_SMLNJ
- Native_Word_Test_SMLNJ2
- Uint_Userguide
Depends on
Used by
- Verified Complete Test Strategies for Finite State Machines
- MiniSail - A kernel language for the ISA specification language SAIL
- Mersenne primes and the Lucas–Lehmer test
- WebAssembly
- Iptables Semantics
- Algorithms for Reduced Ordered Binary Decision Diagrams
- A Separation Logic Framework for Imperative HOL
- Generating linear orders for datatypes
- Collections Framework
- Jinja with Threads