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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
