| Fri, 01 Oct 2010 17:06:49 +0200 |
haftmann |
moved ML_Context.value to Code_Runtime
|
file |
diff |
annotate
|
| Tue, 21 Sep 2010 15:46:06 +0200 |
haftmann |
no_frees_* is subsumed by new framework mechanisms in Code_Preproc
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 16:51:34 +0200 |
haftmann |
separation of static and dynamic thy context
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 08:18:34 +0200 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 15:11:40 +0200 |
haftmann |
static nbe conversion
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 13:44:11 +0200 |
haftmann |
dropped redundant normal_form command
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 12:11:11 +0200 |
haftmann |
more clear separation of static compilation and dynamic evaluation
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 11:30:32 +0200 |
haftmann |
replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
|
file |
diff |
annotate
|
| Sun, 12 Sep 2010 20:47:47 +0200 |
wenzelm |
load type_infer.ML later -- proper context for Type_Infer.infer_types;
|
file |
diff |
annotate
|
| Sun, 12 Sep 2010 19:04:02 +0200 |
wenzelm |
eliminated aliases of Type.constraint;
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 21:41:24 +0200 |
wenzelm |
turned show_sorts/show_types into proper configuration options;
|
file |
diff |
annotate
|
| Tue, 31 Aug 2010 16:23:58 +0200 |
haftmann |
evaluate takes ml context and ml expression parameter
|
file |
diff |
annotate
|
| Tue, 24 Aug 2010 09:06:17 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 11:51:33 +0200 |
haftmann |
use conv alias
|
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
|
| Thu, 17 Jun 2010 15:59:47 +0200 |
haftmann |
more precise code
|
file |
diff |
annotate
|
| Thu, 17 Jun 2010 11:33:04 +0200 |
haftmann |
transitive superclasses were also only a misunderstanding
|
file |
diff |
annotate
|
| Thu, 17 Jun 2010 10:57:00 +0200 |
haftmann |
formal introduction of transitive superclasses
|
file |
diff |
annotate
|
| Thu, 17 Jun 2010 10:51:38 +0200 |
haftmann |
dropped obscure type argument weakening mapping -- was only a misunderstanding
|
file |
diff |
annotate
|
| Tue, 15 Jun 2010 14:28:22 +0200 |
haftmann |
added code_simp infrastructure
|
file |
diff |
annotate
|
| Tue, 15 Jun 2010 08:32:32 +0200 |
haftmann |
formal introduction of case cong
|
file |
diff |
annotate
|
| Mon, 07 Jun 2010 13:42:38 +0200 |
haftmann |
more consistent naming aroud type classes and instances
|
file |
diff |
annotate
|
| Thu, 27 May 2010 18:10:37 +0200 |
wenzelm |
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
|
file |
diff |
annotate
|
| Thu, 27 May 2010 17:41:27 +0200 |
wenzelm |
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
|
file |
diff |
annotate
|
| Wed, 19 May 2010 10:14:37 +0200 |
haftmann |
new version of triv_of_class machinery without legacy_unconstrain
|
file |
diff |
annotate
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| Sun, 09 May 2010 22:06:24 +0200 |
wenzelm |
reactivated Thm.legacy_unconstrainT for Nbe.lift_triv_classes_conv;
|
file |
diff |
annotate
|
| Sun, 09 May 2010 19:15:21 +0200 |
wenzelm |
just one version of Thm.unconstrainT, which affects all variables;
|
file |
diff |
annotate
|
| Mon, 03 May 2010 20:13:36 +0200 |
wenzelm |
renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
|
file |
diff |
annotate
|
| Mon, 03 May 2010 14:25:56 +0200 |
wenzelm |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Sat, 20 Mar 2010 17:33:11 +0100 |
wenzelm |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file |
diff |
annotate
|
| Tue, 02 Mar 2010 15:39:06 +0100 |
haftmann |
dropped superfluous naming
|
file |
diff |
annotate
|
| Wed, 24 Feb 2010 14:19:54 +0100 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
| Mon, 04 Jan 2010 16:00:24 +0100 |
haftmann |
code cache only persists on equal theories
|
file |
diff |
annotate
|
| Mon, 04 Jan 2010 14:09:56 +0100 |
haftmann |
code cache without copy; tuned
|
file |
diff |
annotate
|
| Wed, 23 Dec 2009 08:31:15 +0100 |
haftmann |
reduced code generator cache to the baremost minimum
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 18:43:42 +0100 |
wenzelm |
adapted Theory_Data;
|
file |
diff |
annotate
|
| Mon, 19 Oct 2009 21:54:57 +0200 |
wenzelm |
uniform use of Integer.add/mult/sum/prod;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 15:57:51 +0200 |
wenzelm |
indicate CRITICAL nature of various setmp combinators;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Wed, 09 Sep 2009 11:31:20 +0200 |
haftmann |
moved eq handling in nbe into separate oracle
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 15:44:31 +0200 |
haftmann |
integrated add_triv_classes into evaluation stack
|
file |
diff |
annotate
|
| Wed, 08 Jul 2009 08:18:07 +0200 |
haftmann |
tuned structure Code internally
|
file |
diff |
annotate
|
| Tue, 07 Jul 2009 17:21:27 +0200 |
haftmann |
tuned interface of structure Code
|
file |
diff |
annotate
|
| Tue, 30 Jun 2009 17:33:30 +0200 |
haftmann |
all variable names are optional
|
file |
diff |
annotate
|
| Tue, 30 Jun 2009 16:43:28 +0200 |
haftmann |
variable names in abstractions are optional
|
file |
diff |
annotate
|
| Fri, 19 Jun 2009 17:26:40 +0200 |
haftmann |
more appropriate syntax for IML abstraction
|
file |
diff |
annotate
|
| Thu, 14 May 2009 15:09:48 +0200 |
haftmann |
merged module code_unit.ML into code.ML
|
file |
diff |
annotate
|
| Thu, 07 May 2009 16:22:35 +0200 |
haftmann |
treat frees driectly by the LCF kernel
|
file |
diff |
annotate
|
| Wed, 06 May 2009 16:01:06 +0200 |
haftmann |
explicit type arguments in constants
|
file |
diff |
annotate
|
| Fri, 24 Apr 2009 08:24:54 +0200 |
haftmann |
generic postprocessing scheme for term evaluations
|
file |
diff |
annotate
|
| Fri, 17 Apr 2009 14:29:56 +0200 |
haftmann |
re-engineering of evaluation conversions
|
file |
diff |
annotate
|
| Fri, 17 Apr 2009 08:34:54 +0200 |
haftmann |
diagnostic commands now in code_thingol; tuned code of funny continuations
|
file |
diff |
annotate
|
| Mon, 23 Mar 2009 21:40:11 +0100 |
wenzelm |
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 19:48:02 +0100 |
wenzelm |
Thm.add_oracle interface: replaced old bstring by binding;
|
file |
diff |
annotate
|
| Fri, 20 Feb 2009 18:29:10 +0100 |
haftmann |
maintain order of constructors in datatypes; clarified conventions for type schemes
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 18:53:17 +0100 |
wenzelm |
use regular Term.add_XXX etc.;
|
file |
diff |
annotate
|
| Tue, 28 Oct 2008 16:59:02 +0100 |
haftmann |
restored incremental code generation
|
file |
diff |
annotate
|
| Wed, 22 Oct 2008 14:15:45 +0200 |
haftmann |
code identifier namings are no longer imperative
|
file |
diff |
annotate
|
| Tue, 30 Sep 2008 12:49:18 +0200 |
haftmann |
clarified codegen interfaces
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 09:28:08 +0200 |
haftmann |
non left-linear equations for nbe
|
file |
diff |
annotate
|
| Tue, 23 Sep 2008 18:11:44 +0200 |
haftmann |
case default fallback for NBE
|
file |
diff |
annotate
|
| Fri, 19 Sep 2008 09:41:17 +0200 |
haftmann |
made SMLNJ happy
|
file |
diff |
annotate
|
| Thu, 18 Sep 2008 19:39:44 +0200 |
wenzelm |
simplified oracle interface;
|
file |
diff |
annotate
|
| Wed, 17 Sep 2008 21:27:43 +0200 |
wenzelm |
ML_Context.evaluate: proper context (for ML environment);
|
file |
diff |
annotate
|
| Tue, 16 Sep 2008 09:21:22 +0200 |
haftmann |
generic value command
|
file |
diff |
annotate
|
| Thu, 28 Aug 2008 22:09:20 +0200 |
haftmann |
restructured and split code serializer module
|
file |
diff |
annotate
|
| Tue, 15 Jul 2008 16:02:07 +0200 |
haftmann |
tuned code theorem bookkeeping
|
file |
diff |
annotate
|
| Tue, 08 Jul 2008 18:13:12 +0200 |
haftmann |
clarified code
|
file |
diff |
annotate
|
| Wed, 18 Jun 2008 22:32:03 +0200 |
wenzelm |
simplified TypeInfer.infer_types;
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 15:30:06 +0200 |
haftmann |
major refactorings in code generator modules
|
file |
diff |
annotate
|
| Fri, 23 May 2008 16:05:07 +0200 |
haftmann |
explicit type schemes for functions
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:04:48 +0200 |
wenzelm |
command 'normal_form': proper context via Variable.auto_fixes;
|
file |
diff |
annotate
|
| Sat, 17 May 2008 15:31:42 +0200 |
wenzelm |
cat_lines;
|
file |
diff |
annotate
|
| Thu, 24 Apr 2008 16:53:04 +0200 |
haftmann |
moved 'trivial classes' to foundation of code generator
|
file |
diff |
annotate
|
| Tue, 22 Apr 2008 22:00:25 +0200 |
haftmann |
different handling of eq class for nbe
|
file |
diff |
annotate
|
| Wed, 13 Feb 2008 09:35:33 +0100 |
haftmann |
using integers for pattern matching
|
file |
diff |
annotate
|
| Tue, 29 Jan 2008 10:20:00 +0100 |
haftmann |
cleaned up evaluation interfaces
|
file |
diff |
annotate
|
| Tue, 22 Jan 2008 23:07:25 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 21 Jan 2008 08:43:35 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 18 Jan 2008 08:30:12 +0100 |
haftmann |
improved implementation
|
file |
diff |
annotate
|
| Tue, 08 Jan 2008 11:37:32 +0100 |
haftmann |
tuned comment
|
file |
diff |
annotate
|
| Fri, 26 Oct 2007 19:58:32 +0200 |
wenzelm |
replaced Secure.evaluate by ML_Context.evaluate;
|
file |
diff |
annotate
|
| Thu, 25 Oct 2007 13:52:04 +0200 |
haftmann |
clarified implementation
|
file |
diff |
annotate
|
| Wed, 24 Oct 2007 07:19:57 +0200 |
haftmann |
fixed typo
|
file |
diff |
annotate
|
| Fri, 19 Oct 2007 16:20:27 +0200 |
haftmann |
now employing dictionaries
|
file |
diff |
annotate
|
| Fri, 19 Oct 2007 16:13:55 +0200 |
wenzelm |
tuned CRITICAL markups;
|
file |
diff |
annotate
|
| Thu, 18 Oct 2007 09:21:00 +0200 |
haftmann |
evaluation is CRITICAL
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 00:20:13 +0200 |
wenzelm |
generic Syntax.pretty/string_of operations;
|
file |
diff |
annotate
|
| Sat, 06 Oct 2007 16:50:04 +0200 |
wenzelm |
simplified interfaces for outer syntax;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 19:41:53 +0200 |
haftmann |
step towards proper purge operation
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 17:06:18 +0200 |
wenzelm |
tuned functor application;
|
file |
diff |
annotate
|
| Sun, 23 Sep 2007 22:23:27 +0200 |
wenzelm |
TypeInfer.constrain: canonical argument order;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 18:05:37 +0200 |
wenzelm |
simplified PrintMode interfaces;
|
file |
diff |
annotate
|
| Mon, 17 Sep 2007 16:36:41 +0200 |
wenzelm |
avoid direct access to print_mode;
|
file |
diff |
annotate
|
| Sat, 15 Sep 2007 19:27:48 +0200 |
haftmann |
delayed evaluation
|
file |
diff |
annotate
|
| Sat, 01 Sep 2007 15:46:59 +0200 |
wenzelm |
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
|
file |
diff |
annotate
|
| Thu, 30 Aug 2007 22:35:34 +0200 |
wenzelm |
replaced ProofContext.infer_types by general Syntax.check_terms;
|
file |
diff |
annotate
|
| Fri, 24 Aug 2007 14:14:20 +0200 |
haftmann |
overloaded definitions accompanied by explicit constants
|
file |
diff |
annotate
|
| Tue, 21 Aug 2007 13:30:38 +0200 |
haftmann |
improved evaluation interface
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 18:07:31 +0200 |
haftmann |
explizit dependencies
|
file |
diff |
annotate
|
| Thu, 16 Aug 2007 11:45:05 +0200 |
haftmann |
added evaluation examples
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 08:57:42 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 10 Aug 2007 17:04:34 +0200 |
haftmann |
new structure for code generator modules
|
file |
diff |
annotate
|
| Tue, 07 Aug 2007 09:40:34 +0200 |
haftmann |
new nbe implementation
|
file |
diff |
annotate
|
| Mon, 06 Aug 2007 11:45:39 +0200 |
haftmann |
nbe improved
|
file |
diff |
annotate
|