More Proofview.Goal.enter.

Proofview.Goal.enter is meant to eventually replace the Goal.sensitive monad.

This commit changes the type of Proofview.Goal.enter from taking a four argument function (environment, evar_map, hyps, concl) from a one argument function of abstract type Proofview.Goal.t. It will be both more extensible and more akin to old-style tactics.

This commit also changes the type of Proofview.Goal.{concl,hyps,env} from monadic operations to projection from a Proofview.Goal.t.

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

1 files changed, 125 insertions, 121 deletions

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index fbf9334e0..c865639e6 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1647,17 +1647,18 @@ let destructure_hyps =
   Tacmach.New.pf_apply Typing.type_of >>= fun type_of ->
   Tacmach.New.of_old decidability >>= fun decidability ->
   Tacmach.New.of_old pf_nf >>= fun pf_nf ->
-  let rec loop = function
-    | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega)
-    | (i,body,t)::lit ->
-	begin try match destructurate_prop t with
+  Proofview.Goal.enter begin fun gl ->
+    let rec loop = function
+      | [] -> (Tacticals.New.tclTHEN nat_inject coq_omega)
+      | (i,body,t)::lit ->
+	  begin try match destructurate_prop t with
 	  | Kapp(False,[]) -> elim_id i
           | Kapp((Zle|Zge|Zgt|Zlt|Zne),[t1;t2]) -> loop lit
           | Kapp(Or,[t1;t2]) ->
               (Tacticals.New.tclTHENS
-                (elim_id i)
-                [ onClearedName i (fun i -> (loop ((i,None,t1)::lit)));
-                  onClearedName i (fun i -> (loop ((i,None,t2)::lit))) ])
+                 (elim_id i)
+                 [ onClearedName i (fun i -> (loop ((i,None,t1)::lit)));
+                   onClearedName i (fun i -> (loop ((i,None,t2)::lit))) ])
           | Kapp(And,[t1;t2]) ->
               Tacticals.New.tclTHEN
 		(elim_id i)
@@ -1676,7 +1677,7 @@ let destructure_hyps =
 		let d1 = decidability t1 in
 		Tacticals.New.tclTHENLIST [
 		  Proofview.V82.tactic (generalize_tac [mkApp (Lazy.force coq_imp_simp,
-                    [| t1; t2; d1; mkVar i|])]);
+                                                               [| t1; t2; d1; mkVar i|])]);
 		  (onClearedName i (fun i ->
 		    (loop ((i,None,mk_or (mk_not t1) t2)::lit))))
                 ]
@@ -1684,113 +1685,115 @@ let destructure_hyps =
 		loop lit
           | Kapp(Not,[t]) ->
               begin match destructurate_prop t with
-		  Kapp(Or,[t1;t2]) ->
-                    Tacticals.New.tclTHENLIST [
-		      Proofview.V82.tactic (generalize_tac
-                        [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]);
-		      (onClearedName i (fun i ->
-                        (loop ((i,None,mk_and (mk_not t1) (mk_not t2)):: lit))))
-                    ]
-		| Kapp(And,[t1;t2]) ->
-		    let d1 = decidability t1 in
-                    Tacticals.New.tclTHENLIST [
-		      Proofview.V82.tactic (generalize_tac
-		        [mkApp (Lazy.force coq_not_and,
-				[| t1; t2; d1; mkVar i |])]);
-		      (onClearedName i (fun i ->
-                        (loop ((i,None,mk_or (mk_not t1) (mk_not t2))::lit))))
-                    ]
-		| Kapp(Iff,[t1;t2]) ->
-		    let d1 = decidability t1 in
-		    let d2 = decidability t2 in
-                    Tacticals.New.tclTHENLIST [
-		      Proofview.V82.tactic (generalize_tac
-		        [mkApp (Lazy.force coq_not_iff,
-				[| t1; t2; d1; d2; mkVar i |])]);
-		      (onClearedName i (fun i ->
-                        (loop ((i,None,
-			        mk_or (mk_and t1 (mk_not t2))
-				      (mk_and (mk_not t1) t2))::lit))))
-                    ]
-		| Kimp(t1,t2) ->
+		Kapp(Or,[t1;t2]) ->
+                  Tacticals.New.tclTHENLIST [
+		    Proofview.V82.tactic (generalize_tac
+                                            [mkApp (Lazy.force coq_not_or,[| t1; t2; mkVar i |])]);
+		    (onClearedName i (fun i ->
+                      (loop ((i,None,mk_and (mk_not t1) (mk_not t2)):: lit))))
+                  ]
+	      | Kapp(And,[t1;t2]) ->
+		  let d1 = decidability t1 in
+                  Tacticals.New.tclTHENLIST [
+		    Proofview.V82.tactic (generalize_tac
+		                            [mkApp (Lazy.force coq_not_and,
+				                    [| t1; t2; d1; mkVar i |])]);
+		    (onClearedName i (fun i ->
+                      (loop ((i,None,mk_or (mk_not t1) (mk_not t2))::lit))))
+                  ]
+	      | Kapp(Iff,[t1;t2]) ->
+		  let d1 = decidability t1 in
+		  let d2 = decidability t2 in
+                  Tacticals.New.tclTHENLIST [
+		    Proofview.V82.tactic (generalize_tac
+		                            [mkApp (Lazy.force coq_not_iff,
+				                    [| t1; t2; d1; d2; mkVar i |])]);
+		    (onClearedName i (fun i ->
+                      (loop ((i,None,
+			      mk_or (mk_and t1 (mk_not t2))
+				(mk_and (mk_not t1) t2))::lit))))
+                  ]
+	      | Kimp(t1,t2) ->
 		    (* t2 must be in Prop otherwise ~(t1->t2) wouldn't be ok.
 		       For t1, being decidable implies being Prop. *)
