During closure conversion, the right-hand side of a functional binding in a
recursive binding group is now always closed as a named expression rather than
an anonymous expression. As a result, direct recursive calls do not need to
retrieve their target from a closure environment. This does not only result in
more efficient code being generated, but also avoids a potential blocker for
successful tail-call detection during pseudo-instruction selection.
git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@14966 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
See the long comment in pervasives.ml for an explanation of the
change. The short summary is that we need to prove more elaborate
properties between the format types involved in the typing of %(...%),
and that proving things by writing GADT functions in OCaml reveals
that Coq's Ltac is a miracle of usability.
Proofs on OCaml GADTs are runtime functions that do have a runtime
semantics: it is legitimate to hope that those proof computations are
as simple as possible, but the current implementation was optimized
for feasability, not simplicity. François Bobot has some interesting
suggestions to simplify the reasoning part (with more equality
reasoning where I used transitivity and symmetry of the
relation profusely), which may make the code simpler in the future
(and possibly more efficient: the hope is that only %(...%) users will
pay a proof-related cost).
git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@14897 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
the x87 FP stack, which must not be eliminated.
CSEgen: harden against the same x87-specific issue + against reuse of
values in fixed hardware registers that were destroyed by a prior
operation.
git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@14877 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
This should make the type-checking of formats simpler and more robust:
instead of trying to find a pair as previously, we can now use the
path of the format6 type directly.
A nice side-effect of the change is that the internal definition of
formats (as a pair) is not printed in error messages anymore.
Because format6 is in fact defined in the CamlinternalFormatBasics
submodule of Pervasives, and has an alias at the toplevel of
Pervasives, error messages still expand the definition:
> Error: This expression has type
> ('a, 'b, 'c, 'd, 'd, 'a) format6 =
> ('a, 'b, 'c, 'd, 'd, 'a) CamlinternalFormatBasics.format6
> but an expression was expected of type ...
Passing the option `-short-paths` does avoid this expansion and
returns exactly the same error message as 4.01:
> Error: This expression has type ('a, 'b, 'c, 'd, 'd, 'a) format6
> but an expression was expected of type ...
(To get this error message without -short-paths, one would need to
define format6 directly in Pervasives; but this type is mutually
recursive with several GADT types that we don't want to add in the
Pervasives namespace unqualified. This is why I'll keep the alias
for now.)
git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@14868 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
Contrarily to the previous commit, this change is *not* completely
benine: it corresponds to the fact that Jacques' trunk@14523 (a
principality warning on formats in some situation) has not yet been
replayed on the format-gadts branch -- I mainly focused on backward
compatiblity.
The plan is to replay this change really soon, *after* converting
format6 to a nominal datatype -- this will much simplify the
re-implementation of the warning in the type-checker.
git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@14847 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
The change is benine: currently, error messages about format6 also
give its definition as a product of an inner format and a string: the
message changes, but the semantics is the same.
Ultimately, we want the error message *not* to change (we don't want
the internal implementation of formats to be exposed to the innocent
user), and that will be achieved by converting format6 to a nominal
type instead of a structural pair.
git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@14846 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
Gabriel Scherer
Mark Shinwell
Xavier Leroy
Damien Doligez
Alain Frisch
Maxence Guesdon
Jérémie Dimino
Jacques Garrigue