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.
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.
projects / helm.git / log