src/Tools/nbe.ML
21 months ago wenzelm 2017-12-06 prefer control symbol antiquotations;
2016-05-26 haftmann 2016-05-26 optional timing for code generator conversions
2016-05-26 haftmann 2016-05-26 tuned
2016-05-26 haftmann 2016-05-26 explicit quasi-global context for nbe conversions -- works around quasi-global type variable handling in lift_triv_classes_conv
2016-05-26 haftmann 2016-05-26 clarified naming conventions and code for code evaluation sandwiches
2016-05-26 haftmann 2016-05-26 clarified names of variants
2016-04-12 wenzelm 2016-04-12 Type_Infer.object_logic controls improvement of type inference result;
2016-03-08 haftmann 2016-03-08 explicit record values for dictionary variables
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2015-09-02 wenzelm 2015-09-02 trim context for persistent storage;
2015-07-05 wenzelm 2015-07-05 simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
2015-05-31 wenzelm 2015-05-31 clarified context;
2015-03-06 wenzelm 2015-03-06 clarified context;
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