Re: [isabelle] Code export, type_synonym, any way to preserve?



Hi Tom,


On 08/02/17 14:11, Tom Ridge wrote:



    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
generation?

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.

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,
Andreas




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.