[isabelle-dev] List Comprehension

[Tobias Nipkow]

Am 06/08/2012 04:33, schrieb Christian Sternagel:
> Dear all,
> 
> I was wondering about the reasons for implementing list comprehension as is:
> 
> Why is an optimized translation desirable at all? Isn't that just a matter of
> installing appropriate simplification rules afterwards.

Why is it desirable to require simplification in such trivial cases? Isn't it
just a matter installing appropriate translation functions or rules?

Frankly I don't see that one method is superior to the other. If it can all be
done with simp rules, and those rules don't have unpleasant global effects,
sure, you can do it that way.

> The optimizations I could identify are:
> 
> 1) If in "[e . p <- xs, ...]", p is just a variable, then use "(%p. e)" (instead
> of the default "(%x. case x of p => [e] | _ => [])".
>
> I guess the reason for
> handling this case in a special way is that something like
> 
>   term "(case x of y => a | z => b)"
> 
> results in
> 
>   Error in case expression:
>   The following clauses are redundant (covered by preceding clauses):
>   z => b
> 
> But why? Wouldn't it be less surprising (meaning, less special cases), if we
> could add redundant cases without obtaining an error?

This is a question about case translations. I agree fully with their behaviour.
See my recent support for the changed behavour of fun-definitions which brought
them in line with case: such redundancy should not be accepted because it can
confuse other readers no end. [If one could distinguish user input from
machine-generated text reliably, one could try and treat them differently.]

> 2) Again, if p is a variable, translate "[e. p <- xs]" into "map (%p. e) xs"
> (instead of "concat (map (%x. case x of p => [e] | _ => []) xs)"). Isn't this
> optimization completely irrelevant inside the logic? What about applying it
> later by an appropriate simp rule or code equation?
> 
> Considering the above, why not implement list comprehension by the "easy"
> translations that are present as comment in List.thy and just use a parse
> translation for the hard case (i.e., generating "(%x. case x of p => [e] | _ =>
> [])")?

That may actually work. Try it out.

Tobias

> Thanks for any comments.
> 
> cheers
> 
> chris
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev