diff options
Diffstat (limited to 'tactics/hints.ml')
-rw-r--r-- | tactics/hints.ml | 165 |
1 files changed, 109 insertions, 56 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index a285d6b93..d49c8aaa5 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -12,7 +12,7 @@ open Pp open Util open CErrors open Names -open Term +open Constr open Evd open EConstr open Vars @@ -23,17 +23,16 @@ open Libobject open Namegen open Libnames open Smartlocate -open Misctypes open Termops open Inductiveops open Typing open Decl_kinds +open Typeclasses open Pattern open Patternops open Clenv open Tacred open Printer -open Vernacexpr module NamedDecl = Context.Named.Declaration @@ -94,13 +93,14 @@ let secvars_of_hyps hyps = else pred let empty_hint_info = - let open Vernacexpr in { hint_priority = None; hint_pattern = None } (************************************************************************) (* The Type of Constructions Autotactic Hints *) (************************************************************************) +type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen + type 'a hint_ast = | Res_pf of 'a (* Hint Apply *) | ERes_pf of 'a (* Hint EApply *) @@ -115,7 +115,7 @@ type 'a hints_path_atom_gen = (* For forward hints, their names is the list of projections *) | PathAny -type hints_path_atom = global_reference hints_path_atom_gen +type hints_path_atom = GlobRef.t hints_path_atom_gen type 'a hints_path_gen = | PathAtom of 'a hints_path_atom_gen @@ -126,10 +126,10 @@ type 'a hints_path_gen = | PathEpsilon type pre_hints_path = Libnames.reference hints_path_gen -type hints_path = global_reference hints_path_gen +type hints_path = GlobRef.t hints_path_gen type hint_term = - | IsGlobRef of global_reference + | IsGlobRef of GlobRef.t | IsConstr of constr * Univ.ContextSet.t type 'a with_uid = { @@ -153,9 +153,28 @@ type 'a with_metadata = { type full_hint = hint with_metadata -type hint_entry = global_reference option * +type hint_entry = GlobRef.t option * raw_hint hint_ast with_uid with_metadata +type reference_or_constr = + | HintsReference of reference + | HintsConstr of Constrexpr.constr_expr + +type hint_mode = + | ModeInput (* No evars *) + | ModeNoHeadEvar (* No evar at the head *) + | ModeOutput (* Anything *) + +type hints_expr = + | HintsResolve of (hint_info_expr * bool * reference_or_constr) list + | HintsResolveIFF of bool * reference list * int option + | HintsImmediate of reference_or_constr list + | HintsUnfold of reference list + | HintsTransparency of reference list * bool + | HintsMode of reference * hint_mode list + | HintsConstructors of reference list + | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument + type import_level = [ `LAX | `WARN | `STRICT ] let warn_hint : import_level ref = ref `LAX @@ -276,15 +295,15 @@ let strip_params env sigma c = | App (f, args) -> (match EConstr.kind sigma f with | Const (p,_) -> - let cb = lookup_constant p env in - (match cb.Declarations.const_proj with - | Some pb -> - let n = pb.Declarations.proj_npars in - if Array.length args > n then - mkApp (mkProj (Projection.make p false, args.(n)), - Array.sub args (n+1) (Array.length args - (n + 1))) - else c - | None -> c) + let p = Projection.make p false in + (match lookup_projection p env with + | pb -> + let n = pb.Declarations.proj_npars in + if Array.length args > n then + mkApp (mkProj (p, args.(n)), + Array.sub args (n+1) (Array.length args - (n + 1))) + else c + | exception Not_found -> c) | _ -> c) | _ -> c @@ -308,7 +327,7 @@ let instantiate_hint env sigma p = { p with code = { p.code with obj = code } } let hints_path_atom_eq h1 h2 = match h1, h2 with -| PathHints l1, PathHints l2 -> List.equal eq_gr l1 l2 +| PathHints l1, PathHints l2 -> List.equal GlobRef.equal l1 l2 | PathAny, PathAny -> true | _ -> false @@ -365,7 +384,7 @@ let path_seq p p' = let rec path_derivate hp hint = let rec derivate_atoms hints hints' = match hints, hints' with - | gr :: grs, gr' :: grs' when eq_gr gr gr' -> derivate_atoms grs grs' + | gr :: grs, gr' :: grs' when GlobRef.equal gr gr' -> derivate_atoms grs grs' | [], [] -> PathEpsilon | [], hints -> PathEmpty | grs, [] -> PathAtom (PathHints grs) @@ -448,7 +467,7 @@ let subst_path_atom subst p = | PathAny -> p | PathHints grs -> let gr' gr = fst (subst_global subst gr) in - let grs' = List.smartmap gr' grs in + let grs' = List.Smart.map gr' grs in if grs' == grs then p else PathHints grs' let rec subst_hints_path subst hp = @@ -474,28 +493,28 @@ module Hint_db : sig type t val empty : ?name:hint_db_name -> transparent_state -> bool -> t -val find : global_reference -> t -> search_entry +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 -> global_reference -> 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 -> - (global_reference * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list val map_eauto : evar_map -> secvars:Id.Pred.t -> - (global_reference * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list val map_auto : evar_map -> secvars:Id.Pred.t -> - (global_reference * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list val add_one : env -> evar_map -> hint_entry -> t -> t val add_list : env -> evar_map -> hint_entry list -> t -> t -val remove_one : global_reference -> t -> t -val remove_list : global_reference list -> t -> t -val iter : (global_reference option -> hint_mode array list -> full_hint list -> unit) -> t -> unit +val remove_one : GlobRef.t -> t -> t +val remove_list : GlobRef.t list -> t -> t +val iter : (GlobRef.t option -> hint_mode array list -> full_hint list -> unit) -> t -> unit val use_dn : t -> bool val transparent_state : t -> transparent_state val set_transparent_state : t -> transparent_state -> t val add_cut : hints_path -> t -> t -val add_mode : global_reference -> hint_mode array -> t -> t +val add_mode : GlobRef.t -> hint_mode array -> t -> t val cut : t -> hints_path val unfolds : t -> Id.Set.t * Cset.t -val fold : (global_reference option -> hint_mode array list -> full_hint list -> 'a -> 'a) -> +val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) -> t -> 'a -> 'a end = @@ -510,7 +529,7 @@ struct hintdb_map : search_entry Constr_map.t; (* A list of unindexed entries starting with an unfoldable constant or with no associated pattern. *) - hintdb_nopat : (global_reference option * stored_data) list; + hintdb_nopat : (GlobRef.t option * stored_data) list; hintdb_name : string option; } @@ -654,7 +673,7 @@ struct let add_list env sigma l db = List.fold_left (fun db k -> add_one env sigma k db) db l - let remove_sdl p sdl = List.smartfilter p sdl + let remove_sdl p sdl = List.filter p sdl let remove_he st p se = let sl1' = remove_sdl p se.sentry_nopat in @@ -664,9 +683,9 @@ struct let remove_list grs db = let filter (_, h) = - match h.name with PathHints [gr] -> not (List.mem_f eq_gr gr grs) | _ -> true in + match h.name with PathHints [gr] -> not (List.mem_f GlobRef.equal gr grs) | _ -> true in let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in - let hintnopat = List.smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in + let hintnopat = List.filter (fun (ge, sd) -> filter sd) db.hintdb_nopat in { db with hintdb_map = hintmap; hintdb_nopat = hintnopat } let remove_one gr db = remove_list [gr] db @@ -792,7 +811,7 @@ let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) = match EConstr.kind sigma cty with | Prod _ -> failwith "make_exact_entry" | _ -> - let pat = Patternops.pattern_of_constr env sigma (EConstr.to_constr sigma cty) in + let pat = Patternops.pattern_of_constr env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma cty) in let hd = try head_pattern_bound pat with BoundPattern -> failwith "make_exact_entry" @@ -814,7 +833,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info poly ?(name=PathAny) (c let sigma' = Evd.merge_context_set univ_flexible sigma ctx in let ce = mk_clenv_from_env env sigma' None (c,cty) in let c' = clenv_type (* ~reduce:false *) ce in - let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma c') in + let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr ~abort_on_undefined_evars:false sigma c') in let hd = try head_pattern_bound pat with BoundPattern -> failwith "make_apply_entry" in @@ -876,7 +895,7 @@ let fresh_global_or_constr env sigma poly cr = let isgr, (c, ctx) = match cr with | IsGlobRef gr -> - let (c, ctx) = Universes.fresh_global_instance env gr in + let (c, ctx) = UnivGen.fresh_global_instance env gr in true, (EConstr.of_constr c, ctx) | IsConstr (c, ctx) -> false, (c, ctx) in @@ -1015,9 +1034,9 @@ type hint_action = | CreateDB of bool * transparent_state | AddTransparency of evaluable_global_reference list * bool | AddHints of hint_entry list - | RemoveHints of global_reference list + | RemoveHints of GlobRef.t list | AddCut of hints_path - | AddMode of global_reference * hint_mode array + | AddMode of GlobRef.t * hint_mode array let add_cut dbname path = let db = get_db dbname in @@ -1065,8 +1084,8 @@ let subst_autohint (subst, obj) = in if gr' == gr then gr else gr' in let subst_hint (k,data as hint) = - let k' = Option.smartmap subst_key k in - let pat' = Option.smartmap (subst_pattern subst) data.pat in + let k' = Option.Smart.map subst_key k in + let pat' = Option.Smart.map (subst_pattern 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) -> @@ -1104,13 +1123,13 @@ let subst_autohint (subst, obj) = let action = match obj.hint_action with | CreateDB _ -> obj.hint_action | AddTransparency (grs, b) -> - let grs' = List.smartmap (subst_evaluable_reference subst) grs in + let grs' = List.Smart.map (subst_evaluable_reference subst) grs in if grs == grs' then obj.hint_action else AddTransparency (grs', b) | AddHints hintlist -> - let hintlist' = List.smartmap subst_hint hintlist in + let hintlist' = List.Smart.map subst_hint hintlist in if hintlist' == hintlist then obj.hint_action else AddHints hintlist' | RemoveHints grs -> - let grs' = List.smartmap (subst_global_reference subst) grs in + let grs' = List.Smart.map (subst_global_reference subst) grs in if grs == grs' then obj.hint_action else RemoveHints grs' | AddCut path -> let path' = subst_hints_path subst path in @@ -1218,7 +1237,7 @@ let add_trivials env sigma l local dbnames = type hnf = bool -type hint_info = (patvar list * constr_pattern) hint_info_gen +type nonrec hint_info = hint_info type hints_entry = | HintsResolveEntry of (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list @@ -1226,7 +1245,7 @@ type hints_entry = | HintsCutEntry of hints_path | HintsUnfoldEntry of evaluable_global_reference list | HintsTransparencyEntry of evaluable_global_reference list * bool - | HintsModeEntry of global_reference * hint_mode list + | HintsModeEntry of GlobRef.t * hint_mode list | HintsExternEntry of hint_info * Genarg.glob_generic_argument let default_prepare_hint_ident = Id.of_string "H" @@ -1263,20 +1282,53 @@ let prepare_hint check (poly,local) env init (sigma,c) = subst := (evar,mkVar id)::!subst; mkNamedLambda id t (iter (replace_term sigma evar (mkVar id) c)) in let c' = iter c in - if check then Pretyping.check_evars (Global.env()) Evd.empty sigma c'; + let env = Global.env () in + let empty_sigma = Evd.from_env env in + if check then Pretyping.check_evars env empty_sigma sigma c'; let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in if poly then IsConstr (c', diff) else if local then IsConstr (c', diff) else (Lib.add_anonymous_leaf (input_context_set diff); IsConstr (c', Univ.ContextSet.empty)) +let project_hint ~poly pri l2r r = + let open EConstr in + let open Coqlib in + let gr = Smartlocate.global_with_alias r in + let env = Global.env() in + let sigma = Evd.from_env env in + let sigma, c = Evd.fresh_global env sigma gr in + let t = Retyping.get_type_of env sigma c in + let t = + Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in + let sign,ccl = decompose_prod_assum sigma t in + let (a,b) = match snd (decompose_app sigma ccl) with + | [a;b] -> (a,b) + | _ -> assert false in + let p = + if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in + let sigma, p = Evd.fresh_global env sigma p in + let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in + let c = it_mkLambda_or_LetIn + (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in + let id = + Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) + in + let ctx = Evd.const_univ_entry ~poly sigma in + let c = EConstr.to_constr sigma c in + let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in + let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in + (info,false,true,PathAny, IsGlobRef (Globnames.ConstRef c)) + let interp_hints poly = fun h -> let env = Global.env () in let sigma = Evd.from_env env in let f poly c = let evd,c = Constrintern.interp_open_constr env sigma c in - prepare_hint true (poly,false) (Global.env()) Evd.empty (evd,c) in + let env = Global.env () in + let sigma = Evd.from_env env in + prepare_hint true (poly,false) env sigma (evd,c) in let fref r = let gr = global_with_alias r in Dumpglob.add_glob ?loc:r.CAst.loc gr; @@ -1297,6 +1349,8 @@ let interp_hints poly = in match h with | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints) + | HintsResolveIFF (l2r, lc, n) -> + HintsResolveEntry (List.map (project_hint ~poly n l2r) lc) | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints) | HintsUnfold lhints -> HintsUnfoldEntry (List.map fr lhints) | HintsTransparency (lhints, b) -> @@ -1322,7 +1376,7 @@ let interp_hints poly = let _, tacexp = Genintern.generic_intern env tacexp in HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp) -let add_hints local dbnames0 h = +let add_hints ~local dbnames0 h = if String.List.mem "nocore" dbnames0 then user_err Pp.(str "The hint database \"nocore\" is meant to stay empty."); let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in @@ -1357,12 +1411,10 @@ let expand_constructor_hints env sigma lems = (* builds a hint database from a constr signature *) (* typically used with (lid, ltyp) = pf_hyps_types <some goal> *) -let add_hint_lemmas env sigma eapply lems hint_db = +let constructor_hints env sigma eapply lems = let lems = expand_constructor_hints env sigma lems in - let hintlist' = - List.map_append (fun (poly, lem) -> - make_resolves env sigma (eapply,true,false) empty_hint_info poly lem) lems in - Hint_db.add_list env sigma hintlist' hint_db + List.map_append (fun (poly, lem) -> + make_resolves env sigma (eapply,true,false) empty_hint_info poly lem) lems let make_local_hint_db env sigma ts eapply lems = let map c = c env sigma in @@ -1373,8 +1425,9 @@ let make_local_hint_db env sigma ts eapply lems = | Some ts -> ts in let hintlist = List.map_append (make_resolve_hyp env sigma) sign in - add_hint_lemmas env sigma eapply lems - (Hint_db.add_list env sigma hintlist (Hint_db.empty ts false)) + Hint_db.empty ts false + |> Hint_db.add_list env sigma hintlist + |> Hint_db.add_list env sigma (constructor_hints env sigma eapply lems) let make_local_hint_db env sigma ?ts eapply lems = make_local_hint_db env sigma ts eapply lems |