*To*: Richard Molitor <gattschardo at googlemail.com>, isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Storing Generic_Data in a local theory*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Thu, 12 Mar 2015 12:25:31 +0100*In-reply-to*: <alpine.LNX.2.03.1503071953420.13118@localdomain.local>*Organization*: TU Munich*References*: <alpine.LNX.2.03.1503071953420.13118@localdomain.local>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:31.0) Gecko/20100101 Thunderbird/31.5.0

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: * 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. 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 Am 07.03.2015 um 19:54 schrieb Richard Molitor: > 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 -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Storing Generic_Data in a local theory***From:*Richard Molitor

**References**:**[isabelle] Storing Generic_Data in a local theory***From:*Richard Molitor

- Previous by Date: Re: [isabelle] Weakest precondition of WHILE as a least fixed point
- Next by Date: Re: [isabelle] Weakest precondition of WHILE as a least fixed point
- Previous by Thread: [isabelle] Storing Generic_Data in a local theory
- Next by Thread: Re: [isabelle] Storing Generic_Data in a local theory
- Cl-isabelle-users March 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list