Optimisation of partial applications in the tactic monad.

Explanations here: https://ocaml.janestreet.com/?q=node/30

Patch by Pierre-Marie Pédrot, with modifications from Arnaud Spiwack.

Signed-off-by: Arnaud Spiwack <arnaud@spiwack.net>

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16989 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 110 insertions, 98 deletions

diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml
index 422095870..95609e12d 100644
--- a/proofs/proofview_gen.ml
+++ b/proofs/proofview_gen.ml
@@ -1,7 +1,7 @@
 (* This file has been generated by extraction
    of bootstrap/Monad.v. It shouldn't be
    modified directly. To regenerate it run
-   coqtop -batch -impredicative-set
+   coqtop -batch -impredicative-set -l
    bootstrap/Monad.v in Coq's source
    directory. *)
 
@@ -16,46 +16,46 @@ module IOBase =
   
   (** val ret : 'a1 -> 'a1 coq_T **)
   
-  let ret = fun a () -> a
+  let ret = fun a -> (); fun () -> a
   
   (** val bind :
       'a1 coq_T -> ('a1 -> 'a2 coq_T) -> 'a2
       coq_T **)
   
-  let bind = fun a k () -> k (a ()) ()
+  let bind = fun a k -> (); fun () -> k (a ()) ()
   
   (** val ignore :
       'a1 coq_T -> unit coq_T **)
   
-  let ignore = fun a () -> ignore (a ())
+  let ignore = fun a -> (); fun () -> ignore (a ())
   
   (** val seq :
       unit coq_T -> 'a1 coq_T -> 'a1 coq_T **)
   
-  let seq = fun a k () -> a (); k ()
+  let seq = fun a k -> (); fun () -> a (); k ()
   
   (** val ref : 'a1 -> 'a1 coq_Ref coq_T **)
   
-  let ref = fun a () -> Pervasives.ref a
+  let ref = fun a -> (); fun () -> Pervasives.ref a
   
   (** val set :
       'a1 coq_Ref -> 'a1 -> unit coq_T **)
   
-  let set = fun r a () -> Pervasives.(:=) r a
+  let set = fun r a -> (); fun () -> Pervasives.(:=) r a
   
   (** val get : 'a1 coq_Ref -> 'a1 coq_T **)
   
-  let get = fun r () -> Pervasives.(!) r
+  let get = fun r -> (); fun () -> Pervasives.(!) r
   
   (** val raise : exn -> 'a1 coq_T **)
   
-  let raise = fun e () -> raise (Proof_errors.Exception e)
+  let raise = fun e -> (); fun () -> raise (Proof_errors.Exception e)
   
   (** val catch :
       'a1 coq_T -> (exn -> 'a1 coq_T) -> 'a1
       coq_T **)
   
-  let catch = fun s h () -> try s () with Proof_errors.Exception e -> h e ()
+  let catch = fun s h -> (); fun () -> try s () with Proof_errors.Exception e -> h e ()
   
   (** val read_line : string coq_T **)
   
@@ -63,17 +63,17 @@ module IOBase =
   
   (** val print_char : char -> unit coq_T **)
   
-  let print_char = fun c () -> print_char c
+  let print_char = fun c -> (); fun () -> print_char c
   
   (** val print :
       Pp.std_ppcmds -> unit coq_T **)
   
-  let print = fun s () -> try Pp.pp s; Pp.pp_flush () with e -> raise e ()
+  let print = fun s -> (); fun () -> try Pp.pp s; Pp.pp_flush () with e -> raise e ()
   
   (** val timeout :
       int -> 'a1 coq_T -> 'a1 coq_T **)
   
-  let timeout = fun n t () ->
+  let timeout = fun n t -> (); fun () ->
     let timeout_handler _ = Pervasives.raise (Proof_errors.Exception Proof_errors.Timeout) in
     let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
     Pervasives.ignore (Unix.alarm n);
@@ -194,8 +194,9 @@ module Logical =
       -> (exn -> 'a2 IOBase.coq_T) -> 'a2
       IOBase.coq_T **)
   
-  let ret x s e r sk fk =
-    sk ((x,s),true) fk
+  let ret x =
+    (); (fun s e _ sk fk ->
+      sk ((x,s),true) fk)
   
   (** val bind :
       'a1 t -> ('a1 -> 'a2 t) -> proofview ->
@@ -205,14 +206,15 @@ module Logical =
       (exn -> 'a3 IOBase.coq_T) -> 'a3
       IOBase.coq_T **)
   
-  let bind x k s e r sk fk =
-    Obj.magic x s e __ (fun a fk0 ->
-      let x0,c = a in
-      let x1,s0 = x0 in
-      Obj.magic k x1 s0 e __ (fun a0 fk1 ->
-        let y,c' = a0 in
-        sk (y,(if c then c' else false)) fk1)
-        fk0) fk
+  let bind x k =
+    (); (fun s e _ sk fk ->
+      Obj.magic x s e __ (fun a fk0 ->
+        let x0,c = a in
+        let x1,s0 = x0 in
+        Obj.magic k x1 s0 e __ (fun a0 fk1 ->
+          let y,c' = a0 in
+          sk (y,(if c then c' else false))
+            fk1) fk0) fk)
   
   (** val ignore :
       'a1 t -> proofview -> Environ.env -> __
@@ -221,15 +223,17 @@ module Logical =
       -> (exn -> 'a2 IOBase.coq_T) -> 'a2
       IOBase.coq_T **)
   
-  let ignore x s e r sk fk =
-    Obj.magic x s e __ (fun a fk0 ->
-      let x0,c = a in
-      let sk0 = fun a0 fk1 ->
-        let y,c' = a0 in
-        sk (y,(if c then c' else false)) fk1
-      in
-      let a0,s0 = x0 in
-      sk0 (((),s0),true) fk0) fk
+  let ignore x =
+    (); (fun s e _ sk fk ->
+      Obj.magic x s e __ (fun a fk0 ->
+        let x0,c = a in
+        let sk0 = fun a0 fk1 ->
+          let y,c' = a0 in
+          sk (y,(if c then c' else false))
+            fk1
+        in
+        let a0,s0 = x0 in
+        sk0 (((),s0),true) fk0) fk)
   
   (** val seq :
       unit t -> 'a1 t -> proofview ->
@@ -239,14 +243,15 @@ module Logical =
       (exn -> 'a2 IOBase.coq_T) -> 'a2
       IOBase.coq_T **)
   
-  let seq x k s e r sk fk =
-    Obj.magic x s e __ (fun a fk0 ->
-      let x0,c = a in
-      let u,s0 = x0 in
-      Obj.magic k s0 e __ (fun a0 fk1 ->
-        let y,c' = a0 in
-        sk (y,(if c then c' else false)) fk1)
-        fk0) fk
+  let seq x k =
+    (); (fun s e _ sk fk ->
+      Obj.magic x s e __ (fun a fk0 ->
+        let x0,c = a in
+        let u,s0 = x0 in
+        Obj.magic k s0 e __ (fun a0 fk1 ->
+          let y,c' = a0 in
+          sk (y,(if c then c' else false))
+            fk1) fk0) fk)
   
   (** val set :
       logicalState -> proofview ->
@@ -256,8 +261,9 @@ module Logical =
       (exn -> 'a1 IOBase.coq_T) -> 'a1
       IOBase.coq_T **)
   
-  let set s s0 e r sk fk =
-    sk (((),s),true) fk
+  let set s =
+    (); (fun s0 e _ sk fk ->
+      sk (((),s),true) fk)
   
   (** val get :
       proofview -> Environ.env -> __ ->
@@ -277,8 +283,8 @@ module Logical =
       (exn -> 'a1 IOBase.coq_T) -> 'a1
       IOBase.coq_T **)
   
-  let put m s e r sk fk =
-    sk (((),s),m) fk
+  let put m =
+    (); (fun s e _ sk fk -> sk (((),s),m) fk)
   
   (** val current :
       proofview -> Environ.env -> __ ->
@@ -297,8 +303,8 @@ module Logical =
       -> (exn -> 'a2 IOBase.coq_T) -> 'a2
       IOBase.coq_T **)
   
-  let zero e s e0 r sk fk =
-    fk e
+  let zero e =
+    (); (fun s e0 _ sk fk -> fk e)
   
   (** val plus :
       'a1 t -> (exn -> 'a1 t) -> proofview ->
@@ -308,9 +314,10 @@ module Logical =
       (exn -> 'a2 IOBase.coq_T) -> 'a2
       IOBase.coq_T **)
   
-  let plus x y s env r sk fk =
-    Obj.magic x s env __ sk (fun e ->
-      Obj.magic y e s env __ sk fk)
+  let plus x y =
+    (); (fun s env _ sk fk ->
+      Obj.magic x s env __ sk (fun e ->
+        Obj.magic y e s env __ sk fk))
   
   (** val split :
       'a1 t -> proofview -> Environ.env -> __
@@ -320,59 +327,63 @@ module Logical =
       -> (exn -> 'a2 IOBase.coq_T) -> 'a2
       IOBase.coq_T **)
   
-  let split x s e r sk fk =
-    IOBase.bind
-      (Obj.magic x s e __ (fun a fk0 ->
-        IOBase.ret (Util.Inl
-          (a,(fun e0 _ sk0 fk1 ->
-          IOBase.bind (fk0 e0) (fun x0 ->
-            match x0 with
-            | Util.Inl p ->
-              let a0,x1 = p in
-              sk0 a0 (fun e1 ->
-                x1 e1 __ sk0 fk1)
-            | Util.Inr e1 -> fk1 e1)))))
-        (fun e0 -> IOBase.ret (Util.Inr e0)))
-      (fun x0 ->
-      let sk0 = fun a fk0 ->
-        let sk0 = fun a0 fk1 ->
-          let x1,c = a0 in
-          let sk0 = fun a1 fk2 ->
-            let y,c' = a1 in
-            sk (y,(if c then c' else false))
-              fk2
+  let split x =
+    (); (fun s e _ sk fk ->
+      IOBase.bind
+        (Obj.magic x s e __ (fun a fk0 ->
+          IOBase.ret (Util.Inl
+            (a,(fun e0 _ sk0 fk1 ->
+            IOBase.bind (fk0 e0) (fun x0 ->
+              match x0 with
+              | Util.Inl p ->
+                let a0,x1 = p in
+                sk0 a0 (fun e1 ->
+                  x1 e1 __ sk0 fk1)
+              | Util.Inr e1 -> fk1 e1)))))
+          (fun e0 ->
+          IOBase.ret (Util.Inr e0)))
+        (fun x0 ->
+        let sk0 = fun a fk0 ->
+          let sk0 = fun a0 fk1 ->
+            let x1,c = a0 in
+            let sk0 = fun a1 fk2 ->
+              let y,c' = a1 in
+              sk
+                (y,(if c then c' else false))
+                fk2
+            in
+            (match x1 with
+             | Util.Inl p ->
+               let p0,y = p in
+               let a1,s0 = p0 in
+               sk0 (((Util.Inl
+                 (a1,(fun e0 x2 ->
+                 y e0))),s0),true) fk1
+             | Util.Inr e0 ->
+               sk0 (((Util.Inr e0),s),true)
+                 fk1)
+          in
+          let x1,c = a in
+          let sk1 = fun a0 fk1 ->
+            let y,c' = a0 in
+            sk0 (y,(if c then c' else false))
+              fk1
           in
           (match x1 with
            | Util.Inl p ->
-             let p0,y = p in
-             let a1,s0 = p0 in
-             sk0 (((Util.Inl
-               (a1,(fun e0 x2 ->
-               y e0))),s0),true) fk1
+             let a0,y = p in
+             sk1 ((Util.Inl (a0,(fun e0 x2 ->
+               y e0))),true) fk0
            | Util.Inr e0 ->
-             sk0 (((Util.Inr e0),s),true) fk1)
-        in
-        let x1,c = a in
-        let sk1 = fun a0 fk1 ->
-          let y,c' = a0 in
-          sk0 (y,(if c then c' else false))
-            fk1
+             sk1 ((Util.Inr e0),true) fk0)
         in
-        (match x1 with
+        (match x0 with
          | Util.Inl p ->
-           let a0,y = p in
-           sk1 ((Util.Inl (a0,(fun e0 x2 ->
-             y e0))),true) fk0
+           let p0,y = p in
+           let a,c = p0 in
+           sk0 ((Util.Inl (a,y)),c) fk
          | Util.Inr e0 ->
-           sk1 ((Util.Inr e0),true) fk0)
-      in
-      (match x0 with
-       | Util.Inl p ->
-         let p0,y = p in
-         let a,c = p0 in
-         sk0 ((Util.Inl (a,y)),c) fk
-       | Util.Inr e0 ->
-         sk0 ((Util.Inr e0),true) fk))
+           sk0 ((Util.Inr e0),true) fk)))
   
   (** val lift :
       'a1 NonLogical.t -> proofview ->
@@ -382,9 +393,10 @@ module Logical =
       (exn -> 'a2 IOBase.coq_T) -> 'a2
       IOBase.coq_T **)
   
-  let lift x s e r sk fk =
-    IOBase.bind x (fun x0 ->
-      sk ((x0,s),true) fk)
+  let lift x =
+    (); (fun s e _ sk fk ->
+      IOBase.bind x (fun x0 ->
+        sk ((x0,s),true) fk))
   
   (** val run :
       'a1 t -> logicalEnvironment ->