From 21b4e41544f03de18d9f5b1bdb93a26b36a97999 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 8 Jun 2020 15:17:33 +0200 Subject: Opacify the type of hint metadata. --- tactics/auto.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'tactics/auto.ml') diff --git a/tactics/auto.ml b/tactics/auto.ml index 681c4e910f..a73db95884 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -29,7 +29,7 @@ open Hints (* tactics with a trace mechanism for automatic search *) (**************************************************************************) -let priority l = List.filter (fun (_, hint) -> Int.equal hint.pri 0) l +let priority l = List.filter (fun (_, hint) -> Int.equal (FullHint.priority hint) 0) l let compute_secvars gl = let hyps = Proofview.Goal.hyps gl in @@ -381,7 +381,8 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl = 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;db=dbname})) = +and tac_of_hint dbg db_list local_db concl (flags, h) = + let poly = FullHint.is_polymorphic h in let tactic = function | Res_pf (c,cl) -> unify_resolve_gen ~poly flags (c,cl) | ERes_pf _ -> Proofview.Goal.enter (fun gl -> @@ -403,16 +404,17 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db= Tacticals.New.tclFAIL ~info 0 (str"Unbound reference") end | Extern tacast -> + let p = FullHint.pattern h in conclPattern concl p tacast in let pr_hint env sigma = - let origin = match dbname with + let origin = match FullHint.database h with | None -> mt () | Some n -> str " (in " ++ str n ++ str ")" in - pr_hint env sigma t ++ origin + FullHint.print env sigma h ++ origin in - tclLOG dbg pr_hint (run_hint t tactic) + tclLOG dbg pr_hint (FullHint.run h tactic) and trivial_resolve sigma dbg mod_delta db_list local_db secvars cl = try -- cgit v1.2.3 From 9eca7cca68dc82aa738a8d408d75e1b9b5405646 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 8 Jun 2020 18:57:25 +0200 Subject: Wrap the content of full hints into a record. --- tactics/auto.ml | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) (limited to 'tactics/auto.ml') diff --git a/tactics/auto.ml b/tactics/auto.ml index a73db95884..4ed01d4e65 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -69,7 +69,8 @@ let auto_unif_flags = (* Try unification with the precompiled clause, then use registered Apply *) -let connect_hint_clenv ~poly (c, _, ctx) clenv gl = +let connect_hint_clenv ~poly h gl = + let { hint_term = c; hint_uctx = ctx; hint_clnv = clenv } = h in (* [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. *) @@ -95,9 +96,9 @@ let connect_hint_clenv ~poly (c, _, ctx) clenv gl = { clenv with evd = evd ; env = Proofview.Goal.env gl }, c in clenv, c -let unify_resolve ~poly flags ((c : raw_hint), clenv) = +let unify_resolve ~poly flags (h : hint) = Proofview.Goal.enter begin fun gl -> - let clenv, c = connect_hint_clenv ~poly c clenv gl in + let clenv, c = connect_hint_clenv ~poly h gl in let clenv = clenv_unique_resolver ~flags clenv gl in Clenvtac.clenv_refine clenv end @@ -108,9 +109,9 @@ let unify_resolve_gen ~poly = function | None -> unify_resolve_nodelta poly | Some flags -> unify_resolve ~poly flags -let exact poly (c,clenv) = +let exact poly h = Proofview.Goal.enter begin fun gl -> - let clenv', c = connect_hint_clenv ~poly c clenv gl in + let clenv', c = connect_hint_clenv ~poly h gl in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) (exact_check c) @@ -384,14 +385,14 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl = and tac_of_hint dbg db_list local_db concl (flags, h) = let poly = FullHint.is_polymorphic h in let tactic = function - | Res_pf (c,cl) -> unify_resolve_gen ~poly flags (c,cl) + | Res_pf h -> unify_resolve_gen ~poly flags h | ERes_pf _ -> Proofview.Goal.enter (fun gl -> let info = Exninfo.reify () in Tacticals.New.tclZEROMSG ~info (str "eres_pf")) - | Give_exact (c, cl) -> exact poly (c, cl) - | Res_pf_THEN_trivial_fail (c,cl) -> + | Give_exact h -> exact poly h + | Res_pf_THEN_trivial_fail h -> Tacticals.New.tclTHEN - (unify_resolve_gen ~poly flags (c,cl)) + (unify_resolve_gen ~poly flags h) (* 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 dbg) (not (Option.is_empty flags)) db_list local_db) -- cgit v1.2.3 From c00a369a8bd70efad3e1481daa78ab483038c6cb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 8 Jun 2020 19:20:02 +0200 Subject: Move the hint polymorphic status to the hint instance. It is only used for this kind of hints, never for Extern / Unfold. --- tactics/auto.ml | 27 +++++++++++++-------------- 1 file changed, 13 insertions(+), 14 deletions(-) (limited to 'tactics/auto.ml') diff --git a/tactics/auto.ml b/tactics/auto.ml index 4ed01d4e65..f041af1db1 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -69,7 +69,7 @@ let auto_unif_flags = (* Try unification with the precompiled clause, then use registered Apply *) -let connect_hint_clenv ~poly h gl = +let connect_hint_clenv h gl = let { hint_term = c; hint_uctx = ctx; hint_clnv = clenv } = h in (* [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 @@ -78,7 +78,7 @@ let connect_hint_clenv ~poly h gl = 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 = - if poly then + if h.hint_poly then (* Refresh the instance of the hint *) let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in let emap c = Vars.subst_univs_level_constr subst c in @@ -96,22 +96,22 @@ let connect_hint_clenv ~poly h gl = { clenv with evd = evd ; env = Proofview.Goal.env gl }, c in clenv, c -let unify_resolve ~poly flags (h : hint) = +let unify_resolve flags (h : hint) = Proofview.Goal.enter begin fun gl -> - let clenv, c = connect_hint_clenv ~poly h gl in + let clenv, c = connect_hint_clenv h gl in let clenv = clenv_unique_resolver ~flags clenv gl in Clenvtac.clenv_refine clenv end -let unify_resolve_nodelta poly h = unify_resolve ~poly auto_unif_flags h +let unify_resolve_nodelta h = unify_resolve auto_unif_flags h -let unify_resolve_gen ~poly = function - | None -> unify_resolve_nodelta poly - | Some flags -> unify_resolve ~poly flags +let unify_resolve_gen = function + | None -> unify_resolve_nodelta + | Some flags -> unify_resolve flags -let exact poly h = +let exact h = Proofview.Goal.enter begin fun gl -> - let clenv', c = connect_hint_clenv ~poly h gl in + let clenv', c = connect_hint_clenv h gl in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd)) (exact_check c) @@ -383,16 +383,15 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl = (local_db::db_list) and tac_of_hint dbg db_list local_db concl (flags, h) = - let poly = FullHint.is_polymorphic h in let tactic = function - | Res_pf h -> unify_resolve_gen ~poly flags h + | Res_pf h -> unify_resolve_gen flags h | ERes_pf _ -> Proofview.Goal.enter (fun gl -> let info = Exninfo.reify () in Tacticals.New.tclZEROMSG ~info (str "eres_pf")) - | Give_exact h -> exact poly h + | Give_exact h -> exact h | Res_pf_THEN_trivial_fail h -> Tacticals.New.tclTHEN - (unify_resolve_gen ~poly flags h) + (unify_resolve_gen flags h) (* 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 dbg) (not (Option.is_empty flags)) db_list local_db) -- cgit v1.2.3