Isolating a function "make_abstraction", new name of "letin_abstract",

which compute an abstraction of the goal over a term or a pattern.

4 files changed, 63 insertions, 65 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 8a2b13ebee..d4e42142bb 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -75,7 +75,8 @@
       check_evars_are_solved explicitly to check that evars are solved.
   See also the corresponding commit log.
 
-- Tactics API: new_induct -> induction; new_destruct -> destruct
+- Tactics API: new_induct -> induction; new_destruct -> destruct;
+  letin_pat_tac do not accept a type anymore
 
 =========================================
 = CHANGES BETWEEN COQ V8.3 AND COQ V8.4 =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index b60c1d41be..0d2b3d5a1f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1599,7 +1599,7 @@ and interp_atomic ist tac =
           let let_pat_tac b na c cl eqpat =
             let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in
             let with_eq = if b then None else Some (true,id) in
-            Tactics.letin_pat_tac with_eq na c None cl
+            Tactics.letin_pat_tac with_eq na c cl
           in
           let_pat_tac b (interp_fresh_name ist env na)
             (interp_pure_open_constr ist env sigma c) clp eqpat
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c3331a372a..da33ecfd88 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1691,26 +1691,6 @@ let apply_in simple with_evars id lemmas ipat =
 (* Tactics abstracting terms *)
 (*****************************)
 
