src/Tools/nbe.ML
2014-01-01 haftmann 2014-01-01 explicit distinction between empty code equations and no code equations, including convenient declaration attributes
2013-07-04 haftmann 2013-07-04 explicit hint for domain of class parameters in instance statements
2013-06-28 haftmann 2013-06-28 formally accept dictionary parameters for constants on left hand sides in equations
2013-06-28 haftmann 2013-06-28 do not choke on type variables emerging during rewriting
2013-04-10 wenzelm 2013-04-10 more standard module name Axclass (according to file name);
2012-06-05 haftmann 2012-06-05 prefer records with speaking labels over deeply nested tuples
2012-04-19 haftmann 2012-04-19 dropped dead code
2012-04-19 haftmann 2012-04-19 corrected Nbe.static_value: ignore cached compilations; tuned
2012-04-19 haftmann 2012-04-19 tuned heading
2011-09-07 bulwahn 2011-09-07 adding the body type as well to the code generation for constants as it is required for type annotations of constants
2011-09-07 bulwahn 2011-09-07 changing const type to pass along if typing annotations are necessary for disambigous terms
2011-08-20 wenzelm 2011-08-20 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
2011-07-01 wenzelm 2011-07-01 proper @{binding} antiquotations (relevant for formal references);
2011-06-09 wenzelm 2011-06-09 tuned signature: Name.invent and Name.invent_names;
2011-06-09 wenzelm 2011-06-09 prefer new-style Name.invents;
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-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-01-08 wenzelm 2011-01-08 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
2010-12-21 haftmann 2010-12-21 canonical handling of theory context argument
2010-12-17 haftmann 2010-12-17 avoid slightly odd Conv.tap_thy
2010-12-15 haftmann 2010-12-15 simplified evaluation function names
2010-12-13 haftmann 2010-12-13 separated dictionary weakning into separate type
2010-12-09 haftmann 2010-12-09 dictionary constants must permit explicit weakening of classes; tuned names
2010-12-07 haftmann 2010-12-07 tuned whitespace
2010-12-07 haftmann 2010-12-07 removed experimental equality checking of closures; acknowledge underapproximation of equality in function name
2010-11-26 haftmann 2010-11-26 nbe decides equality of abstractions by extensionality
2010-11-16 haftmann 2010-11-16 added forall2 predicate lifter
2010-11-04 haftmann 2010-11-04 Code.check_const etc.: reject too specific types
2010-10-01 haftmann 2010-10-01 moved ML_Context.value to Code_Runtime
2010-09-21 haftmann 2010-09-21 no_frees_* is subsumed by new framework mechanisms in Code_Preproc
2010-09-16 haftmann 2010-09-16 separation of static and dynamic thy context
2010-09-16 haftmann 2010-09-16 tuned whitespace
2010-09-15 haftmann 2010-09-15 static nbe conversion
2010-09-15 haftmann 2010-09-15 dropped redundant normal_form command
2010-09-15 haftmann 2010-09-15 more clear separation of static compilation and dynamic evaluation
2010-09-15 haftmann 2010-09-15 replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
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 eliminated aliases of Type.constraint;
2010-09-05 wenzelm 2010-09-05 turned show_sorts/show_types into proper configuration options;
2010-08-31 haftmann 2010-08-31 evaluate takes ml context and ml expression parameter
2010-08-24 haftmann 2010-08-24 tuned
2010-08-23 haftmann 2010-08-23 use conv alias
2010-08-23 haftmann 2010-08-23 refined and unified naming convention for dynamic code evaluation techniques
2010-06-17 haftmann 2010-06-17 more precise code
2010-06-17 haftmann 2010-06-17 transitive superclasses were also only a misunderstanding
2010-06-17 haftmann 2010-06-17 formal introduction of transitive superclasses
2010-06-17 haftmann 2010-06-17 dropped obscure type argument weakening mapping -- was only a misunderstanding
2010-06-15 haftmann 2010-06-15 added code_simp infrastructure
2010-06-15 haftmann 2010-06-15 formal introduction of case cong
2010-06-07 haftmann 2010-06-07 more consistent naming aroud type classes and instances
2010-05-27 wenzelm 2010-05-27 renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-27 wenzelm 2010-05-27 renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-19 haftmann 2010-05-19 new version of triv_of_class machinery without legacy_unconstrain
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-05-09 wenzelm 2010-05-09 reactivated Thm.legacy_unconstrainT for Nbe.lift_triv_classes_conv;
2010-05-09 wenzelm 2010-05-09 just one version of Thm.unconstrainT, which affects all variables; temporary workaround for Nbe.lift_triv_classes_conv;
2010-05-03 wenzelm 2010-05-03 renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-02 haftmann 2010-03-02 dropped superfluous naming