Re: [isabelle] Differences between code_reflect and export_code

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.


On 2015-03-24 15:57, Lars Hupel wrote:
Dear codegen experts,

what's the difference between

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


  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.


Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge

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