]> matita.cs.unibo.it Git - helm.git/log
helm.git
15 years ago...
Enrico Tassi [Fri, 16 Oct 2009 14:02:54 +0000 (14:02 +0000)]
...

15 years ago...
Enrico Tassi [Fri, 16 Oct 2009 14:01:18 +0000 (14:01 +0000)]
...

15 years agodebug idem for auto added
Enrico Tassi [Fri, 16 Oct 2009 12:41:41 +0000 (12:41 +0000)]
debug idem for auto added

15 years agonew lambda instros and better logging
Enrico Tassi [Fri, 16 Oct 2009 12:41:22 +0000 (12:41 +0000)]
new lambda instros and better logging

15 years agobetter indexing for auto
Enrico Tassi [Fri, 16 Oct 2009 12:40:36 +0000 (12:40 +0000)]
better indexing for auto

15 years agosome work for auto
Enrico Tassi [Fri, 16 Oct 2009 12:40:16 +0000 (12:40 +0000)]
some work for auto

15 years agosome work for auto
Enrico Tassi [Fri, 16 Oct 2009 12:40:05 +0000 (12:40 +0000)]
some work for auto

15 years agoremoved optimization potentially unsound
Enrico Tassi [Fri, 16 Oct 2009 12:39:27 +0000 (12:39 +0000)]
removed optimization potentially unsound

15 years ago...
Enrico Tassi [Fri, 16 Oct 2009 12:36:12 +0000 (12:36 +0000)]
...

15 years agoProfiling code integrated.
Claudio Sacerdoti Coen [Thu, 15 Oct 2009 13:59:31 +0000 (13:59 +0000)]
Profiling code integrated.

15 years ago freescale porting, work in progress
Cosimo Oliboni [Thu, 15 Oct 2009 08:47:14 +0000 (08:47 +0000)]
 freescale porting, work in progress

15 years agoDebugging improved.
Claudio Sacerdoti Coen [Wed, 14 Oct 2009 21:03:49 +0000 (21:03 +0000)]
Debugging improved.

15 years agoBenchmarking integrated in folding/unfolding.
Claudio Sacerdoti Coen [Wed, 14 Oct 2009 21:01:12 +0000 (21:01 +0000)]
Benchmarking integrated in folding/unfolding.

15 years ago freescale porting, work in progress
Cosimo Oliboni [Wed, 14 Oct 2009 20:52:07 +0000 (20:52 +0000)]
 freescale porting, work in progress

15 years agocantor...
Enrico Tassi [Wed, 14 Oct 2009 15:13:27 +0000 (15:13 +0000)]
cantor...

15 years ago...
Enrico Tassi [Wed, 14 Oct 2009 15:05:15 +0000 (15:05 +0000)]
...

15 years agohints were not used by reduction machines on heads
Enrico Tassi [Wed, 14 Oct 2009 14:38:02 +0000 (14:38 +0000)]
hints were not used by reduction machines on heads

15 years ago...
Enrico Tassi [Wed, 14 Oct 2009 13:45:33 +0000 (13:45 +0000)]
...

15 years agoncheck is not erased
Enrico Tassi [Wed, 14 Oct 2009 13:35:24 +0000 (13:35 +0000)]
ncheck is not erased

15 years ago...
Enrico Tassi [Wed, 14 Oct 2009 13:12:32 +0000 (13:12 +0000)]
...

15 years ago...
Enrico Tassi [Wed, 14 Oct 2009 13:10:22 +0000 (13:10 +0000)]
...

15 years ago...
Enrico Tassi [Wed, 14 Oct 2009 13:09:04 +0000 (13:09 +0000)]
...

15 years ago...
Enrico Tassi [Wed, 14 Oct 2009 13:08:11 +0000 (13:08 +0000)]
...

15 years agominor fix
Enrico Tassi [Wed, 14 Oct 2009 12:52:06 +0000 (12:52 +0000)]
minor fix

15 years agotons of typo fixed
Enrico Tassi [Wed, 14 Oct 2009 12:49:08 +0000 (12:49 +0000)]
tons of typo fixed

15 years agoError message fixed (dereferencing must be done eagerly, not when the error is
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!)

15 years agoSerious bug fixed: fix_sorts used to allow inference of Type[0]:Type[0]!
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]!

15 years agoCProp uri fixed
Enrico Tassi [Wed, 14 Oct 2009 08:51:13 +0000 (08:51 +0000)]
CProp uri fixed

15 years ago...
Enrico Tassi [Tue, 13 Oct 2009 16:59:55 +0000 (16:59 +0000)]
...

15 years ago...
Enrico Tassi [Tue, 13 Oct 2009 16:15:03 +0000 (16:15 +0000)]
...

15 years ago...
Enrico Tassi [Tue, 13 Oct 2009 15:53:50 +0000 (15:53 +0000)]
...

15 years ago...
Enrico Tassi [Tue, 13 Oct 2009 15:50:11 +0000 (15:50 +0000)]
...

15 years ago...
Enrico Tassi [Tue, 13 Oct 2009 15:47:03 +0000 (15:47 +0000)]
...

