Email Gateway (Aug 18 2022 at 19:42): Email Gateway (Aug 18 2022 at 19:42):From: Ondřej Kunčar <kuncar@in.tum.de>
Hi,
I've experienced the following problem with ML-level of Isabelle (namely
with local theories and the code generator):
My code is inside the command quotient_type and thus inside a
local_theory context. In this context a new constant is defined (by
Local_Theory.define) and it's called let's say "abs". Because I am
inside a local_theory context, this constant is actually a fixed
variable and not a real constant. So far so good. But now I want to call
Code.add_datatype and thus say that "abs" is a code datatype
constructor. I do it by the following command:
Local_Theory.declaration {syntax = false, pervasive = true}
(K (Context.mapping (Code.add_datatype [(name, type)]) I))
But then the code generator complains that "abs" is not a constant.
How can I solve this situation? It seems to me that I need
either a) jump away from a local_theory context for a while and let
"abs" get transformed to a real constant
or b) I need something like a "localized" code generator package.
Thanks for an answer.
Cheers,
Ondrej
Email Gateway (Aug 18 2022 at 19:43):From: Makarius <makarius@sketis.net>
On Tue, 15 May 2012, Ondřej Kunčar wrote:
I've experienced the following problem with ML-level of Isabelle (namely
with local theories and the code generator):
You should not use this confusing term "ML-level of Isabelle".
Isabelle/ML and Isabelle/Isar are intertwined in a certain way, and there
is no lower or upper level here. See also the recent thread
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-April/msg00066.html
My code is inside the command quotient_type and thus inside a
local_theory context. In this context a new constant is defined (by
Local_Theory.define) and it's called let's say "abs". Because I am
inside a local_theory context, this constant is actually a fixed
variable and not a real constant.
This is again a bit confusing. Local_Theory.define is for abstract term
definitions. It depends on the local_theory target how this will be
represented in the foundation, and integrated into the target for later
use by the user. For a global theory it will become a constant, for a
locale a constant that depends on locale parameters plus some
abbreviations, for a completely different target something completely
different.
A simple analogy is this: local_theory is the regular virtual memory view
of a process address space that is now commonplace, probably even on tiny
mobile devices. There are physical hardware addresses in the foundations
somewhere, but you cannot count on that in your program code.
But now I want to call Code.add_datatype and thus say that "abs" is a
code datatype constructor. I do it by the following command:
Local_Theory.declaration {syntax = false, pervasive = true} (K
(Context.mapping (Code.add_datatype [(name, type)]) I))
The "K" above is part of the problem. It disregards the morphism for the
mapping, which is required to move things from one context to the other,
before they can be applied to the concrete context in question.
Admittedly this is the difficult aspect of local theory declarations, but
ignoring it is no solution. To make effective use of the Isabelle
infrastructure, it is important to develop a habit to do things in "the
canonical" way. Thus one does not have to revisit all the implementation
details from the ground up over and over again.
But then the code generator complains that "abs" is not a constant. How
can I solve this situation? It seems to me that I need either a) jump
away from a local_theory context for a while and let "abs" get
transformed to a real constant or b) I need something like a "localized"
code generator package.
Generally, you can try to work with general declarations with proper use
of morphisms, or make a reduced version that merely puts things into the
background theory context. For that you transform the abstract term once
to move it the global theory and then work with
Local_Theort.background_theory etc.
I can't say anything about the possibility of a localied code generator.
Florian Haftmann should comment on that.
Makarius
Email Gateway (Aug 18 2022 at 19:44):From: Ondřej Kunčar <kuncar@in.tum.de>
Thanks. Local_Theort.background_theory did the job.
Ondrej
Last updated: Apr 25 2024 at 04:18 UTC