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.
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).
Performance improvement by preserving more sharing. Visible in Oliboni's
development. But still slower then old matita (but pheraps on different data...)
- 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
Inverters/Inversion:
- fixed a bug with left parameters and inversion principles
- hooked automatic definition of inversion principles to the declaration of
inductive types
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)
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
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 [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
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.
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.
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.
projects / helm.git / log