src/Tools/nbe.ML
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 clarified signature;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-12-19 wenzelm 2014-12-19 tuned;
2014-12-19 wenzelm 2014-12-19 proper exception for internal program failure, not user-error;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-09-18 haftmann 2014-09-18 tuned data structure
2014-06-29 haftmann 2014-06-29 modernized diagnostic options
2014-06-05 haftmann 2014-06-05 be more explicit: made sml/nj happy
2014-05-15 haftmann 2014-05-15 accurate separation of static and dynamic context
2014-05-15 haftmann 2014-05-15 syntactic means to prevent accidental mixup of static and dynamic context
2014-05-15 haftmann 2014-05-15 proper separation of static and dynamic context
2014-05-15 haftmann 2014-05-15 dropped obsolete hand-waving adjustion of type variables: safely done in preprocessor
2014-05-09 haftmann 2014-05-09 degeneralized value command into HOL
2014-05-09 haftmann 2014-05-09 normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>; tuned naming; dropped dead parameters;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-02-26 haftmann 2014-02-26 prefer proof context over background theory
2014-01-29 haftmann 2014-01-29 made smlnj happy
2014-01-25 haftmann 2014-01-25 less clumsy namespace
2014-01-25 haftmann 2014-01-25 prefer explicit code symbol type over ad-hoc name mangling
2014-01-19 haftmann 2014-01-19 prefer indexes user for pattern matching to print concrete names for symbols, do not rely on printable unique identifiers
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;