From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- tactics/auto.ml | 207 +++++++++++++++++++++++++++++--------------------------- 1 file changed, 107 insertions(+), 100 deletions(-) (limited to 'tactics/auto.ml') diff --git a/tactics/auto.ml b/tactics/auto.ml index 2d92387c..bc644857 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -10,7 +10,7 @@ *) open Pp open Util -open Errors +open CErrors open Names open Vars open Termops @@ -35,6 +35,10 @@ open Hints let priority l = List.filter (fun (_, hint) -> Int.equal hint.pri 0) l +let compute_secvars gl = + let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + secvars_of_hyps hyps + (* tell auto not to reuse already instantiated metas in unification (for compatibility, since otherwise, apply succeeds oftener) *) @@ -67,16 +71,13 @@ let auto_unif_flags_of st1 st2 useeager = let auto_unif_flags = auto_unif_flags_of full_transparent_state empty_transparent_state false -let auto_flags_of_state st = - auto_unif_flags_of full_transparent_state st false - (* Try unification with the precompiled clause, then use registered Apply *) let connect_hint_clenv poly (c, _, ctx) clenv gl = (** [clenv] has been generated by a hint-making function, so the only relevant data in its evarmap is the set of metas. The [evar_reset_evd] function below just replaces the metas of sigma by those coming from the clenv. *) - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in (** Still, we need to update the universes *) let clenv, c = @@ -85,22 +86,25 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl = let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in let map c = Vars.subst_univs_level_constr subst c in let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in - let clenv = { clenv with evd = evd ; env = Proofview.Goal.env gl } in - (** FIXME: We're being inefficient here because we substitute the whole - evar map instead of just its metas, which are the only ones - mentioning the old universes. *) - Clenv.map_clenv map clenv, map c + (** Only metas are mentioning the old universes. *) + let clenv = { + templval = Evd.map_fl map clenv.templval; + templtyp = Evd.map_fl map clenv.templtyp; + evd = Evd.map_metas map evd; + env = Proofview.Goal.env gl; + } in + clenv, map c else let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in { clenv with evd = evd ; env = Proofview.Goal.env gl }, c in clenv, c - + let unify_resolve poly flags ((c : raw_hint), clenv) = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let clenv, c = connect_hint_clenv poly c clenv gl in let clenv = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags clenv gl) gl in Clenvtac.clenv_refine false clenv - end + end } let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h @@ -109,20 +113,12 @@ let unify_resolve_gen poly = function | Some flags -> unify_resolve poly flags let exact poly (c,clenv) = - let (c, _, _) = c in - let ctx, c' = - if poly then - let evd', subst = Evd.refresh_undefined_universes clenv.evd in - let ctx = Evd.evar_universe_context evd' in - ctx, subst_univs_level_constr subst c - else - let ctx = Evd.evar_universe_context clenv.evd in - ctx, c - in - Proofview.Goal.enter begin fun gl -> - let sigma = Evd.merge_universe_context (Proofview.Goal.sigma gl) ctx in - Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (exact_check c') - end + Proofview.Goal.enter { enter = begin fun gl -> + let clenv', c = connect_hint_clenv poly c clenv gl in + Tacticals.New.tclTHEN + (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) + (exact_check c) + end } (* Util *) @@ -138,8 +134,6 @@ si après Intros la conclusion matche le pattern. (* conclPattern doit échouer avec error car il est rattraper par tclFIRST *) -let (forward_interp_tactic, extern_interp) = Hook.make () - let conclPattern concl pat tac = let constr_bindings env sigma = match pat with @@ -150,11 +144,23 @@ let conclPattern concl pat tac = with Constr_matching.PatternMatchingFailure -> Tacticals.New.tclZEROMSG (str "conclPattern") in - Proofview.Goal.enter (fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in constr_bindings env sigma >>= fun constr_bindings -> - Hook.get forward_interp_tactic constr_bindings tac) + let open Genarg in + let open Geninterp in + let inj c = match val_tag (topwit Constrarg.wit_constr) with + | Val.Base tag -> Val.Dyn (tag, c) + | _ -> assert false + in + let fold id c accu = Id.Map.add id (inj c) accu in + let lfun = Id.Map.fold fold constr_bindings Id.Map.empty in + let ist = { lfun; extra = TacStore.empty } in + match tac with + | GenArg (Glbwit wit, tac) -> + Ftactic.run (Geninterp.interp wit ist tac) (fun _ -> Proofview.tclUNIT ()) + end } (***********************************************************) (** A debugging / verbosity framework for trivial and auto *) @@ -217,11 +223,11 @@ let tclLOG (dbg,depth,trace) pp tac = Proofview.V82.tactic begin fun gl -> try let out = Proofview.V82.of_tactic tac gl in - msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)"); + Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)"); out with reraise -> - let reraise = Errors.push reraise in - msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)"); + let reraise = CErrors.push reraise in + Feedback.msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)"); iraise reraise end | Info -> @@ -232,7 +238,7 @@ let tclLOG (dbg,depth,trace) pp tac = trace := (depth, Some pp) :: !trace; out with reraise -> - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in trace := (depth, None) :: !trace; iraise reraise end @@ -258,31 +264,25 @@ let pr_info_atom (d,pp) = let pr_info_trace = function | (Info,_,{contents=(d,Some pp)::l}) -> - prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l) - | _ -> mt () + Feedback.msg_info (prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l)) + | _ -> () let pr_info_nop = function - | (Info,_,_) -> str "idtac." - | _ -> mt () + | (Info,_,_) -> Feedback.msg_info (str "idtac.") + | _ -> () let pr_dbg_header = function - | (Off,_,_) -> mt () - | (Debug,0,_) -> str "(* debug trivial : *)" - | (Debug,_,_) -> str "(* debug auto : *)" - | (Info,0,_) -> str "(* info trivial : *)" - | (Info,_,_) -> str "(* info auto : *)" + | (Off,_,_) -> () + | (Debug,0,_) -> Feedback.msg_debug (str "(* debug trivial: *)") + | (Debug,_,_) -> Feedback.msg_debug (str "(* debug auto: *)") + | (Info,0,_) -> Feedback.msg_info (str "(* info trivial: *)") + | (Info,_,_) -> Feedback.msg_info (str "(* info auto: *)") let tclTRY_dbg d tac = - let (level, _, _) = d in let delay f = Proofview.tclUNIT () >>= fun () -> f () in - let tac = match level with - | Off -> tac - | Debug | Info -> delay (fun () -> msg_debug (pr_dbg_header d ++ fnl () ++ pr_info_trace d); tac) - in - let after = match level with - | Info -> delay (fun () -> msg_debug (pr_info_nop d); Proofview.tclUNIT ()) - | Off | Debug -> Proofview.tclUNIT () - in + let tac = delay (fun () -> pr_dbg_header d; tac) >>= + fun () -> pr_info_trace d; Proofview.tclUNIT () in + let after = delay (fun () -> pr_info_nop d; Proofview.tclUNIT ()) in Tacticals.New.tclORELSE0 tac after (**************************************************************************) @@ -293,21 +293,19 @@ let tclTRY_dbg d tac = (* Papageno : cette fonction a été pas mal simplifiée depuis que la base de Hint impérative a été remplacée par plusieurs bases fonctionnelles *) -let auto_unif_flags = - auto_unif_flags_of full_transparent_state empty_transparent_state false - let flags_of_state st = auto_unif_flags_of st st false let auto_flags_of_state st = auto_unif_flags_of full_transparent_state st false -let hintmap_of hdc concl = +let hintmap_of secvars hdc concl = match hdc with - | None -> Hint_db.map_none + | None -> Hint_db.map_none ~secvars | Some hdc -> - if occur_existential concl then Hint_db.map_existential hdc concl - else Hint_db.map_auto hdc concl + if occur_existential concl then + Hint_db.map_existential ~secvars hdc concl + else Hint_db.map_auto ~secvars hdc concl let exists_evaluable_reference env = function | EvalConstRef _ -> true @@ -319,35 +317,36 @@ let dbg_assumption dbg = tclLOG dbg (fun () -> str "assumption") assumption let rec trivial_fail_db dbg mod_delta db_list local_db = let intro_tac = Tacticals.New.tclTHEN (dbg_intro dbg) - ( Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in + ( Proofview.Goal.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let nf c = Evarutil.nf_evar sigma c in let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in - let hyp = Context.map_named_declaration nf decl in + let hyp = Context.Named.Declaration.map_constr nf decl in let hintl = make_resolve_hyp env sigma hyp in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list env sigma hintl local_db) - end) + end }) in - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let concl = Tacmach.New.pf_nf_concl gl in + let secvars = compute_secvars gl in Tacticals.New.tclFIRST ((dbg_assumption dbg)::intro_tac:: (List.map Tacticals.New.tclCOMPLETE - (trivial_resolve dbg mod_delta db_list local_db concl))) - end + (trivial_resolve dbg mod_delta db_list local_db secvars concl))) + end } -and my_find_search_nodelta db_list local_db hdc concl = +and my_find_search_nodelta db_list local_db secvars hdc concl = List.map (fun hint -> (None,hint)) - (List.map_append (hintmap_of hdc concl) (local_db::db_list)) + (List.map_append (hintmap_of secvars hdc concl) (local_db::db_list)) and my_find_search mod_delta = if mod_delta then my_find_search_delta else my_find_search_nodelta -and my_find_search_delta db_list local_db hdc concl = - let f = hintmap_of hdc concl in +and my_find_search_delta db_list local_db secvars hdc concl = + let f = hintmap_of secvars hdc concl in if occur_existential concl then List.map_append (fun db -> @@ -367,16 +366,16 @@ and my_find_search_delta db_list local_db hdc concl = let (ids, csts as st) = Hint_db.transparent_state db in let flags, l = let l = - match hdc with None -> Hint_db.map_none db + match hdc with None -> Hint_db.map_none ~secvars db | Some hdc -> if (Id.Pred.is_empty ids && Cpred.is_empty csts) - then Hint_db.map_auto hdc concl db - else Hint_db.map_existential hdc concl db + then Hint_db.map_auto ~secvars hdc concl db + else Hint_db.map_existential ~secvars hdc concl db in auto_flags_of_state st, l in List.map (fun x -> (Some flags,x)) l) (local_db::db_list) -and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly})) = +and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) = let tactic = function | Res_pf (c,cl) -> unify_resolve_gen poly flags (c,cl) | ERes_pf _ -> Proofview.V82.tactic (fun gl -> error "eres_pf") @@ -390,14 +389,21 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly})) | Unfold_nth c -> Proofview.V82.tactic (fun gl -> if exists_evaluable_reference (pf_env gl) c then - tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl) gl + tclPROGRESS (Proofview.V82.of_tactic (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)) gl else tclFAIL 0 (str"Unbound reference") gl) | Extern tacast -> conclPattern concl p tacast in - tclLOG dbg (fun () -> pr_hint t) (run_hint t tactic) + let pr_hint () = + let origin = match dbname with + | None -> mt () + | Some n -> str " (in " ++ str n ++ str ")" + in + pr_hint t ++ origin + in + tclLOG dbg pr_hint (run_hint t tactic) -and trivial_resolve dbg mod_delta db_list local_db cl = +and trivial_resolve dbg mod_delta db_list local_db secvars cl = try let head = try let hdconstr = decompose_app_bound cl in @@ -406,33 +412,33 @@ and trivial_resolve dbg mod_delta db_list local_db cl = in List.map (tac_of_hint dbg db_list local_db cl) (priority - (my_find_search mod_delta db_list local_db head cl)) + (my_find_search mod_delta db_list local_db secvars head cl)) with Not_found -> [] (** The use of the "core" database can be de-activated by passing "nocore" amongst the databases. *) let trivial ?(debug=Off) lems dbnames = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let db_list = make_db_list dbnames in let d = mk_trivial_dbg debug in let hints = make_local_hint_db env sigma false lems in tclTRY_dbg d (trivial_fail_db d false db_list hints) - end + end } let full_trivial ?(debug=Off) lems = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let db_list = current_pure_db () in let d = mk_trivial_dbg debug in let hints = make_local_hint_db env sigma false lems in tclTRY_dbg d (trivial_fail_db d false db_list hints) - end + end } let gen_trivial ?(debug=Off) lems = function | None -> full_trivial ~debug lems @@ -444,7 +450,7 @@ let h_trivial ?(debug=Off) lems l = gen_trivial ~debug lems l (* The classical Auto tactic *) (**************************************************************************) -let possible_resolve dbg mod_delta db_list local_db cl = +let possible_resolve dbg mod_delta db_list local_db secvars cl = try let head = try let hdconstr = decompose_app_bound cl in @@ -452,12 +458,12 @@ let possible_resolve dbg mod_delta db_list local_db cl = with Bound -> None in List.map (tac_of_hint dbg db_list local_db cl) - (my_find_search mod_delta db_list local_db head cl) + (my_find_search mod_delta db_list local_db secvars head cl) with Not_found -> [] let extend_local_db decl db gl = let env = Tacmach.New.pf_env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in Hint_db.add_list env sigma (make_resolve_hyp env sigma decl) db (* Introduce an hypothesis, then call the continuation tactic [kont] @@ -465,10 +471,10 @@ let extend_local_db decl db gl = let intro_register dbg kont db = Tacticals.New.tclTHEN (dbg_intro dbg) - (Proofview.Goal.enter begin fun gl -> + (Proofview.Goal.enter { enter = begin fun gl -> let extend_local_db decl db = extend_local_db decl db gl in Tacticals.New.onLastDecl (fun decl -> kont (extend_local_db decl db)) - end) + end }) (* n is the max depth of search *) (* local_db contains the local Hypotheses *) @@ -481,14 +487,15 @@ let search d n mod_delta db_list local_db = if Int.equal n 0 then Tacticals.New.tclZEROMSG (str"BOUND 2") else Tacticals.New.tclORELSE0 (dbg_assumption d) (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db) - ( Proofview.Goal.enter begin fun gl -> + ( Proofview.Goal.enter { enter = begin fun gl -> let concl = Tacmach.New.pf_nf_concl gl in + let secvars = compute_secvars gl in let d' = incr_dbg d in Tacticals.New.tclFIRST (List.map (fun ntac -> Tacticals.New.tclTHEN ntac (search d' (n-1) local_db)) - (possible_resolve d mod_delta db_list local_db concl)) - end)) + (possible_resolve d mod_delta db_list local_db secvars concl)) + end })) end [] in search d n local_db @@ -496,15 +503,15 @@ let search d n mod_delta db_list local_db = let default_search_depth = ref 5 let delta_auto debug mod_delta n lems dbnames = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let db_list = make_db_list dbnames in let d = mk_auto_dbg debug in let hints = make_local_hint_db env sigma false lems in tclTRY_dbg d (search d n mod_delta db_list hints) - end + end } let delta_auto = if Flags.profile then @@ -519,15 +526,15 @@ let new_auto ?(debug=Off) n = delta_auto debug true n let default_auto = auto !default_search_depth [] [] let delta_full_auto ?(debug=Off) mod_delta n lems = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let db_list = current_pure_db () in let d = mk_auto_dbg debug in let hints = make_local_hint_db env sigma false lems in tclTRY_dbg d (search d n mod_delta db_list hints) - end + end } let full_auto ?(debug=Off) n = delta_full_auto ~debug false n let new_full_auto ?(debug=Off) n = delta_full_auto ~debug true n -- cgit v1.2.3