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



Thanks to all. Very useful, and the '14 paper is a good read.

Thanks

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
>> of
>> 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):
>
> https://www.ethz.ch/content/dam/ethz/special-interest/infk/
> inst-infsec/information-security-group-dam/people/andreloc/
> lochbihler14iw.pdf
>
> Hope this helps,
> Andreas
>
>
>
>> 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?
>>
>> Thanks
>>
>> Tom
>>
>>



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