In 51aa30c9ee4e, I have added lattice instances for the Enum.finite_* types. As expected,
this suffices for the quickcheck examples in Quickcheck_Lattice_Examples (see 9225b2761126).
This now raises the question what we should do with HOL/Library/Quickcheck_Types. Within
the Isabelle distribution and the AFP, this theory is no longer used anywhere. I expect
that almost nobody relies on the quickcheck setup in there. From the quickcheck point of
view, we can therefore drop this theory. Anyone who needs it can keep their own local copy.
However, the constructions might still be useful, as the following comment from Peter
Lammich's AFP entry Refine_Monadic shows.
(* TODO: Library/Quickcheck_Types.thy:flat_complete_lattice provides
an isomorphic contruction. *)
So, should we keep Quickcheck_Types (maybe under a different name, say
Lattice_Constructions) or drop it?
Andreas
On 11/07/14 15:54, Andreas Lochbihler wrote:
Quickcheck does not use these types, because it is currently configures to only
use the
types finite_1 to finite_3 from Enum, because the finite_types parameter is set
by
default. Quickcheck internally also seems to work differently depending on
whether the
finite_types flag is set.
I have only little insight how the parameters affect the performance of
quickcheck, but I
remember that Quickcheck originally used int as a replacement. Quickcheck_Types
clearly is
from that time. However, int is an infinite type and therefore, quantifiers, set
comprehensions and function equality are not executable. Later, he switched to
the
finite_X types, which instantiate enum, but not the other type classes.
Therefore, I recommend the following:
1. Temporarily fix Quickcheck_Types such that it works again, but leave it in
HOL/Library.
Then, anyone who wants to use quickcheck with infinite types can do so. This
way, the
Quickcheck_Examples session can also be reactivated.
2. Instead of moving Quickcheck_Types to Main, it suffices to make the finite_X
types
instances of the lattice type class hierarchy. Probably most of the stuff in
Quickcheck_Types can be adapted to work with the Enum types as well. Maybe even
all the
test cases in Quickcheck_Lattice_Examples work with the Enum types, too.
I have already done step 1 in 36041934e429 and 8840fa17e17c, but I won't have
time for
step 2 before the fork of the release branch.
Andreas
On 11/07/14 14:28, Tobias Nipkow wrote:
On 11/07/2014 13:43, Andreas Lochbihler wrote:
Quickcheck_Types defines a number of artificial types that quickcheck can use to
instantiate type variables that occur in a theorem. Normally, quickcheck
instantiates them with int provided that the sort constraints do not prevent
this. In Enum.thy, there are already the types finite_X that quickcheck uses for
enumerable types (type class enum) such that quantifiers can be unfolded into
conjunctions or disjunctions.
The types in Quickcheck_Types now do the same for the lattices type class
hierarchy, because int and the finite_X types cannot be used for type variables
with sort lattice (or top/bot/...).
I believe that it should be fairly simple to adjust Quickcheck_Types to
Isabelle2014. However, this only makes sense if it becomes part of Main.
Otherwise, it will remain just a library theory that hardly anyone knows about
and no one uses.
Moreover, we should make sure that Quickcheck_Types fits to the current code
generator setup for lattices. IIRC, Florian has reworked a lot there over the
past years. At the very least, we should have some test cases (e.g. in HOL/ex)
to check that Quickcheck_Types works as expected.
If there's consensus on reviving this theory, I can do the changes to
Quickcheck_Types such that Isabelle2014 digests it. This is probably all that
can be done before the release as most of us will be busy in Vienna next week. A
move to Main is something for the next release.
It looks mildly useful. But then Qickcheck would need to use it, which it
currently obviously does not. If you (or somebody) is able to make that happen,
then I am in favour of reviving that theory.
Tobias
Andreas
On 11/07/14 13:22, Lawrence Paulson wrote:
I’m afraid that I don’t even know what it is.
Larry
On 11 Jul 2014, at 12:21, Florian Haftmann
<florian.haftm...@informatik.tu-muenchen.de> wrote:
The issue that src/HOL/Library/Quickcheck_Types.thy is dead and broken
has not been addressed since before the last release.
So, which path to follow? Is there any interested in a serious repair
effort? Otherwise, we should honestly drop it.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
