[isabelle-dev] [isabelle] TYPE_MATCH exception with adhoc_overloading
florian.haftmann at informatik.tu-muenchen.de
Thu Nov 27 08:50:43 CET 2014
> 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
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 181 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev