A version of convert_concl and convert_hyp in new proof engine.

Not very optimized though (if we apply convert_hyp on any hyp, a new
evar will be generated for every different hyp...).

4 files changed, 50 insertions, 18 deletions

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 334e0c22a3..eb9ffd425c 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -563,7 +563,7 @@ let autounfold_one db cl gl =
     if did then
       match cl with
       | Some hyp -> change_in_hyp None (fun env sigma -> sigma, c') hyp gl
-      | None -> convert_concl_no_check c' DEFAULTcast gl
+      | None -> Proofview.V82.of_tactic (convert_concl_no_check c' DEFAULTcast) gl
     else tclFAIL 0 (str "Nothing to unfold") gl
 
 (* 	  Cset.fold (fun cst -> cons (all_occurrences, EvalConstRef cst)) csts *)
@@ -611,7 +611,7 @@ END
 
 
 TACTIC EXTEND convert_concl_no_check
-| ["convert_concl_no_check" constr(x) ] -> [ Proofview.V82.tactic (convert_concl_no_check x DEFAULTcast) ]
+| ["convert_concl_no_check" constr(x) ] -> [ convert_concl_no_check x DEFAULTcast ]
 END
 
 
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 63885318c7..0207b9b0f3 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1543,7 +1543,7 @@ let cl_rewrite_clause_newtac ?abs strat clause =
 	| Some id, (undef, Some p, newt) ->
 	    assert_replacing id newt (new_refine (undef, p))
 	| Some id, (undef, None, newt) ->
-            Proofview.V82.tactic (Tacmach.convert_hyp_no_check (id, None, newt))
+            convert_hyp_no_check (id, None, newt)
 	| None, (undef, Some p, newt) ->
             Proofview.Goal.enter begin fun gl ->
             let env = Proofview.Goal.env gl in
@@ -1555,7 +1555,7 @@ let cl_rewrite_clause_newtac ?abs strat clause =
             Proofview.Refine.refine make
             end
 	| None, (undef, None, newt) ->
-            Proofview.V82.tactic (Tacmach.convert_concl_no_check newt DEFAULTcast)
+            convert_concl_no_check newt DEFAULTcast
   in
   Proofview.Goal.nf_enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 68aac55c8c..391affd112 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -118,8 +118,38 @@ let _ =
 
 let introduction    = Tacmach.introduction
 let refine          = Tacmach.refine
-let convert_concl   = Tacmach.convert_concl
-let convert_hyp     = Tacmach.convert_hyp
+
+let convert_concl ?(unsafe=false) ty k =
+  Proofview.Goal.nf_enter begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
+    let conclty = Proofview.Goal.raw_concl gl in
+    let sigma =
+      if not unsafe then begin
+        ignore (Typing.type_of env sigma ty);
+        let sigma,b = Reductionops.infer_conv env sigma ty conclty in
+        if not b then error "Not convertible.";
+        sigma
+      end else sigma in
+    Tacticals.New.tclTHEN
+      (Proofview.V82.tclEVARS sigma)
+      (Proofview.Refine.refine (fun h ->
+        let (h,x) = Proofview.Refine.new_evar h env ty in
+        (h, if k == DEFAULTcast then x else mkCast(x,k,conclty))))
+  end
+
+let convert_hyp ?(unsafe=false) d =
+  Proofview.Goal.nf_enter begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
+    let ty = Proofview.Goal.raw_concl gl in
+    let sign = convert_hyp (not unsafe) (named_context_val env) sigma d in
+    let env = reset_with_named_context sign env in
+    Proofview.Refine.refine (fun h -> Proofview.Refine.new_evar h env ty)
+  end
+
+let convert_concl_no_check = convert_concl ~unsafe:true
+let convert_hyp_no_check = convert_hyp ~unsafe:true
 
 let convert_gen pb x y =
   Proofview.Goal.enter begin fun gl ->
@@ -390,11 +420,11 @@ let bind_red_expr_occurrences occs nbcl redexp =
    certain hypothesis *)
 
 let reduct_in_concl (redfun,sty) gl =
-  convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) sty gl
+  Proofview.V82.of_tactic (convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) sty) gl
 
 let reduct_in_hyp redfun (id,where) gl =
