| Age | Commit message (Collapse) | Author |
|---|
|
Conflicts:
lib/cSig.mli
|
|
The Map interface of upcoming OCaml 4.03 includes a new union operator. In
order to make our homemade implementation of Maps compatible with OCaml
versions from 3.12 to 4.03, we define our own signatures for Maps.
|
|
|
|
|
|
|
|
|
|
|
|
This commit has deep consequences in term of tactic evaluation,
as it allows to pass any tac_arg to ML and alias tactics rather than
mere generic arguments. This makes the evaluation much more uniform,
and in particular it removes the special evaluation function for notations.
This last point may break some notations out there unluckily.
I had to treat in an ad-hoc way the tactic(...) entry of tactic notations
because it is actually not interpreted as a generic argument but rather
as a proper tactic expression instead.
There is for now no syntax to pass any tactic argument to a given ML or
notation tactic, but this should come soon.
Also fixes bug #3849 en passant.
|
|
|
|
The previous implementation was a source of evar leaks if misused, as
it created values coming together with their current evar_map. This is
dead wrong if the value is not used on the spot. To fix this, we rather
return a ['a delayed_open] object.
Two argument types were modified: bindings and constr_bindings. The
open_constr argument should also be fixed, but it is more entangled and
thus I leave it for another commit.
|
|
|
|
For instance, calling only Id.print is faster than calling both str and
Id.to_string, since the latter performs a copy. It also makes the code a
bit simpler to read.
|
|
The previous behavior was to include the interface of such a functor,
possibly leading to the creation of unexpected axioms, see bug report #3746.
In the case of non-functor module with restricted signature, we could
simply refer to the original objects (strengthening), but for a functor,
the inner objects have no existence yet. As said in the new error message,
a simple workaround is hence to first instantiate the functor, then include
the local instance:
Module LocalInstance := Funct(Args).
Include LocalInstance.
By the way, the mod_type_alg field is now filled more systematically,
cf new comments in declarations.mli. This way, we could use it to know
whether a module had been given a restricted signature (via ":"). Earlier,
some mod_type_alg were None in situations not handled by the extraction
(MEapply of module type).
Some code refactoring on the fly.
|
|
|
|
|
|
|
|
|
|
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.
|
|
During an extraction, a few tables are maintained to cache
intermediate results. Due to modules, the kernel_name index
for these caching tables aren't enough. For instance, in
bug #3923, a constant is first transparent (from inside the
module) then opaque (when seen from the signature). The previous
protections were actually obsolete (tests via visible_con), we
now checks that the constant_body is still the same.
|
|
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.
|
|
|
|
|
|
Some explicit '\n' in Pp.str were interacting badly with Format boxes
in Compcert, leading to right-flushed "sig..end" blocks in some .mli
|
|
|
|
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.
|
|
|
|
The ind_equiv field wasn't correctly set, due to some kernel names
glitches (canonical vs. user). The fix is to take into account the
delta_resolver while traversing module structures.
|
|
|
|
|
|
|
|
|
|
next to each other, waiting for possible integration into a more
uniform API.
|
|
|
|
|
|
|
|
constr, and the associated signature, not needed anymore.
Update CHANGES, no evar_map is produced by pattern_of_constr anymore.
|
|
pattern-matching on function calls.
|
|
which e.g. OCaml 4.02.1 displays.
|
|
- Had to add a Sigma.to_evar_map
- Had to rework coqdep_common.ml{,i} and coqdep.ml
|
|
for reporting it.
A "cut" was not appropriately chained on the second goal but on both
goals, with the chaining on the first goal introducing noise.
|
|
|
|
|
|
|
|
Keep user-side information on the names used in instances of universe
polymorphic references and use them for printing.
|
|
Side effects are now an opaque data type, called private_constant, you can
only obtain from safe_typing. When add_constant is called on a
definition_entry that contains private constants, they are either
- inlined in the main proof term but not re-checked
- declared globally without re-checking them
As a safety measure, the opaque data type contains a pointer to the
revstruct (an internal field of safe_env that changes every time a new
constant is added), and such pointer is compared with the current value
store in safe_env when the private_constant is inlined. Only when the
comparison is successful the private_constant is not re-checked. Otherwise
else it is. In short, we accept into the kernel private constant only
when they arrive in the very same order and on top of the very same env
they arrived when we fist checked them.
Note: private_constants produced by workers never pass the safety
measure (the revstruct pointer is an Ephemeron). Sending back the
entire revstruct is possible but: 1. we lack a way to quickly compare
two revstructs, 2. it can be large.
|
