Re: [isabelle] code_include SML and eval

Florian Haftmann schrieb:
Hi Peter,

I have written some code-generation setup that requires on an additional
What is the recommended way to include this additional module into the
generated code?
I tried:
code_include SML "Foo" {*
 structure Foo = struct
   exception Bar;

For syntactic reasons includes containing structures produce not always
valid code (let structure Foo = ... in ... end is not valid SML!).

Without the surrounding structure, it should work.  Perhaps what you
actually want is something like:

	axiomatization bar :: 'a
	code_abort bar

which produces an exception:

	export_code bar in SML file -

And what is code_include good for?

It is one of the things you should try to get along without...
Hi, thank you for the answer.

The exception was just an example. Actually, the structure contains a functional array implementation (using ML-references to store chains of undo-information for old versions of the array) similar to Haskells Array.Diff package.

So, the other option seems to be to include this structure in the ML-basis under which the generated ML is then executed. However, this makes the generated code not self-contained any more.


Hope this helps,

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