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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev