Re: [isabelle] Code export, type_synonym, any way to preserve?
On 08/02/17 14:11, Tom Ridge wrote:
Sure. You can map any HOL type constructor to any target-language type using adaptation.
But as adaptations are unverified, they become part of the trusted code base, so be careful.
For integers, there's integer in the theory Code_Target, but this maps to Big_Int, not
it. Many years ago, there was also some setup to implement nat with the Big_Int type,
but that has long gone, because it was not formally checked that all functions
maintain the invariant ">= 0". If you import Code_Target_Nat from HOL/Library, your
generated code will implement Arith.nat using Big_Int, so you can construct such
Arith.nat values in your hand-written code and pass it to functions like split_at.
As OCaml's int type is bounded, one should not use it for nat, because nat is
unbounded in HOL. My AFP entry Native_Word imports various fixed-length integers from
the target languages (OCaml's int as Uint.uint). But clearly, Uint.uint is not
isomorphic to nat.
Suppose I know somehow (!) that integer overflow is not a problem, and in OCaml I define a
Nat module, with type t = int, which maintains the >=0 invariant (and others? basically,
int is made to behave like nat). Is it possible to target the Nat.t type in Isabelle code
Adaptations are explained in general the code generator tutorial (isabelle doc codegen,
Section 6). In your case, you can probably copy most of the OCaml adaptations (code_module
and code_printing) for uint in AFP/Native_Word/Uint and change everything from uint to
nat. Note that Native_Word does some things in a somewhat complicated way (there are
several versions of division), because it tries to fit several different target languages
and evaluation by the simplifier under one hood. If you grep for "code_printing" in the
distribution and the AFP, you should find more examples of how adaptation is done in practice.
Hope this helps,
This archive was generated by a fusion of
Pipermail (Mailman edition) and