Hi Brian, this is indeed somehow complicated.
Almost everything in the new shallow syntax translation and in the new check phase destructs and constructs the function type. An example is the print translation case_tr' in "~/src/HOL/Tools/case_translation.ML" which relies on Sign.add_advanced_trfuns to destruct the functional arguments to the syntactic constant "case_guard".
I see two possible solutions:1) Code duplication with appropriate handling of Rep_cfun and Abs_cfun (parameterizing everything with functions like strip_comb/dest_comb is not feasable IMO). 2) Shallow syntactic translation of constants over continuous functions into unspecified (syntactic) constants over functions, which is reverted in a check phase after being processed by the case translation phase. The attached theory shows how this could look like (the check phase is really ad-hoc there, one would need to know precisely what functions are supposed to be converted back to continuous functions).
However, both alternatives seem not to be very clean. Dmitriy On 16.04.2013 01:46, Brian Huffman wrote:
It would be nice to get HOLCF case combinators working with this new system, as the parsing for HOLCF case expressions has been a bit broken for some time. Can case combinators and constructor functions with continuous-function types be made to work with the "case_tr" (or "case_translation"?) attribute? Even if we need a separate HOLCF-specific attribute, might it be possible to get HOLCF case expressions to work with the new translation check phase? - Brian On Wed, Apr 10, 2013 at 9:16 AM, Dmitriy Traytel <tray...@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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Case_HOLCF.thy
Description: application/isabelle-theory
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
