aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/class_tactics.ml13
-rw-r--r--tactics/hints.ml134
-rw-r--r--tactics/hints.mli11
3 files changed, 66 insertions, 92 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 96cbbf0ba8..b4d7e7d7f0 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -158,7 +158,7 @@ let unify_resolve ~with_evars flags h diff = match diff with
| None ->
Hints.hint_res_pf ~with_evars ~with_classes:false ~flags h
| Some (diff, ty) ->
- let () = assert (not h.hint_poly) in
+ let () = assert (Option.is_empty h.hint_uctx) in
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
@@ -203,11 +203,10 @@ let unify_resolve_refine flags h diff =
let with_prods nprods h f =
if get_typeclasses_limit_intros () then
Proofview.Goal.enter begin fun gl ->
- let { hint_term = c; hint_poly = poly } = h in
- if poly || Int.equal nprods 0 then f None
+ if Option.has_some h.hint_uctx || Int.equal nprods 0 then f None
else
let sigma = Tacmach.New.project gl in
- let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in
+ let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma h.hint_term in
let diff = nb_prod sigma ty - nprods in
if (>=) diff 0 then f (Some (diff, ty))
else Tacticals.New.tclZEROMSG (str"Not enough premisses")
@@ -489,12 +488,12 @@ let make_resolve_hyp env sigma st only_classes pri decl =
let hints = build_subclasses ~check:false env sigma id empty_hint_info in
(List.map_append
(fun (path,info,c) ->
- let h = IsConstr (EConstr.of_constr c,Univ.ContextSet.empty) [@ocaml.warning "-3"] in
- make_resolves env sigma ~name:(PathHints path) info ~check:true ~poly:false h)
+ let h = IsConstr (EConstr.of_constr c, None) [@ocaml.warning "-3"] in
+ make_resolves env sigma ~name:(PathHints path) info ~check:true h)
hints)
else []
in
- (hints @ make_resolves env sigma pri ~name ~check:false ~poly:false (IsGlobRef id))
+ (hints @ make_resolves env sigma pri ~name ~check:false (IsGlobRef id))
else []
let make_hints g (modes,st) only_classes sign =
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 355cea8fa8..fe3efef7c5 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -129,22 +129,20 @@ type hints_path = GlobRef.t hints_path_gen
type hint_term =
| IsGlobRef of GlobRef.t
- | IsConstr of constr * Univ.ContextSet.t
+ | IsConstr of constr * Univ.ContextSet.t option (* None if monomorphic *)
type 'a with_uid = {
obj : 'a;
uid : KerName.t;
}
-type raw_hint = constr * types * Univ.ContextSet.t * bool (* poly *)
+type raw_hint = constr * types * Univ.ContextSet.t option
type hint = {
hint_term : constr;
hint_type : types;
- hint_uctx : Univ.ContextSet.t;
+ hint_uctx : Univ.ContextSet.t option; (* None if monomorphic *)
hint_clnv : clausenv;
- hint_poly : bool;
- (** Is the hint polymorpic and hence should be refreshed at each application *)
}
type 'a with_metadata =
@@ -334,15 +332,19 @@ let strip_params env sigma c =
| _ -> c)
| _ -> c
+let merge_context_set_opt sigma ctx = match ctx with
+| None -> sigma
+| Some ctx -> Evd.merge_context_set Evd.univ_flexible sigma ctx
+
let instantiate_hint env sigma p =
- let mk_clenv (c, cty, ctx, poly) =
- let sigma = Evd.merge_context_set univ_flexible sigma ctx in
+ let mk_clenv (c, cty, ctx) =
+ let sigma = merge_context_set_opt 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_poly = poly }
+ { 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 (mk_clenv c)
@@ -816,7 +818,7 @@ let secvars_of_constr env sigma c =
let secvars_of_global env gr =
secvars_of_idset (vars_of_global env gr)
-let make_exact_entry env sigma info ~poly ?(name=PathAny) (c, cty, ctx) =
+let make_exact_entry env sigma info ?(name=PathAny) (c, cty, ctx) =
let secvars = secvars_of_constr env sigma c in
let cty = strip_outer_cast sigma cty in
match EConstr.kind sigma cty with
@@ -835,13 +837,13 @@ let make_exact_entry env sigma info ~poly ?(name=PathAny) (c, cty, ctx) =
(Some hd,
{ pri; pat = Some pat; name;
db = None; secvars;
- code = with_uid (Give_exact (c, cty, ctx, poly)); })
+ code = with_uid (Give_exact (c, cty, ctx)); })
-let make_apply_entry env sigma hnf info ~poly ?(name=PathAny) (c, cty, ctx) =
+let make_apply_entry env sigma hnf info ?(name=PathAny) (c, cty, ctx) =
let cty = if hnf then hnf_constr env sigma cty else cty in
match EConstr.kind sigma cty with
| Prod _ ->
- let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
+ let sigma' = merge_context_set_opt sigma ctx in
let ce = mk_clenv_from_env env sigma' None (c,cty) in
let c' = clenv_type (* ~reduce:false *) ce in
let hd =
@@ -861,49 +863,27 @@ let make_apply_entry env sigma hnf info ~poly ?(name=PathAny) (c, cty, ctx) =
{ pri; pat = Some pat; name;
db = None;
secvars;
- code = with_uid (Res_pf(c,cty,ctx,poly)); })
+ code = with_uid (Res_pf(c,cty,ctx)); })
else
(Some hd,
{ pri; pat = Some pat; name;
db = None; secvars;
- code = with_uid (ERes_pf(c,cty,ctx,poly)); })
+ code = with_uid (ERes_pf(c,cty,ctx)); })
| _ -> failwith "make_apply_entry"
(* flags is (e,h,v) with e=true if eapply and h=true if hnf and v=true if verbose
c is a constr
cty is the type of constr *)
-let pr_hint_term env sigma ctx = function
- | IsGlobRef gr -> pr_global gr
- | IsConstr (c, ctx) ->
- let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
- pr_econstr_env env sigma c
-
-let warn_polymorphic_hint =
- CWarnings.create ~name:"polymorphic-hint" ~category:"automation"
- (fun hint -> strbrk"Using polymorphic hint " ++ hint ++
- str" monomorphically" ++
- strbrk" use Polymorphic Hint to use it polymorphically.")
-
-let fresh_global_or_constr env sigma poly cr =
- let isgr, (c, ctx) =
- match cr with
- | IsGlobRef gr ->
- let (c, ctx) = UnivGen.fresh_global_instance env gr in
- true, (EConstr.of_constr c, ctx)
- | IsConstr (c, ctx) -> false, (c, ctx)
- in
- if poly then (c, ctx)
- else if Univ.ContextSet.is_empty ctx then (c, ctx)
- else begin
- if isgr then
- warn_polymorphic_hint (pr_hint_term env sigma ctx cr);
- DeclareUctx.declare_universe_context ~poly:false ctx;
- (c, Univ.ContextSet.empty)
- end
-
-let make_resolves env sigma (eapply, hnf) info ~check ~poly ?name cr =
- let c, ctx = fresh_global_or_constr env sigma poly cr in
+let fresh_global_or_constr env sigma cr = match cr with
+| IsGlobRef gr ->
+ let (c, ctx) = UnivGen.fresh_global_instance env gr in
+ let ctx = if Environ.is_polymorphic env gr then Some ctx else None in
+ (EConstr.of_constr c, ctx)
+| IsConstr (c, ctx) -> (c, ctx)
+
+let make_resolves env sigma (eapply, hnf) info ~check ?name cr =
+ let c, ctx = fresh_global_or_constr env sigma cr in
let cty = Retyping.get_type_of env sigma c in
let try_apply f =
try
@@ -914,8 +894,8 @@ let make_resolves env sigma (eapply, hnf) info ~check ~poly ?name cr =
with Failure _ -> None
in
let ents = List.map_filter try_apply
- [make_exact_entry env sigma info ~poly ?name;
- make_apply_entry env sigma hnf info ~poly ?name]
+ [make_exact_entry env sigma info ?name;
+ make_apply_entry env sigma hnf info ?name]
in
if check && List.is_empty ents then
user_err ~hdr:"Hint"
@@ -929,9 +909,9 @@ let make_resolve_hyp env sigma decl =
let hname = NamedDecl.get_id decl in
let c = mkVar hname in
try
- [make_apply_entry env sigma true empty_hint_info ~poly:false
+ [make_apply_entry env sigma true empty_hint_info
~name:(PathHints [GlobRef.VarRef hname])
- (c, NamedDecl.get_type decl, Univ.ContextSet.empty)]
+ (c, NamedDecl.get_type decl, None)]
with
| Failure _ -> []
| e when noncritical e -> anomaly (Pp.str "make_resolve_hyp.")
@@ -977,9 +957,9 @@ let make_mode ref m =
str" arguments while the mode declares " ++ int (Array.length m'))
else m'
-let make_trivial env sigma poly ?(name=PathAny) r =
- let c,ctx = fresh_global_or_constr env sigma poly r in
- let sigma = Evd.merge_context_set univ_flexible sigma ctx in
+let make_trivial env sigma ?(name=PathAny) r =
+ let c,ctx = fresh_global_or_constr env sigma r in
+ let sigma = merge_context_set_opt sigma ctx in
let t = hnf_constr env sigma (Retyping.get_type_of env sigma c) in
let hd = head_constr sigma t in
let ce = mk_clenv_from_env env sigma None (c,t) in
@@ -989,7 +969,7 @@ let make_trivial env sigma poly ?(name=PathAny) r =
name = name;
db = None;
secvars = secvars_of_constr env sigma c;
- code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx,poly)) })
+ code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) })
@@ -1102,10 +1082,10 @@ let subst_autohint (subst, obj) =
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 subst_aux ((c, t, ctx) 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)
+ if c==c' && t'==t then h else (c', t', ctx)
in
let subst_hint (k,data as hint) =
let k' = Option.Smart.map subst_key k in
@@ -1214,13 +1194,13 @@ let add_resolves env sigma clist ~local ~superglobal dbnames =
List.iter
(fun dbname ->
let r =
- List.flatten (List.map (fun (pri, poly, hnf, path, gr) ->
+ List.flatten (List.map (fun (pri, hnf, path, gr) ->
make_resolves env sigma (true, hnf)
- pri ~check:true ~poly ~name:path gr) clist)
+ pri ~check:true ~name:path gr) clist)
in
let check (_, hint) = match hint.code.obj with
- | ERes_pf (c, cty, ctx, _) ->
- let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
+ | ERes_pf (c, cty, ctx) ->
+ let sigma' = merge_context_set_opt sigma ctx in
let ce = mk_clenv_from_env env sigma' None (c,cty) in
let miss = clenv_missing ce in
let nmiss = List.length miss in
@@ -1288,7 +1268,7 @@ let add_externs info tacast ~local ~superglobal dbnames =
let add_trivials env sigma l ~local ~superglobal dbnames =
List.iter
(fun dbname ->
- let l = List.map (fun (name, poly, c) -> make_trivial env sigma poly ~name c) l in
+ let l = List.map (fun (name, c) -> make_trivial env sigma ~name c) l in
let hint = make_hint ~local dbname (AddHints { superglobal; hints = l }) in
Lib.add_anonymous_leaf (inAutoHint hint))
dbnames
@@ -1298,8 +1278,8 @@ type hnf = bool
type nonrec hint_info = hint_info
type hints_entry =
- | HintsResolveEntry of (hint_info * bool * hnf * hints_path_atom * hint_term) list
- | HintsImmediateEntry of (hints_path_atom * bool * hint_term) list
+ | HintsResolveEntry of (hint_info * hnf * hints_path_atom * hint_term) list
+ | HintsImmediateEntry of (hints_path_atom * hint_term) list
| HintsCutEntry of hints_path
| HintsUnfoldEntry of evaluable_global_reference list
| HintsTransparencyEntry of evaluable_global_reference hints_transparency_target * bool
@@ -1372,24 +1352,21 @@ let expand_constructor_hints env sigma lems =
match EConstr.kind sigma lem with
| Ind (ind,u) ->
List.init (nconstructors env ind)
- (fun i ->
- let ctx = Univ.ContextSet.diff (Evd.universe_context_set evd)
- (Evd.universe_context_set sigma) in
- not (Univ.ContextSet.is_empty ctx),
- IsConstr (mkConstructU ((ind,i+1),u),ctx))
+ (fun i -> IsGlobRef (GlobRef.ConstructRef ((ind,i+1))))
| _ ->
let (c, ctx) = prepare_hint false env sigma (evd,lem) in
- [not (Univ.ContextSet.is_empty ctx), IsConstr (c, ctx)]) lems
+ let ctx = if Univ.ContextSet.is_empty ctx then None else Some ctx in
+ [IsConstr (c, ctx)]) lems
(* builds a hint database from a constr signature *)
(* typically used with (lid, ltyp) = pf_hyps_types <some goal> *)
let constructor_hints env sigma eapply lems =
let lems = expand_constructor_hints env sigma lems in
- List.map_append (fun (poly, lem) ->
- make_resolves env sigma (eapply, true) empty_hint_info ~check:true ~poly lem) lems
+ List.map_append (fun lem ->
+ make_resolves env sigma (eapply, true) empty_hint_info ~check:true lem) lems
-let make_resolves env sigma info ~check ~poly ?name hint =
- make_resolves env sigma (true, false) info ~check ~poly ?name hint
+let make_resolves env sigma info ~check ?name hint =
+ make_resolves env sigma (true, false) info ~check ?name hint
let make_local_hint_db env sigma ts eapply lems =
let map c = c env sigma in
@@ -1650,7 +1627,8 @@ let connect_hint_clenv h gl =
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 *)
- if h.hint_poly then
+ match h.hint_uctx with
+ | Some ctx ->
(* 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
@@ -1662,21 +1640,19 @@ let connect_hint_clenv h gl =
evd = Evd.map_metas emap evd;
env = Proofview.Goal.env gl;
}
- else
- let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
+ | None ->
{ clenv with evd = evd ; env = Proofview.Goal.env gl }
let fresh_hint env sigma h =
let { hint_term = c; hint_uctx = ctx } = h in
- if h.hint_poly then
+ match h.hint_uctx with
+ | None -> sigma, c
+ | Some ctx ->
(* Refresh the instance of the hint *)
let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
let c = Vars.subst_univs_level_constr subst c in
let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
sigma, c
- else
- let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
- sigma, c
let hint_res_pf ?with_evars ?with_classes ?flags h =
Proofview.Goal.enter begin fun gl ->
diff --git a/tactics/hints.mli b/tactics/hints.mli
index e061bd7648..dd22cff10b 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -42,9 +42,8 @@ type 'a hint_ast =
type hint = private {
hint_term : constr;
hint_type : types;
- hint_uctx : Univ.ContextSet.t;
+ hint_uctx : Univ.ContextSet.t option;
hint_clnv : clausenv;
- hint_poly : bool;
}
type 'a hints_path_atom_gen =
@@ -170,11 +169,11 @@ type hnf = bool
type hint_term =
| IsGlobRef of GlobRef.t
- | IsConstr of constr * Univ.ContextSet.t [@ocaml.deprecated "Declare a hint constant instead"]
+ | IsConstr of constr * Univ.ContextSet.t option [@ocaml.deprecated "Declare a hint constant instead"]
type hints_entry =
- | HintsResolveEntry of (hint_info * bool * hnf * hints_path_atom * hint_term) list
- | HintsImmediateEntry of (hints_path_atom * bool * hint_term) list
+ | HintsResolveEntry of (hint_info * hnf * hints_path_atom * hint_term) list
+ | HintsImmediateEntry of (hints_path_atom * hint_term) list
| HintsCutEntry of hints_path
| HintsUnfoldEntry of evaluable_global_reference list
| HintsTransparencyEntry of evaluable_global_reference hints_transparency_target * bool
@@ -211,7 +210,7 @@ val prepare_hint : bool (* Check no remaining evars *) ->
has missing arguments. *)
val make_resolves :
- env -> evar_map -> hint_info -> check:bool -> poly:bool -> ?name:hints_path_atom ->
+ env -> evar_map -> hint_info -> check:bool -> ?name:hints_path_atom ->
hint_term -> hint_entry list
(** [make_resolve_hyp hname htyp].
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:43:48 +0000