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

[Dmitriy Traytel]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: Case_HOLCF.thy
Type: application/isabelle-theory
Size: 1884 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130416/d3686b18/attachment-0002.bin>