Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Generate fun/datatype definition in ML

view this post on Zulip Email Gateway (May 11 2021 at 09:56):

From: Arcuti Giuseppe <arcutig@student.ethz.ch>
Dear all,

For a project I'm working on, I need to generate functions and datatypes from Isabelle/ML. At the moment I'm building a string corresponding to the datatype I want to generate and then pass that to "BNF_FP_Def_Sugar.co_datatype_cmd". And I guess the equivalent solution for fun's would be passing a definition string to "Function_Common.function_parser". This seems a bit fragile to me, and I was wondering if there is a cleaner/higher-level interface for doing it.

Kind regards and thank you in advance,

Giuseppe

view this post on Zulip Email Gateway (May 11 2021 at 10:17):

From: Jasmin Blanchette via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear Giuseppe,

There's another function in the same file, called "co_datatypes", that takes the arguments after parsing. (If you search in the AFP, you will find two examples of its use.)

I hope this helps.

Cheers,

Jasmin

view this post on Zulip Email Gateway (May 15 2021 at 10:14):

From: Arcuti Giuseppe <arcutig@student.ethz.ch>
Dear Jasmin,

Thank you very much! I had seen that function, but no example of how to use it, so it was kind of difficult to figure out if it was useful.

I have now found the function "define_simple_datatype" in https://www.isa-afp.org/browser_info/current/AFP/Automated_Stateful_Protocol_Verification/trac.html which does exactly what I wanted.

I also saw that a function called "define_simple_fun" is also in there which just might also solve the second part of my question.

Kind regards,

Giuseppe

Last updated: Jan 04 2025 at 20:18 UTC