[isabelle-dev] Two simple beginners question
RenĂ© Thiemann
rene.thiemann at uibk.ac.at
Fri Dec 2 15:04:44 CET 2011
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?
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"})
Best regards,
René
--
René Thiemann mailto:rene.thiemann at uibk.ac.at
Computational Logic Group http://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Science phone: +43 512 507-6434
University of Innsbruck
More information about the isabelle-dev
mailing list