-		    let d1 = decidability t1 in
-                    Tacticals.New.tclTHENLIST [
-		      Proofview.V82.tactic (generalize_tac
-		        [mkApp (Lazy.force coq_not_imp,
-				[| t1; t2; d1; mkVar i |])]);
-		      (onClearedName i (fun i ->
-                        (loop ((i,None,mk_and t1 (mk_not t2)) :: lit))))
-                    ]
-		| Kapp(Not,[t]) ->
-		    let d = decidability t in
-                    Tacticals.New.tclTHENLIST [
-		      Proofview.V82.tactic (generalize_tac
-			[mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]);
-		      (onClearedName i (fun i -> (loop ((i,None,t)::lit))))
-                    ]
-		| Kapp(op,[t1;t2]) ->
-		    (try
-		      let thm = not_binop op in
-                      Tacticals.New.tclTHENLIST [
-			Proofview.V82.tactic (generalize_tac
-			   [mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]);
-			(onClearedName i (fun _ -> loop lit))
-                      ]
-		     with Not_found -> loop lit)
-		| Kapp(Eq,[typ;t1;t2]) ->
-                    if !old_style_flag then begin
-		      match destructurate_type (pf_nf typ) with
-			| Kapp(Nat,_) ->
-                            Tacticals.New.tclTHENLIST [
-			      (simplest_elim
-				(mkApp
-                                  (Lazy.force coq_not_eq, [|t1;t2;mkVar i|])));
-			      (onClearedName i (fun _ -> loop lit))
-                            ]
-			| Kapp(Z,_) ->
-                            Tacticals.New.tclTHENLIST [
-			      (simplest_elim
-				(mkApp
-				  (Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|])));
-			      (onClearedName i (fun _ -> loop lit))
-                            ]
-			| _ -> loop lit
-                    end else begin
-		      match destructurate_type (pf_nf typ) with
-			| Kapp(Nat,_) ->
-                               (Tacticals.New.tclTHEN
-			       (Proofview.V82.tactic (convert_hyp_no_check
-                                  (i,body,
-				  (mkApp (Lazy.force coq_neq, [| t1;t2|])))))
-			       (loop lit))
-			| Kapp(Z,_) ->
-                               (Tacticals.New.tclTHEN
-			       (Proofview.V82.tactic (convert_hyp_no_check
-                                  (i,body,
-				  (mkApp (Lazy.force coq_Zne, [| t1;t2|])))))
-			       (loop lit))
-			| _ -> loop lit
-                    end
-		| _ -> loop lit
+		  let d1 = decidability t1 in
+                  Tacticals.New.tclTHENLIST [
+		    Proofview.V82.tactic (generalize_tac
+		                            [mkApp (Lazy.force coq_not_imp,
+				                    [| t1; t2; d1; mkVar i |])]);
+		    (onClearedName i (fun i ->
+                      (loop ((i,None,mk_and t1 (mk_not t2)) :: lit))))
+                  ]
+	      | Kapp(Not,[t]) ->
+		  let d = decidability t in
+                  Tacticals.New.tclTHENLIST [
+		    Proofview.V82.tactic (generalize_tac
+			                    [mkApp (Lazy.force coq_not_not, [| t; d; mkVar i |])]);
+		    (onClearedName i (fun i -> (loop ((i,None,t)::lit))))
+                  ]
+	      | Kapp(op,[t1;t2]) ->
+		  (try
+		     let thm = not_binop op in
+                     Tacticals.New.tclTHENLIST [
+		       Proofview.V82.tactic (generalize_tac
+			                       [mkApp (Lazy.force thm, [| t1;t2;mkVar i|])]);
+		       (onClearedName i (fun _ -> loop lit))
+                     ]
+		   with Not_found -> loop lit)
+	      | Kapp(Eq,[typ;t1;t2]) ->
+                  if !old_style_flag then begin
+		    match destructurate_type (pf_nf typ) with
+		    | Kapp(Nat,_) ->
+                        Tacticals.New.tclTHENLIST [
+			  (simplest_elim
+			     (mkApp
+                                (Lazy.force coq_not_eq, [|t1;t2;mkVar i|])));
+			  (onClearedName i (fun _ -> loop lit))
+                        ]
+		    | Kapp(Z,_) ->
+                        Tacticals.New.tclTHENLIST [
+			  (simplest_elim
+			     (mkApp
+				(Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|])));
+			  (onClearedName i (fun _ -> loop lit))
+                        ]
+		    | _ -> loop lit
+                  end else begin
+		    match destructurate_type (pf_nf typ) with
+		    | Kapp(Nat,_) ->
+                        (Tacticals.New.tclTHEN
+			   (Proofview.V82.tactic (convert_hyp_no_check
+                                                    (i,body,
+				                     (mkApp (Lazy.force coq_neq, [| t1;t2|])))))
+			   (loop lit))
+		    | Kapp(Z,_) ->
+                        (Tacticals.New.tclTHEN
+			   (Proofview.V82.tactic (convert_hyp_no_check
+                                                    (i,body,
+				                     (mkApp (Lazy.force coq_Zne, [| t1;t2|])))))
+			   (loop lit))
+		    | _ -> loop lit
+                  end
+	      | _ -> loop lit
               end
           | _ -> loop lit
