]> matita.cs.unibo.it Git - helm.git/log
helm.git
14 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

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

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

14 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

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

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

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

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

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

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

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

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

14 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!)

14 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]!

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

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

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

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

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

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

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

14 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.

14 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!

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

14 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

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

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

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

14 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

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

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

14 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

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

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

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

14 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.

14 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).

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

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

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

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

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

14 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.

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

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

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

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

14 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

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

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

14 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.

14 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.

14 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

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

14 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.

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

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

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

14 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

14 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...)

14 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

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

14 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

14 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

14 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

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

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

14 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

14 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

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

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

14 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

14 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

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

14 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

14 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

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

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

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

14 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

14 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)

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

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

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

14 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

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

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

14 years agoadded auto_cache in the dupable status after an
Enrico Tassi [Mon, 5 Oct 2009 14:13:25 +0000 (14:13 +0000)]
added auto_cache in the dupable status after an
re-factoring and re-typing of the whole serialization
code.

14 years agonew ng_library module
Enrico Tassi [Mon, 5 Oct 2009 11:28:05 +0000 (11:28 +0000)]
new ng_library module

14 years agouffa
Enrico Tassi [Mon, 5 Oct 2009 07:56:27 +0000 (07:56 +0000)]
uffa

14 years ago...
Claudio Sacerdoti Coen [Sun, 4 Oct 2009 14:47:15 +0000 (14:47 +0000)]
...

14 years agoDoes not compile! Wrong unification hint?
Claudio Sacerdoti Coen [Sun, 4 Oct 2009 14:46:18 +0000 (14:46 +0000)]
Does not compile! Wrong unification hint?

14 years ago...
Claudio Sacerdoti Coen [Sun, 4 Oct 2009 14:43:48 +0000 (14:43 +0000)]
...

14 years ago...
Claudio Sacerdoti Coen [Sun, 4 Oct 2009 14:37:51 +0000 (14:37 +0000)]
...

14 years ago...
Claudio Sacerdoti Coen [Sun, 4 Oct 2009 14:35:30 +0000 (14:35 +0000)]
...

14 years ago...
Claudio Sacerdoti Coen [Sun, 4 Oct 2009 14:33:10 +0000 (14:33 +0000)]
...

14 years agohints fixed
Enrico Tassi [Fri, 2 Oct 2009 17:58:31 +0000 (17:58 +0000)]
hints fixed

14 years agofixed bug in coercion application, input/output swapped in unification
Enrico Tassi [Fri, 2 Oct 2009 17:58:08 +0000 (17:58 +0000)]
fixed bug in coercion application, input/output swapped in unification

14 years agoif the query has a completely flexible side, the empty result set is given
Enrico Tassi [Fri, 2 Oct 2009 17:55:38 +0000 (17:55 +0000)]
if the query has a completely flexible side, the empty result set is given

14 years agohints input is cleared from projection redexes
Enrico Tassi [Fri, 2 Oct 2009 17:55:03 +0000 (17:55 +0000)]
hints input is cleared from projection redexes