| Commit message (Collapse) | Author | Age |
... | |
|
|
|
|
|
|
|
|
|
| |
Most of the time, a constant name is built from:
- a kernel_name for its user part
- a delta_resolver applied to this kernel_name for its canonical part
With this patch we avoid building unnecessary constants for immediately
amending them (cf in particular the awkward code removed in safe_typing).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14545 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
Inductive definitions aren't that big, but they may contain some
constr (in types, rel_context, etc), hence if we hash-cons the
constr in Definition but not these ones, we may loose some sharing.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14544 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14543 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This is just a minor detail, but if we take care to use in mkRel
always the same physical Rels for n <= 16, then let's ensure that
these Rels are preserved by hash-consing. This way, we avoid
killing some sharing during hash-consing of most of constr but not
all (for instance those in mind).
In fact, this is probably superfluous since earlier commit
about "| Rel n as t -> t", but let's be sure.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14542 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Since we hash-cons arrays in place, no need to re-allocate
a few structures around them.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14540 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
Maybe could we keep only the kernel check, but message would
certainly need to be reformulated then.
For instance, the message was previously different for an attempt to
redefine a name whether this name was in the same section or not.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14528 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
If two distinct parameters of the inductive type contributes to
polymorphism, they must have distinct names, othewise an aliasing
problem of the form "fun x x => max(x,x)" happens.
Also insisted that a parameter contributes to universe polymorphism
only if the corresponding occurrence of Type is not hidden behind a
definition.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14511 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
that the return predicate of the match construction is at an allowed
sort, resulting in tactics possibly manipulating ill-typed terms. This
is now fixed,
Incidentally removed in pretyping an ill-placed coercion.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14508 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- An inductive is hidden inside case_info.
(btw, maybe we could get rid of this ci_ind altogether,
since the information is already in the predicate of the match)
- Typical situation where user kn and canonical kn are initially (==)
was not preserved by hconsing of constant / mutual_inductive
- inductive = (mutual_inductive * int) and
constructor = inductive * int were not properly shared
This should fix the strange situation of Udine/PiCalc taking *more*
vo space after the last round of hcons tweaks.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14507 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
conversion hints to kernel). Whether REVERTcast must be known from
coqchk is unclear. In the meantime, warn about the unstability of the
situation (see also bug #2599).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14495 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
information coming from tactics on how to solve cst/cst critical pairs
in the kernel conversion machine).
In r14448, extra Cast's were removed from kernel type-checker but
(erroneously) not from the terms actually registered in the
environment.
The current commit completes the work by registering the term output
by the type-checker and not the original term. Note that this needs to
move hconsing from before to after typing.
On the Coq library, propagating Cast (without keeping them on disk)
induces a stable 1% speedup (Xeon w3540). Having hcons before or after
type-checking makes no difference. It remains to test on user contribs
whether the current commit compensates the slow down and vo size
increasing coming with the improvement made to Qed in r14407.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14492 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14488 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
Now that Yann has provided a better hashing mechanism for constr,
it might be interesting to (re-?)activate a global hash-consing of
constr. Earlier, specific hash-cons tables were created at each call
to hcons_constant_declaration. According to Hugo, this was meant to
avoid blow-up in at least contrib Pocklington. This contrib seems
to behave nicely now with global hashconsing (thanks Yann ;-).
We'll see tomorrow what impact this has on other contribs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14487 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14468 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- When hash-consing, seeing ident as having string as sub-structure
induces a penalty: two searchs are done in two tables
(one for string, one for id).
We simply say now that the hcons function for ident is the one
for string
- use more == during hash-consing of Names.uniq_ident and
Names.module_path
- clarification concerning hash-cons of Names.constant and
Names.mutual_inductive: we only hash-cons the canonical part,
but == could be used nonetheless on the obtained pair. Simply
note that canonical_con of hash-consed constants will produce
kernel_names that may be (=) but not (==).
- Code cleanup : no direct use of string hash-consing apart in Names,
we hence simplify hcons_names
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14464 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Two issues were preventing the hcons1_univ function to properly work
- a launch of Names.hcons_names () at each hconsing of universe,
hence one separated hash-table for dir-path created at each time,
oups...
- Bad handling of the universe sub-structure universe_level
To check : is there an interest in making separate calls to
Names.hcons_names () in separate places (Univ, Term, Declare) ?
I think not. Btw the hconsing of Declare.hcons_constant_declaration
is also probably wrong. To be fixed in a forthcoming patch.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14463 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
tactic steps (r14407) increased the size of proof-terms, leading in
some cases (e.g. in Nijmegen/Algebra) to calls to simpl becoming
extremely costly on such terms built with tactics.
We try as a workaround to remove the newly introduced Cast after it
has been used by the type-checking algorithm.
We incidentally fixed eq_constr which was not fully transparent wrt
casts. We also removed useless code in judge_of_apply (has_revert).
Note: checker still to be updated to reflect a possible use of this
new kind of cast.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14448 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
that the kernel conversion solves the delta/delta critical pair the
same way the tactics did. This allows to improve Qed time when slow
down is due to conversion having (arbitrarily) made the wrong choice.
Propagation is done thanks to a new kind of cast called REVERTcast.
Notes:
- Vm conversion not modified
- size of vo generally grows because of additional casts
- this remains a heuristic... for the record, when a reduction tactic
is applied on the goal t leading to new goal t', this is translated
in the kernel in a conversion t' <= t where, hence, reducing in t'
must be preferred; what the propagation of reduction cast to the
kernel does not do is whether it is preferable to first unfold c or
to first compare u' and u in "c u' = c u"; in particular,
intermediate casts are sometimes useful to solve this kind of issues
(this is the case e.g. in Nijmegen/LinAlg/subspace_dim.v where the
combination "simpl;red" needs the intermediate cast to ensure Qed
answers quickly); henceforth the merge of nested casts in mkCast is
deactivated
- for tactic "change", REVERTcast should be used when conversion is in
the hypotheses, but convert_hyp does not (yet) support this (would
require e.g. that convert_hyp overwrite some given hyp id with a
body-cleared let-binding new_id := Cast(old_id,REVERTCast,t))
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14407 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14387 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Allows to be sure that we apply the smart constructors.
Propagate the change to Closure, Reduction, Term, Cbv and Newring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14386 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
I think the additional check was here for historical reasons (before the invariant on Apps was enforced)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14379 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14376 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Term: add function eq_rel_declaration
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14366 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14346 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
Constrhash and Termhash
We need a function hash_constr (added in Term)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14345 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
... and report changes on Term
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14344 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14330 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
We need to move eq_constr upwards
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14319 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14315 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
- removed duplicate constructors
- moved code around for more clarity
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14314 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14313 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
- moved the alterate Hashtable module to a separate file
- moved all hashconsing-related function to a separate section in Term
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14312 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14311 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
A particular case in sort-polymorphism of inductive types allows
an informative type (such as prod) to have instances in Prop:
(I,I) : True * True : Prop
This is due to the fact that prod is a singleton type: indeed (I,I)
has no informative content. But this invalidates an important invariant
for the correctness of the extraction: inductive constructors stop
having always the same sort as their inductive type. Consider for instance:
Definition f (X:Type)(x:X*X)(g:X->nat) := g (fst x).
Definition test := f _ (I,I) (fun _ => 0).
Then the inductive element (I,I) is extracted as a logical part __,
but during a strict evaluation (i.e. in Ocaml, not Haskell), this __
will be given to fst, and hence to a match, leading to a nasty result
(potentially segfault). Haskell is not affected, since fst is never
evaluated.
This patch adds a check for this situation during any Ocaml extraction,
leading for the moment to a fatal error. Some functions in inductive.ml
and retyping.ml now have an extra optional argument ?(polyprop=true)
that should stay untouched in regular Coq usage, while type-checking
done during extraction will disable this prop-polymorphism.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14256 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
The env was used for a particular case of Cbytegen.compile_constant_body,
but we can actually guess that it will answer a particular BCallias con.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14134 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
"Print Module M" prints now by default both a signature
(fields with their types) and a body (fields with their types
and transparent bodies).
"Print Module Type M" could be used both when M is a module
or a module Type, it will only display th signature of M.
The earlier minimalist behavior (printing only the field names)
could be reactivated by option "Set Short Module Printing".
For the moment, the content of internal sub-modules and sub-modtypes
are not displayed.
Note: this commit is an experiment, many sitations are still
unsupported. When such situations are encountered, Print Module
will fall back on the earlier minimalist behavior. This might
occur in particular in presence of "with" annotations, or in the
conjonction of a non-global module (i.e. functor or module type)
and internal sub-modules.
Side effects of this commit:
- a better compare function for global_reference, with no
allocations at each comparison
- Nametab.the_globrevtab is now searched according to user part only
of a kernel_name
- The printing of an inductive block is now in Printer, and rely less
on the Nametab. Instead, we use identifiers in mind_typename and
mind_consnames. Note that Print M.indu will not display anymore
the pseudo-code "Inductive M.indu ..." but rather "Inductive indu..."
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14117 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
Bug-Debian: http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=622882
Signed-off-by: Konstantinos Margaritis <markos@genesi-usa.com>
Signed-off-by: Stephane Glondu <steph@glondu.net>
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14027 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
This reverts commit 33434695615806a85cec88452c93ea69ffc0e719.
Conflicts:
kernel/term_typing.ml
test-suite/success/polymorphism.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13998 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
- Be careful with consider_remaining_unif_problems: it might instantiate an evar, including the current goal!
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13995 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13994 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
- Add Set Typeclasses Debug/Depth n options for typeclasses eauto.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13989 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13988 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
After discussion with Bruno and Hugo, coqtop now accepts that an opaque
constant in a module type could be implemented by anything of
the right type, even if bodies differ. Said otherwise, with respect
to subtyping, an opaque constant behaves just as a parameter.
This was already the case in coqchk, and a footnote in documentation
is advertising for quite some time that:
"Opaque definitions are processed as assumptions."
Truly, it might seem awkward that "Definition x:=3" can implement
"Lemma x:nat. Proof 2. Qed." but the opacity ensures that nothing
can go wrong afterwards, since Coq is forced to ignore that the x
in signature has body "2".
Similarly, "T with Definition x := c" is now legal when T contains
an opaque x, even when this x isn't convertible with c.
By avoiding accesses to opaque bodies, we also achieve some speedup
(less delayed load of .vo final sections containing opaque terms).
Nota: the extraction will have to be adapted, since for the moment it
might access the body of opaque constants: the warning emitted when
doing that should become an error.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13987 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
when a "match" is kernel-ill-typed (probably rarely visible from end
user anyway but useful for debugging) + dead code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13969 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13959 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The recent experiment with -dont-load-proofs in the stdlib showed that
this options isn't fully safe: some axioms were generated (Include ?
functor application ? This is still to be fully understood).
Instead, I've implemented an idea of Yann: only load opaque proofs when
we need them. This is almost as fast as -dont-load-proofs (on the stdlib,
we're now 15% faster than before instead of 20% faster with -dont-load-proofs),
but fully compatible with Coq standard behavior.
Technically, the const_body field of Declarations.constant_body now regroup
const_body + const_opaque + const_inline in a ternary type. It is now either:
- Undef : an axiom or parameter, with an inline info
- Def : a transparent definition, with a constr_substituted
- OpaqueDef : an opaque definition, with a lazy constr_substitued
Accessing the lazy constr of an OpaqueDef might trigger the read on disk of
the final section of a .vo, where opaque proofs are located.
Some functions (body_of_constant, is_opaque, constant_has_body) emulate
the behavior of the old fields. The rest of Coq (including the checker)
has been adapted accordingly, either via direct access to the new const_body
or via these new functions. Many places look nicer now (ok, subjective notion).
There are now three options: -lazy-load-proofs (default), -force-load-proofs
(earlier semantics), -dont-load-proofs. Note that -outputstate now implies
-force-load-proofs (otherwise the marshaling fails on some delayed lazy).
On the way, I fixed what looked like a bug : a module type
(T with Definition x := c) was accepted even when x in T was opaque.
I also tried to clarify Subtyping.check_constant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13952 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13948 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We simply reuse the ocaml flag caml_signals_are_pending and the function
caml_process_pending_signals, and place a test at some place of the interpreter
loop (at a similar location as in ocaml byterun/interp.c).
The symbols caml_* we use are not officially made public in *.h installed
alongside ocaml, but they seem pretty stable (there since at least
ocaml 3.10, independent of arch and of byte/asm), so we access them via
"extern". For once, thanks dirty C...
In addition to that, when catching a Ctrl-C, we reset the vm via
"coq_sp = coq_stack_high" as suggested by Benjamin G.
This patch should be quite portable, it might even work in win32.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13947 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
evar, and simultaneously make type inference with universes work better.
This only exports more functions from kernel/univ, to be able to work
with a set of universe variables during type inference. Universe
constraints are gradually added during type checking, adding information
necessary e.g. to lower the level of unknown Type variables to Prop or
Set. There does not seem to be a disastrous performance hit on the
stdlib, but might have one on some contribs (hence the "Tentative").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13905 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13896 85f007b7-540e-0410-9357-904b9bb8a0f7
|