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:[email protected]
Computational Logic Group http://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Science phone: +43 512 507-6434
University of Innsbruck
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
