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

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

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

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

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

15 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?

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

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

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

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

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

15 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

15 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

15 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

15 years agoprojections redex (proj (mk_foo ...)) where mk_foo
Enrico Tassi [Fri, 2 Oct 2009 17:54:16 +0000 (17:54 +0000)]
projections redex (proj (mk_foo ...)) where mk_foo
is explicit (not the result of a reduction) are
always fired.

on the contrary, when the delta avoids the reduction
of a projetion (since the arg reduces to mk_foo but
for a smaller delta) we store in stack not the reduct
but its original version (before reducing it to delta=0).

This seems nice anyway, and a FIXME is left in the code

15 years agoUpdated command ninverter. Syntax:
Wilmer Ricciotti [Fri, 2 Oct 2009 14:50:12 +0000 (14:50 +0000)]
Updated command ninverter. Syntax:

ninverter <id> for <indty> [<selection>] [: <target_sort>]

It is the same as the previous inverter except that:

- <selection> is now optional (when it is omitted, every index is selected)
- the user is allowed to specify a <target_sort> (when it is omitted, ninverter
  defaults to Prop, as it was the case for inverter)

15 years agobetter nlet rec boxing
Enrico Tassi [Fri, 2 Oct 2009 09:45:52 +0000 (09:45 +0000)]
better nlet rec boxing

15 years agoWrong context (again!)
Claudio Sacerdoti Coen [Fri, 2 Oct 2009 09:21:39 +0000 (09:21 +0000)]
Wrong context (again!)

15 years ago...
Claudio Sacerdoti Coen [Fri, 2 Oct 2009 09:08:40 +0000 (09:08 +0000)]
...

15 years agobetter static html pages, now they are generted in the install location
Ferruccio Guidi [Thu, 1 Oct 2009 21:31:15 +0000 (21:31 +0000)]
better static html pages, now they are generted in the install location

15 years ago- delift_type_wrt_term fixed in many ways
Enrico Tassi [Thu, 1 Oct 2009 15:04:27 +0000 (15:04 +0000)]
- delift_type_wrt_term fixed in many ways
  - as a side effect let in expty propagation works
  - as a side effect lambda_intros now works
- is_flexible (delift) improved in case: (? args) ---subst---> (\lambda .?) args

15 years agofixed the type of tactic_term, attributes were useless
Enrico Tassi [Thu, 1 Oct 2009 10:00:40 +0000 (10:00 +0000)]
fixed the type of tactic_term, attributes were useless

15 years agoinstantiate merges tags
Enrico Tassi [Thu, 1 Oct 2009 09:49:13 +0000 (09:49 +0000)]
instantiate merges tags

15 years agoadded sortification for (? args), untested code
Enrico Tassi [Thu, 1 Oct 2009 09:36:12 +0000 (09:36 +0000)]
added sortification for (? args), untested code

15 years agosortification simplified
Enrico Tassi [Thu, 1 Oct 2009 08:46:53 +0000 (08:46 +0000)]
sortification simplified

15 years agofixed off-by-one
Enrico Tassi [Thu, 1 Oct 2009 08:46:21 +0000 (08:46 +0000)]
fixed off-by-one

15 years agoWith this hint, it diverges.
Claudio Sacerdoti Coen [Wed, 30 Sep 2009 20:28:17 +0000 (20:28 +0000)]
With this hint, it diverges.

15 years agorewritten instantiate code
Enrico Tassi [Wed, 30 Sep 2009 20:19:38 +0000 (20:19 +0000)]
rewritten instantiate code

15 years agoNew datatype for metasenv/subst: full fledged attributes in place of optional
Claudio Sacerdoti Coen [Wed, 30 Sep 2009 13:48:03 +0000 (13:48 +0000)]
New datatype for metasenv/subst: full fledged attributes in place of optional
strings.

15 years agoAdded initial support for inversion principles in Matita NG.
Wilmer Ricciotti [Wed, 30 Sep 2009 13:35:06 +0000 (13:35 +0000)]
Added initial support for inversion principles in Matita NG.
Added a case_tac tactical, performing goal selection matching metavariables by
means of their associated tag.
Added tagged implicits, which are refined as tagged metavariables.

15 years agoBetter (but still broken) fix for the case ?sort vs ?term.
Claudio Sacerdoti Coen [Wed, 30 Sep 2009 12:55:49 +0000 (12:55 +0000)]
Better (but still broken) fix for the case ?sort vs ?term.
To implement the right thing, we need to be able to mark metas as sort without
using the fact that their type is an Implicit.

15 years agoThe term contains dummy.conv that was searched over the net.
Claudio Sacerdoti Coen [Wed, 30 Sep 2009 08:18:31 +0000 (08:18 +0000)]
The term contains dummy.conv that was searched over the net.

15 years ago1) improved (???) debugging, with
Claudio Sacerdoti Coen [Tue, 29 Sep 2009 17:28:24 +0000 (17:28 +0000)]
1) improved (???) debugging, with
  1.1 more messages (good)
  1.2 messages for exceptions (very good)
  1.3 vim folding/unfolding (good or very bad?)
2) bug partially fixed (to be improved/totally fixed):
   when we unify a ?n:? vs a term t, we need to check
   that t is a sort! (or a flexible term??? what to do in that case?)
   otherwise we can get ?n := O and ?1:?2:?n=0 which is a not
   well typed metasenv. Hence boom later.