src/Pure/type_infer.ML
2011-06-09 wenzelm 2011-06-09 tuned signature: Name.invent and Name.invent_names;
2011-04-19 wenzelm 2011-04-19 split Type_Infer into early and late part, after Proof_Context; added Type_Infer_Context.const_sorts option, which allows NBE to use regular Syntax.check_term;
2011-04-19 wenzelm 2011-04-19 more precise treatment of existing type inference parameters; tuned;
2011-04-18 wenzelm 2011-04-18 tuned;
2011-04-18 wenzelm 2011-04-18 simplified pretty printing context, which is only required for certain kernel operations; disentangled dependencies of structure Pretty;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
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;