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
When going under a binder, a term must be converted twice, as explained in the
previous commit. The problem is that in this way the complexity of the
translation becomes O(2^n) when n is the maximum depth of binders. However,
this computation is completely unuseful if no (co)fix is found in the term.
This commits adds as much lazyness as possible to fix the issue.
ported the instantiate-left-params-to-calculate-rec-args patch from the old to the new kernel,
to test the patch properly some steps of substitution inside a possibly blocked fix are performed,
this should be in general avoided without good checks (still to understand)
defn2.ma is to be used with part1a_inversion3
the induction/inversion lemma in part1a_inversion3 is more regular w.r.t.
the meta-theory
automation pushed to its limits in part1a_inversion3.ma
fix universe handling, newly encountered objects are typed in an empty ugraph
that after the cleanup phase is committed into the cic_environement and merged
with the current one.
minor reformatting of sources and some more for_all
ancient graph regarding universes and trust=false, universes calculated for internal objects
were used for the toplevel object (that should be sound) but cleaned using the univ list of
the internal object
ranking function fixed: when graphs are collapsed one step links are not updated (nor serialized to disk)
thus you can not rely on them, just use the closures!
new calculation of recursive parameters in guarded by destructors:
inductive I : Type :=
| K : list (pair Type I) -> I
let rec f t on t : I -> bool :=
match t with
| k ((nat, x)::_) -> f x
| k _ -> true
is now accepted. the arg of k used to be recursive but not the head of the list
(only its tail) since constructors types were not specialized on actual left
arguments (and the information that the type of the head contains I was lost).
check_is_really_smaller simplified to consider that it is called only on terms
(immediately put in normal form) that inhabit an inductive type. Moreover,
some duplicated code has been removed.
1. bug fixed: the context must be type-checked before using it in type_of_aux'.
Otherwise get_cooked_obj raises Not_found in Deannotate
2. big improvement in guarded_by_destructors: when a fix applied to a safe
argument is found in the body of another fix, the body of the inner fix
is check adding the recusrive formal parameter as an additional safe
argument.
positivity condition was relying on the name declared in abstractions, and
was checking for a dependent product calling does not occurr with a wrong
index
load the graph of objects that depend on the ones requested,
rank universes and use them in the transformation to obtain terms
with TypeK and not always Type0
Extracted code. The main executable is medium_tests that runs the emulator on
a few assembly programs with inputs of different sizes:
* string reverse
* counting sort
* perfect numbers
Conversion of 2 lambdas was not requiring equality on universes of the source type, while the conversion of products was requiring so.
Moreover Coq seems to force that constraint too.
projects / helm.git / log