src/Tools/Code/code_thingol.ML
2011-09-20 bulwahn 2011-09-20 syntactic improvements and tuning names in the code generator due to Florian's code review
2011-09-19 bulwahn 2011-09-19 adding abstraction layer; more precise function names
2011-09-19 bulwahn 2011-09-19 adding type annotations more aggressively and redundantly to make code generation more reliable even when special printers for some constants are used
2011-09-19 bulwahn 2011-09-19 determining the fastype of a case-pattern but ignoring dummy type constructors that were added as markers for type annotations
2011-09-19 bulwahn 2011-09-19 only annotating constants with sort constraints
2011-09-19 bulwahn 2011-09-19 also adding type annotations for the dynamic invocation
2011-09-09 bulwahn 2011-09-09 stating more explicitly our expectation that these two terms have the same term structure
2011-09-09 bulwahn 2011-09-09 revisiting type annotations for Haskell: necessary type annotations are not inferred on the provided theorems but using the arguments and right hand sides, as these might differ in the case of constants with abstract code types
2011-09-07 bulwahn 2011-09-07 removing previously used function locally_monomorphic in the code generator
2011-09-07 bulwahn 2011-09-07 setting const_sorts to false in the type inference of the code generator
2011-09-07 bulwahn 2011-09-07 removing previous crude approximation to add type annotations to disambiguate types
2011-09-07 bulwahn 2011-09-07 adding minimalistic implementation for printing the type annotations
2011-09-07 bulwahn 2011-09-07 adding call to disambiguation annotations
2011-09-07 bulwahn 2011-09-07 adding type inference for disambiguation annotations in code equation
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-06-09 wenzelm 2011-06-09 tuned signature: Name.invent and Name.invent_names;
2011-06-09 wenzelm 2011-06-09 simplified Name.variant -- discontinued builtin fold_map;
2011-05-30 bulwahn 2011-05-30 improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
2011-04-18 wenzelm 2011-04-18 simplified Sorts.class_error: plain Proof.context; 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-16 wenzelm 2011-04-16 prefer local name spaces; tuned signatures; tuned;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-02-17 haftmann 2011-02-17 added is_IAbs; tuned brackets and comments
2010-12-21 haftmann 2010-12-21 proper static closures
2010-12-21 haftmann 2010-12-21 canonical handling of theory context argument
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-01 wenzelm 2010-12-01 more direct use of binder_types/body_type;
2010-11-26 haftmann 2010-11-26 keep type variable arguments of datatype constructors in bookkeeping
2010-11-26 haftmann 2010-11-26 globbing constant expressions use more idiomatic underscore rather than star
2010-09-20 haftmann 2010-09-20 Pure equality is a regular cpde operation
2010-09-17 haftmann 2010-09-17 proper closures for static evaluation; no need for FIXMEs any longer
2010-09-16 haftmann 2010-09-16 separation of static and dynamic thy context
2010-09-15 haftmann 2010-09-15 ignore code cache optionally
2010-09-07 haftmann 2010-09-07 dropped outdated substitution
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-23 haftmann 2010-08-23 preliminary versions of static_eval_conv(_simple)
2010-08-23 haftmann 2010-08-23 refined and unified naming convention for dynamic code evaluation techniques
2010-07-21 wenzelm 2010-07-21 replaced Thy_Info.the_theory by Context.this_theory -- avoid referring to accidental theory loader state;
2010-07-16 haftmann 2010-07-16 don't fail gracefully
2010-07-08 haftmann 2010-07-08 tuned titles
2010-07-05 haftmann 2010-07-05 dropped passed irregular names
2010-07-02 haftmann 2010-07-02 reverted to verion from fc27be4c6b1c
2010-07-02 haftmann 2010-07-02 traceback for error messages
2010-06-30 haftmann 2010-06-30 unfold_fun_n
2010-06-17 haftmann 2010-06-17 explicit type variable arguments for constructors
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 maintain cong rules for case combinators; more precise permissiveness
2010-06-15 haftmann 2010-06-15 formal introduction of case cong
2010-06-14 haftmann 2010-06-14 teaked naming of superclass projections
2010-06-07 haftmann 2010-06-07 more consistent naming aroud type classes and instances
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
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-04-21 haftmann 2010-04-21 optionally ignore errors during translation of equations; tuned representation of abstraction points