[isabelle-dev] [isabelle] TYPE_MATCH exception with adhoc_overloading

[Florian Haftmann]

Hi Christian,

> I'm mostly guessing here. Maybe somebody with deeper knowledge of the
> system could comment whether this would be feasible (and also the right
> way to go).

I have not spent much thought on the code, but tried to take a bird's
perspective.

The whole matter is about overloaded abbreviations.  Hence, it's about
abbreviation expansion intermingled with type inference.

Having a look syntax_phases.ML

> (* standard phases *)
> 
> val _ = Context.>>
>  (typ_check 0 "standard" Proof_Context.standard_typ_check #>
>   term_check 0 "standard"
>     (fn ctxt => Type_Infer_Context.infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)) #>
>   term_check 100 "standard_finish" Proof_Context.standard_term_check_finish #>
>   term_uncheck 0 "standard" Proof_Context.standard_term_uncheck);

I see that type inference and abbreviation expansion occur on the same
term check level.  Hence the overloading mechanisms could go here.

Proof_Context.expand_abbrevs essentially boils down to Consts.certify.

Maybe a comparision of these with the current implementation of
adhoc-overloading can give some clues.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20141127/e7688782/attachment.sig>