[isabelle-dev] Type error in metis call with Toplevel.debug

[Lawrence Paulson]

The offending code is here:

   fun fol_terms_to_hol ctxt fol_tms =
     let val ts = map (fol_term_to_hol_RAW ctxt) fol_tms
         val _ = Output.debug (fn () => "  calling type inference:")
         val _ = app (fn t => Output.debug (fn () =>  
Syntax.string_of_term ctxt t)) ts
         val ts' = infer_types ctxt ts;
         val _ = app (fn t => Output.debug
                       (fn () => "  final term: " ^  
Syntax.string_of_term ctxt t ^
                                 "  of type  " ^ Syntax.string_of_typ  
ctxt (type_of t)))
                     ts'
     in  ts'  end;

We call the function Syntax.string_of_term on a list of terms ts prior  
to type inference, so it is unsurprising that some of these terms are  
not type correct. In fact, the only surprise is that we don't get an  
error message more often. I was under the impression that that  
particular function did not perform type-checking. Is there a more  
appropriate function to call?

Larry

On 12 Jun 2009, at 12:46, Alexander Krauss wrote:

> Dear isabelle-dev,
>
> Andy Schropp found the following weird behaviour, which seems to be  
> both in Isabelle2009 and the current developer version (reproduced  
> in b63d253ed9e2).
>
> Steps to reproduce:
>
> - Starting from Pure or HOL-Plain, load List.thy in PG
> - Enable Toplevel.debug
> - The metis call in lemma "sorted_distinct_set_unique", fails with
>
> *** exception TERM raised: fastype_of: expected function type
>
> When Toplevel.debug is switched off then it works, so my guess is  
> that it is related to the pretty printing of some of the debug  
> messages, but I am not sure.
>
> Any ideas? Anybody inclined to debug this further?
>
> Alex
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev