[isabelle-dev] NEWS: Case translations as a separate check phase independent of the datatype package
huffman at in.tum.de
Wed Apr 24 16:18:13 CEST 2013
On Wed, Apr 24, 2013 at 2:52 AM, Dmitriy Traytel <traytel at in.tum.de> wrote:
> Hi Brian
> thanks for the report. Isabelle/cf039b3c42a7 resolves this in the sense that
> internal constants (like case_guard) are not visible anymore.
Thanks for taking care of this so quickly!
> However, your example is still not printed as expected (assuming that the
> output should be equal to the input in this case):
> "(case x of (a, b) => λ(c, d). e) y"
Usually "prod_case" is printed as a tuple-lambda when partially
applied, and as a case expression when fully applied. So considering
that the underlying term in my example is "prod_case (λa b. prod_case
(λc d. e)) x y", the above output makes perfect sense.
> I think, the proper resolution to this is to have an uncheck phase for
> turning "prod_case e" intro λ(x, y). e x y" before the case translation
> uncheck phase. Maybe Makarius or Stefan could comment on this. Then, I could
> have a look.
Although previous Isabelle versions had output equal to the input in
this case, it seems a bit strange for "(λ(a, b) (c, d). e)" to be
printed as a lambda if applied to 0 or 2 arguments, and as a case if
applied to 1. I'm not sure it's worth complicating the pretty printer
just to get this behavior back.
> On 24.04.2013 02:10, Brian Huffman wrote:
>> I discovered a problem with the pretty-printing of some terms (I am
>> using revision 4392eb046a97).
>> term "(λ(a, b) (c, d). e) x y"
>> "case_guard True x
>> (case_cons (case_abs (λa. case_abs (λb. case_elem (a, b) (λ(c, d).
>> :: "'e"
>> I assume this is a result of the recent changes to the handling of
>> case expressions?
>> - Brian
>> On Wed, Apr 10, 2013 at 9:16 AM, Dmitriy Traytel <traytel at in.tum.de>
>>> * Nested case expressions are now translated in a separate check
>>> phase rather than during parsing. The data for case combinators
>>> is separated from the datatype package. The declaration attribute
>>> "case_tr" can be used to register new case combinators:
>>> declare [[case_translation case_combinator constructor1 ...
>>> This refers to Isabelle/bdaa1582dc8b
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
More information about the isabelle-dev