15 years ago...
Enrico Tassi [Tue, 13 Oct 2009 15:13:09 +0000 (15:13 +0000)]
...

15 years agoExperimental scripts for nth-order rewriting principles.
Wilmer Ricciotti [Tue, 13 Oct 2009 14:57:30 +0000 (14:57 +0000)]
Experimental scripts for nth-order rewriting principles.

15 years agorelocate is hopefully fixed once and for-all!
Enrico Tassi [Tue, 13 Oct 2009 13:36:32 +0000 (13:36 +0000)]
relocate is hopefully fixed once and for-all!

15 years agobetter screenshot
Enrico Tassi [Tue, 13 Oct 2009 11:27:03 +0000 (11:27 +0000)]
better screenshot

15 years ago freescale porting, work in progress
Cosimo Oliboni [Tue, 13 Oct 2009 11:18:49 +0000 (11:18 +0000)]
 freescale porting, work in progress

15 years agorelocate fixed
Enrico Tassi [Tue, 13 Oct 2009 11:13:46 +0000 (11:13 +0000)]
relocate fixed

15 years agobetter ppcontext
Enrico Tassi [Tue, 13 Oct 2009 10:14:50 +0000 (10:14 +0000)]
better ppcontext

15 years agobetter ppcontext
Enrico Tassi [Tue, 13 Oct 2009 10:14:36 +0000 (10:14 +0000)]
better ppcontext

15 years agodebug + relocate uses Prop instead of (Prop Prop)... we should think a better solution
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

15 years agoone mode debug item
Enrico Tassi [Tue, 13 Oct 2009 09:43:02 +0000 (09:43 +0000)]
one mode debug item

15 years ago...
Enrico Tassi [Tue, 13 Oct 2009 09:36:39 +0000 (09:36 +0000)]
...

15 years agono mode middle age debug menu
Enrico Tassi [Tue, 13 Oct 2009 09:33:40 +0000 (09:33 +0000)]
no mode middle age debug menu

15 years agomore comments
Enrico Tassi [Tue, 13 Oct 2009 09:21:04 +0000 (09:21 +0000)]
more comments

15 years ago...
Enrico Tassi [Tue, 13 Oct 2009 07:56:48 +0000 (07:56 +0000)]
...

15 years ago...
Enrico Tassi [Mon, 12 Oct 2009 20:08:36 +0000 (20:08 +0000)]
...

15 years ago1) Bug fixed: the case Meta(i) vs Meta(i) was handled in a particular way,
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.

15 years agoBug fixed: in case of (t ...) where t has flexible type, a failure obtained
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).

15 years agoTypo fixed.
Claudio Sacerdoti Coen [Mon, 12 Oct 2009 16:03:39 +0000 (16:03 +0000)]
Typo fixed.

15 years agoadded last 10 months work...
Enrico Tassi [Mon, 12 Oct 2009 16:00:29 +0000 (16:00 +0000)]
added last 10 months work...

15 years ago...
Enrico Tassi [Mon, 12 Oct 2009 15:31:48 +0000 (15:31 +0000)]
...

15 years ago...
Enrico Tassi [Mon, 12 Oct 2009 15:28:50 +0000 (15:28 +0000)]
...

15 years agonew standard library inside path
Enrico Tassi [Mon, 12 Oct 2009 14:27:36 +0000 (14:27 +0000)]
new standard library inside path

15 years agoClosed metas must have closed (expected) types.
Claudio Sacerdoti Coen [Mon, 12 Oct 2009 14:22:34 +0000 (14:22 +0000)]
Closed metas must have closed (expected) types.

15 years agoImproved debugging code.
Claudio Sacerdoti Coen [Mon, 12 Oct 2009 13:34:42 +0000 (13:34 +0000)]
Improved debugging code.

15 years ago...
Enrico Tassi [Mon, 12 Oct 2009 09:30:47 +0000 (09:30 +0000)]
...

15 years ago...
Enrico Tassi [Mon, 12 Oct 2009 08:10:14 +0000 (08:10 +0000)]
...

15 years ago...
Enrico Tassi [Mon, 12 Oct 2009 08:05:05 +0000 (08:05 +0000)]
...

15 years agono need to compile/install the standard library. if included it
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

15 years agocan live without library db
Enrico Tassi [Sun, 11 Oct 2009 21:42:23 +0000 (21:42 +0000)]
can live without library db

15 years agoauto with intro
Enrico Tassi [Sun, 11 Oct 2009 13:54:47 +0000 (13:54 +0000)]
auto with intro

15 years agoA new switch to activate/deactive nCicReduction pretty printing.
Claudio Sacerdoti Coen [Thu, 8 Oct 2009 16:13:54 +0000 (16:13 +0000)]
A new switch to activate/deactive nCicReduction pretty printing.

15 years agoPrinting extremely large terms no longer raises Failure.
Claudio Sacerdoti Coen [Thu, 8 Oct 2009 16:07:20 +0000 (16:07 +0000)]
Printing extremely large terms no longer raises Failure.

