Email Gateway (Aug 19 2022 at 17:19): Email Gateway (Aug 19 2022 at 17:19):From: Richard Molitor <gattschardo@googlemail.com>
Hello Florian,
thanks for your reply!
On Thu, 12 Mar 2015, Florian Haftmann wrote:
a) Your »workaround« with Local_Theory.background_theory is correct – as
long as you want to store data in background theories only. There are a
couple of applications where this indeed is feasible, but it is usually
not what you want.
The background for this is that I had my data stored in a Theory_Data struct
before, so my ``workaround'' just does exactly what I did before, except it's
now wrapped in a generic context. Which somehow does not seem to be what I
want.
My "dream" here was that the generic context would magically convert between
theory data and proof data for me, which was maybe a bit too much to whish
for.
In general I think I'm fine with just having the data in the background theory
only, the main problem is that I need to somewhat awkwardly extract it when
I'm in a local theory context.
b) The established pattern to store data generically is
Local_Theory.declaration (fn phi => …)
As a simple example, you might study src/HOL/Tools/functor.ML.
The idea is basically the following:
fun foo … lthy =
let
(We are relative to some local theory lthy here
and have some entities (terms t, theorems thm, …) relative
to lthy flying around as ML values here)
fun decl phi =
let
(We are called for each instance (interpretation)
of the original lthy, including lthy itself; the
logical difference is represented by morphism phi,
which we can apply (using Morphism.…) to transform our
original entities t, thm to obtain their appropriate
shape to do something with them relative
to the current instance)
in Data.put (a data record resulting from suitable) end;
in
lthy
|> Local_Theory.declaration decl
end;Put differently: * Your data is of a certain type T. * You explain how a fundamental morphism phi is applied to a value of
type T by giving a suitable lifting f :: morphism -> T -> T * Then your declaration for a particular x :: T looks as follows:
fun decl phi = Data.put (f phi x)Unfortunately, there is no elaborate section on this in the
implementation manual yet.
I will look into this. I had seen the morphisms before, but given the lack of
documentation, I decided to use the well-documented old-fashioned way of doing
things. Maybe reading functor.ML will enlighten me, thanks for the pointer!
If you can tell more about the application you are aiming towards, a
more concrete description than this generic abstract nonsense can be given.
The application is the ``open inductive'' [1] [2] package that I developed for
my master's thesis. It is in a working (but not pretty) state right now, what
I am trying to do is refine the code as best as I can, so it can be submitted
to the AFP in a somewhat maintainable state.
Greetings,
Richard
[1] documentation: http://pp.info.uni-karlsruhe.de/thesis.php?id=253
[2] code: https://github.com/gattschardo/open-inductive
Email Gateway (Aug 19 2022 at 17:19):From: Richard Molitor <gattschardo@googlemail.com>
Hello again,
I managed to implement the suggested morphsim variant to some success now,
thanks to your example!
What somewhat worries me is that I end up ignoring the morphism argument
completely, since it can contain thms and terms and (I think) they do not
affect the outcome of my commands, since they are just storing data.
When I figure out which additional thms may affect my commands though, this
way at least the infrastructure is in place in contrast to just storing in the
background theory as I did before [1], so I think I stick with this for now.
In the last part of the linked commit, I have a local_theory_to_proof command.
What I do now is store the result I get in after_qed using background_theory,
I could not get declaration to work here: No matter how I produce the initial
generic context, either from the local or the background theory, I somehow
always end up needing the other variant in the end.
Richard
[1]: https://github.com/gattschardo/open-inductive/commit/62a4bd010e91540a00427b18c5a5656f57686591
Email Gateway (Aug 19 2022 at 17:19):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Richard,
I just glanced quickly over your code, so the following might not be 100% accurate, but
here are my observations nevertheless.
Your data structure for the open theorems looks rather unusual, because as far as I can
see, you are storing the literal string input rather than the parsed terms and theorems.
Of course, there is no infrastructure in Isabelle to apply the morphisms to strings.
From what I know about open inductive, I can see why you store the strings, but I am
pretty sure that this will eventually get you into trouble. Ultimately, you have to parse
the strings, but the context may have changed in between -- just think of deleting a
notation and installing the same notation for some other constant. That is, you probably
get parsing with respect to dynamic contexts. because you no longer have access to the old
context. So I recomment that you immediately convert the strings into logical entities
(terms, types, theorems) and push them through the morphism as intended.
Best,
Andreas
Email Gateway (Aug 19 2022 at 17:19):From: Richard Molitor <gattschardo@googlemail.com>
Hello Andreas,
you have the correct answer! Converting these strings had been on my to-do
list, I just failed to realize that now is the moment were I need it done.
Thanks for your feedback, sometimes it takes a second pair of eyes :)
Richard
Email Gateway (Aug 19 2022 at 17:21):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Richard,
you have the correct answer! Converting these strings had been on my to-do
list, I just failed to realize that now is the moment were I need it done.
text representation of entities like terms, theorems are indeed always
parsed at the very place of their occurence in a theory text. The whole
machinery in the background then proceeds with proper internalized ML
values of type term, thm, etc.
So I would suggest to modify this accordingly and come back here for
further counsel.
Hope this helps,
Florian
Thanks for your feedback, sometimes it takes a second pair of eyes :)
Richard
On Thu, 12 Mar 2015, Andreas Lochbihler wrote:
Dear Richard,
I just glanced quickly over your code, so the following might not be
100% accurate, but here are my observations nevertheless.Your data structure for the open theorems looks rather unusual,
because as far as I can see, you are storing the literal string input
rather than the parsed terms and theorems. Of course, there is no
infrastructure in Isabelle to apply the morphisms to strings.
From what I know about open inductive, I can see why you store the
strings, but I am pretty sure that this will eventually get you into
trouble. Ultimately, you have to parse the strings, but the context
may have changed in between -- just think of deleting a notation and
installing the same notation for some other constant. That is, you
probably get parsing with respect to dynamic contexts. because you no
longer have access to the old context. So I recomment that you
immediately convert the strings into logical entities (terms, types,
theorems) and push them through the morphism as intended.Best,
AndreasOn 12/03/15 18:38, Richard Molitor wrote:
Hello again,
I managed to implement the suggested morphsim variant to some success
now,
thanks to your example!
On Thu, 12 Mar 2015, Richard Molitor wrote:
Put differently: * Your data is of a certain type T. * You explain how a fundamental morphism phi is applied to a value of
type T by giving a suitable lifting f :: morphism -> T -> T * Then your declaration for a particular x :: T looks as follows:
fun decl phi = Data.put (f phi x)Unfortunately, there is no elaborate section on this in the
implementation manual yet.I will look into this. I had seen the morphisms before, but given
the lack of
documentation, I decided to use the well-documented old-fashioned
way of doing
things. Maybe reading functor.ML will enlighten me, thanks for the
pointer!What somewhat worries me is that I end up ignoring the morphism argument
completely, since it can contain thms and terms and (I think) they do
not
affect the outcome of my commands, since they are just storing data.When I figure out which additional thms may affect my commands
though, this
way at least the infrastructure is in place in contrast to just
storing in the
background theory as I did before [1], so I think I stick with this
for now.In the last part of the linked commit, I have a local_theory_to_proof
command.
What I do now is store the result I get in after_qed using
background_theory,
I could not get declaration to work here: No matter how I produce the
initial
generic context, either from the local or the background theory, I
somehow
always end up needing the other variant in the end.Richard
[1]:
https://github.com/gattschardo/open-inductive/commit/62a4bd010e91540a00427b18c5a5656f57686591
Email Gateway (Aug 19 2022 at 17:22):From: Makarius <makarius@sketis.net>
These are very important observations. I've point out some of this
already privately.
The whole complex of "locality" in Isabelle is rather complex; it is not
easily disassembled to understand how it really works. Ultimately, it is
all about "abstract concepts" of contexts, morphisms, declarations etc.
The main strategies of survival are:
(1) Study published documents (the "implementation" manual with cited
papers) about the concepts themselves. I know that the manual is
not finished in that respect yet, but it does contain some
information, notably some references to papers by Chaieb, Haftmann,
Wenzel.
(2) Figure out the canonical way to do it, by looking closely at
existing examples. Find such examples, by asking the question
"Which existing things are close to what I need?". Then look
through the sources, and make educated guesses about their quality,
ask experts about them etc.
Often people say "I don't understand localization so I better stick with
old-fashioned global theory contexts". This only works in limited
situations, and usually turns into a much harder problem to make it work
in general: both locality and globality need to be understood, instead of
just using locality in the proper way.
Makarius
Email Gateway (Aug 22 2022 at 09:05):From: Richard Molitor <gattschardo@googlemail.com>
Hello,
I have a question concerning the usage of Generic_Data in conjunction with an
Outer_Syntax.local_theory command. The parameter to my handler function is of
type local_theory, which can be used initialize a generic context using
Context.Proof, which can then be used to store some data:
fun test_thy_cmd name =
Context.Proof #> Data.put name #> Context.proof_of
val _ = Outer_Syntax.local_theory @{command_spec "test_thy"}
"test" (Parse.name >> test_thy_cmd)
I would expect to have it stored back in the background theory when the
command completes, so using it like this:
test_thy foo
ML_val {* Data.get (Context.Theory @{theory}) *}
I would expect to get "foo" back, but i stays at the default value.
The workaround I found was wrapping the whole function in background_theory
and initializing the generic context from the theory:
fun test_prf_cmd name =
Local_Theory.background_theory (Context.Theory #> Data.put name #> Context.theory_of)
val _ = Outer_Syntax.local_theory @{command_spec "test_prf"}
"test" (Parse.name >> test_prf_cmd)
Using this:
test_prf bar
ML_val {* Data.get (Context.Theory @{theory}) *}
I get "bar" back.
Is this behaviour intended? If modify the local theory in other ways (i.e.
note theorems) the data seems to be transferred as I expect (in my first
example above).
Kind regards
Richard
P.S.: A full working example is attached
Generic.thy
Email Gateway (Aug 22 2022 at 09:07):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Richard,
my answer is twofold.
a) Your »workaround« with Local_Theory.background_theory is correct – as
long as you want to store data in background theories only. There are a
couple of applications where this indeed is feasible, but it is usually
not what you want.
b) The established pattern to store data generically is
Local_Theory.declaration (fn phi => …)
As a simple example, you might study src/HOL/Tools/functor.ML.
The idea is basically the following:
fun foo … lthy =
let
(We are relative to some local theory lthy here
and have some entities (terms t, theorems thm, …) relative
to lthy flying around as ML values here)
fun decl phi =
let
(We are called for each instance (interpretation)
of the original lthy, including lthy itself; the
logical difference is represented by morphism phi,
which we can apply (using Morphism.…) to transform our
original entities t, thm to obtain their appropriate
shape to do something with them relative
to the current instance)
in Data.put (a data record resulting from suitable) end;
in
lthy
|> Local_Theory.declaration decl
end;
Put differently:
You explain how a fundamental morphism phi is applied to a value of
type T by giving a suitable lifting f :: morphism -> T -> T
Then your declaration for a particular x :: T looks as follows:
fun decl phi = Data.put (f phi x)
Unfortunately, there is no elaborate section on this in the
implementation manual yet.
If you can tell more about the application you are aiming towards, a
more concrete description than this generic abstract nonsense can be given.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 10:58):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Richard,
as far as I discern, these are indeed the relevant patterns, although I
personally prefer to think about this without historic references like
»old way« ;-).
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 11:05):From: Richard Molitor via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Sorry for resurrecting this somewhat dated thread. It seems the same saying
that applies to PhD thesis also applies to Masters: They are never finished,
only abandoned.
The strings are now out of my implementation, (actually for several months
now) and all my usages of the global Local_Theory.background_theory are now
replaced by using generic contexts and calls to Local_Theory.declaration, as
was suggested here. ^1
Studying some other occurences in the code as suggested by Makarius I made the
following observations for "How to converted global to localized code" in this
setting:
If the command needs to store Generic_Data, Local_Theory.declaration is a
drop-in replacement for the old way (provided terms are parsed and not kept
as strings), as explained here before.
If the command transitions to the proof state and needs to store
Generic_Data afterwards, the call to Local_Theory.declaration needs to be in
the after_qed continuation function.
If the Generic_Data is not to be modified by the command, reading it can be
accomplished by instantiating a generic context explicitly e.g. using
Context.Proof ^2
I have attached a theory file that demonstrates these on a toy example. I
think that these are the appropriate solutions, but please point out any
errors if I have gone wrong somewhere. Otherwise I hope these example may be
helpful to others that want to update their older Isabelle/ML code.
Kind regards
Richard
1: https://github.com/gattschardo/open-inductive/blob/master/src/open_inductive.ML
2: $ISABELLE_HOME/src/HOL/Eisbach/method_closure.ML contains an example of
this
Generic.thy
Last updated: Apr 24 2024 at 01:07 UTC