diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 2 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 24 | ||||
| -rw-r--r-- | tactics/declare.ml | 35 | ||||
| -rw-r--r-- | tactics/declare.mli | 2 | ||||
| -rw-r--r-- | tactics/eauto.ml | 2 | ||||
| -rw-r--r-- | tactics/eauto.mli | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 77 | ||||
| -rw-r--r-- | tactics/equality.mli | 2 | ||||
| -rw-r--r-- | tactics/hipattern.ml | 1 |
9 files changed, 84 insertions, 63 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 499e7a63d7..67f49f0074 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -49,7 +49,7 @@ let auto_core_unif_flags_of st1 st2 = { check_applied_meta_types = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; - frozen_evars = Evar.Set.empty; + allowed_evars = AllowAll; restrict_conv_on_strict_subterms = false; (* Compat *) modulo_betaiota = false; modulo_eta = true; diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 05f40d0570..cf5c64c3ae 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -151,7 +151,7 @@ let pr_ev evs ev = open Auto open Unification -let auto_core_unif_flags st freeze = { +let auto_core_unif_flags st allowed_evars = { modulo_conv_on_closed_terms = Some st; use_metas_eagerly_in_conv_on_closed_terms = true; use_evars_eagerly_in_conv_on_closed_terms = false; @@ -160,14 +160,14 @@ let auto_core_unif_flags st freeze = { check_applied_meta_types = false; use_pattern_unification = true; use_meta_bound_pattern_unification = true; - frozen_evars = freeze; + allowed_evars; restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = true; modulo_eta = false; } -let auto_unif_flags freeze st = - let fl = auto_core_unif_flags st freeze in +let auto_unif_flags ?(allowed_evars = AllowAll) st = + let fl = auto_core_unif_flags st allowed_evars in { core_unify_flags = fl; merge_unify_flags = fl; subterm_unify_flags = fl; @@ -357,23 +357,25 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm let open Proofview.Notations in let prods, concl = EConstr.decompose_prod_assum sigma concl in let nprods = List.length prods in - let freeze = + let allowed_evars = try match hdc with | Some (hd,_) when only_classes -> let cl = Typeclasses.class_info env sigma hd in if cl.cl_strict then - Evarutil.undefined_evars_of_term sigma concl - else Evar.Set.empty - | _ -> Evar.Set.empty - with e when CErrors.noncritical e -> Evar.Set.empty + let undefined = lazy (Evarutil.undefined_evars_of_term sigma concl) in + let allowed evk = not (Evar.Set.mem evk (Lazy.force undefined)) in + AllowFun allowed + else AllowAll + | _ -> AllowAll + with e when CErrors.noncritical e -> AllowAll in let hint_of_db = hintmap_of sigma hdc secvars concl in let hintl = List.map_append (fun db -> let tacs = hint_of_db db in - let flags = auto_unif_flags freeze (Hint_db.transparent_state db) in + let flags = auto_unif_flags ~allowed_evars (Hint_db.transparent_state db) in List.map (fun x -> (flags, x)) tacs) (local_db::db_list) in @@ -1198,7 +1200,7 @@ let autoapply c i = let hintdb = try Hints.searchtable_map i with Not_found -> CErrors.user_err (Pp.str ("Unknown hint database " ^ i ^ ".")) in - let flags = auto_unif_flags Evar.Set.empty + let flags = auto_unif_flags (Hints.Hint_db.transparent_state hintdb) in let cty = Tacmach.New.pf_unsafe_type_of gl c in let ce = mk_clenv_from gl (c,cty) in diff --git a/tactics/declare.ml b/tactics/declare.ml index b8ba62a5e5..c280760e84 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -71,8 +71,7 @@ let load_constant i ((sp,kn), obj) = let cooking_info segment = let modlist = replacement_context () in - let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = segment in - let named_ctx = List.map fst hyps in + let { abstr_ctx = named_ctx; abstr_subst = subst; abstr_uctx = uctx } = segment in let abstract = (named_ctx, subst, uctx) in { Opaqueproof.modlist; abstract } @@ -244,11 +243,16 @@ let get_roles export eff = in List.map map export +let feedback_axiom () = Feedback.(feedback AddedAxiom) +let is_unsafe_typing_flags () = + let flags = Environ.typing_flags (Global.env()) in + not (flags.check_universes && flags.check_guarded && flags.check_positive) + let define_constant ~side_effect ~name cd = let open Proof_global in (* Logically define the constant and its subproofs, no libobject tampering *) let in_section = Lib.sections_are_opened () in - let export, decl = match cd with + let export, decl, unsafe = match cd with | DefinitionEntry de -> (* We deal with side effects *) if not de.proof_entry_opaque then @@ -258,19 +262,20 @@ let define_constant ~side_effect ~name cd = let export = get_roles export eff in let de = { de with proof_entry_body = Future.from_val (body, ()) } in let cd = Entries.DefinitionEntry (cast_proof_entry de) in - export, ConstantEntry (PureEntry, cd) + export, ConstantEntry (PureEntry, cd), false else let map (body, eff) = body, eff.Evd.seff_private in let body = Future.chain de.proof_entry_body map in let de = { de with proof_entry_body = body } in let de = cast_opaque_proof_entry de in - [], ConstantEntry (EffectEntry, Entries.OpaqueEntry de) + [], ConstantEntry (EffectEntry, Entries.OpaqueEntry de), false | ParameterEntry e -> - [], ConstantEntry (PureEntry, Entries.ParameterEntry e) + [], ConstantEntry (PureEntry, Entries.ParameterEntry e), not (Lib.is_modtype_strict()) | PrimitiveEntry e -> - [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e) + [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e), false in let kn, eff = Global.add_constant ~side_effect ~in_section name decl in + if unsafe || is_unsafe_typing_flags() then feedback_axiom(); kn, eff, export let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd = @@ -295,7 +300,7 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind (** Declaration of section variables and local definitions *) type variable_declaration = | SectionLocalDef of Evd.side_effects Proof_global.proof_entry - | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:bool } + | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind } (* This object is only for things which iterate over objects to find variables (only Prettyp.print_context AFAICT) *) @@ -308,12 +313,11 @@ let declare_variable ~name ~kind d = if Decls.variable_exists name then raise (AlreadyDeclared (None, name)); - let impl,opaque,poly,univs = match d with (* Fails if not well-typed *) + let impl,opaque,poly = match d with (* Fails if not well-typed *) | SectionLocalAssum {typ;univs;poly;impl} -> let () = declare_universe_context ~poly univs in let () = Global.push_named_assum (name,typ) in - let impl = if impl then Decl_kinds.Implicit else Decl_kinds.Explicit in - impl, true, poly, univs + impl, true, poly | SectionLocalDef (de) -> (* The body should already have been forced upstream because it is a section-local definition, but it's not enforced by typing *) @@ -337,14 +341,14 @@ let declare_variable ~name ~kind d = secdef_type = de.proof_entry_type; } in let () = Global.push_named_def (name, se) in - Decl_kinds.Explicit, de.proof_entry_opaque, - poly, univs + Glob_term.Explicit, de.proof_entry_opaque, + poly in Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name); - add_section_variable ~name ~kind:impl ~poly univs; + add_section_variable ~name ~poly; Decls.(add_variable_data name {opaque;kind}); add_anonymous_leaf (inVariable ()); - Impargs.declare_var_implicits name; + Impargs.declare_var_implicits ~impl name; Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name) (** Declaration of inductive blocks *) @@ -490,6 +494,7 @@ let declare_mind mie = | ind::_ -> ind.mind_entry_typename | [] -> CErrors.anomaly (Pp.str "cannot declare an empty list of inductives.") in let (sp,kn as oname) = add_leaf id (inInductive mie) in + if is_unsafe_typing_flags() then feedback_axiom(); let mind = Global.mind_of_delta_kn kn in let isprim = declare_projections mie.mind_entry_universes mind in Impargs.declare_mib_implicits mind; diff --git a/tactics/declare.mli b/tactics/declare.mli index 89b41076f7..4ae9f6c7ae 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -23,7 +23,7 @@ open Entries type variable_declaration = | SectionLocalDef of Evd.side_effects Proof_global.proof_entry - | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:bool } + | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind } type 'a constant_entry = | DefinitionEntry of 'a Proof_global.proof_entry diff --git a/tactics/eauto.ml b/tactics/eauto.ml index cc3e78f3b8..d4e4322bef 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -408,7 +408,7 @@ let e_search_auto debug (in_depth,p) lems db_list gl = (* let e_search_auto = CProfile.profile5 e_search_auto_key e_search_auto *) let eauto_with_bases ?(debug=Off) np lems db_list = - Proofview.V82.of_tactic (Hints.wrap_hint_warning (Proofview.V82.tactic (tclTRY (e_search_auto debug np lems db_list)))) + Hints.wrap_hint_warning (Proofview.V82.tactic (tclTRY (e_search_auto debug np lems db_list))) let eauto ?(debug=Off) np lems dbnames = let db_list = make_db_list dbnames in diff --git a/tactics/eauto.mli b/tactics/eauto.mli index ec99baef45..f9347b7b0f 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -26,7 +26,7 @@ val gen_eauto : ?debug:debug -> bool * int -> delayed_open_constr list -> val eauto_with_bases : ?debug:debug -> bool * int -> - delayed_open_constr list -> hint_db list -> Proofview.V82.tac + delayed_open_constr list -> hint_db list -> unit Proofview.tactic val autounfold : hint_db_name list -> Locus.clause -> unit Proofview.tactic val autounfold_tac : hint_db_name list option -> Locus.clause -> unit Proofview.tactic diff --git a/tactics/equality.ml b/tactics/equality.ml index 7c90c59f61..220b9bc475 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -38,7 +38,6 @@ open Coqlib open Declarations open Indrec open Clenv -open Evd open Ind_tables open Eqschemes open Locus @@ -107,7 +106,7 @@ let rewrite_core_unif_flags = { check_applied_meta_types = true; use_pattern_unification = true; use_meta_bound_pattern_unification = true; - frozen_evars = Evar.Set.empty; + allowed_evars = AllowAll; restrict_conv_on_strict_subterms = false; modulo_betaiota = false; modulo_eta = true; @@ -126,16 +125,17 @@ let freeze_initial_evars sigma flags clause = (* We take evars of the type: this may include old evars! For excluding *) (* all old evars, including the ones occurring in the rewriting lemma, *) (* we would have to take the clenv_value *) - let newevars = Evarutil.undefined_evars_of_term sigma (clenv_type clause) in - let evars = - fold_undefined (fun evk _ evars -> - if Evar.Set.mem evk newevars then evars - else Evar.Set.add evk evars) - sigma Evar.Set.empty in + let newevars = lazy (Evarutil.undefined_evars_of_term sigma (clenv_type clause)) in + let initial = Evd.undefined_map sigma in + let allowed evk = + if Evar.Map.mem evk initial then false + else Evar.Set.mem evk (Lazy.force newevars) + in + let allowed_evars = AllowFun allowed in {flags with - core_unify_flags = {flags.core_unify_flags with frozen_evars = evars}; - merge_unify_flags = {flags.merge_unify_flags with frozen_evars = evars}; - subterm_unify_flags = {flags.subterm_unify_flags with frozen_evars = evars}} + core_unify_flags = {flags.core_unify_flags with allowed_evars}; + merge_unify_flags = {flags.merge_unify_flags with allowed_evars}; + subterm_unify_flags = {flags.subterm_unify_flags with allowed_evars}} let make_flags frzevars sigma flags clause = if frzevars then freeze_initial_evars sigma flags clause else flags @@ -188,8 +188,7 @@ let rewrite_conv_closed_core_unif_flags = { use_meta_bound_pattern_unification = true; - frozen_evars = Evar.Set.empty; - (* This is set dynamically *) + allowed_evars = AllowAll; restrict_conv_on_strict_subterms = false; modulo_betaiota = false; @@ -223,8 +222,7 @@ let rewrite_keyed_core_unif_flags = { use_meta_bound_pattern_unification = true; - frozen_evars = Evar.Set.empty; - (* This is set dynamically *) + allowed_evars = AllowAll; restrict_conv_on_strict_subterms = false; modulo_betaiota = true; @@ -334,6 +332,21 @@ let jmeq_same_dom env sigma = function | _, [dom1; _; dom2;_] -> is_conv env sigma dom1 dom2 | _ -> false +let eq_elimination_ref l2r sort = + let name = + if l2r then + match sort with + | InProp -> "core.eq.ind_r" + | InSProp -> "core.eq.sind_r" + | InSet | InType -> "core.eq.rect_r" + else + match sort with + | InProp -> "core.eq.ind" + | InSProp -> "core.eq.sind" + | InSet | InType -> "core.eq.rect" + in + if Coqlib.has_ref name then Some (Coqlib.lib_ref name) else None + (* find_elim determines which elimination principle is necessary to eliminate lbeq on sort_of_gl. *) @@ -345,35 +358,35 @@ let find_elim hdcncl lft2rgt dep cls ot = in let inccl = Option.is_empty cls in let env = Proofview.Goal.env gl in - (* if (is_global Coqlib.glob_eq hdcncl || *) - (* (is_global Coqlib.glob_jmeq hdcncl && *) - (* jmeq_same_dom env sigma ot)) && not dep *) - if (is_global_exists "core.eq.type" hdcncl || - (is_global_exists "core.JMeq.type" hdcncl - && jmeq_same_dom env sigma ot)) && not dep + let is_eq = is_global_exists "core.eq.type" hdcncl in + let is_jmeq = is_global_exists "core.JMeq.type" hdcncl && jmeq_same_dom env sigma ot in + if (is_eq || is_jmeq) && not dep then + let sort = elimination_sort_of_clause cls gl in let c = match EConstr.kind sigma hdcncl with | Ind (ind_sp,u) -> - let pr1 = - lookup_eliminator env ind_sp (elimination_sort_of_clause cls gl) - in begin match lft2rgt, cls with | Some true, None | Some false, Some _ -> - let c1 = destConstRef pr1 in - let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical c1)) in - let l' = Label.of_id (add_suffix (Label.to_id l) "_r") in - let c1' = Global.constant_of_delta_kn (KerName.make mp l') in - begin + begin match if is_eq then eq_elimination_ref true sort else None with + | Some r -> destConstRef r + | None -> + let c1 = destConstRef (lookup_eliminator env ind_sp sort) in + let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical c1)) in + let l' = Label.of_id (add_suffix (Label.to_id l) "_r") in + let c1' = Global.constant_of_delta_kn (KerName.make mp l') in try - let _ = Global.lookup_constant c1' in - c1' + let _ = Global.lookup_constant c1' in c1' with Not_found -> user_err ~hdr:"Equality.find_elim" (str "Cannot find rewrite principle " ++ Label.print l' ++ str ".") end - | _ -> destConstRef pr1 + | _ -> + begin match if is_eq then eq_elimination_ref false sort else None with + | Some r -> destConstRef r + | None -> destConstRef (lookup_eliminator env ind_sp sort) + end end | _ -> (* cannot occur since we checked that we are in presence of diff --git a/tactics/equality.mli b/tactics/equality.mli index f8166bba2d..8225195ca7 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -29,6 +29,8 @@ type conditions = | FirstSolved (* Use the first match whose side-conditions are solved *) | AllMatches (* Rewrite all matches whose side-conditions are solved *) +val eq_elimination_ref : orientation -> Sorts.family -> GlobRef.t option + val general_rewrite_bindings : orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag -> ?tac:(unit Proofview.tactic * conditions) -> constr with_bindings -> evars_flag -> unit Proofview.tactic diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index a3a88df21e..61e0e41eb9 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -258,7 +258,6 @@ type equation_kind = exception NoEquationFound open Glob_term -open Decl_kinds open Evar_kinds let mkPattern c = snd (Patternops.pattern_of_glob_constr c) |