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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
