[isabelle] Code generation - bidirectionally?

[Moa Johansson]

Hi,

We’ve got a tool (Hipster) which relies on external tools to generate candidate lemmas for Isabelle theories. However, it is not always stable when it comes to translation between Isabelle-Haskell and back.

Currently we use Isabelle’s code generator to first generate Haskell code, which then gets processed by another tool in charge of producing the conjectures. The conjectures are then read back into Isabelle. We regularly come across problems with how (library) functions and datatypes gets renamed during this process. For instance, functions over natural numbers will, when translated to Haskell, get names like “plus_nat”, “mult_nat” and so on. However, when reading a conjecture about e.g. “plus_nat” back it needs to be parsed in Isabelle as its internal long name “Groups.plus_class.plus”.

I know we’re using the code generator in a way it was never intended, but is there a way of knowing which constants in Isabelle gets renamed by code generation (and to what)?

Would like to have a less brittle way of translating back and forth if at all possible. Preferably without having to resort to

[Florian Haftmann]

Hi Moa,

there are actually two relevant aspects.

We’ve got a tool (Hipster) which relies on external tools to generate candidate lemmas for Isabelle theories. However, it is not always stable when it comes to translation between Isabelle-Haskell and back.
Currently we use Isabelle’s code generator to first generate Haskell code, which then gets processed by another tool in charge of producing the conjectures. The conjectures are then read back into Isabelle. We regularly come across problems with how (library) functions and datatypes gets renamed during this process. For instance, functions over natural numbers will, when translated to Haskell, get names like “plus_nat”, “mult_nat” and so on. However, when reading a conjecture about e.g. “plus_nat” back it needs to be parsed in Isabelle as its internal long name “Groups.plus_class.plus”.
I know we’re using the code generator in a way it was never intended, but is there a way of knowing which constants in Isabelle gets renamed by code generation (and to what)?

Concerning »plus_nat« etc., this has nothing to do with code generation
itself but is just a purely logical substitution of class parameters on
specific instances by dedicated shadow constants:

ML_val ‹Axclass.unoverload @{context} @{thm Suc_nat_number_of_add}›

ML_val ‹Axclass.overload_conv @{context} @{cterm
"plus_nat_inst.plus_nat"}›

Would like to have a less brittle way of translating back and forth if at all possible. Preferably without having to resort to writing our own code generator ☺.

Do you know a priori which set of identifiers is relevant for you? Then
there are the following possibilities:

a) You can control the resulting name space explicitly, e.g.

code_identifier constant distinct ⇀ (Haskell) "Bar.blubb"

export_code distinct in Haskell

You can use the corresponding ML interface to establish your own
controlled name mapping.

b) Functions Code_Target.produce_code* take a list of identifiers and
return their images under code generation.

Hope this helps,
Florian