[isabelle-dev] Error with case syntax?

[Makarius]

On Fri, 31 May 2013, Jasmin Christian Blanchette wrote:

> Hi all,
>
> Using Isabelle/c3f837d92537,
>
>    theory Bug imports Main begin
>
>    lemma "(case p of (a, b) => f (a, b)) = f p"
>
> raises
>
>    *** exception TERM raised (line 332 of "term.ML"): fastype_of: expected function type
>
> in Proof General and in "isabelle tty" but not in jEdit.

The error did not show up in in Isabelle/jEdit, because the (still crude) 
mechanism to print proof states asynchronously just failed without further 
notice.  (Hopefully I will managed this summer to get this all on a more 
solid foundation as "asynchronous agents framework" -- when I am back from 
my vacation in June.)


Sneaking the exception_trace combinator into Goal_Display.pretty_goals 
produces this:

Exception trace for exception - TERM raised in term.ML line 332

Case_Translation.encode_case(3)
Case_Translation.strip_case_full(3)
Case_Translation.strip_case_full(3)
Case_Translation.strip_case_full(3)
List.map(2)
Syntax_Phases.simple_check(1)(1)(1)(1)
Library.perhaps_loop(1)(1)
Library.perhaps_apply(1)(1)
Syntax_Phases.check(4)
Goal_Display.pretty_goals(2)(1)pretty_subgoal(2)
Library.map_index(1)map_aux(2)
Goal_Display.pretty_goals(2)(1)

It means that the new case translation uncheck phase by Dmitriy chokes on 
an ill-typed term.

The reason for the malformed term is the new Type_Annotation markup that I 
had put in the wrong spot -- after having explained to you privately that 
it has to be after "uncheck" and before "unparse" (it is relevant for 
Sledgehammer Isar output with type annotations).  This problem is now 
addressed in b12f2cef3ee5.

Moreover, I've made Dmitriy's uncheck function *permissive* in 
da42b500a6aa, similar to contraction of term abbreviations.  Thus it might 
have taken longer to find out about this lapse mine, but print functions 
need to be as total as feasibile, to allow certain error situations to be 
reported to the user, even if they contain malformed terms.


 	Makarius