aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--bootstrap/Monads.v61
-rw-r--r--proofs/proofview_gen.ml208
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 ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 04:12:16 +0000