src/Pure/type_infer.ML
2011-03-28 wenzelm 2011-03-28 address serious problem of type inference (introduced in 6f085332c7d3): _type_constraint_ needs type scheme A --> A with proper scope of parameters, otherwise term "(f :: _ => _) :: 'c => 'c" will get type "'a => 'b", for example;
2010-10-29 wenzelm 2010-10-29 more sharing of operations, without aliases;
2010-09-13 wenzelm 2010-09-13 tuned signature; tuned comments;
2010-09-13 wenzelm 2010-09-13 Type_Infer.finish: index 0 -- freshness supposedly via Name.invents; Type_Infer.fixate_params: full Proof.context;
2010-09-13 wenzelm 2010-09-13 simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
2010-09-12 wenzelm 2010-09-12 Type_Infer.preterm: eliminated separate Constraint;
2010-09-12 wenzelm 2010-09-12 Type_Infer.infer_types: plain error instead of kernel exception TYPE;
2010-09-12 wenzelm 2010-09-12 load type_infer.ML later -- proper context for Type_Infer.infer_types; renamed Type_Infer.polymorphicT to Type.mark_polymorphic;
2010-09-12 wenzelm 2010-09-12 common Type.appl_error, which also covers explicit constraints;
2010-09-12 wenzelm 2010-09-12 eliminated aliases of Type.constraint;
2010-09-12 wenzelm 2010-09-12 tuned;
2010-09-12 wenzelm 2010-09-12 tuned messages; tuned comments;
2010-06-01 berghofe 2010-06-01 merged
2010-06-01 berghofe 2010-06-01 assign now applies meet before update_new to avoid misleading error message.
2010-05-27 wenzelm 2010-05-27 renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-02-06 wenzelm 2010-02-06 fixed spelling;
2009-07-23 wenzelm 2009-07-23 paramify_vars: Term_Subst.map_atypsT_same recovered coding conventions of this module;
2009-07-23 berghofe 2009-07-23 Purely functional type inference.
2009-07-17 wenzelm 2009-07-17 tuned;
2009-07-14 wenzelm 2009-07-14 tuned paramify_vars: Term_Subst.map_atypsT_option;
2009-07-09 wenzelm 2009-07-09 renamed structure TermSubst to Term_Subst;
2009-02-27 wenzelm 2009-02-27 eliminated NJ's List.nth;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-06-18 wenzelm 2008-06-18 improved error output -- variant/mark bounds; simplified infer_types -- always freeze, no result substitution;
2007-10-04 wenzelm 2007-10-04 replaced literal 'a by Name.aT;
2007-09-29 wenzelm 2007-09-29 added fixate_params; type_infer: freeze_mode = NONE keeps inference parameters in result; type_infer: observe Variable.maxidx_of;
2007-09-23 wenzelm 2007-09-23 constrain: canonical argument order; removed obsolete logicT;
2007-08-31 wenzelm 2007-08-31 exported is_param;
2007-08-30 wenzelm 2007-08-30 infer_types: general check_typs instead of Type.cert_typ_mode;
2007-08-14 wenzelm 2007-08-14 infer_types: depend on Type.mode;
2007-04-23 wenzelm 2007-04-23 added paramify_vars; infer: replace params uniformly (notably freeze);
2007-04-15 wenzelm 2007-04-15 moved get_sort to sign.ML; moved decode_types to Syntax/type_ext.ML; moved mixfixT to Syntax/mixfix.ML; proper infer_types, without decode/name lookup; tuned;
2007-04-14 wenzelm 2007-04-14 tuned comment;
2007-04-14 wenzelm 2007-04-14 Term.string_of_vname;
2006-10-04 haftmann 2006-10-04 insert replacing ins ins_int ins_string
2006-09-27 wenzelm 2006-09-27 internal params: Vartab instead of AList;
2006-09-21 wenzelm 2006-09-21 tuned;
2006-07-19 wenzelm 2006-07-19 Name.context for used'';
2006-07-11 wenzelm 2006-07-11 Name.invent_list;
2006-05-05 wenzelm 2006-05-05 added syntax for _type_constraint_;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-25 wenzelm 2006-04-25 refer to structure Type instead of Sorts;
2006-02-15 wenzelm 2006-02-15 removed distinct, renamed gen_distinct to distinct;
2006-02-11 wenzelm 2006-02-11 tuned;
2006-02-10 wenzelm 2006-02-10 decode: observe Syntax.constN;
2006-02-07 wenzelm 2006-02-07 renamed gen_duplicates to duplicates;
2006-02-06 wenzelm 2006-02-06 tuned;
2005-12-02 wenzelm 2005-12-02 added mixfixT; paramify_dummies: treat dummyT as well, tuned;
2005-09-20 haftmann 2005-09-20 slight adaptions to library changes
2005-09-06 wenzelm 2005-09-06 AList.defined;
2005-09-06 haftmann 2005-09-06 introduced some new-style AList operations
2005-07-01 wenzelm 2005-07-01 avoid polyeq;
2005-06-11 wenzelm 2005-06-11 accomodate changed #classes;
2005-06-02 wenzelm 2005-06-02 tuned;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-22 wenzelm 2004-06-22 tuned certify_typ/term;
2004-06-21 wenzelm 2004-06-21 Type.cert_typ;
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic';
2004-05-29 wenzelm 2004-05-29 improved output; refer to Pretty.pp;