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

2 files changed, 148 insertions, 121 deletions

diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
index c9cdfc2ad6..6aae038b0a 100644
--- a/bootstrap/Monads.v
+++ b/bootstrap/Monads.v
@@ -35,6 +35,21 @@ Extract Inductive sum => "Util.union" [
   "Util.Inr"
 ].
 
+(*** Closure elimination **)
+
+(* [freeze] is used to help OCaml figure where partial applications
+   are usually made. This way, the compiler will output code optimised
+   for partial applications to happen at this point. It happens to
+   make the monadic code substantially faster.
+
+   Documentation on that particular behaviour can be found at:
+   https://ocaml.janestreet.com/?q=node/30
+*)
+
+Parameter freeze : forall (A : Set), A -> A.
+Extraction Implicit freeze [A].
+Extract Inlined Constant freeze => "();".
+
 (*** Exceptions ***)
 
 Parameter Exception : Set.
@@ -152,44 +167,44 @@ Module IOBase.
  Extract Constant Ref "'a" => "'a Pervasives.ref".
 
  Parameter ret : forall (A:Set), A -> T A.
- Extract Constant ret => "fun a () -> a".
+ Extract Constant ret => "fun a -> (); fun () -> a".
  Extraction Implicit ret [A].
  Parameter bind : forall A B, T A -> (A->T B) -> T B.
- Extract Constant bind => "fun a k () -> k (a ()) ()".
+ Extract Constant bind => "fun a k -> (); fun () -> k (a ()) ()".
  Extraction Implicit bind [A B].
  Parameter ignore : forall A, T A -> T unit.
- Extract Constant ignore => "fun a () -> ignore (a ())".
+ Extract Constant ignore => "fun a -> (); fun () -> ignore (a ())".
  Extraction Implicit ignore [A].
  Parameter seq : forall A, T unit -> T A -> T A.
- Extract Constant seq => "fun a k () -> a (); k ()".
+ Extract Constant seq => "fun a k -> (); fun () -> a (); k ()".
  Extraction Implicit seq [A].
 
  Parameter ref : forall (A:Set), A -> T (Ref A).
- Extract Constant ref => "fun a () -> Pervasives.ref a".
+ Extract Constant ref => "fun a -> (); fun () -> Pervasives.ref a".
  Extraction Implicit ref [A].
  Parameter set : forall A, Ref A -> A -> T unit.
- Extract Constant set => "fun r a () -> Pervasives.(:=) r a".
+ Extract Constant set => "fun r a -> (); fun () -> Pervasives.(:=) r a".
  Extraction Implicit set [A].
  Parameter get : forall A, Ref A -> T A.
- Extract Constant get => "fun r () -> Pervasives.(!) r".
+ Extract Constant get => "fun r -> (); fun () -> Pervasives.(!) r".
  Extraction Implicit get [A].
 
  Parameter raise : forall A, Exception -> T A.
- Extract Constant raise => "fun e () -> raise (Proof_errors.Exception e)".
+ Extract Constant raise => "fun e -> (); fun () -> raise (Proof_errors.Exception e)".
  Extraction Implicit raise [A].
  Parameter catch : forall A, T A -> (Exception -> T A) -> T A.
- Extract Constant catch => "fun s h () -> try s () with Proof_errors.Exception e -> h e ()".
+ Extract Constant catch => "fun s h -> (); fun () -> try s () with Proof_errors.Exception e -> h e ()".
  Extraction Implicit catch [A].
 
  Parameter read_line : T String.
  Extract Constant read_line => "fun () -> try Pervasives.read_line () with e -> raise e ()".
  Parameter print_char : Char -> T unit.
- Extract Constant print_char => "fun c () -> print_char c".
+ Extract Constant print_char => "fun c -> (); fun () -> print_char c".
  Parameter print : Ppcmds -> T unit.
- Extract Constant print => "fun s () -> try Pp.pp s; Pp.pp_flush () with e -> raise e ()".
+ Extract Constant print => "fun s -> (); fun () -> try Pp.pp s; Pp.pp_flush () with e -> raise e ()".
 
  Parameter timeout: forall A, Int -> T A -> T A.
- Extract Constant timeout => "fun n t () ->
+ Extract Constant 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);
@@ -597,28 +612,28 @@ Module Logical.
 
  Definition t (a:Set) := Eval compute in LogicalType a.
 
- Definition ret {a:Set} (x:a) : t a := Eval compute in ret _ LogicalMonad x.
+ Definition ret {a:Set} (x:a) : t a := Eval compute in freeze _ (ret _ LogicalMonad x).
  Extraction Implicit ret [a].
- Definition bind {a b:Set} (x:t a) (k:a-> t b) : t b := Eval compute in bind _ LogicalMonad x k.
+ Definition bind {a b:Set} (x:t a) (k:a-> t b) : t b := Eval compute in freeze _ (bind _ LogicalMonad x k).
  Extraction Implicit bind [a b].
- Definition ignore {a:Set} (x:t a) : t unit := Eval compute in ignore _ LogicalMonad x.
+ Definition ignore {a:Set} (x:t a) : t unit := Eval compute in freeze _ (ignore _ LogicalMonad x).
  Extraction Implicit ignore [a].
- Definition seq {a:Set} (x:t unit) (k:t a) : t a := Eval compute in seq _ LogicalMonad x k.
+ Definition seq {a:Set} (x:t unit) (k:t a) : t a := Eval compute in freeze _ (seq _ LogicalMonad x k).
  Extraction Implicit seq [a].
 
- Definition set (s:LogicalState) : t unit := Eval compute in set _ _ LogicalStateM s.
+ Definition set (s:LogicalState) : t unit := Eval compute in freeze _ (set _ _ LogicalStateM s).
  Definition get : t LogicalState := Eval compute in get _ _ LogicalStateM.
- Definition put (m:LogicalMessageType) : t unit := Eval compute in State.lift _ _ LogicalMonadEnv (Environment.lift _ _ (put _ _ LogicalWriter m)).
+ Definition put (m:LogicalMessageType) : t unit := Eval compute in freeze _ (State.lift _ _ LogicalMonadEnv (Environment.lift _ _ (put _ _ LogicalWriter m))).
  Definition current : t LogicalEnvironment := Eval compute in State.lift _ _ LogicalMonadEnv (current _ _ LogicalReader).
 
- Definition zero {a:Set} (e:Exception) : t a := Eval compute in zero _ LogicalLogic e.
+ Definition zero {a:Set} (e:Exception) : t a := Eval compute in freeze _ (zero _ LogicalLogic e).
  Extraction Implicit zero [a].
- Definition plus {a:Set} (x:t a) (y:Exception -> t a) : t a := Eval compute in plus _ LogicalLogic x y.
+ Definition plus {a:Set} (x:t a) (y:Exception -> t a) : t a := Eval compute in freeze _ (plus _ LogicalLogic x y).
  Extraction Implicit plus [a].
- Definition split {a:Set} (x:t a) : t ((a*(Exception -> t a))+Exception) := Eval compute in split _ LogicalLogic x.
+ Definition split {a:Set} (x:t a) : t ((a*(Exception -> t a))+Exception) := Eval compute in freeze _ (split _ LogicalLogic x).
  Extraction Implicit split [a].
  Definition lift {a:Set} (x:NonLogical.t a) : t a := Eval compute in
-  State.lift _ _ LogicalMonadEnv (Environment.lift _ _ (Writer.lift _ LogicalMessage _ LogicalMonadBase (Logic.lift _ NonLogicalMonad x))).
+  freeze _ (State.lift _ _ LogicalMonadEnv (Environment.lift _ _ (Writer.lift _ LogicalMessage _ LogicalMonadBase (Logic.lift _ NonLogicalMonad x)))).
  Extraction Implicit lift [a].
 
  Definition run {a:Set} (x:t a) (e:LogicalEnvironment) (s:LogicalState) : NonLogical.t ((a*LogicalState)*LogicalMessageType) := Eval compute in
@@ -633,7 +648,7 @@ Set Extraction Conservative Types.
 Set Extraction File Comment "
 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 bootstrap/Monad.v in Coq's source
+coqtop -batch -impredicative-set -l bootstrap/Monad.v in Coq's source
 directory.
 ".
 
diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml
index 4220958700..95609e12d6 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 ->