[isabelle-dev] set_comprehension_pointfree simproc

[Tobias Nipkow]

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
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev