Stream: Archive Mirror: Isabelle Users Mailing List

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

view this post on Zulip Email Gateway (Aug 22 2022 at 15:01):

From: Tom Ridge via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
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:

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

view this post on Zulip Email Gateway (Aug 22 2022 at 15:01):

From: Tobias Nipkow <nipkow@in.tum.de>
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

smime.p7s

view this post on Zulip Email Gateway (Aug 22 2022 at 15:01):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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.

Andreas

view this post on Zulip Email Gateway (Aug 22 2022 at 15:01):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

view this post on Zulip Email Gateway (Aug 22 2022 at 15:01):

From: Tom Ridge via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Thanks to all. Very useful, and the '14 paper is a good read.

Thanks

view this post on Zulip Email Gateway (Aug 22 2022 at 15:02):

From: Tom Ridge via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Suppose I know somehow (!) that integer overflow is not a problem, and in
OCaml I define a Nat module, with type t = int, which maintains the >=0
invariant (and others? basically, int is made to behave like nat). Is it
possible to target the Nat.t type in Isabelle code generation?

Thanks

view this post on Zulip Email Gateway (Aug 22 2022 at 15:02):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Tom,

Sure. You can map any HOL type constructor to any target-language type using adaptation.
But as adaptations are unverified, they become part of the trusted code base, so be careful.

Adaptations are explained in general the code generator tutorial (isabelle doc codegen,
Section 6). In your case, you can probably copy most of the OCaml adaptations (code_module
and code_printing) for uint in AFP/Native_Word/Uint and change everything from uint to
nat. Note that Native_Word does some things in a somewhat complicated way (there are
several versions of division), because it tries to fit several different target languages
and evaluation by the simplifier under one hood. If you grep for "code_printing" in the
distribution and the AFP, you should find more examples of how adaptation is done in practice.

Hope this helps,
Andreas

Last updated: Apr 25 2024 at 20:15 UTC