Merge PR #9983: Hypothesis conversion allocates a single evar

Reviewed-by: gares
Ack-by: herbelin

8 files changed, 122 insertions, 124 deletions

diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 523c7c8305..ec5e46d89b 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -184,7 +184,7 @@ END
 
 
 TACTIC EXTEND convert_concl_no_check
-| ["convert_concl_no_check" constr(x) ] -> { Tactics.convert_concl_no_check x DEFAULTcast }
+| ["convert_concl_no_check" constr(x) ] -> { Tactics.convert_concl ~check:false x DEFAULTcast }
 END
 
 {
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 2d40ba6562..99a9c1ab9a 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1596,7 +1596,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
 	    tclTHENFIRST (assert_replacing id newt tac) (beta_hyp id)
 	| Some id, None ->
             Proofview.Unsafe.tclEVARS undef <*>
-            convert_hyp_no_check (LocalAssum (make_annot id Sorts.Relevant, newt)) <*>
+            convert_hyp ~check:false (LocalAssum (make_annot id Sorts.Relevant, newt)) <*>
             beta_hyp id
 	| None, Some p ->
             Proofview.Unsafe.tclEVARS undef <*>
@@ -1610,7 +1610,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
             end
 	| None, None ->
             Proofview.Unsafe.tclEVARS undef <*>
-            convert_concl_no_check newt DEFAULTcast
+            convert_concl ~check:false newt DEFAULTcast
   in
   Proofview.Goal.enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 4802608fda..f3bc791b8d 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -535,7 +535,7 @@ let focused_simpl path =
   let open Tacmach.New in
   Proofview.Goal.enter begin fun gl ->
   let newc = context (project gl) (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
-  convert_concl_no_check newc DEFAULTcast
+  convert_concl ~check:false newc DEFAULTcast
   end
 
 let focused_simpl path = focused_simpl path
@@ -687,7 +687,7 @@ let simpl_coeffs path_init path_k =
   let n = Pervasives.(-) (List.length path_k) (List.length path_init) in
   let newc = context sigma (fun _ t -> loop n t) (List.rev path_init) (pf_concl gl)
   in
-  convert_concl_no_check newc DEFAULTcast
+  convert_concl ~check:false newc DEFAULTcast
   end
 
 let rec shuffle p (t1,t2) =
@@ -1849,12 +1849,12 @@ let destructure_hyps =
                     match destructurate_type env sigma typ with
 		    | Kapp(Nat,_) ->
                         (tclTHEN
-			   (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|]))
+                           (Tactics.convert_hyp ~check:false (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|]))
                                                                      decl))
 			   (loop lit))
 		    | Kapp(Z,_) ->
                         (tclTHEN
-			   (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|]))
+                           (Tactics.convert_hyp ~check:false (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|]))
                                                                      decl))
 			   (loop lit))
 		    | _ -> loop lit
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index a05b1e3d81..a4caeb403c 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -426,7 +426,7 @@ let mk_anon_id t gl_ids =
     (set s i (Char.chr (Char.code (get s i) + 1)); s) in
   Id.of_string_soft (Bytes.to_string (loop (n - 1)))
 
-let convert_concl_no_check t = Tactics.convert_concl_no_check t DEFAULTcast
+let convert_concl_no_check t = Tactics.convert_concl ~check:false t DEFAULTcast
 let convert_concl t = Tactics.convert_concl t DEFAULTcast
 
 let rename_hd_prod orig_name_ref gl =
@@ -1409,8 +1409,6 @@ let tclINTRO_ANON ?seed () =
   | Some seed -> tclINTRO ~id:(Seed seed) ~conclusion:return
 
 let tclRENAME_HD_PROD name = Goal.enter begin fun gl ->
-  let convert_concl_no_check t =
-    Tactics.convert_concl_no_check t DEFAULTcast in
   let concl = Goal.concl gl in
   let sigma = Goal.sigma gl in
   match EConstr.kind sigma concl with
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index bbe7bde78b..17e4114958 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -110,7 +110,7 @@ let endclausestac id_map clseq gl_id cl0 gl =
   | _ -> EConstr.map (project gl) unmark c in
   let utac hyp =
     Proofview.V82.of_tactic 
