Re: [isabelle] Code export, type_synonym, any way to preserve?
Thanks to all. Very useful, and the '14 paper is a good read.
On 8 February 2017 at 11:54, Andreas Lochbihler <
andreas.lochbihler at inf.ethz.ch> wrote:
> Hi Tom,
> On 08/02/17 11:44, Tom Ridge via Cl-isabelle-users wrote:
>> A related question: The code contains eg:
>> let rec dest_lista
>> xs = (match xs
>> with  ->
>> failwitha ['d'; 'e'; 's'; 't'; '_'; 'l'; 'i'; 's'; 't'; '\039';
>> ' ']
>> | _ :: _ -> (List.butlast xs, List.last xs));;
>> In Isabelle, the param to failwitha is a string. How can I make the list
>> chars param in the generated code a proper OCaml string?
> There are a few types in Isabelle/HOL's library which are designed for
> exchanging data in the generated code. For strings, you should use
> String.literal if you want to have OCaml strings.
> 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.
> In general, I recommend that you define a clear interface between the
> generated code and your hand-written parts, which should be as small as
> possible. Some thought's on this can be found in my Isabelle 2014 workshop
> paper (Section 4):
> Hope this helps,
>> Similarly, my exported code contains things like:
>> val split_at : Arith.nat -> 'a list -> 'a list * 'a list
>> How can I get OCaml's "int" type instead of Arith.nat?
This archive was generated by a fusion of
Pipermail (Mailman edition) and