]> matita.cs.unibo.it Git - helm.git/log
helm.git
18 years agofixed some bugs
Enrico Tassi [Sat, 13 May 2006 15:12:04 +0000 (15:12 +0000)]
fixed some bugs

18 years agofull script generation
Enrico Tassi [Sat, 13 May 2006 15:11:18 +0000 (15:11 +0000)]
full script generation

18 years agofixed some pp stuff
Enrico Tassi [Sat, 13 May 2006 13:43:42 +0000 (13:43 +0000)]
fixed some pp stuff

18 years ago...
Enrico Tassi [Fri, 12 May 2006 15:25:13 +0000 (15:25 +0000)]
...

18 years agoremoved shift-reduce conflict
Enrico Tassi [Fri, 12 May 2006 15:19:40 +0000 (15:19 +0000)]
removed shift-reduce conflict

18 years agoadded parser (and future converter) of tptp files
Enrico Tassi [Fri, 12 May 2006 15:15:29 +0000 (15:15 +0000)]
added parser (and future converter) of tptp files

18 years agoBugs fixed:
Claudio Sacerdoti Coen [Thu, 11 May 2006 11:27:44 +0000 (11:27 +0000)]
Bugs fixed:
 * the dependency parser no longer fails when an incomplete "include" or "set"
   are met
 * ask_and_save_moo is now performed more lazily and some bugs have been fixed

18 years agofew more bits for zack
Enrico Tassi [Tue, 9 May 2006 16:26:48 +0000 (16:26 +0000)]
few more bits for zack

18 years agohalf ported to the "new" module organization.
Enrico Tassi [Tue, 9 May 2006 13:41:00 +0000 (13:41 +0000)]
half ported to the "new" module organization.

18 years agotypes2006 patch
Enrico Tassi [Tue, 9 May 2006 13:40:24 +0000 (13:40 +0000)]
types2006 patch

18 years agoNew version of deep_subsumption
Andrea Asperti [Fri, 5 May 2006 14:56:30 +0000 (14:56 +0000)]
New version of deep_subsumption

18 years agogoal demodulated with new
Enrico Tassi [Thu, 4 May 2006 15:15:47 +0000 (15:15 +0000)]
goal demodulated with new

18 years agonew pp function for proofs
Enrico Tassi [Thu, 4 May 2006 10:55:15 +0000 (10:55 +0000)]
new pp function for proofs

18 years agoeq_chain
Enrico Tassi [Wed, 3 May 2006 11:26:21 +0000 (11:26 +0000)]
eq_chain

18 years agomore transitivity on proofs
Enrico Tassi [Wed, 3 May 2006 11:25:45 +0000 (11:25 +0000)]
more transitivity on proofs

18 years agoEquality chains.
Andrea Asperti [Thu, 27 Apr 2006 10:07:47 +0000 (10:07 +0000)]
Equality chains.
-This line, and those below, will be ignored--

M    acic_content/acic2content.ml

18 years agoAdded is_trans_eq_URI and is_sym_eq_URI
Andrea Asperti [Thu, 27 Apr 2006 10:06:54 +0000 (10:06 +0000)]
Added is_trans_eq_URI and is_sym_eq_URI

18 years agoBuild_proof_goal does not return the metasenv any more.
Andrea Asperti [Wed, 26 Apr 2006 14:53:03 +0000 (14:53 +0000)]
Build_proof_goal does not return the metasenv any more.

18 years agofixed demodulation_goal (used to return always false)
Andrea Asperti [Wed, 26 Apr 2006 13:23:55 +0000 (13:23 +0000)]
fixed demodulation_goal (used to return always false)

18 years agoremoved ocaml equality on equations
Andrea Asperti [Wed, 26 Apr 2006 13:23:29 +0000 (13:23 +0000)]
removed ocaml equality on equations

18 years agomore cleanup
Enrico Tassi [Wed, 26 Apr 2006 10:05:28 +0000 (10:05 +0000)]
more cleanup

18 years agocleanup of saturate
Enrico Tassi [Wed, 26 Apr 2006 09:59:07 +0000 (09:59 +0000)]
cleanup of saturate

18 years agoadded a new type for proofs.
Enrico Tassi [Wed, 26 Apr 2006 09:21:07 +0000 (09:21 +0000)]
added a new type for proofs.

