| Thu, 13 Apr 2017 10:10:12 +0200 |
haftmann |
for generated Haskell code, never use let-binds with pattern matching: irrefutable patterns destroy partial correctness
|
file |
diff |
annotate
|
| Thu, 26 Jan 2017 16:06:19 +0100 |
haftmann |
tuned structure and terminology
|
file |
diff |
annotate
|
| Tue, 14 Jun 2016 20:48:41 +0200 |
haftmann |
explicit resolution of ambiguous dictionaries
|
file |
diff |
annotate
|
| Sun, 29 May 2016 14:43:18 +0200 |
haftmann |
explicit check that abstract constructors cannot be part of official interface
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
optional timing for code generator conversions
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
corrected closure scope of static_conv_thingol;
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
clarified proof context vs. background theory
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
clarified naming conventions and code for code evaluation sandwiches
|
file |
diff |
annotate
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
clarified names of variants
|
file |
diff |
annotate
|
| Mon, 09 May 2016 14:37:47 +0200 |
wenzelm |
clarified context, notably for internal use of Simplifier;
|
file |
diff |
annotate
|
| Tue, 08 Mar 2016 21:07:48 +0100 |
haftmann |
explicit record values for dictionary variables
|
file |
diff |
annotate
|
| Tue, 08 Mar 2016 21:07:47 +0100 |
haftmann |
provide explicit hint concering uniqueness of derivation
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 19:13:47 +0200 |
wenzelm |
tuned signature: eliminated pointless type Context.pretty;
|
file |
diff |
annotate
|
| Thu, 09 Jul 2015 00:39:49 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Mon, 27 Apr 2015 16:46:52 +0200 |
wenzelm |
code equations as displayable content in code dependency graph
|
file |
diff |
annotate
|
| Mon, 27 Apr 2015 15:53:11 +0200 |
wenzelm |
filtering of reflexive dependencies avoids problems with state-of-the-art graph browser;
|
file |
diff |
annotate
|
| Thu, 16 Apr 2015 15:22:44 +0200 |
wenzelm |
discontinued pointless warnings: commands are only defined inside a theory context;
|
file |
diff |
annotate
|
| Thu, 16 Apr 2015 11:22:36 +0200 |
wenzelm |
let the system choose Graph_Display.display_graph_old: thm_deps needs tree hierarchy, code_deps needs cycles (!?);
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Tue, 24 Mar 2015 11:53:18 +0100 |
wenzelm |
clarified input source;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 23:52:14 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Sun, 15 Feb 2015 08:17:46 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sun, 15 Feb 2015 08:17:44 +0100 |
haftmann |
purge variables not mentioned in body from pattern
|
file |
diff |
annotate
|
| Sat, 14 Feb 2015 19:57:26 +0100 |
haftmann |
only collapse patterns with disjunctive variable names
|
file |
diff |
annotate
|
| Sat, 14 Feb 2015 19:57:24 +0100 |
haftmann |
clarified
|
file |
diff |
annotate
|
| Wed, 31 Dec 2014 20:42:45 +0100 |
wenzelm |
clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names);
|
file |
diff |
annotate
|
| Wed, 31 Dec 2014 14:15:52 +0100 |
wenzelm |
for graph display, prefer graph data structure over list with dependencies;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2014 14:13:11 +0100 |
wenzelm |
more explict and generic field names
|
file |
diff |
annotate
|
| Wed, 31 Dec 2014 14:08:50 +0100 |
wenzelm |
uniform variable name for presentation graphs, to distinguish from values of type Graph.T
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Mon, 03 Nov 2014 14:50:27 +0100 |
wenzelm |
eliminated unused int_only flag (see also c12484a27367);
|
file |
diff |
annotate
|
| Thu, 18 Sep 2014 18:48:04 +0200 |
haftmann |
tuned data structure
|
file |
diff |
annotate
|
| Thu, 15 May 2014 16:38:31 +0200 |
haftmann |
syntactic means to prevent accidental mixup of static and dynamic context
|
file |
diff |
annotate
|
| Thu, 15 May 2014 16:38:29 +0200 |
haftmann |
dropped obsolete hand-waving adjustion of type variables: safely done in preprocessor
|
file |
diff |
annotate
|
| Fri, 09 May 2014 08:13:26 +0200 |
haftmann |
normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>;
|
file |
diff |
annotate
|
| Thu, 01 May 2014 09:30:35 +0200 |
haftmann |
optional case enforcement
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 11:42:32 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Wed, 12 Mar 2014 14:37:14 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 13:55:03 +0100 |
wenzelm |
abstract type Name_Space.table;
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 22:46:31 +0100 |
wenzelm |
clarified language markup: added "delimited" property;
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 11:57:52 +0100 |
haftmann |
prefer proof context over background theory
|
file |
diff |
annotate
|
| Thu, 30 Jan 2014 16:30:01 +0100 |
haftmann |
dependency reporting for code generation errors
|
file |
diff |
annotate
|
| Thu, 30 Jan 2014 16:30:00 +0100 |
haftmann |
more abstract dictionary construction
|
file |
diff |
annotate
|
| Thu, 30 Jan 2014 16:09:04 +0100 |
haftmann |
reduced prominence of "permissive code generation"
|
file |
diff |
annotate
|
| Sat, 25 Jan 2014 23:50:49 +0100 |
haftmann |
less clumsy namespace
|
file |
diff |
annotate
|
| Sat, 25 Jan 2014 23:50:49 +0100 |
haftmann |
prefer explicit code symbol type over ad-hoc name mangling
|
file |
diff |
annotate
|
| Mon, 06 Jan 2014 09:31:19 +0100 |
haftmann |
special treatment of ==> and == solely as constants
|
file |
diff |
annotate
|
| Mon, 06 Jan 2014 09:31:18 +0100 |
haftmann |
uniform orientation of instances as (type constructor, type class)
|
file |
diff |
annotate
|
| Wed, 01 Jan 2014 01:05:46 +0100 |
haftmann |
explicit distinction between empty code equations and no code equations, including convenient declaration attributes
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 22:31:34 +0200 |
wenzelm |
proper PIDE markup for codegen arguments;
|
file |
diff |
annotate
|
| Thu, 04 Jul 2013 08:52:44 +0200 |
haftmann |
explicit hint for domain of class parameters in instance statements
|
file |
diff |
annotate
|
| Sun, 26 May 2013 21:05:03 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 24 May 2013 23:57:24 +0200 |
haftmann |
bookkeeping and input syntax for exact specification of names of symbols in generated code
|
file |
diff |
annotate
|
| Wed, 10 Apr 2013 15:30:19 +0200 |
wenzelm |
more standard module name Axclass (according to file name);
|
file |
diff |
annotate
|
| Tue, 09 Apr 2013 15:29:25 +0200 |
wenzelm |
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
|
file |
diff |
annotate
|
| Thu, 27 Dec 2012 21:01:08 +0100 |
haftmann |
more explicit name
|
file |
diff |
annotate
|
| Tue, 25 Sep 2012 15:40:41 +0200 |
wenzelm |
separate module Graph_Display;
|
file |
diff |
annotate
|
| Tue, 05 Jun 2012 07:11:49 +0200 |
haftmann |
clarified code translation code
|
file |
diff |
annotate
|
| Tue, 05 Jun 2012 07:05:56 +0200 |
haftmann |
prefer records with speaking labels over deeply nested tuples
|
file |
diff |
annotate
|
| Mon, 28 May 2012 13:38:07 +0200 |
haftmann |
dropped sort constraints on datatype specifications
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 10:16:51 +0200 |
haftmann |
dropped dead code;
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 09:58:54 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 21:47:26 +0200 |
haftmann |
tuned name
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 21:11:50 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 10:29:45 +0200 |
Andreas Lochbihler |
generalise case certificates to allow ignored parameters
|
file |
diff |
annotate
|
| Sun, 18 Mar 2012 13:04:22 +0100 |
wenzelm |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 18:20:12 +0100 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
| Sat, 25 Feb 2012 12:34:56 +0100 |
wenzelm |
discontinued slightly odd Graph.del_nodes (inefficient due to full Table.map);
|
file |
diff |
annotate
|
| Thu, 23 Feb 2012 15:49:40 +0100 |
wenzelm |
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
|
file |
diff |
annotate
|
| Mon, 26 Dec 2011 18:32:43 +0100 |
haftmann |
dropped disfruitful `constant signatures`
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 09:11:18 +0200 |
bulwahn |
removing dependency of the generic code generator to old code generator functions thyname_of_type and thyname_of_const
|
file |
diff |
annotate
|
| Wed, 12 Oct 2011 16:21:07 +0200 |
wenzelm |
discontinued obsolete alias structure ProofContext;
|
file |
diff |
annotate
|
| Tue, 20 Sep 2011 09:30:19 +0200 |
bulwahn |
syntactic improvements and tuning names in the code generator due to Florian's code review
|
file |
diff |
annotate
|
| Mon, 19 Sep 2011 16:18:23 +0200 |
bulwahn |
adding abstraction layer; more precise function names
|
file |
diff |
annotate
|
| Mon, 19 Sep 2011 16:18:21 +0200 |
bulwahn |
adding type annotations more aggressively and redundantly to make code generation more reliable even when special printers for some constants are used
|
file |
diff |
annotate
|
| Mon, 19 Sep 2011 16:18:19 +0200 |
bulwahn |
determining the fastype of a case-pattern but ignoring dummy type constructors that were added as markers for type annotations
|
file |
diff |
annotate
|
| Mon, 19 Sep 2011 16:18:19 +0200 |
bulwahn |
only annotating constants with sort constraints
|
file |
diff |
annotate
|
| Mon, 19 Sep 2011 16:18:18 +0200 |
bulwahn |
also adding type annotations for the dynamic invocation
|
file |
diff |
annotate
|
| Fri, 09 Sep 2011 14:43:50 +0200 |
bulwahn |
stating more explicitly our expectation that these two terms have the same term structure
|
file |
diff |
annotate
|
| Fri, 09 Sep 2011 12:33:09 +0200 |
bulwahn |
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
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:51:39 +0200 |
bulwahn |
removing previously used function locally_monomorphic in the code generator
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:51:38 +0200 |
bulwahn |
setting const_sorts to false in the type inference of the code generator
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:51:36 +0200 |
bulwahn |
removing previous crude approximation to add type annotations to disambiguate types
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:51:35 +0200 |
bulwahn |
adding minimalistic implementation for printing the type annotations
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:51:34 +0200 |
bulwahn |
adding call to disambiguation annotations
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:51:34 +0200 |
bulwahn |
adding type inference for disambiguation annotations in code equation
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:51:32 +0200 |
bulwahn |
adding the body type as well to the code generation for constants as it is required for type annotations of constants
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 13:51:30 +0200 |
bulwahn |
changing const type to pass along if typing annotations are necessary for disambigous terms
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 23:35:30 +0200 |
wenzelm |
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 20:22:22 +0200 |
wenzelm |
tuned signature: Name.invent and Name.invent_names;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 17:51:49 +0200 |
wenzelm |
simplified Name.variant -- discontinued builtin fold_map;
|
file |
diff |
annotate
|
| Mon, 30 May 2011 13:58:00 +0200 |
bulwahn |
improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 12:04:21 +0200 |
wenzelm |
simplified Sorts.class_error: plain Proof.context;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 11:13:29 +0200 |
wenzelm |
simplified pretty printing context, which is only required for certain kernel operations;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:25:25 +0200 |
wenzelm |
prefer local name spaces;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 13:31:16 +0200 |
wenzelm |
explicit structure Syntax_Trans;
|
file |
diff |
annotate
|
| Thu, 17 Feb 2011 09:31:29 +0100 |
haftmann |
added is_IAbs; tuned brackets and comments
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 15:15:55 +0100 |
haftmann |
proper static closures
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 09:18:29 +0100 |
haftmann |
canonical handling of theory context argument
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 09:47:12 +0100 |
haftmann |
simplified evaluation function names
|
file |
diff |
annotate
|
| Mon, 13 Dec 2010 22:54:47 +0100 |
haftmann |
separated dictionary weakning into separate type
|
file |
diff |
annotate
|
| Thu, 09 Dec 2010 17:25:43 +0100 |
haftmann |
dictionary constants must permit explicit weakening of classes;
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 15:03:44 +0100 |
wenzelm |
more direct use of binder_types/body_type;
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 22:33:21 +0100 |
haftmann |
keep type variable arguments of datatype constructors in bookkeeping
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 12:03:18 +0100 |
haftmann |
globbing constant expressions use more idiomatic underscore rather than star
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 18:43:18 +0200 |
haftmann |
Pure equality is a regular cpde operation
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 11:05:53 +0200 |
haftmann |
proper closures for static evaluation; no need for FIXMEs any longer
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 16:51:34 +0200 |
haftmann |
separation of static and dynamic thy context
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 15:11:39 +0200 |
haftmann |
ignore code cache optionally
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 16:05:20 +0200 |
haftmann |
dropped outdated substitution
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 10:56:46 +0200 |
haftmann |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 11:51:32 +0200 |
haftmann |
preliminary versions of static_eval_conv(_simple)
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 11:09:49 +0200 |
haftmann |
refined and unified naming convention for dynamic code evaluation techniques
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 15:31:38 +0200 |
wenzelm |
replaced Thy_Info.the_theory by Context.this_theory -- avoid referring to accidental theory loader state;
|
file |
diff |
annotate
|
| Fri, 16 Jul 2010 13:57:46 +0200 |
haftmann |
don't fail gracefully
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
tuned titles
|
file |
diff |
annotate
|
| Mon, 05 Jul 2010 10:39:49 +0200 |
haftmann |
dropped passed irregular names
|
file |
diff |
annotate
|