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