diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/abstract.ml | 57 | ||||
| -rw-r--r-- | tactics/declare.ml | 469 | ||||
| -rw-r--r-- | tactics/declare.mli | 203 | ||||
| -rw-r--r-- | tactics/hints.ml | 4 | ||||
| -rw-r--r-- | tactics/hints.mli | 2 | ||||
| -rw-r--r-- | tactics/pfedit.ml | 189 | ||||
| -rw-r--r-- | tactics/pfedit.mli | 94 | ||||
| -rw-r--r-- | tactics/proof_global.ml | 283 | ||||
| -rw-r--r-- | tactics/proof_global.mli | 98 | ||||
| -rw-r--r-- | tactics/tactics.mllib | 2 |
10 files changed, 613 insertions, 788 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/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/hints.ml b/tactics/hints.ml index f8a46fcb1d..ffb0e030db 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1163,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; } @@ -1562,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.") 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 c139594f13..0000000000 --- a/tactics/pfedit.ml +++ /dev/null @@ -1,189 +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 = - Goptions.declare_bool_option_and_ref - ~depr:false - ~key:["Solve";"Unification";"Constraints"] - ~value:true - -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 68de9c7a00..0000000000 --- a/tactics/proof_global.ml +++ /dev/null @@ -1,283 +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 = - 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 *) -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/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 |