Made the subterm finding function make_abstraction independent of the

proof engine. Moved it to unification.ml.

1 files changed, 24 insertions, 156 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8dfd1b14bf..450b48d455 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -86,18 +86,6 @@ let _ =
       optread  = (fun () -> !Flags.tactic_context_compat) ;
       optwrite = (fun b -> Flags.tactic_context_compat := b) }
 
-let tactic_infer_flags = {
-  Pretyping.use_typeclasses = true;
-  Pretyping.use_unif_heuristics = true;
-  Pretyping.use_hook = Some solve_by_implicit_tactic;
-  Pretyping.fail_evar = true;
-  Pretyping.expand_evars = true }
-
-let finish_evar_resolution env initial_sigma (sigma,c) =
-  let sigma =
-    Pretyping.solve_remaining_evars tactic_infer_flags env initial_sigma sigma
-  in Evd.evar_universe_context sigma, nf_evar sigma c
-
 (*********************************************)
 (*                 Tactics                   *)
 (*********************************************)
@@ -1740,141 +1728,19 @@ let apply_in simple with_evars id lemmas ipat =
 (* Tactics abstracting terms *)
 (*****************************)
 
-let out_arg = function
-  | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable")
-  | ArgArg x -> x
-
-let occurrences_of_hyp id cls =
-  let rec hyp_occ = function
-      [] -> None
-    | ((occs,id'),hl)::_ when Id.equal id id' ->
-        Some (occurrences_map (List.map out_arg) occs, hl)
-    | _::l -> hyp_occ l in
-  match cls.onhyps with
-      None -> Some (AllOccurrences,InHyp)
-    | Some l -> hyp_occ l
-
-let occurrences_of_goal cls =
-  if cls.concl_occs == NoOccurrences then None
-  else Some (occurrences_map (List.map out_arg) cls.concl_occs)
-
-let in_every_hyp cls = Option.is_empty cls.onhyps
-
 (* Implementation without generalisation: abbrev will be lost in hyps in *)
 (* in the extracted proof *)
 
-let default_matching_flags sigma = {
-  modulo_conv_on_closed_terms = Some empty_transparent_state;
-  use_metas_eagerly_in_conv_on_closed_terms = false;
-  modulo_delta = empty_transparent_state;
-  modulo_delta_types = full_transparent_state;
-  modulo_delta_in_merge = Some full_transparent_state;
-  check_applied_meta_types = true;
-  resolve_evars = false;
-  use_pattern_unification = false;
-  use_meta_bound_pattern_unification = false;
-  frozen_evars =
-    fold_undefined (fun evk _ evars -> Evar.Set.add evk evars)
-      sigma Evar.Set.empty;
-  restrict_conv_on_strict_subterms = false;
-  modulo_betaiota = false;
-  modulo_eta = false;
-  allow_K_in_toplevel_higher_order_unification = false
-}
-
-(* This supports search of occurrences of term from a pattern *)
-
-let make_pattern_test env sigma0 (sigma,c) =
-  let flags = default_matching_flags sigma0 in
-  let matching_fun _ t =
-    try let sigma = w_unify env sigma Reduction.CONV ~flags c t in
-	  Some(sigma, t)
-    with e when Errors.noncritical e -> raise NotUnifiable in
-  let merge_fun c1 c2 =
-    match c1, c2 with
-    | Some (evd,c1), Some (_,c2) ->
-      (try let evd = w_unify env evd Reduction.CONV ~flags c1 c2 in
-	     Some (evd, c1)
-       with e when Errors.noncritical e -> raise NotUnifiable)
-    | Some _, None -> c1
-    | None, Some _ -> c2
-    | None, None -> None
-  in
-  { match_fun = matching_fun; merge_fun = merge_fun;
-    testing_state = None; last_found = None },
-  (fun test -> match test.testing_state with
-  | None ->
-    let ctx, c = finish_evar_resolution env sigma0 (sigma,c) in
-      Proofview.V82.tclEVARUNIVCONTEXT ctx, c
-  | Some (sigma,_) ->
-     let univs, subst = nf_univ_variables sigma in
-       Proofview.V82.tclEVARUNIVCONTEXT (Evd.evar_universe_context univs),
-       subst_univs_constr subst (nf_evar sigma c))
-
-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
-      | Some ((AllOccurrences, InHyp) as occ) ->
-          let newdecl = subst_closed_term_occ_decl_modulo occ test d in
-          if eq_named_declaration d newdecl then
-            if check_occs && not (in_every_hyp occs)
-            then raise (RefinerError (DoesNotOccurIn (c,hyp)))
-            else depdecls
-          else
-            (subst1_named_decl (mkVar id) newdecl)::depdecls
-      | Some occ ->
-          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 -> concl
-    | Some occ ->
-        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
-  (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 tactic_infer_flags = {
+  Pretyping.use_typeclasses = true;
+  Pretyping.use_unif_heuristics = true;
+  Pretyping.use_hook = Some solve_by_implicit_tactic;
+  Pretyping.fail_evar = true;
+  Pretyping.expand_evars = true }
 
-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 decode_hyp = function
+  | None -> MoveLast
+  | Some id -> MoveAfter id
 
 (* [letin_tac b (... abstract over c ...) gl] transforms
    [...x1:T1(c),...,x2:T2(c),... |- G(c)] into
@@ -1885,7 +1751,9 @@ let make_abstraction abs gl =
 let letin_tac_gen with_eq abs ty =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
-    let (id,depdecls,lastlhyp,ccl,(tac,c)) = make_abstraction abs gl in
+    let evd = Proofview.Goal.sigma gl in
+    let ccl = Proofview.Goal.concl gl in
+    let (id,depdecls,lastlhyp,ccl,(ctx,c)) = make_abstraction env evd ccl abs in
     let t = match ty with Some t -> t | _ -> typ_of env (Proofview.Goal.sigma gl) c in
     let eq_tac gl = match with_eq with
       | Some (lr,(loc,ido)) ->
@@ -1904,26 +1772,26 @@ let letin_tac_gen with_eq abs ty =
 	  let sigma, _ = Typing.e_type_of env sigma term in
             sigma, term,
             Tacticals.New.tclTHEN
-	      (intro_gen loc (IntroMustBe heq) lastlhyp true false)
+	      (intro_gen loc (IntroMustBe heq) (decode_hyp lastlhyp) true false)
 	      (Proofview.V82.tactic (thin_body [heq;id]))
       | None ->
 	  (Proofview.Goal.sigma gl, mkNamedLetIn id c t ccl, Proofview.tclUNIT ()) in
-    Proofview.tclBIND tac (fun () ->
-      Proofview.Goal.enter (fun gl -> 
-	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);
-              intro_gen dloc (IntroMustBe id) lastlhyp true false;
-              Proofview.V82.tactic (tclMAP convert_hyp_no_check depdecls);
-              eq_tac ]))
+    Proofview.Goal.enter (fun gl -> 
+      let (sigma,newcl,eq_tac) = eq_tac gl in
+      Tacticals.New.tclTHENLIST
+	[ Proofview.V82.tclEVARS sigma;
+          Proofview.V82.tclEVARUNIVCONTEXT ctx;
+	  Proofview.V82.tactic (convert_concl_no_check newcl DEFAULTcast);
+          intro_gen dloc (IntroMustBe id) (decode_hyp lastlhyp) true false;
+          Proofview.V82.tactic (tclMAP convert_hyp_no_check depdecls);
+          eq_tac ])
   end
 
 let letin_tac with_eq name c ty occs =
   letin_tac_gen with_eq (AbstractExact (name,c,ty,occs,true)) ty
 
 let letin_pat_tac with_eq name c occs =
-  letin_tac_gen with_eq (AbstractPattern (name,c,occs,false)) None
+  letin_tac_gen with_eq (AbstractPattern (name,c,occs,false,tactic_infer_flags)) None
 
 (* Tactics "pose proof" (usetac=None) and "assert" (otherwise) *)
 let forward usetac ipat c =
@@ -3437,7 +3305,7 @@ let induction_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
 	    Tacticals.New.tclTHEN
             (* Warning: letin is buggy when c is not of inductive type *)
 	      (letin_tac_gen with_eq
-                 (AbstractPattern (Name id,(sigma,c),(Option.default allHypsAndConcl cls),false)) None)
+                 (AbstractPattern (Name id,(sigma,c),(Option.default allHypsAndConcl cls),false,tactic_infer_flags)) None)
 	      (induction_with_atomization_of_ind_arg
 	         isrec with_evars elim names (id,lbind) inhyps)
           end