From c951e2ed88437c613bd4355b32547f9c39269eed Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 20 Aug 2019 00:02:28 +0200 Subject: [declare] Move proof_entry type to declare, put interactive proof data on top of declare. This PR is a follow up to #10406 , moving the then introduced `proof_entry` type to `Declare`. This makes sense as `Declare` is the main consumer of the entry type, and already provides the constructors for it. This is a step towards making the entry type private, which will allow us to enforce / handle invariants on entry data better. A side-effect of this PR is that now `Proof_global` does depend on `Declare`, not the other way around, but that makes sense given that closing an interactive proof will be a client of declare. Indeed, all `Declare` / `Pfedit` / and `Proof_global` are tied into tactics due to `abstract`, at some point we may be able to unify all them into a single file in `vernac`. --- .../10674-ejgallego-proofs+declare_unif.sh | 6 + plugins/funind/gen_principle.ml | 18 +- plugins/funind/indfun_common.ml | 2 +- plugins/funind/indfun_common.mli | 2 +- proofs/pfedit.ml | 195 ------------- proofs/pfedit.mli | 89 ------ proofs/proof_global.ml | 314 --------------------- proofs/proof_global.mli | 121 -------- proofs/proofs.mllib | 2 - tactics/abstract.ml | 10 +- tactics/abstract.mli | 4 +- tactics/declare.ml | 21 +- tactics/declare.mli | 19 +- tactics/ind_tables.ml | 2 +- tactics/pfedit.ml | 195 +++++++++++++ tactics/pfedit.mli | 89 ++++++ tactics/proof_global.ml | 303 ++++++++++++++++++++ tactics/proof_global.mli | 103 +++++++ tactics/tactics.mllib | 2 + vernac/comDefinition.ml | 4 +- vernac/comDefinition.mli | 2 +- vernac/declareDef.ml | 2 +- vernac/declareDef.mli | 4 +- vernac/declareObl.ml | 9 +- vernac/declareObl.mli | 2 +- vernac/indschemes.ml | 1 - vernac/lemmas.ml | 22 +- vernac/obligations.ml | 4 +- vernac/record.ml | 1 - 29 files changed, 771 insertions(+), 777 deletions(-) create mode 100644 dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh delete mode 100644 proofs/pfedit.ml delete mode 100644 proofs/pfedit.mli delete mode 100644 proofs/proof_global.ml delete mode 100644 proofs/proof_global.mli create mode 100644 tactics/pfedit.ml create mode 100644 tactics/pfedit.mli create mode 100644 tactics/proof_global.ml create mode 100644 tactics/proof_global.mli diff --git a/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh b/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh new file mode 100644 index 0000000000..6dc44aa627 --- /dev/null +++ b/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10674" ] || [ "$CI_BRANCH" = "proofs+declare_unif" ]; then + + equations_CI_REF=proofs+declare_unif + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 60717c6eec..352b21a15a 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -1170,7 +1170,7 @@ let get_funs_constant mp = in l_const -let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_effects Proof_global.proof_entry list = +let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_effects Declare.proof_entry list = let exception Found_type of int in let env = Global.env () in let funs = List.map fst fas in @@ -1244,7 +1244,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef | Some equation -> Declareops.is_opaque (Global.lookup_constant equation) in - let const = {const with Proof_global.proof_entry_opaque = opacity } in + let const = {const with Declare.proof_entry_opaque = opacity } in (* The others are just deduced *) if List.is_empty other_princ_types then @@ -1255,8 +1255,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef let sorts = Array.of_list sorts in List.map (Functional_principles_types.compute_new_princ_type_from_rel funs sorts) other_princ_types in - let open Proof_global in - let first_princ_body,first_princ_type = const.proof_entry_body, const.proof_entry_type in + let first_princ_body,first_princ_type = Declare.(const.proof_entry_body, const.proof_entry_type) in let ctxt,fix = Term.decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*) let (idxs,_),(_,ta,_ as decl) = Constr.destFix fix in let other_result = @@ -1299,10 +1298,10 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef let princ_body = Termops.it_mkLambda_or_LetIn (Constr.mkFix((idxs,i),decl)) ctxt in - {const with - proof_entry_body = - (Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects)); - proof_entry_type = Some scheme_type + { const with + Declare.proof_entry_body = + (Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects)); + proof_entry_type = Some scheme_type } ) other_fun_princ_types @@ -1358,7 +1357,8 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) = Array.of_list (List.map (fun entry -> - (EConstr.of_constr (fst (fst(Future.force entry.Proof_global.proof_entry_body))), EConstr.of_constr (Option.get entry.Proof_global.proof_entry_type )) + (EConstr.of_constr (fst (fst (Future.force entry.Declare.proof_entry_body))), + EConstr.of_constr (Option.get entry.Declare.proof_entry_type )) ) (make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs)) ) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 7719705138..ba37b9b461 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -115,7 +115,7 @@ open DeclareDef let definition_message = Declare.definition_message let save name const ?hook uctx scope kind = - let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in + let fix_exn = Future.fix_exn_of const.Declare.proof_entry_body in let r = match scope with | Discharge -> let c = SectionLocalDef const in diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 16beaaa3c7..34fb10bb67 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -44,7 +44,7 @@ val make_eq : unit -> EConstr.constr val save : Id.t - -> Evd.side_effects Proof_global.proof_entry + -> Evd.side_effects Declare.proof_entry -> ?hook:DeclareDef.Hook.t -> UState.t -> DeclareDef.locality diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml deleted file mode 100644 index 99a254652c..0000000000 --- a/proofs/pfedit.ml +++ /dev/null @@ -1,195 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* !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 -> CErrors.user_err Pp.(str "No such goal.") - | _ -> raise CErrors.Unhandled -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_current_context pf = - let p = Proof_global.get_proof pf in - try get_goal_context_gen p 1 - with - | NoSuchGoal -> - (* No more focused goals *) - let { Proof.sigma } = Proof.data p in - sigma, Global.env () - -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 ctx sign ~poly typ tac = - let evd = Evd.from_ctx ctx 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 - try - let pf, status = by tac pf in - let open Proof_global in - let { entries; universes } = close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in - match entries with - | [entry] -> - let univs = UState.demote_seff_univs entry.Proof_global.proof_entry_universes universes in - entry, status, univs - | _ -> - CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term") - with reraise -> - let reraise = CErrors.push reraise in - iraise reraise - -let build_by_tactic ?(side_eff=true) env sigma ~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 sigma sign ~poly typ tac in - let body, eff = Future.force ce.Proof_global.proof_entry_body in - let (cb, ctx) = - if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) - else body - in - let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in - cb, 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) = CErrors.push src in - 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/proofs/pfedit.mli b/proofs/pfedit.mli deleted file mode 100644 index 0626e40047..0000000000 --- a/proofs/pfedit.mli +++ /dev/null @@ -1,89 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* 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_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 - -> UState.t - -> named_context_val - -> poly:bool - -> EConstr.types - -> unit Proofview.tactic - -> Evd.side_effects Proof_global.proof_entry * bool * UState.t - -val build_by_tactic - : ?side_eff:bool - -> env - -> UState.t - -> poly:bool - -> EConstr.types - -> unit Proofview.tactic - -> constr * 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/proofs/proof_global.ml b/proofs/proof_global.ml deleted file mode 100644 index 851a3d1135..0000000000 --- a/proofs/proof_global.ml +++ /dev/null @@ -1,314 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* 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"); - (* EJGA: This is always empty thus we should modify the type *) - (ctx, []), { ps with section_vars = Some 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; - optname = "use private polymorphic universes for Qed constants"; - optkey = ["Private";"Polymorphic";"Universes"]; - optread = (fun () -> !b); - optwrite = ((:=) b); - }) - in - fun () -> !b - -let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now - (fpl : closed_proof_output Future.computation) ps = - let { section_vars; proof; udecl; initial_euctx } = ps in - let Proof.{ name; poly; entry } = Proof.data proof in - let opaque = match opaque with Opaque -> true | Transparent -> false in - let constrain_variables ctx = - UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx - in - let fpl, univs = Future.split2 fpl in - let universes = if poly || now then Future.force univs else initial_euctx 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 = - let { Proof.sigma } = Proof.data proof in - Evd.existential_opt_value0 sigma k in - let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar - (UState.subst universes) in - - let make_body = - if poly || now then - let make_body t (c, eff) = - let body = c in - let allow_deferred = - not poly && (keep_body_ucst_separate || - not (Safe_typing.empty_private_constants = eff.Evd.seff_private)) - in - let typ = if allow_deferred then t else nf t in - let used_univs_body = Vars.universes_of_constr body in - let used_univs_typ = Vars.universes_of_constr typ in - if allow_deferred then - let initunivs = UState.univ_entry ~poly initial_euctx in - let ctx = constrain_variables universes 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 used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let ctx_body = UState.restrict ctx used_univs in - let univs = UState.check_mono_univ_decl ctx_body udecl in - (initunivs, typ), ((body, univs), eff) - else if poly && opaque && private_poly_univs () then - let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let universes = UState.restrict universes used_univs in - let typus = UState.restrict universes used_univs_typ in - let udecl = UState.check_univ_decl ~poly typus udecl in - let ubody = Univ.ContextSet.diff - (UState.context_set universes) - (UState.context_set typus) - in - (udecl, typ), ((body, ubody), eff) - 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 used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let ctx = UState.restrict universes used_univs in - let univs = UState.check_univ_decl ~poly ctx udecl in - (univs, typ), ((body, Univ.ContextSet.empty), eff) - in - fun t p -> Future.split2 (Future.chain p (make_body t)) - else - fun t p -> - (* Already checked the univ_decl for the type universes when starting the proof. *) - let univctx = UState.univ_entry ~poly:false universes in - let t = nf t in - Future.from_val (univctx, t), - 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 univs = Future.force univs in - let univs = constrain_variables univs in - let used_univs = Univ.LSet.union - (Vars.universes_of_constr t) - (Vars.universes_of_constr pt) - in - let univs = UState.restrict univs used_univs in - let univs = UState.check_mono_univ_decl univs udecl in - (pt,univs),eff) - in - let entry_fn p (_, t) = - let t = EConstr.Unsafe.to_constr t in - let univstyp, body = make_body t p in - let univs, typ = Future.force univstyp in - { - proof_entry_body = body; - proof_entry_secctx = section_vars; - proof_entry_feedback = feedback_id; - proof_entry_type = Some typ; - proof_entry_inline_code = false; - proof_entry_opaque = opaque; - proof_entry_universes = univs; } - in - let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in - { name; entries = entries; poly; universes; udecl } - -let return_proof ?(allow_partial=false) ps = - let { proof } = ps in - if allow_partial then begin - 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 - end else - 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 *) - let proofs = - List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in - proofs, Evd.evar_universe_context evd - -let close_future_proof ~opaque ~feedback_id ps proof = - close_proof ~opaque ~keep_body_ucst_separate:true ~feedback_id ~now:false proof ps - -let close_proof ~opaque ~keep_body_ucst_separate fix_exn ps = - close_proof ~opaque ~keep_body_ucst_separate ~now:true - (Future.from_val ~fix_exn (return_proof ps)) ps - -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/proofs/proof_global.mli b/proofs/proof_global.mli deleted file mode 100644 index 54d5c2087a..0000000000 --- a/proofs/proof_global.mli +++ /dev/null @@ -1,121 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* Proof.t -val get_proof_name : t -> Names.Id.t -val get_used_variables : t -> Constr.named_context 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], where - [id] is the name of the proof, [entries] the list of the proof terms - (in a form suitable for definitions). Together with the [terminator] - function which takes a [proof_object] together with a [proof_end] - (i.e. an proof ending command) and registers the appropriate - values. *) -type 'a proof_entry = { - proof_entry_body : 'a Entries.const_entry_body; - (* List of section variables *) - proof_entry_secctx : Constr.named_context option; - (* State id on which the completion of type checking is reported *) - proof_entry_feedback : Stateid.t option; - proof_entry_type : Constr.types option; - proof_entry_universes : Entries.universes_entry; - proof_entry_opaque : bool; - proof_entry_inline_code : bool; -} - -(** 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 proof_entry list - (** list of the proof terms (in a form suitable for definitions). *) - ; poly : bool - (** polymorphic status *) - ; universes: UState.t - (** universe state *) - ; udecl : UState.universe_decl - (** universe declaration *) - } - -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 -> Future.fix_exn -> 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 = (Constr.t * Evd.side_effects) list * UState.t - -(* If allow_partial is set (default no) then an incomplete proof - * is allowed (no error), and a warn is given if the proof is complete. *) -val return_proof : ?allow_partial:bool -> t -> closed_proof_output -val close_future_proof : opaque:opacity_flag -> 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) + a list of - * ids to be cleared *) -val set_used_variables : t -> - Names.Id.t list -> (Constr.named_context * Names.lident list) * t diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 0ce726db25..756fef0511 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -6,9 +6,7 @@ Proof Logic Goal_select Proof_bullet -Proof_global Refiner Tacmach -Pfedit Clenv Clenvtac diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 09d7e0278a..edeb27ab88 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -69,7 +69,7 @@ let rec shrink ctx sign c t accu = | _ -> assert false let shrink_entry sign const = - let open Proof_global in + let open Declare in let typ = match const.proof_entry_type with | None -> assert false | Some t -> t @@ -151,7 +151,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = in let const, args = shrink_entry sign const in let args = List.map EConstr.of_constr args in - let cd = Declare.DefinitionEntry { const with Proof_global.proof_entry_opaque = opaque } in + let cd = Declare.DefinitionEntry { const with Declare.proof_entry_opaque = opaque } in let kind = if opaque then Decls.(IsProof Lemma) else Decls.(IsDefinition Definition) in let cst () = (* do not compute the implicit arguments, it may be costly *) @@ -160,20 +160,20 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = Declare.declare_private_constant ~local:Declare.ImportNeedQualified ~name ~kind cd in let cst, eff = Impargs.with_implicit_protection cst () in - let inst = match const.Proof_global.proof_entry_universes with + 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.Proof_global.proof_entry_body in + 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 evd = Evd.set_universe_context evd ectx in let effs = Evd.concat_side_effects eff - Proof_global.(snd (Future.force const.proof_entry_body)) in + (snd (Future.force const.Declare.proof_entry_body)) in let solve = Proofview.tclEFFECTS effs <*> tacK lem args diff --git a/tactics/abstract.mli b/tactics/abstract.mli index e278729f89..96ddbea7b2 100644 --- a/tactics/abstract.mli +++ b/tactics/abstract.mli @@ -26,5 +26,5 @@ val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit P save path *) val shrink_entry : ('a, 'b) Context.Named.Declaration.pt list - -> 'c Proof_global.proof_entry - -> 'c Proof_global.proof_entry * Constr.t list + -> 'c Declare.proof_entry + -> 'c Declare.proof_entry * Constr.t list diff --git a/tactics/declare.ml b/tactics/declare.ml index c280760e84..694bd6d1cd 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -55,8 +55,20 @@ type constant_obj = { cst_locl : import_status; } +type 'a proof_entry = { + proof_entry_body : 'a Entries.const_entry_body; + (* List of section variables *) + proof_entry_secctx : Constr.named_context option; + (* State id on which the completion of type checking is reported *) + proof_entry_feedback : Stateid.t option; + proof_entry_type : Constr.types option; + proof_entry_universes : Entries.universes_entry; + proof_entry_opaque : bool; + proof_entry_inline_code : bool; +} + type 'a constant_entry = - | DefinitionEntry of 'a Proof_global.proof_entry + | DefinitionEntry of 'a proof_entry | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry @@ -174,7 +186,6 @@ let record_aux env s_ty s_bo = let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body = - let open Proof_global in { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); proof_entry_secctx = None; proof_entry_type = types; @@ -184,7 +195,6 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types proof_entry_inline_code = inline} let cast_proof_entry e = - let open Proof_global in let (body, ctx), () = Future.force e.proof_entry_body in let univs = if Univ.ContextSet.is_empty ctx then e.proof_entry_universes @@ -205,7 +215,6 @@ let cast_proof_entry e = } let cast_opaque_proof_entry e = - let open Proof_global in let typ = match e.proof_entry_type with | None -> assert false | Some typ -> typ @@ -249,7 +258,6 @@ let is_unsafe_typing_flags () = not (flags.check_universes && flags.check_guarded && flags.check_positive) let define_constant ~side_effect ~name cd = - let open Proof_global in (* Logically define the constant and its subproofs, no libobject tampering *) let in_section = Lib.sections_are_opened () in let export, decl, unsafe = match cd with @@ -299,7 +307,7 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind (** Declaration of section variables and local definitions *) type variable_declaration = - | SectionLocalDef of Evd.side_effects Proof_global.proof_entry + | SectionLocalDef of Evd.side_effects proof_entry | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind } (* This object is only for things which iterate over objects to find @@ -321,7 +329,6 @@ let declare_variable ~name ~kind d = | SectionLocalDef (de) -> (* The body should already have been forced upstream because it is a section-local definition, but it's not enforced by typing *) - let open Proof_global in let (body, eff) = Future.force de.proof_entry_body in let ((body, uctx), export) = Global.export_private_constants ~in_section:true (body, eff.Evd.seff_private) in let eff = get_roles export eff in diff --git a/tactics/declare.mli b/tactics/declare.mli index 4ae9f6c7ae..4cb876cecb 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -19,14 +19,27 @@ open Entries reset works properly --- and will fill some global tables such as [Nametab] and [Impargs]. *) +(** Proof entries *) +type 'a proof_entry = { + proof_entry_body : 'a Entries.const_entry_body; + (* List of section variables *) + proof_entry_secctx : Constr.named_context option; + (* State id on which the completion of type checking is reported *) + proof_entry_feedback : Stateid.t option; + proof_entry_type : Constr.types option; + proof_entry_universes : Entries.universes_entry; + proof_entry_opaque : bool; + proof_entry_inline_code : bool; +} + (** Declaration of local constructions (Variable/Hypothesis/Local) *) type variable_declaration = - | SectionLocalDef of Evd.side_effects Proof_global.proof_entry + | SectionLocalDef of Evd.side_effects proof_entry | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind } type 'a constant_entry = - | DefinitionEntry of 'a Proof_global.proof_entry + | DefinitionEntry of 'a proof_entry | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry @@ -43,7 +56,7 @@ val declare_variable val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:types -> ?univs:Entries.universes_entry -> - ?eff:Evd.side_effects -> constr -> Evd.side_effects Proof_global.proof_entry + ?eff:Evd.side_effects -> constr -> Evd.side_effects proof_entry type import_status = ImportDefaultBehavior | ImportNeedQualified diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index e2ef05461b..1f973ace6f 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -125,7 +125,7 @@ let define internal role id c poly univs = let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in let univs = UState.univ_entry ~poly ctx in let entry = { - Proof_global.proof_entry_body = + Declare.proof_entry_body = Future.from_val ((c,Univ.ContextSet.empty), Evd.empty_side_effects); proof_entry_secctx = None; diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml new file mode 100644 index 0000000000..5be7b4fa28 --- /dev/null +++ b/tactics/pfedit.ml @@ -0,0 +1,195 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* !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 -> CErrors.user_err Pp.(str "No such goal.") + | _ -> raise CErrors.Unhandled +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_current_context pf = + let p = Proof_global.get_proof pf in + try get_goal_context_gen p 1 + with + | NoSuchGoal -> + (* No more focused goals *) + let { Proof.sigma } = Proof.data p in + sigma, Global.env () + +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 ctx sign ~poly typ tac = + let evd = Evd.from_ctx ctx 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 + try + let pf, status = by tac pf in + let open Proof_global in + let { entries; universes } = close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in + match entries with + | [entry] -> + let univs = UState.demote_seff_univs entry.Declare.proof_entry_universes universes in + entry, status, univs + | _ -> + CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term") + with reraise -> + let reraise = CErrors.push reraise in + iraise reraise + +let build_by_tactic ?(side_eff=true) env sigma ~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 sigma sign ~poly typ tac in + let body, eff = Future.force ce.Declare.proof_entry_body in + let (cb, ctx) = + if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) + else body + in + let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in + cb, 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) = CErrors.push src in + 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 new file mode 100644 index 0000000000..30514191fa --- /dev/null +++ b/tactics/pfedit.mli @@ -0,0 +1,89 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* 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_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 + -> UState.t + -> 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 + -> UState.t + -> poly:bool + -> EConstr.types + -> unit Proofview.tactic + -> constr * 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 new file mode 100644 index 0000000000..a2929e45cd --- /dev/null +++ b/tactics/proof_global.ml @@ -0,0 +1,303 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* 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"); + (* EJGA: This is always empty thus we should modify the type *) + (ctx, []), { ps with section_vars = Some 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; + optname = "use private polymorphic universes for Qed constants"; + optkey = ["Private";"Polymorphic";"Universes"]; + optread = (fun () -> !b); + optwrite = ((:=) b); + }) + in + fun () -> !b + +let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now + (fpl : closed_proof_output Future.computation) ps = + let { section_vars; proof; udecl; initial_euctx } = ps in + let Proof.{ name; poly; entry } = Proof.data proof in + let opaque = match opaque with Opaque -> true | Transparent -> false in + let constrain_variables ctx = + UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx + in + let fpl, univs = Future.split2 fpl in + let universes = if poly || now then Future.force univs else initial_euctx 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 = + let { Proof.sigma } = Proof.data proof in + Evd.existential_opt_value0 sigma k in + let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar + (UState.subst universes) in + + let make_body = + if poly || now then + let make_body t (c, eff) = + let body = c in + let allow_deferred = + not poly && (keep_body_ucst_separate || + not (Safe_typing.empty_private_constants = eff.Evd.seff_private)) + in + let typ = if allow_deferred then t else nf t in + let used_univs_body = Vars.universes_of_constr body in + let used_univs_typ = Vars.universes_of_constr typ in + if allow_deferred then + let initunivs = UState.univ_entry ~poly initial_euctx in + let ctx = constrain_variables universes 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 used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let ctx_body = UState.restrict ctx used_univs in + let univs = UState.check_mono_univ_decl ctx_body udecl in + (initunivs, typ), ((body, univs), eff) + else if poly && opaque && private_poly_univs () then + let used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let universes = UState.restrict universes used_univs in + let typus = UState.restrict universes used_univs_typ in + let udecl = UState.check_univ_decl ~poly typus udecl in + let ubody = Univ.ContextSet.diff + (UState.context_set universes) + (UState.context_set typus) + in + (udecl, typ), ((body, ubody), eff) + 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 used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let ctx = UState.restrict universes used_univs in + let univs = UState.check_univ_decl ~poly ctx udecl in + (univs, typ), ((body, Univ.ContextSet.empty), eff) + in + fun t p -> Future.split2 (Future.chain p (make_body t)) + else + fun t p -> + (* Already checked the univ_decl for the type universes when starting the proof. *) + let univctx = UState.univ_entry ~poly:false universes in + let t = nf t in + Future.from_val (univctx, t), + 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 univs = Future.force univs in + let univs = constrain_variables univs in + let used_univs = Univ.LSet.union + (Vars.universes_of_constr t) + (Vars.universes_of_constr pt) + in + let univs = UState.restrict univs used_univs in + let univs = UState.check_mono_univ_decl univs udecl in + (pt,univs),eff) + in + let entry_fn p (_, t) = + let t = EConstr.Unsafe.to_constr t in + let univstyp, body = make_body t p in + let univs, typ = Future.force univstyp in + let open Declare in + { + proof_entry_body = body; + proof_entry_secctx = section_vars; + proof_entry_feedback = feedback_id; + proof_entry_type = Some typ; + proof_entry_inline_code = false; + proof_entry_opaque = opaque; + proof_entry_universes = univs; } + in + let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in + { name; entries = entries; poly; universes; udecl } + +let return_proof ?(allow_partial=false) ps = + let { proof } = ps in + if allow_partial then begin + 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 + end else + 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 *) + let proofs = + List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in + proofs, Evd.evar_universe_context evd + +let close_future_proof ~opaque ~feedback_id ps proof = + close_proof ~opaque ~keep_body_ucst_separate:true ~feedback_id ~now:false proof ps + +let close_proof ~opaque ~keep_body_ucst_separate fix_exn ps = + close_proof ~opaque ~keep_body_ucst_separate ~now:true + (Future.from_val ~fix_exn (return_proof ps)) ps + +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 new file mode 100644 index 0000000000..d15e23c2cc --- /dev/null +++ b/tactics/proof_global.mli @@ -0,0 +1,103 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* Proof.t +val get_proof_name : t -> Names.Id.t +val get_used_variables : t -> Constr.named_context 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). *) + ; poly : bool + (** polymorphic status *) + ; universes: UState.t + (** universe state *) + ; udecl : UState.universe_decl + (** universe declaration *) + } + +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 -> Future.fix_exn -> 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 = (Constr.t * Evd.side_effects) list * UState.t + +(* If allow_partial is set (default no) then an incomplete proof + * is allowed (no error), and a warn is given if the proof is complete. *) +val return_proof : ?allow_partial:bool -> t -> closed_proof_output +val close_future_proof : opaque:opacity_flag -> 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) + a list of + * ids to be cleared *) +val set_used_variables : t -> + Names.Id.t list -> (Constr.named_context * Names.lident list) * t diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 6dd749aa0d..c5c7969a09 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -1,4 +1,6 @@ Declare +Proof_global +Pfedit Dnet Dn Btermdn diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 57de719cb4..9745358ba2 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -85,12 +85,12 @@ let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_o in if program_mode then let env = Global.env () in - let (c,ctx), sideff = Future.force ce.Proof_global.proof_entry_body in + let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private); assert(Univ.ContextSet.is_empty ctx); Obligations.check_evars env evd; let c = EConstr.of_constr c in - let typ = match ce.Proof_global.proof_entry_type with + let typ = match ce.Declare.proof_entry_type with | Some t -> EConstr.of_constr t | None -> Retyping.get_type_of env evd c in diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index db0c102e14..01505d0733 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -41,5 +41,5 @@ val interp_definition -> red_expr option -> constr_expr -> constr_expr option - -> Evd.side_effects Proof_global.proof_entry * + -> Evd.side_effects Declare.proof_entry * Evd.evar_map * UState.universe_decl * Impargs.manual_implicits diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 5e4f2dcd34..1926faaf0e 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -44,7 +44,7 @@ end (* Locality stuff *) let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = - let fix_exn = Future.fix_exn_of ce.Proof_global.proof_entry_body in + let fix_exn = Future.fix_exn_of ce.proof_entry_body in let gr = match scope with | Discharge -> let () = diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 606cfade46..54a0c9a7e8 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -45,7 +45,7 @@ val declare_definition -> kind:Decls.definition_object_kind -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) -> UnivNames.universe_binders - -> Evd.side_effects Proof_global.proof_entry + -> Evd.side_effects Declare.proof_entry -> Impargs.manual_implicits -> GlobRef.t @@ -66,7 +66,7 @@ val prepare_definition : allow_evars:bool -> ?opaque:bool -> ?inline:bool -> poly:bool -> Evd.evar_map -> UState.universe_decl -> types:EConstr.t option -> body:EConstr.t -> - Evd.evar_map * Evd.side_effects Proof_global.proof_entry + Evd.evar_map * Evd.side_effects Declare.proof_entry val prepare_parameter : allow_evars:bool -> poly:bool -> Evd.evar_map -> UState.universe_decl -> EConstr.types -> diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index c5cbb095ca..9c8213ad8a 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -153,7 +153,7 @@ let declare_obligation prg obl body ty uctx = ((body, Univ.ContextSet.empty), Evd.empty_side_effects) in let ce = - Proof_global.{ proof_entry_body = Future.from_val ~fix_exn:(fun x -> x) body + { Declare.proof_entry_body = Future.from_val ~fix_exn:(fun x -> x) body ; proof_entry_secctx = None ; proof_entry_type = ty ; proof_entry_universes = uctx @@ -495,12 +495,11 @@ type obligation_qed_info = } let obligation_terminator entries uctx { name; num; auto } = - let open Proof_global in match entries with | [entry] -> let env = Global.env () in - let ty = entry.proof_entry_type in - let body, eff = Future.force entry.proof_entry_body in + let ty = entry.Declare.proof_entry_type in + let body, eff = Future.force entry.Declare.proof_entry_body in let (body, cstr) = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in let sigma = Evd.from_ctx uctx in let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in @@ -514,7 +513,7 @@ let obligation_terminator entries uctx { name; num; auto } = let obls, rem = prg.prg_obligations in let obl = obls.(num) in let status = - match obl.obl_status, entry.proof_entry_opaque with + match obl.obl_status, entry.Declare.proof_entry_opaque with | (_, Evar_kinds.Expand), true -> err_not_transp () | (true, _), true -> err_not_transp () | (false, _), true -> Evar_kinds.Define true diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli index 2a8fa734b3..7d8a112cc6 100644 --- a/vernac/declareObl.mli +++ b/vernac/declareObl.mli @@ -76,7 +76,7 @@ type obligation_qed_info = } val obligation_terminator - : Evd.side_effects Proof_global.proof_entry list + : Evd.side_effects Declare.proof_entry list -> UState.t -> obligation_qed_info -> unit (** [obligation_terminator] part 2 of saving an obligation *) diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index cf87646905..18955c2ba3 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -101,7 +101,6 @@ let () = let define ~poly name sigma c t = let f = declare_constant ~kind:Decls.(IsDefinition Scheme) in let univs = Evd.univ_entry ~poly sigma in - let open Proof_global in let kn = f ~name (DefinitionEntry { proof_entry_body = c; diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 7809425a10..42d1a1f3fc 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -383,10 +383,9 @@ let adjust_guardness_conditions const = function | possible_indexes -> (* Try all combinations... not optimal *) let env = Global.env() in - let open Proof_global in { const with - proof_entry_body = - Future.chain const.proof_entry_body + Declare.proof_entry_body = + Future.chain const.Declare.proof_entry_body (fun ((body, ctx), eff) -> match Constr.kind body with | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> @@ -404,10 +403,11 @@ let finish_proved env sigma idopt po info = let name = match idopt with | None -> name | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in - let fix_exn = Future.fix_exn_of const.proof_entry_body in + let fix_exn = Future.fix_exn_of const.Declare.proof_entry_body in let () = try let const = adjust_guardness_conditions const compute_guard in - let should_suggest = const.proof_entry_opaque && Option.is_empty const.proof_entry_secctx in + let should_suggest = const.Declare.proof_entry_opaque && + Option.is_empty const.Declare.proof_entry_secctx in let open DeclareDef in let r = match scope with | Discharge -> @@ -451,7 +451,7 @@ let finish_derived ~f ~name ~idopt ~entries = in (* The opacity of [f_def] is adjusted to be [false], as it must. Then [f] is declared in the global environment. *) - let f_def = { f_def with Proof_global.proof_entry_opaque = false } in + let f_def = { f_def with Declare.proof_entry_opaque = false } in let f_kind = Decls.(IsDefinition Definition) in let f_def = Declare.DefinitionEntry f_def in let f_kn = Declare.declare_constant ~name:f ~kind:f_kind f_def in @@ -463,17 +463,17 @@ let finish_derived ~f ~name ~idopt ~entries = let substf c = Vars.replace_vars [f,f_kn_term] c in (* Extracts the type of the proof of [suchthat]. *) let lemma_pretype = - match Proof_global.(lemma_def.proof_entry_type) with + match lemma_def.Declare.proof_entry_type with | Some t -> t | None -> assert false (* Proof_global always sets type here. *) in (* The references of [f] are subsituted appropriately. *) let lemma_type = substf lemma_pretype in (* The same is done in the body of the proof. *) - let lemma_body = Future.chain Proof_global.(lemma_def.proof_entry_body) (fun ((b,ctx),fx) -> (substf b, ctx), fx) in - let lemma_def = let open Proof_global in + let lemma_body = Future.chain lemma_def.Declare.proof_entry_body (fun ((b,ctx),fx) -> (substf b, ctx), fx) in + let lemma_def = { lemma_def with - proof_entry_body = lemma_body; + Declare.proof_entry_body = lemma_body; proof_entry_type = Some lemma_type } in let lemma_def = Declare.DefinitionEntry lemma_def in @@ -530,7 +530,7 @@ let save_lemma_admitted_delayed ~proof ~info = let { Info.hook; scope; impargs; other_thms } = info in if List.length entries <> 1 then user_err Pp.(str "Admitted does not support multiple statements"); - let { proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in + let { Declare.proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in let poly = match proof_entry_universes with | Entries.Monomorphic_entry _ -> false | Entries.Polymorphic_entry (_, _) -> true in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 37fe0df0ee..5d153fa8be 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -423,11 +423,11 @@ let solve_by_tac ?loc name evi t poly ctx = Pfedit.build_constant_by_tactic ~name ~poly ctx evi.evar_hyps evi.evar_concl t in let env = Global.env () in - let (body, eff) = Future.force entry.Proof_global.proof_entry_body in + let (body, eff) = Future.force entry.Declare.proof_entry_body in let body = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body)); - Some (fst body, entry.Proof_global.proof_entry_type, Evd.evar_universe_context ctx') + Some (fst body, entry.Declare.proof_entry_type, Evd.evar_universe_context ctx') with | Refiner.FailError (_, s) as exn -> let _ = CErrors.push exn in diff --git a/vernac/record.ml b/vernac/record.ml index 86745212e7..1bb8ddf5dc 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -340,7 +340,6 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in try - let open Proof_global in let entry = { proof_entry_body = Future.from_val ((proj, Univ.ContextSet.empty), Evd.empty_side_effects); -- cgit v1.2.3 From 5196ab8da3416bb7ebd17c1445afe7f08ab01cae Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 20 Aug 2019 19:57:17 +0200 Subject: [declare] Use entry constructor instead of low-level record. Non-delayed entries can be done with the current constructor, delayed ones will require more work. --- plugins/funind/gen_principle.ml | 53 +++++++++++++++++++---------------------- tactics/ind_tables.ml | 12 +--------- vernac/declareObl.ml | 14 ++--------- vernac/indschemes.ml | 20 ++++------------ vernac/record.ml | 10 +------- 5 files changed, 33 insertions(+), 76 deletions(-) diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 352b21a15a..92b7f2accf 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -164,7 +164,7 @@ let prepare_body { Vernacexpr.binders } rt = let fun_args,rt' = chop_rlambda_n n rt in (fun_args,rt') -let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook = +let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook = (* First we get the type of the old graph principle *) let mutr_nparams = (Tactics.compute_elim_sig !evd (EConstr.of_constr old_princ_type)).Tactics.nparams in (* let time1 = System.get_time () in *) @@ -199,10 +199,10 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin (* end; *) let open Proof_global in - let { name; entries } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in + let { name; entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)) lemma in match entries with | [entry] -> - name, entry, hook + entry, hook | _ -> CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term") @@ -282,7 +282,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) register_with_sort Sorts.InProp; register_with_sort Sorts.InSet in - let id,entry,hook = + let entry, hook = build_functional_principle evd interactive_proof old_princ_type new_sorts funs i proof_tac hook in @@ -1219,9 +1219,21 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef s::l_schemes -> s,l_schemes | _ -> CErrors.anomaly (Pp.str "") in - let _,const,_ = + let opaque = + let finfos = + match find_Function_infos (fst first_fun) with + | None -> raise Not_found + | Some finfos -> finfos + in + let open Proof_global in + match finfos.equation_lemma with + | None -> Transparent (* non recursive definition *) + | Some equation -> + if Declareops.is_opaque (Global.lookup_constant equation) then Opaque else Transparent + in + let entry, _hook = try - build_functional_principle evd false + build_functional_principle ~opaque evd false first_type (Array.of_list sorts) this_block_funs @@ -1233,29 +1245,16 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef in incr i; - let opacity = - let finfos = - match find_Function_infos (fst first_fun) with - | None -> raise Not_found - | Some finfos -> finfos - in - match finfos.equation_lemma with - | None -> false (* non recursive definition *) - | Some equation -> - Declareops.is_opaque (Global.lookup_constant equation) - in - let const = {const with Declare.proof_entry_opaque = opacity } in (* The others are just deduced *) if List.is_empty other_princ_types - then - [const] + then [entry] else let other_fun_princ_types = let funs = Array.map Constr.mkConstU this_block_funs in let sorts = Array.of_list sorts in List.map (Functional_principles_types.compute_new_princ_type_from_rel funs sorts) other_princ_types in - let first_princ_body,first_princ_type = Declare.(const.proof_entry_body, const.proof_entry_type) in + let first_princ_body,first_princ_type = Declare.(entry.proof_entry_body, entry.proof_entry_type) in let ctxt,fix = Term.decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*) let (idxs,_),(_,ta,_ as decl) = Constr.destFix fix in let other_result = @@ -1282,7 +1281,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef (* If we reach this point, the two principle are not mutually recursive We fall back to the previous method *) - let _,const,_ = + let entry, _hook = build_functional_principle evd false @@ -1293,20 +1292,16 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef (Functional_principles_proofs.prove_princ_for_struct evd false !i (Array.of_list (List.map fst funs))) (fun _ _ -> ()) in - const + entry with Found_type i -> let princ_body = Termops.it_mkLambda_or_LetIn (Constr.mkFix((idxs,i),decl)) ctxt in - { const with - Declare.proof_entry_body = - (Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects)); - proof_entry_type = Some scheme_type - } + Declare.definition_entry ~types:scheme_type princ_body ) other_fun_princ_types in - const::other_result + entry::other_result (* [derive_correctness funs graphs] create correctness and completeness lemmas for each function in [funs] w.r.t. [graphs] diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 1f973ace6f..54393dce00 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -124,17 +124,7 @@ let define internal role id c poly univs = let ctx = UState.minimize univs in let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in let univs = UState.univ_entry ~poly ctx in - let entry = { - Declare.proof_entry_body = - Future.from_val ((c,Univ.ContextSet.empty), - Evd.empty_side_effects); - proof_entry_secctx = None; - proof_entry_type = None; - proof_entry_universes = univs; - proof_entry_opaque = false; - proof_entry_inline_code = false; - proof_entry_feedback = None; - } in + let entry = Declare.definition_entry ~univs c in let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id (Declare.DefinitionEntry entry) in let () = match internal with | InternalTacticRequest -> () diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 9c8213ad8a..e3cffa8523 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -149,18 +149,8 @@ let declare_obligation prg obl body ty uctx = if get_shrink_obligations () && not poly then shrink_body body ty else ([], body, ty, [||]) in - let body = - ((body, Univ.ContextSet.empty), Evd.empty_side_effects) - in - let ce = - { Declare.proof_entry_body = Future.from_val ~fix_exn:(fun x -> x) body - ; proof_entry_secctx = None - ; proof_entry_type = ty - ; proof_entry_universes = uctx - ; proof_entry_opaque = opaque - ; proof_entry_inline_code = false - ; proof_entry_feedback = None } - in + let ce = Declare.definition_entry ?types:ty ~opaque ~univs:uctx body in + (* ppedrot: seems legit to have obligations as local *) let constant = Declare.declare_constant ~name:obl.obl_name diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 18955c2ba3..a6c577a878 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -98,19 +98,11 @@ let () = (* Util *) -let define ~poly name sigma c t = +let define ~poly name sigma c types = let f = declare_constant ~kind:Decls.(IsDefinition Scheme) in let univs = Evd.univ_entry ~poly sigma in - let kn = f ~name - (DefinitionEntry - { proof_entry_body = c; - proof_entry_secctx = None; - proof_entry_type = t; - proof_entry_universes = univs; - proof_entry_opaque = false; - proof_entry_inline_code = false; - proof_entry_feedback = None; - }) in + let entry = Declare.definition_entry ~univs ?types c in + let kn = f ~name (DefinitionEntry entry) in definition_message name; kn @@ -411,8 +403,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort = let declare decl fi lrecref = let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in let decltype = EConstr.to_constr sigma decltype in - let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Evd.empty_side_effects) in - let cst = define ~poly fi sigma proof_output (Some decltype) in + let cst = define ~poly fi sigma decl (Some decltype) in GlobRef.ConstRef cst :: lrecref in let _ = List.fold_right2 declare listdecl lrecnames [] in @@ -533,7 +524,6 @@ let do_combined_scheme name schemes = schemes in let sigma,body,typ = build_combined_scheme (Global.env ()) csts in - let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Evd.empty_side_effects) in (* It is possible for the constants to have different universe polymorphism from each other, however that is only when the user manually defined at least one of them (as Scheme would pick the @@ -541,7 +531,7 @@ let do_combined_scheme name schemes = some other polymorphism they can also manually define the combined scheme. *) let poly = Global.is_polymorphic (GlobRef.ConstRef (List.hd csts)) in - ignore (define ~poly name.v sigma proof_output (Some typ)); + ignore (define ~poly name.v sigma body (Some typ)); fixpoint_message None [name.v] (**********************************************************************) diff --git a/vernac/record.ml b/vernac/record.ml index 1bb8ddf5dc..11237f3873 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -340,15 +340,7 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in try - let entry = { - proof_entry_body = - Future.from_val ((proj, Univ.ContextSet.empty), Evd.empty_side_effects); - proof_entry_secctx = None; - proof_entry_type = Some projtyp; - proof_entry_universes = ctx; - proof_entry_opaque = false; - proof_entry_inline_code = false; - proof_entry_feedback = None } in + let entry = Declare.definition_entry ~univs:ctx ~types:projtyp proj in let kind = Decls.IsDefinition kind in let kn = declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry) in let constr_fip = -- cgit v1.2.3