This question comes in a context where Isabelle is used with formal software development in mind more than with pure maths theorization in mind (and from a standalone developer's context).
Seems at best, SML programs generated from an Isabelle theory, use SML's IntInf.int
, not the native integer type, which is Int.int
; even if Code_Target_Int
, Code_Binary_Nat
or Code_Target_Nat
is used. Investigation of these theories sources seems to confirm it's all it can do. Native platform integers may be required for multiple reasons, including efficiency and the case the SML imperative program is to be optionally translated into an imperative language subset (ex. C or Ada), which is relevant when the theory relies on the Imperative_HOL
theory. The codegen.pdf
document which comes with the Isabelle distribution, did not help with it, except in suggesting the first of the options below.
Options may be:
- Not using Isabelle's
int
and nat
and re‑create a new numeric type from scratch, then use the code_printing
commands (with its type_constructor
and constant
) to give it the native platform representation and operations (implies inclusion of range limitations in some way in the theory) : must be tedious, although unlikely error‑prone I hope, due to the formal environment. Note this does seems feasible with Isabelle's own int
and nat
… it makes code generation fails, and nothing tells which constants are missing in the code_printing
command.
- If the SML program is to be compiled directly (ex. with MLTon), tweak the SML environment with a replacement
IntInf
structure : may be unsafe or not feasible, and still requires to embed the range limitations in the theory, so the previous options may finally be better than this one.
- Touch the generated program to change
IntInf
into Int
: easy, but it is safe? (at least, IntInf
implements the same signature as Int
do, so may be it's safe). As above, requires to specifies bounds in the theory in some way, it's OK with this.
- Dive into Isabelle internals : surely unreasonable, even worse than the second option.
- There exist a
Word
theory, but according to some readings, it's seems not suited for that purpose.
Are they other known options not listed here? Are they comments on the listed options?
If there is no ready‑to‑cook solutions (I feel there is no at the time), what hints or tracks would be best known? (ex. links to documents, mentions of concepts).
Update
Points #2 and #3 of the list, may be OK (if it really is) only if there is a single integer type. If the program use more than only one, it's not applicable.