[isabelle-dev] List Comprehension
c-sterna at jaist.ac.jp
Mon Aug 6 04:33:46 CEST 2012
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.
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)"
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?
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] | _ => )")?
Thanks for any comments.
More information about the isabelle-dev