| Tue, 13 Dec 2011 14:55:42 +0100 |
blanchet |
correctly declare implicit TFF1 types that appear first as type arguments with "$tType" and not "$i
|
file |
diff |
annotate
|
| Wed, 07 Dec 2011 16:03:05 +0100 |
blanchet |
avoid multiple TFF1 declarations
|
file |
diff |
annotate
|
| Wed, 07 Dec 2011 16:03:05 +0100 |
blanchet |
updated TFF1 support
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
pull variables (Var) out of lambdas, so that the Isabelle theorems closely mirror the Metis lambda-lifted ones
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
move eta-contraction to before translation to Metis, to ensure everything stays in sync
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
fixed bugs in lambda-lifting code -- ensure distinct names for variables
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
protect prefix against variant mutations
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
don't pass "lam_lifted" option to "metis" unless there's a good reason
|
file |
diff |
annotate
|
| Fri, 18 Nov 2011 11:47:12 +0100 |
blanchet |
removed needless baggage
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 16:35:19 +0100 |
blanchet |
thread in additional options to minimizer
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 13:22:36 +0100 |
blanchet |
make metis reconstruction handling more flexible
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 10:34:08 +0100 |
blanchet |
document "lam_trans" option
|
file |
diff |
annotate
|
| Wed, 16 Nov 2011 09:42:27 +0100 |
blanchet |
parse lambda translation option in Metis
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 22:20:58 +0100 |
blanchet |
rename the lambda translation schemes, so that they are understandable out of context
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 22:13:39 +0100 |
blanchet |
continued implementation of lambda-lifting in Metis
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 22:13:39 +0100 |
blanchet |
use consts, not frees, for lambda-lifting
|
file |
diff |
annotate
|
| Tue, 15 Nov 2011 22:13:39 +0100 |
blanchet |
started implementing lambda-lifting in Metis
|
file |
diff |
annotate
|
| Tue, 08 Nov 2011 08:56:23 +0100 |
blanchet |
made SML/NJ happy
|
file |
diff |
annotate
|
| Sun, 06 Nov 2011 22:18:54 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Sun, 06 Nov 2011 11:13:47 +0100 |
blanchet |
repaired quantification over type variables for non-TFF1/THF encodings
|
file |
diff |
annotate
|
| Mon, 31 Oct 2011 17:51:01 +0100 |
blanchet |
improve handling of bound type variables (esp. for TFF1)
|
file |
diff |
annotate
|
| Mon, 31 Oct 2011 17:51:01 +0100 |
blanchet |
improved TFF1 output
|
file |
diff |
annotate
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
always use DFG format to talk to SPASS -- since that's what we'll need to use anyway to benefit from sorts and other extensions
|
file |
diff |
annotate
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
added DFG unsorted support (like in the old days)
|
file |
diff |
annotate
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
added sorted DFG output for coming version of SPASS
|
file |
diff |
annotate
|
| Sat, 29 Oct 2011 13:15:58 +0200 |
blanchet |
check "sound" flag before doing something unsound...
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 16:36:13 +0200 |
blanchet |
avoid generating too meta theorems -- this sometimes leads to type errors, e.g. when "pp" is applied to a "prop" instead of a "bool"
|
file |
diff |
annotate
|
| Tue, 18 Oct 2011 15:40:59 +0200 |
blanchet |
freeze conjecture schematics before applying lambda-translation, which sometimes calls "close_form" and ruins it for freezing
|
file |
diff |
annotate
|
| Tue, 18 Oct 2011 15:40:58 +0200 |
blanchet |
gracefully handle quantifiers of the form "All $ t" where "t" is not a lambda-abstraction in higher-order translations
|
file |
diff |
annotate
|
| Sat, 10 Sep 2011 00:44:25 +0200 |
blanchet |
fixed definition of type intersection (soundness bug)
|
file |
diff |
annotate
|