The point of the code simproc is to execute terms of the form "{t|x y z. P}",
also in the interactive "values" command. These terms are not infrequent and
this is a valuable part of the code generator. I am aware that it can fail, but
it seems to work for fine in many situations, eg all of IMP. I do not want to
see it removed from Main because then
- most users will simply think that such terms are not executable and will not
be aware of the extension.
- the code generator will fail reliably, only with a "wellsortedness" error.Tobias On 14/03/2014 14:03, Dmitriy Traytel wrote: > > > Am 14.03.2014 13:36, schrieb Makarius: >> What is the status of the set_comprehension_pointfree simproc? >> >> In 31afce809794 Dmitriy says "set_comprehension_pointfree simproc causes to >> many surprises if enabled by default", and in 4d899933a51a I've tried to >> reconstruct the missing NEWS entry, since this is cleary a user-relevant >> change. >> >> Looking around in the sources and the history, e.g. 9979d64b8016 where Lukas >> Bulwahn is "moving simproc from Finite_Set to more appropriate Product_Type >> theory" shows that there is a related >> Set_Comprehension_Pointfree.code_simproc >> still present today >> http://isabelle.in.tum.de/repos/isabelle/annotate/9979d64b8016/src/HOL/Product_Type.thy#l1127 >> > > When working towards 31afce809794, I also tried deactivating this code > preprocessor, but it was used in some places outside of HOL-Main for code > generation (e.g. in HOL-IMP). >> >> Does anybody understand how the tool was initially intended to work? Is it >> feasible to move it just in one place? Lets say >> src/HOL/Library/Set_Comprehension_Pointfree.thy, so that the applications >> that >> need it can import just that theory, and main HOL remains clear. > Yes, that's a good idea. The is one usage of the simproc in HOL > (Relation.thy), > but this should be easy to get rid of. > > Dmitriy > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
