| Age | Commit message (Collapse) | Author |
|---|
|
This generalizes the BuildVi flag and lets one choose which
opaque proofs are done and which not.
|
|
Now the seff contains it directly, no need to force the future
or to hope that it is a Direct opaque proof.
|
|
Before this patch opaque tables were only growing, making them unusable
in interactive mode (leak on Undo).
With this patch the opaque tables are functional and part of the env.
I.e. a constant_body can point to the proof term in 2 ways:
1) directly (before the constant is discharged)
2) indirectly, via an int, that is mapped by the opaque table to
the proof term.
This is now consistent in batch/interactive mode
This is step 0 to make an interactive coqtop able to dump a .vo/.vi
|
|
for the record binder of classes. This name is no longer generated
in the kernel but part of the declaration. Also cleanup the interface
to recognize primitive records based on an option type instead of a
dynamic check of the length of an array.
|
|
Thanks to Yves for reporting it!
|
|
inductives).
The implementation constant should have the a universe instance
of the same length, we assume the universes are in the same order
and we check that the definition does not add any constraints
to the expected ones. This fixes bug #3670.
|
|
it closer to evarconv/unification's behavior and it is less prone
to weird failures and successes in case of first-order unification
sending problems where the two terms have different types.
|
|
using whd_state_gen to handle unfolding. Add an isProj/destProj
in term. Use the proper environment everywhere in unification.ml.
|
|
so as to reproduce correctly the reduction behavior of existing
projections, i.e. delta + iota. Make [projection] an abstract datatype
in Names.ml, most of the patch is about using that abstraction.
Fix unification.ml which tried canonical projections too early in
presence of primitive projections.
|
|
Essential for parallel processing of Coq documents.
It is a fairly straightforward change but a tad tedious, I may have introduced some bugs in the process.
|
|
|
|
|
|
Let r.(p) be a strict subterm of r during the guardness check.
|
|
|
|
subst_univs_levels.
|
|
it to the new representation of projections and the new mind_finite
type.
|
|
|
|
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.
|
