From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- tactics/auto.ml | 197 ++++++++++++++++++++++++++++---------------------------- 1 file changed, 99 insertions(+), 98 deletions(-) (limited to 'tactics/auto.ml') diff --git a/tactics/auto.ml b/tactics/auto.ml index bc644857..0c0d9bcf 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1,26 +1,24 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Int.equal hint.pri 0) l let compute_secvars gl = - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let hyps = Proofview.Goal.hyps gl in secvars_of_hyps hyps (* tell auto not to reuse already instantiated metas in unification (for @@ -44,9 +42,9 @@ let compute_secvars gl = open Unification -let auto_core_unif_flags_of st1 st2 useeager = { +let auto_core_unif_flags_of st1 st2 = { modulo_conv_on_closed_terms = Some st1; - use_metas_eagerly_in_conv_on_closed_terms = useeager; + use_metas_eagerly_in_conv_on_closed_terms = false; use_evars_eagerly_in_conv_on_closed_terms = false; modulo_delta = st2; modulo_delta_types = full_transparent_state; @@ -59,8 +57,8 @@ let auto_core_unif_flags_of st1 st2 useeager = { modulo_eta = true; } -let auto_unif_flags_of st1 st2 useeager = - let flags = auto_core_unif_flags_of st1 st2 useeager in { +let auto_unif_flags_of st1 st2 = + let flags = auto_core_unif_flags_of st1 st2 in { core_unify_flags = flags; merge_unify_flags = flags; subterm_unify_flags = { flags with modulo_delta = empty_transparent_state }; @@ -69,7 +67,7 @@ let auto_unif_flags_of st1 st2 useeager = } let auto_unif_flags = - auto_unif_flags_of full_transparent_state empty_transparent_state false + auto_unif_flags_of full_transparent_state empty_transparent_state (* Try unification with the precompiled clause, then use registered Apply *) @@ -84,27 +82,28 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl = if poly then (** Refresh the instance of the hint *) let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in - let map c = Vars.subst_univs_level_constr subst c in + let map c = CVars.subst_univs_level_constr subst c in + let emap c = Vars.subst_univs_level_constr subst c in let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in (** Only metas are mentioning the old universes. *) let clenv = { - templval = Evd.map_fl map clenv.templval; - templtyp = Evd.map_fl map clenv.templtyp; + templval = Evd.map_fl emap clenv.templval; + templtyp = Evd.map_fl emap clenv.templtyp; evd = Evd.map_metas map evd; env = Proofview.Goal.env gl; } in - clenv, map c + clenv, emap 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 { enter = begin fun gl -> + Proofview.Goal.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 + let clenv = clenv_unique_resolver ~flags clenv gl in Clenvtac.clenv_refine false clenv - end } + end let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h @@ -113,12 +112,12 @@ let unify_resolve_gen poly = function | Some flags -> unify_resolve poly flags let exact poly (c,clenv) = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.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 } + end (* Util *) @@ -142,15 +141,15 @@ let conclPattern concl pat tac = try Proofview.tclUNIT (Constr_matching.matches env sigma pat concl) with Constr_matching.PatternMatchingFailure -> - Tacticals.New.tclZEROMSG (str "conclPattern") + Tacticals.New.tclZEROMSG (str "pattern-matching failed") in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in constr_bindings env sigma >>= fun constr_bindings -> let open Genarg in let open Geninterp in - let inj c = match val_tag (topwit Constrarg.wit_constr) with + let inj c = match val_tag (topwit Stdarg.wit_constr) with | Val.Base tag -> Val.Dyn (tag, c) | _ -> assert false in @@ -160,7 +159,7 @@ let conclPattern concl pat tac = match tac with | GenArg (Glbwit wit, tac) -> Ftactic.run (Geninterp.interp wit ist tac) (fun _ -> Proofview.tclUNIT ()) - end } + end (***********************************************************) (** A debugging / verbosity framework for trivial and auto *) @@ -177,8 +176,7 @@ let global_info_auto = ref false let add_option ls refe = let _ = Goptions.declare_bool_option - { Goptions.optsync = true; - Goptions.optdepr = false; + { Goptions.optdepr = false; Goptions.optname = String.concat " " ls; Goptions.optkey = ls; Goptions.optread = (fun () -> !refe); @@ -191,35 +189,34 @@ let _ = add_option ["Info";"Trivial"] global_info_trivial; add_option ["Info";"Auto"] global_info_auto -let no_dbg () = (Off,0,ref []) +type debug_kind = ReportForTrivial | ReportForAuto + +let no_dbg (_,whatfor,_,_) = (Off,whatfor,0,ref []) let mk_trivial_dbg debug = let d = if debug == Debug || !global_debug_trivial then Debug else if debug == Info || !global_info_trivial then Info else Off - in (d,0,ref []) - -(** Note : we start the debug depth of auto at 1 to distinguish it - for trivial (whose depth is 0). *) + in (d,ReportForTrivial,0,ref []) let mk_auto_dbg debug = let d = if debug == Debug || !global_debug_auto then Debug else if debug == Info || !global_info_auto then Info else Off - in (d,1,ref []) + in (d,ReportForAuto,0,ref []) -let incr_dbg = function (dbg,depth,trace) -> (dbg,depth+1,trace) +let incr_dbg = function (dbg,whatfor,depth,trace) -> (dbg,whatfor,depth+1,trace) (** A tracing tactic for debug/info trivial/auto *) -let tclLOG (dbg,depth,trace) pp tac = +let tclLOG (dbg,_,depth,trace) pp tac = match dbg with | Off -> tac | Debug -> (* For "debug (trivial/auto)", we directly output messages *) - let s = String.make depth '*' in + let s = String.make (depth+1) '*' in Proofview.V82.tactic begin fun gl -> try let out = Proofview.V82.of_tactic tac gl in @@ -263,20 +260,20 @@ let pr_info_atom (d,pp) = str (String.make d ' ') ++ pp () ++ str "." let pr_info_trace = function - | (Info,_,{contents=(d,Some pp)::l}) -> + | (Info,_,_,{contents=(d,Some pp)::l}) -> Feedback.msg_info (prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l)) | _ -> () let pr_info_nop = function - | (Info,_,_) -> Feedback.msg_info (str "idtac.") + | (Info,_,_,_) -> Feedback.msg_info (str "idtac.") | _ -> () let pr_dbg_header = function - | (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: *)") + | (Off,_,_,_) -> () + | (Debug,ReportForTrivial,_,_) -> Feedback.msg_debug (str "(* debug trivial: *)") + | (Debug,ReportForAuto,_,_) -> Feedback.msg_debug (str "(* debug auto: *)") + | (Info,ReportForTrivial,_,_) -> Feedback.msg_info (str "(* info trivial: *)") + | (Info,ReportForAuto,_,_) -> Feedback.msg_info (str "(* info auto: *)") let tclTRY_dbg d tac = let delay f = Proofview.tclUNIT () >>= fun () -> f () in @@ -294,18 +291,18 @@ let tclTRY_dbg d tac = de Hint impérative a été remplacée par plusieurs bases fonctionnelles *) let flags_of_state st = - auto_unif_flags_of st st false + auto_unif_flags_of st st let auto_flags_of_state st = - auto_unif_flags_of full_transparent_state st false + auto_unif_flags_of full_transparent_state st -let hintmap_of secvars hdc concl = +let hintmap_of sigma secvars hdc concl = match hdc with | None -> Hint_db.map_none ~secvars | Some hdc -> - if occur_existential concl then - Hint_db.map_existential ~secvars hdc concl - else Hint_db.map_auto ~secvars hdc concl + if occur_existential sigma concl then + Hint_db.map_existential sigma ~secvars hdc concl + else Hint_db.map_auto sigma ~secvars hdc concl let exists_evaluable_reference env = function | EvalConstRef _ -> true @@ -317,37 +314,38 @@ 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 { enter = begin fun gl -> + ( Proofview.Goal.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 decl = Tacmach.New.pf_last_hyp gl 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 { enter = begin fun gl -> - let concl = Tacmach.New.pf_nf_concl gl in + Proofview.Goal.enter begin fun gl -> + let concl = Tacmach.New.pf_concl gl in + let sigma = Tacmach.New.project 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 secvars concl))) - end } + (trivial_resolve sigma dbg mod_delta db_list local_db secvars concl))) + end -and my_find_search_nodelta db_list local_db secvars hdc concl = +and my_find_search_nodelta sigma db_list local_db secvars hdc concl = List.map (fun hint -> (None,hint)) - (List.map_append (hintmap_of secvars hdc concl) (local_db::db_list)) + (List.map_append (hintmap_of sigma 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 secvars hdc concl = - let f = hintmap_of secvars hdc concl in - if occur_existential concl then +and my_find_search_delta sigma db_list local_db secvars hdc concl = + let f = hintmap_of sigma secvars hdc concl in + if occur_existential sigma concl then List.map_append (fun db -> if Hint_db.use_dn db then @@ -369,8 +367,8 @@ and my_find_search_delta db_list local_db secvars hdc concl = 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 ~secvars hdc concl db - else Hint_db.map_existential ~secvars hdc concl db + then Hint_db.map_auto sigma ~secvars hdc concl db + else Hint_db.map_existential sigma ~secvars hdc concl db in auto_flags_of_state st, l in List.map (fun x -> (Some flags,x)) l) (local_db::db_list) @@ -378,20 +376,21 @@ and my_find_search_delta db_list local_db secvars hdc concl = 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") + | ERes_pf _ -> Proofview.Goal.enter (fun gl -> Tacticals.New.tclZEROMSG (str "eres_pf")) | Give_exact (c, cl) -> exact poly (c, cl) | Res_pf_THEN_trivial_fail (c,cl) -> Tacticals.New.tclTHEN (unify_resolve_gen poly flags (c,cl)) (* With "(debug) trivial", we shouldn't end here, and with "debug auto" we don't display the details of inner trivial *) - (trivial_fail_db (no_dbg ()) (not (Option.is_empty flags)) db_list local_db) + (trivial_fail_db (no_dbg dbg) (not (Option.is_empty flags)) db_list local_db) | Unfold_nth c -> - Proofview.V82.tactic (fun gl -> - if exists_evaluable_reference (pf_env gl) c then - tclPROGRESS (Proofview.V82.of_tactic (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)) gl - else tclFAIL 0 (str"Unbound reference") gl) - | Extern tacast -> + Proofview.Goal.enter begin fun gl -> + if exists_evaluable_reference (Tacmach.New.pf_env gl) c then + Tacticals.New.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl) + else Tacticals.New.tclFAIL 0 (str"Unbound reference") + end + | Extern tacast -> conclPattern concl p tacast in let pr_hint () = @@ -399,27 +398,28 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db= | None -> mt () | Some n -> str " (in " ++ str n ++ str ")" in - pr_hint t ++ origin + let sigma, env = Pfedit.get_current_context () in + pr_hint env sigma t ++ origin in tclLOG dbg pr_hint (run_hint t tactic) -and trivial_resolve dbg mod_delta db_list local_db secvars cl = +and trivial_resolve sigma dbg mod_delta db_list local_db secvars cl = try let head = - try let hdconstr = decompose_app_bound cl in + try let hdconstr = decompose_app_bound sigma cl in Some hdconstr with Bound -> None in List.map (tac_of_hint dbg db_list local_db cl) (priority - (my_find_search mod_delta db_list local_db secvars head cl)) + (my_find_search mod_delta sigma 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 { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let db_list = make_db_list dbnames in @@ -427,10 +427,10 @@ let trivial ?(debug=Off) lems dbnames = 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 { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let db_list = current_pure_db () in @@ -438,7 +438,7 @@ let full_trivial ?(debug=Off) lems = 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 @@ -450,15 +450,15 @@ 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 secvars cl = +let possible_resolve sigma dbg mod_delta db_list local_db secvars cl = try let head = - try let hdconstr = decompose_app_bound cl in + try let hdconstr = decompose_app_bound sigma cl in Some hdconstr with Bound -> None in List.map (tac_of_hint dbg db_list local_db cl) - (my_find_search mod_delta db_list local_db secvars head cl) + (my_find_search mod_delta sigma db_list local_db secvars head cl) with Not_found -> [] let extend_local_db decl db gl = @@ -471,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 { enter = begin fun gl -> + (Proofview.Goal.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 *) @@ -487,15 +487,16 @@ 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 { enter = begin fun gl -> - let concl = Tacmach.New.pf_nf_concl gl in + ( Proofview.Goal.enter begin fun gl -> + let concl = Tacmach.New.pf_concl gl in + let sigma = Tacmach.New.project 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 secvars concl)) - end })) + (possible_resolve sigma d mod_delta db_list local_db secvars concl)) + end)) end [] in search d n local_db @@ -503,7 +504,7 @@ 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 { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let db_list = make_db_list dbnames in @@ -511,12 +512,12 @@ let delta_auto debug mod_delta n lems dbnames = 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 - let key = Profile.declare_profile "delta_auto" in - Profile.profile5 key delta_auto + let key = CProfile.declare_profile "delta_auto" in + CProfile.profile5 key delta_auto else delta_auto let auto ?(debug=Off) n = delta_auto debug false n @@ -526,7 +527,7 @@ 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 { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let db_list = current_pure_db () in @@ -534,7 +535,7 @@ let delta_full_auto ?(debug=Off) mod_delta n lems = 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