| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
| |
The option is still there, but not documented since it is too
dangerous. Hints and type classes instances are not taking cleared
variables into account.
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
Change was introduced by cedcfc9bc386456f3fdd225f739706e4f7a2902c.
|
| |
|
|
| |
vars by _)
|
| | |
|
| |
|
|
|
|
| |
The unshelve tactical can be used to get the shelved holes. This changes the
proper ordering of holes though, so expect some broken scripts. Also, the
test-suite is not fixed yet.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
| |
Force failing when reaching end of file with unterminated comment when
parsing Make (project) file.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
2.14. Debian ships with lablgtk 2.16 only since a few months, so we apply the
fix to trunk instead.
This reverts commits:
490160d25d3caac1d2ea5beebbbebc959b1b3832.
ef8718a7fd3bcd960d954093d8c636525e6cc492.
6f9cc3aca5bb0e5684268a7283796a9272ed5f9d.
901a9b29adf507370732aeafbfea6718c1842f1b.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
| |
same evar.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Marking it as experimental.
|
| |
|
|
| |
"open Unix" from lib/system.ml.
|
| |
|
|
|
|
| |
be cleared.
This should fix the contrib failures on tactics like "destruct (0)".
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
Pierre Letouzey
Enrico Tassi
Maxime Dénès
Pierre-Marie Pédrot
Hugo Herbelin
Matthieu Sozeau
Guillaume Melquiond
Matej Kosik