| Fri, 07 Mar 2014 01:02:21 +0100 |
blanchet |
balance tuples that represent curried functions
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalized internals
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
rationalize internals
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
optimized simple non-recursive datatypes by reusing 'case' for 'rec' constant
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:48:20 +0100 |
blanchet |
got rid of automatically generated fold constant and theorems (to reduce overhead)
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 18:14:26 +0100 |
traytel |
joint work with blanchet: intermediate typedef for the input to fp-operations
|
file |
diff |
annotate
|
| Thu, 27 Feb 2014 13:04:57 +0100 |
blanchet |
correct most general type for mutual recursion when several identical types are involved
|
file |
diff |
annotate
|
| Sun, 23 Feb 2014 22:51:11 +0100 |
blanchet |
improved accounting for dead variables when naming set functions (refines d71c2737ee21)
|
file |
diff |
annotate
|
| Sun, 23 Feb 2014 22:51:11 +0100 |
blanchet |
added explicit killing
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 08:34:33 +0100 |
blanchet |
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 17:52:28 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 22:54:38 +0100 |
blanchet |
simplified data structure by reducing the incidence of clumsy indices
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 18:42:43 +0100 |
blanchet |
generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 15:03:24 +0100 |
blanchet |
allow different functions to recurse on the same type, like in the old package
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 15:03:23 +0100 |
blanchet |
improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 17:36:00 +0100 |
blanchet |
iteration n in the 'default' vs. 'update_new' vs. 'update' saga -- 'update' makes sense now that we honor the canonical order on 'merge' (as opposed to raising 'DUP')
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
made 'ctr_sugar' more friendly to the 'datatype_realizer'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
more liberal merging of BNFs and constructor sugar
|
file |
diff |
annotate
|
| Thu, 06 Feb 2014 00:24:02 +0100 |
blanchet |
expand 'split' in direct corecursion as well
|
file |
diff |
annotate
|
| Wed, 05 Feb 2014 16:33:22 +0100 |
blanchet |
fixed handling of 'split'
|
file |
diff |
annotate
|
| Tue, 21 Jan 2014 14:52:23 +0100 |
blanchet |
made SML/NJ happier
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
adjusted comments
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
avoid nested 'Tools' directories
|
file |
diff |
annotate
| base
|