| Sat, 18 Feb 2012 11:31:35 +0100 |
haftmann |
more explicit error on malformed abstract equation; dropped dead code; tuned signature
|
file |
diff |
annotate
|
| Mon, 26 Dec 2011 18:32:43 +0100 |
haftmann |
dropped disfruitful `constant signatures`
|
file |
diff |
annotate
|
| Wed, 09 Nov 2011 21:36:18 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Sat, 05 Nov 2011 15:00:49 +0100 |
wenzelm |
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 23:07:48 +0200 |
haftmann |
removed some remaining artefacts of ancient SML code generator
|
file |
diff |
annotate
|
| Wed, 06 Jul 2011 20:46:06 +0200 |
wenzelm |
prefer Synchronized.var;
|
file |
diff |
annotate
|
| Sat, 02 Jul 2011 10:37:35 +0200 |
haftmann |
correction: do not assume that case const index covered all cases
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 23:31:23 +0200 |
haftmann |
remove illegal case combinators after merge
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 23:10:27 +0200 |
haftmann |
corrected misunderstanding what `old functions` are supposed to be
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 23:07:06 +0200 |
haftmann |
centralized deletion of equations for constructors; corrected misunderstanding what `old functions` are supposed to be
|
file |
diff |
annotate
|
| Fri, 01 Jul 2011 19:57:41 +0200 |
haftmann |
index cases for constructors
|
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
|
| Fri, 06 May 2011 11:57:21 +0200 |
bulwahn |
improving merge of code specifications by removing code equations of constructors after merging two theories
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 19:54:04 +0200 |
wenzelm |
report Name_Space.declare/define, relatively to context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:47:52 +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
|
| Mon, 10 Jan 2011 16:45:28 +0100 |
wenzelm |
added merge_options convenience;
|
file |
diff |
annotate
|
| Sat, 08 Jan 2011 17:14:48 +0100 |
wenzelm |
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
|
file |
diff |
annotate
|
| Wed, 01 Dec 2010 15:03:44 +0100 |
wenzelm |
more direct use of binder_types/body_type;
|
file |
diff |
annotate
|
| Mon, 29 Nov 2010 11:38:59 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sat, 27 Nov 2010 22:01:27 +0100 |
haftmann |
typscheme with signatures is inappropriate when building empty certificate;
|
file |
diff |
annotate
|
| Sat, 27 Nov 2010 19:41:28 +0100 |
haftmann |
corrected: use canonical variables of type scheme uniformly
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 23:49:49 +0100 |
haftmann |
consider sort constraints for datatype constructors when constructing the empty equation certificate;
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 22:33:21 +0100 |
haftmann |
keep type variable arguments of datatype constructors in bookkeeping
|
file |
diff |
annotate
|
| Tue, 16 Nov 2010 10:33:36 +0100 |
haftmann |
added forall2 predicate lifter
|
file |
diff |
annotate
|
| Thu, 04 Nov 2010 17:27:38 +0100 |
haftmann |
Code.check_const etc.: reject too specific types
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 11:06:22 +0100 |
wenzelm |
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 15:00:42 +0200 |
haftmann |
more general treatment of type argument in code certificates for operations on abstract types
|
file |
diff |
annotate
|
| Fri, 01 Oct 2010 10:25:36 +0200 |
haftmann |
chop_while replace drop_while and take_while
|
file |
diff |
annotate
|
| Thu, 30 Sep 2010 18:37:29 +0200 |
haftmann |
take_while, drop_while
|
file |
diff |
annotate
|
| Thu, 30 Sep 2010 08:50:45 +0200 |
haftmann |
corrected subsumption check: arguments have been reversed; addition of default equations to non-default equations is identity
|
file |
diff |
annotate
|
| Wed, 29 Sep 2010 15:28:29 +0200 |
haftmann |
redundancy check: drop trailing Var arguments (avoids eta problems with equations)
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 18:43:26 +0200 |
haftmann |
corrected long-overlooked slip: the Pure equality of a code equation is no part of the code equation itself
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 11:55:21 +0200 |
haftmann |
more accurate exception handling
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 15:11:39 +0200 |
haftmann |
ignore code cache optionally
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 21:41:24 +0200 |
wenzelm |
turned show_sorts/show_types into proper configuration options;
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 15:33:59 +0200 |
haftmann |
replaced Table.map' by Table.map
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 11:09:48 +0200 |
haftmann |
dropped now obsolete purge_data -- happens implicitly on change of theory identity
|
file |
diff |
annotate
|
| Thu, 24 Jun 2010 09:04:50 +0200 |
haftmann |
made smlnj happy
|
file |
diff |
annotate
|
| Fri, 18 Jun 2010 15:03:21 +0200 |
haftmann |
drop subsumed default equations (requires a little bit unfortunate laziness)
|
file |
diff |
annotate
|
| Thu, 17 Jun 2010 15:59:46 +0200 |
haftmann |
explicit type variable arguments for constructors
|
file |
diff |
annotate
|
| Tue, 15 Jun 2010 11:38:39 +0200 |
haftmann |
maintain cong rules for case combinators
|
file |
diff |
annotate
|
| Mon, 14 Jun 2010 12:01:30 +0200 |
haftmann |
explicitly name and note equations for class eq
|
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
|
| Mon, 19 Apr 2010 15:31:56 +0200 |
haftmann |
more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
|
file |
diff |
annotate
|
| Mon, 19 Apr 2010 11:30:08 +0200 |
haftmann |
explicit check sorts in abstract certificates; abstractor is part of dependencies
|
file |
diff |
annotate
|
| Tue, 13 Apr 2010 11:30:12 +0200 |
haftmann |
more accurate pattern match
|
file |
diff |
annotate
|
| Sun, 11 Apr 2010 16:51:07 +0200 |
haftmann |
user interface for abstract datatypes is an attribute, not a command
|
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
|
| Sun, 07 Mar 2010 11:57:16 +0100 |
wenzelm |
modernized structure Local_Defs;
|
file |
diff |
annotate
|
| Fri, 26 Feb 2010 10:48:21 +0100 |
haftmann |
use abstract code cerficates for bare code theorems
|
file |
diff |
annotate
|
| Wed, 24 Feb 2010 14:42:28 +0100 |
haftmann |
bound argument for abstype proposition
|
file |
diff |
annotate
|
| Wed, 24 Feb 2010 14:19:54 +0100 |
haftmann |
more precise exception handler
|
file |
diff |
annotate
|
| Mon, 22 Feb 2010 15:53:19 +0100 |
haftmann |
more accurate when registering new types
|
file |
diff |
annotate
|
| Mon, 22 Feb 2010 11:10:20 +0100 |
haftmann |
proper distinction of code datatypes and abstypes
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 11:06:21 +0100 |
haftmann |
a simple concept for datatype invariants
|
file |
diff |
annotate
|
| Thu, 14 Jan 2010 17:47:39 +0100 |
haftmann |
printing of cases
|
file |
diff |
annotate
|
| Wed, 13 Jan 2010 12:20:37 +0100 |
haftmann |
explicit abstract type of code certificates
|
file |
diff |
annotate
|
| Wed, 13 Jan 2010 10:18:45 +0100 |
haftmann |
corrected error messages; tuned
|
file |
diff |
annotate
|
| Tue, 12 Jan 2010 16:27:42 +0100 |
haftmann |
code certificates as integral part of code generation
|
file |
diff |
annotate
|
| Mon, 11 Jan 2010 16:45:02 +0100 |
haftmann |
added code certificates
|
file |
diff |
annotate
|
| Tue, 05 Jan 2010 14:19:12 +0100 |
haftmann |
avoid exporting Type.build_tsig
|
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
|
| Thu, 24 Dec 2009 11:05:58 +0100 |
haftmann |
made sml/nj happy
|
file |
diff |
annotate
|
| Wed, 23 Dec 2009 08:31:15 +0100 |
haftmann |
reduced code generator cache to the baremost minimum
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 15:30:36 +0100 |
wenzelm |
merged, resolving minor conflict, and recovering sane state;
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 15:20:24 +0100 |
wenzelm |
merged, resolving minor conflicts;
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 12:22:09 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 30 Nov 2009 12:28:12 +0100 |
haftmann |
dropped some unused bindings
|
file |
diff |
annotate
|
| Wed, 25 Nov 2009 09:13:46 +0100 |
haftmann |
normalized uncurry take/drop
|
file |
diff |
annotate
|
| Tue, 24 Nov 2009 17:28:25 +0100 |
haftmann |
curried take/drop
|
file |
diff |
annotate
|
| Wed, 02 Dec 2009 17:53:35 +0100 |
haftmann |
crude support for type aliasses and corresponding constant signatures
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 08:25:57 +0100 |
bulwahn |
replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules
|
file |
diff |
annotate
|
| Mon, 16 Nov 2009 10:16:40 +0100 |
haftmann |
proper purge
|
file |
diff |
annotate
|
| Mon, 09 Nov 2009 14:47:16 +0100 |
haftmann |
tuned error messages; tuned code
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 18:43:42 +0100 |
wenzelm |
adapted Theory_Data;
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 16:15:33 +0100 |
wenzelm |
modernized functor/structures Interpretation;
|
file |
diff |
annotate
|
| Thu, 22 Oct 2009 16:50:24 +0200 |
haftmann |
close thm derivations explicitly
|
file |
diff |
annotate
|
| Mon, 19 Oct 2009 16:34:12 +0200 |
haftmann |
dropped lazy code equations
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 15:57:51 +0200 |
wenzelm |
indicate CRITICAL nature of various setmp combinators;
|
file |
diff |
annotate
|
| Wed, 14 Oct 2009 13:56:56 +0200 |
haftmann |
sharpened name
|
file |
diff |
annotate
|
| Wed, 14 Oct 2009 12:20:01 +0200 |
haftmann |
more explicit notion of canonized code equations
|
file |
diff |
annotate
|
| Mon, 05 Oct 2009 15:04:45 +0200 |
haftmann |
tuned handling of type variable names further
|
file |
diff |
annotate
|
| Mon, 05 Oct 2009 08:36:33 +0200 |
haftmann |
variables in type schemes must be renamed simultaneously with variables in equations
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
handling of definitions
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
experimenting to add some useful interface for definitions
|
file |
diff |
annotate
|
| Tue, 22 Sep 2009 08:58:08 +0200 |
haftmann |
corrected order of type variables in code equations; more precise certificate for cases
|
file |
diff |
annotate
|
| Wed, 09 Sep 2009 11:31:20 +0200 |
haftmann |
moved eq handling in nbe into separate oracle
|
file |
diff |
annotate
|
| Mon, 10 Aug 2009 12:25:30 +0200 |
haftmann |
same_typscheme replaces ugly common_typ_eqns
|
file |
diff |
annotate
|
| Fri, 31 Jul 2009 09:46:09 +0200 |
haftmann |
using certify_instantiate
|
file |
diff |
annotate
|
| Fri, 31 Jul 2009 09:34:05 +0200 |
haftmann |
cleaned up variable desymbolification and argument expansion
|
file |
diff |
annotate
|
| Wed, 22 Jul 2009 11:23:09 +0200 |
wenzelm |
merged, resolving trivial conflict;
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 15:44:31 +0200 |
haftmann |
more accurate check of judgment type
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 01:03:18 +0200 |
wenzelm |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 16:27:33 +0200 |
haftmann |
clarified code
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 10:54:04 +0200 |
haftmann |
code attributes use common underscore convention
|
file |
diff |
annotate
|
| Thu, 09 Jul 2009 22:01:41 +0200 |
wenzelm |
renamed functor TableFun to Table, and GraphFun to Graph;
|
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 18:23:50 +0200 |
haftmann |
an intermediate step towards a refined translation of cases
|
file |
diff |
annotate
|
| Mon, 15 Jun 2009 16:13:04 +0200 |
haftmann |
permissive code attribute; all_eqns
|
file |
diff |
annotate
|
| Tue, 09 Jun 2009 22:59:55 +0200 |
haftmann |
tuned make/map/merge combinators
|
file |
diff |
annotate
|
| Thu, 14 May 2009 15:09:48 +0200 |
haftmann |
merged module code_unit.ML into code.ML
|
file |
diff |
annotate
|
| Thu, 14 May 2009 09:16:36 +0200 |
haftmann |
strip sorts while checking pattern subsumption
|
file |
diff |
annotate
|
| Tue, 12 May 2009 19:30:33 +0200 |
haftmann |
transferred code generator preprocessor into separate module
|
file |
diff |
annotate
|
| Mon, 11 May 2009 11:53:21 +0200 |
haftmann |
corrected deletetion of code equations for constructors
|
file |
diff |
annotate
|
| Mon, 11 May 2009 10:53:19 +0200 |
haftmann |
clarified matter of "proper" flag in code equations
|
file |
diff |
annotate
|
| Mon, 11 May 2009 09:40:38 +0200 |
haftmann |
clarified terminilogy concerning nbe equations
|
file |
diff |
annotate
|
| Wed, 15 Apr 2009 15:38:30 +0200 |
haftmann |
say farewell to code related to old code_funcgr module
|
file |
diff |
annotate
|
| Thu, 26 Mar 2009 14:14:02 +0100 |
wenzelm |
simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
|
file |
diff |
annotate
|
| Sun, 15 Mar 2009 15:59:44 +0100 |
wenzelm |
simplified attribute setup;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 21:25:15 +0100 |
wenzelm |
eliminated type Args.T;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 12:16:12 +0100 |
wenzelm |
proper context for Simplifier.pretty_ss;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|