-(* [letin_tac b na c (occ_hyp,occ_ccl) gl] transforms
-   [...x1:T1(c),...,x2:T2(c),... |- G(c)] into
-   [...x:T;Heqx:(x=c);x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is false or
-   [...x:=c:T;x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is true
-
-   [occ_hyp,occ_ccl] tells which occurrences of [c] have to be substituted;
-   if [occ_hyp = []] and [occ_ccl = None] then [c] is substituted
-   wherever it occurs, otherwise [c] is substituted only in hyps
-   present in [occ_hyps] at the specified occurrences (everywhere if
-   the list of occurrences is empty), and in the goal at the specified
-   occurrences if [occ_goal] is not [None];
-
-   if name = Anonymous, the name is build from the first letter of the type;
-
-   The tactic first quantify the goal over x1, x2,... then substitute then
-   re-intro x1, x2,... at their initial place ([marks] is internally
-   used to remember the place of x1, x2, ...: it is the list of hypotheses on
-   the left of each x1, ...).
-*)
-
 let out_arg = function
   | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable")
   | ArgArg x -> x
@@ -1782,8 +1762,23 @@ let make_pattern_test env sigma0 (sigma,c) =
        Proofview.V82.tclEVARUNIVCONTEXT (Evd.evar_universe_context univs),
        subst_univs_constr subst (nf_evar sigma c))
 
-let letin_abstract id c (test,out) (occs,check_occs) gl =
-  let env = pf_env gl in
+let make_eq_test evd c =
+  let out cstr = 
+    let tac = Proofview.V82.tclEVARUNIVCONTEXT (Evd.evar_universe_context cstr.testing_state) in
+      tac, c
+  in
+    (Tacred.make_eq_univs_test evd c, out)
+
+let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs gl =
+  let env = Proofview.Goal.env gl in
+  let id =
+    let t = match ty with Some t -> t | None -> typ_of env sigmac c in
+    let x = id_of_name_using_hdchar (Global.env()) t name in
+    if name == Anonymous then Tacmach.New.of_old (fresh_id [] x) gl else
+      let hyps = Proofview.Goal.hyps gl in
+      if not (mem_named_context x hyps) then x else
+	error ("The variable "^(Id.to_string x)^" is already declared.")
+  in
   let compute_dependency _ (hyp,_,_ as d) depdecls =
     match occurrences_of_hyp hyp occs with
       | None -> depdecls
@@ -1799,31 +1794,50 @@ let letin_abstract id c (test,out) (occs,check_occs) gl =
           let newdecl = subst_closed_term_occ_decl_modulo occ test d in
 	    (subst1_named_decl (mkVar id) newdecl)::depdecls in
   let depdecls = fold_named_context compute_dependency env ~init:[] in
+  let concl = Proofview.Goal.concl gl in
   let ccl = match occurrences_of_goal occs with
-    | None -> pf_concl gl
+    | None -> concl
     | Some occ ->
-        subst1 (mkVar id) (subst_closed_term_occ_modulo occ test None (pf_concl gl)) in
+        subst1 (mkVar id) (subst_closed_term_occ_modulo occ test None concl) in
   let lastlhyp =
     if List.is_empty depdecls then MoveLast else MoveAfter(pi1(List.last depdecls)) in
-  (depdecls,lastlhyp,ccl,out test)
+  (id,depdecls,lastlhyp,ccl,out test)
+
+(** [make_abstraction] is the main entry point to abstract over a term
+    or pattern at some occurrences; it returns:
+    - the id used for the abstraction
+    - the type of the abstraction
+    - the hypotheses from the context which depend on the term or pattern
+    - the most recent hyp before which there is no dependency in the term of pattern
+    - the abstracted conclusion
+    - a tactic to apply to take evars effects into account
+    - the term or pattern to abstract fully instantiated
+*)
+
+type abstraction_request =
+| AbstractPattern of Name.t * (evar_map * constr) * clause * bool
+| AbstractExact of Name.t * constr * types option * clause * bool
+
+let make_abstraction abs gl =
+  let evd = Proofview.Goal.sigma gl in
+  let env = Proofview.Goal.env gl in
+  match abs with
+  | AbstractPattern (name,c,occs,check_occs) ->
+      make_abstraction_core name (make_pattern_test env evd c) c None occs check_occs gl
+  | AbstractExact (name,c,ty,occs,check_occs) ->
+      make_abstraction_core name (make_eq_test evd c) (evd,c) ty occs check_occs gl
 
-let letin_tac_gen with_eq name (sigmac,c) test ty occs =
+(* [letin_tac b (... abstract over c ...) gl] transforms
+   [...x1:T1(c),...,x2:T2(c),... |- G(c)] into
+   [...x:T;Heqx:(x=c);x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is false or
+   [...x:=c:T;x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is true
+*)
+
+let letin_tac_gen with_eq abs ty =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
-    let hyps = Proofview.Goal.hyps gl in
-    let id =
-      let t = match ty with Some t -> t | None -> typ_of env sigmac c in
-      let x = id_of_name_using_hdchar (Global.env()) t name in
-      if name == Anonymous then Tacmach.New.of_old (fresh_id [] x) gl else
-          if not (mem_named_context x hyps) then x else
-	    error ("The variable "^(Id.to_string x)^" is already declared.")
-    in
-    let (depdecls,lastlhyp,ccl,(tac,c)) =
-      Tacmach.New.of_old (letin_abstract id c test occs) gl
-    in
-    let t =
-      match ty with Some t -> t | None -> Tacmach.New.pf_apply (fun e s -> typ_of e s c) gl
-    in
+    let (id,depdecls,lastlhyp,ccl,(tac,c)) = make_abstraction abs gl in
+    let t = match ty with Some t -> t | _ -> typ_of env (Proofview.Goal.sigma gl) c in
     let (sigma,newcl,eq_tac) = match with_eq with
       | Some (lr,(loc,ido)) ->
           let heq = match ido with
@@ -1851,25 +1865,11 @@ let letin_tac_gen with_eq name (sigmac,c) test ty occs =
         eq_tac ]
   end
 
-let make_eq_test evd c =
-  let out cstr = 
-    let tac = Proofview.V82.tclEVARUNIVCONTEXT (Evd.evar_universe_context cstr.testing_state) in
-      tac, c
-  in
-    (Tacred.make_eq_univs_test evd c, out)
-
 let letin_tac with_eq name c ty occs =
-  Proofview.tclEVARMAP >>= fun sigma ->
-  letin_tac_gen with_eq name (sigma,c) (make_eq_test sigma c) ty (occs,true)
+  letin_tac_gen with_eq (AbstractExact (name,c,ty,occs,true)) ty
 
-let letin_pat_tac with_eq name c ty occs =
-  Proofview.Goal.raw_enter begin fun gl ->
-    let sigma = Proofview.Goal.sigma gl in
-    let env = Proofview.Goal.env gl in
-  letin_tac_gen with_eq name c
-    (make_pattern_test env sigma c)
-    ty (occs,true)
-  end
+let letin_pat_tac with_eq name c occs =
+  letin_tac_gen with_eq (AbstractPattern (name,c,occs,false)) None
 
 (* Tactics "pose proof" (usetac=None) and "assert" (otherwise) *)
 let forward usetac ipat c =
@@ -3380,7 +3380,6 @@ let induction_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
 	    isrec with_evars elim names (id,lbind) inhyps)
     | _        ->
         Proofview.Goal.raw_enter begin fun gl ->
-          let defs = Proofview.Goal.sigma gl in
           let env = Proofview.Goal.env gl in
 	  let x = id_of_name_using_hdchar (Global.env()) (typ_of env sigma c)
 	        Anonymous in
@@ -3389,12 +3388,10 @@ let induction_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
 	  let with_eq = Option.map (fun eq -> (false,eq)) eqname in
 	(* TODO: if ind has predicate parameters, use JMeq instead of eq *)
           Proofview.Goal.raw_enter begin fun gl ->
-            let env = Proofview.Goal.env gl in
 	    Tacticals.New.tclTHEN
             (* Warning: letin is buggy when c is not of inductive type *)
-	      (letin_tac_gen with_eq (Name id) (sigma,c)
-                 (make_pattern_test env defs (sigma,c))
-                 None (Option.default allHypsAndConcl cls,false))
+	      (letin_tac_gen with_eq
+                 (AbstractPattern (Name id,(sigma,c),(Option.default allHypsAndConcl cls),false)) None)
 	      (induction_with_atomization_of_ind_arg
 	         isrec with_evars elim names (id,lbind) inhyps)
           end
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 0ee307c232..b1d69a2a91 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -346,7 +346,7 @@ val forward   : unit Proofview.tactic option -> intro_pattern_expr located optio
 val letin_tac : (bool * intro_pattern_expr located) option -> Name.t ->
   constr -> types option -> clause -> unit Proofview.tactic
 val letin_pat_tac : (bool * intro_pattern_expr located) option -> Name.t ->
-  evar_map * constr -> types option -> clause -> unit Proofview.tactic
+  evar_map * constr -> clause -> unit Proofview.tactic
 val assert_tac : Name.t -> types -> unit Proofview.tactic
 val assert_by  : Name.t -> types -> unit Proofview.tactic -> unit Proofview.tactic
 val pose_proof : Name.t -> constr -> unit Proofview.tactic