diff options
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 181 |
1 files changed, 27 insertions, 154 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index a907b9e783..5fb519cc4f 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -23,7 +23,6 @@ open Globnames open Libobject open Namegen open Libnames -open Smartlocate open Termops open Inductiveops open Typeclasses @@ -100,8 +99,6 @@ let empty_hint_info = (* 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 *) @@ -164,10 +161,6 @@ type full_hint = hint with_metadata type hint_entry = GlobRef.t option * raw_hint hint_ast with_uid with_metadata -type reference_or_constr = - | HintsReference of qualid - | HintsConstr of Constrexpr.constr_expr - type hint_mode = | ModeInput (* No evars *) | ModeNoHeadEvar (* No evar at the head *) @@ -178,37 +171,26 @@ type 'a hints_transparency_target = | HintsConstants | HintsReferences of 'a list -type hints_expr = - | HintsResolve of (hint_info_expr * bool * reference_or_constr) list - | HintsResolveIFF of bool * qualid list * int option - | HintsImmediate of reference_or_constr list - | HintsUnfold of qualid list - | HintsTransparency of qualid hints_transparency_target * bool - | HintsMode of qualid * hint_mode list - | HintsConstructors of qualid 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 -let read_warn_hint () = match !warn_hint with -| `LAX -> "Lax" -| `WARN -> "Warn" -| `STRICT -> "Strict" - -let write_warn_hint = function -| "Lax" -> warn_hint := `LAX -| "Warn" -> warn_hint := `WARN -| "Strict" -> warn_hint := `STRICT -| _ -> user_err Pp.(str "Only the following flags are accepted: Lax, Warn, Strict.") - -let () = - Goptions.(declare_string_option - { optdepr = false; - optkey = ["Loose"; "Hint"; "Behavior"]; - optread = read_warn_hint; - optwrite = write_warn_hint; - }) +type import_level = HintLax | HintWarn | HintStrict + +let warn_hint_to_string = function +| HintLax -> "Lax" +| HintWarn -> "Warn" +| HintStrict -> "Strict" + +let string_to_warn_hint = function +| "Lax" -> HintLax +| "Warn" -> HintWarn +| "Strict" -> HintStrict +| _ -> user_err Pp.(str "Only the following values are accepted: Lax, Warn, Strict.") + +let warn_hint = + Goptions.declare_interpreted_string_option_and_ref + ~depr:false + ~key:["Loose"; "Hint"; "Behavior"] + ~value:HintLax + string_to_warn_hint + warn_hint_to_string let fresh_key = let id = Summary.ref ~name:"HINT-COUNTER" 0 in @@ -896,7 +878,7 @@ let fresh_global_or_constr env sigma poly cr = else begin if isgr then warn_polymorphic_hint (pr_hint_term env sigma ctx cr); - Declare.declare_universe_context ~poly:false ctx; + DeclareUctx.declare_universe_context ~poly:false ctx; (c, Univ.ContextSet.empty) end @@ -1164,7 +1146,7 @@ let inAutoHint : hint_obj -> obj = declare_object {(default_object "AUTOHINT") with cache_function = cache_autohint; load_function = load_autohint; - open_function = open_autohint; + open_function = simple_open open_autohint; subst_function = subst_autohint; classify_function = classify_autohint; } @@ -1311,114 +1293,6 @@ let prepare_hint check env init (sigma,c) = let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in (c', diff) -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 (lib_ref "core.iff.type") 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 lib_ref "core.iff.proj1" else lib_ref "core.iff.proj2" 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 Sorts.Relevant (lift 1 b);mkArrow b Sorts.Relevant (lift 1 a);c|])) sign in - let name = - Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) - in - let ctx = Evd.univ_entry ~poly sigma in - let c = EConstr.to_constr sigma c in - let cb = Declare.(DefinitionEntry (definition_entry ~univs:ctx ~opaque:false c)) in - let c = Declare.declare_constant - ~local:Declare.ImportDefaultBehavior - ~name ~kind:Decls.(IsDefinition Definition) cb - in - let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in - (info,false,true,PathAny, IsGlobRef (GlobRef.ConstRef c)) - -let warn_deprecated_hint_constr = - CWarnings.create ~name:"deprecated-hint-constr" ~category:"deprecated" - (fun () -> - Pp.strbrk - "Declaring arbitrary terms as hints is deprecated; declare a global reference instead" - ) - -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 - let env = Global.env () in - let sigma = Evd.from_env env in - let (c, diff) = prepare_hint true env sigma (evd,c) in - if poly then IsConstr (c, diff) - else - let () = Declare.declare_universe_context ~poly:false diff in - IsConstr (c, Univ.ContextSet.empty) - in - let fref r = - let gr = global_with_alias r in - Dumpglob.add_glob ?loc:r.CAst.loc gr; - gr in - let fr r = evaluable_of_global_reference env (fref r) in - let fi c = - match c with - | HintsReference c -> - let gr = global_with_alias c in - (PathHints [gr], poly, IsGlobRef gr) - | HintsConstr c -> - let () = warn_deprecated_hint_constr () in - (PathAny, poly, 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 info = { info with hint_pattern = Option.map fp info.hint_pattern } in - (info, poly, b, path, gr) - in - let ft = function - | HintsVariables -> HintsVariables - | HintsConstants -> HintsConstants - | HintsReferences lhints -> HintsReferences (List.map fr lhints) - in - let fp = Constrintern.intern_constr_pattern (Global.env()) 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 (t, b) -> HintsTransparencyEntry (ft t, b) - | HintsMode (r, l) -> HintsModeEntry (fref r, l) - | HintsConstructors lqid -> - let constr_hints_of_ind qid = - let ind = global_inductive_with_alias qid in - let mib,_ = Global.lookup_inductive ind in - Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_qualid qid) "ind"; - List.init (nconstructors env ind) - (fun i -> 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) - in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid)) - | HintsExtern (pri, patcom, tacexp) -> - let pat = Option.map (fp sigma) patcom in - let l = match pat with None -> [] | Some (l, _) -> l in - let ltacvars = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in - let env = Genintern.({ (empty_glob_sign env) with ltacvars }) in - let _, tacexp = Genintern.generic_intern env tacexp in - HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp) - let add_hints ~locality dbnames h = let local, superglobal = match locality with | Goptions.OptDefault | Goptions.OptGlobal -> false, true @@ -1563,8 +1437,7 @@ let pr_hint_term env sigma cl = (* print all hints that apply to the concl of the current goal *) let pr_applicable_hint pf = let env = Global.env () in - let pts = Proof_global.get_proof pf in - let Proof.{goals;sigma} = Proof.data pts in + let Proof.{goals;sigma} = Proof.data pf in match goals with | [] -> CErrors.user_err Pp.(str "No focused goal.") | g::_ -> @@ -1690,12 +1563,12 @@ let wrap_hint_warning_fun env sigma t = in (ans, set_extra_data store sigma) -let run_hint tac k = match !warn_hint with -| `LAX -> k tac.obj -| `WARN -> +let run_hint tac k = match warn_hint () with +| HintLax -> k tac.obj +| HintWarn -> if is_imported tac then k tac.obj else Proofview.tclTHEN (log_hint tac) (k tac.obj) -| `STRICT -> +| HintStrict -> if is_imported tac then k tac.obj else Proofview.tclZERO (UserError (None, (str "Tactic failure."))) |