| 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
|
| Fri, 02 Jul 2010 16:20:56 +0200 |
haftmann |
reverted to verion from fc27be4c6b1c
|
file |
diff |
annotate
|
| Fri, 02 Jul 2010 16:15:49 +0200 |
haftmann |
traceback for error messages
|
file |
diff |
annotate
|
| Wed, 30 Jun 2010 11:38:51 +0200 |
haftmann |
unfold_fun_n
|
file |
diff |
annotate
|
| Thu, 17 Jun 2010 15:59:46 +0200 |
haftmann |
explicit type variable arguments for constructors
|
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 11:38:40 +0200 |
haftmann |
maintain cong rules for case combinators; more precise permissiveness
|
file |
diff |
annotate
|
| Tue, 15 Jun 2010 08:32:32 +0200 |
haftmann |
formal introduction of case cong
|
file |
diff |
annotate
|
| Mon, 14 Jun 2010 16:00:47 +0200 |
haftmann |
teaked naming of superclass projections
|
file |
diff |
annotate
|
| Mon, 07 Jun 2010 13:42:38 +0200 |
haftmann |
more consistent naming aroud type classes and instances
|
file |
diff |
annotate
|
| Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| Wed, 21 Apr 2010 15:20:59 +0200 |
haftmann |
optionally ignore errors during translation of equations; tuned representation of abstraction points
|
file |
diff |
annotate
|
| Mon, 19 Apr 2010 15:31:58 +0200 |
haftmann |
more appropriate representation of valid positions for abstractors
|
file |
diff |
annotate
|
| Sun, 11 Apr 2010 13:08:14 +0200 |
wenzelm |
of_sort_derivation: pass-through full type information -- following the version by krauss/schropp;
|
file |
diff |
annotate
|
| Thu, 25 Mar 2010 21:27:04 +0100 |
wenzelm |
Sorts.of_sort_derivation: do not use slow Graph.irreducible_paths here, which not always needed (SUBTLE CHANGE IN SEMANTICS);
|
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
|
| 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
|
| Wed, 13 Jan 2010 12:20:37 +0100 |
haftmann |
explicit abstract type of code certificates
|
file |
diff |
annotate
|
| Tue, 12 Jan 2010 16:27:42 +0100 |
haftmann |
code certificates as integral part of code generation
|
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
|
| Mon, 14 Dec 2009 10:23:25 +0100 |
haftmann |
explicit name for function space
|
file |
diff |
annotate
|
| Mon, 07 Dec 2009 09:16:27 +0100 |
haftmann |
repaired read_const_expr, broken in 1e7ca47c6c3d
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 18:51:15 +0100 |
haftmann |
merged, resolving minor conflicts
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 18:19:31 +0100 |
haftmann |
avoid misleading name "superarities"
|
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:36 +0100 |
haftmann |
subst_signatures
|
file |
diff |
annotate
|
| Tue, 03 Nov 2009 17:06:08 +0100 |
haftmann |
pretty name for ==>
|
file |
diff |
annotate
|
| Mon, 26 Oct 2009 10:51:42 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 20:54:21 +0100 |
wenzelm |
maintain theory name via name space, not tags;
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 20:54:31 +0200 |
wenzelm |
uniform use of Integer.min/max;
|
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, 12 Oct 2009 16:16:44 +0200 |
haftmann |
added add_tyconames; tuned
|
file |
diff |
annotate
|
| Mon, 12 Oct 2009 12:19:19 +0200 |
haftmann |
added is_IVar
|
file |
diff |
annotate
|
| Thu, 08 Oct 2009 15:59:17 +0200 |
haftmann |
added group_stmts
|
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
|
| Wed, 30 Sep 2009 23:30:37 +0200 |
wenzelm |
Sorts.of_sort_derivation: no pp here;
|
file |
diff |
annotate
|
| Wed, 09 Sep 2009 12:27:12 +0200 |
haftmann |
explicit transfer avoids spurious merge problems
|
file |
diff |
annotate
|
| Tue, 11 Aug 2009 10:43:43 +0200 |
haftmann |
proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
|
file |
diff |
annotate
|
| Mon, 10 Aug 2009 12:24:49 +0200 |
haftmann |
moved all technical processing of code equations to code_thingol.ML
|
file |
diff |
annotate
|
| Mon, 10 Aug 2009 08:37:37 +0200 |
haftmann |
attempt to move desymbolization to translation
|
file |
diff |
annotate
|
| Wed, 29 Jul 2009 16:42:47 +0200 |
haftmann |
abstractions: desymbolize name hint
|
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 |
integrated add_triv_classes into evaluation stack
|
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
|
| 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
|
| Fri, 03 Jul 2009 16:51:07 +0200 |
haftmann |
cleaned up fundamental iml term functions; nested patterns
|
file |
diff |
annotate
|
| Tue, 30 Jun 2009 19:31:50 +0200 |
haftmann |
improved treatment of case patterns
|
file |
diff |
annotate
|
| Tue, 30 Jun 2009 18:23:50 +0200 |
haftmann |
an intermediate step towards a refined translation of cases
|
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
|
| Tue, 30 Jun 2009 14:54:00 +0200 |
haftmann |
simplified binding concept
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 12:09:30 +0200 |
haftmann |
uniformly capitialized names for subdirectories
|
file |
diff |
annotate
| base
|