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

[Dmitriy Traytel]

Hi Brian

thanks for the report. Isabelle/cf039b3c42a7 resolves this in the sense 
that internal constants (like case_guard) are not visible anymore.

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"

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

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