Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] code_thms does not print (not implemented) con...

Email Gateway (Aug 22 2022 at 15:35):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear code generation experts,

I noticed some strange behaviour of code_thms. I don't really understand when code_thms
prints "(not implemented)" for a constructor and when it prints nothing. The difference
can be seen in this tiny example:

theory Thy imports Main begin
datatype t = T | F
code_thms T True

The output is

T
(not implemented)
True

Why is "T" marked as "not implemented" whereas True is not? This difference not only shows
up for T and True, but all my datatype constructors are marked as "not implemented",
whereas most of the datatype constructors defined in HOL (True, False, Nil, Cons, Suc,
Inl, Inr) are not. Why?

IMO constructors declared with code_datatype should not be marked as "not implemented"
because I'd prefer if this is reserved for constants that are actually missing code
equations. Constructors cannot be given code equations anyway.

Best,
Andreas

Email Gateway (Aug 22 2022 at 15:36):

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

I noticed some strange behaviour of code_thms. I don't really understand
when code_thms prints "(not implemented)" for a constructor and when it
prints nothing. The difference can be seen in this tiny example:

theory Thy imports Main begin
datatype t = T | F
code_thms T True

The output is

T
(not implemented)
True

thanks for reporting this.

The reason is that constructors are currently treated inconsistently at
the time a datatype is registered vs. at theory merge.

IMO constructors declared with code_datatype should not be marked as
"not implemented" because I'd prefer if this is reserved for constants
that are actually missing code equations.

Indeed.

I will have a look after that.

Cheers,
Florian
signature.asc

Email Gateway (Aug 22 2022 at 15:54):

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

your observation actually triggered an inspection, substantially
reformulation and clarification of considerable parts of the code
generator data store which maybe will lead to some kind of localized
code generation in the future.

Now you may inspect whether the output of the diagnostic code generator
commands seems reasonable.

Cheers,
Florian
signature.asc

Last updated: Apr 25 2024 at 08:20 UTC