[isabelle-dev] isabelle test failures

[Makarius]

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.


 	Makarius