From f66bd46c551915267a88d1ee2534ba091292882e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 8 Jun 2020 12:54:27 +0200 Subject: Do not export flags in Hints.make_resolves. They are always the same. --- tactics/hints.ml | 3 +++ 1 file changed, 3 insertions(+) (limited to 'tactics/hints.ml') diff --git a/tactics/hints.ml b/tactics/hints.ml index 0c23532e12..58fbf2fd66 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1336,6 +1336,9 @@ let constructor_hints env sigma eapply lems = List.map_append (fun (poly, lem) -> make_resolves env sigma (eapply,true,false) empty_hint_info ~check:true ~poly lem) lems +let make_resolves env sigma info ~check ~poly ?name hint = + make_resolves env sigma (true, false, false) info ~check ~poly ?name hint + let make_local_hint_db env sigma ts eapply lems = let map c = c env sigma in let lems = List.map map lems in -- cgit v1.2.3 From 2a24a665ca63d82ce2576e75636ab6fdbcad9b36 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 8 Jun 2020 15:19:03 +0200 Subject: Remove dead code in the Hints API. --- tactics/hints.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'tactics/hints.ml') diff --git a/tactics/hints.ml b/tactics/hints.ml index 58fbf2fd66..9595fa2033 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -489,7 +489,6 @@ module Hint_db : sig type t val empty : ?name:hint_db_name -> TransparentState.t -> bool -> t -val find : GlobRef.t -> t -> search_entry val map_none : secvars:Id.Pred.t -> t -> full_hint list val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list val map_existential : evar_map -> secvars:Id.Pred.t -> -- cgit v1.2.3 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/hints.ml | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) (limited to 'tactics/hints.ml') diff --git a/tactics/hints.ml b/tactics/hints.ml index 9595fa2033..78ed81ec37 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1576,4 +1576,17 @@ let run_hint tac k = match warn_hint () with let info = Exninfo.reify () in Proofview.tclZERO ~info (UserError (None, (str "Tactic failure."))) -let repr_hint h = h.obj +module FullHint = +struct + type t = full_hint + let priority (h : t) = h.pri + let is_polymorphic (h : t) = h.poly + let pattern (h : t) = h.pat + let database (h : t) = h.db + let run (h : t) k = run_hint h.code k + let print env sigma (h : t) = pr_hint env sigma h.code + let name (h : t) = h.name + let secvars (h : t) = h.secvars + + let repr (h : t) = h.code.obj +end -- cgit v1.2.3 From 437f86aaa55bbae99742b600bb52a234d75667e5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 8 Jun 2020 16:21:21 +0200 Subject: Remove access to hint section variables. The only use was seemingly a bug introduced in 0aec9033a by an accidental variable capture. There is indeed no reason that the set of variables of a hint corresponds to the one of the current environment. --- tactics/hints.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'tactics/hints.ml') diff --git a/tactics/hints.ml b/tactics/hints.ml index 78ed81ec37..63ca4b8834 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1586,7 +1586,6 @@ struct let run (h : t) k = run_hint h.code k let print env sigma (h : t) = pr_hint env sigma h.code let name (h : t) = h.name - let secvars (h : t) = h.secvars let repr (h : t) = h.code.obj end -- 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/hints.ml | 31 +++++++++++++++++++------------ 1 file changed, 19 insertions(+), 12 deletions(-) (limited to 'tactics/hints.ml') diff --git a/tactics/hints.ml b/tactics/hints.ml index 63ca4b8834..0a213d5d0e 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -137,7 +137,12 @@ type 'a with_uid = { type raw_hint = constr * types * Univ.ContextSet.t -type hint = (raw_hint * clausenv) hint_ast with_uid +type hint = { + hint_term : constr; + hint_type : types; + hint_uctx : Univ.ContextSet.t; + hint_clnv : clausenv; +} type 'a with_metadata = { pri : int @@ -156,7 +161,7 @@ type 'a with_metadata = (** the tactic to apply when the concl matches pat *) } -type full_hint = hint with_metadata +type full_hint = hint hint_ast with_uid with_metadata type hint_entry = GlobRef.t option * raw_hint hint_ast with_uid with_metadata @@ -303,16 +308,18 @@ let instantiate_hint env sigma p = let mk_clenv (c, cty, ctx) = let sigma = Evd.merge_context_set univ_flexible sigma ctx in let cl = mk_clenv_from_env env sigma None (c,cty) in - {cl with templval = + let cl = {cl with templval = { cl.templval with rebus = strip_params env sigma cl.templval.rebus }; env = empty_env} + in + { hint_term = c; hint_type = cty; hint_uctx = ctx; hint_clnv = cl; } in let code = match p.code.obj with - | Res_pf c -> Res_pf (c, mk_clenv c) - | ERes_pf c -> ERes_pf (c, mk_clenv c) + | Res_pf c -> Res_pf (mk_clenv c) + | ERes_pf c -> ERes_pf (mk_clenv c) | Res_pf_THEN_trivial_fail c -> - Res_pf_THEN_trivial_fail (c, mk_clenv c) - | Give_exact c -> Give_exact (c, mk_clenv c) + Res_pf_THEN_trivial_fail (mk_clenv c) + | Give_exact c -> Give_exact (mk_clenv c) | Unfold_nth e -> Unfold_nth e | Extern t -> Extern t in @@ -1367,13 +1374,13 @@ let make_db_list dbnames = (* Functions for printing the hints *) (**************************************************************************) -let pr_hint_elt env sigma (c, _, _) = pr_econstr_env env sigma c +let pr_hint_elt env sigma h = pr_econstr_env env sigma h.hint_term let pr_hint env sigma h = match h.obj with - | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt env sigma c) - | ERes_pf (c, _) -> (str"simple eapply " ++ pr_hint_elt env sigma c) - | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt env sigma c) - | Res_pf_THEN_trivial_fail (c, _) -> + | Res_pf c -> (str"simple apply " ++ pr_hint_elt env sigma c) + | ERes_pf c -> (str"simple eapply " ++ pr_hint_elt env sigma c) + | Give_exact c -> (str"exact " ++ pr_hint_elt env sigma c) + | Res_pf_THEN_trivial_fail c -> (str"simple apply " ++ pr_hint_elt env sigma c ++ str" ; trivial") | Unfold_nth c -> str"unfold " ++ pr_evaluable_reference c -- 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/hints.ml | 63 +++++++++++++++++++++++++++----------------------------- 1 file changed, 30 insertions(+), 33 deletions(-) (limited to 'tactics/hints.ml') diff --git a/tactics/hints.ml b/tactics/hints.ml index 0a213d5d0e..7a5615dd8e 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -135,20 +135,20 @@ type 'a with_uid = { uid : KerName.t; } -type raw_hint = constr * types * Univ.ContextSet.t +type raw_hint = constr * types * Univ.ContextSet.t * bool (* poly *) type hint = { hint_term : constr; hint_type : types; hint_uctx : Univ.ContextSet.t; hint_clnv : clausenv; + hint_poly : bool; + (** Is the hint polymorpic and hence should be refreshed at each application *) } type 'a with_metadata = { pri : int (** A number lower is higher priority *) - ; poly : bool - (** Is the hint polymorpic and hence should be refreshed at each application *) ; pat : constr_pattern option (** A pattern for the concl of the Goal *) ; name : hints_path_atom @@ -305,14 +305,14 @@ let strip_params env sigma c = | _ -> c let instantiate_hint env sigma p = - let mk_clenv (c, cty, ctx) = + let mk_clenv (c, cty, ctx, poly) = let sigma = Evd.merge_context_set univ_flexible sigma ctx in let cl = mk_clenv_from_env env sigma None (c,cty) in let cl = {cl with templval = { cl.templval with rebus = strip_params env sigma cl.templval.rebus }; env = empty_env} in - { hint_term = c; hint_type = cty; hint_uctx = ctx; hint_clnv = cl; } + { hint_term = c; hint_type = cty; hint_uctx = ctx; hint_clnv = cl; hint_poly = poly } in let code = match p.code.obj with | Res_pf c -> Res_pf (mk_clenv c) @@ -806,9 +806,9 @@ let make_exact_entry env sigma info ~poly ?(name=PathAny) (c, cty, ctx) = | None -> pat in (Some hd, - { pri; poly; pat = Some pat; name; + { pri; pat = Some pat; name; db = None; secvars; - code = with_uid (Give_exact (c, cty, ctx)); }) + code = with_uid (Give_exact (c, cty, ctx, poly)); }) let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) (c, cty, ctx) = let cty = if hnf then hnf_constr env sigma cty else cty in @@ -830,10 +830,10 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) ( in if Int.equal nmiss 0 then (Some hd, - { pri; poly; pat = Some pat; name; + { pri; pat = Some pat; name; db = None; secvars; - code = with_uid (Res_pf(c,cty,ctx)); }) + code = with_uid (Res_pf(c,cty,ctx,poly)); }) else begin if not eapply then failwith "make_apply_entry"; if verbose then begin @@ -849,9 +849,9 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) ( ) end; (Some hd, - { pri; poly; pat = Some pat; name; + { pri; pat = Some pat; name; db = None; secvars; - code = with_uid (ERes_pf(c,cty,ctx)); }) + code = with_uid (ERes_pf(c,cty,ctx,poly)); }) end | _ -> failwith "make_apply_entry" @@ -922,7 +922,6 @@ let make_unfold eref = let g = global_of_evaluable_reference eref in (Some g, { pri = 4; - poly = false; pat = None; name = PathHints [g]; db = None; @@ -933,7 +932,6 @@ let make_extern pri pat tacast = let hdconstr = Option.map try_head_pattern pat in (hdconstr, { pri = pri; - poly = false; pat = pat; name = PathAny; db = None; @@ -960,12 +958,11 @@ let make_trivial env sigma poly ?(name=PathAny) r = let ce = mk_clenv_from_env env sigma None (c,t) in (Some hd, { pri=1; - poly = poly; pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma (clenv_type ce))); name = name; db = None; secvars = secvars_of_constr env sigma c; - code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) }) + code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx,poly)) }) @@ -1076,29 +1073,30 @@ let subst_autohint (subst, obj) = (try head_constr_bound Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value) with Bound -> gr') in + let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in + let subst_aux ((c, t, ctx, poly) as h) = + let c' = subst_mps subst c in + let t' = subst_mps subst t in + if c==c' && t'==t then h else (c', t', ctx, poly) + in let subst_hint (k,data as hint) = let k' = Option.Smart.map subst_key k in let env = Global.env () in let sigma = Evd.from_env env in let pat' = Option.Smart.map (subst_pattern env sigma subst) data.pat in - let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in let code' = match data.code.obj with - | Res_pf (c,t,ctx) -> - let c' = subst_mps subst c in - let t' = subst_mps subst t in - if c==c' && t'==t then data.code.obj else Res_pf (c', t',ctx) - | ERes_pf (c,t,ctx) -> - let c' = subst_mps subst c in - let t' = subst_mps subst t in - if c==c' && t'==t then data.code.obj else ERes_pf (c',t',ctx) - | Give_exact (c,t,ctx) -> - let c' = subst_mps subst c in - let t' = subst_mps subst t in - if c==c' && t'== t then data.code.obj else Give_exact (c',t',ctx) - | Res_pf_THEN_trivial_fail (c,t,ctx) -> - let c' = subst_mps subst c in - let t' = subst_mps subst t in - if c==c' && t==t' then data.code.obj else Res_pf_THEN_trivial_fail (c',t',ctx) + | Res_pf h -> + let h' = subst_aux h in + if h == h' then data.code.obj else Res_pf h' + | ERes_pf h -> + let h' = subst_aux h in + if h == h' then data.code.obj else ERes_pf h' + | Give_exact h -> + let h' = subst_aux h in + if h == h' then data.code.obj else Give_exact h' + | Res_pf_THEN_trivial_fail h -> + let h' = subst_aux h in + if h == h' then data.code.obj else Res_pf_THEN_trivial_fail h' | Unfold_nth ref -> let ref' = subst_evaluable_reference subst ref in if ref==ref' then data.code.obj else Unfold_nth ref' @@ -1587,7 +1585,6 @@ module FullHint = struct type t = full_hint let priority (h : t) = h.pri - let is_polymorphic (h : t) = h.poly let pattern (h : t) = h.pat let database (h : t) = h.db let run (h : t) k = run_hint h.code k -- cgit v1.2.3