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





On 08/02/2017 11:44, Tom Ridge via Cl-isabelle-users wrote:
Dear All,

I'm exporting to OCaml from Isabelle/HOL. I would like type synonyms to be
preserved (because I perform some munging on the generated code). Is this
possible? The top of the isabelle .thy looks like:

Unfortunately not, they are expanded after parsing. What you can do, but this is a hack, is to fold them back explicitly via a translation. Example:

type_synonym nat_list = "nat list"

translations
(type) "nat_list" <= (type) "nat list"

But now EVERY occurrence of "nat list" becomes "nat_list". Use at your own risk.

Tobias

theory Export_code
imports Find Insert Delete Insert_many
"~~/src/HOL/Library/Code_Target_Numeral"
"~~/src/HOL/Library/Code_Char"
begin


export_code "Code_Numeral.nat_of_integer" "Code_Numeral.int_of_integer"

...


----

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?

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


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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