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

Pretty-print translations only work within Isabelle, not for the generated code. The code generator does not offer any means to use type synonyms. You have to make the type synonym a typedef and lift all functions in your formalisation to the new type.


On 08/02/17 11:55, Tobias Nipkow wrote:

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"

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

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


theory Export_code
imports Find Insert Delete Insert_many

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?



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