diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:35:34 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:35:34 +0000 |
| commit | e6404437c1f6ae451f4253cd3450f75513b395c3 (patch) | |
| tree | b8fae579662002cd7a921aa6baa5af6d920204a4 /proofs/proofs.mllib | |
| parent | 15effb7dedbaa407bbe25055da6efded366dd3b1 (diff) | |
Replaced monads.ml by an essentially equivalent proofview_gen.ml generated 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
Diffstat (limited to 'proofs/proofs.mllib')
| -rw-r--r-- | proofs/proofs.mllib | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 19f289316..4a7efb029 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -1,7 +1,9 @@ Goal Evar_refiner -Monads Proof_type +Proof_errors +Proofview_gen +Proofview_monad Proofview Proof Proof_global |