diff options
| -rw-r--r-- | dev/ci/user-overlays/12977-ppedrot-static-hint-poly.sh | 9 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 13 | ||||
| -rw-r--r-- | tactics/hints.ml | 134 | ||||
| -rw-r--r-- | tactics/hints.mli | 11 | ||||
| -rw-r--r-- | vernac/classes.ml | 11 | ||||
| -rw-r--r-- | vernac/comHints.ml | 16 |
6 files changed, 87 insertions, 107 deletions
diff --git a/dev/ci/user-overlays/12977-ppedrot-static-hint-poly.sh b/dev/ci/user-overlays/12977-ppedrot-static-hint-poly.sh new file mode 100644 index 0000000000..7bed43afe1 --- /dev/null +++ b/dev/ci/user-overlays/12977-ppedrot-static-hint-poly.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "12977" ] || [ "$CI_BRANCH" = "static-hint-poly" ]; then + + equations_CI_REF=static-hint-poly + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + + fiat_parsers_CI_REF=static-hint-poly + fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat + +fi 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]. diff --git a/vernac/classes.ml b/vernac/classes.ml index 02cb60f1cf..b38a249b73 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -41,11 +41,11 @@ let classes_transparent_state () = let () = Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state -let add_instance_hint inst path ~locality info poly = +let add_instance_hint inst path ~locality info = Flags.silently (fun () -> Hints.add_hints ~locality [typeclasses_db] (Hints.HintsResolveEntry - [info, poly, false, Hints.PathHints path, inst])) () + [info, false, Hints.PathHints path, inst])) () let is_local_for_hint i = match i.is_global with @@ -56,14 +56,13 @@ let is_local_for_hint i = itself *) let add_instance_base inst = - let poly = Global.is_polymorphic inst.is_impl in let locality = if is_local_for_hint inst then Goptions.OptLocal else Goptions.OptGlobal in add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] ~locality - inst.is_info poly; + inst.is_info; List.iter (fun (path, pri, c) -> - let h = Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty) [@ocaml.warning "-3"] in + let h = Hints.IsConstr (EConstr.of_constr c, None) [@ocaml.warning "-3"] in add_instance_hint h path - ~locality pri poly) + ~locality pri) (build_subclasses ~check:(not (isVarRef inst.is_impl)) (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info) diff --git a/vernac/comHints.ml b/vernac/comHints.ml index 051560fb63..9eac558908 100644 --- a/vernac/comHints.ml +++ b/vernac/comHints.ml @@ -62,7 +62,7 @@ let project_hint ~poly pri l2r r = cb in let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in - (info, false, true, Hints.PathAny, Hints.IsGlobRef (GlobRef.ConstRef c)) + (info, true, Hints.PathAny, Hints.IsGlobRef (GlobRef.ConstRef c)) let warn_deprecated_hint_constr = CWarnings.create ~name:"fragile-hint-constr" ~category:"automation" @@ -89,10 +89,10 @@ let interp_hints ~poly h = let env = Global.env () in let sigma = Evd.from_env env in let c, diff = Hints.prepare_hint true env sigma (evd, c) in - if poly then (Hints.IsConstr (c, diff) [@ocaml.warning "-3"]) + if poly then (Hints.IsConstr (c, Some diff) [@ocaml.warning "-3"]) else let () = DeclareUctx.declare_universe_context ~poly:false diff in - (Hints.IsConstr (c, Univ.ContextSet.empty) [@ocaml.warning "-3"]) + (Hints.IsConstr (c, None) [@ocaml.warning "-3"]) in let fref r = let gr = Smartlocate.global_with_alias r in @@ -106,20 +106,20 @@ let interp_hints ~poly h = match c with | HintsReference c -> let gr = Smartlocate.global_with_alias c in - (PathHints [gr], poly, IsGlobRef gr) + (PathHints [gr], IsGlobRef gr) | HintsConstr c -> let () = warn_deprecated_hint_constr () in - (PathAny, poly, f poly c) + (PathAny, f poly c) in let fp = Constrintern.intern_constr_pattern env sigma in let fres (info, b, r) = - let path, poly, gr = fi r in + let path, gr = fi r in let info = { info with Typeclasses.hint_pattern = Option.map fp info.Typeclasses.hint_pattern } in - (info, poly, b, path, gr) + (info, b, path, gr) in let open Hints in let open Vernacexpr in @@ -140,7 +140,6 @@ let interp_hints ~poly h = | HintsConstructors lqid -> let constr_hints_of_ind qid = let ind = Smartlocate.global_inductive_with_alias qid in - let mib, _ = Global.lookup_inductive ind in Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (Libnames.string_of_qualid qid) "ind"; @@ -148,7 +147,6 @@ let interp_hints ~poly h = let c = (ind, i + 1) in let gr = GlobRef.ConstructRef c in ( empty_hint_info - , Declareops.inductive_is_polymorphic mib , true , PathHints [gr] , IsGlobRef gr )) |