[isabelle-dev] Let and tuple case expressions

[Dmitriy Traytel]

Hi Florian,

On 27.08.2015 10:03, Florian Haftmann wrote:
> Hi Dmitriy,
>
>> In short, I have come to the conclusion that
>>
>>    let (a, b) = p in t
>>
>>    case p of (a, b) => t
>>
>> at the moment being logically distinct, should be one and the same.  In
>> other words, I suggest that any case expression on tuples should be
>> printed using »let« rather than »case«.  The constant »Let« would turn
>> into a degenerate case combinator with no actual pattern match.
> I tried to change this in the expectation that tuning the syntax rules
> for Let would be sufficient, but found out that's not the case: if case
> is to be interwoven with let, the syntax machinery for let must act on
> the same syntactic layer to behave consistently (the usual observation
> when dealing with syntax).
>
> Hence, to go forward here, it is inevitable to extend the case syntax
> code itself, roughly as follows:
>
> a) Map »case x of y ⇒ f y« to »Let x f« and vice versa.
> b) Map singleton case clauses to let clauses and vice versa.
> c) Collapse/expand consecutive let clauses (let x = y in let z = w in …
> <--> let x = y; z = w in …)
>
> Since I suppose you know that code best, how feasible does this agenda
> look for you?  I guess a) has to be implemented in Isabelle/ML anyway,
> but maybe then b) and c) are simple enough to be achieved using »syntax«
> productions.
I am slightly confused by "and vice versa". Clearly you want the mapping 
to go in one direction. There are two questions: (1) what is the logical 
representation (2) what is printed.

If I understand you correctly you want the answer for both to be Let 
expressions (for case combinators of single-constructor (co)datatypes). 
Then I would say, the way to go is to implement a syntax phase for 
translating the affected case combinators into Let expressions and 
install it *after* the case syntax translation phase. Something along 
the following lines (generalized beyond the product type).


ML ‹
fun Let_of_case ctxt ts =
   let
     fun substT T =
       let
         val ((U1, (U2, U3)), (U4, U5)) = T |> dest_funT |>> (dest_funT 
##> dest_funT) ||> dest_funT;
       in
         U4 --> (HOLogic.mk_prodT (U1, U2) --> U3) --> U5
       end;

     fun subst (Const (@{const_name case_prod}, T) $ rhs $ t) =
       Const (@{const_name Let}, substT T) $ (subst t) $ 
(HOLogic.mk_split (subst rhs))
       | subst (t $ u) = subst t $ subst u
       | subst t = t
   in
     map subst ts
   end;

val _ = Context.>> (Syntax_Phases.term_check 2 "case → Let" Let_of_case)
›

This, however, does not work with (a), since today "case x of y ⇒ f y" 
is translated to "f x". But the question is anyway whether this is not 
what you want.

In contrast, if you would like to have the case combinators as the 
logical representation, the translation of Let into case probably should 
happen before the case syntax translation phase (and would be more 
complicated). Printing then would work roughly as in the code above 
(replace "check 2" with "uncheck 0").

In any case I would prefer not to extend the case syntax translation 
itself, since it is quite complicated already.

Hope that helps,
Dmitriy