15 years agodrgAut: we fixed the order of multi application arguments
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

15 years agoremoved misleading context
Enrico Tassi [Thu, 8 Oct 2009 10:01:46 +0000 (10:01 +0000)]
removed misleading context

15 years agonew discrimination tree instantiation with
Enrico Tassi [Thu, 8 Oct 2009 09:59:20 +0000 (09:59 +0000)]
new discrimination tree instantiation with
inverse De Brujin indexes.

15 years agoavoid warning
Enrico Tassi [Thu, 8 Oct 2009 09:48:24 +0000 (09:48 +0000)]
avoid warning

15 years ago...
Enrico Tassi [Thu, 8 Oct 2009 09:47:47 +0000 (09:47 +0000)]
...

15 years agoremoved printing
Enrico Tassi [Wed, 7 Oct 2009 20:18:17 +0000 (20:18 +0000)]
removed printing

15 years agowe enabled the new style xml exportation, in particular for dual_rg
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

15 years agoPerformance improvement by preserving more sharing. Visible in Oliboni's
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...)

15 years agoterms indexed in the automation cache are saturated
Enrico Tassi [Wed, 7 Oct 2009 13:57:57 +0000 (13:57 +0000)]
terms indexed in the automation cache are saturated

15 years agoshort names
Enrico Tassi [Wed, 7 Oct 2009 13:53:01 +0000 (13:53 +0000)]
short names

15 years agoauto works on the regular tactics status
Enrico Tassi [Wed, 7 Oct 2009 13:35:37 +0000 (13:35 +0000)]
auto works on the regular tactics status

15 years agothe wrap function takes a string argument so that we know
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

15 years agounfocus can be performed also if all goals are closed
Enrico Tassi [Wed, 7 Oct 2009 13:34:17 +0000 (13:34 +0000)]
unfocus can be performed also if all goals are closed

15 years agoDebugging code commented out.
Claudio Sacerdoti Coen [Wed, 7 Oct 2009 11:50:03 +0000 (11:50 +0000)]
Debugging code commented out.

15 years agofixed Ref generation
Enrico Tassi [Wed, 7 Oct 2009 09:48:36 +0000 (09:48 +0000)]
fixed Ref generation

15 years ago- oCic2NCic and nCic2OCic moved to ng_library
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

15 years agodrgOutput: bug fix
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

15 years agoremoved useless stuff
Enrico Tassi [Tue, 6 Oct 2009 15:04:24 +0000 (15:04 +0000)]
removed useless stuff

15 years agosome fixes
Enrico Tassi [Tue, 6 Oct 2009 15:04:00 +0000 (15:04 +0000)]
some fixes

15 years agodrg: we added the "positive projection" in environments
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

15 years agofixed constructor on non inductive type
Enrico Tassi [Tue, 6 Oct 2009 14:38:00 +0000 (14:38 +0000)]
fixed constructor on non inductive type

15 years agoSyntax highlighting for 'ninverter' keyword
Wilmer Ricciotti [Tue, 6 Oct 2009 14:13:51 +0000 (14:13 +0000)]
Syntax highlighting for 'ninverter' keyword

15 years agoInverters/Inversion:
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

15 years agounification pps can be activated by the menu debug
Enrico Tassi [Tue, 6 Oct 2009 13:37:01 +0000 (13:37 +0000)]
unification pps can be activated by the menu debug

15 years ago...
Enrico Tassi [Tue, 6 Oct 2009 13:16:08 +0000 (13:16 +0000)]
...

15 years agonAuto W.I.P.
Enrico Tassi [Tue, 6 Oct 2009 11:48:02 +0000 (11:48 +0000)]
nAuto W.I.P.

15 years agoImproved error message.
Claudio Sacerdoti Coen [Tue, 6 Oct 2009 08:16:10 +0000 (08:16 +0000)]
Improved error message.

15 years agonew toplevel: tentative implementation with more CPS
Ferruccio Guidi [Mon, 5 Oct 2009 20:55:46 +0000 (20:55 +0000)]
new toplevel: tentative implementation with more CPS

15 years ago- common/entity: new format for kernel entities
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)

15 years ago...
Claudio Sacerdoti Coen [Mon, 5 Oct 2009 15:39:55 +0000 (15:39 +0000)]
...

15 years ago...
Claudio Sacerdoti Coen [Mon, 5 Oct 2009 15:06:32 +0000 (15:06 +0000)]
...

15 years ago...
Claudio Sacerdoti Coen [Mon, 5 Oct 2009 14:59:23 +0000 (14:59 +0000)]
...

15 years agoauto and auto_paramod are in nAuto
Enrico Tassi [Mon, 5 Oct 2009 14:53:10 +0000 (14:53 +0000)]
auto and auto_paramod are in nAuto

15 years agonew file for auto
Enrico Tassi [Mon, 5 Oct 2009 14:36:13 +0000 (14:36 +0000)]
new file for auto

15 years agodowncast removed
Enrico Tassi [Mon, 5 Oct 2009 14:23:02 +0000 (14:23 +0000)]
downcast removed