| Age | Commit message (Collapse) | Author |
|---|
|
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
|
|
|
|
In #6092, `global_reference` was moved to `kernel`. It makes sense to
go further and use the current kernel style for names.
This has a good effect on the dependency graph, as some core modules
don't depend on library anymore.
A question about providing equality for the GloRef module remains, as
there are two different notions of equality for constants. In that
sense, `KerPair` seems suspicious and at some point it should be
looked at.
|
|
|
|
Compute plugin
|
|
BZ#4852)
This code simplification isn't that important, but it can trigger further
simplifications elsewhere, see for instance BZ#4852.
NB: normally, the extraction favors eta-expanded forms, since that's the usual
way to avoid issues about '_a type variables that cannot be generalized. But
the atomic eta-reductions done here shouldn't be problematic (no applications
put outside of functions).
|
|
See https://github.com/letouzey/extraction-compute for more details
|
|
4844 and 4824)
The commit 8e257d4 (which consider the dummy type Tdummy to be polymorphic and hence
immune of the need for unsafeCoerce) is quite wrong, even if in pratice it worked ok
most of the time. The confusion comes from the fact that the dummy value (__ aka MLdummy
internally) is implemented in Haskell as Prelude.error, hence it has indeed a polymorphic
unrestricted type. But the dummy type Tdummy used when extracting types must be monomorphic
(otherwise type parameters would have to be propagated out of any type definition involving
Tdummy). We implement Tdummy by Haskell's (), which for instance isn't convertible to Any,
as shown by the examples in bug reports 4844 and 4824.
This fix will bring back some more unsafeCoerce in Haskell extraction, including possibly
a few spurious ones. And these extra unsafeCoerce might also hinder further code optimisations.
We tried to mitigate that by directly removing [MLmagic] constructors in front of [MLdummy _].
NB: even if the original bug report mentions universe polymorphism, this issue is
almost unrelated to it. It just happens that when universe polymorphism is off,
an inductive instance is fully placed in Prop (cf. template polymorphism) in the example,
avoiding triggering the issue.
Warning: the test-suite file is there for archiving the repro case, but currently it doesn't
test much (we should run ghc on the extracted code).
|
|
|
|
|
|
|
|
|
|
|
|
On an application (f args) where the head is magic, we first remove Obj.magic
on arguments before continuing with simplifications (that may push magic down
inside the arguments).
For instance, starting with ((Obj.magic f) (Obj.magic (g h))), we now end
with ((Obj.magic f) (g h)) instead of ((Obj.magic f) ((Obj.magic g) h))) as
before.
|
|
Unfortunately, my first attempt at replacing (Obj.magic (fun x -> u) v)
by ((fun x -> Obj.magic u) v) was badly typed, as seen in FingerTree:
the argument v should also be magic now, otherwise it might not have
the same type as x.
This optimization is now correctly done, and to mitigate the potential inflation
of Obj.magic, I've added a few simplification rules to avoid redundant magics,
push them down inside terms, favor the form (Obj.magic f x y z), etc.
|
|
vars by _)
|
|
This is done via a unique pass which seems roughly linear in practice,
even on big developments like CompCert. There's a List.nth in an env at
each MLrel, that could be made logarithmic if necessary via Okasaki's
skew list for instance.
Another approach would be to keep names (as a form of documentation), but
prefix them by _ to please OCaml's warnings. For now, let's be radical and
use the _ pattern.
|
|
This fix only handles MLapp(MLmagic(MLlam...),...). Someday, we'll have
to properly investigate the interaction between all the other optimizations
and MLmagic. But well, at least this precise bug is fixed now.
|
|
In front of "let rec f x y = ... in f n m", if n is now an implicit argument,
then the argument x of the inner fixpoint f is also considered as implicit.
This optimization is rather ad-hoc, since we only handle MLapp(MLfix()) for
now, and the implicit argument should be reused verbatim as argument.
Note that it might happen that x cannot be implicit in f. But in this
case we would have add an error message about n still occurring somewhere...
At least this small heuristic was easy to add, and was sufficient to solve
the part 2 of bug #4243.
|
|
Instead of the original hacks (embedding implicits in string msg in MLexn !)
we now use a proper construction MLdummy (Kimplicit (r,i)) to replace the use
of the i-th argument of constant or constructor r when this argument has been
declared as implicit.
A new option Set/Unset Extraction SafeImplicits controls what happens
when some implicits still occur after an extraction : fail in safe mode,
or otherwise produce some code nonetheless. This code is probably buggish
if the implicits are actually used to do anything relevant (match, function
call, etc), but it might also be fine if the implicits are just passed along.
And anyway, this unsafe mode could help figure what's going on.
Note: the MLdummy now expected a kill_reason, just as Tdummy.
These kill_reason are now Ktype, Kprop (formerly Kother) and Kimplicit.
Some minor refactoring on the fly.
|
|
|
|
|
|
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).
|
|
With ocaml 4.01, the 'unused open' warning also checks the mli :-)
Beware: some open are reported as useless when compiling with camlp5,
but are necessary for compatibility with camlp4. These open are now
marked with a comment.
|
|
|
|
To reduce the amount of syntactic noise, we now provide
a few inner modules Int.List, Id.List, String.List, Sorts.List
which contain some monomorphic (or semi-monomorphic) functions
such as mem, assoc, ...
NB: for Int.List.mem and co we reuse List.memq and so on.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16936 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
with OCaml 3.12.1).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16727 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16282 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16249 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Ok, this is merely a matter of taste, but up to now the usage
in Coq is rather to use capital letters instead of _ in the
names of inner modules.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16097 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16067 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15805 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
List module. That way, an "open Util" in the header permits using
any function of CList in the List namespace (and in particular, this
permits optimized reimplementations of the List functions, as, for
example, tail-rec implementations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
compiler warnings).
I was afraid that such a brutal refactoring breaks some obscure
invariant about linking order and side-effects but the standard
library still compiles.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
especially about unused definitions, unused opens and unused rec
flags.
The following patch uses information gathered using these warnings to
clean Coq source tree. In this patch, I focused on warnings whose fix
are very unlikely to introduce bugs.
(a) "unused rec flags". They cannot change the semantics of the program
but only allow the inliner to do a better job.
(b) "unused type definitions". I only removed type definitions that were
given to functors that do not require them. Some type definitions were
used as documentation to obtain better error messages, but were not
ascribed to any definition. I superficially mentioned them in one
arbitrary chosen definition to remove the warning. This is unaesthetic
but I did not find a better way.
(c) "unused for loop index". The following idiom of imperative
programming is used at several places: "for i = 1 to n do
that_side_effect () done". I replaced "i" with "_i" to remove the
warning... but, there is a combinator named "Util.repeat" that
would only cost us a function call while improving readibility.
Should'nt we use it?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15797 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Extracted code need not preserve typing relations (e:t) from the source code.
This may be a problem as the extracted code may not implement the intented
interface. This option disables the optimisations which would prevent an
extracted term's type to be its extracted source term's type.
At this point the only such optimization is (I think) removing some dummy
λ-abstractions in constant definitions.
Extraction Implicit is still honored in this mode, and it's mostly necessary
to produce reasonable types. So in the conservative type mode, which
abstractions can be removed and which can'tt is entirely under the user's
control.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15762 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
grammar.cma
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Util only depends on Ocaml stdlib and Utf8 tables.
Generic pretty printing and loc functions are in Pp.
Generic errors are in Errors.
+ Training white-spaces, useless open, prlist copies random erasure.
Too many "open Errors" on the contrary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14785 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14782 85f007b7-540e-0410-9357-904b9bb8a0f7
|
