On 07/21/2011 09:47 PM, Gerwin Klein wrote:
The idea has potential for generalisation. Could we turn this into
something similar to Haskell's "deriving"?
The command would take a datatype and a list of instantiation methods
that each know how to instantiate a datatype for a specific type
class, e.g. enum, countable, order, etc. An instantiation method
would be basically a usual proof method plus some small part that
knows how to set up the specific instantiation goal (probably the
same code for pretty much all applications of this) plus some
background theory that provides the basic setup.
I like this approach. You ask for something explicitly and then you get
it, but you don't have to remember a new obscure syntax for every bit of
it. You would just write
datatype foo = ....
deriving countable, finite,
Several existing things fit into this scheme: When I define a fresh
"datatype foo = Bar" in Main, it automatically becomes an instance of
the following type classes:
- equal (executable equality, for code generation)
- term_of (reifiable term structure, for code generation)
- size (size function, for termination proofs)
- full_exhaustive (for exhaustive quickcheck)
(there is actually a large zoo of type classes for quickcheck...)
This doesn't mean that we have to make every last thing explicit, but a
mechanism would make sense.
Note that in general, a proof method is not enough, since we have to
define overloaded constants. Here, countable is an exception since the
class has no parameters.
Alex
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
