]>
matita.cs.unibo.it Git - helm.git/log
Enrico Tassi [Fri, 16 Oct 2009 14:02:54 +0000 (14:02 +0000)]
...
Enrico Tassi [Fri, 16 Oct 2009 14:01:18 +0000 (14:01 +0000)]
...
Enrico Tassi [Fri, 16 Oct 2009 12:41:41 +0000 (12:41 +0000)]
debug idem for auto added
Enrico Tassi [Fri, 16 Oct 2009 12:41:22 +0000 (12:41 +0000)]
new lambda instros and better logging
Enrico Tassi [Fri, 16 Oct 2009 12:40:36 +0000 (12:40 +0000)]
better indexing for auto
Enrico Tassi [Fri, 16 Oct 2009 12:40:16 +0000 (12:40 +0000)]
some work for auto
Enrico Tassi [Fri, 16 Oct 2009 12:40:05 +0000 (12:40 +0000)]
some work for auto
Enrico Tassi [Fri, 16 Oct 2009 12:39:27 +0000 (12:39 +0000)]
removed optimization potentially unsound
Enrico Tassi [Fri, 16 Oct 2009 12:36:12 +0000 (12:36 +0000)]
...
Claudio Sacerdoti Coen [Thu, 15 Oct 2009 13:59:31 +0000 (13:59 +0000)]
Profiling code integrated.
Cosimo Oliboni [Thu, 15 Oct 2009 08:47:14 +0000 (08:47 +0000)]
freescale porting, work in progress
Claudio Sacerdoti Coen [Wed, 14 Oct 2009 21:03:49 +0000 (21:03 +0000)]
Debugging improved.
Claudio Sacerdoti Coen [Wed, 14 Oct 2009 21:01:12 +0000 (21:01 +0000)]
Benchmarking integrated in folding/unfolding.
Cosimo Oliboni [Wed, 14 Oct 2009 20:52:07 +0000 (20:52 +0000)]
freescale porting, work in progress
Enrico Tassi [Wed, 14 Oct 2009 15:13:27 +0000 (15:13 +0000)]
cantor...
Enrico Tassi [Wed, 14 Oct 2009 15:05:15 +0000 (15:05 +0000)]
...
Enrico Tassi [Wed, 14 Oct 2009 14:38:02 +0000 (14:38 +0000)]
hints were not used by reduction machines on heads
Enrico Tassi [Wed, 14 Oct 2009 13:45:33 +0000 (13:45 +0000)]
...
Enrico Tassi [Wed, 14 Oct 2009 13:35:24 +0000 (13:35 +0000)]
ncheck is not erased
Enrico Tassi [Wed, 14 Oct 2009 13:12:32 +0000 (13:12 +0000)]
...
Enrico Tassi [Wed, 14 Oct 2009 13:10:22 +0000 (13:10 +0000)]
...
Enrico Tassi [Wed, 14 Oct 2009 13:09:04 +0000 (13:09 +0000)]
...
Enrico Tassi [Wed, 14 Oct 2009 13:08:11 +0000 (13:08 +0000)]
...
Enrico Tassi [Wed, 14 Oct 2009 12:52:06 +0000 (12:52 +0000)]
minor fix
Enrico Tassi [Wed, 14 Oct 2009 12:49:08 +0000 (12:49 +0000)]
tons of typo fixed
Claudio Sacerdoti Coen [Wed, 14 Oct 2009 11:19:03 +0000 (11:19 +0000)]
Error message fixed (dereferencing must be done eagerly, not when the error is
actually printed!)
Claudio Sacerdoti Coen [Wed, 14 Oct 2009 09:37:50 +0000 (09:37 +0000)]
Serious bug fixed: fix_sorts used to allow inference of Type[0]:Type[0]!
Enrico Tassi [Wed, 14 Oct 2009 08:51:13 +0000 (08:51 +0000)]
CProp uri fixed
Enrico Tassi [Tue, 13 Oct 2009 16:59:55 +0000 (16:59 +0000)]
...
Enrico Tassi [Tue, 13 Oct 2009 16:15:03 +0000 (16:15 +0000)]
...
Enrico Tassi [Tue, 13 Oct 2009 15:53:50 +0000 (15:53 +0000)]
...
Enrico Tassi [Tue, 13 Oct 2009 15:50:11 +0000 (15:50 +0000)]
...
Enrico Tassi [Tue, 13 Oct 2009 15:47:03 +0000 (15:47 +0000)]
...
Enrico Tassi [Tue, 13 Oct 2009 15:13:09 +0000 (15:13 +0000)]
...
Wilmer Ricciotti [Tue, 13 Oct 2009 14:57:30 +0000 (14:57 +0000)]
Experimental scripts for nth-order rewriting principles.
Enrico Tassi [Tue, 13 Oct 2009 13:36:32 +0000 (13:36 +0000)]
relocate is hopefully fixed once and for-all!
Enrico Tassi [Tue, 13 Oct 2009 11:27:03 +0000 (11:27 +0000)]
better screenshot
Cosimo Oliboni [Tue, 13 Oct 2009 11:18:49 +0000 (11:18 +0000)]
freescale porting, work in progress
Enrico Tassi [Tue, 13 Oct 2009 11:13:46 +0000 (11:13 +0000)]
relocate fixed
Enrico Tassi [Tue, 13 Oct 2009 10:14:50 +0000 (10:14 +0000)]
better ppcontext
Enrico Tassi [Tue, 13 Oct 2009 10:14:36 +0000 (10:14 +0000)]
better ppcontext
Enrico Tassi [Tue, 13 Oct 2009 10:14:07 +0000 (10:14 +0000)]
debug + relocate uses Prop instead of (Prop Prop)... we should think a better solution
Enrico Tassi [Tue, 13 Oct 2009 09:43:02 +0000 (09:43 +0000)]
one mode debug item
Enrico Tassi [Tue, 13 Oct 2009 09:36:39 +0000 (09:36 +0000)]
...
Enrico Tassi [Tue, 13 Oct 2009 09:33:40 +0000 (09:33 +0000)]
no mode middle age debug menu
Enrico Tassi [Tue, 13 Oct 2009 09:21:04 +0000 (09:21 +0000)]
more comments
Enrico Tassi [Tue, 13 Oct 2009 07:56:48 +0000 (07:56 +0000)]
...
Enrico Tassi [Mon, 12 Oct 2009 20:08:36 +0000 (20:08 +0000)]
...
Claudio Sacerdoti Coen [Mon, 12 Oct 2009 17:38:50 +0000 (17:38 +0000)]
1) Bug fixed: the case Meta(i) vs Meta(i) was handled in a particular way,
but the case Meta(i) vs (Appl (Meta(j),...)) that reduces to Meta(i) was
not. As a result, a tempeted self assegniment yielded strange errors.
Fixed by more aggressively unwinding the subst during fo_unif.
2) Major re-organization of the code to gain some speed in Oliboni's stuff.
The idea is that of introducing a new internal exception KeepReducing
used to signal that, after a fo_unif, it still makes sense to fall back
to machines. Only if it does not it makes sense to distinguish between
Failures and Uncertain and the latter test can now be implemented more
lazily w.r.t. the old version that used to call metas_of_term on the
unwinded machines (that are potentially HUGE).
With this modification, all Oliboni's tests terminate, even if they are
still very slow compared to the height=0 strategy. Moreover, the tests
show that unification on closed terms can still be 4x slower than conversion,
which is partially unexpected.
Claudio Sacerdoti Coen [Mon, 12 Oct 2009 17:04:46 +0000 (17:04 +0000)]
Bug fixed: in case of (t ...) where t has flexible type, a failure obtained
without extending ... (since this could cause divergence) should be considered
an uncertain (since extension may be necessary).
Claudio Sacerdoti Coen [Mon, 12 Oct 2009 16:03:39 +0000 (16:03 +0000)]
Typo fixed.
Enrico Tassi [Mon, 12 Oct 2009 16:00:29 +0000 (16:00 +0000)]
added last 10 months work...
Enrico Tassi [Mon, 12 Oct 2009 15:31:48 +0000 (15:31 +0000)]
...
Enrico Tassi [Mon, 12 Oct 2009 15:28:50 +0000 (15:28 +0000)]
...
Enrico Tassi [Mon, 12 Oct 2009 14:27:36 +0000 (14:27 +0000)]
new standard library inside path
Claudio Sacerdoti Coen [Mon, 12 Oct 2009 14:22:34 +0000 (14:22 +0000)]
Closed metas must have closed (expected) types.
Claudio Sacerdoti Coen [Mon, 12 Oct 2009 13:34:42 +0000 (13:34 +0000)]
Improved debugging code.
Enrico Tassi [Mon, 12 Oct 2009 09:30:47 +0000 (09:30 +0000)]
...
Enrico Tassi [Mon, 12 Oct 2009 08:10:14 +0000 (08:10 +0000)]
...
Enrico Tassi [Mon, 12 Oct 2009 08:05:05 +0000 (08:05 +0000)]
...
Enrico Tassi [Sun, 11 Oct 2009 21:42:58 +0000 (21:42 +0000)]
no need to compile/install the standard library. if included it
will be compiled on the fly in user space
Enrico Tassi [Sun, 11 Oct 2009 21:42:23 +0000 (21:42 +0000)]
can live without library db
Enrico Tassi [Sun, 11 Oct 2009 13:54:47 +0000 (13:54 +0000)]
auto with intro
Claudio Sacerdoti Coen [Thu, 8 Oct 2009 16:13:54 +0000 (16:13 +0000)]
A new switch to activate/deactive nCicReduction pretty printing.
Claudio Sacerdoti Coen [Thu, 8 Oct 2009 16:07:20 +0000 (16:07 +0000)]
Printing extremely large terms no longer raises Failure.
Ferruccio Guidi [Thu, 8 Oct 2009 14:43:54 +0000 (14:43 +0000)]
drgAut: we fixed the order of multi application arguments
drgBrg: we started the translation from drg to brg
Enrico Tassi [Thu, 8 Oct 2009 10:01:46 +0000 (10:01 +0000)]
removed misleading context
Enrico Tassi [Thu, 8 Oct 2009 09:59:20 +0000 (09:59 +0000)]
new discrimination tree instantiation with
inverse De Brujin indexes.
Enrico Tassi [Thu, 8 Oct 2009 09:48:24 +0000 (09:48 +0000)]
avoid warning
Enrico Tassi [Thu, 8 Oct 2009 09:47:47 +0000 (09:47 +0000)]
...
Enrico Tassi [Wed, 7 Oct 2009 20:18:17 +0000 (20:18 +0000)]
removed printing
Ferruccio Guidi [Wed, 7 Oct 2009 20:05:02 +0000 (20:05 +0000)]
we enabled the new style xml exportation, in particular for dual_rg
Claudio Sacerdoti Coen [Wed, 7 Oct 2009 18:18:00 +0000 (18:18 +0000)]
Performance improvement by preserving more sharing. Visible in Oliboni's
development. But still slower then old matita (but pheraps on different data...)
Enrico Tassi [Wed, 7 Oct 2009 13:57:57 +0000 (13:57 +0000)]
terms indexed in the automation cache are saturated
Enrico Tassi [Wed, 7 Oct 2009 13:53:01 +0000 (13:53 +0000)]
short names
Enrico Tassi [Wed, 7 Oct 2009 13:35:37 +0000 (13:35 +0000)]
auto works on the regular tactics status
Enrico Tassi [Wed, 7 Oct 2009 13:35:20 +0000 (13:35 +0000)]
the wrap function takes a string argument so that we know
which wrapper function failed
Enrico Tassi [Wed, 7 Oct 2009 13:34:17 +0000 (13:34 +0000)]
unfocus can be performed also if all goals are closed
Claudio Sacerdoti Coen [Wed, 7 Oct 2009 11:50:03 +0000 (11:50 +0000)]
Debugging code commented out.
Enrico Tassi [Wed, 7 Oct 2009 09:48:36 +0000 (09:48 +0000)]
fixed Ref generation
Claudio Sacerdoti Coen [Wed, 7 Oct 2009 09:43:18 +0000 (09:43 +0000)]
- oCic2NCic and nCic2OCic moved to ng_library
- spurious dependencies of ng_library on modules that need to convert
old tables added; to be removed in the future
Ferruccio Guidi [Tue, 6 Oct 2009 18:20:27 +0000 (18:20 +0000)]
drgOutput: bug fix
we maked the non-tail recursive functions in: lib, common, automath, dual_rg
Enrico Tassi [Tue, 6 Oct 2009 15:04:24 +0000 (15:04 +0000)]
removed useless stuff
Enrico Tassi [Tue, 6 Oct 2009 15:04:00 +0000 (15:04 +0000)]
some fixes
Ferruccio Guidi [Tue, 6 Oct 2009 14:46:38 +0000 (14:46 +0000)]
drg: we added the "positive projection" in environments
top: we enabled the automath/drg transformation
Enrico Tassi [Tue, 6 Oct 2009 14:38:00 +0000 (14:38 +0000)]
fixed constructor on non inductive type
Wilmer Ricciotti [Tue, 6 Oct 2009 14:13:51 +0000 (14:13 +0000)]
Syntax highlighting for 'ninverter' keyword
Wilmer Ricciotti [Tue, 6 Oct 2009 14:08:58 +0000 (14:08 +0000)]
Inverters/Inversion:
- fixed a bug with left parameters and inversion principles
- hooked automatic definition of inversion principles to the declaration of
inductive types
Enrico Tassi [Tue, 6 Oct 2009 13:37:01 +0000 (13:37 +0000)]
unification pps can be activated by the menu debug
Enrico Tassi [Tue, 6 Oct 2009 13:16:08 +0000 (13:16 +0000)]
...
Enrico Tassi [Tue, 6 Oct 2009 11:48:02 +0000 (11:48 +0000)]
nAuto W.I.P.
Claudio Sacerdoti Coen [Tue, 6 Oct 2009 08:16:10 +0000 (08:16 +0000)]
Improved error message.
Ferruccio Guidi [Mon, 5 Oct 2009 20:55:46 +0000 (20:55 +0000)]
new toplevel: tentative implementation with more CPS
Ferruccio Guidi [Mon, 5 Oct 2009 16:05:53 +0000 (16:05 +0000)]
- common/entity: new format for kernel entities
- common/library: new CPS infrastructure for XML exportation
- toplevel/meta: now uses common/entity
- dual_rg/drg: some fixes
- dual_rg/drgOutput: XML exportation started (alpha-conversion is missing)
Claudio Sacerdoti Coen [Mon, 5 Oct 2009 15:39:55 +0000 (15:39 +0000)]
...
Claudio Sacerdoti Coen [Mon, 5 Oct 2009 15:06:32 +0000 (15:06 +0000)]
...
Claudio Sacerdoti Coen [Mon, 5 Oct 2009 14:59:23 +0000 (14:59 +0000)]
...
Enrico Tassi [Mon, 5 Oct 2009 14:53:10 +0000 (14:53 +0000)]
auto and auto_paramod are in nAuto
Enrico Tassi [Mon, 5 Oct 2009 14:36:13 +0000 (14:36 +0000)]
new file for auto
Enrico Tassi [Mon, 5 Oct 2009 14:23:02 +0000 (14:23 +0000)]
downcast removed