| Tue, 23 Aug 2011 07:14:09 +0200 |
haftmann |
tuned specifications, syntax and proofs
|
changeset |
files
|
| Mon, 22 Aug 2011 22:00:36 +0200 |
haftmann |
tuned specifications and syntax
|
changeset |
files
|
| Tue, 23 Aug 2011 03:34:17 +0900 |
Cezary Kaliszyk |
Quotient Package: some infrastructure for lifting inside sets
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
include all encodings in tests, now that the incompleteness of some encodings has been addressed
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
change Metis's default settings if type information axioms are generated
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
we must tag any type whose ground types intersect a nonmonotonic type
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
prefer the lighter, slightly unsound monotonicity-based encodings for Metis
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
made reconstruction of type tag equalities "\?x = \?x" reliable
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
tuning ATP problem output
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
revert guard logic -- make sure that typing information is generated for existentials
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
generate tag equations for existential variables
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
tuning, plus started implementing tag equation generation for existential variables
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
precisely distinguish between universal and existential quantifiers, instead of assuming the worst (universal), for monotonicity analysis
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
clearer terminology
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
renamed "heavy" to "uniform", based on discussion with Nick Smallbone
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
removed unused configuration option
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
added caching for (in)finiteness checks
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
remove needless typing information
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
cleaner handling of polymorphic monotonicity inference
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
started cleaning up polymorphic monotonicity-based encodings, based on discussions with Nick Smallbone
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
more precise warning
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
added option to control soundness of encodings more precisely, for evaluation purposes
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
make sound mode more sound (and clean up code)
|
changeset |
files
|
| Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
|
changeset |
files
|