*To*: Tom Ridge <tom.j.ridge+list at googlemail.com>*Subject*: Re: [isabelle] Code export, type_synonym, any way to preserve?*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Wed, 8 Feb 2017 14:22:28 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <CABooLwPrX6v7=Eiu1_Gaktw_=SHtmftfzUNVdsF6EC7fksWc-g@mail.gmail.com>*References*: <CABooLwO0cJb4ARMTwmUWibFngK_fiBFjkaa-RVrff3caLyRP2Q@mail.gmail.com> <61a9d112-6bdd-6e3a-2eac-4f6d7a670ba8@inf.ethz.ch> <CABooLwPrX6v7=Eiu1_Gaktw_=SHtmftfzUNVdsF6EC7fksWc-g@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.7.0

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?

Hope this helps, Andreas

**References**:**[isabelle] Code export, type_synonym, any way to preserve?***From:*Tom Ridge via Cl-isabelle-users

**Re: [isabelle] Code export, type_synonym, any way to preserve?***From:*Andreas Lochbihler

**Re: [isabelle] Code export, type_synonym, any way to preserve?***From:*Tom Ridge via Cl-isabelle-users

- Previous by Date: Re: [isabelle] Code export, type_synonym, any way to preserve?
- Next by Date: Re: [isabelle] Browsing finished theories in Isabelle/jEdit
- Previous by Thread: Re: [isabelle] Code export, type_synonym, any way to preserve?
- Next by Thread: [isabelle] Interesting example of blast looping in 2016-1
- Cl-isabelle-users February 2017 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list