On Wed, Apr 24, 2013 at 2:52 AM, Dmitriy Traytel <[email protected]> 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 <[email protected]> >> 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 >>> [email protected] >>> >>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > > _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
