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.
huge commit regarding universes:
- only Type[foo] can be declare with a strict (<) constraint among other
Type[bar]
- CProp[foo] is automatically available for Type[foo]
- The CProp hierarchy can be collapsed (hopefully in a consistent way)
to both Prop OR Type:
- You cannot eliminate CProp to build a Type like for Prop/Type
- You cannot eliminate Prop to build a CProp, like for Prop/Type
- Peculiarity: CProp[i] has type Type[i+1], since CProp[i+1] is only >=
of CProp[i] to allow collapsing them (while < whould be violated).
New function to delift a type w.r.t. a term list, to potentially build a
dependent type, used in lambda_intro and Letin expected type propagation.
The left parameters coming from the constructor types have been refined in a
longer context. Thus we need to unify them in the longer context (that does not
hurt those coming from the inductive types).
improved check in delift for flexible lc entries.
added a function to easily delift a term w.r.t.
other terms, thanks to delift, used to propagate the expected type
of a letin.
to me, the problem:
? t ==?== ?->?
where the first ? has an empty local context
is always Uncertain... to be fully understood
why unification gives Failure. It may be correct if
t has type (Rel k). I wrap it in the refiner.
the refiner was not checking that the resulting type
of an application was the expected one in case
the application is ((lambda...) ?...) when ?...
resolves to the empty ? vector.
the TypeError exception is back in place inside the Type modules
basic_rg: some typing-related code is back in place inside the Type module
log: some improvements in the interface
The ~delta argument was accidentally saved in the closure of aux that was
passed to all functions defined by the reduction strategy. So, most of the
terms where shared by the KAM environment in whd normal form with delta=max_int
(that means, not delta/iota-reduced at all, just beta-normal).
Thus many heavy computations where not shared, completely loosing the point
of having a KM.
The solution was to fix the API so that delta is not hidden anymore, then
really sharing computations with delta=0 (the most common case, I think).
The bad behaviour is still present for other values of delta, and an imperative
cache may be emplyed.
The ~delta argument was accidentally saved in the closure of aux that was
passed to all functions defined by the reduction strategy. So, most of the
terms where shared by the KAM environment in whd normal form with delta=max_int
(that means, not delta/iota-reduced at all, just beta-normal).
Thus many heavy computations where not shared, completely loosing the point
of having a KM.
The solution was to fix the API so that delta is not hidden anymore, then
really sharing computations with delta=0 (the most common case, I think).
The bad behaviour is still present for other values of delta, and an imperative cache may be emplyed.
projects / helm.git / log