Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] code_include SML and eval

Email Gateway (Aug 18 2022 at 14:44):

From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,

I have written some code-generation setup that requires on an additional
module.
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;
end;
*}

This works fine for code_export.
However, the eval-method seems to have problems with it:
lemma "(5::code_numeral) = Code_Numeral.of_nat 5"
apply eval
yields:
*** Error (line 3):
*** in expected but structure was found
*** Error (line 3):
*** Expression expected but structure was found
*** Error (line 3):
*** end expected but structure was found
*** Error (line 3):
*** ) expected but structure was found
*** Error (line 3):
*** ) expected but structure was found
*** Exception- ERROR "Static Errors" raised
*** At command "apply".

Without the code_include, it works fine!

How should I include my additional code. And what is code_include good for?

Regards and thanks in advance for any hints,
Peter

Email Gateway (Aug 18 2022 at 14:45):

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

I have written some code-generation setup that requires on an additional
module.
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;
end;
*}

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...

Hope this helps,
Florian
signature.asc

Email Gateway (Aug 18 2022 at 14:45):

From: Peter Lammich <peter.lammich@uni-muenster.de>
Florian Haftmann schrieb:

Hi Peter,

I have written some code-generation setup that requires on an additional
module.
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;
end;
*}

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.

Regards,
Peter

Hope this helps,
Florian

Email Gateway (Aug 18 2022 at 14:45):

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

One possibility (not very convinving) is to leave everything outside the
structure. But I guess there is a more direct way: are your functional
arrays functional in the sense that from outside they behave functional?
Then it would be feasible to implement them functionally in HOL,
together with some code_consts directives which implement some
operations destructively.

Hope this helps,
Florian
signature.asc

Email Gateway (Aug 18 2022 at 14:46):

From: Peter Lammich <peter.lammich@uni-muenster.de>
Florian Haftmann schrieb:

Hi Peter,

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.

One possibility (not very convinving) is to leave everything outside the
structure. But I guess there is a more direct way: are your functional
arrays functional in the sense that from outside they behave functional?

Yes, exactly that.
Then it would be feasible to implement them functionally in HOL,
together with some code_consts directives which implement some
operations destructively.

Ok, then I still need a trick how to include the
datatype 'a FArray = A of 'a Array.array | U of (int'a'a FArray ref)
in the generated ML.

The code_datatype to that I map the Isabelle-array type is: "'a FArray
ref", but the
above FArray-datatype has no counterpart in Isabelle.

Hmm? (not sure whether I understood your proposal)

regards + thank you,
Peter

Last updated: May 06 2024 at 12:29 UTC