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

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):

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 MHonArc.