Re: [isabelle] Storing Generic_Data in a local theory

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 =
    (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 =
        (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;
    |> Local_Theory.declaration decl

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,

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" ( >> 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" ( >> 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:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.