On 11/07/2014 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.
Thank you for that. Tobias > 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