The code for universes was not correct in many borderline cases.
The new code should be correct. For sure, it is much simpler, shorter,
characterized by better invariants and its interface has less functions.
Enrico Tassi [Thu, 15 May 2008 12:39:00 +0000 (12:39 +0000)]
Major code semplification and bugs removed (thanks to a better invariant):
small_delta_step always put the terms in WHNF, even if it can do that with delta > 0.
Terms in WHNF, delta=0 that are not head-alpha convertible and tail-machine convertible
are not convertible.
- is_closed removed from the kernel (it used to make a loose test, replaced
with a tighter one)
- does_not_occur no longer calls lift (performance improvement)
- does_not_occur: bug fixed in management of Metas
New implementation of CicEnvironment:
a) I have splitted out nCicLibrary from nCicEnvironment
b) Recursion changed: the nCicTypechecker now registers itself to the
nCicEnvironment. Then it is the nCicEnvironment.get_obj that retrieves
an object from the library before calling the registered typecheck_obj
c) The logger is now called every time NCicTypechecker.get_obj is invoked,
both by the nCicEnvironment and by another module
Enrico Tassi [Mon, 5 May 2008 17:02:26 +0000 (17:02 +0000)]
get_check_fix and cofix unified, bug regarding debruijnation of constructors types fixed everywhere.
the constructor typs are debruinated wrt some inductive type uri an not wrt
their own, thus a wrong context was created. guarded by constructors ported from the old kernel.
Enrico Tassi [Mon, 5 May 2008 13:34:10 +0000 (13:34 +0000)]
guarded_by_constructors implemented, some cleanup here and there.
fix_lefts_in_constr fixed: the inductive type list was returned with
constructors instantiated and debruijned, but with types whose arity was
instantiated with lefts too. This is wrong since we want to use these types to
build a context, that is closed, and will be put at the end of the actual
context since debruijn will make uris point to those terms
Bug fixed in handling of explicit named substitutions: it could happen that
explicit named substitution are merged not in the expected order. This happens
comparing the case of an instantiation inside and outside a (nested) section.
Thus I have added back the re-ordering of the explicit named substitution in
CicSubstitution.subst_vars and in CicReduction.unwind_aux. Moreover, I have
added to CicTypechecker.type_of_aux' the check that verifies if an explicit
named substitution is ordered.
Implementation of guarded_by_destructor is now complete w.r.t. the old kernel:
a) bug fixed in eat_lambdas_etc: we cannot apply the term to the residual
arguments since these are not left arguments
b) when the recursive argument of the nested "let rec" is safe, the formal
argument can also be considered safe.
TODO:
This implementation of condition b) could be improved by re-writing eat_lambdas
in such a way that it uses a shift_k function to add the context item to the
"context".
universes are written with the URI inside objects, this allows
universes to be actually shared between objects and no duplication is necessary.
in this way the typechecker is more strict and unification can be an ungly beast implicitly
adding an = constranint between two universes. speedup granted!
when Fix/i args and some args are not guarded
1) fixed params in interval 0..i are checked for bewing just passed around
2) the fix is unfolded, debruijned, fixed arguments substituted,
not fixed arguments pushed and checked for guardednes
3) a new function with relative fixed arguments (not to be checked again)
is added to k
4) the resulting term is applied to the remaining arguments
Avoid (whd ~delta:true) during guarded_by_destructors as much as possible.
Note: it is better to check again if this commit is fully correct (i.e.
w.r.t. the catch-all case in the main "match ... with" of the aux function).
In guarded by destructors, avoid computing the (whd ~delta:true) unless the
check fails. This is a major speed up, for instance for
cic:/Coq/ZArith/Zsqrt/sqrtrempos.con
projects / helm.git / log