Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Adding a [map] primitive to the tactic monad. Hopefully this should be

slightly more efficient in general.
  • Loading branch information...
commit 0f3f29792b8165b7eb89c049c76d065942739674 1 parent 635f559
@ppedrot ppedrot authored
View
28 bootstrap/Monads.v
@@ -123,7 +123,8 @@ Record Monad (T:Set->Set) := {
ret : forall{A:Set}, A->T A;
bind : forall{A B:Set}, T A -> (A -> T B) -> T B;
ignore : forall{A:Set}, T A -> T unit;
- seq : forall{A:Set}, T unit -> T A -> T A
+ seq : forall{A:Set}, T unit -> T A -> T A;
+ map : forall {A B : Set}, (A -> B) -> T A -> T B
}.
Notation "'do' M x ':=' e 'in' u" := (bind _ M e (fun x => u)).
@@ -175,7 +176,8 @@ Module Id.
ret := fun _ x => x;
bind := fun _ _ x k => k x;
ignore := fun _ x => ();
- seq := fun _ x k => k
+ seq := fun _ x k => k;
+ map := fun _ _ f x => f x
|}.
End Id.
@@ -199,6 +201,9 @@ Module IOBase.
Parameter seq : forall A, T unit -> T A -> T A.
Extract Constant seq => "fun a k -> (); fun () -> a (); k ()".
Extraction Implicit seq [A].
+ Parameter map : forall (A B : Set), (A -> B) -> T A -> T B.
+ Extract Constant map => "fun f a -> (); fun () -> f (a ())".
+ Extraction Implicit map [A B].
Parameter ref : forall (A:Set), A -> T (Ref A).
Extract Constant ref => "fun a -> (); fun () -> Pervasives.ref a".
@@ -277,7 +282,8 @@ Module IO.
ret := IOBase.ret;
bind := IOBase.bind;
ignore := IOBase.ignore;
- seq := IOBase.seq
+ seq := IOBase.seq;
+ map := IOBase.map
|}.
Definition IO : S Ref T := {|
@@ -314,7 +320,8 @@ Section Common.
ignore A x := fun R k s =>
x R (fun _ s' => k tt s') s ;
seq A x y := fun R k s =>
- x R (fun _ s' => y R k s') s
+ x R (fun _ s' => y R k s') s;
+ map A B f x := fun R k s => x R (fun a s => k (f a) s) s
|}.
Definition State : State S T := {|
@@ -376,7 +383,8 @@ Section Common.
ret A x := fun R k e => k x;
bind A B x f := fun R k e => x _ (fun a => f a _ k e) e;
ignore A x := fun R k e => x _ (fun _ => k tt) e;
- seq A x y := fun R k e => x _ (fun _ => y _ k e) e
+ seq A x y := fun R k e => x _ (fun _ => y _ k e) e;
+ map A B f x := fun R k e => x _ (fun a => k (f a)) e
|}.
Definition Environment : Environment E T := {|
@@ -432,7 +440,8 @@ Section Common.
x _ (fun a c => f a _ (fun b c' => k b (Monoid.prod _ m c c')));
ignore A x := fun R k => x _ (fun _ c => k tt c);
seq A x y := fun R k =>
- x _ (fun _ c => y _ (fun b c' => k b (Monoid.prod _ m c c')))
+ x _ (fun _ c => y _ (fun b c' => k b (Monoid.prod _ m c c')));
+ map A B f x := fun R k => x _ (fun a c => k (f a) c)
|}.
Definition Writer : Writer C T := {|
@@ -507,7 +516,8 @@ Section Common.
ignore A x R sk fk :=
x _ (fun _ fk => sk () fk) fk;
seq A x k R sk fk :=
- x _ (fun _ fk => k _ sk fk) fk
+ x _ (fun _ fk => k _ sk fk) fk;
+ map A B f x R sk fk := x _ (fun a fk => sk (f a) fk) fk
|}.
Definition lift {A} (x:T₀ A) : T A := fun _ sk fk =>
@@ -637,6 +647,8 @@ Module NonLogical.
Extraction Implicit ignore [a].
Definition seq {a:Set} (x:t unit) (k:t a) : t a := Eval compute in seq _ NonLogicalMonad x k.
Extraction Implicit seq [a].
+ Definition map {a b:Set} (f:a -> b) (x:t a) : t b := Eval compute in freeze _ (map _ NonLogicalMonad f x).
+ Extraction Implicit map [a b].
Definition new_ref {a:Set} (x:a) : t (ref a) := Eval compute in IO.ref _ _ NonLogicalIO x.
Extraction Implicit new_ref [a].
@@ -679,6 +691,8 @@ Module Logical.
Extraction Implicit ignore [a].
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 map {a b:Set} (f:a -> b) (x:t a) : t b := Eval compute in freeze _ (map _ LogicalMonad f x).
+ Extraction Implicit map [a b].
Definition set (s:LogicalState) : t unit := Eval compute in freeze _ (set _ _ LogicalStateM s).
Definition get : t LogicalState := Eval compute in get _ _ LogicalStateM.
View
22 proofs/proofview.ml
@@ -385,8 +385,7 @@ let list_iter_goal s i =
~adv: begin fun goal ->
set_comb [goal] >>
i goal r >>= fun r ->
- Proof.get >>= fun step ->
- Proof.ret ( r , step.comb::subgoals )
+ Proof.map (fun step -> (r, step.comb :: subgoals)) Proof.get
end
end >>= fun (r,subgoals) ->
set_comb (List.flatten (List.rev subgoals)) >>
@@ -405,8 +404,7 @@ let list_iter_goal2 l s i =
~adv: begin fun goal ->
set_comb [goal] >>
i goal a r >>= fun r ->
- Proof.get >>= fun step ->
- Proof.ret ( r , step.comb::subgoals )
+ Proof.map (fun step -> (r, step.comb :: subgoals)) Proof.get
end
end >>= fun (r,subgoals) ->
set_comb (List.flatten (List.rev subgoals)) >>
@@ -434,17 +432,14 @@ let tclDISPATCHGEN f join tacs =
on_advance goal
~solved:( tclUNIT (join []) )
~adv:begin fun _ ->
- f tac >>= fun res ->
- Proof.ret (join [res])
+ Proof.map (fun res -> join [res]) (f tac)
end
| _ -> tclZERO SizeMismatch
end
| _ ->
- list_iter_goal2 tacs [] begin fun _ t cur ->
- f t >>= fun y ->
- Proof.ret ( y :: cur )
- end >>= fun res ->
- Proof.ret (join res)
+ let iter _ t cur = Proof.map (fun y -> y :: cur) (f t) in
+ let ans = list_iter_goal2 tacs [] iter in
+ Proof.map join ans
let tclDISPATCH tacs = tclDISPATCHGEN Util.identity ignore tacs
@@ -532,10 +527,7 @@ let tclPROGRESS t =
tclZERO (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress."))
let tclEVARMAP =
- (* spiwack: convenience notations, waiting for ocaml 3.12 *)
- let (>>=) = Proof.bind in
- Proof.get >>= fun initial ->
- Proof.ret (initial.solution)
+ Proof.map (fun initial -> initial.solution) Proof.get
let tclENV = Proof.current
View
33 proofs/proofview_gen.ml
@@ -31,6 +31,10 @@ module IOBase =
let seq = fun a k -> (); fun () -> a (); k ()
+ (** val map : ('a1 -> 'a2) -> 'a1 coq_T -> 'a2 coq_T **)
+
+ let map = fun f a -> (); fun () -> f (a ())
+
(** val ref : 'a1 -> 'a1 coq_Ref coq_T **)
let ref = fun a -> (); fun () -> Pervasives.ref a
@@ -124,6 +128,11 @@ module NonLogical =
let seq x k =
IOBase.seq x k
+ (** val map : ('a1 -> 'a2) -> 'a1 t -> 'a2 t **)
+
+ let map f x =
+ (); (IOBase.map f x)
+
(** val new_ref : 'a1 -> 'a1 ref t **)
let new_ref x =
@@ -296,6 +305,30 @@ module Logical =
let seq x k =
(); (fun _ k0 s -> Obj.magic x __ (fun x1 s' -> Obj.magic k __ k0 s') s)
+ (** val map :
+ ('a1 -> 'a2) -> 'a1 t -> __ -> ('a2 -> proofview -> __ -> ('a3 -> __ ->
+ (__ -> (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ Environ.env -> __ -> (__ -> (bool*(Goal.goal list*Goal.goal list)) ->
+ __ -> (__ -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> (__ -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> proofview -> __ -> ('a3 -> __ -> ('a4 ->
+ (bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __
+ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> __ -> (__ -> (exn -> __ IOBase.coq_T) -> __
+ IOBase.coq_T) -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) ->
+ Environ.env -> __ -> ('a4 -> (bool*(Goal.goal list*Goal.goal list)) ->
+ __ -> ('a5 -> (exn -> __ IOBase.coq_T) -> __ IOBase.coq_T) -> (exn ->
+ __ IOBase.coq_T) -> __ IOBase.coq_T) -> __ -> ('a5 -> (exn -> 'a6
+ IOBase.coq_T) -> 'a6 IOBase.coq_T) -> (exn -> 'a6 IOBase.coq_T) -> 'a6
+ IOBase.coq_T **)
+
+ let map f x =
+ (); (fun _ k s -> Obj.magic x __ (fun a s0 -> k (f a) s0) s)
+
(** val set :
logicalState -> __ -> (unit -> proofview -> __ -> ('a1 -> __ -> (__ ->
(bool*(Goal.goal list*Goal.goal list)) -> __ -> (__ -> (exn -> __
View
2  proofs/proofview_monad.mli
@@ -23,6 +23,7 @@ module NonLogical : sig
val ret : 'a -> 'a t
val bind : 'a t -> ('a -> 'b t) -> 'b t
+ val map : ('a -> 'b) -> 'a t -> 'b t
val ignore : 'a t -> unit t
val seq : unit t -> 'a t -> 'a t
@@ -51,6 +52,7 @@ module Logical : sig
val ret : 'a -> 'a t
val bind : 'a t -> ('a -> 'b t) -> 'b t
+ val map : ('a -> 'b) -> 'a t -> 'b t
val ignore : 'a t -> unit t
val seq : unit t -> 'a t -> 'a t
Please sign in to comment.
Something went wrong with that request. Please try again.