18 years agoadded a whd (nodelta) in the carr function used by the refiner (in the eat_prods...
Enrico Tassi [Wed, 26 Apr 2006 09:16:01 +0000 (09:16 +0000)]
added a whd (nodelta) in the carr function used by the refiner (in the eat_prods case)
to get the carrier of a coercion. this is useful in case of terms generated by paramodulation
(and we want to refine the proof letting the refiner add symmetry steps)
where we have ((\lambda x:A.P(x)) t) === P'(t)
and P/P' is M=N/N=M

18 years agoBug fixed: "paste as pattern" now pastes the full pattern (e.g.
Claudio Sacerdoti Coen [Sun, 16 Apr 2006 14:45:11 +0000 (14:45 +0000)]
Bug fixed: "paste as pattern" now pastes the full pattern (e.g.
"in H:(? %)"; it used to paste "(? %)" only)

18 years agoPatch to avoid double execution of whelp queries reverted (since it seems
Claudio Sacerdoti Coen [Sat, 15 Apr 2006 16:57:24 +0000 (16:57 +0000)]
Patch to avoid double execution of whelp queries reverted (since it seems
that queries are NOT executed twice without the patch (!?!) and with the
patch the query is sometimes not executed).

18 years agouft8 string length bug fixed (Ctr-Alt-. did not work properly any longer)
Enrico Tassi [Fri, 14 Apr 2006 11:36:27 +0000 (11:36 +0000)]
uft8 string length bug fixed (Ctr-Alt-. did not work properly any longer)

18 years agomulti-instances aliases are compressed to single instances if possible
Enrico Tassi [Fri, 14 Apr 2006 10:15:48 +0000 (10:15 +0000)]
multi-instances aliases are compressed to single instances if possible

18 years ago duplicate check for coercions when added to Db
Enrico Tassi [Fri, 14 Apr 2006 10:14:43 +0000 (10:14 +0000)]
duplicate check for coercions when added to Db

18 years agoalases instance not printed if 0
Enrico Tassi [Fri, 14 Apr 2006 10:13:55 +0000 (10:13 +0000)]
alases instance not printed if 0

18 years agothe same utf8 bug as before
Enrico Tassi [Fri, 14 Apr 2006 10:13:07 +0000 (10:13 +0000)]
the same utf8 bug as before

18 years ago fixed another utf8 string length bug
Enrico Tassi [Fri, 14 Apr 2006 10:12:27 +0000 (10:12 +0000)]
fixed another utf8 string length bug

18 years ago added minimal euristic for generic terms carrier comparison
Enrico Tassi [Fri, 14 Apr 2006 10:11:32 +0000 (10:11 +0000)]
added minimal euristic for generic terms carrier comparison

18 years agoto tired to write a message.
Enrico Tassi [Thu, 13 Apr 2006 23:44:51 +0000 (23:44 +0000)]
to tired to write a message.

18 years agoadded include' to include everything but preferences (aka aliases)
Enrico Tassi [Thu, 13 Apr 2006 14:24:03 +0000 (14:24 +0000)]
added include' to include everything but preferences (aka aliases)

18 years agopartially fixed boxes in rewite
Enrico Tassi [Thu, 13 Apr 2006 14:23:30 +0000 (14:23 +0000)]
partially fixed  boxes in rewite

18 years agoadded keyword include'
Enrico Tassi [Thu, 13 Apr 2006 14:21:12 +0000 (14:21 +0000)]
added keyword include'

18 years ago-debug should work better
Enrico Tassi [Thu, 13 Apr 2006 14:20:25 +0000 (14:20 +0000)]
-debug should work better

18 years agoin eta_finxing: type_of_aux' not called on eta_fixed terms
Enrico Tassi [Thu, 13 Apr 2006 13:06:25 +0000 (13:06 +0000)]
in eta_finxing: type_of_aux' not called on eta_fixed terms
in doubletypeInference calls to type_of_aux' wrapped because of eta fixing

18 years agoUgly solution to the "we proved T that is equivalent to T" problem:
Claudio Sacerdoti Coen [Thu, 13 Apr 2006 11:17:10 +0000 (11:17 +0000)]
Ugly solution to the "we proved T that is equivalent to T" problem:
we use pack_coercion (defined into cicRefine) inside doubleTypeInference
(that is well below in the module hierarchy :-(

This is also supposed to be quite expensive (since pack_coercion uses
the refiner and coercion packing is applied to every expected/synthesized
type).

18 years agoProfiling code commented out.
Claudio Sacerdoti Coen [Thu, 13 Apr 2006 11:10:27 +0000 (11:10 +0000)]
Profiling code commented out.

18 years agoSome times reduced in a second benchmark.
Claudio Sacerdoti Coen [Thu, 13 Apr 2006 11:08:19 +0000 (11:08 +0000)]
Some times reduced in a second benchmark.

18 years agoUtime + Systime used in place of gettimeofday.
Claudio Sacerdoti Coen [Thu, 13 Apr 2006 11:06:29 +0000 (11:06 +0000)]
Utime + Systime used in place of gettimeofday.

18 years agoadded patch to allow agin "match sin ? = ?"
Enrico Tassi [Wed, 12 Apr 2006 21:18:44 +0000 (21:18 +0000)]
added patch to allow agin "match sin ? = ?"

18 years agofixed new compilation order
Enrico Tassi [Wed, 12 Apr 2006 21:17:18 +0000 (21:17 +0000)]
fixed new compilation order

18 years agoexported pp function for terms
Enrico Tassi [Wed, 12 Apr 2006 21:15:27 +0000 (21:15 +0000)]
exported pp function for terms

18 years agowhelp locate now accepts * and ?
Enrico Tassi [Wed, 12 Apr 2006 16:22:09 +0000 (16:22 +0000)]
whelp locate now accepts * and ?

18 years agowhelp macros have now () around args
Enrico Tassi [Wed, 12 Apr 2006 15:50:57 +0000 (15:50 +0000)]
whelp macros have now () around args

18 years agosome fixes for whelp macros (concerning pprint...)
Enrico Tassi [Wed, 12 Apr 2006 15:48:08 +0000 (15:48 +0000)]
some fixes for whelp macros (concerning pprint...)

18 years agoAltri benchmarks.
Claudio Sacerdoti Coen [Tue, 11 Apr 2006 14:20:11 +0000 (14:20 +0000)]
Altri benchmarks.

18 years agoCicEnvironment is emptied when a size treshold is reached.
Claudio Sacerdoti Coen [Tue, 11 Apr 2006 10:02:32 +0000 (10:02 +0000)]
CicEnvironment is emptied when a size treshold is reached.

18 years agoRemoved negative equations.
Andrea Asperti [Mon, 10 Apr 2006 09:02:37 +0000 (09:02 +0000)]
Removed negative equations.

18 years agolinks to .opt are now generated in the world target
Enrico Tassi [Wed, 5 Apr 2006 15:00:49 +0000 (15:00 +0000)]
links to .opt are now generated in the world target

18 years agofix for distro
Enrico Tassi [Wed, 5 Apr 2006 14:47:33 +0000 (14:47 +0000)]
fix for distro

18 years agoa bit of shareing
Enrico Tassi [Wed, 5 Apr 2006 13:24:35 +0000 (13:24 +0000)]
a bit of shareing

18 years agoadded estimate_size
Enrico Tassi [Wed, 5 Apr 2006 13:23:39 +0000 (13:23 +0000)]
added estimate_size

18 years agocreate directory paramodulation for tests for paramodulation
Enrico Tassi [Wed, 5 Apr 2006 12:10:15 +0000 (12:10 +0000)]
create directory paramodulation for tests for paramodulation

18 years agoadded another interesting problem for paramodulation
Enrico Tassi [Wed, 5 Apr 2006 12:08:32 +0000 (12:08 +0000)]
added another interesting problem for paramodulation

18 years agothe tactic now returns as open goals the open metas in the proof
Enrico Tassi [Wed, 5 Apr 2006 12:07:51 +0000 (12:07 +0000)]
the tactic now returns as open goals the open metas in the proof
subsumption is now used correctly in given_clause_fullred

18 years agosubsumption fixed and called in given_clause_fullred.
Enrico Tassi [Wed, 5 Apr 2006 08:06:55 +0000 (08:06 +0000)]
subsumption fixed and called in given_clause_fullred.

18 years agoNaif substitution. Removed local context in metas during relocation.
Andrea Asperti [Tue, 4 Apr 2006 15:01:30 +0000 (15:01 +0000)]
Naif substitution. Removed local context in metas during relocation.
Removed apply_theorems in saturate, replaced by a local check for
identity.

18 years agoUseless code simplified out.
Claudio Sacerdoti Coen [Mon, 3 Apr 2006 13:12:21 +0000 (13:12 +0000)]
Useless code simplified out.

18 years agoNew benchmark after removal of some profiling code.
Claudio Sacerdoti Coen [Fri, 31 Mar 2006 11:02:29 +0000 (11:02 +0000)]
New benchmark after removal of some profiling code.

18 years agoLess profiling.
Claudio Sacerdoti Coen [Thu, 30 Mar 2006 16:40:50 +0000 (16:40 +0000)]
Less profiling.

18 years agoProfiling code for merge_ugraphs commented out (since profiling is much more
Claudio Sacerdoti Coen [Thu, 30 Mar 2006 16:21:45 +0000 (16:21 +0000)]
Profiling code for merge_ugraphs commented out (since profiling is much more
expensive than the profiled code).

18 years agoA few benchmarks on the library of Coq committed.
Claudio Sacerdoti Coen [Thu, 30 Mar 2006 14:28:28 +0000 (14:28 +0000)]
A few benchmarks on the library of Coq committed.

18 years agoAdded deadline (now 30s) to each test.
Claudio Sacerdoti Coen [Thu, 30 Mar 2006 11:40:40 +0000 (11:40 +0000)]
Added deadline (now 30s) to each test.

18 years agoSys.Break used to be captured.
Claudio Sacerdoti Coen [Thu, 30 Mar 2006 11:15:52 +0000 (11:15 +0000)]
Sys.Break used to be captured.

18 years agoBug fixed: terms with a Cast used to raise assert false when whd was avoided
Claudio Sacerdoti Coen [Thu, 30 Mar 2006 11:12:53 +0000 (11:12 +0000)]
Bug fixed: terms with a Cast used to raise assert false when whd was avoided
by the conversion strategy.

18 years agoHuge speed-up in conversion: the old conversion strategy is set back.
Claudio Sacerdoti Coen [Wed, 29 Mar 2006 16:26:32 +0000 (16:26 +0000)]
Huge speed-up in conversion: the old conversion strategy is set back.
 1. try to "convert" the two terms recursively without performing reduction
 2. if it fails, do a whd and try again
The overall result on the library of Coq is really remarkable.

18 years ago#### EXPERIMENTAL COMMIT ####
Claudio Sacerdoti Coen [Wed, 29 Mar 2006 14:44:00 +0000 (14:44 +0000)]
#### EXPERIMENTAL COMMIT ####
Added a potentially dangerous ~expand_beta_redexes flag to
CicSubstitution.subst. If used carefully, it enormously speeds up
the type-checking of many theorems (since a very frequent conversion test
happens between a beta-redex and its contractum).

18 years agoDebugging code added.
Claudio Sacerdoti Coen [Wed, 29 Mar 2006 13:34:55 +0000 (13:34 +0000)]
Debugging code added.

18 years agoremoved unif_ty ref
Enrico Tassi [Wed, 29 Mar 2006 12:18:56 +0000 (12:18 +0000)]
removed unif_ty ref

18 years agoreverted the addition of _ to mistyped names
Enrico Tassi [Wed, 29 Mar 2006 12:13:16 +0000 (12:13 +0000)]
reverted the addition of _ to mistyped names

18 years agofew bits to debug the benchmark system
Enrico Tassi [Wed, 29 Mar 2006 12:07:55 +0000 (12:07 +0000)]
few bits to debug the benchmark system

18 years agodeals with colors
Enrico Tassi [Tue, 28 Mar 2006 08:41:01 +0000 (08:41 +0000)]
deals with colors

18 years agomore profiling and fixes for paramod
Enrico Tassi [Tue, 28 Mar 2006 08:22:51 +0000 (08:22 +0000)]
more profiling and fixes for paramod

18 years agoargs removed from equalities.
Andrea Asperti [Mon, 27 Mar 2006 15:02:32 +0000 (15:02 +0000)]
args removed from equalities.
New selection strategy. De morgan: 253 s.

18 years agoDebugging code commented out.
Claudio Sacerdoti Coen [Mon, 27 Mar 2006 14:14:52 +0000 (14:14 +0000)]
Debugging code commented out.

18 years ago* trust = true
Claudio Sacerdoti Coen [Mon, 27 Mar 2006 14:10:47 +0000 (14:10 +0000)]
* trust = true
* better pretty-printing of type-checking exceptions

18 years ago"Performance bug" fixed: I removed a whd in the does_not_occur function.
Claudio Sacerdoti Coen [Mon, 27 Mar 2006 14:01:26 +0000 (14:01 +0000)]
"Performance bug" fixed: I removed a whd in the does_not_occur function.
Consequences:
  1. incredible speed-up in the type-checking of certain inductive types
  2. "dummy" occurrences (i.e. occurrences that are doomed to disappear because
     of reduction) are now rejected (they used to be accepted). Coq has the
     same behaviour.

18 years agoSeveral "try ... with _ -> " specialized.
Claudio Sacerdoti Coen [Mon, 27 Mar 2006 12:21:48 +0000 (12:21 +0000)]
Several "try ... with _ -> " specialized.

18 years agoMore robust handling of Control-C.
Claudio Sacerdoti Coen [Mon, 27 Mar 2006 11:28:06 +0000 (11:28 +0000)]
More robust handling of Control-C.

18 years agoFlush stdout added in proper position.
Claudio Sacerdoti Coen [Mon, 27 Mar 2006 08:33:25 +0000 (08:33 +0000)]
Flush stdout added in proper position.

18 years agoignoring test_library{,.opt}
Stefano Zacchiroli [Fri, 24 Mar 2006 20:45:13 +0000 (20:45 +0000)]
ignoring test_library{,.opt}

18 years agoRecently introduced bug fixed in the kernel: a stack was "forgot" during
Claudio Sacerdoti Coen [Fri, 24 Mar 2006 18:33:30 +0000 (18:33 +0000)]
Recently introduced bug fixed in the kernel: a stack was "forgot" during
reduction of a MutCase.

18 years agoUnable to parse my own output. Fixed.
Claudio Sacerdoti Coen [Fri, 24 Mar 2006 18:02:18 +0000 (18:02 +0000)]
Unable to parse my own output. Fixed.

18 years ago% forgot in the output
Claudio Sacerdoti Coen [Fri, 24 Mar 2006 17:57:58 +0000 (17:57 +0000)]
% forgot in the output

18 years agoSerious test for the Coq library added (name test_library).
Claudio Sacerdoti Coen [Fri, 24 Mar 2006 17:56:35 +0000 (17:56 +0000)]
Serious test for the Coq library added (name test_library).
Input: a file that holds a list of URIs.
Output: the benchmark; the output file is also a valid input.
        In this case the output also prints the differences w.r.t. the
        last execution.
Ctrl-break can be used to interrupt the type-checking of a single URI.
An interactive question is posed to the user to decide if proceeding with
the next URIs or not.

18 years agomore error messages were on stdout :-(
Claudio Sacerdoti Coen [Fri, 24 Mar 2006 17:54:21 +0000 (17:54 +0000)]
more error messages were on stdout :-(

18 years agoerror message was printed on stdout
Claudio Sacerdoti Coen [Fri, 24 Mar 2006 17:52:05 +0000 (17:52 +0000)]
error message was printed on stdout

18 years agoColors are back! :-)
Claudio Sacerdoti Coen [Fri, 24 Mar 2006 16:07:10 +0000 (16:07 +0000)]
Colors are back! :-)

18 years agoNew unification and new matching.
Andrea Asperti [Fri, 24 Mar 2006 16:01:08 +0000 (16:01 +0000)]
New unification and new matching.

18 years agoLegend for profiling printed iff something is profiled.
Claudio Sacerdoti Coen [Fri, 24 Mar 2006 15:36:03 +0000 (15:36 +0000)]
Legend for profiling printed iff something is profiled.

18 years agofix
Enrico Tassi [Thu, 23 Mar 2006 11:12:15 +0000 (11:12 +0000)]
fix

18 years agofix
Enrico Tassi [Thu, 23 Mar 2006 10:49:30 +0000 (10:49 +0000)]
fix

18 years agoBest parameter setting for de morgan.
Andrea Asperti [Thu, 23 Mar 2006 10:33:41 +0000 (10:33 +0000)]
Best parameter setting for de morgan.
-- This line, and those below, will be ignored--

M    tactics/paramodulation/saturation.ml

18 years agofix
Enrico Tassi [Thu, 23 Mar 2006 09:06:06 +0000 (09:06 +0000)]
fix

18 years agoif DISTRIBUTED all targets require a depend-stamp
Enrico Tassi [Wed, 22 Mar 2006 14:29:21 +0000 (14:29 +0000)]
if DISTRIBUTED all targets require a depend-stamp

18 years ago:
Andrea Asperti [Wed, 22 Mar 2006 13:47:39 +0000 (13:47 +0000)]
:
This line, and those below, will be ignored--

M    tactics/paramodulation/utils.ml