-  convert_hyp_no_check
-    (pf_reduce_decl redfun where (pf_get_hyp gl id) gl) gl
+  Proofview.V82.of_tactic (convert_hyp_no_check
+    (pf_reduce_decl redfun where (pf_get_hyp gl id) gl)) gl
 
 let revert_cast (redfun,kind as r) =
   if kind == DEFAULTcast then (redfun,REVERTcast) else r
@@ -413,7 +443,7 @@ let tclWITHEVARS f k gl =
 let e_reduct_in_concl (redfun,sty) gl =
   tclWITHEVARS
     (fun env sigma -> redfun env sigma (pf_concl gl))
-    (fun c -> convert_concl_no_check c sty) gl
+    (fun c -> Proofview.V82.of_tactic (convert_concl_no_check c sty)) gl
 
 let e_pf_reduce_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env sigma =
   match c with
@@ -430,7 +460,7 @@ let e_pf_reduce_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env
 let e_reduct_in_hyp redfun (id,where) gl =
   tclWITHEVARS
     (e_pf_reduce_decl redfun where (pf_get_hyp gl id))
-    convert_hyp_no_check gl
+    (fun s -> Proofview.V82.of_tactic (convert_hyp_no_check s)) gl
 
 type change_arg = env -> evar_map -> evar_map * constr
 
@@ -1690,7 +1720,7 @@ let constructor_tac with_evars expctdnumopt i lbind =
       let apply_tac = general_apply true false with_evars None (dloc,(cons,lbind)) in
 	(Tacticals.New.tclTHENLIST
            [Proofview.V82.tclEVARS sigma; 
-	    Proofview.V82.tactic (convert_concl_no_check redcl DEFAULTcast); 
+	    convert_concl_no_check redcl DEFAULTcast;
 	    intros; apply_tac])
   end
 
@@ -2098,9 +2128,9 @@ let letin_tac_gen with_eq abs ty =
 	let (sigma,newcl,eq_tac) = eq_tac gl in
 	  Tacticals.New.tclTHENLIST
 	    [ Proofview.V82.tclEVARS sigma;
-	      Proofview.V82.tactic (convert_concl_no_check newcl DEFAULTcast);
+	      convert_concl_no_check newcl DEFAULTcast;
               intro_gen (NamingMustBe (dloc,id)) (decode_hyp lastlhyp) true false;
-              Proofview.V82.tactic (tclMAP convert_hyp_no_check depdecls);
+              Tacticals.New.tclMAP convert_hyp_no_check depdecls;
               eq_tac ]))
   end
 
@@ -3894,7 +3924,7 @@ let symmetry_red allowred =
   match with_eqn with
   | Some eq_data,_,_ ->
       Tacticals.New.tclTHEN
-        (Proofview.V82.tactic (convert_concl_no_check concl DEFAULTcast))
+        (convert_concl_no_check concl DEFAULTcast)
         (Tacticals.New.pf_constr_of_global eq_data.sym apply)
   | None,eq,eq_kind -> prove_symmetry eq eq_kind
   end
@@ -3986,7 +4016,7 @@ let transitivity_red allowred t =
   match with_eqn with
   | Some eq_data,_,_ ->
       Tacticals.New.tclTHEN
-        (Proofview.V82.tactic (convert_concl_no_check concl DEFAULTcast))
+        (convert_concl_no_check concl DEFAULTcast)
         (match t with
 	  | None -> Tacticals.New.pf_constr_of_global eq_data.trans eapply
 	  | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans (fun trans -> apply_list [trans;t]))
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 6ecb481018..c2beefdfb8 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -32,8 +32,10 @@ val is_quantified_hypothesis : Id.t -> goal sigma -> bool
 
 val introduction    : Id.t -> tactic
 val refine          : constr -> tactic
-val convert_concl   : constr -> cast_kind -> tactic
-val convert_hyp     : named_declaration -> tactic
+val convert_concl   : ?unsafe:bool -> types -> cast_kind -> unit Proofview.tactic
+val convert_hyp     : ?unsafe:bool -> named_declaration -> unit Proofview.tactic
+val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic
+val convert_hyp_no_check : named_declaration -> unit Proofview.tactic
 val thin            : Id.t list -> tactic
 val mutual_fix      :
   Id.t -> int -> (Id.t * int * constr) list -> int -> tactic