[isabelle-dev] Let and tuple case expressions

[Florian Haftmann]

Hi Dmitriy,

thanks for your answer.

Let me rephrase the matter as I perceive it:

Syntactic requirement: Print and parse singleton case clauses as let
bindings.
I agree that this can (and should) be done in a separate phase.  Still
not sure whether check/uncheck is the right layer to accomplish this,
but this can still be elaborated.

But I see also that your suggestion would not need any special treatment
for simple let bindings (let x = y in t).

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

Well, in my original approach this would have been a necessity.

I'll try the check/uncheck approach.

Thanks a lot,
	Florian


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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150827/3d4c9135/attachment.sig>