[isabelle-dev] Two simple beginners question

[Lukas Bulwahn]

Hello Rene,

On 12/02/2011 03:04 PM, René Thiemann wrote:
> Dear all,
>
> I'm currently trying to develop a package for automatic generation of linear orders for datatypes.
> I have already defined some functions which generate the corresponding equations which encode the linear order.
>
> Now the first question I have is how to store these functions:
> - when registering the equations via the function package (Function.add_function) I essentially have
>    a local theory transformer of type "lthy ->  lthy"
> - afterwards, I would like to store the newly created constant of the function symbol and some other data
>    in some global store so
>    that I can reuse it later in other generated orders. Here, I currently use
>    structure Ordering_Data = Theory_Data( type T = ...)
>    with the update function Ordering_Data.map (Symtab.update ...)
>    which is essentially a theory transformer of type "thy ->  thy"
> - how is it now possible to combine these transformers into one method foo, such that either
>    setup {* foo "my_datatype" *} or local_setup {* foo "my_datatype" *}
>    can both register the function via the function package, and also store all informations in
>    the Ordering_Data store.
>    To be more precise: Is there a way to convert a function (lthy ->  lthy) into a function (thy ->  thy)
>    or vice versa?
It is best practice to make your data storage local, i.e., to a 
Generic_Data functor.
Then update the generic data storage with Local_Theory.declaration.

Looking in the sources for the usage of Local_Theory.declaration should 
give you a rough pattern, how to employ this function.

> The second is a rather simple ML question:
> - Is it possible to conveniently update single fields in a record as in OCaml?
>    E.g., val r1 = {a = 5, b = "foo", c = ..} and many fields
>          val r2 = '' r1 where only b is changed to "bar" ''
>               (in OCaml: val r2 = {r1 with b = "bar"})

To my knowledge, there is no convenient update functions for record in 
ML provided automatically.
Therefore, many developers just define the ones of interest with some 
boiler-plate code.


Lukas