| Age | Commit message (Collapse) | Author |
|---|
|
introducing constants (e.g. Top.1 is always before Top.2), compatible with the one
used before introduction of hMaps in LMap/LSet.
|
|
Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced.
|
|
This revert somehow f5d7b2b1eda550f5bf0965286d449112acbbadde about "Hypotheses
don't respect Barendregt convention".
|
|
now done entirely using declare_mind, which declares the associated
constants for primitive records. This avoids a hack related to
elimination schemes and ensures that the forward references to constants
in the mutual inductive entry are properly declared just after the
inductive. This also clarifies (and simplifies) the code of term_typing
for constants which does not have to deal with building
or checking projections anymore.
Also fix printing of universes showing the de Bruijn encoding in a few places.
|
|
eta-expanded version of a projection as before.
|
|
Now kernel/indtypes builds the corresponding terms (has to be trusted)
while translate_constant just binds a constant name to the
already entered projection body, avoiding the dubious "check"
of user given terms. "case" Pattern-matching on primitive records is
now disallowed, and the default scheme is implemented using
projections and eta (all elimination tactics now use projections
as well). Elaborate "let (x, y) := p in t" using let bindings
for the projections of p too.
|
|
It's possible that I should have removed more "allows", as many
instances of "foo allows to bar" could have been replaced by "foo bars"
(e.g., "[Qed] allows to check and save a complete proof term" could be
"[Qed] checks and saves a complete proof term"), but not always (e.g.,
"the optional argument allows to ignore universe polymorphism" should
not be "the optional argument ignores universe polymorphism" but "the
optional argument allows the caller to instruct Coq to ignore universe
polymorphism" or something similar).
|
|
larger than Type.1 etc...
|
|
|
|
|
|
of the argument is smaller than the other one.
|
|
Names and arguments were uniformized, and some functions were redesigned to
take their typical use-case into account.
|
|
My previous optimization of guard checking (f1280889) made it slightly stricter,
in the presence of dependent pattern matching and nested inductive types whose
toplevel types are mutually recursive.
The following (cooked-up) example illustrates this:
Inductive list (A B : Type) := nil : list A B | cons : A -> list A B -> list
A B.
Inductive tree := Node : list tree tree -> tree.
Lemma foo : tree = tree. exact eq_refl. Qed.
Fixpoint id (t : tree) :=
match t with
| Node l =>
let l := match foo in (_ = T) return list tree T with eq_refl => l end
in
match l with
| nil => Node (nil _ _)
| cons x tl => Node (cons _ _ (id x) tl)
end
end.
is accepted, but changing tree to:
Inductive tree := Node : list tree tree -> tree.
with tree2 := .
made id be rejected after the optimization.
The same problem occurred in Paco, and is now fixed.
Note that in the example above, list cannot be mutually recursive because of the
current strict positivity condition for tree.
|
|
|
|
In check_one_cofix, we now avoid calling dest_subterms each time we meet a
constructor by storing both the current tree (needed for the new criterion)
and a precomputed array of trees for subterms.
|
|
When dynamically computing the recarg tree, we now prune it according to the
inferred tree. Compilation of CompCert is now ok.
|
|
I had introduced it by mistake due to my OCaml dyslexia :)
Thanks to Enrico and Arnaud for saving my day!
|
|
|
|
for constants that are not unfolded during conversion.
Fix discharge of polymorphic section variables over inductive types.
|
|
- Decomment code in reductionops forgotten after debugging.
|
|
variables.
Simplifies instantiation of constants/inductives, requiring less allocation and Map.find's.
Abstraction by variables is handled mostly inside the kernel but could be moved outside.
|
|
- realargs: refers either to the indices of an inductive, or to the proper args
of a constructor
- params: refers to parameters (which are common to inductive and constructors)
- allargs = params + realargs
- realdecls: refers to the defining context of indices or proper args
of a constructor (it includes letins)
- paramdecls: refers to the defining context of params (it includes letins)
- alldecls = paramdecls + realdecls
|
|
function, so plain pointer equality is sufficient.
|
|
If the return predicate is not dependent, we avoid dynamically regenerating the
regular tree of the corresponding inductive type. This includes the commutative
cut rule. Should solve some performance issues observed in Compcert and Paco at
Qed time.
|
|
Used by the new guard criterion compatible with type isomorphisms.
|
|
|
|
|
|
- Distinguish between primitive and non-primitive records in the kernel
declaration, so as to try eta-conversion on primitive records only.
|
|
|
|
This reverts commit ec1bb8a981fef14b58ab65483244fc42b05aef13.
|
|
This reverts commit 6a3bcd3ae320e65347cbd6ef4bac458f073d02ea.
Apply again if this kind of dependently typed programming idioms are needed.
|
|
commutative cut rule.
The error messages of the guard checker are now sometimes not
informative enough.
|
|
A pattern matching is can now be a subterm if:
- Every branch is a subterm
- The return predicate is a pattern matching whose return predicate is an arity.
- That pattern matching (in the return predicate) returns the same inductive
family in the conclusion of each branch.
The commutative cut rule hasn't been updated accordingly yet.
|
|
|
|
Following Bruno's suggestion, we check if the tree expected for the recursive
argument is included in the one which is inferred. This check is probably
not necessary in the current state of affairs, but might become so after
further extensions of the guard condition.
|
|
extensions.
|
|
|
|
|
|
|
|
instantiated in the return predicate are now taken into account. The resulting
recargs tree is the intersection between the one of the branches and the
appearing in the return predicate. Both the domain and co-domain are filtered.
|
|
Some fixpoints are now rejected in the standard library, but that's probably
because we compare trees for equality instead of intersecting them.
|
|
pattern matching.
This patch should be improved in two ways:
(1) Implement the same checks for the commutative cut subterm rule.
(2) When checking safe recursive subterms for each of the branches in a match,
instanciated parameters in the return predicate should be taken into account.
Step (1) should be enough to restore a correct guard condition, but (2) will
be required if we don't want to rule out some legitimate and practical examples.
|
|
|
|
and disable hashconsing of substituted instances which had a huge performance
penalty in general. They are hashconsed when put in the environment only now.
|
|
|
|
unification, speeding it up considerably
Revert backwards-incompatible commit 77df7b1283940d979d3e14893d151bc544f41410
|
|
more than one constructor.
|
|
a primitive projection impossible.
|
|
|
|
|
