Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] HOLCF code generation (was: Lazy Lists)


view this post on Zulip Email Gateway (Aug 18 2022 at 20:13):

From: Brian Huffman <huffman@in.tum.de>
One obstacle to code generation in HOLCF is the application operator:
If you have a HOLCF function "foo" with equation "foo\<cdot>x = x",
the code generator will try to interpret this as a defining equation
for "op \<cdot>" (because that is the top-most constant on the lhs)
instead of "foo", as intended.

If there is demand for code generation in HOLCF, it would probably be
worthwhile to put some effort into implementing it. It might be easy
to modify the code generator to handle application operators.

Alternatively, we could implement some new HOLCF automation: We could
define full-function-space copies of constants with
continuous-function types, and translate code equations involving
\<cdot> to use these copies.


Last updated: May 02 2024 at 08:19 UTC