Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Differences between code_reflect and export_code


view this post on Zulip Email Gateway (Aug 19 2022 at 17:29):

From: Lars Hupel <hupel@in.tum.de>
Dear codegen experts,

what's the difference between

code_reflect Foo
functions ...
file "foo.ML"

and

export_code ...
module_name Foo
in SML
file "foo.ML"

As far as I can tell, the effects are the same – SML code is being
produced and saved into a file, without processing it.

Cheers
Lars

view this post on Zulip Email Gateway (Aug 19 2022 at 17:29):

From: Wenda Li <wl302@cam.ac.uk>
Dear Lars,

In this example, I think they are the same. However, from my experience,
code_reflect is always used to make the code generation process static.
That is, when we are building a decision procedure based on
reflection/code generation, we really don't want the code generation
process to happen every time the decision procedure is called, instead
what we should expect is that the code is generated only once and
executed directly when needed. In this case, the file option is not used
quite often.

In short, I believe code_reflect and export_code should be almost the
same with the file option, but in general they serve different purposes.

Cheers,
Wenda

view this post on Zulip Email Gateway (Aug 19 2022 at 17:31):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>

In short, I believe code_reflect and export_code should be almost the
same with the file option, but in general they serve different purposes.

Indeed. code_reflect has a rather particular purpose. More on that can
be found in the tutorial on code generation.

Cheers,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 17:31):

From: Lars Hupel <hupel@in.tum.de>

Indeed. code_reflect has a rather particular purpose. More on that can
be found in the tutorial on code generation.

I've recently discovered 'code_reflect' as a means to replace the
cumbersome pattern

export_code in SML file foo.ML

SML_file foo.ML

And for that use case, it works well for me. It was just the additional
'file' argument which was hampering my understanding.

Cheers
Lars


Last updated: Apr 19 2024 at 16:20 UTC