Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Interfacing of generated with native code

view this post on Zulip Email Gateway (Aug 22 2022 at 20:59):

From: Peter Lammich <lammich@in.tum.de>
Hi List,

I have a datatype
datatype result = INT integer | STRING String.literal

and an Isabelle function
compute :: int => result

I now want the code generator to map this Isabelle function to an
external implementation, e.g.

code_printing
constant compute ⇀ (Scala) "MyObject.compute"

However, is there any way to come up with a Scala implementation for
MyObject.compute, that can "see" the datatype "result", which is
generated by the code generator?

If not, is there any possibility how to pass complex data types between
Isabelle generated and native Scala code?

Thanks in advance for any help,
Peter

Last updated: Apr 20 2024 at 04:19 UTC