[isabelle-dev] Let and tuple case expressions

[Florian Haftmann]

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.

Thanks a lot for any suggestion,
	Florian

-- 

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://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20150827/337b5cc4/attachment.asc>