[isabelle] Generic Contexts and Generic Data



Dear experts,

what is the canonical way of turning a function

  add ::  key => value => Context.generic => Context.generic

into a function of type "key => value => local_theory => local_theory"?

Btw: The reason for the type of "add" is that it is the add-function for some generic data (i.e., something of the form "structure Data = Generic_Data (...)"). More specifically I have

  add key value = Data.map (Symtab.update_new (key, value))

Until now I used "Local_Theory.declaration" (and applied the obtained morphism to all elements of my "value", which happen to be terms or theorems). Although I have to admit that I'm clueless about the meaning of the "syntax" and "pervasive" flags of "Local_Theory.declaration" (so I just used "false" for both).

Doing the above I obtain the function:

  add' key value =
    Local_Theory.declaration {syntax=false,pervasive=false} (fn phi =>
      add x (apply phi value)

which is itself of type "key => value => local_theory => local_theory".

The reason why I'm asking is that I recently found out that my "add" function is actually called 3 times every time "add'" is called and the morphism applied to "value" seems to be different the last time (i.e., constants, generated via "BNF_LFP_Rec_Sugar.add_primrec" that are "Const"s as expected the first 2 times, are "Free"s the 3rd time).

cheers

chris




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