[isabelle-dev] NEWS: Case translations as a separate check phase independent of the datatype package

[Brian Huffman]

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.
>
> Dmitriy

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.

- Brian

> 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))))
>>      case_nil)
>>    y"
>>    :: "'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>
>> wrote:
>>>
>>> * 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 ...
>>> constructorN]]
>>>
>>> This refers to Isabelle/bdaa1582dc8b
>>>
>>> Dmitriy
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>>>
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
>