| Commit message (Collapse) | Author | Age |
|
|
|
|
| |
This completes the port of the native compiler to retroknowledge.
However, some testing and optimizations are still to be done.
|
|
|
|
| |
dependencies.
|
| |
|
|
|
|
| |
(hopefully), and forbids generic equality. Still, it allows generic hash.
|
|
|
|
|
|
|
|
|
|
|
| |
the provided type to come with a hashing function. The internal representation
is changed, such that values are first compared w.r.t. to their hash.
This effectively saves a lot of comparisons which may be far more expensive
than O(1), as in the string case, hence resulting in an overall speedup.
CAVEAT: everything is not implemented yet, and order-sensitive functions
now do not respect the provided order anymore.
|
| |
|
|
|
|
|
|
|
| |
There are currently two other clashs : Lexer and Errors, but for
the moment these ones haven't impacted my experiments with extraction
and compiler-libs, while this Matching issue had. And anyway the new
name is more descriptive, in the spirit of the recent TacticMatching.
|
|
|
|
|
| |
NB: new file miscprint.ml deserves to be part of printing.cma,
but should be part of proofs.cma for the moment, due to use in logic.ml
|
| |
|
|
|
| |
This commit also introduces a module Monad to generate monadic combinators (currently, only List.map).
|
|
|
|
|
| |
Make this module deal only with opaque proofs.
Make discharging/substitution invariant more explicit via a third constructor.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
For a file dir/a.v the corresponding aux file dir/.a.aux can store
arbitrary data. It maps a "Loc.t * string" (key) to a "string" (value).
Pretty much anything can fit in this schema, but ATM I see only the
following possible uses:
1) record inferred data, like the set of section variable used, so that
one can later use this info to process proofs asynchronously (i.e.
compute their discharged type without knowing the proof term).
2) record timings (how long it takes to build a proof term or check it),
so that one can take smarter scheduling decisions
3) record a bloated proof trace for automatic tactics, so that one can
replay it faster (a sort of cache). For that to be useful an Ltac
API is required.
The .aux file contains the path of the .v and its md5 hash. When loaded
it defaults to the empty map is the file is not there or if the .v file
changed.
Not finding some data in the .aux file cannot be a failure, but finding
it may help in many ways.
The current file format is very simple but human readable. It is
generated/parsed using printf/scanf and in particular the %S formatter
for the value string. The file format is private to the Aux_file
module: only an abstract interface is provided.
The current file format is not robust in face of local changes.
Any change invalidates the md5 hash (and the Loc.t is very likely to
change too).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Experimental. Turned out to be much harder to implement than I thought. The main
issue is that the reification in the native compiler and the VM is not quite
untyped. Indeed, type annotations for lambdas have to be reconstructed. Hence,
when reifying an application u = t a1 ... an, the type of t has to be known or
reconstructed. It is always possible to do so in plain CIC, when u is in normal
form and its type is known. However, with partial terms this may no longer be
the case, as in: ?1 a1 ... an. So we also compile and evaluate the type of
evars and metas.
This still has to be tested more extensively, but the correction of the kernel
native conversion (on terms without evars or metas) should not be impacted.
Much of this could be reused for the VM.
|
|
|
|
| |
internalization time.
|
|
|
|
| |
parsing is plugged.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
by extraction.
The goal was to use Coq's partial evaluation capabilities to do manually some
inlining that Ocaml couldn't do. It may be critical as we are defining higher
order combinators in term of others and no inlining means a lot of
unnecessary, short-lived closures built.
With this modification we get back some (but not all) of the loss of performance introduced by threading the monadic type all over the place.
I still have an estimated 15% longer compilation time for Coq.
Makes use of Set Extraction Conservative Types and Set Extraction File Comment
to maintain the relationship between the functions and their types.
Uses an intermediate layer Proofview_monad between Proofview_gen and
Proofview in order to use a hand-written mli to catch potential errors in the
generated file (it uses Extract Constant a lot).
A bug in the extraction of signatures forces to remove the generated
proofview_gen.mli which does not have the correct types.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16981 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
But for vm, the kernel should be functional now
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16961 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
Ideally all unmarshallable content in the state should be
stocked using Ephemeron keys. In this way the state becomes
always marshallable (because the unmarshallable content is magically
dropped). The mli contains more detailed doc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16891 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
casts of ints to evars.
- 2 in Evarutil and Goal which are really needed, even though the Goal
one could (and should) be removed;
- 2 in G_xml and Detyping that are there for completeness sake, but
that might be made anomalies altogether;
- 1 in Newring which is quite dubious at best, and should be fixed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16786 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16765 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
The extended signature is defined in CMap, and should be compatible
with the old one, except that module arguments have to be explicitely
named. The implementation itself is quite unsafe, as it relies on the
current implementation of OCaml maps, even though that should not be
a problem (it has not changed in ages).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16735 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16717 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The process_transaction function adds a new edge to the Dag without
executing the transaction (when possible).
The observe id function runs the transactions necessary to reach to the
state id. Transaction being on a merged branch are not executed but
stored into a future.
The finish function calls observe on the tip of the current branch.
Imperative modifications to the environment made by some tactics are
now explicitly declared by the tactic and modeled as let-in/beta-redexes
at the root of the proof term. An example is the abstract tactic.
This is the work described in the Coq Workshop 2012 paper.
Coq is compile with thread support from now on.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16674 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Since the whole system is imperative, futures are run protecting
the global state, and the final state is also saved to let the user
freely chain futures.
Futures can represent local (lazy) computations or remote ones
(delegated). Delegating a future lets a third party assign its
value at some poit in the future; in the meanwhile accessing the
future value raises an exception.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16669 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
through a unique generic argument, and the level is only considered
at parsing time.
This may introduce unnecessary parentheses in Ltac printing though,
as every tactic argument is collapsed at the lowest level. I assume
this does not matter that much, and anyway Ltac printing is quite
bugged as of today.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16616 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
1. Genarg itself which only defines the abstract datatypes needed.
2. Genintern, first file of interp/, defining the intern and subst
functions.
3. Geninterp, first file of tactics/, defining the interp function.
4. Genprint, first file of printing/, dealing with the printers.
The Genarg file has no dependency and is in lib/, so that we can put
generic arguments everywhere, and in particular in ASTs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16601 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
related types. This will ultimately allow putting genargs into
these ASTs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16600 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
their own file, Stdarg.
This required a little trick to correctly handle wit_* naming. We
use a dynamic table to remember exactly where those arguments come
from.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16587 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16532 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16523 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16519 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16515 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
exactly once at runtime, often to reduce the mutual dependency of
modules. This module permits to track them more easily.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16509 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16500 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16492 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16463 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
1. sorts.ml: A small file utility for sorts;
2. constr.ml: Really low-level terms, essentially kind_of_constr, smart
constructor and basic operators;
3. vars.ml: Everything related to term variables, that is, occurences
and substitution;
4. context.ml: Rel/Named context and all that;
5. term.ml: derived utility operations on terms; also includes constr.ml
up to some renaming, and acts as a compatibility layer, to be deprecated.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16462 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16268 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
- constr_substituted and lazy_constr are now in a dedicated kernel/lazyconstr.ml
- the functions that were in declarations.ml (mostly substitution utilities
and hashcons) are now in kernel/declareops.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16250 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
information worn by exceptions. The implementation is quite hackish
but it should work nonetheless.
Basically, it adds an additional cell to exceptions arguments, in
which you can put whatever you want. By typing invariants, you may
not reach this cell by normal means, so it should be safe.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16212 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16195 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Using OCaml 3.11+ builtin facilities to record stack frames during
exception raising, we can now recover at runtime the backtrace of
an uncaught toplevel exception and display it to the user, without
the infamous OCaml debugger. The backtrace is displayed when using
the [-debug] flag.
This requires a bit of discipline, as each time we reraise an
exception we need to keep track of those frames we discarded
between the previous raise and the current [try-with] branch.
Currently, only [Anomaly] is handled, but this can be ported to any
exception as long as we add the backtrace info into the exception,
and we provide the corresponding handler to
[Backtracke.register_backtrace_handler].
Hopefully this should not be to costly, as we only do little work
when reraising, and only with the [-debug] flag set.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16166 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
native OCaml code.
Warning: the "retroknowledge" mechanism has not been ported to the native
compiler, because integers and persistent arrays will ultimately be defined as
primitive constructions. Until then, computation on numbers may be faster using
the VM, since it takes advantage of machine integers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16069 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15968 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15956 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15928 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Btw, remove unused code in the xml plugin and in Tactic_printer
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15863 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
kernel on CAMLP4/5 structures, and consequently should also erase
such structures from vo files.
This modification requires some code duplication, mainly while
reimplementing our own location data type. This is chiefly visible
in the ml4 files, where CAMLP4/5 locations must be manually converted
to our locations with an explicit (!@) cast operator.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15847 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15834 85f007b7-540e-0410-9357-904b9bb8a0f7
|