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.
BSD LicenseTopics
Theories of 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
- 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