[isabelle-dev] case syntax

[Makarius]

On Wed, 11 Jan 2012, Makarius wrote:

> On Wed, 11 Jan 2012, Lukas Bulwahn wrote:
>
>> I bisected the failure further on my local machine and it turns out it is 
>> related to the changeset
>> 
>> changeset:   46143:463b594e186a
>> user:        wenzelm
>> date:        Fri Jan 06 20:18:49 2012 +0100
>> summary:     refined case syntax again, improved treatment of constructors 
>> without arguments, e.g. "case a of (True, x) => x";
>
> Thanks for bisecting this.  After several isatest mails I've started to 
> suspect something like this already.
>
> There is a deeper problem with this case syntax stuff: there are two versions 
> of the code, one for terms as parse trees (in the sense of syntax 
> translations), another for regular terms with proper type information. The 
> former does certain strange operations on parsetrees, like interfering with 
> type constraints or comparing parse trees.  The latter then suffers from 
> attempts to refine this (I did not write "fix" in the log for the usual 
> reasons).
>
> I was about to start a thread about getting case syntax conceptually right 
> last week, but did not manage so far.  The basic idea is to separete the 
> syntax translation part from another check/unckeck phase to do the 
> non-trivial re-arrangements on properly typed abstract syntax.
>
> The basic motivation for my changes so far is to get the Prover IDE markup 
> right.  This is not just a matter of having variable scopes and inferred type 
> highlighted in the editor, but also a pre-requisite for the tentative plan to 
> make the "source position" status of variables more formal, say for the 
> "default types" problem that some people should know already.

For the moment it appears to be just a very superficial lapse concerning 
bound names, see now 8297006abc13.


The conceptual questions about more robust case syntax remain.  The main 
change in the recent tinkering is 00cd193a48dc.  Apart from tweaking 
case_tr/case_tr' it includes some slightly odd attempts to keep some 
old-style translations working that happen use the same 
syntactic space of _case1/_case2.

As I've discussed this with Stefan and Brian already in december.  The 
idea is to separate superficial case syntax translations from the main 
work in a suitable check/unckeck phase.  E.g. certain packages could 
provide abstract syntax (like abbreviations) for destructors, and issue a 
suitable context declaration to relate groups of them with certain case 
combinators.

The logical representation of the resulting terms would not change, only 
the concrete vs. abstract syntax (using technology from Isabelle2007/2008 
instead of stretching syntax translations a bit too far).


 	Makarius