Re: [isabelle] Generic Contexts and Generic Data

Maybe the real question is: How do I turn the free variables in "consts" below, into proper constants?

  val ((cs, c_simps), lthy') =
    BNF_LFP_Rec_Sugar.add_primrec bindings equations lthy

As a more concrete example take:

local_setup {* fn lthy =>
  val cs = [Free ("c", @{typ "'a list => 'a list => 'a list"})]
  val equations = [
    @{prop "c ([]::'a list) (ys::'a list) = ([]::'a list)"}]
val bindings = map ((fn (name,ty) => ( name, SOME ty, NoSyn)) o dest_Free) cs;
  val equations' = map (pair Attrib.empty_binding) equations;
  val ((cs, c_simps), lthy') =
    BNF_LFP_Rec_Sugar.add_primrec bindings equations' lthy;
  val _ = @{print} (cs, c_simps)

Where the @{print} shows "c" as "Free". What is the proper way of turning this into a "Const"?



On 11/11/2014 04:04 PM, Christian Sternagel wrote:
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 = (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).



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