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

On Mon, Jun 25, 2012 at 9:54 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> [...] HOLCF is explicitly a theory of computation; [...] Such a pity if it doesn't yet support code generation.
> Larry

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.

- Brian

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.