-	with
-	  | Undecidable -> loop lit
-	  | e when catchable_exception e -> loop lit
-	end
-  in
-  Proofview.Goal.hyps >>= fun hyps ->
-  try (* type_of can raise exceptions *)
-    loop (Environ.named_context_of_val hyps)
-  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+	    with
+	    | Undecidable -> loop lit
+	    | e when catchable_exception e -> loop lit
+	  end
+    in
+    let hyps = Proofview.Goal.hyps gl in
+    try (* type_of can raise exceptions *)
+      loop (Environ.named_context_of_val hyps)
+    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+  end
 
 let destructure_goal =
-  Proofview.Goal.concl >>= fun concl ->
-  Tacmach.New.of_old decidability >>= fun decidability ->
-  let rec loop t =
-    match destructurate_prop t with
+  Proofview.Goal.enter begin fun gl ->
+    let concl = Proofview.Goal.concl gl in
+    Tacmach.New.of_old decidability >>= fun decidability ->
+    let rec loop t =
+      match destructurate_prop t with
       | Kapp(Not,[t]) ->
           (Tacticals.New.tclTHEN
 	     (Tacticals.New.tclTHEN (Proofview.V82.tactic (unfold sp_not)) intro)
@@ -1798,18 +1801,19 @@ let destructure_goal =
       | Kimp(a,b) -> (Tacticals.New.tclTHEN intro (loop b))
       | Kapp(False,[]) -> destructure_hyps
       | _ ->
-	let goal_tac =
-	  try
-	    let dec = decidability t in
-	    Tacticals.New.tclTHEN
-              (Proofview.V82.tactic (Tactics.refine
-		 (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |]))))
-	      intro
-	  with Undecidable -> Proofview.V82.tactic (Tactics.elim_type (build_coq_False ()))
-	in
-	Tacticals.New.tclTHEN goal_tac destructure_hyps
-  in
-  (loop concl)
+	  let goal_tac =
+	    try
+	      let dec = decidability t in
+	      Tacticals.New.tclTHEN
+                (Proofview.V82.tactic (Tactics.refine
+		                         (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |]))))
+	        intro
+	    with Undecidable -> Proofview.V82.tactic (Tactics.elim_type (build_coq_False ()))
+	  in
+	  Tacticals.New.tclTHEN goal_tac destructure_hyps
+    in
+    (loop concl)
+  end
 
 let destructure_goal = destructure_goal