From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- tactics/class_tactics.ml | 67 +++++++++++++++++++++++++----------------------- 1 file changed, 35 insertions(+), 32 deletions(-) (limited to 'tactics/class_tactics.ml') diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index e11458c0..f3a48634 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -141,6 +141,7 @@ let progress_evars t = let e_give_exact flags poly (c,clenv) gl = + let (c, _, _) = c in let c, gl = if poly then let clenv', subst = Clenv.refresh_undefined_univs clenv in @@ -149,36 +150,35 @@ let e_give_exact flags poly (c,clenv) gl = c, {gl with sigma = clenv'.evd} else c, gl in - let t1 = pf_type_of gl c in + let t1 = pf_unsafe_type_of gl c in tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl let unify_e_resolve poly flags (c,clenv) gls = - let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in - let clenv' = connect_clenv gls clenv' in - let clenv' = clenv_unique_resolver ~flags clenv' gls in - Proofview.V82.of_tactic (Clenvtac.clenv_refine true ~with_classes:false clenv') gls + let clenv', c = connect_hint_clenv poly c clenv gls in + let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in + Clenvtac.clenv_refine true ~with_classes:false clenv' let unify_resolve poly flags (c,clenv) gls = - let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in - let clenv' = connect_clenv gls clenv' in - let clenv' = clenv_unique_resolver ~flags clenv' gls in - Proofview.V82.of_tactic - (Clenvtac.clenv_refine false ~with_classes:false clenv') gls + let clenv', _ = connect_hint_clenv poly c clenv gls in + let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in + Clenvtac.clenv_refine false ~with_classes:false clenv' -let clenv_of_prods poly nprods (c, clenv) gls = +let clenv_of_prods poly nprods (c, clenv) gl = + let (c, _, _) = c in if poly || Int.equal nprods 0 then Some clenv else - let ty = pf_type_of gls c in + let ty = Tacmach.New.pf_unsafe_type_of gl c in let diff = nb_prod ty - nprods in if Pervasives.(>=) diff 0 then (* Was Some clenv... *) - Some (mk_clenv_from_n gls (Some diff) (c,ty)) + Some (Tacmach.New.of_old (fun gls -> mk_clenv_from_n gls (Some diff) (c,ty)) gl) else None -let with_prods nprods poly (c, clenv) f gls = - match clenv_of_prods poly nprods (c, clenv) gls with - | None -> tclFAIL 0 (str"Not enough premisses") gls - | Some clenv' -> f (c, clenv') gls +let with_prods nprods poly (c, clenv) f = + Proofview.Goal.nf_enter (fun gl -> + match clenv_of_prods poly nprods (c, clenv) gl with + | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses") + | Some clenv' -> f (c, clenv') gl) (** Hack to properly solve dependent evars that are typeclasses *) @@ -190,7 +190,7 @@ let rec e_trivial_fail_db db_list local_db goal = let d = pf_last_hyp g' in let hintl = make_resolve_hyp (pf_env g') (project g') d in (e_trivial_fail_db db_list - (Hint_db.add_list hintl local_db) g'))) :: + (Hint_db.add_list (pf_env g') (project g') hintl local_db) g'))) :: (List.map (fun (x,_,_,_,_) -> x) (e_trivial_resolve db_list local_db (project goal) (pf_concl goal))) in @@ -205,7 +205,7 @@ and e_my_find_search db_list local_db hdc complete sigma concl = if cl.cl_strict then Evd.evars_of_term concl else Evar.Set.empty - with _ -> Evar.Set.empty + with e when Errors.noncritical e -> Evar.Set.empty in let hintl = List.map_append @@ -222,22 +222,23 @@ and e_my_find_search db_list local_db hdc complete sigma concl = let tac_of_hint = fun (flags, {pri = b; pat = p; poly = poly; code = t; name = name}) -> let tac = function - | Res_pf (term,cl) -> Proofview.V82.tactic (with_prods nprods poly (term,cl) (unify_resolve poly flags)) - | ERes_pf (term,cl) -> Proofview.V82.tactic (with_prods nprods poly (term,cl) (unify_e_resolve poly flags)) + | Res_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_resolve poly flags) + | ERes_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_e_resolve poly flags) | Give_exact c -> Proofview.V82.tactic (e_give_exact flags poly c) | Res_pf_THEN_trivial_fail (term,cl) -> - Proofview.V82.tactic (tclTHEN (with_prods nprods poly (term,cl) (unify_e_resolve poly flags)) - (if complete then tclIDTAC else e_trivial_fail_db db_list local_db)) + Proofview.V82.tactic (tclTHEN + (Proofview.V82.of_tactic ((with_prods nprods poly (term,cl) (unify_e_resolve poly flags)))) + (if complete then tclIDTAC else e_trivial_fail_db db_list local_db)) | Unfold_nth c -> Proofview.V82.tactic (tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c])) | Extern tacast -> conclPattern concl p tacast in - let tac = Proofview.V82.of_tactic (run_auto_tactic t tac) in + let tac = Proofview.V82.of_tactic (run_hint t tac) in let tac = if complete then tclCOMPLETE tac else tac in - match repr_auto_tactic t with - | Extern _ -> (tac,b,true, name, lazy (pr_autotactic t)) + match repr_hint t with + | Extern _ -> (tac,b,true, name, lazy (pr_hint t)) | _ -> (* let tac gl = with_pattern (pf_env gl) (project gl) flags p concl tac gl in *) - (tac,b,false, name, lazy (pr_autotactic t)) + (tac,b,false, name, lazy (pr_hint t)) in List.map tac_of_hint hintl and e_trivial_resolve db_list local_db sigma concl = @@ -339,7 +340,7 @@ let make_hints g st only_classes sign = (PathOr (paths, path), hint @ hints) else (paths, hints)) (PathEmpty, []) sign - in Hint_db.add_list hintlist (Hint_db.empty st true) + in Hint_db.add_list (pf_env g) (project g) hintlist (Hint_db.empty st true) let make_autogoal_hints = let cache = ref (true, Environ.empty_named_context_val, @@ -374,7 +375,7 @@ let intro_tac : atac = let context = Environ.named_context_of_val (Goal.V82.hyps s g') in let hint = make_resolve_hyp env s (Hint_db.transparent_state info.hints) (true,false,false) info.only_classes None (List.hd context) in - let ldb = Hint_db.add_list hint info.hints in + let ldb = Hint_db.add_list env s hint info.hints in (g', { info with is_evar = None; hints = ldb; auto_last_tac = lazy (str"intro") })) gls in {it = gls'; sigma = s;}) @@ -397,7 +398,7 @@ let is_unique env concl = try let (cl,u), args = dest_class_app env concl in cl.cl_unique - with _ -> false + with e when Errors.noncritical e -> false let needs_backtrack env evd oev concl = if Option.is_empty oev || is_Prop env evd concl then @@ -490,6 +491,7 @@ let hints_tac hints = let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk = let rec aux s (acc : autogoal list list) fk = function | (gl,info) :: gls -> + Control.check_for_interrupt (); (match info.is_evar with | Some ev when Evd.is_defined s ev -> aux s acc fk gls | _ -> @@ -842,6 +844,7 @@ let is_ground c gl = let autoapply c i gl = let flags = auto_unif_flags Evar.Set.empty (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in - let cty = pf_type_of gl c in + let cty = pf_unsafe_type_of gl c in let ce = mk_clenv_from gl (c,cty) in - unify_e_resolve false flags (c,ce) gl + let tac = unify_e_resolve false flags ((c,cty,Univ.ContextSet.empty),ce) in + Proofview.V82.of_tactic (Proofview.Goal.nf_enter tac) gl -- cgit v1.2.3