-     (Tactics.convert_hyp_no_check (NamedDecl.map_constr unmark hyp)) in
+     (Tactics.convert_hyp ~check:false (NamedDecl.map_constr unmark hyp)) in
   let utacs = List.map utac (pf_hyps gl) in
   let ugtac gl' =
     Proofview.V82.of_tactic
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 3019fc0231..70854e6e3c 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -515,6 +515,6 @@ let autounfold_one db cl =
     if did then
       match cl with
       | Some hyp -> change_in_hyp None (make_change_arg c') hyp
-      | None -> convert_concl_no_check c' DEFAULTcast
+      | None -> convert_concl ~check:false c' DEFAULTcast
     else Tacticals.New.tclFAIL 0 (str "Nothing to unfold")
   end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 066b9c7794..b70dd63211 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -614,18 +614,22 @@ let cofix id = mutual_cofix id [] 0
 type tactic_reduction = Reductionops.reduction_function
 type e_tactic_reduction = Reductionops.e_reduction_function
 
-let pf_reduce_decl redfun where decl gl =
+let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigma =
   let open Context.Named.Declaration in
-  let redfun' c = Tacmach.New.pf_apply redfun gl c in
   match decl with
   | LocalAssum (id,ty) ->
       if where == InHypValueOnly then
         user_err  (Id.print id.binder_name ++ str " has no value.");
-      LocalAssum (id,redfun' ty)
+    let (sigma, ty') = redfun false env sigma ty in
+    (sigma, LocalAssum (id, ty'))
   | LocalDef (id,b,ty) ->
-      let b' = if where != InHypTypeOnly then redfun' b else b in
-      let ty' =	if where != InHypValueOnly then redfun' ty else ty in
-      LocalDef (id,b',ty')
+      let (sigma, b') =
+        if where != InHypTypeOnly then redfun true env sigma b else (sigma, b)
+      in
+      let (sigma, ty') =
+        if where != InHypValueOnly then redfun false env sigma ty else (sigma, ty)
+      in
+      (sigma, LocalDef (id,b',ty'))
 
 (* Possibly equip a reduction with the occurrences mentioned in an
    occurrence clause *)
@@ -695,41 +699,9 @@ let bind_red_expr_occurrences occs nbcl redexp =
    reduction function either to the conclusion or to a
    certain hypothesis *)
 
-let reduct_in_concl (redfun,sty) =
-  Proofview.Goal.enter begin fun gl ->
-    convert_concl_no_check (Tacmach.New.pf_apply redfun gl (Tacmach.New.pf_concl gl)) sty
-  end
-
-let reduct_in_hyp ?(check=false) redfun (id,where) =
-  Proofview.Goal.enter begin fun gl ->
-  convert_hyp ~check (pf_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl)
-  end
-
-let revert_cast (redfun,kind as r) =
-  if kind == DEFAULTcast then (redfun,REVERTcast) else r
-
-let reduct_option ?(check=false) redfun = function
-  | Some id -> reduct_in_hyp ~check (fst redfun) id
-  | None    -> reduct_in_concl (revert_cast redfun)
-
 (** Tactic reduction modulo evars (for universes essentially) *)
 
-let pf_e_reduce_decl redfun where decl gl =
-  let open Context.Named.Declaration in
-  let sigma = Proofview.Goal.sigma gl in
-  let redfun sigma c = redfun (Tacmach.New.pf_env gl) sigma c in
-  match decl with
-  | LocalAssum (id,ty) ->
-      if where == InHypValueOnly then
-        user_err  (Id.print id.binder_name ++ str " has no value.");
-    let (sigma, ty') = redfun sigma ty in
-    (sigma, LocalAssum (id, ty'))
-  | LocalDef (id,b,ty) ->
-      let (sigma, b') = if where != InHypTypeOnly then redfun sigma b else (sigma, b) in
-      let (sigma, ty') = if where != InHypValueOnly then redfun sigma ty else (sigma, ty) in
-      (sigma, LocalDef (id, b', ty'))
-
-let e_reduct_in_concl ~check (redfun, sty) =
+let e_change_in_concl ?(check = false) (redfun, sty) =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let (sigma, c') = redfun (Tacmach.New.pf_env gl) sigma (Tacmach.New.pf_concl gl) in
@@ -737,53 +709,64 @@ let e_reduct_in_concl ~check (redfun, sty) =
     (convert_concl ~check c' sty)
   end
 
-let e_reduct_in_hyp ?(check=false) redfun (id, where) =
+let e_change_in_hyp ?(check = false) redfun (id,where) =
   Proofview.Goal.enter begin fun gl ->
-    let (sigma, decl') = pf_e_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl in
+    let sigma = Proofview.Goal.sigma gl in
+    let hyp = Tacmach.New.pf_get_hyp id gl in
+    let (sigma, c) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
-    (convert_hyp ~check decl')
+    (convert_hyp ~check c)
   end
 
-let e_reduct_option ?(check=false) redfun = function
-  | Some id -> e_reduct_in_hyp ~check (fst redfun) id
-  | None    -> e_reduct_in_concl ~check (revert_cast redfun)
-
-(** Versions with evars to maintain the unification of universes resulting
-    from conversions. *)
-
-let e_change_in_concl (redfun,sty) =
+let e_change_in_hyps ?(check=true) f args =
   Proofview.Goal.enter begin fun gl ->
-    let sigma = Proofview.Goal.sigma gl in
-    let (sigma, c) = redfun (Proofview.Goal.env gl) sigma (Proofview.Goal.concl gl) in
-    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
-    (convert_concl_no_check c sty)
+    let fold (env, sigma) arg =
+      let (redfun, id, where) = f arg in
+      let hyp =
+        try lookup_named id env
+        with Not_found ->
+          raise (RefinerError (env, sigma, NoSuchHyp id))
+      in
+      let (sigma, d) = e_pf_change_decl redfun where hyp env sigma in
+      let sign = Logic.convert_hyp check (named_context_val env) sigma d in
+      let env = reset_with_named_context sign env in
+      (env, sigma)
+    in
+    let env = Proofview.Goal.env gl in
+    let sigma = Tacmach.New.project gl in
+    let (env, sigma) = List.fold_left fold (env, sigma) args in
+    let ty = Proofview.Goal.concl gl in
+    Proofview.Unsafe.tclEVARS sigma
+    <*>
+    Refine.refine ~typecheck:false begin fun sigma ->
+      Evarutil.new_evar env sigma ~principal:true ty
+    end
   end
 
-let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigma =
-  let open Context.Named.Declaration in
-  match decl with
-  | LocalAssum (id,ty) ->
-      if where == InHypValueOnly then
-        user_err  (Id.print id.binder_name ++ str " has no value.");
-    let (sigma, ty') = redfun false env sigma ty in
-    (sigma, LocalAssum (id, ty'))
-  | LocalDef (id,b,ty) ->
-      let (sigma, b') =
-	if where != InHypTypeOnly then redfun true env sigma b else (sigma, b)
-      in
-      let (sigma, ty') =
-	if where != InHypValueOnly then redfun false env sigma ty else (sigma, ty)
-      in
-      (sigma, LocalDef (id,b',ty'))
+let e_reduct_in_concl = e_change_in_concl
 
-let e_change_in_hyp redfun (id,where) =
-  Proofview.Goal.enter begin fun gl ->
-    let sigma = Proofview.Goal.sigma gl in
-    let hyp = Tacmach.New.pf_get_hyp id gl in
-    let (sigma, c) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in
-    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
-    (convert_hyp c)
-  end
+let reduct_in_concl ?(check = false) (redfun, sty) =
+  let redfun env sigma c = (sigma, redfun env sigma c) in
+  e_change_in_concl ~check (redfun, sty)
+
+let e_reduct_in_hyp ?(check=false) redfun (id, where) =
+  let redfun _ env sigma c = redfun env sigma c in
+  e_change_in_hyp ~check redfun (id, where)
+
+let reduct_in_hyp ?(check = false) redfun (id, where) =
+  let redfun _ env sigma c = (sigma, redfun env sigma c) in
+  e_change_in_hyp ~check redfun (id, where)
+
+let revert_cast (redfun,kind as r) =
+  if kind == DEFAULTcast then (redfun,REVERTcast) else r
+
+let e_reduct_option ?(check=false) redfun = function
+  | Some id -> e_reduct_in_hyp ~check (fst redfun) id
+  | None    -> e_change_in_concl ~check (revert_cast redfun)
+
+let reduct_option ?(check = false) (redfun, sty) where =
+  let redfun env sigma c = (sigma, redfun env sigma c) in
+  e_reduct_option ~check (redfun, sty) where
 
 type change_arg = Ltac_pretype.patvar_map -> env -> evar_map -> evar_map * EConstr.constr
 
@@ -837,24 +820,35 @@ let change_on_subterm cv_pb deep t where env sigma c =
   (sigma, c)
 
 let change_in_concl occl t =
-  e_change_in_concl ((change_on_subterm Reduction.CUMUL false t occl),DEFAULTcast)
+  e_change_in_concl ~check:false ((change_on_subterm Reduction.CUMUL false t occl),DEFAULTcast)
 
 let change_in_hyp occl t id  =
-  e_change_in_hyp (fun x -> change_on_subterm Reduction.CONV x t occl) id
-
-let change_option occl t = function
-  | Some id -> change_in_hyp occl t id
-  | None -> change_in_concl occl t
+  (* FIXME: we set the [check] flag only to reorder hypotheses in case of
+    introduction of dependencies in new variables. We should separate this
+    check from the conversion function. *)
+  e_change_in_hyp ~check:true (fun x -> change_on_subterm Reduction.CONV x t occl) id
+
+let concrete_clause_of enum_hyps cl = match cl.onhyps with
+| None ->
+  let f id = (id, AllOccurrences, InHyp) in
+  List.map f (enum_hyps ())
+| Some l ->
+  List.map (fun ((occs, id), w) -> (id, occs, w)) l
 
 let change chg c cls =
   Proofview.Goal.enter begin fun gl ->
-    let cls = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cls in
-    Tacticals.New.tclMAP (function
-    | OnHyp (id,occs,where) ->
-       change_option (bind_change_occurrences occs chg) c (Some (id,where))
-    | OnConcl occs ->
-       change_option (bind_change_occurrences occs chg) c None)
-    cls
+    let hyps = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cls in
+    begin match cls.concl_occs with
+    | NoOccurrences -> Proofview.tclUNIT ()
+    | occs -> change_in_concl (bind_change_occurrences occs chg) c
+    end
+    <*>
+    let f (id, occs, where) =
+      let occl = bind_change_occurrences occs chg in
+      let redfun deep env sigma t = change_on_subterm Reduction.CONV deep c occl env sigma t in
+      (redfun, id, where)
+    in
+    e_change_in_hyps ~check:true f hyps
   end
 
 let change_concl t = 
@@ -881,14 +875,6 @@ let pattern_option l = e_reduct_option (pattern_occs l,DEFAULTcast)
 
 (* The main reduction function *)
 
-let reduction_clause redexp cl =
-  let nbcl = List.length cl in
-  List.map (function
-    | OnHyp (id,occs,where) ->
-	(Some (id,where), bind_red_expr_occurrences occs nbcl redexp)
-    | OnConcl occs ->
-	(None, bind_red_expr_occurrences occs nbcl redexp)) cl
-
 let reduce redexp cl =
   let trace env sigma =
     let open Printer in
@@ -897,12 +883,24 @@ let reduce redexp cl =
   in
   Proofview.Trace.name_tactic trace begin
   Proofview.Goal.enter begin fun gl ->
-  let cl' = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in
-  let redexps = reduction_clause redexp cl' in
+  let hyps = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in
+  let nbcl = (if cl.concl_occs = NoOccurrences then 0 else 1) + List.length hyps in
   let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in
-  Tacticals.New.tclMAP (fun (where,redexp) ->
-    e_reduct_option ~check
-      (Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp) where) redexps
+  begin match cl.concl_occs with
+  | NoOccurrences -> Proofview.tclUNIT ()
+  | occs ->
+    let redexp = bind_red_expr_occurrences occs nbcl redexp in
+    let redfun = Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp in
+    e_change_in_concl ~check (revert_cast redfun)
+  end
+  <*>
+  let f (id, occs, where) =
+    let redexp = bind_red_expr_occurrences occs nbcl redexp in
+    let (redfun, _) = Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp in
+    let redfun _ env sigma c = redfun env sigma c in
+    (redfun, id, where)
+  in
+  e_change_in_hyps ~check f hyps
   end
   end
 
@@ -2174,7 +2172,7 @@ let constructor_tac with_evars expctdnumopt i lbind =
     let nconstr = Array.length (snd (Global.lookup_inductive ind)).mind_consnames in
     check_number_of_constructors expctdnumopt i nconstr;
     Tacticals.New.tclTHENLIST [
-      convert_concl_no_check redcl DEFAULTcast;
+      convert_concl ~check:false redcl DEFAULTcast;
       intros;
       constructor_core with_evars (ind, i) lbind
     ]
@@ -2203,7 +2201,7 @@ let any_constructor with_evars tacopt =
       Array.length (snd (Global.lookup_inductive ind)).mind_consnames in
     if Int.equal nconstr 0 then error "The type has no constructors.";
     Tacticals.New.tclTHENLIST [
-      convert_concl_no_check redcl DEFAULTcast;
+      convert_concl ~check:false redcl DEFAULTcast;
       intros;
       any_constr ind nconstr 1 ()
     ]
@@ -2647,9 +2645,9 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
     in
       Tacticals.New.tclTHENLIST
       [ Proofview.Unsafe.tclEVARS sigma;
-        convert_concl_no_check newcl DEFAULTcast;
+        convert_concl ~check:false newcl DEFAULTcast;
         intro_gen (NamingMustBe (CAst.make id)) (decode_hyp lastlhyp) true false;
-        Tacticals.New.tclMAP convert_hyp_no_check depdecls;
+        Tacticals.New.tclMAP (convert_hyp ~check:false) depdecls;
         eq_tac ]
   end
 
@@ -4799,7 +4797,7 @@ let symmetry_red allowred =
   match with_eqn with
   | Some eq_data,_,_ ->
       Tacticals.New.tclTHEN
-        (convert_concl_no_check concl DEFAULTcast)
+        (convert_concl ~check:false concl DEFAULTcast)
         (Tacticals.New.pf_constr_of_global eq_data.sym >>= apply)
   | None,eq,eq_kind -> prove_symmetry eq eq_kind
   end
@@ -4894,7 +4892,7 @@ let transitivity_red allowred t =
   match with_eqn with
   | Some eq_data,_,_ ->
       Tacticals.New.tclTHEN
-        (convert_concl_no_check concl DEFAULTcast)
+        (convert_concl ~check:false 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 75b5caaa36..e7b95a820e 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -36,7 +36,9 @@ val introduction    : Id.t -> unit Proofview.tactic
 val convert_concl   : ?check:bool -> types -> cast_kind -> unit Proofview.tactic
 val convert_hyp     : ?check:bool -> named_declaration -> unit Proofview.tactic
 val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic
+[@@ocaml.deprecated "use [Tactics.convert_concl]"]
 val convert_hyp_no_check : named_declaration -> unit Proofview.tactic
+[@@ocaml.deprecated "use [Tactics.convert_hyp]"]
 val mutual_fix      :
   Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic
 val fix             : Id.t -> int -> unit Proofview.tactic
@@ -152,8 +154,8 @@ type change_arg = patvar_map -> env -> evar_map -> evar_map * constr
 val make_change_arg   : constr -> change_arg
 val reduct_in_hyp     : ?check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic
 val reduct_option     : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> unit Proofview.tactic
-val reduct_in_concl   : tactic_reduction * cast_kind -> unit Proofview.tactic
-val e_reduct_in_concl   : check:bool -> e_tactic_reduction * cast_kind -> unit Proofview.tactic
+val reduct_in_concl   : ?check:bool -> tactic_reduction * cast_kind -> unit Proofview.tactic
+val e_reduct_in_concl   : ?check:bool -> e_tactic_reduction * cast_kind -> unit Proofview.tactic
 val change_in_concl   : (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic
 val change_concl      : constr -> unit Proofview.tactic
 val change_in_hyp     : (occurrences * constr_pattern) option -> change_arg ->