| 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
|