]>
matita.cs.unibo.it Git - helm.git/log
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
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.
Enrico Tassi [Mon, 5 Oct 2009 11:28:05 +0000 (11:28 +0000)]
new ng_library module
Enrico Tassi [Mon, 5 Oct 2009 07:56:27 +0000 (07:56 +0000)]
uffa
Claudio Sacerdoti Coen [Sun, 4 Oct 2009 14:47:15 +0000 (14:47 +0000)]
...
Claudio Sacerdoti Coen [Sun, 4 Oct 2009 14:46:18 +0000 (14:46 +0000)]
Does not compile! Wrong unification hint?
Claudio Sacerdoti Coen [Sun, 4 Oct 2009 14:43:48 +0000 (14:43 +0000)]
...
Claudio Sacerdoti Coen [Sun, 4 Oct 2009 14:37:51 +0000 (14:37 +0000)]
...
Claudio Sacerdoti Coen [Sun, 4 Oct 2009 14:35:30 +0000 (14:35 +0000)]
...
Claudio Sacerdoti Coen [Sun, 4 Oct 2009 14:33:10 +0000 (14:33 +0000)]
...
Enrico Tassi [Fri, 2 Oct 2009 17:58:31 +0000 (17:58 +0000)]
hints fixed
Enrico Tassi [Fri, 2 Oct 2009 17:58:08 +0000 (17:58 +0000)]
fixed bug in coercion application, input/output swapped in unification
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
Enrico Tassi [Fri, 2 Oct 2009 17:55:03 +0000 (17:55 +0000)]
hints input is cleared from projection redexes
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
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)
Enrico Tassi [Fri, 2 Oct 2009 09:45:52 +0000 (09:45 +0000)]
better nlet rec boxing
Claudio Sacerdoti Coen [Fri, 2 Oct 2009 09:21:39 +0000 (09:21 +0000)]
Wrong context (again!)
Claudio Sacerdoti Coen [Fri, 2 Oct 2009 09:08:40 +0000 (09:08 +0000)]
...
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
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
Enrico Tassi [Thu, 1 Oct 2009 10:00:40 +0000 (10:00 +0000)]
fixed the type of tactic_term, attributes were useless
Enrico Tassi [Thu, 1 Oct 2009 09:49:13 +0000 (09:49 +0000)]
instantiate merges tags
Enrico Tassi [Thu, 1 Oct 2009 09:36:12 +0000 (09:36 +0000)]
added sortification for (? args), untested code
Enrico Tassi [Thu, 1 Oct 2009 08:46:53 +0000 (08:46 +0000)]
sortification simplified
Enrico Tassi [Thu, 1 Oct 2009 08:46:21 +0000 (08:46 +0000)]
fixed off-by-one
Claudio Sacerdoti Coen [Wed, 30 Sep 2009 20:28:17 +0000 (20:28 +0000)]
With this hint, it diverges.
Enrico Tassi [Wed, 30 Sep 2009 20:19:38 +0000 (20:19 +0000)]
rewritten instantiate code
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.
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.
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.
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.
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.
Enrico Tassi [Tue, 29 Sep 2009 17:20:47 +0000 (17:20 +0000)]
...
Claudio Sacerdoti Coen [Tue, 29 Sep 2009 17:01:28 +0000 (17:01 +0000)]
Re-indentiation
Enrico Tassi [Tue, 29 Sep 2009 16:53:28 +0000 (16:53 +0000)]
ugly coerc db print
Claudio Sacerdoti Coen [Tue, 29 Sep 2009 14:48:11 +0000 (14:48 +0000)]
The unification does not longer use the refiner (urrah!)
Claudio Sacerdoti Coen [Tue, 29 Sep 2009 14:06:40 +0000 (14:06 +0000)]
...
Enrico Tassi [Tue, 29 Sep 2009 14:03:50 +0000 (14:03 +0000)]
...
Enrico Tassi [Tue, 29 Sep 2009 12:58:16 +0000 (12:58 +0000)]
more virtuals
Enrico Tassi [Tue, 29 Sep 2009 12:28:08 +0000 (12:28 +0000)]
...
Claudio Sacerdoti Coen [Tue, 29 Sep 2009 08:22:56 +0000 (08:22 +0000)]
It does not work recursively...
Claudio Sacerdoti Coen [Tue, 29 Sep 2009 08:18:25 +0000 (08:18 +0000)]
...
Enrico Tassi [Mon, 28 Sep 2009 19:27:14 +0000 (19:27 +0000)]
non ho resistito!
Enrico Tassi [Mon, 28 Sep 2009 16:14:46 +0000 (16:14 +0000)]
- fixed bug in coercion application, input/output swapped in unification
- experimental automatic reduction of projections in apply-subst-metasenv
Enrico Tassi [Mon, 28 Sep 2009 14:38:54 +0000 (14:38 +0000)]
2 lift related bugs fixed!
Enrico Tassi [Mon, 28 Sep 2009 14:38:13 +0000 (14:38 +0000)]
better debug pp
Claudio Sacerdoti Coen [Mon, 28 Sep 2009 11:12:13 +0000 (11:12 +0000)]
Experiment...
Claudio Sacerdoti Coen [Mon, 28 Sep 2009 09:59:15 +0000 (09:59 +0000)]
Experiment...
Enrico Tassi [Sun, 27 Sep 2009 21:22:09 +0000 (21:22 +0000)]
Type printed as such, CProp printed as such
Enrico Tassi [Sun, 27 Sep 2009 20:33:46 +0000 (20:33 +0000)]
fixpoint have attributes for pragma (i.e. they can be marked as projections)
Enrico Tassi [Fri, 25 Sep 2009 18:01:44 +0000 (18:01 +0000)]
...
Enrico Tassi [Fri, 25 Sep 2009 15:39:03 +0000 (15:39 +0000)]
...
Enrico Tassi [Fri, 25 Sep 2009 15:28:24 +0000 (15:28 +0000)]
...
Enrico Tassi [Thu, 24 Sep 2009 16:00:37 +0000 (16:00 +0000)]
...