diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/abstract.ml | 57 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 97 | ||||
| -rw-r--r-- | tactics/class_tactics.mli | 2 | ||||
| -rw-r--r-- | tactics/declare.ml | 469 | ||||
| -rw-r--r-- | tactics/declare.mli | 203 | ||||
| -rw-r--r-- | tactics/eauto.ml | 48 | ||||
| -rw-r--r-- | tactics/hints.ml | 53 | ||||
| -rw-r--r-- | tactics/hints.mli | 2 | ||||
| -rw-r--r-- | tactics/pfedit.ml | 193 | ||||
| -rw-r--r-- | tactics/pfedit.mli | 94 | ||||
| -rw-r--r-- | tactics/proof_global.ml | 288 | ||||
| -rw-r--r-- | tactics/proof_global.mli | 98 | ||||
| -rw-r--r-- | tactics/redexpr.ml | 15 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.mllib | 2 |
15 files changed, 709 insertions, 914 deletions
diff --git a/tactics/abstract.ml b/tactics/abstract.ml index e85d94cd72..0e78a03f45 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -11,7 +11,6 @@ open Util open Termops open EConstr -open Evarutil module NamedDecl = Context.Named.Declaration @@ -76,61 +75,9 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = | None -> Proofview.Goal.concl gl | Some ty -> ty in let concl = it_mkNamedProd_or_LetIn concl sign in - let concl = - try flush_and_check_evars sigma concl - with Uninstantiated_evar _ -> - CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials.") in - - let sigma, ctx, concl = - (* FIXME: should be done only if the tactic succeeds *) - let sigma = Evd.minimize_universes sigma in - let ctx = Evd.universe_context_set sigma in - sigma, ctx, Evarutil.nf_evars_universes sigma concl - in - let concl = EConstr.of_constr concl in let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in - let ectx = Evd.evar_universe_context sigma in - let (const, safe, ectx) = - try Pfedit.build_constant_by_tactic ~name ~opaque:Proof_global.Transparent ~poly ~uctx:ectx ~sign:secsign concl solve_tac - with Logic_monad.TacticFailure e as src -> - (* if the tactic [tac] fails, it reports a [TacticFailure e], - which is an error irrelevant to the proof system (in fact it - means that [e] comes from [tac] failing to yield enough - success). Hence it reraises [e]. *) - let (_, info) = Exninfo.capture src in - Exninfo.iraise (e, info) - in - let body, effs = Future.force const.Declare.proof_entry_body in - (* We drop the side-effects from the entry, they already exist in the ambient environment *) - let const = Declare.Internal.map_entry_body const ~f:(fun _ -> body, ()) in - (* EJGA: Hack related to the above call to - `build_constant_by_tactic` with `~opaque:Transparent`. Even if - the abstracted term is destined to be opaque, if we trigger the - `if poly && opaque && private_poly_univs ()` in `Proof_global` - kernel will boom. This deserves more investigation. *) - let const = Declare.Internal.set_opacity ~opaque const in - let const, args = Declare.Internal.shrink_entry sign const in - let args = List.map EConstr.of_constr args in - let cst () = - (* do not compute the implicit arguments, it may be costly *) - let () = Impargs.make_implicit_args false in - (* ppedrot: seems legit to have abstracted subproofs as local*) - Declare.declare_private_constant ~local:Declare.ImportNeedQualified ~name ~kind const - in - let cst, eff = Impargs.with_implicit_protection cst () in - let inst = match const.Declare.proof_entry_universes with - | Entries.Monomorphic_entry _ -> EInstance.empty - | Entries.Polymorphic_entry (_, ctx) -> - (* We mimic what the kernel does, that is ensuring that no additional - constraints appear in the body of polymorphic constants. Ideally this - should be enforced statically. *) - let (_, body_uctx), _ = Future.force const.Declare.proof_entry_body in - let () = assert (Univ.ContextSet.is_empty body_uctx) in - EInstance.make (Univ.UContext.instance ctx) - in - let lem = mkConstU (cst, inst) in - let sigma = Evd.set_universe_context sigma ectx in - let effs = Evd.concat_side_effects eff effs in + let effs, sigma, lem, args, safe = + Declare.declare_abstract ~name ~poly ~sign ~secsign ~kind ~opaque ~solve_tac sigma concl in let solve = Proofview.tclEFFECTS effs <*> tacK lem args diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 182493baf9..a51fc8b347 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -38,33 +38,48 @@ let typeclasses_db = "typeclass_instances" (** Options handling *) let typeclasses_debug = ref 0 -let typeclasses_depth = ref None + +let typeclasses_depth_opt_name = ["Typeclasses";"Depth"] +let get_typeclasses_depth = + Goptions.declare_intopt_option_and_ref + ~depr:false + ~key:typeclasses_depth_opt_name + +let set_typeclasses_depth = + Goptions.set_int_option_value typeclasses_depth_opt_name (** When this flag is enabled, the resolution of type classes tries to avoid useless introductions. This is no longer useful since we have eta, but is here for compatibility purposes. Another compatibility issues is that the cost (in terms of search depth) can differ. *) -let typeclasses_limit_intros = ref true -let set_typeclasses_limit_intros d = (:=) typeclasses_limit_intros d -let get_typeclasses_limit_intros () = !typeclasses_limit_intros - -let typeclasses_dependency_order = ref false -let set_typeclasses_dependency_order d = (:=) typeclasses_dependency_order d -let get_typeclasses_dependency_order () = !typeclasses_dependency_order - -let typeclasses_iterative_deepening = ref false -let set_typeclasses_iterative_deepening d = (:=) typeclasses_iterative_deepening d -let get_typeclasses_iterative_deepening () = !typeclasses_iterative_deepening +let get_typeclasses_limit_intros = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Typeclasses";"Limit";"Intros"] + ~value:true + +let get_typeclasses_dependency_order = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Typeclasses";"Dependency";"Order"] + ~value:false + +let iterative_deepening_opt_name = ["Typeclasses";"Iterative";"Deepening"] +let get_typeclasses_iterative_deepening = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:iterative_deepening_opt_name + ~value:false (** [typeclasses_filtered_unif] governs the unification algorithm used by type classes. If enabled, a new algorithm based on pattern filtering and refine will be used. When disabled, the previous algorithm based on apply will be used. *) -let typeclasses_filtered_unification = ref false -let set_typeclasses_filtered_unification d = - (:=) typeclasses_filtered_unification d -let get_typeclasses_filtered_unification () = - !typeclasses_filtered_unification +let get_typeclasses_filtered_unification = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Typeclasses";"Filtered";"Unification"] + ~value:false let set_typeclasses_debug d = (:=) typeclasses_debug (if d then 1 else 0) let get_typeclasses_debug () = if !typeclasses_debug > 0 then true else false @@ -75,40 +90,8 @@ let set_typeclasses_verbose = let get_typeclasses_verbose () = if !typeclasses_debug = 0 then None else Some !typeclasses_debug -let set_typeclasses_depth d = (:=) typeclasses_depth d -let get_typeclasses_depth () = !typeclasses_depth - -open Goptions - -let () = - declare_bool_option - { optdepr = false; - optkey = ["Typeclasses";"Limit";"Intros"]; - optread = get_typeclasses_limit_intros; - optwrite = set_typeclasses_limit_intros; } - -let () = - declare_bool_option - { optdepr = false; - optkey = ["Typeclasses";"Dependency";"Order"]; - optread = get_typeclasses_dependency_order; - optwrite = set_typeclasses_dependency_order; } - -let () = - declare_bool_option - { optdepr = false; - optkey = ["Typeclasses";"Iterative";"Deepening"]; - optread = get_typeclasses_iterative_deepening; - optwrite = set_typeclasses_iterative_deepening; } - -let () = - declare_bool_option - { optdepr = false; - optkey = ["Typeclasses";"Filtered";"Unification"]; - optread = get_typeclasses_filtered_unification; - optwrite = set_typeclasses_filtered_unification; } - let () = + let open Goptions in declare_bool_option { optdepr = false; optkey = ["Typeclasses";"Debug"]; @@ -116,24 +99,18 @@ let () = optwrite = set_typeclasses_debug; } let _ = + let open Goptions in declare_int_option { optdepr = false; optkey = ["Typeclasses";"Debug";"Verbosity"]; optread = get_typeclasses_verbose; optwrite = set_typeclasses_verbose; } -let () = - declare_int_option - { optdepr = false; - optkey = ["Typeclasses";"Depth"]; - optread = get_typeclasses_depth; - optwrite = set_typeclasses_depth; } - type search_strategy = Dfs | Bfs let set_typeclasses_strategy = function - | Dfs -> set_typeclasses_iterative_deepening false - | Bfs -> set_typeclasses_iterative_deepening true + | Dfs -> Goptions.set_bool_option_value iterative_deepening_opt_name false + | Bfs -> Goptions.set_bool_option_value iterative_deepening_opt_name true let pr_ev evs ev = Printer.pr_econstr_env (Goal.V82.env evs ev) evs (Goal.V82.concl evs ev) @@ -977,7 +954,7 @@ module Search = struct | None -> None (* This happens only because there's no evar having p *) | Some (goals, nongoals) -> let goalsl = - if !typeclasses_dependency_order then + if get_typeclasses_dependency_order () then top_sort evm goals else Evar.Set.elements goals in diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index e26338436d..b97b90d777 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -19,10 +19,8 @@ val catchable : exn -> bool [@@ocaml.deprecated "Use instead CErrors.noncritical, or the exact name of the exception that matters in the corresponding case."] val set_typeclasses_debug : bool -> unit -val get_typeclasses_debug : unit -> bool val set_typeclasses_depth : int option -> unit -val get_typeclasses_depth : unit -> int option type search_strategy = Dfs | Bfs diff --git a/tactics/declare.ml b/tactics/declare.ml index 324007930a..cce43e833e 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -13,11 +13,112 @@ open Pp open Util open Names -open Declarations -open Entries open Safe_typing -open Libobject -open Lib +module NamedDecl = Context.Named.Declaration + +type opacity_flag = Opaque | Transparent + +type t = + { endline_tactic : Genarg.glob_generic_argument option + ; section_vars : Id.Set.t option + ; proof : Proof.t + ; udecl: UState.universe_decl + (** Initial universe declarations *) + ; initial_euctx : UState.t + (** The initial universe context (for the statement) *) + } + +(*** Proof Global manipulation ***) + +let get_proof ps = ps.proof +let get_proof_name ps = (Proof.data ps.proof).Proof.name + +let get_initial_euctx ps = ps.initial_euctx + +let map_proof f p = { p with proof = f p.proof } +let map_fold_proof f p = let proof, res = f p.proof in { p with proof }, res + +let map_fold_proof_endline f ps = + let et = + match ps.endline_tactic with + | None -> Proofview.tclUNIT () + | Some tac -> + let open Geninterp in + let {Proof.poly} = Proof.data ps.proof in + let ist = { lfun = Id.Map.empty; poly; extra = TacStore.empty } in + let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in + let tac = Geninterp.interp tag ist tac in + Ftactic.run tac (fun _ -> Proofview.tclUNIT ()) + in + let (newpr,ret) = f et ps.proof in + let ps = { ps with proof = newpr } in + ps, ret + +let compact_the_proof pf = map_proof Proof.compact pf + +(* Sets the tactic to be used when a tactic line is closed with [...] *) +let set_endline_tactic tac ps = + { ps with endline_tactic = Some tac } + +(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of + name [name] with goals [goals] (a list of pairs of environment and + conclusion). The proof is started in the evar map [sigma] (which + can typically contain universe constraints), and with universe + bindings [udecl]. *) +let start_proof ~name ~udecl ~poly sigma goals = + let proof = Proof.start ~name ~poly sigma goals in + let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in + { proof + ; endline_tactic = None + ; section_vars = None + ; udecl + ; initial_euctx + } + +let start_dependent_proof ~name ~udecl ~poly goals = + let proof = Proof.dependent_start ~name ~poly goals in + let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in + { proof + ; endline_tactic = None + ; section_vars = None + ; udecl + ; initial_euctx + } + +let get_used_variables pf = pf.section_vars +let get_universe_decl pf = pf.udecl + +let set_used_variables ps l = + let open Context.Named.Declaration in + let env = Global.env () in + let ids = List.fold_right Id.Set.add l Id.Set.empty in + let ctx = Environ.keep_hyps env ids in + let ctx_set = + List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in + let vars_of = Environ.global_vars_set in + let aux env entry (ctx, all_safe as orig) = + match entry with + | LocalAssum ({Context.binder_name=x},_) -> + if Id.Set.mem x all_safe then orig + else (ctx, all_safe) + | LocalDef ({Context.binder_name=x},bo, ty) as decl -> + if Id.Set.mem x all_safe then orig else + let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in + if Id.Set.subset vars all_safe + then (decl :: ctx, Id.Set.add x all_safe) + else (ctx, all_safe) in + let ctx, _ = + Environ.fold_named_context aux env ~init:(ctx,ctx_set) in + if not (Option.is_empty ps.section_vars) then + CErrors.user_err Pp.(str "Used section variables can be declared only once"); + ctx, { ps with section_vars = Some (Context.Named.to_vars ctx) } + +let get_open_goals ps = + let Proof.{ goals; stack; shelf } = Proof.data ps.proof in + List.length goals + + List.fold_left (+) 0 + (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) + + List.length shelf (* object_kind , id *) exception AlreadyDeclared of (string option * Id.t) @@ -30,8 +131,6 @@ let _ = CErrors.register_handler (function | _ -> None) -module NamedDecl = Context.Named.Declaration - type import_status = ImportDefaultBehavior | ImportNeedQualified (** Monomorphic universes need to survive sections. *) @@ -78,10 +177,118 @@ type 'a proof_entry = { proof_entry_inline_code : bool; } +let default_univ_entry = Entries.Monomorphic_entry Univ.ContextSet.empty + +let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types + ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univsbody=Univ.ContextSet.empty) body = + { proof_entry_body = Future.from_val ?fix_exn ((body,univsbody), eff); + proof_entry_secctx = section_vars; + proof_entry_type = types; + proof_entry_universes = univs; + proof_entry_opaque = opaque; + proof_entry_feedback = feedback_id; + proof_entry_inline_code = inline} + +type proof_object = + { name : Names.Id.t + (* [name] only used in the STM *) + ; entries : Evd.side_effects proof_entry list + ; uctx: UState.t + } + +let private_poly_univs = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Private";"Polymorphic";"Universes"] + ~value:true + +(* XXX: This is still separate from close_proof below due to drop_pt in the STM *) +(* XXX: Unsafe_typ:true is needed by vio files, see bf0499bc507d5a39c3d5e3bf1f69191339270729 *) +let prepare_proof ~unsafe_typ { proof } = + let Proof.{name=pid;entry;poly} = Proof.data proof in + let initial_goals = Proofview.initial_goals entry in + let evd = Proof.return ~pid proof in + let eff = Evd.eval_side_effects evd in + let evd = Evd.minimize_universes evd in + let to_constr_body c = + match EConstr.to_constr_opt evd c with + | Some p -> p + | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain") + in + let to_constr_typ t = + if unsafe_typ then EConstr.Unsafe.to_constr t else to_constr_body t + in + (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate + side-effects... This may explain why one need to uniquize side-effects + thereafter... *) + (* EJGA: actually side-effects de-duplication and this codepath is + unrelated. Duplicated side-effects arise from incorrect scheme + generation code, the main bulk of it was mostly fixed by #9836 + but duplication can still happen because of rewriting schemes I + think; however the code below is mostly untested, the only + code-paths that generate several proof entries are derive and + equations and so far there is no code in the CI that will + actually call those and do a side-effect, TTBOMK *) + (* EJGA: likely the right solution is to attach side effects to the first constant only? *) + let proofs = List.map (fun (body, typ) -> (to_constr_body body, eff), to_constr_typ typ) initial_goals in + proofs, Evd.evar_universe_context evd + +let close_proof ~opaque ~keep_body_ucst_separate ps = + + let { section_vars; proof; udecl; initial_euctx } = ps in + let { Proof.name; poly } = Proof.data proof in + let unsafe_typ = keep_body_ucst_separate && not poly in + let elist, uctx = prepare_proof ~unsafe_typ ps in + let opaque = match opaque with Opaque -> true | Transparent -> false in + + let make_entry ((body, eff), typ) = + + let allow_deferred = + not poly && + (keep_body_ucst_separate + || not (Safe_typing.is_empty_private_constants eff.Evd.seff_private)) + in + let used_univs_body = Vars.universes_of_constr body in + let used_univs_typ = Vars.universes_of_constr typ in + let used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let utyp, ubody = + if allow_deferred then + let utyp = UState.univ_entry ~poly initial_euctx in + let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in + (* For vi2vo compilation proofs are computed now but we need to + complement the univ constraints of the typ with the ones of + the body. So we keep the two sets distinct. *) + let uctx_body = UState.restrict uctx used_univs in + let ubody = UState.check_mono_univ_decl uctx_body udecl in + utyp, ubody + else if poly && opaque && private_poly_univs () then + let universes = UState.restrict uctx used_univs in + let typus = UState.restrict universes used_univs_typ in + let utyp = UState.check_univ_decl ~poly typus udecl in + let ubody = Univ.ContextSet.diff + (UState.context_set universes) + (UState.context_set typus) + in + utyp, ubody + else + (* Since the proof is computed now, we can simply have 1 set of + constraints in which we merge the ones for the body and the ones + for the typ. We recheck the declaration after restricting with + the actually used universes. + TODO: check if restrict is really necessary now. *) + let ctx = UState.restrict uctx used_univs in + let utyp = UState.check_univ_decl ~poly ctx udecl in + utyp, Univ.ContextSet.empty + in + definition_entry ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body + in + let entries = CList.map make_entry elist in + { name; entries; uctx } + type 'a constant_entry = | DefinitionEntry of 'a proof_entry - | ParameterEntry of parameter_entry - | PrimitiveEntry of primitive_entry + | ParameterEntry of Entries.parameter_entry + | PrimitiveEntry of Entries.primitive_entry (* At load-time, the segment starting from the module name to the discharge *) (* section (if Remark or Fact) is needed to access a construction *) @@ -93,13 +300,14 @@ let load_constant i ((sp,kn), obj) = Dumpglob.add_constant_kind con obj.cst_kind (* Opening means making the name without its module qualification available *) -let open_constant i ((sp,kn), obj) = +let open_constant f i ((sp,kn), obj) = (* Never open a local definition *) match obj.cst_locl with | ImportNeedQualified -> () | ImportDefaultBehavior -> let con = Global.constant_of_delta_kn kn in - Nametab.push (Nametab.Exactly i) sp (GlobRef.ConstRef con) + if Libobject.in_filter_ref (GlobRef.ConstRef con) f then + Nametab.push (Nametab.Exactly i) sp (GlobRef.ConstRef con) let exists_name id = Decls.variable_exists id || Global.exists_objlabel (Label.of_id id) @@ -129,9 +337,10 @@ let dummy_constant cst = { cst_locl = cst.cst_locl; } -let classify_constant cst = Substitute (dummy_constant cst) +let classify_constant cst = Libobject.Substitute (dummy_constant cst) let (objConstant : constant_obj Libobject.Dyn.tag) = + let open Libobject in declare_object_full { (default_object "CONSTANT") with cache_function = cache_constant; load_function = load_constant; @@ -152,7 +361,7 @@ let register_constant kn kind local = cst_locl = local; } in let id = Label.to_id (Constant.label kn) in - let _ = add_leaf id o in + let _ = Lib.add_leaf id o in update_tables kn let register_side_effect (c, role) = @@ -185,18 +394,6 @@ let record_aux env s_ty s_bo = (keep_hyps env s_bo)) in Aux_file.record_in_aux "context_used" v -let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty - -let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types - ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univsbody=Univ.ContextSet.empty) body = - { proof_entry_body = Future.from_val ?fix_exn ((body,univsbody), eff); - proof_entry_secctx = section_vars; - proof_entry_type = types; - proof_entry_universes = univs; - proof_entry_opaque = opaque; - proof_entry_feedback = feedback_id; - proof_entry_inline_code = inline} - let pure_definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types ?(univs=default_univ_entry) body = { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), ()); @@ -207,14 +404,14 @@ let pure_definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types proof_entry_feedback = None; proof_entry_inline_code = inline} -let delayed_definition_entry ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?(univs=default_univ_entry) ?types body = +let delayed_definition_entry ~opaque ?feedback_id ~section_vars ~univs ?types body = { proof_entry_body = body ; proof_entry_secctx = section_vars ; proof_entry_type = types ; proof_entry_universes = univs ; proof_entry_opaque = opaque ; proof_entry_feedback = feedback_id - ; proof_entry_inline_code = inline + ; proof_entry_inline_code = false } let cast_proof_entry e = @@ -222,14 +419,13 @@ let cast_proof_entry e = let univs = if Univ.ContextSet.is_empty ctx then e.proof_entry_universes else match e.proof_entry_universes with - | Monomorphic_entry ctx' -> + | Entries.Monomorphic_entry ctx' -> (* This can actually happen, try compiling EqdepFacts for instance *) - Monomorphic_entry (Univ.ContextSet.union ctx' ctx) - | Polymorphic_entry _ -> + Entries.Monomorphic_entry (Univ.ContextSet.union ctx' ctx) + | Entries.Polymorphic_entry _ -> CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition."); in - { - const_entry_body = body; + { Entries.const_entry_body = body; const_entry_secctx = e.proof_entry_secctx; const_entry_feedback = e.proof_entry_feedback; const_entry_type = e.proof_entry_type; @@ -241,7 +437,7 @@ type ('a, 'b) effect_entry = | EffectEntry : (private_constants, private_constants Entries.const_entry_body) effect_entry | PureEntry : (unit, Constr.constr) effect_entry -let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proof_entry) : b opaque_entry = +let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proof_entry) : b Entries.opaque_entry = let typ = match e.proof_entry_type with | None -> assert false | Some typ -> typ @@ -275,16 +471,16 @@ let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proo | PureEntry -> let (body, uctx), () = Future.force e.proof_entry_body in let univs = match e.proof_entry_universes with - | Monomorphic_entry uctx' -> Monomorphic_entry (Univ.ContextSet.union uctx uctx') - | Polymorphic_entry _ -> + | Entries.Monomorphic_entry uctx' -> + Entries.Monomorphic_entry (Univ.ContextSet.union uctx uctx') + | Entries.Polymorphic_entry _ -> assert (Univ.ContextSet.is_empty uctx); e.proof_entry_universes in body, univs | EffectEntry -> e.proof_entry_body, e.proof_entry_universes in - { - opaque_entry_body = body; + { Entries.opaque_entry_body = body; opaque_entry_secctx = secctx; opaque_entry_feedback = e.proof_entry_feedback; opaque_entry_type = typ; @@ -294,6 +490,7 @@ let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proo let feedback_axiom () = Feedback.(feedback AddedAxiom) let is_unsafe_typing_flags () = + let open Declarations in let flags = Environ.typing_flags (Global.env()) in not (flags.check_universes && flags.check_guarded && flags.check_positive) @@ -365,6 +562,7 @@ type variable_declaration = (* This object is only for things which iterate over objects to find variables (only Prettyp.print_context AFAICT) *) let objVariable : unit Libobject.Dyn.tag = + let open Libobject in declare_object_full { (default_object "VARIABLE") with classify_function = (fun () -> Dispose)} @@ -385,15 +583,15 @@ let declare_variable ~name ~kind d = let ((body, body_ui), eff) = Future.force de.proof_entry_body in let () = export_side_effects eff in let poly, entry_ui = match de.proof_entry_universes with - | Monomorphic_entry uctx -> false, uctx - | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx + | Entries.Monomorphic_entry uctx -> false, uctx + | Entries.Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx in let univs = Univ.ContextSet.union body_ui entry_ui in (* We must declare the universe constraints before type-checking the term. *) let () = declare_universe_context ~poly univs in let se = { - secdef_body = body; + Entries.secdef_body = body; secdef_secctx = de.proof_entry_secctx; secdef_feedback = de.proof_entry_feedback; secdef_type = de.proof_entry_type; @@ -403,7 +601,7 @@ let declare_variable ~name ~kind d = in Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name); Decls.(add_variable_data name {opaque;kind}); - ignore(add_leaf name (inVariable ()) : Libobject.object_name); + ignore(Lib.add_leaf name (inVariable ()) : Libobject.object_name); Impargs.declare_var_implicits ~impl name; Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name) @@ -510,3 +708,194 @@ module Internal = struct let objConstant = objConstant end +(*** Proof Global Environment ***) + +type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t + +let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.computation) = + let { section_vars; proof; udecl; initial_euctx } = ps in + let { Proof.name; poly; entry; sigma } = Proof.data proof in + + (* We don't allow poly = true in this path *) + if poly then + CErrors.anomaly (Pp.str "Cannot delay universe-polymorphic constants."); + + let fpl, uctx = Future.split2 fpl in + (* Because of dependent subgoals at the beginning of proofs, we could + have existential variables in the initial types of goals, we need to + normalise them for the kernel. *) + let subst_evar k = Evd.existential_opt_value0 sigma k in + let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar (UState.subst initial_euctx) in + + (* We only support opaque proofs, this will be enforced by using + different entries soon *) + let opaque = true in + let make_entry p (_, types) = + (* Already checked the univ_decl for the type universes when starting the proof. *) + let univs = UState.univ_entry ~poly:false initial_euctx in + let types = nf (EConstr.Unsafe.to_constr types) in + + Future.chain p (fun (pt,eff) -> + (* Deferred proof, we already checked the universe declaration with + the initial universes, ensure that the final universes respect + the declaration as well. If the declaration is non-extensible, + this will prevent the body from adding universes and constraints. *) + let uctx = Future.force uctx in + let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in + let used_univs = Univ.LSet.union + (Vars.universes_of_constr types) + (Vars.universes_of_constr pt) + in + let univs = UState.restrict uctx used_univs in + let univs = UState.check_mono_univ_decl univs udecl in + (pt,univs),eff) + |> delayed_definition_entry ~opaque ~feedback_id ~section_vars ~univs ~types + in + let entries = Future.map2 make_entry fpl (Proofview.initial_goals entry) in + { name; entries; uctx = initial_euctx } + +let close_future_proof = close_proof_delayed + +let return_partial_proof { proof } = + let proofs = Proof.partial_proof proof in + let Proof.{sigma=evd} = Proof.data proof in + let eff = Evd.eval_side_effects evd in + (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate + side-effects... This may explain why one need to uniquize side-effects + thereafter... *) + let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in + proofs, Evd.evar_universe_context evd + +let return_proof ps = + let p, uctx = prepare_proof ~unsafe_typ:false ps in + List.map fst p, uctx + +let update_global_env = + map_proof (fun p -> + let { Proof.sigma } = Proof.data p in + let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in + let p, (status,info), _ = Proof.run_tactic (Global.env ()) tac p in + p) + +let next = let n = ref 0 in fun () -> incr n; !n + +let by tac = map_fold_proof (Proof.solve (Goal_select.SelectNth 1) None tac) + +let build_constant_by_tactic ~name ?(opaque=Transparent) ~uctx ~sign ~poly typ tac = + let evd = Evd.from_ctx uctx in + let goals = [ (Global.env_of_context sign , typ) ] in + let pf = start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in + let pf, status = by tac pf in + let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false pf in + match entries with + | [entry] -> + entry, status, uctx + | _ -> + CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term") + +let build_by_tactic ?(side_eff=true) env ~uctx ~poly ~typ tac = + let name = Id.of_string ("temporary_proof"^string_of_int (next())) in + let sign = Environ.(val_of_named_context (named_context env)) in + let ce, status, univs = build_constant_by_tactic ~name ~uctx ~sign ~poly typ tac in + let cb, uctx = + if side_eff then inline_private_constants ~uctx env ce + else + (* GG: side effects won't get reset: no need to treat their universes specially *) + let (cb, ctx), _eff = Future.force ce.proof_entry_body in + cb, UState.merge ~sideff:false Evd.univ_rigid uctx ctx + in + cb, ce.proof_entry_type, status, univs + +let declare_abstract ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma concl = + (* EJGA: flush_and_check_evars is only used in abstract, could we + use a different API? *) + let concl = + try Evarutil.flush_and_check_evars sigma concl + with Evarutil.Uninstantiated_evar _ -> + CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials.") + in + let sigma, concl = + (* FIXME: should be done only if the tactic succeeds *) + let sigma = Evd.minimize_universes sigma in + sigma, Evarutil.nf_evars_universes sigma concl + in + let concl = EConstr.of_constr concl in + let uctx = Evd.evar_universe_context sigma in + let (const, safe, uctx) = + try build_constant_by_tactic ~name ~opaque:Transparent ~poly ~uctx ~sign:secsign concl solve_tac + with Logic_monad.TacticFailure e as src -> + (* if the tactic [tac] fails, it reports a [TacticFailure e], + which is an error irrelevant to the proof system (in fact it + means that [e] comes from [tac] failing to yield enough + success). Hence it reraises [e]. *) + let (_, info) = Exninfo.capture src in + Exninfo.iraise (e, info) + in + let sigma = Evd.set_universe_context sigma uctx in + let body, effs = Future.force const.proof_entry_body in + (* We drop the side-effects from the entry, they already exist in the ambient environment *) + let const = Internal.map_entry_body const ~f:(fun _ -> body, ()) in + (* EJGA: Hack related to the above call to + `build_constant_by_tactic` with `~opaque:Transparent`. Even if + the abstracted term is destined to be opaque, if we trigger the + `if poly && opaque && private_poly_univs ()` in `Proof_global` + kernel will boom. This deserves more investigation. *) + let const = Internal.set_opacity ~opaque const in + let const, args = Internal.shrink_entry sign const in + let cst () = + (* do not compute the implicit arguments, it may be costly *) + let () = Impargs.make_implicit_args false in + (* ppedrot: seems legit to have abstracted subproofs as local*) + declare_private_constant ~local:ImportNeedQualified ~name ~kind const + in + let cst, eff = Impargs.with_implicit_protection cst () in + let inst = match const.proof_entry_universes with + | Entries.Monomorphic_entry _ -> EConstr.EInstance.empty + | Entries.Polymorphic_entry (_, ctx) -> + (* We mimic what the kernel does, that is ensuring that no additional + constraints appear in the body of polymorphic constants. Ideally this + should be enforced statically. *) + let (_, body_uctx), _ = Future.force const.proof_entry_body in + let () = assert (Univ.ContextSet.is_empty body_uctx) in + EConstr.EInstance.make (Univ.UContext.instance ctx) + in + let args = List.map EConstr.of_constr args in + let lem = EConstr.mkConstU (cst, inst) in + let effs = Evd.concat_side_effects eff effs in + effs, sigma, lem, args, safe + +let get_goal_context pf i = + let p = get_proof pf in + Proof.get_goal_context_gen p i + +let get_current_goal_context pf = + let p = get_proof pf in + try Proof.get_goal_context_gen p 1 + with + | Proof.NoSuchGoal _ -> + (* spiwack: returning empty evar_map, since if there is no goal, + under focus, there is no accessible evar either. EJGA: this + seems strange, as we have pf *) + let env = Global.env () in + Evd.from_env env, env + +let get_current_context pf = + let p = get_proof pf in + Proof.get_proof_context p + +module Proof = struct + type nonrec t = t + let get_proof = get_proof + let get_proof_name = get_proof_name + let get_used_variables = get_used_variables + let get_universe_decl = get_universe_decl + let get_initial_euctx = get_initial_euctx + let map_proof = map_proof + let map_fold_proof = map_fold_proof + let map_fold_proof_endline = map_fold_proof_endline + let set_endline_tactic = set_endline_tactic + let set_used_variables = set_used_variables + let compact = compact_the_proof + let update_global_env = update_global_env + let get_open_goals = get_open_goals +end diff --git a/tactics/declare.mli b/tactics/declare.mli index 615cffeae7..1fabf80b2a 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -12,14 +12,92 @@ open Names open Constr open Entries -(** This module provides the official functions to declare new variables, - parameters, constants and inductive types. Using the following functions - will add the entries in the global environment (module [Global]), will - register the declarations in the library (module [Lib]) --- so that the - reset works properly --- and will fill some global tables such as - [Nametab] and [Impargs]. *) - -(** Proof entries *) +(** This module provides the official functions to declare new + variables, parameters, constants and inductive types in the global + environment. It also updates some accesory tables such as [Nametab] + (name resolution), [Impargs], and [Notations]. *) + +(** We provide two kind of fuctions: + + - one go functions, that will register a constant in one go, suited + for non-interactive definitions where the term is given. + + - two-phase [start/declare] functions which will create an + interactive proof, allow its modification, and saving when + complete. + + Internally, these functions mainly differ in that usually, the first + case doesn't require setting up the tactic engine. + + *) + +(** [Declare.Proof.t] Construction of constants using interactive proofs. *) +module Proof : sig + + type t + + (** XXX: These are internal and will go away from publis API once + lemmas is merged here *) + val get_proof : t -> Proof.t + val get_proof_name : t -> Names.Id.t + + (** XXX: These 3 are only used in lemmas *) + val get_used_variables : t -> Names.Id.Set.t option + val get_universe_decl : t -> UState.universe_decl + val get_initial_euctx : t -> UState.t + + val map_proof : (Proof.t -> Proof.t) -> t -> t + val map_fold_proof : (Proof.t -> Proof.t * 'a) -> t -> t * 'a + val map_fold_proof_endline : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a + + (** Sets the tactic to be used when a tactic line is closed with [...] *) + val set_endline_tactic : Genarg.glob_generic_argument -> t -> t + + (** Sets the section variables assumed by the proof, returns its closure + * (w.r.t. type dependencies and let-ins covered by it) *) + val set_used_variables : t -> + Names.Id.t list -> Constr.named_context * t + + val compact : t -> t + + (** Update the proofs global environment after a side-effecting command + (e.g. a sublemma definition) has been run inside it. Assumes + there_are_pending_proofs. *) + val update_global_env : t -> t + + val get_open_goals : t -> int + +end + +type opacity_flag = Opaque | Transparent + +(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of + name [name] with goals [goals] (a list of pairs of environment and + conclusion); [poly] determines if the proof is universe + polymorphic. The proof is started in the evar map [sigma] (which + can typically contain universe constraints), and with universe + bindings [udecl]. *) +val start_proof + : name:Names.Id.t + -> udecl:UState.universe_decl + -> poly:bool + -> Evd.evar_map + -> (Environ.env * EConstr.types) list + -> Proof.t + +(** Like [start_proof] except that there may be dependencies between + initial goals. *) +val start_dependent_proof + : name:Names.Id.t + -> udecl:UState.universe_decl + -> poly:bool + -> Proofview.telescope + -> Proof.t + +(** Proof entries represent a proof that has been finished, but still + not registered with the kernel. + + XXX: Scheduled for removal from public API, don't rely on it *) type 'a proof_entry = private { proof_entry_body : 'a Entries.const_entry_body; (* List of section variables *) @@ -32,12 +110,26 @@ type 'a proof_entry = private { proof_entry_inline_code : bool; } +(** XXX: Scheduled for removal from public API, don't rely on it *) +type proof_object = private + { name : Names.Id.t + (** name of the proof *) + ; entries : Evd.side_effects proof_entry list + (** list of the proof terms (in a form suitable for definitions). *) + ; uctx: UState.t + (** universe state *) + } + +val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Proof.t -> proof_object + (** Declaration of local constructions (Variable/Hypothesis/Local) *) +(** XXX: Scheduled for removal from public API, don't rely on it *) type variable_declaration = | SectionLocalDef of Evd.side_effects proof_entry | SectionLocalAssum of { typ:types; impl:Glob_term.binding_kind; } +(** XXX: Scheduled for removal from public API, don't rely on it *) type 'a constant_entry = | DefinitionEntry of 'a proof_entry | ParameterEntry of parameter_entry @@ -52,9 +144,9 @@ val declare_variable -> unit (** Declaration of global constructions - i.e. Definition/Theorem/Axiom/Parameter/... *) + i.e. Definition/Theorem/Axiom/Parameter/... -(* Default definition entries, transparent with no secctx or proj information *) + XXX: Scheduled for removal from public API, use `DeclareDef` instead *) val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool @@ -70,6 +162,7 @@ val definition_entry -> constr -> Evd.side_effects proof_entry +(** XXX: Scheduled for removal from public API, use `DeclareDef` instead *) val pure_definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool @@ -79,17 +172,6 @@ val pure_definition_entry -> constr -> unit proof_entry -(* Delayed definition entries *) -val delayed_definition_entry - : ?opaque:bool - -> ?inline:bool - -> ?feedback_id:Stateid.t - -> ?section_vars:Id.Set.t - -> ?univs:Entries.universes_entry - -> ?types:types - -> 'a Entries.const_entry_body - -> 'a proof_entry - type import_status = ImportDefaultBehavior | ImportNeedQualified (** [declare_constant id cd] declares a global declaration @@ -97,7 +179,9 @@ type import_status = ImportDefaultBehavior | ImportNeedQualified the full path of the declaration internal specify if the constant has been created by the kernel or by the - user, and in the former case, if its errors should be silent *) + user, and in the former case, if its errors should be silent + + XXX: Scheduled for removal from public API, use `DeclareDef` instead *) val declare_constant : ?local:import_status -> name:Id.t @@ -115,7 +199,9 @@ val declare_private_constant (** [inline_private_constants ~sideff ~uctx env ce] will inline the constants in [ce]'s body and return the body plus the updated - [UState.t]. *) + [UState.t]. + + XXX: Scheduled for removal from public API, don't rely on it *) val inline_private_constants : uctx:UState.t -> Environ.env @@ -124,10 +210,10 @@ val inline_private_constants (** Declaration messages *) +(** XXX: Scheduled for removal from public API, do not use *) val definition_message : Id.t -> unit val assumption_message : Id.t -> unit val fixpoint_message : int array option -> Id.t list -> unit -val cofixpoint_message : Id.t list -> unit val recursive_message : bool (** true = fixpoint *) -> int array option -> Id.t list -> unit @@ -157,3 +243,72 @@ module Internal : sig val objVariable : unit Libobject.Dyn.tag end + +(* Intermediate step necessary to delegate the future. + * Both access the current proof state. The former is supposed to be + * chained with a computation that completed the proof *) +type closed_proof_output + +(** Requires a complete proof. *) +val return_proof : Proof.t -> closed_proof_output + +(** An incomplete proof is allowed (no error), and a warn is given if + the proof is complete. *) +val return_partial_proof : Proof.t -> closed_proof_output +val close_future_proof : feedback_id:Stateid.t -> Proof.t -> closed_proof_output Future.computation -> proof_object + +(** [by tac] applies tactic [tac] to the 1st subgoal of the current + focused proof. + Returns [false] if an unsafe tactic has been used. *) +val by : unit Proofview.tactic -> Proof.t -> Proof.t * bool + +(** Declare abstract constant; will check no evars are possible; *) +val declare_abstract : + name:Names.Id.t + -> poly:bool + -> kind:Decls.logical_kind + -> sign:EConstr.named_context + -> secsign:Environ.named_context_val + -> opaque:bool + -> solve_tac:unit Proofview.tactic + -> Evd.evar_map + -> EConstr.t + -> Evd.side_effects * Evd.evar_map * EConstr.t * EConstr.t list * bool + +val build_by_tactic + : ?side_eff:bool + -> Environ.env + -> uctx:UState.t + -> poly:bool + -> typ:EConstr.types + -> unit Proofview.tactic + -> Constr.constr * Constr.types option * bool * UState.t + +(** {6 Helpers to obtain proof state when in an interactive proof } *) + +(** [get_goal_context n] returns the context of the [n]th subgoal of + the current focused proof or raises a [UserError] if there is no + focused proof or if there is no more subgoals *) + +val get_goal_context : Proof.t -> int -> Evd.evar_map * Environ.env + +(** [get_current_goal_context ()] works as [get_goal_context 1] *) +val get_current_goal_context : Proof.t -> Evd.evar_map * Environ.env + +(** [get_current_context ()] returns the context of the + current focused goal. If there is no focused goal but there + is a proof in progress, it returns the corresponding evar_map. + If there is no pending proof then it returns the current global + environment and empty evar_map. *) +val get_current_context : Proof.t -> Evd.evar_map * Environ.env + +(** Temporarily re-exported for 3rd party code; don't use *) +val build_constant_by_tactic : + name:Names.Id.t -> + ?opaque:opacity_flag -> + uctx:UState.t -> + sign:Environ.named_context_val -> + poly:bool -> + EConstr.types -> + unit Proofview.tactic -> + Evd.side_effects proof_entry * bool * UState.t diff --git a/tactics/eauto.ml b/tactics/eauto.ml index a89e5ef19a..28b5ed5811 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -430,29 +430,39 @@ let make_dimension n = function | None -> (true,make_depth n) | Some d -> (false,d) +let autounfolds ids csts gl cls = + let hyps = Tacmach.New.pf_ids_of_hyps gl in + let env = Tacmach.New.pf_env gl in + let ids = List.filter (fun id -> List.mem id hyps && Tacred.is_evaluable env (EvalVarRef id)) ids in + let csts = List.filter (fun cst -> Tacred.is_evaluable env (EvalConstRef cst)) csts in + let flags = + List.fold_left (fun flags cst -> CClosure.RedFlags.(red_add flags (fCONST cst))) + (List.fold_left (fun flags id -> CClosure.RedFlags.(red_add flags (fVAR id))) + CClosure.betaiotazeta ids) csts + in reduct_option ~check:false (Reductionops.clos_norm_flags flags, DEFAULTcast) cls + let cons a l = a :: l -let autounfolds db occs cls gl = - let unfolds = List.concat (List.map (fun dbname -> - let db = try searchtable_map dbname - with Not_found -> user_err ~hdr:"autounfold" (str "Unknown database " ++ str dbname) - in - let (ids, csts) = Hint_db.unfolds db in - let hyps = pf_ids_of_hyps gl in - let ids = Id.Set.filter (fun id -> List.mem id hyps) ids in - Cset.fold (fun cst -> cons (AllOccurrences, EvalConstRef cst)) csts - (Id.Set.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db) - in Proofview.V82.of_tactic (unfold_option unfolds cls) gl +exception UnknownDatabase of string let autounfold db cls = - Proofview.V82.tactic begin fun gl -> - let cls = concrete_clause_of (fun () -> pf_ids_of_hyps gl) cls in - let tac = autounfolds db in - tclMAP (function - | OnHyp (id,occs,where) -> tac occs (Some (id,where)) - | OnConcl occs -> tac occs None) - cls gl - end + if not (Locusops.clause_with_generic_occurrences cls) then + user_err ~hdr:"autounfold" (str "\"at\" clause not supported"); + match List.fold_left (fun (ids, csts) dbname -> + let db = try searchtable_map dbname + with Not_found -> raise (UnknownDatabase dbname) + in + let (db_ids, db_csts) = Hint_db.unfolds db in + (Id.Set.fold cons db_ids ids, Cset.fold cons db_csts csts)) ([], []) db + with + | (ids, csts) -> Proofview.Goal.enter begin fun gl -> + let cls = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cls in + let tac = autounfolds ids csts gl in + Tacticals.New.tclMAP (function + | OnHyp (id, _, where) -> tac (Some (id, where)) + | OnConcl _ -> tac None) cls + end + | exception UnknownDatabase dbname -> Tacticals.New.tclZEROMSG (str "Unknown database " ++ str dbname) let autounfold_tac db cls = Proofview.tclUNIT () >>= fun () -> diff --git a/tactics/hints.ml b/tactics/hints.ml index a907b9e783..ffb0e030db 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -188,27 +188,26 @@ type hints_expr = | 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 @@ -1164,7 +1163,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; } @@ -1563,7 +1562,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 pts = Declare.Proof.get_proof pf in let Proof.{goals;sigma} = Proof.data pts in match goals with | [] -> CErrors.user_err Pp.(str "No focused goal.") @@ -1690,12 +1689,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."))) diff --git a/tactics/hints.mli b/tactics/hints.mli index 9e11931247..eed0e37fac 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -306,7 +306,7 @@ val wrap_hint_warning_fun : env -> evar_map -> (** Printing hints *) val pr_searchtable : env -> evar_map -> Pp.t -val pr_applicable_hint : Proof_global.t -> Pp.t +val pr_applicable_hint : Declare.Proof.t -> Pp.t val pr_hint_ref : env -> evar_map -> GlobRef.t -> Pp.t val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml deleted file mode 100644 index 22d0ce5328..0000000000 --- a/tactics/pfedit.ml +++ /dev/null @@ -1,193 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Pp -open Util -open Names -open Environ -open Evd - -let use_unification_heuristics_ref = ref true -let () = Goptions.(declare_bool_option { - optdepr = false; - optkey = ["Solve";"Unification";"Constraints"]; - optread = (fun () -> !use_unification_heuristics_ref); - optwrite = (fun a -> use_unification_heuristics_ref:=a); -}) - -let use_unification_heuristics () = !use_unification_heuristics_ref - -exception NoSuchGoal -let () = CErrors.register_handler begin function - | NoSuchGoal -> Some Pp.(str "No such goal.") - | _ -> None -end - -let get_nth_V82_goal p i = - let Proof.{ sigma; goals } = Proof.data p in - try { it = List.nth goals (i-1) ; sigma } - with Failure _ -> raise NoSuchGoal - -let get_goal_context_gen pf i = - let { it=goal ; sigma=sigma; } = get_nth_V82_goal pf i in - (sigma, Refiner.pf_env { it=goal ; sigma=sigma; }) - -let get_goal_context pf i = - let p = Proof_global.get_proof pf in - get_goal_context_gen p i - -let get_current_goal_context pf = - let p = Proof_global.get_proof pf in - try get_goal_context_gen p 1 - with - | NoSuchGoal -> - (* spiwack: returning empty evar_map, since if there is no goal, - under focus, there is no accessible evar either. EJGA: this - seems strange, as we have pf *) - let env = Global.env () in - Evd.from_env env, env - -let get_proof_context p = - try get_goal_context_gen p 1 - with - | NoSuchGoal -> - (* No more focused goals *) - let { Proof.sigma } = Proof.data p in - sigma, Global.env () - -let get_current_context pf = - let p = Proof_global.get_proof pf in - get_proof_context p - -let solve ?with_end_tac gi info_lvl tac pr = - let tac = match with_end_tac with - | None -> tac - | Some etac -> Proofview.tclTHEN tac etac in - let tac = match info_lvl with - | None -> tac - | Some _ -> Proofview.Trace.record_info_trace tac - in - let nosuchgoal = Proofview.tclZERO (Proof_bullet.SuggestNoSuchGoals (1,pr)) in - let tac = let open Goal_select in match gi with - | SelectAlreadyFocused -> - let open Proofview.Notations in - Proofview.numgoals >>= fun n -> - if n == 1 then tac - else - let e = CErrors.UserError - (None, - Pp.(str "Expected a single focused goal but " ++ - int n ++ str " goals are focused.")) - in - Proofview.tclZERO e - - | SelectNth i -> Proofview.tclFOCUS ~nosuchgoal i i tac - | SelectList l -> Proofview.tclFOCUSLIST ~nosuchgoal l tac - | SelectId id -> Proofview.tclFOCUSID ~nosuchgoal id tac - | SelectAll -> tac - in - let tac = - if use_unification_heuristics () then - Proofview.tclTHEN tac Refine.solve_constraints - else tac - in - let env = Global.env () in - let (p,(status,info),()) = Proof.run_tactic env tac pr in - let env = Global.env () in - let sigma = Evd.from_env env in - let () = - match info_lvl with - | None -> () - | Some i -> Feedback.msg_info (hov 0 (Proofview.Trace.pr_info env sigma ~lvl:i info)) - in - (p,status) - -let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None tac) - -(**********************************************************************) -(* Shortcut to build a term using tactics *) - -let next = let n = ref 0 in fun () -> incr n; !n - -let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ~uctx ~sign ~poly typ tac = - let evd = Evd.from_ctx uctx in - let goals = [ (Global.env_of_context sign , typ) ] in - let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in - let pf, status = by tac pf in - let open Proof_global in - let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false pf in - match entries with - | [entry] -> - entry, status, uctx - | _ -> - CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term") - -let build_by_tactic ?(side_eff=true) env ~uctx ~poly ~typ tac = - let name = Id.of_string ("temporary_proof"^string_of_int (next())) in - let sign = val_of_named_context (named_context env) in - let ce, status, univs = build_constant_by_tactic ~name ~uctx ~sign ~poly typ tac in - let cb, uctx = - if side_eff then Declare.inline_private_constants ~uctx env ce - else - (* GG: side effects won't get reset: no need to treat their universes specially *) - let (cb, ctx), _eff = Future.force ce.Declare.proof_entry_body in - cb, UState.merge ~sideff:false Evd.univ_rigid uctx ctx - in - cb, ce.Declare.proof_entry_type, status, univs - -let refine_by_tactic ~name ~poly env sigma ty tac = - (* Save the initial side-effects to restore them afterwards. We set the - current set of side-effects to be empty so that we can retrieve the - ones created during the tactic invocation easily. *) - let eff = Evd.eval_side_effects sigma in - let sigma = Evd.drop_side_effects sigma in - (* Save the existing goals *) - let prev_future_goals = save_future_goals sigma in - (* Start a proof *) - let prf = Proof.start ~name ~poly sigma [env, ty] in - let (prf, _, ()) = - try Proof.run_tactic env tac prf - with Logic_monad.TacticFailure e as src -> - (* Catch the inner error of the monad tactic *) - let (_, info) = Exninfo.capture src in - Exninfo.iraise (e, info) - in - (* Plug back the retrieved sigma *) - let Proof.{ goals; stack; shelf; given_up; sigma; entry } = Proof.data prf in - assert (stack = []); - let ans = match Proofview.initial_goals entry with - | [c, _] -> c - | _ -> assert false - in - let ans = EConstr.to_constr ~abort_on_undefined_evars:false sigma ans in - (* [neff] contains the freshly generated side-effects *) - let neff = Evd.eval_side_effects sigma in - (* Reset the old side-effects *) - let sigma = Evd.drop_side_effects sigma in - let sigma = Evd.emit_side_effects eff sigma in - (* Restore former goals *) - let sigma = restore_future_goals sigma prev_future_goals in - (* Push remaining goals as future_goals which is the only way we - have to inform the caller that there are goals to collect while - not being encapsulated in the monad *) - (* Goals produced by tactic "shelve" *) - let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToShelve) shelf sigma in - (* Goals produced by tactic "give_up" *) - let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToGiveUp) given_up sigma in - (* Other goals *) - let sigma = List.fold_right Evd.declare_future_goal goals sigma in - (* Get rid of the fresh side-effects by internalizing them in the term - itself. Note that this is unsound, because the tactic may have solved - other goals that were already present during its invocation, so that - those goals rely on effects that are not present anymore. Hopefully, - this hack will work in most cases. *) - let neff = neff.Evd.seff_private in - let (ans, _) = Safe_typing.inline_private_constants env ((ans, Univ.ContextSet.empty), neff) in - ans, sigma diff --git a/tactics/pfedit.mli b/tactics/pfedit.mli deleted file mode 100644 index c49e997757..0000000000 --- a/tactics/pfedit.mli +++ /dev/null @@ -1,94 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** Global proof state. A quite redundant wrapper on {!Proof_global}. *) - -open Names -open Constr -open Environ - -(** {6 ... } *) - -exception NoSuchGoal - -(** [get_goal_context n] returns the context of the [n]th subgoal of - the current focused proof or raises a [UserError] if there is no - focused proof or if there is no more subgoals *) - -val get_goal_context : Proof_global.t -> int -> Evd.evar_map * env - -(** [get_current_goal_context ()] works as [get_goal_context 1] *) -val get_current_goal_context : Proof_global.t -> Evd.evar_map * env - -(** [get_proof_context ()] gets the goal context for the first subgoal - of the proof *) -val get_proof_context : Proof.t -> Evd.evar_map * env - -(** [get_current_context ()] returns the context of the - current focused goal. If there is no focused goal but there - is a proof in progress, it returns the corresponding evar_map. - If there is no pending proof then it returns the current global - environment and empty evar_map. *) -val get_current_context : Proof_global.t -> Evd.evar_map * env - -(** {6 ... } *) - -(** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th - subgoal of the current focused proof. [solve SelectAll - tac] applies [tac] to all subgoals. *) - -val solve : ?with_end_tac:unit Proofview.tactic -> - Goal_select.t -> int option -> unit Proofview.tactic -> - Proof.t -> Proof.t * bool - -(** [by tac] applies tactic [tac] to the 1st subgoal of the current - focused proof. - Returns [false] if an unsafe tactic has been used. *) - -val by : unit Proofview.tactic -> Proof_global.t -> Proof_global.t * bool - -(** Option telling if unification heuristics should be used. *) -val use_unification_heuristics : unit -> bool - -(** [build_by_tactic typ tac] returns a term of type [typ] by calling - [tac]. The return boolean, if [false] indicates the use of an unsafe - tactic. *) - -val build_constant_by_tactic - : name:Id.t - -> ?opaque:Proof_global.opacity_flag - -> uctx:UState.t - -> sign:named_context_val - -> poly:bool - -> EConstr.types - -> unit Proofview.tactic - -> Evd.side_effects Declare.proof_entry * bool * UState.t - -val build_by_tactic - : ?side_eff:bool - -> env - -> uctx:UState.t - -> poly:bool - -> typ:EConstr.types - -> unit Proofview.tactic - -> constr * types option * bool * UState.t - -val refine_by_tactic - : name:Id.t - -> poly:bool - -> env -> Evd.evar_map - -> EConstr.types - -> unit Proofview.tactic - -> constr * Evd.evar_map -(** A variant of the above function that handles open terms as well. - Caveat: all effects are purged in the returned term at the end, but other - evars solved by side-effects are NOT purged, so that unexpected failures may - occur. Ideally all code using this function should be rewritten in the - monad. *) diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml deleted file mode 100644 index d7dcc13e79..0000000000 --- a/tactics/proof_global.ml +++ /dev/null @@ -1,288 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Util -open Names -open Context - -module NamedDecl = Context.Named.Declaration - -(*** Proof Global Environment ***) - -type proof_object = - { name : Names.Id.t - (* [name] only used in the STM *) - ; entries : Evd.side_effects Declare.proof_entry list - ; uctx: UState.t - } - -type opacity_flag = Opaque | Transparent - -type t = - { endline_tactic : Genarg.glob_generic_argument option - ; section_vars : Id.Set.t option - ; proof : Proof.t - ; udecl: UState.universe_decl - (** Initial universe declarations *) - ; initial_euctx : UState.t - (** The initial universe context (for the statement) *) - } - -(*** Proof Global manipulation ***) - -let get_proof ps = ps.proof -let get_proof_name ps = (Proof.data ps.proof).Proof.name - -let get_initial_euctx ps = ps.initial_euctx - -let map_proof f p = { p with proof = f p.proof } -let map_fold_proof f p = let proof, res = f p.proof in { p with proof }, res - -let map_fold_proof_endline f ps = - let et = - match ps.endline_tactic with - | None -> Proofview.tclUNIT () - | Some tac -> - let open Geninterp in - let {Proof.poly} = Proof.data ps.proof in - let ist = { lfun = Id.Map.empty; poly; extra = TacStore.empty } in - let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in - let tac = Geninterp.interp tag ist tac in - Ftactic.run tac (fun _ -> Proofview.tclUNIT ()) - in - let (newpr,ret) = f et ps.proof in - let ps = { ps with proof = newpr } in - ps, ret - -let compact_the_proof pf = map_proof Proof.compact pf - -(* Sets the tactic to be used when a tactic line is closed with [...] *) -let set_endline_tactic tac ps = - { ps with endline_tactic = Some tac } - -(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of - name [name] with goals [goals] (a list of pairs of environment and - conclusion). The proof is started in the evar map [sigma] (which - can typically contain universe constraints), and with universe - bindings [udecl]. *) -let start_proof ~name ~udecl ~poly sigma goals = - let proof = Proof.start ~name ~poly sigma goals in - let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in - { proof - ; endline_tactic = None - ; section_vars = None - ; udecl - ; initial_euctx - } - -let start_dependent_proof ~name ~udecl ~poly goals = - let proof = Proof.dependent_start ~name ~poly goals in - let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in - { proof - ; endline_tactic = None - ; section_vars = None - ; udecl - ; initial_euctx - } - -let get_used_variables pf = pf.section_vars -let get_universe_decl pf = pf.udecl - -let set_used_variables ps l = - let open Context.Named.Declaration in - let env = Global.env () in - let ids = List.fold_right Id.Set.add l Id.Set.empty in - let ctx = Environ.keep_hyps env ids in - let ctx_set = - List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in - let vars_of = Environ.global_vars_set in - let aux env entry (ctx, all_safe as orig) = - match entry with - | LocalAssum ({binder_name=x},_) -> - if Id.Set.mem x all_safe then orig - else (ctx, all_safe) - | LocalDef ({binder_name=x},bo, ty) as decl -> - if Id.Set.mem x all_safe then orig else - let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in - if Id.Set.subset vars all_safe - then (decl :: ctx, Id.Set.add x all_safe) - else (ctx, all_safe) in - let ctx, _ = - Environ.fold_named_context aux env ~init:(ctx,ctx_set) in - if not (Option.is_empty ps.section_vars) then - CErrors.user_err Pp.(str "Used section variables can be declared only once"); - ctx, { ps with section_vars = Some (Context.Named.to_vars ctx) } - -let get_open_goals ps = - let Proof.{ goals; stack; shelf } = Proof.data ps.proof in - List.length goals + - List.fold_left (+) 0 - (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) + - List.length shelf - -type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t - -let private_poly_univs = - let b = ref true in - let _ = Goptions.(declare_bool_option { - optdepr = false; - optkey = ["Private";"Polymorphic";"Universes"]; - optread = (fun () -> !b); - optwrite = ((:=) b); - }) - in - fun () -> !b - -(* XXX: This is still separate from close_proof below due to drop_pt in the STM *) -let return_proof { proof } = - let Proof.{name=pid;entry} = Proof.data proof in - let initial_goals = Proofview.initial_goals entry in - let evd = Proof.return ~pid proof in - let eff = Evd.eval_side_effects evd in - let evd = Evd.minimize_universes evd in - let proof_opt c = - match EConstr.to_constr_opt evd c with - | Some p -> p - | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain") - in - (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate - side-effects... This may explain why one need to uniquize side-effects - thereafter... *) - (* EJGA: actually side-effects de-duplication and this codepath is - unrelated. Duplicated side-effects arise from incorrect scheme - generation code, the main bulk of it was mostly fixed by #9836 - but duplication can still happen because of rewriting schemes I - think; however the code below is mostly untested, the only - code-paths that generate several proof entries are derive and - equations and so far there is no code in the CI that will - actually call those and do a side-effect, TTBOMK *) - (* EJGA: likely the right solution is to attach side effects to the first constant only? *) - let proofs = List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in - proofs, Evd.evar_universe_context evd - -let close_proof ~opaque ~keep_body_ucst_separate ps = - let elist, uctx = return_proof ps in - let { section_vars; proof; udecl; initial_euctx } = ps in - let { Proof.name; poly; entry; sigma } = Proof.data proof in - let opaque = match opaque with Opaque -> true | Transparent -> false in - - (* Because of dependent subgoals at the beginning of proofs, we could - have existential variables in the initial types of goals, we need to - normalise them for the kernel. *) - let subst_evar k = Evd.existential_opt_value0 sigma k in - let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar (UState.subst uctx) in - - let make_entry (body, eff) (_, typ) = - let allow_deferred = - not poly && (keep_body_ucst_separate || - not (Safe_typing.empty_private_constants = eff.Evd.seff_private)) - in - (* EJGA: Why are we doing things this way? *) - let typ = EConstr.Unsafe.to_constr typ in - let typ = if allow_deferred then typ else nf typ in - (* EJGA: End "Why are we doing things this way?" *) - - let used_univs_body = Vars.universes_of_constr body in - let used_univs_typ = Vars.universes_of_constr typ in - let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let utyp, ubody = - if allow_deferred then - let utyp = UState.univ_entry ~poly initial_euctx in - let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in - (* For vi2vo compilation proofs are computed now but we need to - complement the univ constraints of the typ with the ones of - the body. So we keep the two sets distinct. *) - let uctx_body = UState.restrict uctx used_univs in - let ubody = UState.check_mono_univ_decl uctx_body udecl in - utyp, ubody - else if poly && opaque && private_poly_univs () then - let universes = UState.restrict uctx used_univs in - let typus = UState.restrict universes used_univs_typ in - let utyp = UState.check_univ_decl ~poly typus udecl in - let ubody = Univ.ContextSet.diff - (UState.context_set universes) - (UState.context_set typus) - in - utyp, ubody - else - (* Since the proof is computed now, we can simply have 1 set of - constraints in which we merge the ones for the body and the ones - for the typ. We recheck the declaration after restricting with - the actually used universes. - TODO: check if restrict is really necessary now. *) - let ctx = UState.restrict uctx used_univs in - let utyp = UState.check_univ_decl ~poly ctx udecl in - utyp, Univ.ContextSet.empty - in - Declare.definition_entry ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body - in - let entries = CList.map2 make_entry elist (Proofview.initial_goals entry) in - { name; entries; uctx } - -let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.computation) = - let { section_vars; proof; udecl; initial_euctx } = ps in - let { Proof.name; poly; entry; sigma } = Proof.data proof in - - (* We don't allow poly = true in this path *) - if poly then - CErrors.anomaly (Pp.str "Cannot delay universe-polymorphic constants."); - - let fpl, uctx = Future.split2 fpl in - (* Because of dependent subgoals at the beginning of proofs, we could - have existential variables in the initial types of goals, we need to - normalise them for the kernel. *) - let subst_evar k = Evd.existential_opt_value0 sigma k in - let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar (UState.subst initial_euctx) in - - (* We only support opaque proofs, this will be enforced by using - different entries soon *) - let opaque = true in - let make_entry p (_, types) = - (* Already checked the univ_decl for the type universes when starting the proof. *) - let univs = UState.univ_entry ~poly:false initial_euctx in - let types = nf (EConstr.Unsafe.to_constr types) in - - Future.chain p (fun (pt,eff) -> - (* Deferred proof, we already checked the universe declaration with - the initial universes, ensure that the final universes respect - the declaration as well. If the declaration is non-extensible, - this will prevent the body from adding universes and constraints. *) - let uctx = Future.force uctx in - let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in - let used_univs = Univ.LSet.union - (Vars.universes_of_constr types) - (Vars.universes_of_constr pt) - in - let univs = UState.restrict uctx used_univs in - let univs = UState.check_mono_univ_decl univs udecl in - (pt,univs),eff) - |> Declare.delayed_definition_entry ~opaque ~feedback_id ?section_vars ~univs ~types - in - let entries = Future.map2 make_entry fpl (Proofview.initial_goals entry) in - { name; entries; uctx = initial_euctx } - -let close_future_proof = close_proof_delayed - -let return_partial_proof { proof } = - let proofs = Proof.partial_proof proof in - let Proof.{sigma=evd} = Proof.data proof in - let eff = Evd.eval_side_effects evd in - (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate - side-effects... This may explain why one need to uniquize side-effects - thereafter... *) - let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in - proofs, Evd.evar_universe_context evd - -let update_global_env = - map_proof (fun p -> - let { Proof.sigma } = Proof.data p in - let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in - let p, (status,info), _ = Proof.run_tactic (Global.env ()) tac p in - p) diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli deleted file mode 100644 index 874708ded8..0000000000 --- a/tactics/proof_global.mli +++ /dev/null @@ -1,98 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** State for interactive proofs. *) - -type t - -(* Should be moved into a proper view *) -val get_proof : t -> Proof.t -val get_proof_name : t -> Names.Id.t -val get_used_variables : t -> Names.Id.Set.t option - -(** Get the universe declaration associated to the current proof. *) -val get_universe_decl : t -> UState.universe_decl - -(** Get initial universe state *) -val get_initial_euctx : t -> UState.t - -val compact_the_proof : t -> t - -(** When a proof is closed, it is reified into a [proof_object] *) -type proof_object = - { name : Names.Id.t - (** name of the proof *) - ; entries : Evd.side_effects Declare.proof_entry list - (** list of the proof terms (in a form suitable for definitions). *) - ; uctx: UState.t - (** universe state *) - } - -type opacity_flag = Opaque | Transparent - -(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of - name [name] with goals [goals] (a list of pairs of environment and - conclusion); [poly] determines if the proof is universe - polymorphic. The proof is started in the evar map [sigma] (which - can typically contain universe constraints), and with universe - bindings [udecl]. *) -val start_proof - : name:Names.Id.t - -> udecl:UState.universe_decl - -> poly:bool - -> Evd.evar_map - -> (Environ.env * EConstr.types) list - -> t - -(** Like [start_proof] except that there may be dependencies between - initial goals. *) -val start_dependent_proof - : name:Names.Id.t - -> udecl:UState.universe_decl - -> poly:bool - -> Proofview.telescope - -> t - -(** Update the proofs global environment after a side-effecting command - (e.g. a sublemma definition) has been run inside it. Assumes - there_are_pending_proofs. *) -val update_global_env : t -> t - -(* Takes a function to add to the exceptions data relative to the - state in which the proof was built *) -val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> t -> proof_object - -(* Intermediate step necessary to delegate the future. - * Both access the current proof state. The former is supposed to be - * chained with a computation that completed the proof *) - -type closed_proof_output - -(** Requires a complete proof. *) -val return_proof : t -> closed_proof_output - -(** An incomplete proof is allowed (no error), and a warn is given if - the proof is complete. *) -val return_partial_proof : t -> closed_proof_output -val close_future_proof : feedback_id:Stateid.t -> t -> closed_proof_output Future.computation -> proof_object - -val get_open_goals : t -> int - -val map_proof : (Proof.t -> Proof.t) -> t -> t -val map_fold_proof : (Proof.t -> Proof.t * 'a) -> t -> t * 'a -val map_fold_proof_endline : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a - -(** Sets the tactic to be used when a tactic line is closed with [...] *) -val set_endline_tactic : Genarg.glob_generic_argument -> t -> t - -(** Sets the section variables assumed by the proof, returns its closure - * (w.r.t. type dependencies and let-ins covered by it) *) -val set_used_variables : t -> - Names.Id.t list -> Constr.named_context * t diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index db09a2e69e..f681e4e99e 100644 --- a/tactics/redexpr.ml +++ b/tactics/redexpr.ml @@ -53,13 +53,8 @@ let whd_cbn flags env sigma t = let strong_cbn flags = strong_with_flags whd_cbn flags -let simplIsCbn = ref (false) -let () = Goptions.(declare_bool_option { - optdepr = false; - optkey = ["SimplIsCbn"]; - optread = (fun () -> !simplIsCbn); - optwrite = (fun a -> simplIsCbn:=a); -}) +let simplIsCbn = + Goptions.declare_bool_option_and_ref ~depr:false ~key:["SimplIsCbn"] ~value:false let set_strategy_one ref l = let k = @@ -228,10 +223,10 @@ let reduction_of_red_expr env = else (e_red red_product,DEFAULTcast) | Hnf -> (e_red hnf_constr,DEFAULTcast) | Simpl (f,o) -> - let whd_am = if !simplIsCbn then whd_cbn (make_flag f) else whd_simpl in - let am = if !simplIsCbn then strong_cbn (make_flag f) else simpl in + let whd_am = if simplIsCbn () then whd_cbn (make_flag f) else whd_simpl in + let am = if simplIsCbn () then strong_cbn (make_flag f) else simpl in let () = - if not (!simplIsCbn || List.is_empty f.rConst) then + if not (simplIsCbn () || List.is_empty f.rConst) then warn_simpl_unfolding_modifiers () in (contextualize (if head_style then whd_am else am) am o,DEFAULTcast) | Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 71eef1a135..0df4f5b207 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4499,7 +4499,7 @@ let check_expected_type env sigma (elimc,bl) elimt = if n == 0 then error "Scheme cannot be applied."; let sigma,cl = make_evar_clause env sigma ~len:(n - 1) elimt in let sigma = solve_evar_clause env sigma true cl bl in - let (_,u,_) = destProd sigma cl.cl_concl in + let (_,u,_) = destProd sigma (whd_all env sigma cl.cl_concl) in fun t -> match Evarconv.unify_leq_delay env sigma t u with | _sigma -> true | exception Evarconv.UnableToUnify _ -> false diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 0c4e496650..537d111f23 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -1,7 +1,5 @@ DeclareScheme Declare -Proof_global -Pfedit Dnet Dn Btermdn |