diff options
Diffstat (limited to 'vernac')
71 files changed, 2500 insertions, 1924 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 9353ef3902..d7cb9dc727 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -168,7 +168,7 @@ let rec traverse current ctx accu t = match Constr.kind t with let body () = id |> Global.lookup_named |> NamedDecl.get_value in traverse_object accu body (VarRef id) | Const (kn, _) -> - let body () = Option.map fst (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in + let body () = Option.map pi1 (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in traverse_object accu body (ConstRef kn) | Ind ((mind, _) as ind, _) -> traverse_inductive accu mind (IndRef ind) @@ -181,7 +181,7 @@ let rec traverse current ctx accu t = match Constr.kind t with | Lambda(_,_,oty), Const (kn, _) when Vars.noccurn 1 oty && not (Declareops.constant_has_body (lookup_constant kn)) -> - let body () = Option.map fst (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in + let body () = Option.map pi1 (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in traverse_object ~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn) | _ -> diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli index 536185f4aa..5e63829411 100644 --- a/vernac/assumptions.mli +++ b/vernac/assumptions.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 1ad5862d5d..6af454eee5 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -73,11 +73,6 @@ module Notations = struct end open Notations -type deprecation = { since : string option ; note : string option } - -let mk_deprecation ?(since=None) ?(note=None) () = - { since ; note } - let assert_empty k v = if v <> VernacFlagEmpty then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments") @@ -213,19 +208,16 @@ let polymorphic = universe_transform ~warn_unqualified:true >> qualify_attribute ukey polymorphic_base -let deprecation_parser : deprecation key_parser = fun orig args -> +let deprecation_parser : Deprecation.t key_parser = fun orig args -> assert_once ~name:"deprecation" orig; match args with | VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ] | VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] -> - let since = Some since and note = Some note in - mk_deprecation ~since ~note () + Deprecation.make ~since ~note () | VernacFlagList [ "since", VernacFlagLeaf since ] -> - let since = Some since in - mk_deprecation ~since () + Deprecation.make ~since () | VernacFlagList [ "note", VernacFlagLeaf note ] -> - let note = Some note in - mk_deprecation ~note () + Deprecation.make ~note () | _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute") let deprecation = attribute_of_list ["deprecated",deprecation_parser] diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 44688ddafc..34ff15ca7d 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -43,15 +43,11 @@ end (** Definitions for some standard attributes. *) -type deprecation = { since : string option ; note : string option } - -val mk_deprecation : ?since: string option -> ?note: string option -> unit -> deprecation - val polymorphic : bool attribute val program : bool attribute val template : bool option attribute val locality : bool option attribute -val deprecation : deprecation option attribute +val deprecation : Deprecation.t option attribute val canonical : bool attribute val program_mode_option_name : string list diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 5aec5cac2c..38852992e4 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -195,7 +195,7 @@ let build_beq_scheme mode kn = let (c,a) = Reductionops.whd_betaiota_stack Evd.empty EConstr.(of_constr c) in let (c,a) = EConstr.Unsafe.(to_constr c, List.map to_constr a) in match Constr.kind c with - | Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants + | Rel x -> mkRel (x-nlist+ndx), Evd.empty_side_effects | Var x -> (* Support for working in a context with "eq_x : x -> x -> bool" *) let eid = Id.of_string ("eq_"^(Id.to_string x)) in @@ -203,11 +203,11 @@ let build_beq_scheme mode kn = try ignore (Environ.lookup_named eid env) with Not_found -> raise (ParameterWithoutEquality (VarRef x)) in - mkVar eid, Safe_typing.empty_private_constants + mkVar eid, Evd.empty_side_effects | Cast (x,_,_) -> aux (Term.applist (x,a)) | App _ -> assert false | Ind ((kn',i as ind'),u) (*FIXME: universes *) -> - if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Safe_typing.empty_private_constants + if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Evd.empty_side_effects else begin try let eq, eff = @@ -216,7 +216,7 @@ let build_beq_scheme mode kn = let eqa, eff = let eqa, effs = List.split (List.map aux a) in Array.of_list eqa, - List.fold_left Safe_typing.concat_private eff (List.rev effs) + List.fold_left Evd.concat_side_effects eff (List.rev effs) in let args = Array.append @@ -239,7 +239,7 @@ let build_beq_scheme mode kn = let kneq = Constant.change_label kn eq_lbl in try let _ = Environ.constant_opt_value_in env (kneq, u) in Term.applist (mkConst kneq,a), - Safe_typing.empty_private_constants + Evd.empty_side_effects with Not_found -> raise (ParameterWithoutEquality (ConstRef kn))) | Proj _ -> raise (EqUnknown "projection") | Construct _ -> raise (EqUnknown "constructor") @@ -270,7 +270,7 @@ let build_beq_scheme mode kn = let constrsi = constrs (3+nparrec) in let n = Array.length constrsi in let ar = Array.make n (ff ()) in - let eff = ref Safe_typing.empty_private_constants in + let eff = ref Evd.empty_side_effects in for i=0 to n-1 do let nb_cstr_args = List.length constrsi.(i).cs_args in let ar2 = Array.make n (ff ()) in @@ -288,7 +288,7 @@ let build_beq_scheme mode kn = (nb_cstr_args+ndx+1) cc in - eff := Safe_typing.concat_private eff' !eff; + eff := Evd.concat_side_effects eff' !eff; Array.set eqs ndx (mkApp (eqA, [|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|] @@ -320,7 +320,7 @@ let build_beq_scheme mode kn = let names = Array.make nb_ind (make_annot Anonymous Sorts.Relevant) and types = Array.make nb_ind mkSet and cores = Array.make nb_ind mkSet in - let eff = ref Safe_typing.empty_private_constants in + let eff = ref Evd.empty_side_effects in let u = Univ.Instance.empty in for i=0 to (nb_ind-1) do names.(i) <- make_annot (Name (Id.of_string (rec_name i))) Sorts.Relevant; @@ -328,7 +328,7 @@ let build_beq_scheme mode kn = (mkArrow (mkFullInd ((kn,i),u) 1) Sorts.Relevant (bb ())); let c, eff' = make_one_eq i in cores.(i) <- c; - eff := Safe_typing.concat_private eff' !eff + eff := Evd.concat_side_effects eff' !eff done; (Array.init nb_ind (fun i -> let kelim = Inductive.elim_sort (mib,mib.mind_packets.(i)) in @@ -938,7 +938,7 @@ let compute_dec_tact ind lnamesparrec nparrec = Not_found -> Tacticals.New.tclZEROMSG (str "Error during the decidability part, leibniz to boolean equality is required.") end >>= fun (lbI,eff'') -> - let eff = (Safe_typing.concat_private eff'' (Safe_typing.concat_private eff' eff)) in + let eff = (Evd.concat_side_effects eff'' (Evd.concat_side_effects eff' eff)) in Tacticals.New.tclTHENLIST [ Proofview.tclEFFECTS eff; intros_using fresh_first_intros; @@ -1005,7 +1005,7 @@ let make_eq_decidability mode mind = (EConstr.of_constr (compute_dec_goal (ind,u) lnamesparrec nparrec)) (compute_dec_tact ind lnamesparrec nparrec) in - ([|ans|], ctx), Safe_typing.empty_private_constants + ([|ans|], ctx), Evd.empty_side_effects let eq_dec_scheme_kind = declare_mutual_scheme_object "_eq_dec" make_eq_decidability diff --git a/vernac/auto_ind_decl.mli b/vernac/auto_ind_decl.mli index 647ff3d8d6..0de8c61f59 100644 --- a/vernac/auto_ind_decl.mli +++ b/vernac/auto_ind_decl.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/canonical.ml b/vernac/canonical.ml index 92d5731f92..e9454bab8a 100644 --- a/vernac/canonical.ml +++ b/vernac/canonical.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/canonical.mli b/vernac/canonical.mli index 5b223a0615..a3bbaf6d18 100644 --- a/vernac/canonical.mli +++ b/vernac/canonical.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/class.ml b/vernac/class.ml index f3a279eab1..d5c75ed809 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -17,7 +17,6 @@ open Constr open Context open Vars open Termops -open Entries open Environ open Classops open Declare @@ -358,23 +357,23 @@ let try_add_new_coercion_with_source ref ~local poly ~source = let add_coercion_hook poly _uctx _trans local ref = let local = match local with - | Discharge - | Local -> true - | Global -> false + | Discharge -> assert false (* Local Coercion in section behaves like Local Definition *) + | Global ImportNeedQualified -> true + | Global ImportDefaultBehavior -> false in let () = try_add_new_coercion ref ~local poly in let msg = Nametab.pr_global_env Id.Set.empty ref ++ str " is now a coercion" in Flags.if_verbose Feedback.msg_info msg -let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly) +let add_coercion_hook poly = DeclareDef.Hook.make (add_coercion_hook poly) let add_subclass_hook poly _uctx _trans local ref = let stre = match local with - | Local -> true - | Global -> false - | Discharge -> assert false + | Discharge -> assert false (* Local Subclass in section behaves like Local Definition *) + | Global ImportNeedQualified -> true + | Global ImportDefaultBehavior -> false in let cl = class_of_global ref in try_add_new_coercion_subclass cl ~local:stre poly -let add_subclass_hook poly = Lemmas.mk_hook (add_subclass_hook poly) +let add_subclass_hook poly = DeclareDef.Hook.make (add_subclass_hook poly) diff --git a/vernac/class.mli b/vernac/class.mli index 80d6d4383c..d530d218d4 100644 --- a/vernac/class.mli +++ b/vernac/class.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -42,8 +42,8 @@ val try_add_new_coercion_with_source : GlobRef.t -> local:bool -> val try_add_new_identity_coercion : Id.t -> local:bool -> Decl_kinds.polymorphic -> source:cl_typ -> target:cl_typ -> unit -val add_coercion_hook : Decl_kinds.polymorphic -> Lemmas.declaration_hook +val add_coercion_hook : Decl_kinds.polymorphic -> DeclareDef.Hook.t -val add_subclass_hook : Decl_kinds.polymorphic -> Lemmas.declaration_hook +val add_subclass_hook : Decl_kinds.polymorphic -> DeclareDef.Hook.t val class_of_global : GlobRef.t -> cl_typ diff --git a/vernac/classes.ml b/vernac/classes.ml index ea66234993..d6a2f2727a 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -29,7 +29,6 @@ module NamedDecl = Context.Named.Declaration (*i*) open Decl_kinds -open Entries let set_typeclass_transparency c local b = Hints.add_hints ~local [typeclasses_db] @@ -281,9 +280,6 @@ let existing_instance glob g info = ~hdr:"declare_instance" (Pp.str "Constant does not build instances of a declared type class.") -let mismatched_params env n m = Implicit_quantifiers.mismatched_ctx_inst_err env Parameters n m -let mismatched_props env n m = Implicit_quantifiers.mismatched_ctx_inst_err env Properties n m - (* Declare everything in the parameters as implicit, and the class instance as well *) let type_ctx_instance ~program_mode env sigma ctx inst subst = @@ -309,7 +305,7 @@ let id_of_class cl = mip.(0).Declarations.mind_typename | _ -> assert false -let instance_hook k info global imps ?hook cst = +let instance_hook info global imps ?hook cst = Impargs.maybe_declare_manual_implicits false cst imps; let info = intern_info info in let env = Global.env () in @@ -317,7 +313,7 @@ let instance_hook k info global imps ?hook cst = declare_instance env sigma (Some info) (not global) cst; (match hook with Some h -> h cst | None -> ()) -let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype = +let declare_instance_constant info global imps ?hook id decl poly sigma term termtype = (* XXX: Duplication of the declare_constant path *) let kind = IsDefinition Instance in let sigma = @@ -327,13 +323,13 @@ let declare_instance_constant k info global imps ?hook id decl poly sigma term t in let uctx = Evd.check_univ_decl ~poly sigma decl in let entry = Declare.definition_entry ~types:termtype ~univs:uctx term in - let cdecl = (DefinitionEntry entry, kind) in + let cdecl = (Declare.DefinitionEntry entry, kind) in let kn = Declare.declare_constant id cdecl in Declare.definition_message id; Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma); - instance_hook k info global imps ?hook (ConstRef kn) + instance_hook info global imps ?hook (ConstRef kn) -let do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst id = +let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst id = let subst = List.fold_left2 (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst') [] subst (snd k.cl_context) @@ -342,138 +338,80 @@ let do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id - (ParameterEntry entry, Decl_kinds.IsAssumption Decl_kinds.Logical) in + (Declare.ParameterEntry entry, Decl_kinds.IsAssumption Decl_kinds.Logical) in Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma); - instance_hook k pri global imps (ConstRef cst) - -let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl ids term termtype = - let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in - if program_mode then - let hook _ _ vis gr = - let cst = match gr with ConstRef kn -> kn | _ -> assert false in - Impargs.declare_manual_implicits false gr imps; - let pri = intern_info pri in - let env = Global.env () in - let sigma = Evd.from_env env in - declare_instance env sigma (Some pri) (not global) (ConstRef cst) - in - let obls, constr, typ = - match term with - | Some t -> - let termtype = EConstr.of_constr termtype in - let obls, _, constr, typ = - Obligations.eterm_obligations env id sigma 0 t termtype - in obls, Some constr, typ - | None -> [||], None, termtype - in - let hook = Lemmas.mk_hook hook in - let ctx = Evd.evar_universe_context sigma in - let _progress = Obligations.add_definition id ?term:constr - ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls in - pstate - else - Some Flags.(silently (fun () -> - (* spiwack: it is hard to reorder the actions to do - the pretyping after the proof has opened. As a - consequence, we use the low-level primitives to code - the refinement manually.*) - let gls = List.rev (Evd.future_goals sigma) in - let sigma = Evd.reset_future_goals sigma in - let pstate = Lemmas.start_proof ~ontop:pstate id ~pl:decl kind sigma (EConstr.of_constr termtype) - ~hook:(Lemmas.mk_hook - (fun _ _ _ -> instance_hook k pri global imps ?hook)) in - (* spiwack: I don't know what to do with the status here. *) - let pstate = - if not (Option.is_empty term) then - let init_refine = - Tacticals.New.tclTHENLIST [ - Refine.refine ~typecheck:false (fun sigma -> (sigma, Option.get term)); - Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls); - Tactics.New.reduce_after_refine; - ] - in - let pstate, _ = Pfedit.by init_refine pstate in - pstate - else - let pstate, _ = Pfedit.by (Tactics.auto_intros_tac ids) pstate in - pstate - in - match tac with - | Some tac -> - let pstate, _ = Pfedit.by tac pstate in - pstate - | None -> - pstate) ()) - -let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props = - let props = - match props with - | Some (true, { CAst.v = CRecord fs }) -> - if List.length fs > List.length k.cl_props then - mismatched_props env' (List.map snd fs) k.cl_props; - Some (Inl fs) - | Some (_, t) -> Some (Inr t) - | None -> - if program_mode then Some (Inl []) - else None + instance_hook pri global imps (ConstRef cst) + +let declare_instance_program env sigma ~global ~poly id pri imps decl term termtype = + let hook _ _ vis gr = + let cst = match gr with ConstRef kn -> kn | _ -> assert false in + Impargs.declare_manual_implicits false gr imps; + let pri = intern_info pri in + let env = Global.env () in + let sigma = Evd.from_env env in + declare_instance env sigma (Some pri) (not global) (ConstRef cst) in - let subst, sigma = - match props with - | None -> - (if List.is_empty k.cl_props then Some (Inl subst) else None), sigma - | Some (Inr term) -> - let sigma, c = interp_casted_constr_evars ~program_mode env' sigma term cty in - Some (Inr (c, subst)), sigma - | Some (Inl props) -> - let get_id qid = CAst.make ?loc:qid.CAst.loc @@ qualid_basename qid in - let props, rest = - List.fold_left - (fun (props, rest) decl -> - if is_local_assum decl then - try - let is_id (id', _) = match RelDecl.get_name decl, get_id id' with - | Name id, {CAst.v=id'} -> Id.equal id id' - | Anonymous, _ -> false - in - let (loc_mid, c) = List.find is_id rest in - let rest' = List.filter (fun v -> not (is_id v)) rest - in - let {CAst.loc;v=mid} = get_id loc_mid in - List.iter (fun (n, _, x) -> - if Name.equal n (Name mid) then - Option.iter (fun x -> Dumpglob.add_glob ?loc (ConstRef x)) x) k.cl_projs; - c :: props, rest' - with Not_found -> - ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Namegen.IntroAnonymous, None)) :: props), rest - else props, rest) - ([], props) k.cl_props - in - match rest with - | (n, _) :: _ -> - unbound_method env' sigma k.cl_impl (get_id n) - | _ -> - let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in - let sigma, res = type_ctx_instance ~program_mode (push_rel_context ctx' env') sigma kcl_props props subst in - Some (Inl res), sigma + let obls, constr, typ = + match term with + | Some t -> + let termtype = EConstr.of_constr termtype in + let obls, _, constr, typ = + Obligations.eterm_obligations env id sigma 0 t termtype + in obls, Some constr, typ + | None -> [||], None, termtype in - let term, termtype = - match subst with - | None -> let termtype = it_mkProd_or_LetIn cty ctx in - None, termtype - | Some (Inl subst) -> - let subst = List.fold_left2 - (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst') - [] subst (k.cl_props @ snd k.cl_context) + let hook = DeclareDef.Hook.make hook in + let ctx = Evd.evar_universe_context sigma in + ignore(Obligations.add_definition id ?term:constr + ~univdecl:decl typ ctx ~kind:(Global ImportDefaultBehavior,poly,Instance) ~hook obls) + + +let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids term termtype = + (* spiwack: it is hard to reorder the actions to do + the pretyping after the proof has opened. As a + consequence, we use the low-level primitives to code + the refinement manually.*) + let gls = List.rev (Evd.future_goals sigma) in + let sigma = Evd.reset_future_goals sigma in + let kind = Decl_kinds.(Global ImportDefaultBehavior, poly, DefinitionBody Instance) in + let lemma = Lemmas.start_lemma id ~pl:decl kind sigma (EConstr.of_constr termtype) + ~hook:(DeclareDef.Hook.make + (fun _ _ _ -> instance_hook pri global imps ?hook)) in + (* spiwack: I don't know what to do with the status here. *) + let lemma = + if not (Option.is_empty term) then + let init_refine = + Tacticals.New.tclTHENLIST [ + Refine.refine ~typecheck:false (fun sigma -> (sigma, Option.get term)); + Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls); + Tactics.New.reduce_after_refine; + ] in - let (app, ty_constr) = instance_constructor (k,u) subst in - let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - let term = it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in - Some term, termtype - | Some (Inr (def, subst)) -> - let termtype = it_mkProd_or_LetIn cty ctx in - let term = it_mkLambda_or_LetIn def ctx in - Some term, termtype + let lemma, _ = Lemmas.by init_refine lemma in + lemma + else + let lemma, _ = Lemmas.by (Tactics.auto_intros_tac ids) lemma in + lemma + in + match tac with + | Some tac -> + let lemma, _ = Lemmas.by tac lemma in + lemma + | None -> + lemma + +let do_instance_subst_constructor_and_ty subst k u ctx = + let subst = + List.fold_left2 (fun subst' s decl -> + if is_local_assum decl then s :: subst' else subst') + [] subst (k.cl_props @ snd k.cl_context) in + let (app, ty_constr) = instance_constructor (k,u) subst in + let termtype = it_mkProd_or_LetIn ty_constr ctx in + let term = it_mkLambda_or_LetIn (Option.get app) ctx in + term, termtype + +let do_instance_resolve_TC term termtype sigma env = let sigma = Evarutil.nf_evar_map sigma in let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true env sigma in (* Try resolving fields that are typeclasses automatically. *) @@ -484,17 +422,108 @@ let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode ct (* Check that the type is free of evars now. *) Pretyping.check_evars env (Evd.from_env env) sigma termtype; let termtype = to_constr sigma termtype in - let pstate = - if not (Evd.has_undefined sigma) && not (Option.is_empty props) then - let term = to_constr sigma (Option.get term) in - (declare_instance_constant k pri global imps ?hook id decl poly sigma term termtype; - None) - else if program_mode || Option.is_empty props then - declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype - else CErrors.user_err Pp.(str "Unsolved obligations remaining.") in - id, pstate - -let interp_instance_context ~program_mode env ctx ?(generalize=false) pl tclass = + termtype, sigma + +let do_instance_type_ctx_instance props k env' ctx' sigma ~program_mode subst = + let get_id qid = CAst.make ?loc:qid.CAst.loc @@ qualid_basename qid in + let props, rest = + List.fold_left + (fun (props, rest) decl -> + if is_local_assum decl then + try + let is_id (id', _) = match RelDecl.get_name decl, get_id id' with + | Name id, {CAst.v=id'} -> Id.equal id id' + | Anonymous, _ -> false + in + let (loc_mid, c) = List.find is_id rest in + let rest' = List.filter (fun v -> not (is_id v)) rest + in + let {CAst.loc;v=mid} = get_id loc_mid in + List.iter (fun (n, _, x) -> + if Name.equal n (Name mid) then + Option.iter (fun x -> Dumpglob.add_glob ?loc (ConstRef x)) x) k.cl_projs; + c :: props, rest' + with Not_found -> + ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Namegen.IntroAnonymous, None)) :: props), rest + else props, rest) + ([], props) k.cl_props + in + match rest with + | (n, _) :: _ -> + unbound_method env' sigma k.cl_impl (get_id n) + | _ -> + let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in + let sigma, res = + type_ctx_instance ~program_mode + (push_rel_context ctx' env') sigma kcl_props props subst in + res, sigma + +let do_instance_interactive env sigma ?hook ~tac ~global ~poly cty k u ctx ctx' pri decl imps subst id = + let term, termtype = + if List.is_empty k.cl_props then + let term, termtype = + do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in + Some term, termtype + else + None, it_mkProd_or_LetIn cty ctx in + let termtype, sigma = do_instance_resolve_TC term termtype sigma env in + Flags.silently (fun () -> + declare_instance_open sigma ?hook ~tac ~global ~poly + id pri imps decl (List.map RelDecl.get_name ctx) term termtype) + () + +let do_instance env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id props = + let term, termtype, sigma = + match props with + | (true, { CAst.v = CRecord fs; loc }) -> + check_duplicate ?loc fs; + let subst, sigma = do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode:false subst in + let term, termtype = + do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in + term, termtype, sigma + | (_, term) -> + let sigma, def = + interp_casted_constr_evars ~program_mode:false env' sigma term cty in + let termtype = it_mkProd_or_LetIn cty ctx in + let term = it_mkLambda_or_LetIn def ctx in + term, termtype, sigma in + let termtype, sigma = do_instance_resolve_TC (Some term) termtype sigma env in + if Evd.has_undefined sigma then + CErrors.user_err Pp.(str "Unsolved obligations remaining.") + else + let term = to_constr sigma term in + declare_instance_constant pri global imps ?hook id decl poly sigma term termtype + +let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props = + let term, termtype, sigma = + match opt_props with + | Some (true, { CAst.v = CRecord fs; loc }) -> + check_duplicate ?loc fs; + let subst, sigma = + do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode:true subst in + let term, termtype = + do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in + Some term, termtype, sigma + | Some (_, term) -> + let sigma, def = + interp_casted_constr_evars ~program_mode:true env' sigma term cty in + let termtype = it_mkProd_or_LetIn cty ctx in + let term = it_mkLambda_or_LetIn def ctx in + Some term, termtype, sigma + | None -> + let subst, sigma = + do_instance_type_ctx_instance [] k env' ctx' sigma ~program_mode:true subst in + let term, termtype = + do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in + Some term, termtype, sigma in + let termtype, sigma = do_instance_resolve_TC term termtype sigma env in + if not (Evd.has_undefined sigma) && not (Option.is_empty opt_props) then + let term = to_constr sigma (Option.get term) in + declare_instance_constant pri global imps ?hook id decl poly sigma term termtype + else + declare_instance_program env sigma ~global ~poly id pri imps decl term termtype + +let interp_instance_context ~program_mode env ctx ~generalize pl tclass = let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in let tclass = if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass) @@ -502,8 +531,7 @@ let interp_instance_context ~program_mode env ctx ?(generalize=false) pl tclass in let sigma, (impls, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma ctx in let sigma, (c', imps') = interp_type_evars_impls ~program_mode ~impls env' sigma tclass in - let len = Context.Rel.nhyps ctx in - let imps = imps @ Impargs.lift_implicits len imps' in + let imps = imps @ imps' in let ctx', c = decompose_prod_assum sigma c' in let ctx'' = ctx' @ ctx in let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) sigma c in @@ -522,14 +550,12 @@ let interp_instance_context ~program_mode env ctx ?(generalize=false) pl tclass let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in sigma, cl, u, c', ctx', ctx, imps, args, decl -let new_instance ~pstate ?(global=false) ~program_mode - poly instid ctx cl props - ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = - let env = Global.env() in +let new_instance_common ~program_mode ~generalize env instid ctx cl = let ({CAst.loc;v=instid}, pl) = instid in let sigma, k, u, cty, ctx', ctx, imps, subst, decl = interp_instance_context ~program_mode env ~generalize ctx pl cl in + (* The name generator should not be here *) let id = match instid with | Name id -> id @@ -538,13 +564,41 @@ let new_instance ~pstate ?(global=false) ~program_mode Namegen.next_global_ident_away i (Termops.vars_of_env env) in let env' = push_rel_context ctx env in - do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode - cty k u ctx ctx' pri decl imps subst id props + id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl + +let new_instance_interactive ?(global=false) + poly instid ctx cl + ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = + let env = Global.env() in + let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl = + new_instance_common ~program_mode:false ~generalize env instid ctx cl in + id, do_instance_interactive env sigma ?hook ~tac ~global ~poly + cty k u ctx ctx' pri decl imps subst id + +let new_instance_program ?(global=false) + poly instid ctx cl opt_props + ?(generalize=true) ?hook pri = + let env = Global.env() in + let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl = + new_instance_common ~program_mode:true ~generalize env instid ctx cl in + do_instance_program env env' sigma ?hook ~global ~poly + cty k u ctx ctx' pri decl imps subst id opt_props; + id + +let new_instance ?(global=false) + poly instid ctx cl props + ?(generalize=true) ?hook pri = + let env = Global.env() in + let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl = + new_instance_common ~program_mode:false ~generalize env instid ctx cl in + do_instance env env' sigma ?hook ~global ~poly + cty k u ctx ctx' pri decl imps subst id props; + id let declare_new_instance ?(global=false) ~program_mode poly instid ctx cl pri = let env = Global.env() in let ({CAst.loc;v=instid}, pl) = instid in let sigma, k, u, cty, ctx', ctx, imps, subst, decl = - interp_instance_context ~program_mode env ctx pl cl + interp_instance_context ~program_mode ~generalize:false env ctx pl cl in - do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst instid + do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst instid diff --git a/vernac/classes.mli b/vernac/classes.mli index 8d5f3e3a06..472690cdd4 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -14,12 +14,6 @@ open Constrexpr open Typeclasses open Libnames -(** Errors *) - -val mismatched_params : env -> constr_expr list -> Constr.rel_context -> 'a - -val mismatched_props : env -> constr_expr list -> Constr.rel_context -> 'a - (** Instance declaration *) val declare_instance : ?warn:bool -> env -> Evd.evar_map -> @@ -31,34 +25,41 @@ val declare_instance : ?warn:bool -> env -> Evd.evar_map -> val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit (** globality, reference, optional priority and pattern information *) -val declare_instance_constant : - typeclass -> - Hints.hint_info_expr (** priority *) -> - bool (** globality *) -> - Impargs.manual_explicitation list (** implicits *) -> - ?hook:(GlobRef.t -> unit) -> - Id.t (** name *) -> - UState.universe_decl -> - bool (** polymorphic *) -> - Evd.evar_map (** Universes *) -> - Constr.t (** body *) -> - Constr.types (** type *) -> - unit +val new_instance_interactive + : ?global:bool (** Not global by default. *) + -> Decl_kinds.polymorphic + -> name_decl + -> local_binder_expr list + -> constr_expr + -> ?generalize:bool + -> ?tac:unit Proofview.tactic + -> ?hook:(GlobRef.t -> unit) + -> Hints.hint_info_expr + -> Id.t * Lemmas.t + +val new_instance + : ?global:bool (** Not global by default. *) + -> Decl_kinds.polymorphic + -> name_decl + -> local_binder_expr list + -> constr_expr + -> (bool * constr_expr) + -> ?generalize:bool + -> ?hook:(GlobRef.t -> unit) + -> Hints.hint_info_expr + -> Id.t -val new_instance : - pstate:Proof_global.t option - -> ?global:bool (** Not global by default. *) - -> program_mode:bool +val new_instance_program + : ?global:bool (** Not global by default. *) -> Decl_kinds.polymorphic -> name_decl -> local_binder_expr list -> constr_expr -> (bool * constr_expr) option -> ?generalize:bool - -> ?tac:unit Proofview.tactic -> ?hook:(GlobRef.t -> unit) -> Hints.hint_info_expr - -> Id.t * Proof_global.t option (* May open a proof *) + -> Id.t val declare_new_instance : ?global:bool (** Not global by default. *) diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index c37e90650a..b0297b7c51 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -37,15 +37,15 @@ let () = optwrite = (:=) axiom_into_instance; } let should_axiom_into_instance = function - | Discharge -> + | Context -> (* The typeclass behaviour of Variable and Context doesn't depend on section status *) true - | Global | Local -> !axiom_into_instance + | Definitional | Logical | Conjectural -> !axiom_into_instance let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ident} = match local with -| Discharge when Lib.sections_are_opened () -> +| Discharge -> let ctx = match ctx with | Monomorphic_entry ctx -> ctx | Polymorphic_entry (_, ctx) -> Univ.ContextSet.of_context ctx @@ -61,15 +61,14 @@ match local with let () = if is_coe then Class.try_add_new_coercion r ~local:true false in (r,Univ.Instance.empty,true) -| Global | Local | Discharge -> - let do_instance = should_axiom_into_instance local in - let local = DeclareDef.get_locality ident ~kind:"axiom" local in +| Global local -> + let do_instance = should_axiom_into_instance kind in let inl = let open Declaremods in match nl with | NoInline -> None | DefaultInline -> Some (Flags.get_inline_level()) | InlineAt i -> Some i in - let decl = (ParameterEntry (None,(c,ctx),inl), IsAssumption kind) in + let decl = (Declare.ParameterEntry (None,(c,ctx),inl), IsAssumption kind) in let kn = declare_constant ident ~local decl in let gr = ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in @@ -78,6 +77,7 @@ match local with let env = Global.env () in let sigma = Evd.from_env env in let () = if do_instance then Classes.declare_instance env sigma None false gr in + let local = match local with ImportNeedQualified -> true | ImportDefaultBehavior -> false in let () = if is_coe then Class.try_add_new_coercion gr ~local p in let inst = match ctx with | Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx @@ -124,7 +124,7 @@ let process_assumptions_udecls kind l = | (_, ([], _))::_ | [] -> assert false in let () = match kind, udecl with - | (Discharge, _, _), Some _ when Lib.sections_are_opened () -> + | (Discharge, _, _), Some _ -> let loc = first_id.CAst.loc in let msg = Pp.str "Section variables cannot be polymorphic." in user_err ?loc msg @@ -273,22 +273,24 @@ let context poly l = (* Declare the universe context once *) let decl = match b with | None -> - (ParameterEntry (None,(t,univs),None), IsAssumption Logical) + (Declare.ParameterEntry (None,(t,univs),None), IsAssumption Logical) | Some b -> let entry = Declare.definition_entry ~univs ~types:t b in - (DefinitionEntry entry, IsAssumption Logical) + (Declare.DefinitionEntry entry, IsAssumption Logical) in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in let env = Global.env () in Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (ConstRef cst); status else - let test (x, _) = match x with - | Constrexpr.ExplByPos (_, Some id') -> Id.equal id id' + let test x = match x.CAst.v with + | Some (Name id',_) -> Id.equal id id' | _ -> false in let impl = List.exists test impls in - let decl = (Discharge, poly, Definitional) in + let persistence = + if Lib.sections_are_opened () then Discharge else Global ImportDefaultBehavior in + let decl = (persistence, poly, Context) in let nstatus = match b with | None -> pi3 (declare_assumption false decl (t, univs) UnivNames.empty_binders [] impl diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 8f37bc0ba4..07e96d87a2 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 4cae4b8a74..b3cc0a4236 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -10,7 +10,6 @@ open Pp open Util -open Entries open Redexpr open Constrintern open Pretyping @@ -27,18 +26,19 @@ let warn_implicits_in_term = CWarnings.create ~name:"implicits-in-term" ~category:"implicits" (fun () -> strbrk "Implicit arguments declaration relies on type." ++ spc () ++ - strbrk "The term declares more implicits than the type here.") + strbrk "Discarding incompatible declaration in term.") let check_imps ~impsty ~impsbody = - let b = - try - List.for_all (fun (key, (va:bool*bool*bool)) -> - (* Pervasives.(=) is OK for this type *) - Pervasives.(=) (List.assoc_f Constrexpr_ops.explicitation_eq key impsty) va) - impsbody - with Not_found -> false - in - if not b then warn_implicits_in_term () + let rec aux impsty impsbody = + match impsty, impsbody with + | a1 :: impsty, a2 :: impsbody -> + (match a1.CAst.v, a2.CAst.v with + | None , None -> aux impsty impsbody + | Some _ , Some _ -> aux impsty impsbody + | _, _ -> warn_implicits_in_term ?loc:a2.CAst.loc ()) + | _ :: _, [] | [], _ :: _ -> (* Information only on one side *) () + | [], [] -> () in + aux impsty impsbody let interp_definition ~program_mode pl bl poly red_option c ctypopt = let env = Global.env() in @@ -56,11 +56,11 @@ let interp_definition ~program_mode pl bl poly red_option c ctypopt = match tyopt with | None -> let evd, (c, impsbody) = interp_constr_evars_impls ~program_mode ~impls env_bl evd c in - evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsbody, None + evd, c, imps1@impsbody, None | Some (ty, impsty) -> let evd, (c, impsbody) = interp_casted_constr_evars_impls ~program_mode ~impls env_bl evd c ty in check_imps ~impsty ~impsbody; - evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsty, Some ty + evd, c, imps1@impsty, Some ty in (* Do the reduction *) let evd, c = red_constant_body red_option env_bl evd c in @@ -85,12 +85,12 @@ let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt = in if program_mode then let env = Global.env () in - let (c,ctx), sideff = Future.force ce.const_entry_body in - assert(Safe_typing.empty_private_constants = sideff); + let (c,ctx), sideff = Future.force ce.Proof_global.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.const_entry_type with + let typ = match ce.Proof_global.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 fa4860b079..256abed6a1 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Entries open Decl_kinds open Redexpr open Constrexpr @@ -18,7 +17,7 @@ open Constrexpr val do_definition : program_mode:bool - -> ?hook:Lemmas.declaration_hook + -> ?hook:DeclareDef.Hook.t -> Id.t -> definition_kind -> universe_decl_expr option @@ -33,7 +32,13 @@ val do_definition (************************************************************************) (** Not used anywhere. *) -val interp_definition : program_mode:bool -> - universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr -> - constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * - UState.universe_decl * Impargs.manual_implicits +val interp_definition + : program_mode:bool + -> universe_decl_expr option + -> local_binder_expr list + -> polymorphic + -> red_expr option + -> constr_expr + -> constr_expr option + -> Evd.side_effects Proof_global.proof_entry * + Evd.evar_map * UState.universe_decl * Impargs.manual_implicits diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index a428c42e49..a88413cf7f 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -197,7 +197,7 @@ let interp_recursive ~program_mode ~cofix fixl notations = let fixtypes = List.map2 build_fix_type fixctxs fixccls in let fixtypes = List.map (fun c -> nf_evar sigma c) fixtypes in let fiximps = List.map3 - (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (Context.Rel.nhyps ctx) cclimps)) + (fun ctximps cclimps (_,ctx) -> ctximps@cclimps) fixctximps fixcclimps fixctxs in let sigma, rec_sign = List.fold_left2 @@ -255,79 +255,80 @@ let interp_fixpoint ~cofix l ntns = let uctx,fix = ground_fixpoint env evd fix in (fix,pl,uctx,info) -let declare_fixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns = - let pstate = - if List.exists Option.is_empty fixdefs then - (* Some bodies to define by proof *) - let thms = - List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps)))) - fixnames fixtypes fiximps in - let init_tac = - Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) - fixdefs) in - let evd = Evd.from_ctx ctx in - Some - (Lemmas.start_proof_with_initialization ~ontop (local,poly,DefinitionBody Fixpoint) - evd pl (Some(false,indexes,init_tac)) thms None) - else begin - (* We shortcut the proof process *) - let fixdefs = List.map Option.get fixdefs in - let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in - let env = Global.env() in - let indexes = search_guard env indexes fixdecls in - let fiximps = List.map (fun (n,r,p) -> r) fiximps in - let vars = Vars.universes_of_constr (mkFix ((indexes,0),fixdecls)) in - let fixdecls = - List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in - let evd = Evd.from_ctx ctx in - let evd = Evd.restrict_universe_context evd vars in - let ctx = Evd.check_univ_decl ~poly evd pl in - let pl = Evd.universe_binders evd in - let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in - ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx) - fixnames fixdecls fixtypes fiximps); - (* Declare the recursive definitions *) - fixpoint_message (Some indexes) fixnames; - None - end in - (* Declare notations *) - List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; - pstate - -let declare_cofixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = - let pstate = - if List.exists Option.is_empty fixdefs then - (* Some bodies to define by proof *) - let thms = - List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps)))) - fixnames fixtypes fiximps in - let init_tac = - Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) - fixdefs) in - let evd = Evd.from_ctx ctx in - Some (Lemmas.start_proof_with_initialization ~ontop (Global,poly, DefinitionBody CoFixpoint) - evd pl (Some(true,[],init_tac)) thms None) - else begin - (* We shortcut the proof process *) - let fixdefs = List.map Option.get fixdefs in - let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in - let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in - let vars = Vars.universes_of_constr (List.hd fixdecls) in - let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in - let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in - let evd = Evd.from_ctx ctx in - let evd = Evd.restrict_universe_context evd vars in - let ctx = Evd.check_univ_decl ~poly evd pl in - let pl = Evd.universe_binders evd in - ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx) - fixnames fixdecls fixtypes fiximps); - (* Declare the recursive definitions *) - cofixpoint_message fixnames; - None - end in - (* Declare notations *) - List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; - pstate +let declare_fixpoint_notations ntns = + List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns + +let declare_fixpoint_interactive local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns = + (* Some bodies to define by proof *) + let thms = + List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps)))) + fixnames fixtypes fiximps in + let init_tac = + Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) + fixdefs) in + let evd = Evd.from_ctx ctx in + let lemma = Lemmas.start_lemma_with_initialization (local,poly,DefinitionBody Fixpoint) + evd pl (Some(false,indexes,init_tac)) thms None in + declare_fixpoint_notations ntns; + lemma + +let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns = + (* We shortcut the proof process *) + let fixdefs = List.map Option.get fixdefs in + let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in + let env = Global.env() in + let indexes = search_guard env indexes fixdecls in + let fiximps = List.map (fun (n,r,p) -> r) fiximps in + let vars = Vars.universes_of_constr (mkFix ((indexes,0),fixdecls)) in + let fixdecls = + List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in + let evd = Evd.from_ctx ctx in + let evd = Evd.restrict_universe_context evd vars in + let ctx = Evd.check_univ_decl ~poly evd pl in + let pl = Evd.universe_binders evd in + let mk_pure c = (c, Univ.ContextSet.empty), Evd.empty_side_effects in + let fixdecls = List.map mk_pure fixdecls in + ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx) + fixnames fixdecls fixtypes fiximps); + (* Declare the recursive definitions *) + fixpoint_message (Some indexes) fixnames; + declare_fixpoint_notations ntns + +let declare_cofixpoint_notations = declare_fixpoint_notations + +let declare_cofixpoint_interactive local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = + (* Some bodies to define by proof *) + let thms = + List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps)))) + fixnames fixtypes fiximps in + let init_tac = + Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) + fixdefs) in + let evd = Evd.from_ctx ctx in + let lemma = Lemmas.start_lemma_with_initialization + (Global ImportDefaultBehavior,poly, DefinitionBody CoFixpoint) + evd pl (Some(true,[],init_tac)) thms None in + declare_cofixpoint_notations ntns; + lemma + +let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = + (* We shortcut the proof process *) + let fixdefs = List.map Option.get fixdefs in + let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in + let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in + let vars = Vars.universes_of_constr (List.hd fixdecls) in + let mk_pure c = (c, Univ.ContextSet.empty), Evd.empty_side_effects in + let fixdecls = List.map mk_pure fixdecls in + let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in + let evd = Evd.from_ctx ctx in + let evd = Evd.restrict_universe_context evd vars in + let ctx = Evd.check_univ_decl ~poly evd pl in + let pl = Evd.universe_binders evd in + ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx) + fixnames fixdecls fixtypes fiximps); + (* Declare the recursive definitions *) + cofixpoint_message fixnames; + declare_cofixpoint_notations ntns let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v with | CStructRec na -> na @@ -366,18 +367,33 @@ let check_safe () = let flags = Environ.typing_flags (Global.env ()) in flags.check_universes && flags.check_guarded -let do_fixpoint ~ontop local poly l = +let do_fixpoint_common l = let fixl, ntns = extract_fixpoint_components ~structonly:true l in let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in - let possible_indexes = - List.map compute_possible_guardness_evidences info in - let pstate = declare_fixpoint ~ontop local poly fix possible_indexes ntns in + fixl, ntns, fix, List.map compute_possible_guardness_evidences info + +let do_fixpoint_interactive local poly l = + let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in + let pstate = declare_fixpoint_interactive local poly fix possible_indexes ntns in if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else (); pstate -let do_cofixpoint ~ontop local poly l = +let do_fixpoint local poly l = + let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in + declare_fixpoint local poly fix possible_indexes ntns; + if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () + +let do_cofixpoint_common l = let fixl,ntns = extract_cofixpoint_components l in - let cofix = interp_fixpoint ~cofix:true fixl ntns in - let pstate = declare_cofixpoint ~ontop local poly cofix ntns in + ntns, interp_fixpoint ~cofix:true fixl ntns + +let do_cofixpoint_interactive local poly l = + let ntns, cofix = do_cofixpoint_common l in + let pstate = declare_cofixpoint_interactive local poly cofix ntns in if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else (); pstate + +let do_cofixpoint local poly l = + let ntns, cofix = do_cofixpoint_common l in + declare_cofixpoint local poly cofix ntns; + if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index 5937842f17..b42e877d41 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -18,15 +18,17 @@ open Vernacexpr (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) +val do_fixpoint_interactive : + locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Lemmas.t + val do_fixpoint : - ontop:Proof_global.t option -> - (* When [false], assume guarded. *) - locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Proof_global.t option + locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit + +val do_cofixpoint_interactive : + locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Lemmas.t val do_cofixpoint : - ontop:Proof_global.t option -> - (* When [false], assume guarded. *) - locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Proof_global.t option + locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit (************************************************************************) (** Internal API *) @@ -55,7 +57,7 @@ val interp_recursive : (* names / defs / types *) (Id.t list * Sorts.relevance list * EConstr.constr option list * EConstr.types list) * (* ctx per mutual def / implicits / struct annotations *) - (EConstr.rel_context * Impargs.manual_explicitation list * int option) list + (EConstr.rel_context * Impargs.manual_implicits * int option) list (** Exported for Funind *) @@ -83,20 +85,17 @@ val interp_fixpoint : (** [Not used so far] *) val declare_fixpoint : - ontop:Proof_global.t option -> locality -> polymorphic -> recursive_preentry * UState.universe_decl * UState.t * (Constr.rel_context * Impargs.manual_implicits * int option) list -> - Proof_global.lemma_possible_guards -> decl_notation list -> - Proof_global.t option + Lemmas.lemma_possible_guards -> decl_notation list -> + unit val declare_cofixpoint : - ontop:Proof_global.t option -> locality -> polymorphic -> recursive_preentry * UState.universe_decl * UState.t * (Constr.rel_context * Impargs.manual_implicits * int option) list -> - decl_notation list -> - Proof_global.t option + decl_notation list -> unit (** Very private function, do not use *) val compute_possible_guardness_evidences : diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 977e804da2..363ba5beff 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -121,7 +121,7 @@ let mk_mltype_data sigma env assums arity indname = let rec check_anonymous_type ind = let open Glob_term in match DAst.get ind with - | GSort (GType []) -> true + | GSort (UAnonymous {rigid=true}) -> true | GProd ( _, _, _, e) | GLetIn (_, _, _, e) | GLambda (_, _, _, e) @@ -375,8 +375,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not let env_ar_params = EConstr.push_rel_context ctx_params env_ar in (* Compute interpretation metadatas *) - let indimpls = List.map (fun impls -> userimpls @ - lift_implicits (Context.Rel.nhyps ctx_params) impls) indimpls in + let indimpls = List.map (fun impls -> userimpls @ impls) indimpls in let impls = compute_internalization_env env_uparams sigma ~impls (Inductive (params,true)) indnames fullarities indimpls in let ntn_impls = compute_internalization_env env_uparams sigma (Inductive (params,true)) indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data sigma env_params params) arities indnames in @@ -402,8 +401,8 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not constructors in let ctx_params = ctx_params @ ctx_uparams in - let userimpls = useruimpls @ (lift_implicits (Context.Rel.nhyps ctx_uparams) userimpls) in - let indimpls = List.map (fun iimpl -> useruimpls @ (lift_implicits (Context.Rel.nhyps ctx_uparams) iimpl)) indimpls in + let userimpls = useruimpls @ userimpls in + let indimpls = List.map (fun iimpl -> useruimpls @ iimpl) indimpls in let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_uparams) fullarities in let env_ar = push_types env0 indnames relevances fullarities in let env_ar_params = EConstr.push_rel_context ctx_params env_ar in @@ -450,10 +449,9 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not indl arities arityconcl constructors in let impls = - let len = Context.Rel.nhyps ctx_params in List.map2 (fun indimpls (_,_,cimpls) -> indimpls, List.map (fun impls -> - userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors + userimpls @ impls) cimpls) indimpls constructors in let variance = if poly && cum then Some (InferCumulativity.dummy_variance uctx) else None in (* Build the mutual inductive entry *) @@ -495,7 +493,7 @@ let extract_params indl = let extract_inductive indl = List.map (fun ({CAst.v=indname},_,ar,lc) -> { ind_name = indname; - ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (Glob_term.GType [])) ar; + ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (Glob_term.UAnonymous {rigid=true})) ar; ind_lc = List.map (fun (_,({CAst.v=id},t)) -> (id,t)) lc }) indl @@ -559,8 +557,8 @@ let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie p mind type one_inductive_impls = - Impargs.manual_explicitation list (* for inds *)* - Impargs.manual_explicitation list list (* for constrs *) + Impargs.manual_implicits (* for inds *) * + Impargs.manual_implicits list (* for constrs *) type uniform_inductive_flag = | UniformParameters diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 224cce67ad..2d6ecf48ef 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 69e2a209eb..6c1c23eacb 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -13,7 +13,6 @@ open CErrors open Util open Constr open Context -open Entries open Vars open Declare open Names @@ -229,7 +228,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = in hook, recname, typ in (* XXX: Capturing sigma here... bad bad *) - let hook = Lemmas.mk_hook (hook sigma) in + let hook = DeclareDef.Hook.make (hook sigma) in Obligations.check_evars env sigma; let evars, _, evars_def, evars_typ = Obligations.eterm_obligations env recname sigma 0 def typ @@ -248,7 +247,7 @@ let collect_evars_of_term evd c ty = evars (Evd.from_ctx (Evd.evar_universe_context evd)) let do_program_recursive local poly fixkind fixl ntns = - let cofix = fixkind = Obligations.IsCoFixpoint in + let cofix = fixkind = DeclareObl.IsCoFixpoint in let (env, rec_sign, pl, evd), fix, info = interp_recursive ~cofix ~program_mode:true fixl ntns in @@ -289,8 +288,8 @@ let do_program_recursive local poly fixkind fixl ntns = end in let ctx = Evd.evar_universe_context evd in let kind = match fixkind with - | Obligations.IsFixpoint _ -> (local, poly, Fixpoint) - | Obligations.IsCoFixpoint -> (local, poly, CoFixpoint) + | DeclareObl.IsFixpoint _ -> (local, poly, Fixpoint) + | DeclareObl.IsCoFixpoint -> (local, poly, CoFixpoint) in Obligations.add_mutual_definitions defs ~kind ~univdecl:pl ctx ntns fixkind @@ -316,7 +315,7 @@ let do_program_fixpoint local poly l = | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g -> let fixl,ntns = extract_fixpoint_components ~structonly:true l in - let fixkind = Obligations.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in + let fixkind = DeclareObl.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in do_program_recursive local poly fixkind fixl ntns | _, _ -> @@ -341,5 +340,5 @@ let do_fixpoint local poly l = let do_cofixpoint local poly l = let fixl,ntns = extract_cofixpoint_components l in - do_program_recursive local poly Obligations.IsCoFixpoint fixl ntns; + do_program_recursive local poly DeclareObl.IsCoFixpoint fixl ntns; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index bdda3314ca..a467c22ede 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -10,31 +10,39 @@ open Decl_kinds open Declare -open Entries open Globnames open Impargs -let warn_local_declaration = - CWarnings.create ~name:"local-declaration" ~category:"scope" - Pp.(fun (id,kind) -> - Names.Id.print id ++ strbrk " is declared as a local " ++ str kind) +(* Hooks naturally belong here as they apply to both definitions and lemmas *) +module Hook = struct + module S = struct + type t = UState.t + -> (Names.Id.t * Constr.t) list + -> Decl_kinds.locality + -> Names.GlobRef.t + -> unit + end -let get_locality id ~kind = function -| Discharge -> - (* If a Let is defined outside a section, then we consider it as a local definition *) - warn_local_declaration (id,kind); - true -| Local -> true -| Global -> false + type t = S.t CEphemeron.key + let make hook = CEphemeron.create hook + + let call ?hook ?fix_exn uctx trans l c = + try Option.iter (fun hook -> CEphemeron.get hook uctx trans l c) hook + with e when CErrors.noncritical e -> + let e = CErrors.push e in + let e = Option.cata (fun fix -> fix e) e fix_exn in + Util.iraise e +end + +(* Locality stuff *) let declare_definition ident (local, p, k) ?hook_data ce pl imps = - let fix_exn = Future.fix_exn_of ce.const_entry_body in + let fix_exn = Future.fix_exn_of ce.Proof_global.proof_entry_body in let gr = match local with - | Discharge when Lib.sections_are_opened () -> + | Discharge -> let _ = declare_variable ident (Lib.cwd(), SectionLocalDef ce, IsDefinition k) in VarRef ident - | Discharge | Local | Global -> - let local = get_locality ident ~kind:"definition" local in + | Global local -> let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in let gr = ConstRef kn in let () = Declare.declare_univ_binders gr pl in @@ -46,7 +54,7 @@ let declare_definition ident (local, p, k) ?hook_data ce pl imps = match hook_data with | None -> () | Some (hook, uctx, extra_defs) -> - Lemmas.call_hook ~fix_exn ~hook uctx extra_defs local gr + Hook.call ~fix_exn ~hook uctx extra_defs local gr end; gr diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index c4500d0a6b..ac4f44608b 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -11,25 +11,51 @@ open Names open Decl_kinds -val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool +(** Declaration hooks *) +module Hook : sig + type t + + (** Hooks allow users of the API to perform arbitrary actions at + proof/definition saving time. For example, to register a constant + as a Coercion, perform some cleanup, update the search database, + etc... *) + module S : sig + (** [S.t] passes to the client: *) + type t + = UState.t + (** [ustate]: universe constraints obtained when the term was closed *) + -> (Id.t * Constr.t) list + (** [(n1,t1),...(nm,tm)]: association list between obligation + name and the corresponding defined term (might be a constant, + but also an arbitrary term in the Expand case of obligations) *) + -> Decl_kinds.locality + (** [locality]: Locality of the original declaration *) + -> GlobRef.t + (** [ref]: identifier of the origianl declaration *) + -> unit + end + + val make : S.t -> t + val call : ?hook:t -> ?fix_exn:Future.fix_exn -> S.t +end val declare_definition : Id.t -> definition_kind - -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list) - -> Safe_typing.private_constants Entries.definition_entry + -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) + -> Evd.side_effects Proof_global.proof_entry -> UnivNames.universe_binders -> Impargs.manual_implicits -> GlobRef.t val declare_fix : ?opaque:bool - -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list) + -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) -> definition_kind -> UnivNames.universe_binders -> Entries.universes_entry -> Id.t - -> Safe_typing.private_constants Entries.proof_output + -> Evd.side_effects Entries.proof_output -> Constr.types -> Impargs.manual_implicits -> GlobRef.t @@ -38,7 +64,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 * Safe_typing.private_constants Entries.definition_entry + Evd.evar_map * Evd.side_effects Proof_global.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 new file mode 100644 index 0000000000..4936c9838d --- /dev/null +++ b/vernac/declareObl.ml @@ -0,0 +1,562 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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 Environ +open Context +open Constr +open Vars +open Decl_kinds +open Entries + +type 'a obligation_body = DefinedObl of 'a | TermObl of constr + +type obligation = + { obl_name : Id.t + ; obl_type : types + ; obl_location : Evar_kinds.t Loc.located + ; obl_body : pconstant obligation_body option + ; obl_status : bool * Evar_kinds.obligation_definition_status + ; obl_deps : Int.Set.t + ; obl_tac : unit Proofview.tactic option } + +type obligations = obligation array * int + +type notations = + (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list + +type fixpoint_kind = + | IsFixpoint of lident option list + | IsCoFixpoint + +type program_info = + { prg_name : Id.t + ; prg_body : constr + ; prg_type : constr + ; prg_ctx : UState.t + ; prg_univdecl : UState.universe_decl + ; prg_obligations : obligations + ; prg_deps : Id.t list + ; prg_fixkind : fixpoint_kind option + ; prg_implicits : Impargs.manual_implicits + ; prg_notations : notations + ; prg_kind : definition_kind + ; prg_reduce : constr -> constr + ; prg_hook : DeclareDef.Hook.t option + ; prg_opaque : bool + ; prg_sign : named_context_val } + +(* Saving an obligation *) + +let get_shrink_obligations = + Goptions.declare_bool_option_and_ref ~depr:true (* remove in 8.8 *) + ~name:"Shrinking of Program obligations" ~key:["Shrink"; "Obligations"] + ~value:true + +(* XXX: Is this the right place for this? *) +let it_mkLambda_or_LetIn_or_clean t ctx = + let open Context.Rel.Declaration in + let fold t decl = + if is_local_assum decl then Term.mkLambda_or_LetIn decl t + else if noccurn 1 t then subst1 mkProp t + else Term.mkLambda_or_LetIn decl t + in + Context.Rel.fold_inside fold ctx ~init:t + +(* XXX: Is this the right place for this? *) +let decompose_lam_prod c ty = + let open Context.Rel.Declaration in + let rec aux ctx c ty = + match (Constr.kind c, Constr.kind ty) with + | LetIn (x, b, t, c), LetIn (x', b', t', ty) + when Constr.equal b b' && Constr.equal t t' -> + let ctx' = Context.Rel.add (LocalDef (x, b', t')) ctx in + aux ctx' c ty + | _, LetIn (x', b', t', ty) -> + let ctx' = Context.Rel.add (LocalDef (x', b', t')) ctx in + aux ctx' (lift 1 c) ty + | LetIn (x, b, t, c), _ -> + let ctx' = Context.Rel.add (LocalDef (x, b, t)) ctx in + aux ctx' c (lift 1 ty) + | Lambda (x, b, t), Prod (x', b', t') + (* By invariant, must be convertible *) -> + let ctx' = Context.Rel.add (LocalAssum (x, b')) ctx in + aux ctx' t t' + | Cast (c, _, _), _ -> aux ctx c ty + | _, _ -> (ctx, c, ty) + in + aux Context.Rel.empty c ty + +(* XXX: What's the relation of this with Abstract.shrink ? *) +let shrink_body c ty = + let ctx, b, ty = + match ty with + | None -> + let ctx, b = Term.decompose_lam_assum c in + (ctx, b, None) + | Some ty -> + let ctx, b, ty = decompose_lam_prod c ty in + (ctx, b, Some ty) + in + let b', ty', n, args = + List.fold_left + (fun (b, ty, i, args) decl -> + if noccurn 1 b && Option.cata (noccurn 1) true ty then + (subst1 mkProp b, Option.map (subst1 mkProp) ty, succ i, args) + else + let open Context.Rel.Declaration in + let args = if is_local_assum decl then mkRel i :: args else args in + ( Term.mkLambda_or_LetIn decl b + , Option.map (Term.mkProd_or_LetIn decl) ty + , succ i + , args ) ) + (b, ty, 1, []) ctx + in + (ctx, b', ty', Array.of_list args) + +let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst] + +let add_hint local prg cst = + Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst) + +(***********************************************************************) +(* Saving an obligation *) +(***********************************************************************) + +(* true = hide obligations *) +let get_hide_obligations = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"Hidding of Program obligations" + ~key:["Hide"; "Obligations"] + ~value:false + +let declare_obligation prg obl body ty uctx = + let body = prg.prg_reduce body in + let ty = Option.map prg.prg_reduce ty in + match obl.obl_status with + | _, Evar_kinds.Expand -> (false, {obl with obl_body = Some (TermObl body)}) + | force, Evar_kinds.Define opaque -> + let opaque = (not force) && opaque in + let poly = pi2 prg.prg_kind in + let ctx, body, ty, args = + 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 = + Proof_global.{ 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 + (* ppedrot: seems legit to have obligations as local *) + let constant = + Declare.declare_constant obl.obl_name ~local:ImportNeedQualified + (Declare.DefinitionEntry ce, IsProof Property) + in + if not opaque then + add_hint (Locality.make_section_locality None) prg constant; + Declare.definition_message obl.obl_name; + let body = + match uctx with + | Polymorphic_entry (_, uctx) -> + Some (DefinedObl (constant, Univ.UContext.instance uctx)) + | Monomorphic_entry _ -> + Some + (TermObl + (it_mkLambda_or_LetIn_or_clean + (mkApp (mkConst constant, args)) + ctx)) + in + (true, {obl with obl_body = body}) + +(* Updating the obligation meta-info on close *) + +let not_transp_msg = + Pp.( + str "Obligation should be transparent but was declared opaque." + ++ spc () + ++ str "Use 'Defined' instead.") + +let pperror cmd = CErrors.user_err ~hdr:"Program" cmd +let err_not_transp () = pperror not_transp_msg + +module ProgMap = Id.Map + +let from_prg, program_tcc_summary_tag = + Summary.ref_tag ProgMap.empty ~name:"program-tcc-table" + +(* In all cases, the use of the map is read-only so we don't expose the ref *) +let get_prg_info_map () = !from_prg + +let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] + +let close sec = + if not (ProgMap.is_empty !from_prg) then + let keys = map_keys !from_prg in + CErrors.user_err ~hdr:"Program" + Pp.( + str "Unsolved obligations when closing " + ++ str sec ++ str ":" ++ spc () + ++ prlist_with_sep spc (fun x -> Id.print x) keys + ++ ( str (if Int.equal (List.length keys) 1 then " has " else " have ") + ++ str "unsolved obligations" )) + +let input : program_info CEphemeron.key ProgMap.t -> Libobject.obj = + let open Libobject in + declare_object + { (default_object "Program state") with + cache_function = (fun (na, pi) -> from_prg := pi) + ; load_function = (fun _ (_, pi) -> from_prg := pi) + ; discharge_function = + (fun _ -> + close "section"; + None ) + ; classify_function = + (fun _ -> + close "module"; + Dispose ) } + +let map_replace k v m = + ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m) + +let progmap_remove prg = + Lib.add_anonymous_leaf (input (ProgMap.remove prg.prg_name !from_prg)) + +let progmap_add n prg = + Lib.add_anonymous_leaf (input (ProgMap.add n prg !from_prg)) + +let progmap_replace prg' = + Lib.add_anonymous_leaf (input (map_replace prg'.prg_name prg' !from_prg)) + +let obligations_solved prg = Int.equal (snd prg.prg_obligations) 0 + +let obligations_message rem = + if rem > 0 then + if Int.equal rem 1 then + Flags.if_verbose Feedback.msg_info + Pp.(int rem ++ str " obligation remaining") + else + Flags.if_verbose Feedback.msg_info + Pp.(int rem ++ str " obligations remaining") + else + Flags.if_verbose Feedback.msg_info Pp.(str "No more obligations remaining") + +type progress = Remain of int | Dependent | Defined of GlobRef.t + +let get_obligation_body expand obl = + match obl.obl_body with + | None -> None + | Some c -> ( + if expand && snd obl.obl_status == Evar_kinds.Expand then + match c with + | DefinedObl pc -> Some (constant_value_in (Global.env ()) pc) + | TermObl c -> Some c + else + match c with DefinedObl pc -> Some (mkConstU pc) | TermObl c -> Some c ) + +let obl_substitution expand obls deps = + Int.Set.fold + (fun x acc -> + let xobl = obls.(x) in + match get_obligation_body expand xobl with + | None -> acc + | Some oblb -> (xobl.obl_name, (xobl.obl_type, oblb)) :: acc ) + deps [] + +let rec intset_to = function + | -1 -> Int.Set.empty + | n -> Int.Set.add n (intset_to (pred n)) + +let obligation_substitution expand prg = + let obls, _ = prg.prg_obligations in + let ints = intset_to (pred (Array.length obls)) in + obl_substitution expand obls ints + +let hide_obligation () = + Coqlib.check_required_library ["Coq"; "Program"; "Tactics"]; + UnivGen.constr_of_monomorphic_global + (Coqlib.lib_ref "program.tactics.obligation") + +(* XXX: Is this the right place? *) +let rec prod_app t n = + match + Constr.kind + (EConstr.Unsafe.to_constr + (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) + (* FIXME *) + with + | Prod (_, _, b) -> subst1 n b + | LetIn (_, b, t, b') -> prod_app (subst1 b b') n + | _ -> + CErrors.user_err ~hdr:"prod_app" + Pp.(str "Needed a product, but didn't find one" ++ fnl ()) + +(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *) +let prod_applist t nL = List.fold_left prod_app t nL + +let replace_appvars subst = + let rec aux c = + let f, l = decompose_app c in + if isVar f then + try + let c' = List.map (Constr.map aux) l in + let t, b = Id.List.assoc (destVar f) subst in + mkApp + ( delayed_force hide_obligation + , [|prod_applist t c'; Term.applistc b c'|] ) + with Not_found -> Constr.map aux c + else Constr.map aux c + in + Constr.map aux + +let subst_prog subst prg = + if get_hide_obligations () then + ( replace_appvars subst prg.prg_body + , replace_appvars subst (* Termops.refresh_universes *) prg.prg_type ) + else + let subst' = List.map (fun (n, (_, b)) -> (n, b)) subst in + ( Vars.replace_vars subst' prg.prg_body + , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_type ) + +let get_fix_exn, stm_get_fix_exn = Hook.make () + +let declare_definition prg = + let varsubst = obligation_substitution true prg in + let body, typ = subst_prog varsubst prg in + let nf = + UnivSubst.nf_evars_and_universes_opt_subst + (fun x -> None) + (UState.subst prg.prg_ctx) + in + let opaque = prg.prg_opaque in + let fix_exn = Hook.get get_fix_exn () in + let typ = nf typ in + let body = nf body in + let obls = List.map (fun (id, (_, c)) -> (id, nf c)) varsubst in + let uvars = + Univ.LSet.union + (Vars.universes_of_constr typ) + (Vars.universes_of_constr body) + in + let uctx = UState.restrict prg.prg_ctx uvars in + let univs = + UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl + in + let ce = Declare.definition_entry ~fix_exn ~opaque ~types:typ ~univs body in + let () = progmap_remove prg in + let ubinders = UState.universe_binders uctx in + let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in + DeclareDef.declare_definition prg.prg_name prg.prg_kind ce ubinders + prg.prg_implicits ?hook_data + +let rec lam_index n t acc = + match Constr.kind t with + | Lambda ({binder_name=Name n'}, _, _) when Id.equal n n' -> acc + | Lambda (_, _, b) -> lam_index n b (succ acc) + | _ -> raise Not_found + +let compute_possible_guardness_evidences n fixbody fixtype = + match n with + | Some {CAst.loc; v = n} -> [lam_index n fixbody 0] + | None -> + (* If recursive argument was not given by user, we try all args. + An earlier approach was to look only for inductive arguments, + but doing it properly involves delta-reduction, and it finally + doesn't seem to worth the effort (except for huge mutual + fixpoints ?) *) + let m = + Termops.nb_prod Evd.empty (EConstr.of_constr fixtype) + (* FIXME *) + in + let ctx = fst (Term.decompose_prod_n_assum m fixtype) in + List.map_i (fun i _ -> i) 0 ctx + +let mk_proof c = + ((c, Univ.ContextSet.empty), Evd.empty_side_effects) + +let declare_mutual_definition l = + let len = List.length l in + let first = List.hd l in + let defobl x = + let oblsubst = obligation_substitution true x in + let subs, typ = subst_prog oblsubst x in + let env = Global.env () in + let sigma = Evd.from_ctx x.prg_ctx in + let r = Retyping.relevance_of_type env sigma (EConstr.of_constr typ) in + let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) in + let typ = snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) in + let term = EConstr.to_constr sigma term in + let typ = EConstr.to_constr sigma typ in + let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_implicits) in + let oblsubst = List.map (fun (id, (_, c)) -> (id, c)) oblsubst in + def, oblsubst + in + let defs, obls = + List.fold_right (fun x (defs, obls) -> + let xdef, xobls = defobl x in + (xdef :: defs, xobls @ obls)) l ([], []) + in + (* let fixdefs = List.map reduce_fix fixdefs in *) + let fixdefs, fixrs,fixtypes, fiximps = List.split4 defs in + let fixkind = Option.get first.prg_fixkind in + let arrrec, recvec = (Array.of_list fixtypes, Array.of_list fixdefs) in + let rvec = Array.of_list fixrs in + let namevec = Array.of_list (List.map (fun x -> Name x.prg_name) l) in + let fixdecls = (Array.map2 make_annot namevec rvec, arrrec, recvec) in + let local, poly, kind = first.prg_kind in + let fixnames = first.prg_deps in + let opaque = first.prg_opaque in + let kind = if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in + let indexes, fixdecls = + match fixkind with + | IsFixpoint wfl -> + let possible_indexes = + List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes + in + let indexes = + Pretyping.search_guard (Global.env ()) possible_indexes fixdecls + in + ( Some indexes + , List.map_i (fun i _ -> mk_proof (mkFix ((indexes, i), fixdecls))) 0 l + ) + | IsCoFixpoint -> + (None, List.map_i (fun i _ -> mk_proof (mkCoFix (i, fixdecls))) 0 l) + in + (* Declare the recursive definitions *) + let univs = UState.univ_entry ~poly first.prg_ctx in + let fix_exn = Hook.get get_fix_exn () in + let kns = + List.map4 + (DeclareDef.declare_fix ~opaque (local, poly, kind) + UnivNames.empty_binders univs) + fixnames fixdecls fixtypes fiximps + in + (* Declare notations *) + List.iter + (Metasyntax.add_notation_interpretation (Global.env ())) + first.prg_notations; + Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; + let gr = List.hd kns in + DeclareDef.Hook.call ?hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr; + List.iter progmap_remove l; + gr + +let update_obls prg obls rem = + let prg' = {prg with prg_obligations = (obls, rem)} in + progmap_replace prg'; + obligations_message rem; + if rem > 0 then Remain rem + else + match prg'.prg_deps with + | [] -> + let kn = declare_definition prg' in + progmap_remove prg'; + Defined kn + | l -> + let progs = + List.map + (fun x -> CEphemeron.get (ProgMap.find x !from_prg)) + prg'.prg_deps + in + if List.for_all (fun x -> obligations_solved x) progs then + let kn = declare_mutual_definition progs in + Defined kn + else Dependent + +let dependencies obls n = + let res = ref Int.Set.empty in + Array.iteri + (fun i obl -> + if (not (Int.equal i n)) && Int.Set.mem n obl.obl_deps then + res := Int.Set.add i !res ) + obls; + !res + +type obligation_qed_info = + { name : Id.t + ; num : int + ; auto : Id.t option -> Int.Set.t -> unit Proofview.tactic option -> progress + } + +let obligation_terminator opq 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 (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 + Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body); + (* Declare the obligation ourselves and drop the hook *) + let prg = CEphemeron.get (ProgMap.find name !from_prg) in + (* Ensure universes are substituted properly in body and type *) + let body = EConstr.to_constr sigma (EConstr.of_constr body) in + let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in + let ctx = Evd.evar_universe_context sigma in + let obls, rem = prg.prg_obligations in + let obl = obls.(num) in + let status = + match obl.obl_status, opq with + | (_, Evar_kinds.Expand), Opaque -> err_not_transp () + | (true, _), Opaque -> err_not_transp () + | (false, _), Opaque -> Evar_kinds.Define true + | (_, Evar_kinds.Define true), Transparent -> + Evar_kinds.Define false + | (_, status), Transparent -> status + in + let obl = { obl with obl_status = false, status } in + let ctx = + if pi2 prg.prg_kind then ctx + else UState.union prg.prg_ctx ctx + in + let uctx = UState.univ_entry ~poly:(pi2 prg.prg_kind) ctx in + let (defined, obl) = declare_obligation prg obl body ty uctx in + let obls = Array.copy obls in + let () = obls.(num) <- obl in + let prg_ctx = + if pi2 (prg.prg_kind) then (* Polymorphic *) + (* We merge the new universes and constraints of the + polymorphic obligation with the existing ones *) + UState.union prg.prg_ctx ctx + else + (* The first obligation, if defined, + declares the univs of the constant, + each subsequent obligation declares its own additional + universes and constraints if any *) + if defined then UState.make (Global.universes ()) + else ctx + in + let prg = {prg with prg_ctx} in + begin try + ignore (update_obls prg obls (pred rem)); + if pred rem > 0 then + let deps = dependencies obls num in + if not (Int.Set.is_empty deps) then + ignore (auto (Some name) deps None) + with e when CErrors.noncritical e -> + let e = CErrors.push e in + pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e)) + end + | _ -> + CErrors.anomaly + Pp.( + str + "[obligation_terminator] close_proof returned more than one proof \ + term") diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli new file mode 100644 index 0000000000..f4495181b3 --- /dev/null +++ b/vernac/declareObl.mli @@ -0,0 +1,114 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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 Names +open Constr + +type 'a obligation_body = DefinedObl of 'a | TermObl of constr + +type obligation = + { obl_name : Id.t + ; obl_type : types + ; obl_location : Evar_kinds.t Loc.located + ; obl_body : pconstant obligation_body option + ; obl_status : bool * Evar_kinds.obligation_definition_status + ; obl_deps : Int.Set.t + ; obl_tac : unit Proofview.tactic option } + +type obligations = obligation array * int + +type notations = + (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list + +type fixpoint_kind = + | IsFixpoint of lident option list + | IsCoFixpoint + +type program_info = + { prg_name : Id.t + ; prg_body : constr + ; prg_type : constr + ; prg_ctx : UState.t + ; prg_univdecl : UState.universe_decl + ; prg_obligations : obligations + ; prg_deps : Id.t list + ; prg_fixkind : fixpoint_kind option + ; prg_implicits : Impargs.manual_implicits + ; prg_notations : notations + ; prg_kind : Decl_kinds.definition_kind + ; prg_reduce : constr -> constr + ; prg_hook : DeclareDef.Hook.t option + ; prg_opaque : bool + ; prg_sign : Environ.named_context_val } + +val declare_obligation : + program_info + -> obligation + -> Constr.types + -> Constr.types option + -> Entries.universes_entry + -> bool * obligation +(** [declare_obligation] Save an obligation *) + +module ProgMap : CMap.ExtS with type key = Id.t and module Set := Id.Set + +val declare_definition : program_info -> Names.GlobRef.t + +type progress = + (* Resolution status of a program *) + | Remain of int + (* n obligations remaining *) + | Dependent + (* Dependent on other definitions *) + | Defined of GlobRef.t + (* Defined as id *) + +type obligation_qed_info = + { name : Id.t + ; num : int + ; auto : Id.t option -> Int.Set.t -> unit Proofview.tactic option -> progress + } + +val obligation_terminator + : Proof_global.opacity_flag + -> Evd.side_effects Proof_global.proof_entry list + -> UState.t + -> obligation_qed_info -> unit +(** [obligation_terminator] part 2 of saving an obligation *) + +val update_obls : + program_info + -> obligation array + -> int + -> progress +(** [update_obls prg obls n progress] What does this do? *) + +(** { 2 Util } *) + +val get_prg_info_map : unit -> program_info CEphemeron.key ProgMap.t + +val program_tcc_summary_tag : + program_info CEphemeron.key Id.Map.t Summary.Dyn.tag + +val obl_substitution : + bool + -> obligation array + -> Int.Set.t + -> (ProgMap.key * (Constr.types * Constr.types)) list + +val dependencies : obligation array -> int -> Int.Set.t + +val err_not_transp : unit -> unit +val progmap_add : ProgMap.key -> program_info CEphemeron.key -> unit + +(* This is a hack to make it possible for Obligations to craft a Qed + * behind the scenes. The fix_exn the Stm attaches to the Future proof + * is not available here, so we provide a side channel to get it *) +val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) Hook.t diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 9bc225475d..c9d9b65e04 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/egramcoq.mli b/vernac/egramcoq.mli index 3a6f8ae015..f879d51660 100644 --- a/vernac/egramcoq.mli +++ b/vernac/egramcoq.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/egramml.ml b/vernac/egramml.ml index bc58993a2e..62eb561f3c 100644 --- a/vernac/egramml.ml +++ b/vernac/egramml.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/egramml.mli b/vernac/egramml.mli index 1cf75a55b1..1fe2395df2 100644 --- a/vernac/egramml.mli +++ b/vernac/egramml.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index 2bc95dbfcd..5c5a4ffbcb 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -44,59 +44,61 @@ let explain_exn_default = function let _ = CErrors.register_handler explain_exn_default -(** Pre-explain a vernac interpretation error *) - -let wrap_vernac_error (exn, info) strm = (EvaluatedError (strm, None), info) - -let process_vernac_interp_error exn = match fst exn with +let vernac_interp_error_handler = function | Univ.UniverseInconsistency i -> let msg = if !Constrextern.print_universes then - str "." ++ spc() ++ - Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i + str "." ++ spc() ++ + Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i else mt() in - wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".") + str "Universe inconsistency" ++ msg ++ str "." | TypeError(ctx,te) -> - let te = map_ptype_error EConstr.of_constr te in - wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te) + let te = map_ptype_error EConstr.of_constr te in + Himsg.explain_type_error ctx Evd.empty te | PretypeError(ctx,sigma,te) -> - wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te) + Himsg.explain_pretype_error ctx sigma te | Notation.PrimTokenNotationError(kind,ctx,sigma,te) -> - wrap_vernac_error exn (Himsg.explain_prim_token_notation_error kind ctx sigma te) + Himsg.explain_prim_token_notation_error kind ctx sigma te | Typeclasses_errors.TypeClassError(env, sigma, te) -> - wrap_vernac_error exn (Himsg.explain_typeclass_error env sigma te) - | Implicit_quantifiers.MismatchedContextInstance(e,c,l,x) -> - wrap_vernac_error exn (Himsg.explain_mismatched_contexts e c l x) + Himsg.explain_typeclass_error env sigma te | InductiveError e -> - wrap_vernac_error exn (Himsg.explain_inductive_error e) + Himsg.explain_inductive_error e | Modops.ModuleTypingError e -> - wrap_vernac_error exn (Himsg.explain_module_error e) + Himsg.explain_module_error e | Modintern.ModuleInternalizationError e -> - wrap_vernac_error exn (Himsg.explain_module_internalization_error e) + Himsg.explain_module_internalization_error e | RecursionSchemeError (env,e) -> - wrap_vernac_error exn (Himsg.explain_recursion_scheme_error env e) + Himsg.explain_recursion_scheme_error env e | Cases.PatternMatchingError (env,sigma,e) -> - wrap_vernac_error exn (Himsg.explain_pattern_matching_error env sigma e) + Himsg.explain_pattern_matching_error env sigma e | Tacred.ReductionTacticError e -> - wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e) + Himsg.explain_reduction_tactic_error e | Logic.RefinerError (env, sigma, e) -> - wrap_vernac_error exn (Himsg.explain_refiner_error env sigma e) + Himsg.explain_refiner_error env sigma e | Nametab.GlobalizationError q -> - wrap_vernac_error exn - (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++ - spc () ++ str "was not found" ++ - spc () ++ str "in the current" ++ spc () ++ str "environment.") + str "The reference" ++ spc () ++ Libnames.pr_qualid q ++ + spc () ++ str "was not found" ++ + spc () ++ str "in the current" ++ spc () ++ str "environment." | Refiner.FailError (i,s) -> - let s = Lazy.force s in - wrap_vernac_error exn - (str "Tactic failure" ++ - (if Pp.ismt s then s else str ": " ++ s) ++ - if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").") + let s = Lazy.force s in + str "Tactic failure" ++ + (if Pp.ismt s then s else str ": " ++ s) ++ + if Int.equal i 0 then str "." else str " (level " ++ int i ++ str")." | AlreadyDeclared msg -> - wrap_vernac_error exn (msg ++ str ".") + msg ++ str "." | _ -> - exn + raise CErrors.Unhandled + +let _ = CErrors.register_handler vernac_interp_error_handler + +(** Pre-explain a vernac interpretation error *) + +let wrap_vernac_error (exn, info) strm = (EvaluatedError (strm, None), info) + +let process_vernac_interp_error exn = + try vernac_interp_error_handler (fst exn) |> wrap_vernac_error exn + with CErrors.Unhandled -> exn let rec strip_wrapping_exceptions = function | Logic_monad.TacticFailure e -> @@ -108,16 +110,9 @@ let additional_error_info = ref [] let register_additional_error_info f = additional_error_info := f :: !additional_error_info -let process_vernac_interp_error ?(allow_uncaught=true) (exc, info) = +let process_vernac_interp_error (exc, info) = let exc = strip_wrapping_exceptions exc in let e = process_vernac_interp_error (exc, info) in - let () = - if not allow_uncaught && not (CErrors.handled (fst e)) then - let (e, info) = e in - let msg = str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "." in - let err = CErrors.make_anomaly msg in - Util.iraise (err, info) - in let e' = try Some (CList.find_map (fun f -> f e) !additional_error_info) with _ -> None diff --git a/vernac/explainErr.mli b/vernac/explainErr.mli index b54912a144..cc2a130925 100644 --- a/vernac/explainErr.mli +++ b/vernac/explainErr.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -13,7 +13,7 @@ exception EvaluatedError of Pp.t * exn option (** Pre-explain a vernac interpretation error *) -val process_vernac_interp_error : ?allow_uncaught:bool -> Util.iexn -> Util.iexn +val process_vernac_interp_error : Util.iexn -> Util.iexn (** General explain function. Should not be used directly now, see instead function [Errors.print] and variants *) diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index ecc7d3ff88..94876d2142 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -88,7 +88,6 @@ GRAMMAR EXTEND Gram | IDENT "Show" -> { VernacShow (ShowGoal OpenSubgoals) } | IDENT "Show"; n = natural -> { VernacShow (ShowGoal (NthGoal n)) } | IDENT "Show"; id = ident -> { VernacShow (ShowGoal (GoalId id)) } - | IDENT "Show"; IDENT "Script" -> { VernacShow ShowScript } | IDENT "Show"; IDENT "Existentials" -> { VernacShow ShowExistentials } | IDENT "Show"; IDENT "Universes" -> { VernacShow ShowUniverses } | IDENT "Show"; IDENT "Conjectures" -> { VernacShow ShowProofNames } diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 5eec8aed1e..74bd552459 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -50,7 +50,6 @@ let def_body = Entry.create "vernac:def_body" let decl_notation = Entry.create "vernac:decl_notation" let record_field = Entry.create "vernac:record_field" let of_type_with_opt_coercion = Entry.create "vernac:of_type_with_opt_coercion" -let instance_name = Entry.create "vernac:instance_name" let section_subset_expr = Entry.create "vernac:section_subset_expr" let make_bullet s = @@ -296,8 +295,8 @@ GRAMMAR EXTEND Gram | -> { NoInline } ] ] ; univ_constraint: - [ [ l = universe_level; ord = [ "<" -> { Univ.Lt } | "=" -> { Univ.Eq } | "<=" -> { Univ.Le } ]; - r = universe_level -> { (l, ord, r) } ] ] + [ [ l = universe_name; ord = [ "<" -> { Univ.Lt } | "=" -> { Univ.Eq } | "<=" -> { Univ.Le } ]; + r = universe_name -> { (l, ord, r) } ] ] ; univ_decl : [ [ "@{" ; l = LIST0 identref; ext = [ "+" -> { true } | -> { false } ]; @@ -683,7 +682,7 @@ END (* Extensions: implicits, coercions, etc. *) GRAMMAR EXTEND Gram - GLOBAL: gallina_ext instance_name hint_info; + GLOBAL: gallina_ext hint_info; gallina_ext: [ [ (* Transparent and Opaque *) diff --git a/vernac/himsg.ml b/vernac/himsg.ml index a1f7835cbe..2e218942cb 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -1095,19 +1095,6 @@ let explain_unbound_method env sigma cid { CAst.v = id } = str "Unbound method name " ++ Id.print (id) ++ spc () ++ str"of class" ++ spc () ++ pr_global cid ++ str "." -let pr_constr_exprs env sigma exprs = - hv 0 (List.fold_right - (fun d pps -> ws 2 ++ Ppconstr.pr_constr_expr env sigma d ++ pps) - exprs (mt ())) - -let explain_mismatched_contexts env c i j = - let sigma = Evd.from_env env in - let pm, pn = with_diffs (pr_rel_context env sigma j) (pr_constr_exprs env sigma i) in - str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++ - hov 1 (str"Expected:" ++ brk (1, 1) ++ pm) ++ - fnl () ++ brk (1,1) ++ - hov 1 (str"Found:" ++ brk (1, 1) ++ pn) - let explain_typeclass_error env sigma = function | NotAClass c -> explain_not_a_class env sigma c | UnboundMethod (cid, id) -> explain_unbound_method env sigma cid id diff --git a/vernac/himsg.mli b/vernac/himsg.mli index d1c1c092e3..6458fb9e30 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -24,8 +24,6 @@ val explain_pretype_error : env -> Evd.evar_map -> pretype_error -> Pp.t val explain_inductive_error : inductive_error -> Pp.t -val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Constr.rel_context -> Pp.t - val explain_typeclass_error : env -> Evd.evar_map -> typeclass_error -> Pp.t val explain_recursion_scheme_error : env -> recursion_scheme_error -> Pp.t diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index de7d2fd49a..b393f33d5d 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -21,7 +21,6 @@ open CErrors open Util open Names open Declarations -open Entries open Term open Constr open Inductive @@ -104,15 +103,16 @@ let () = let define ~poly id internal sigma c t = let f = declare_constant ~internal in let univs = Evd.univ_entry ~poly sigma in + let open Proof_global in let kn = f id (DefinitionEntry - { const_entry_body = c; - const_entry_secctx = None; - const_entry_type = t; - const_entry_universes = univs; - const_entry_opaque = false; - const_entry_inline_code = false; - const_entry_feedback = None; + { 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; }, Decl_kinds.IsDefinition Scheme) in definition_message id; @@ -414,7 +414,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),Safe_typing.empty_private_constants) in + let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Evd.empty_side_effects) in let cst = define ~poly fi UserIndividualRequest sigma proof_output (Some decltype) in ConstRef cst :: lrecref in @@ -536,7 +536,7 @@ 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),Safe_typing.empty_private_constants) 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 diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli index ebfc76de9d..a747ac6598 100644 --- a/vernac/indschemes.mli +++ b/vernac/indschemes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 740b9031cc..c2de83c1bb 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -26,7 +26,6 @@ open Decl_kinds open Declare open Pretyping open Termops -open Namegen open Reductionops open Constrintern open Impargs @@ -34,17 +33,60 @@ open Impargs module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -type hook_type = UState.t -> (Id.t * Constr.t) list -> Decl_kinds.locality -> GlobRef.t -> unit -type declaration_hook = hook_type +(* Support for terminators and proofs with an associated constant + [that can be saved] *) -let mk_hook hook = hook +type lemma_possible_guards = int list list -let call_hook ?hook ?fix_exn uctx trans l c = - try Option.iter (fun hook -> hook uctx trans l c) hook - with e when CErrors.noncritical e -> - let e = CErrors.push e in - let e = Option.cata (fun fix -> fix e) e fix_exn in - iraise e +module Proof_ending = struct + + type t = + | Regular + | End_obligation of DeclareObl.obligation_qed_info + | End_derive of { f : Id.t; name : Id.t } + | End_equations of { hook : Constant.t list -> Evd.evar_map -> unit + ; i : Id.t + ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list + ; wits : EConstr.t list ref + (* wits are actually computed by the proof + engine by side-effect after creating the + proof! This is due to the start_dependent_proof API *) + ; sigma : Evd.evar_map + } + +end + +(* Proofs with a save constant function *) +type t = + { proof : Proof_global.t + ; hook : DeclareDef.Hook.t option + ; compute_guard : lemma_possible_guards + ; proof_ending : Proof_ending.t CEphemeron.key + (* This could be improved and the CEphemeron removed *) + } + +let pf_map f pf = { pf with proof = f pf.proof } +let pf_fold f pf = f pf.proof + +let set_endline_tactic t = pf_map (Proof_global.set_endline_tactic t) + +(* To be removed *) +module Internal = struct + +(** Gets the current terminator without checking that the proof has + been completed. Useful for the likes of [Admitted]. *) +let get_info ps = ps.hook, ps.compute_guard, ps.proof_ending + +end +(* Internal *) + +let by tac pf = + let proof, res = Pfedit.by tac pf.proof in + { pf with proof }, res + +(************************************************************************) +(* Creating a lemma-like constant *) +(************************************************************************) (* Support for mutually proved theorems *) @@ -56,7 +98,7 @@ let retrieve_first_recthm uctx = function (* we get the right order somehow but surely it could be enforced in a better way *) let uctx = UState.context uctx in let inst = Univ.UContext.instance uctx in - let map (c, ctx) = Vars.subst_instance_constr inst c in + let map (c, _, _) = Vars.subst_instance_constr inst c in (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), is_opaque cb) | _ -> assert false @@ -65,8 +107,9 @@ let adjust_guardness_conditions const = function | possible_indexes -> (* Try all combinations... not optimal *) let env = Global.env() in - { const with const_entry_body = - Future.chain const.const_entry_body + let open Proof_global in + { const with proof_entry_body = + Future.chain const.proof_entry_body (fun ((body, ctx), eff) -> match Constr.kind body with | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> @@ -75,7 +118,7 @@ let adjust_guardness_conditions const = function List.interval 0 (List.length ((lam_assum c)))) lemma_guard (Array.to_list fixdefs) in *) - let env = Safe_typing.push_private_constants env eff in + let env = Safe_typing.push_private_constants env eff.Evd.seff_private in let indexes = search_guard env possible_indexes fixdecls in @@ -169,55 +212,12 @@ let look_for_possibly_mutual_statements sigma = function Some recguard,thms, Some (List.map (fun (_,_,i) -> succ i) ordered_inds) | [] -> anomaly (Pp.str "Empty list of theorems.") -(* Saving a goal *) - -let save ?export_seff id const uctx do_guard (locality,poly,kind) hook universes = - let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in - try - let const = adjust_guardness_conditions const do_guard in - let k = Kindops.logical_kind_of_goal_kind kind in - let should_suggest = const.const_entry_opaque && Option.is_empty const.const_entry_secctx in - let r = match locality with - | Discharge when Lib.sections_are_opened () -> - let c = SectionLocalDef const in - let _ = declare_variable id (Lib.cwd(), c, k) in - let () = if should_suggest - then Proof_using.suggest_variable (Global.env ()) id - in - VarRef id - | Local | Global | Discharge -> - let local = match locality with - | Local | Discharge -> true - | Global -> false - in - let kn = - declare_constant ?export_seff id ~local (DefinitionEntry const, k) in - let () = if should_suggest - then Proof_using.suggest_constant (Global.env ()) kn - in - let gr = ConstRef kn in - Declare.declare_univ_binders gr (UState.universe_binders uctx); - gr - in - definition_message id; - call_hook ?hook universes [] locality r - with e when CErrors.noncritical e -> - let e = CErrors.push e in - iraise (fix_exn e) - let default_thm_id = Id.of_string "Unnamed_thm" -let fresh_name_for_anonymous_theorem ~pstate = - let avoid = match pstate with - | None -> Id.Set.empty - | Some pstate -> Id.Set.of_list (Proof_global.get_all_proof_names pstate) - in - next_global_ident_away default_thm_id avoid - let check_name_freshness locality {CAst.loc;v=id} : unit = (* We check existence here: it's a bit late at Qed time *) if Nametab.exists_cci (Lib.make_path id) || is_section_variable id || - locality == Global && Nametab.exists_cci (Lib.make_path_except_section id) + locality <> Discharge && Nametab.exists_cci (Lib.make_path_except_section id) then user_err ?loc (Id.print id ++ str " already exists.") @@ -237,16 +237,12 @@ let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i (i in let c = SectionLocalAssum ((t_i, univs),p,impl) in let _ = declare_variable id (Lib.cwd(),c,k) in - (Discharge, VarRef id,imps) - | Local | Global -> - let local = match locality with - | Local -> true - | Global -> false - | Discharge -> assert false - in + (VarRef id,imps) + | Global local -> + let k = IsAssumption Conjectural in let decl = (ParameterEntry (None,(t_i,univs),None), k) in let kn = declare_constant id ~local decl in - (locality,ConstRef kn,imps)) + (ConstRef kn,imps)) | Some body -> let body = norm body in let k = Kindops.logical_kind_of_goal_kind kind in @@ -264,62 +260,13 @@ let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i (i let const = definition_entry ~types:t_i ~opaque:opaq ~univs body_i in let c = SectionLocalDef const in let _ = declare_variable id (Lib.cwd(), c, k) in - (Discharge,VarRef id,imps) - | Local | Global -> - let local = match locality with - | Local -> true - | Global -> false - | Discharge -> assert false - in + (VarRef id,imps) + | Global local -> let const = Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i in let kn = declare_constant id ~local (DefinitionEntry const, k) in - (locality,ConstRef kn,imps) - -let check_anonymity id save_ident = - if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then - user_err Pp.(str "This command can only be used for unnamed theorem.") - -(* Admitted *) - -let warn_let_as_axiom = - CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" - (fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++ - spc () ++ strbrk "declared as an axiom.") - -let admit ?hook ctx (id,k,e) pl () = - let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in - let () = match k with - | Global, _, _ -> () - | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id - in - let () = assumption_message id in - Declare.declare_univ_binders (ConstRef kn) pl; - call_hook ?hook ctx [] Global (ConstRef kn) - -(* Starting a goal *) - -let standard_proof_terminator ?(hook : declaration_hook option) compute_guard = - let open Proof_global in - make_terminator begin function - | Admitted (id,k,pe,ctx) -> - let () = admit ?hook ctx (id,k,pe) (UState.universe_binders ctx) () in - Feedback.feedback Feedback.AddedAxiom - | Proved (opaque,idopt, { id; entries=[const]; persistence; universes } ) -> - let is_opaque, export_seff = match opaque with - | Transparent -> false, true - | Opaque -> true, false - in - assert (is_opaque == const.const_entry_opaque); - let id = match idopt with - | None -> id - | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in - let () = save ~export_seff id const universes compute_guard persistence hook universes in - () - | Proved (opaque,idopt, _ ) -> - CErrors.anomaly Pp.(str "[universe_proof_terminator] close_proof returned more than one proof term") - end + (ConstRef kn,imps) let initialize_named_context_for_proof () = let sign = Global.named_context () in @@ -329,18 +276,52 @@ let initialize_named_context_for_proof () = let d = if variable_opacity id then NamedDecl.drop_body d else d in Environ.push_named_context_val d signv) sign Environ.empty_named_context_val -let start_proof ~ontop id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c = - let terminator = match terminator with - | None -> standard_proof_terminator ?hook compute_guard - | Some terminator -> terminator ?hook compute_guard - in - let sign = - match sign with - | Some sign -> sign - | None -> initialize_named_context_for_proof () - in +module Stack = struct + + type lemma = t + type nonrec t = t * t list + + let map f (pf, pfl) = (f pf, List.map f pfl) + + let map_top ~f (pf, pfl) = (f pf, pfl) + let map_top_pstate ~f (pf, pfl) = (pf_map f pf, pfl) + + let pop (ps, p) = match p with + | [] -> ps, None + | pp :: p -> ps, Some (pp, p) + + let with_top (p, _) ~f = f p + let with_top_pstate (p, _) ~f = f p.proof + + let push ontop a = + match ontop with + | None -> a , [] + | Some (l,ls) -> a, (l :: ls) + + let get_all_proof_names (pf : t) = + let prj x = Proof_global.get_proof x in + let (pn, pns) = map Proof.(function pf -> (data (prj pf.proof)).name) pf in + pn :: pns + + let copy_info ~src ~tgt = + let (ps, psl), (ts,tsl) = src, tgt in + assert(List.length psl = List.length tsl); + { ps with proof = ts.proof }, + List.map2 (fun op p -> { op with proof = p.proof }) psl tsl + +end + +(* Starting a goal *) +let start_lemma id ?pl kind sigma ?(proof_ending = Proof_ending.Regular) + ?(sign=initialize_named_context_for_proof()) ?(compute_guard=[]) ?hook c = let goals = [ Global.env_of_context sign , c ] in - Proof_global.start_proof ~ontop sigma id ?pl kind goals terminator + let proof = Proof_global.start_proof sigma id ?pl kind goals in + { proof ; hook; compute_guard; proof_ending = CEphemeron.create proof_ending } + +let start_dependent_lemma id ?pl kind ?(proof_ending = Proof_ending.Regular) + ?(compute_guard=[]) ?hook telescope = + let proof = Proof_global.start_dependent_proof id ?pl kind telescope in + { proof; hook; compute_guard; proof_ending = CEphemeron.create proof_ending } let rec_tac_initializer finite guard thms snl = if finite then @@ -356,7 +337,7 @@ let rec_tac_initializer finite guard thms snl = | (id,n,_)::l -> Tactics.mutual_fix id n l 0 | _ -> assert false -let start_proof_with_initialization ~ontop ?hook kind sigma decl recguard thms snl = +let start_lemma_with_initialization ?hook kind sigma decl recguard thms snl = let intro_tac (_, (_, (ids, _))) = Tactics.auto_intros_tac ids in let init_tac,guard = match recguard with | Some (finite,guard,init_tac) -> @@ -384,18 +365,19 @@ let start_proof_with_initialization ~ontop ?hook kind sigma decl recguard thms s let uctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in let env = Global.env () in List.map_i (save_remaining_recthms env sigma kind norm uctx body opaq) 1 other_thms in - let thms_data = (strength,ref,imps)::other_thms_data in - List.iter (fun (strength,ref,imps) -> + let thms_data = (ref,imps)::other_thms_data in + List.iter (fun (ref,imps) -> maybe_declare_manual_implicits false ref imps; - call_hook ?hook ctx [] strength ref) thms_data in - let pstate = start_proof ~ontop id ~pl:decl kind sigma t ~hook ~compute_guard:guard in - let pstate = Proof_global.simple_with_current_proof (fun _ p -> + DeclareDef.Hook.call ?hook ctx [] strength ref) thms_data in + let hook = DeclareDef.Hook.make hook in + let lemma = start_lemma id ~pl:decl kind sigma t ~hook ~compute_guard:guard in + let lemma = pf_map (Proof_global.map_proof (fun p -> match init_tac with | None -> p - | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p) pstate in - pstate + | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p)) lemma in + lemma -let start_proof_com ~program_mode ~ontop ?inference_hook ?hook kind thms = +let start_lemma_com ~program_mode ?inference_hook ?hook kind thms = let env0 = Global.env () in let decl = fst (List.hd thms) in let evd, decl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in @@ -410,7 +392,7 @@ let start_proof_com ~program_mode ~ontop ?inference_hook ?hook kind thms = (* XXX: The nf_evar is critical !! *) evd, (id.CAst.v, (Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx), - (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps')))) + (ids, imps @ imps')))) evd thms in let recguard,thms,snl = look_for_possibly_mutual_statements evd thms in let evd = Evd.minimize_universes evd in @@ -427,38 +409,56 @@ let start_proof_com ~program_mode ~ontop ?inference_hook ?hook kind thms = else (* We fix the variables to ensure they won't be lowered to Set *) Evd.fix_undefined_variables evd in - start_proof_with_initialization ~ontop ?hook kind evd decl recguard thms snl + start_lemma_with_initialization ?hook kind evd decl recguard thms snl -(* Saving a proof *) +(************************************************************************) +(* Admitting a lemma-like constant *) +(************************************************************************) -let keep_admitted_vars = ref true +let check_anonymity id save_ident = + if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then + user_err Pp.(str "This command can only be used for unnamed theorem.") -let () = - let open Goptions in - declare_bool_option - { optdepr = false; - optname = "keep section variables in admitted proofs"; - optkey = ["Keep"; "Admitted"; "Variables"]; - optread = (fun () -> !keep_admitted_vars); - optwrite = (fun b -> keep_admitted_vars := b) } +(* Admitted *) +let warn_let_as_axiom = + CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" + (fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++ + spc () ++ strbrk "declared as an axiom.") -let save_proof_admitted ?proof ~pstate = - let pe = +let finish_admitted id k pe ctx hook = + let local = match k with + | Global local, _, _ -> local + | Discharge, _, _ -> warn_let_as_axiom id; ImportNeedQualified + in + let kn = declare_constant id ~local (ParameterEntry pe, IsAssumption Conjectural) in + let () = assumption_message id in + Declare.declare_univ_binders (ConstRef kn) (UState.universe_binders ctx); + DeclareDef.Hook.call ?hook ctx [] (Global local) (ConstRef kn); + Feedback.feedback Feedback.AddedAxiom + +let get_keep_admitted_vars = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"keep section variables in admitted proofs" + ~key:["Keep"; "Admitted"; "Variables"] + ~value:true + +let save_lemma_admitted ?proof ~(lemma : t) = let open Proof_global in match proof with - | Some ({ id; entries; persistence = k; universes }, _) -> + | Some ({ id; entries; persistence = k; universes }, (hook, _, _)) -> if List.length entries <> 1 then user_err Pp.(str "Admitted does not support multiple statements"); - let { const_entry_secctx; const_entry_type } = List.hd entries in - if const_entry_type = None then + let { proof_entry_secctx; proof_entry_type } = List.hd entries in + if proof_entry_type = None then user_err Pp.(str "Admitted requires an explicit statement"); - let typ = Option.get const_entry_type in + let typ = Option.get proof_entry_type in let ctx = UState.univ_entry ~poly:(pi2 k) universes in - let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in - Admitted(id, k, (sec_vars, (typ, ctx), None), universes) + let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in + finish_admitted id k (sec_vars, (typ, ctx), None) universes hook | None -> - let pftree = Proof_global.give_me_the_proof pstate in - let gk = Proof_global.get_current_persistence pstate in + let pftree = Proof_global.get_proof lemma.proof in + let gk = Proof_global.get_persistence lemma.proof in let Proof.{ name; poly; entry } = Proof.data pftree in let typ = match Proofview.initial_goals entry with | [typ] -> snd typ @@ -470,10 +470,10 @@ let save_proof_admitted ?proof ~pstate = let universes = Proof.((data pftree).initial_euctx) in (* This will warn if the proof is complete *) let pproofs, _univs = - Proof_global.return_proof ~allow_partial:true pstate in + Proof_global.return_proof ~allow_partial:true lemma.proof in let sec_vars = - if not !keep_admitted_vars then None - else match Proof_global.get_used_variables pstate, pproofs with + if not (get_keep_admitted_vars ()) then None + else match Proof_global.get_used_variables lemma.proof, pproofs with | Some _ as x, _ -> x | None, (pproof, _) :: _ -> let env = Global.env () in @@ -481,26 +481,154 @@ let save_proof_admitted ?proof ~pstate = let ids_def = Environ.global_vars_set env pproof in Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def)) | _ -> None in - let decl = Proof_global.get_universe_decl pstate in + let decl = Proof_global.get_universe_decl lemma.proof in let ctx = UState.check_univ_decl ~poly universes decl in - Admitted(name,gk,(sec_vars, (typ, ctx), None), universes) + finish_admitted name gk (sec_vars, (typ, ctx), None) universes lemma.hook + +(************************************************************************) +(* Saving a lemma-like constant *) +(************************************************************************) + +type proof_info = DeclareDef.Hook.t option * lemma_possible_guards * Proof_ending.t CEphemeron.key + +let default_info = None, [], CEphemeron.create Proof_ending.Regular + +let finish_proved opaque idopt po hook compute_guard = + let open Proof_global in + match po with + | { id; entries=[const]; persistence=locality,poly,kind; universes } -> + let is_opaque = match opaque with + | Transparent -> false + | Opaque -> true + in + assert (is_opaque == const.proof_entry_opaque); + let id = match idopt with + | None -> id + | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in + let fix_exn = Future.fix_exn_of const.proof_entry_body in + let () = try + let const = adjust_guardness_conditions const compute_guard in + let k = Kindops.logical_kind_of_goal_kind kind in + let should_suggest = const.proof_entry_opaque && Option.is_empty const.proof_entry_secctx in + let r = match locality with + | Discharge -> + let c = SectionLocalDef const in + let _ = declare_variable id (Lib.cwd(), c, k) in + let () = if should_suggest + then Proof_using.suggest_variable (Global.env ()) id + in + VarRef id + | Global local -> + let kn = + declare_constant id ~local (DefinitionEntry const, k) in + let () = if should_suggest + then Proof_using.suggest_constant (Global.env ()) kn + in + let gr = ConstRef kn in + Declare.declare_univ_binders gr (UState.universe_binders universes); + gr + in + definition_message id; + DeclareDef.Hook.call ~fix_exn ?hook universes [] locality r + with e when CErrors.noncritical e -> + let e = CErrors.push e in + iraise (fix_exn e) + in () + | _ -> + CErrors.anomaly Pp.(str "[standard_proof_terminator] close_proof returned more than one proof term") + +let finish_derived ~f ~name ~idopt ~opaque ~entries = + (* [f] and [name] correspond to the proof of [f] and of [suchthat], respectively. *) + + if Option.has_some idopt then + CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name."); + + let opaque, f_def, lemma_def = + match entries with + | [_;f_def;lemma_def] -> + opaque <> Proof_global.Transparent , f_def , lemma_def + | _ -> assert false + 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 = Declare.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in + let f_kn = Declare.declare_constant f f_def in + let f_kn_term = mkConst f_kn in + (* In the type and body of the proof of [suchthat] there can be + references to the variable [f]. It needs to be replaced by + references to the constant [f] declared above. This substitution + performs this precise action. *) + 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 + | 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 + { lemma_def with + proof_entry_body = lemma_body ; + proof_entry_type = Some lemma_type ; + proof_entry_opaque = opaque ; } in - Proof_global.apply_terminator (Proof_global.get_terminator pstate) pe + let lemma_def = + Declare.DefinitionEntry lemma_def , + Decl_kinds.(IsProof Proposition) + in + ignore (Declare.declare_constant name lemma_def) + +let finish_proved_equations opaque lid proof_obj hook i types wits sigma0 = -let save_proof_proved ?proof ?pstate ~opaque ~idopt = + let open Decl_kinds in + let obls = ref 1 in + let kind = match pi3 proof_obj.Proof_global.persistence with + | DefinitionBody d -> IsDefinition d + | Proof p -> IsProof p + in + let sigma, recobls = + CList.fold_left2_map (fun sigma (wit, (evar_env, ev, evi, local_context, type_)) entry -> + let id = + match Evd.evar_ident ev sigma0 with + | Some id -> id + | None -> let n = !obls in incr obls; add_suffix i ("_obligation_" ^ string_of_int n) + in + let entry, args = Abstract.shrink_entry local_context entry in + let cst = Declare.declare_constant id (Declare.DefinitionEntry entry, kind) in + let sigma, app = Evarutil.new_global sigma (ConstRef cst) in + let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in + sigma, cst) sigma0 + (CList.combine (List.rev !wits) types) proof_obj.Proof_global.entries + in + hook recobls sigma + +let save_lemma_proved ?proof ?lemma ~opaque ~idopt = (* Invariant (uh) *) - if Option.is_empty pstate && Option.is_empty proof then + if Option.is_empty lemma && Option.is_empty proof then user_err (str "No focused proof (No proof-editing in progress)."); - let (proof_obj,terminator) = + let proof_obj, proof_info = match proof with | None -> (* XXX: The close_proof and proof state API should be refactored so it is possible to insert proofs properly into the state *) - let pstate = Option.get pstate in - Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pstate - | Some proof -> proof + let { proof; hook; compute_guard; proof_ending } = Option.get lemma in + Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, (hook, compute_guard, proof_ending) + | Some (proof, info) -> + proof, info in - (* if the proof is given explicitly, nothing has to be deleted *) - let pstate = if Option.is_empty proof then Proof_global.discard_current Option.(get pstate) else pstate in - Proof_global.(apply_terminator terminator (Proved (opaque,idopt,proof_obj))); - pstate + let hook, compute_guard, proof_ending = proof_info in + let open Proof_global in + let open Proof_ending in + match CEphemeron.default proof_ending Regular with + | Regular -> + finish_proved opaque idopt proof_obj hook compute_guard + | End_obligation oinfo -> + DeclareObl.obligation_terminator opaque proof_obj.entries proof_obj.universes oinfo + | End_derive { f ; name } -> + finish_derived ~f ~name ~idopt ~opaque ~entries:proof_obj.entries + | End_equations { hook; i; types; wits; sigma } -> + finish_proved_equations opaque idopt proof_obj hook i types wits sigma diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 1f70cfa1ad..70c8b511a1 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -11,74 +11,120 @@ open Names open Decl_kinds -type declaration_hook - -(* Hooks allow users of the API to perform arbitrary actions at - * proof/definition saving time. For example, to register a constant - * as a Coercion, perform some cleanup, update the search database, - * etc... - * - * Here, we use an extended hook type suitable for obligations / - * equations. - *) -(** [hook_type] passes to the client: - - [ustate]: universe constraints obtained when the term was closed - - [(n1,t1),...(nm,tm)]: association list between obligation - name and the corresponding defined term (might be a constant, - but also an arbitrary term in the Expand case of obligations) - - [locality]: Locality of the original declaration - - [ref]: identifier of the origianl declaration - *) -type hook_type = UState.t -> (Id.t * Constr.t) list -> Decl_kinds.locality -> GlobRef.t -> unit - -val mk_hook : hook_type -> declaration_hook -val call_hook - : ?hook:declaration_hook - -> ?fix_exn:Future.fix_exn - -> hook_type - -val start_proof : ontop:Proof_global.t option -> Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> - ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) -> - ?sign:Environ.named_context_val -> - ?compute_guard:Proof_global.lemma_possible_guards -> - ?hook:declaration_hook -> EConstr.types -> Proof_global.t - -val start_proof_com +(* Proofs that define a constant *) +type t +type lemma_possible_guards = int list list + +module Stack : sig + + type lemma = t + type t + + val pop : t -> lemma * t option + val push : t option -> lemma -> t + + val map_top : f:(lemma -> lemma) -> t -> t + val map_top_pstate : f:(Proof_global.t -> Proof_global.t) -> t -> t + + val with_top : t -> f:(lemma -> 'a ) -> 'a + val with_top_pstate : t -> f:(Proof_global.t -> 'a ) -> 'a + + val get_all_proof_names : t -> Names.Id.t list + + val copy_info : src:t -> tgt:t -> t + (** Gets the current info without checking that the proof has been + completed. Useful for the likes of [Admitted]. *) + +end + +val set_endline_tactic : Genarg.glob_generic_argument -> t -> t +val pf_map : (Proof_global.t -> Proof_global.t) -> t -> t +val pf_fold : (Proof_global.t -> 'a) -> t -> 'a + +val by : unit Proofview.tactic -> t -> t * bool + +(* Start of high-level proofs with an associated constant *) + +module Proof_ending : sig + + type t = + | Regular + | End_obligation of DeclareObl.obligation_qed_info + | End_derive of { f : Id.t; name : Id.t } + | End_equations of { hook : Constant.t list -> Evd.evar_map -> unit + ; i : Id.t + ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list + ; wits : EConstr.t list ref + ; sigma : Evd.evar_map + } + +end + +val start_lemma + : Id.t + -> ?pl:UState.universe_decl + -> goal_kind + -> Evd.evar_map + -> ?proof_ending:Proof_ending.t + -> ?sign:Environ.named_context_val + -> ?compute_guard:lemma_possible_guards + -> ?hook:DeclareDef.Hook.t + -> EConstr.types + -> t + +val start_dependent_lemma + : Id.t + -> ?pl:UState.universe_decl + -> goal_kind + -> ?proof_ending:Proof_ending.t + -> ?compute_guard:lemma_possible_guards + -> ?hook:DeclareDef.Hook.t + -> Proofview.telescope + -> t + +val start_lemma_com : program_mode:bool - -> ontop:Proof_global.t option -> ?inference_hook:Pretyping.inference_hook - -> ?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list - -> Proof_global.t + -> ?hook:DeclareDef.Hook.t -> goal_kind -> Vernacexpr.proof_expr list + -> t -val start_proof_with_initialization : ontop:Proof_global.t option -> - ?hook:declaration_hook -> - goal_kind -> Evd.evar_map -> UState.universe_decl -> - (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option -> - (Id.t (* name of thm *) * - (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list - -> int list option -> Proof_global.t +val start_lemma_with_initialization + : ?hook:DeclareDef.Hook.t + -> goal_kind -> Evd.evar_map -> UState.universe_decl + -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option + -> (Id.t (* name of thm *) * + (EConstr.types (* type of thm *) * + (Name.t list (* names to pre-introduce *) * Impargs.manual_implicits))) list + -> int list option + -> t -val standard_proof_terminator : - ?hook:declaration_hook -> Proof_global.lemma_possible_guards -> - Proof_global.proof_terminator - -val fresh_name_for_anonymous_theorem : pstate:Proof_global.t option -> Id.t +val default_thm_id : Names.Id.t (* Prepare global named context for proof session: remove proofs of opaque section definitions and remove vm-compiled code *) val initialize_named_context_for_proof : unit -> Environ.named_context_val -(** {6 ... } *) +(** {6 Saving proofs } *) + +type proof_info + +val default_info : proof_info -val save_proof_admitted - : ?proof:Proof_global.closed_proof - -> pstate:Proof_global.t +val save_lemma_admitted + : ?proof:(Proof_global.proof_object * proof_info) + -> lemma:t -> unit -val save_proof_proved - : ?proof:Proof_global.closed_proof - -> ?pstate:Proof_global.t +val save_lemma_proved + : ?proof:(Proof_global.proof_object * proof_info) + -> ?lemma:t -> opaque:Proof_global.opacity_flag -> idopt:Names.lident option - -> Proof_global.t option + -> unit + +(* To be removed *) +module Internal : sig + (** Only needed due to the Proof_global compatibility layer. *) + val get_info : t -> proof_info +end diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml index f5e8b6d12f..bea0c943c3 100644 --- a/vernac/loadpath.ml +++ b/vernac/loadpath.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/loadpath.mli b/vernac/loadpath.mli index 6605daa8d2..47d2d34125 100644 --- a/vernac/loadpath.mli +++ b/vernac/loadpath.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/locality.ml b/vernac/locality.ml index 21be73b39c..bc33d53594 100644 --- a/vernac/locality.ml +++ b/vernac/locality.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -12,10 +12,9 @@ open Decl_kinds (** * Managing locality *) -let local_of_bool = function - | true -> Local - | false -> Global - +let importability_of_bool = function + | true -> ImportNeedQualified + | false -> ImportDefaultBehavior (** Positioning locality for commands supporting discharging and export outside of modules *) @@ -28,10 +27,22 @@ let make_non_locality = function Some false -> false | _ -> true let make_locality = function Some true -> true | _ -> false +let warn_local_declaration = + CWarnings.create ~name:"local-declaration" ~category:"scope" + Pp.(fun () -> + Pp.strbrk "Interpreting this declaration as if " ++ + strbrk "a global declaration prefixed by \"Local\", " ++ + strbrk "i.e. as a global declaration which shall not be " ++ + strbrk "available without qualification when imported.") + let enforce_locality_exp locality_flag discharge = match locality_flag, discharge with - | Some b, NoDischarge -> local_of_bool b - | None, NoDischarge -> Global + | Some b, NoDischarge -> Global (importability_of_bool b) + | None, NoDischarge -> Global ImportDefaultBehavior + | None, DoDischarge when not (Lib.sections_are_opened ()) -> + (* If a Let/Variable is defined outside a section, then we consider it as a local definition *) + warn_local_declaration (); + Global ImportNeedQualified | None, DoDischarge -> Discharge | Some true, DoDischarge -> CErrors.user_err Pp.(str "Local not allowed in this case") | Some false, DoDischarge -> CErrors.user_err Pp.(str "Global not allowed in this case") diff --git a/vernac/locality.mli b/vernac/locality.mli index 3c63c82117..be7e0cbe76 100644 --- a/vernac/locality.mli +++ b/vernac/locality.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 50914959dc..90892feb13 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -732,13 +732,8 @@ type syntax_extension = { synext_notgram : notation_grammar; synext_unparsing : unparsing list; synext_extra : (string * string) list; - synext_compat : Flags.compat_version option; } -let is_active_compat = function -| None -> true -| Some v -> 0 <= Flags.version_compare v !Flags.compat_version - type syntax_extension_obj = locality_flag * syntax_extension let check_and_extend_constr_grammar ntn rule = @@ -759,7 +754,7 @@ let cache_one_syntax_extension se = let oldprec = Notgram_ops.level_of_notation ~onlyprint ntn in if not (Notgram_ops.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec; with Not_found -> - if is_active_compat se.synext_compat then begin + begin (* Reserve the notation level *) Notgram_ops.declare_notation_level ntn prec ~onlyprint; (* Declare the parsing rule *) @@ -934,10 +929,6 @@ let is_only_printing mods = let test = function SetOnlyPrinting -> true | _ -> false in List.exists test mods -let get_compat_version mods = - let test = function SetCompatVersion v -> Some v | _ -> None in - try Some (List.find_map test mods) with Not_found -> None - (* Compute precedences from modifiers (or find default ones) *) let set_entry_type from etyps (x,typ) = @@ -1177,7 +1168,7 @@ module SynData = struct (* Fields coming from the vernac-level modifiers *) only_parsing : bool; only_printing : bool; - compat : Flags.compat_version option; + deprecation : Deprecation.t option; format : lstring option; extra : (string * string) list; @@ -1222,12 +1213,32 @@ let check_locality_compatibility local custom i_typs = strbrk " which is local.")) (List.uniquize allcustoms) -let compute_syntax_data local df modifiers = +let warn_deprecated_compat = + CWarnings.create ~name:"deprecated-compat" ~category:"deprecated" + (fun () -> Pp.(str"The \"compat\" modifier is deprecated." ++ spc () ++ + str"Please use the \"deprecated\" attributed instead.")) + +(* Returns the new deprecation and the onlyparsing status. This should be +removed together with the compat syntax modifier. *) +let merge_compat_deprecation compat deprecation = + match compat, deprecation with + | Some Flags.Current, _ -> deprecation, true + | Some _, Some _ -> + CErrors.user_err Pp.(str"The \"compat\" modifier cannot be used with the \"deprecated\" attribute." + ++ spc () ++ str"Please use only the latter.") + | Some v, None -> + warn_deprecated_compat (); + Some (Deprecation.make ~since:(Flags.pr_version v) ()), true + | None, Some _ -> deprecation, true + | None, None -> deprecation, false + +let compute_syntax_data ~local deprecation df modifiers = let open SynData in let open NotationMods in let mods = interp_modifiers modifiers in let onlyprint = mods.only_printing in let onlyparse = mods.only_parsing in + let deprecation, _ = merge_compat_deprecation mods.compat deprecation in if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'."); let assoc = Option.append mods.assoc (Some Gramlib.Gramext.NonA) in let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint df in @@ -1265,7 +1276,7 @@ let compute_syntax_data local df modifiers = only_parsing = mods.only_parsing; only_printing = mods.only_printing; - compat = mods.compat; + deprecation; format = mods.format; extra = mods.extra; @@ -1281,9 +1292,9 @@ let compute_syntax_data local df modifiers = not_data = sy_fulldata; } -let compute_pure_syntax_data local df mods = +let compute_pure_syntax_data ~local df mods = let open SynData in - let sd = compute_syntax_data local df mods in + let sd = compute_syntax_data ~local None df mods in let msgs = if sd.only_parsing then (Feedback.msg_warning ?loc:None, @@ -1301,7 +1312,7 @@ type notation_obj = { notobj_coercion : entry_coercion_kind option; notobj_onlyparse : bool; notobj_onlyprint : bool; - notobj_compat : Flags.compat_version option; + notobj_deprecation : Deprecation.t option; notobj_notation : notation * notation_location; } @@ -1323,11 +1334,11 @@ let open_notation i (_, nobj) = let (ntn, df) = nobj.notobj_notation in let pat = nobj.notobj_interp in let onlyprint = nobj.notobj_onlyprint in + let deprecation = nobj.notobj_deprecation in let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in - let active = is_active_compat nobj.notobj_compat in - if Int.equal i 1 && fresh && active then begin + if Int.equal i 1 && fresh then begin (* Declare the interpretation *) - let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint in + let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in (* Declare the uninterpretation *) if not nobj.notobj_onlyparse then Notation.declare_uninterpretation (NotationRule (scope, ntn)) pat; @@ -1388,7 +1399,6 @@ let recover_notation_syntax ntn = synext_notgram = pa_rule; synext_unparsing = pp_rule; synext_extra = pp_extra_rules; - synext_compat = None; } with Not_found -> raise NoSyntaxRule @@ -1437,7 +1447,6 @@ let make_syntax_rules (sd : SynData.syn_data) = let open SynData in synext_notgram = { notgram_onlyprinting = sd.only_printing; notgram_rules = pa_rule }; synext_unparsing = pp_rule; synext_extra = sd.extra; - synext_compat = sd.compat; } (**********************************************************************) @@ -1447,9 +1456,9 @@ let to_map l = let fold accu (x, v) = Id.Map.add x v accu in List.fold_left fold Id.Map.empty l -let add_notation_in_scope local df env c mods scope = +let add_notation_in_scope ~local deprecation df env c mods scope = let open SynData in - let sd = compute_syntax_data local df mods in + let sd = compute_syntax_data ~local deprecation df mods in (* Prepare the interpretation *) (* Prepare the parsing and printing rules *) let sy_rules = make_syntax_rules sd in @@ -1470,7 +1479,7 @@ let add_notation_in_scope local df env c mods scope = notobj_onlyparse = onlyparse; notobj_coercion = coe; notobj_onlyprint = sd.only_printing; - notobj_compat = sd.compat; + notobj_deprecation = sd.deprecation; notobj_notation = sd.info; } in (* Ready to change the global state *) @@ -1479,7 +1488,7 @@ let add_notation_in_scope local df env c mods scope = Lib.add_anonymous_leaf (inNotation notation); sd.info -let add_notation_interpretation_core local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat = +let add_notation_interpretation_core ~local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint deprecation = let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint df in (* Recover types of variables and pa/pp rules; redeclare them if needed *) let level, i_typs, onlyprint = if not (is_numeral symbs) then begin @@ -1510,7 +1519,7 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_ notobj_onlyparse = onlyparse; notobj_coercion = coe; notobj_onlyprint = onlyprint; - notobj_compat = compat; + notobj_deprecation = deprecation; notobj_notation = df'; } in Lib.add_anonymous_leaf (inNotation notation); @@ -1518,41 +1527,40 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_ (* Notations without interpretation (Reserved Notation) *) -let add_syntax_extension local ({CAst.loc;v=df},mods) = let open SynData in - let psd = compute_pure_syntax_data local df mods in - let sy_rules = make_syntax_rules {psd with compat = None} in +let add_syntax_extension ~local ({CAst.loc;v=df},mods) = let open SynData in + let psd = compute_pure_syntax_data ~local df mods in + let sy_rules = make_syntax_rules {psd with deprecation = None} in Flags.if_verbose (List.iter (fun (f,x) -> f x)) psd.msgs; Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules)) (* Notations with only interpretation *) let add_notation_interpretation env ({CAst.loc;v=df},c,sc) = - let df' = add_notation_interpretation_core false df env c sc false false None in + let df' = add_notation_interpretation_core ~local:false df env c sc false false None in Dumpglob.dump_notation (loc,df') sc true let set_notation_for_interpretation env impls ({CAst.v=df},c,sc) = (try ignore - (Flags.silently (fun () -> add_notation_interpretation_core false df env ~impls c sc false false None) ()); + (Flags.silently (fun () -> add_notation_interpretation_core ~local:false df env ~impls c sc false false None) ()); with NoSyntaxRule -> user_err Pp.(str "Parsing rule for this notation has to be previously declared.")); Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc (* Main entry point *) -let add_notation local env c ({CAst.loc;v=df},modifiers) sc = +let add_notation ~local deprecation env c ({CAst.loc;v=df},modifiers) sc = let df' = if no_syntax_modifiers modifiers then (* No syntax data: try to rely on a previously declared rule *) let onlyparse = is_only_parsing modifiers in let onlyprint = is_only_printing modifiers in - let compat = get_compat_version modifiers in - try add_notation_interpretation_core local df env c sc onlyparse onlyprint compat + try add_notation_interpretation_core ~local df env c sc onlyparse onlyprint deprecation with NoSyntaxRule -> (* Try to determine a default syntax rule *) - add_notation_in_scope local df env c modifiers sc + add_notation_in_scope ~local deprecation df env c modifiers sc else (* Declare both syntax and interpretation *) - add_notation_in_scope local df env c modifiers sc + add_notation_in_scope ~local deprecation df env c modifiers sc in Dumpglob.dump_notation (loc,df') sc true @@ -1566,7 +1574,7 @@ let add_notation_extra_printing_rule df k v = let inject_var x = CAst.make @@ CRef (qualid_of_ident x,None) -let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc = +let add_infix ~local deprecation env ({CAst.loc;v=inf},modifiers) pr sc = check_infix_modifiers modifiers; (* check the precedence *) let vars = names_of_constr_expr pr in @@ -1575,7 +1583,7 @@ let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc = let metas = [inject_var x; inject_var y] in let c = mkAppC (pr,metas) in let df = CAst.make ?loc @@ Id.to_string x ^" "^(quote_notation_token inf)^" "^Id.to_string y in - add_notation local env c (df,modifiers) sc + add_notation ~local deprecation env c (df,modifiers) sc (**********************************************************************) (* Scopes, delimiters and classes bound to scopes *) @@ -1651,7 +1659,7 @@ let try_interp_name_alias = function | [], { CAst.v = CRef (ref,_) } -> intern_reference ref | _ -> raise Not_found -let add_syntactic_definition env ident (vars,c) local onlyparse = +let add_syntactic_definition ~local deprecation env ident (vars,c) compat = let vars,reversibility,pat = try [], APrioriReversible, NRef (try_interp_name_alias (vars,c)) with Not_found -> @@ -1665,11 +1673,9 @@ let add_syntactic_definition env ident (vars,c) local onlyparse = let map id = let (_,sc) = Id.Map.find id nvars in (id, sc) in List.map map vars, reversibility, pat in - let onlyparse = match onlyparse with - | None when fst (printability None false reversibility pat) -> Some Flags.Current - | p -> p - in - Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat) + let deprecation, onlyparsing = merge_compat_deprecation compat deprecation in + let onlyparsing = onlyparsing || fst (printability None false reversibility pat) in + Syntax_def.declare_syntactic_definition ~local deprecation ident ~onlyparsing (vars,pat) (**********************************************************************) (* Declaration of custom entry *) diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index 6435df23c7..44e08c4819 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -19,10 +19,10 @@ val add_token_obj : string -> unit (** Adding a (constr) notation in the environment*) -val add_infix : locality_flag -> env -> (lstring * syntax_modifier list) -> +val add_infix : local:bool -> Deprecation.t option -> env -> (lstring * syntax_modifier list) -> constr_expr -> scope_name option -> unit -val add_notation : locality_flag -> env -> constr_expr -> +val add_notation : local:bool -> Deprecation.t option -> env -> constr_expr -> (lstring * syntax_modifier list) -> scope_name option -> unit val add_notation_extra_printing_rule : string -> string -> string -> unit @@ -47,12 +47,12 @@ val set_notation_for_interpretation : env -> Constrintern.internalization_env -> (** Add only the parsing/printing rule of a notation *) val add_syntax_extension : - locality_flag -> (lstring * syntax_modifier list) -> unit + local:bool -> (lstring * syntax_modifier list) -> unit (** Add a syntactic definition (as in "Notation f := ...") *) -val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr -> - bool -> Flags.compat_version option -> unit +val add_syntactic_definition : local:bool -> Deprecation.t option -> env -> + Id.t -> Id.t list * constr_expr -> Flags.compat_version option -> unit (** Print the Camlp5 state of a grammar *) diff --git a/vernac/mltop.ml b/vernac/mltop.ml index bbee9988d0..0130de2543 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/mltop.mli b/vernac/mltop.mli index b457c9c88f..56a28b64b0 100644 --- a/vernac/mltop.mli +++ b/vernac/mltop.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index bc741a0ec7..aa15718452 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -1,8 +1,15 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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 Printf -open Libobject -open Entries open Decl_kinds -open Declare (** - Get types of existentials ; @@ -13,7 +20,6 @@ open Declare open Term open Constr -open Context open Vars open Names open Evd @@ -23,7 +29,7 @@ open Util module NamedDecl = Context.Named.Declaration -let get_fix_exn, stm_get_fix_exn = Hook.make () +open DeclareObl let succfix (depth, fixrels) = (succ depth, List.map succ fixrels) @@ -163,16 +169,16 @@ let evar_dependencies evm oev = else aux deps' in aux (Evar.Set.singleton oev) -let move_after (id, ev, deps as obl) l = +let move_after (id, ev, deps as obl) l = let rec aux restdeps = function - | (id', _, _) as obl' :: tl -> + | (id', _, _) as obl' :: tl -> let restdeps' = Evar.Set.remove id' restdeps in if Evar.Set.is_empty restdeps' then obl' :: obl :: tl else obl' :: aux restdeps' tl | [] -> [obl] in aux (Evar.Set.remove id deps) l - + let sort_dependencies evl = let rec aux l found list = match l with @@ -186,7 +192,7 @@ let sort_dependencies evl = open Environ -let eterm_obligations env name evm fs ?status t ty = +let eterm_obligations env name evm fs ?status t ty = (* 'Serialize' the evars *) let nc = Environ.named_context env in let nc_len = Context.Named.length nc in @@ -253,10 +259,6 @@ let eterm_obligations env name evm fs ?status t ty = let evmap f c = pi1 (subst_evar_constr evm evts 0 f c) in Array.of_list (List.rev evars), (evnames, evmap), t', ty -let hide_obligation () = - Coqlib.check_required_library ["Coq";"Program";"Tactics"]; - UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "program.tactics.obligation") - let pperror cmd = CErrors.user_err ~hdr:"Program" cmd let error s = pperror (str s) @@ -276,386 +278,27 @@ type obligation_info = (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array -type 'a obligation_body = - | DefinedObl of 'a - | TermObl of constr - -type obligation = - { obl_name : Id.t; - obl_type : types; - obl_location : Evar_kinds.t Loc.located; - obl_body : pconstant obligation_body option; - obl_status : bool * Evar_kinds.obligation_definition_status; - obl_deps : Int.Set.t; - obl_tac : unit Proofview.tactic option; - } - -type obligations = (obligation array * int) - -type fixpoint_kind = - | IsFixpoint of lident option list - | IsCoFixpoint - -type notations = (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list - -type program_info_aux = { - prg_name: Id.t; - prg_body: constr; - prg_type: constr; - prg_ctx: UState.t; - prg_univdecl: UState.universe_decl; - prg_obligations: obligations; - prg_deps : Id.t list; - prg_fixkind : fixpoint_kind option ; - prg_implicits : (Constrexpr.explicitation * (bool * bool * bool)) list; - prg_notations : notations ; - prg_kind : definition_kind; - prg_reduce : constr -> constr; - prg_hook : Lemmas.declaration_hook option; - prg_opaque : bool; - prg_sign: named_context_val; -} - -type program_info = program_info_aux CEphemeron.key - -let get_info x = - try CEphemeron.get x - with CEphemeron.InvalidKey -> - CErrors.anomaly Pp.(str "Program obligation can't be accessed by a worker.") - let assumption_message = Declare.assumption_message let default_tactic = ref (Proofview.tclUNIT ()) -(* true = hide obligations *) -let get_hide_obligations = - Goptions.declare_bool_option_and_ref - ~depr:false - ~name:"Hiding of Program obligations" - ~key:["Hide";"Obligations"] - ~value:false - - -let get_shrink_obligations = - Goptions.declare_bool_option_and_ref - ~depr:true (* remove in 8.8 *) - ~name:"Shrinking of Program obligations" - ~key:["Shrink";"Obligations"] - ~value:true - let evar_of_obligation o = make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type) -let get_obligation_body expand obl = - match obl.obl_body with - | None -> None - | Some c -> - if expand && snd obl.obl_status == Evar_kinds.Expand then - match c with - | DefinedObl pc -> Some (constant_value_in (Global.env ()) pc) - | TermObl c -> Some c - else (match c with - | DefinedObl pc -> Some (mkConstU pc) - | TermObl c -> Some c) - -let obl_substitution expand obls deps = - Int.Set.fold - (fun x acc -> - let xobl = obls.(x) in - match get_obligation_body expand xobl with - | None -> acc - | Some oblb -> (xobl.obl_name, (xobl.obl_type, oblb)) :: acc) - deps [] - let subst_deps expand obls deps t = let osubst = obl_substitution expand obls deps in (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t) -let rec prod_app t n = - match Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) (* FIXME *) with - | Prod (_,_,b) -> subst1 n b - | LetIn (_, b, t, b') -> prod_app (subst1 b b') n - | _ -> - user_err ~hdr:"prod_app" - (str"Needed a product, but didn't find one" ++ fnl ()) - - -(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *) -let prod_applist t nL = List.fold_left prod_app t nL - -let replace_appvars subst = - let rec aux c = - let f, l = decompose_app c in - if isVar f then - try - let c' = List.map (Constr.map aux) l in - let (t, b) = Id.List.assoc (destVar f) subst in - mkApp (delayed_force hide_obligation, - [| prod_applist t c'; applistc b c' |]) - with Not_found -> Constr.map aux c - else Constr.map aux c - in Constr.map aux - let subst_deps_obl obls obl = let t' = subst_deps true obls obl.obl_deps obl.obl_type in { obl with obl_type = t' } -module ProgMap = Id.Map - -let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m) - -let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] - -let from_prg, program_tcc_summary_tag = - Summary.ref_tag ProgMap.empty ~name:"program-tcc-table" - -let close sec = - if not (ProgMap.is_empty !from_prg) then - let keys = map_keys !from_prg in - user_err ~hdr:"Program" - (str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++ - prlist_with_sep spc (fun x -> Id.print x) keys ++ - (str (if Int.equal (List.length keys) 1 then " has " else " have ") ++ - str "unsolved obligations")) - -let input : program_info ProgMap.t -> obj = - declare_object - { (default_object "Program state") with - cache_function = (fun (na, pi) -> from_prg := pi); - load_function = (fun _ (_, pi) -> from_prg := pi); - discharge_function = (fun _ -> close "section"; None); - classify_function = (fun _ -> close "module"; Dispose) } - open Evd -let progmap_remove prg = - Lib.add_anonymous_leaf (input (ProgMap.remove prg.prg_name !from_prg)) - -let progmap_add n prg = - Lib.add_anonymous_leaf (input (ProgMap.add n prg !from_prg)) - -let progmap_replace prg' = - Lib.add_anonymous_leaf (input (map_replace prg'.prg_name prg' !from_prg)) - -let rec intset_to = function - -1 -> Int.Set.empty - | n -> Int.Set.add n (intset_to (pred n)) - -let subst_prog subst prg = - if get_hide_obligations () then - (replace_appvars subst prg.prg_body, - replace_appvars subst ((* Termops.refresh_universes *) prg.prg_type)) - else - let subst' = List.map (fun (n, (_, b)) -> n, b) subst in - (Vars.replace_vars subst' prg.prg_body, - Vars.replace_vars subst' ((* Termops.refresh_universes *) prg.prg_type)) - -let obligation_substitution expand prg = - let obls, _ = prg.prg_obligations in - let ints = intset_to (pred (Array.length obls)) in - obl_substitution expand obls ints - -let declare_definition prg = - let varsubst = obligation_substitution true prg in - let body, typ = subst_prog varsubst prg in - let nf = UnivSubst.nf_evars_and_universes_opt_subst (fun x -> None) - (UState.subst prg.prg_ctx) in - let opaque = prg.prg_opaque in - let fix_exn = Hook.get get_fix_exn () in - let typ = nf typ in - let body = nf body in - let obls = List.map (fun (id, (_, c)) -> (id, nf c)) varsubst in - let uvars = Univ.LSet.union - (Vars.universes_of_constr typ) - (Vars.universes_of_constr body) in - let uctx = UState.restrict prg.prg_ctx uvars in - let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl in - let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in - let () = progmap_remove prg in - let ubinders = UState.universe_binders uctx in - let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in - DeclareDef.declare_definition prg.prg_name - prg.prg_kind ce ubinders prg.prg_implicits ?hook_data - -let rec lam_index n t acc = - match Constr.kind t with - | Lambda ({binder_name=Name n'}, _, _) when Id.equal n n' -> - acc - | Lambda (_, _, b) -> - lam_index n b (succ acc) - | _ -> raise Not_found - -let compute_possible_guardness_evidences n fixbody fixtype = - match n with - | Some { CAst.loc; v = n } -> [lam_index n fixbody 0] - | None -> - (* If recursive argument was not given by user, we try all args. - An earlier approach was to look only for inductive arguments, - but doing it properly involves delta-reduction, and it finally - doesn't seem to worth the effort (except for huge mutual - fixpoints ?) *) - let m = Termops.nb_prod Evd.empty (EConstr.of_constr fixtype) (* FIXME *) in - let ctx = fst (decompose_prod_n_assum m fixtype) in - List.map_i (fun i _ -> i) 0 ctx - -let mk_proof c = ((c, Univ.ContextSet.empty), Safe_typing.empty_private_constants) - -let declare_mutual_definition l = - let len = List.length l in - let first = List.hd l in - let defobl x = - let oblsubst = obligation_substitution true x in - let subs, typ = subst_prog oblsubst x in - let env = Global.env () in - let sigma = Evd.from_ctx x.prg_ctx in - let r = Retyping.relevance_of_type env sigma (EConstr.of_constr typ) in - let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) in - let typ = snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) in - let term = EConstr.to_constr sigma term in - let typ = EConstr.to_constr sigma typ in - let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_implicits) in - let oblsubst = List.map (fun (id, (_, c)) -> id, c) oblsubst in - def, oblsubst - in - let defs, obls = - List.fold_right (fun x (defs, obls) -> - let xdef, xobls = defobl x in - (xdef :: defs, xobls @ obls)) l ([], []) - in -(* let fixdefs = List.map reduce_fix fixdefs in *) - let fixdefs, fixrs, fixtypes, fiximps = List.split4 defs in - let fixkind = Option.get first.prg_fixkind in - let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in - let rvec = Array.of_list fixrs in - let namevec = Array.of_list (List.map (fun x -> Name x.prg_name) l) in - let fixdecls = (Array.map2 make_annot namevec rvec, arrrec, recvec) in - let (local,poly,kind) = first.prg_kind in - let fixnames = first.prg_deps in - let opaque = first.prg_opaque in - let kind = if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in - let indexes, fixdecls = - match fixkind with - | IsFixpoint wfl -> - let possible_indexes = - List.map3 compute_possible_guardness_evidences - wfl fixdefs fixtypes in - let indexes = - Pretyping.search_guard (Global.env()) - possible_indexes fixdecls in - Some indexes, - List.map_i (fun i _ -> - mk_proof (mkFix ((indexes,i),fixdecls))) 0 l - | IsCoFixpoint -> - None, - List.map_i (fun i _ -> - mk_proof (mkCoFix (i,fixdecls))) 0 l - in - (* Declare the recursive definitions *) - let univs = UState.univ_entry ~poly first.prg_ctx in - let fix_exn = Hook.get get_fix_exn () in - let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs) - fixnames fixdecls fixtypes fiximps in - (* Declare notations *) - List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations; - Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; - let gr = List.hd kns in - Lemmas.call_hook ?hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr; - List.iter progmap_remove l; gr - -let decompose_lam_prod c ty = - let open Context.Rel.Declaration in - let rec aux ctx c ty = - match Constr.kind c, Constr.kind ty with - | LetIn (x, b, t, c), LetIn (x', b', t', ty) - when Constr.equal b b' && Constr.equal t t' -> - let ctx' = Context.Rel.add (LocalDef (x,b',t')) ctx in - aux ctx' c ty - | _, LetIn (x', b', t', ty) -> - let ctx' = Context.Rel.add (LocalDef (x',b',t')) ctx in - aux ctx' (lift 1 c) ty - | LetIn (x, b, t, c), _ -> - let ctx' = Context.Rel.add (LocalDef (x,b,t)) ctx in - aux ctx' c (lift 1 ty) - | Lambda (x, b, t), Prod (x', b', t') - (* By invariant, must be convertible *) -> - let ctx' = Context.Rel.add (LocalAssum (x,b')) ctx in - aux ctx' t t' - | Cast (c, _, _), _ -> aux ctx c ty - | _, _ -> ctx, c, ty - in aux Context.Rel.empty c ty - -let shrink_body c ty = - let ctx, b, ty = - match ty with - | None -> - let ctx, b = decompose_lam_assum c in - ctx, b, None - | Some ty -> - let ctx, b, ty = decompose_lam_prod c ty in - ctx, b, Some ty - in - let b', ty', n, args = - List.fold_left (fun (b, ty, i, args) decl -> - if noccurn 1 b && Option.cata (noccurn 1) true ty then - subst1 mkProp b, Option.map (subst1 mkProp) ty, succ i, args - else - let open Context.Rel.Declaration in - let args = if is_local_assum decl then mkRel i :: args else args in - mkLambda_or_LetIn decl b, Option.map (mkProd_or_LetIn decl) ty, - succ i, args) - (b, ty, 1, []) ctx - in ctx, b', ty', Array.of_list args - let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst] let add_hint local prg cst = Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst) -let it_mkLambda_or_LetIn_or_clean t ctx = - let open Context.Rel.Declaration in - let fold t decl = - if is_local_assum decl then mkLambda_or_LetIn decl t - else - if noccurn 1 t then subst1 mkProp t - else mkLambda_or_LetIn decl t - in - Context.Rel.fold_inside fold ctx ~init:t - -let declare_obligation prg obl body ty uctx = - let body = prg.prg_reduce body in - let ty = Option.map prg.prg_reduce ty in - match obl.obl_status with - | _, Evar_kinds.Expand -> false, { obl with obl_body = Some (TermObl body) } - | force, Evar_kinds.Define opaque -> - let opaque = not force && opaque in - let poly = pi2 prg.prg_kind in - let ctx, body, ty, args = - if get_shrink_obligations () && not poly then - shrink_body body ty else [], body, ty, [||] - in - let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in - let ce = - { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body; - const_entry_secctx = None; - const_entry_type = ty; - const_entry_universes = uctx; - const_entry_opaque = opaque; - const_entry_inline_code = false; - const_entry_feedback = None; - } in - (* ppedrot: seems legit to have obligations as local *) - let constant = Declare.declare_constant obl.obl_name ~local:true - (DefinitionEntry ce,IsProof Property) - in - if not opaque then add_hint (Locality.make_section_locality None) prg constant; - definition_message obl.obl_name; - let body = match uctx with - | Polymorphic_entry (_, uctx) -> - Some (DefinedObl (constant, Univ.UContext.instance uctx)) - | Monomorphic_entry _ -> - Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) - in - true, { obl with obl_body = body } - let init_prog_info ?(opaque = false) ?hook sign n udecl b t ctx deps fixkind notations obls impls kind reduce = let obls', b = @@ -671,27 +314,27 @@ let init_prog_info ?(opaque = false) ?hook sign n udecl b t ctx deps fixkind | Some b -> Array.mapi (fun i (n, t, l, o, d, tac) -> - { obl_name = n ; obl_body = None; + { obl_name = n ; obl_body = None; obl_location = l; obl_type = t; obl_status = o; obl_deps = d; obl_tac = tac }) obls, b in let ctx = UState.make_flexible_nonalgebraic ctx in - { prg_name = n ; prg_body = b; prg_type = reduce t; + { prg_name = n ; prg_body = b; prg_type = reduce t; prg_ctx = ctx; prg_univdecl = udecl; prg_obligations = (obls', Array.length obls'); prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ; - prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; + prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; prg_hook = hook; prg_opaque = opaque; prg_sign = sign } let map_cardinal m = let i = ref 0 in ProgMap.iter (fun _ v -> - if snd (CEphemeron.get v).prg_obligations > 0 then incr i) m; + if snd (CEphemeron.get v).prg_obligations > 0 then incr i) m; !i -exception Found of program_info +exception Found of program_info CEphemeron.key let map_first m = try @@ -702,28 +345,28 @@ let map_first m = with Found x -> x let get_prog name = - let prg_infos = !from_prg in + let prg_infos = get_prg_info_map () in match name with Some n -> - (try get_info (ProgMap.find n prg_infos) + (try CEphemeron.get (ProgMap.find n prg_infos) with Not_found -> raise (NoObligations (Some n))) | None -> (let n = map_cardinal prg_infos in match n with 0 -> raise (NoObligations None) - | 1 -> get_info (map_first prg_infos) + | 1 -> CEphemeron.get (map_first prg_infos) | _ -> let progs = Id.Set.elements (ProgMap.domain prg_infos) in let prog = List.hd progs in let progs = prlist_with_sep pr_comma Id.print progs in - user_err + user_err (str "More than one program with unsolved obligations: " ++ progs ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Id.print prog ++ str "\"")) let get_any_prog () = - let prg_infos = !from_prg in + let prg_infos = get_prg_info_map () in let n = map_cardinal prg_infos in - if n > 0 then get_info (map_first prg_infos) + if n > 0 then CEphemeron.get (map_first prg_infos) else raise (NoObligations None) let get_prog_err n = @@ -732,42 +375,8 @@ let get_prog_err n = let get_any_prog_err () = try get_any_prog () with NoObligations id -> pperror (explain_no_obligations id) -let obligations_solved prg = Int.equal (snd prg.prg_obligations) 0 - let all_programs () = - ProgMap.fold (fun k p l -> p :: l) !from_prg [] - -type progress = - | Remain of int - | Dependent - | Defined of GlobRef.t - -let obligations_message rem = - if rem > 0 then - if Int.equal rem 1 then - Flags.if_verbose Feedback.msg_info (int rem ++ str " obligation remaining") - else - Flags.if_verbose Feedback.msg_info (int rem ++ str " obligations remaining") - else - Flags.if_verbose Feedback.msg_info (str "No more obligations remaining") - -let update_obls prg obls rem = - let prg' = { prg with prg_obligations = (obls, rem) } in - progmap_replace prg'; - obligations_message rem; - if rem > 0 then Remain rem - else ( - match prg'.prg_deps with - | [] -> - let kn = declare_definition prg' in - progmap_remove prg'; - Defined kn - | l -> - let progs = List.map (fun x -> get_info (ProgMap.find x !from_prg)) prg'.prg_deps in - if List.for_all (fun x -> obligations_solved x) progs then - let kn = declare_mutual_definition progs in - Defined kn - else Dependent) + ProgMap.fold (fun k p l -> p :: l) (get_prg_info_map ()) [] let is_defined obls x = not (Option.is_empty obls.(x).obl_body) @@ -778,30 +387,18 @@ let deps_remaining obls deps = else x :: acc) deps [] -let dependencies obls n = - let res = ref Int.Set.empty in - Array.iteri - (fun i obl -> - if not (Int.equal i n) && Int.Set.mem n obl.obl_deps then - res := Int.Set.add i !res) - obls; - !res -let goal_kind poly = Decl_kinds.Local, poly, Decl_kinds.DefinitionBody Decl_kinds.Definition +let goal_kind poly = + Decl_kinds.(Global ImportNeedQualified, poly, DefinitionBody Definition) -let goal_proof_kind poly = Decl_kinds.Local, poly, Decl_kinds.Proof Decl_kinds.Lemma +let goal_proof_kind poly = + Decl_kinds.(Global ImportNeedQualified, poly, Proof Lemma) let kind_of_obligation poly o = match o with | Evar_kinds.Define false | Evar_kinds.Expand -> goal_kind poly | _ -> goal_proof_kind poly -let not_transp_msg = - str "Obligation should be transparent but was declared opaque." ++ spc () ++ - str"Use 'Defined' instead." - -let err_not_transp () = pperror not_transp_msg - let rec string_of_list sep f = function [] -> "" | x :: [] -> f x @@ -820,11 +417,11 @@ let solve_by_tac ?loc name evi t poly ctx = Pfedit.build_constant_by_tactic id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl t in let env = Global.env () in - let body = Future.force entry.const_entry_body in - let body = Safe_typing.inline_private_constants env body in + let (body, eff) = Future.force entry.Proof_global.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.const_entry_type, Evd.evar_universe_context ctx') + Some (fst body, entry.Proof_global.proof_entry_type, Evd.evar_universe_context ctx') with | Refiner.FailError (_, s) as exn -> let _ = CErrors.push exn in @@ -837,80 +434,12 @@ let solve_by_tac ?loc name evi t poly ctx = warn_solve_errored ?loc err; None -let obligation_terminator ?hook name num guard auto pf = - let open Proof_global in - let term = Lemmas.standard_proof_terminator ?hook guard in - match pf with - | Admitted _ -> apply_terminator term pf - | Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin - let env = Global.env () in - let ty = entry.Entries.const_entry_type in - let body = Future.force entry.const_entry_body in - let (body, cstr) = Safe_typing.inline_private_constants env body in - let sigma = Evd.from_ctx uctx in - let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in - Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body); - (* Declare the obligation ourselves and drop the hook *) - let prg = get_info (ProgMap.find name !from_prg) in - (* Ensure universes are substituted properly in body and type *) - let body = EConstr.to_constr sigma (EConstr.of_constr body) in - let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in - let ctx = Evd.evar_universe_context sigma in - let obls, rem = prg.prg_obligations in - let obl = obls.(num) in - let status = - match obl.obl_status, opq with - | (_, Evar_kinds.Expand), Opaque -> err_not_transp () - | (true, _), Opaque -> err_not_transp () - | (false, _), Opaque -> Evar_kinds.Define true - | (_, Evar_kinds.Define true), Transparent -> - Evar_kinds.Define false - | (_, status), Transparent -> status - in - let obl = { obl with obl_status = false, status } in - let ctx = - if pi2 prg.prg_kind then ctx - else UState.union prg.prg_ctx ctx - in - let uctx = UState.univ_entry ~poly:(pi2 prg.prg_kind) ctx in - let (defined, obl) = declare_obligation prg obl body ty uctx in - let obls = Array.copy obls in - let () = obls.(num) <- obl in - let prg_ctx = - if pi2 (prg.prg_kind) then (* Polymorphic *) - (* We merge the new universes and constraints of the - polymorphic obligation with the existing ones *) - UState.union prg.prg_ctx ctx - else - (* The first obligation, if defined, - declares the univs of the constant, - each subsequent obligation declares its own additional - universes and constraints if any *) - if defined then UState.make (Global.universes ()) - else ctx - in - let prg = { prg with prg_ctx } in - try - ignore (update_obls prg obls (pred rem)); - if pred rem > 0 then - begin - let deps = dependencies obls num in - if not (Int.Set.is_empty deps) then - ignore (auto (Some name) None deps) - end - with e when CErrors.noncritical e -> - let e = CErrors.push e in - pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e)) - end - | Proved (_, _, _ ) -> - CErrors.anomaly Pp.(str "[obligation_terminator] close_proof returned more than one proof term") - let obligation_hook prg obl num auto ctx' _ _ gr = let obls, rem = prg.prg_obligations in let cst = match gr with GlobRef.ConstRef cst -> cst | _ -> assert false in let transparent = evaluable_constant cst (Global.env ()) in let () = match obl.obl_status with - (true, Evar_kinds.Expand) + (true, Evar_kinds.Expand) | (true, Evar_kinds.Define true) -> if not transparent then err_not_transp () | _ -> () @@ -941,10 +470,10 @@ let obligation_hook prg obl num auto ctx' _ _ gr = if pred rem > 0 then begin let deps = dependencies obls num in if not (Int.Set.is_empty deps) then - ignore (auto (Some prg.prg_name) None deps) + ignore (auto (Some prg.prg_name) deps None) end -let rec solve_obligation ~ontop prg num tac = +let rec solve_obligation prg num tac = let user_num = succ num in let obls, rem = prg.prg_obligations in let obl = obls.(num) in @@ -960,24 +489,22 @@ let rec solve_obligation ~ontop prg num tac = let kind = kind_of_obligation (pi2 prg.prg_kind) (snd obl.obl_status) in let evd = Evd.from_ctx prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in - let auto n tac oblset = auto_solve_obligations n ~oblset tac in - let terminator ?hook guard = - Proof_global.make_terminator - (obligation_terminator prg.prg_name num guard ?hook auto) in - let hook = Lemmas.mk_hook (obligation_hook prg obl num auto) in - let pstate = Lemmas.start_proof ~ontop ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in - let pstate = fst @@ Pfedit.by !default_tactic pstate in - let pstate = Option.cata (fun tac -> Proof_global.set_endline_tactic tac pstate) pstate tac in - pstate - -and obligation ~ontop (user_num, name, typ) tac = + let auto n oblset tac = auto_solve_obligations n ~oblset tac in + let proof_ending = Lemmas.Proof_ending.End_obligation (DeclareObl.{name = prg.prg_name; num; auto}) in + let hook = DeclareDef.Hook.make (obligation_hook prg obl num auto) in + let lemma = Lemmas.start_lemma ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~proof_ending ~hook in + let lemma = fst @@ Lemmas.by !default_tactic lemma in + let lemma = Option.cata (fun tac -> Lemmas.set_endline_tactic tac lemma) lemma tac in + lemma + +and obligation (user_num, name, typ) tac = let num = pred user_num in let prg = get_prog_err name in let obls, rem = prg.prg_obligations in if num >= 0 && num < Array.length obls then let obl = obls.(num) in match obl.obl_body with - | None -> solve_obligation ~ontop prg num tac + | None -> solve_obligation prg num tac | Some r -> error "Obligation already solved" else error (sprintf "Unknown obligation number %i" (succ num)) @@ -1046,7 +573,7 @@ and solve_obligations n tac = solve_prg_obligations prg tac and solve_all_obligations tac = - ProgMap.iter (fun k v -> ignore(solve_prg_obligations (get_info v) tac)) !from_prg + ProgMap.iter (fun k v -> ignore(solve_prg_obligations (CEphemeron.get v) tac)) (get_prg_info_map ()) and try_solve_obligation n prg tac = let prg = get_prog prg in @@ -1088,9 +615,9 @@ let show_obligations ?(msg=true) n = let progs = match n with | None -> all_programs () | Some n -> - try [ProgMap.find n !from_prg] + try [ProgMap.find n (get_prg_info_map ())] with Not_found -> raise (NoObligations (Some n)) - in List.iter (fun x -> show_obligations_of_prg ~msg (get_info x)) progs + in List.iter (fun x -> show_obligations_of_prg ~msg (CEphemeron.get x)) progs let show_term n = let prg = get_prog_err n in @@ -1102,7 +629,7 @@ let show_term n = ++ Printer.pr_constr_env env sigma prg.prg_body) let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) - ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic + ?(implicits=[]) ?(kind=Global ImportDefaultBehavior,false,Definition) ?tactic ?(reduce=reduce) ?hook ?(opaque = false) obls = let sign = Lemmas.initialize_named_context_for_proof () in let info = Id.print n ++ str " has type-checked" in @@ -1110,8 +637,8 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) let obls,_ = prg.prg_obligations in if Int.equal (Array.length obls) 0 then ( Flags.if_verbose Feedback.msg_info (info ++ str "."); - let cst = declare_definition prg in - Defined cst) + let cst = DeclareObl.declare_definition prg in + Defined cst) else ( let len = Array.length obls in let () = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in @@ -1122,7 +649,7 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) | _ -> res) let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic - ?(kind=Global,false,Definition) ?(reduce=reduce) + ?(kind=Global ImportDefaultBehavior,false,Definition) ?(reduce=reduce) ?hook ?(opaque = false) notations fixkind = let sign = Lemmas.initialize_named_context_for_proof () in let deps = List.map (fun (n, b, t, imps, obls) -> n) l in @@ -1137,8 +664,8 @@ let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic else let res = auto_solve_obligations (Some x) tactic in match res with - | Defined _ -> - (* If one definition is turned into a constant, + | Defined _ -> + (* If one definition is turned into a constant, the whole block is defined. *) true | _ -> false) false deps @@ -1147,14 +674,14 @@ let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic let admit_prog prg = let obls, rem = prg.prg_obligations in let obls = Array.copy obls in - Array.iteri + Array.iteri (fun i x -> match x.obl_body with | None -> let x = subst_deps_obl obls x in let ctx = UState.univ_entry ~poly:false prg.prg_ctx in - let kn = Declare.declare_constant x.obl_name ~local:true - (ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural) + let kn = Declare.declare_constant x.obl_name ~local:ImportNeedQualified + (Declare.ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural) in assumption_message x.obl_name; obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) } @@ -1177,7 +704,7 @@ let admit_obligations n = let prg = get_prog_err n in admit_prog prg -let next_obligation ~ontop n tac = +let next_obligation n tac = let prg = match n with | None -> get_any_prog_err () | Some _ -> get_prog_err n @@ -1188,7 +715,7 @@ let next_obligation ~ontop n tac = | Some i -> i | None -> anomaly (Pp.str "Could not find a solvable obligation.") in - solve_obligation ~ontop prg i tac + solve_obligation prg i tac let check_program_libraries () = Coqlib.check_required_library Coqlib.datatypes_module_name; diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 9214ddd4b9..a0010a5026 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -13,11 +13,6 @@ open Constr open Evd open Names -(* This is a hack to make it possible for Obligations to craft a Qed - * behind the scenes. The fix_exn the Stm attaches to the Future proof - * is not available here, so we provide a side channel to get it *) -val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) Hook.t - val check_evars : env -> evar_map -> unit val evar_dependencies : evar_map -> Evar.t -> Evar.Set.t @@ -45,11 +40,6 @@ type obligation_info = (* ident, type, location, (opaque or transparent, expand or define), dependencies, tactic to solve it *) -type progress = (* Resolution status of a program *) - | Remain of int (* n obligations remaining *) - | Dependent (* Dependent on other definitions *) - | Defined of GlobRef.t (* Defined as id *) - val default_tactic : unit Proofview.tactic ref val add_definition @@ -57,47 +47,38 @@ val add_definition -> ?term:constr -> types -> UState.t -> ?univdecl:UState.universe_decl (* Universe binders and constraints *) - -> ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list + -> ?implicits:Impargs.manual_implicits -> ?kind:Decl_kinds.definition_kind -> ?tactic:unit Proofview.tactic -> ?reduce:(constr -> constr) - -> ?hook:Lemmas.declaration_hook + -> ?hook:DeclareDef.Hook.t -> ?opaque:bool -> obligation_info - -> progress - -type notations = - (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list - -type fixpoint_kind = - | IsFixpoint of lident option list - | IsCoFixpoint + -> DeclareObl.progress val add_mutual_definitions : - (Names.Id.t * constr * types * - (Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list -> + (Names.Id.t * constr * types * Impargs.manual_implicits * obligation_info) list -> UState.t -> ?univdecl:UState.universe_decl -> (* Universe binders and constraints *) ?tactic:unit Proofview.tactic -> ?kind:Decl_kinds.definition_kind -> ?reduce:(constr -> constr) -> - ?hook:Lemmas.declaration_hook -> ?opaque:bool -> - notations -> - fixpoint_kind -> unit + ?hook:DeclareDef.Hook.t -> ?opaque:bool -> + DeclareObl.notations -> + DeclareObl.fixpoint_kind -> unit val obligation - : ontop:Proof_global.t option - -> int * Names.Id.t option * Constrexpr.constr_expr option + : int * Names.Id.t option * Constrexpr.constr_expr option -> Genarg.glob_generic_argument option - -> Proof_global.t + -> Lemmas.t val next_obligation - : ontop:Proof_global.t option - -> Names.Id.t option + : Names.Id.t option -> Genarg.glob_generic_argument option - -> Proof_global.t + -> Lemmas.t -val solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> progress +val solve_obligations : Names.Id.t option -> unit Proofview.tactic option + -> DeclareObl.progress (* Number of remaining obligations to be solved for this program *) val solve_all_obligations : unit Proofview.tactic option -> unit @@ -117,6 +98,3 @@ exception NoObligations of Names.Id.t option val explain_no_obligations : Names.Id.t option -> Pp.t val check_program_libraries : unit -> unit - -type program_info -val program_tcc_summary_tag : program_info Id.Map.t Summary.Dyn.tag diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index e307c0c268..4f053b98ae 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -39,8 +39,8 @@ open Pputils pr_sep_com spc @@ pr_lconstr_expr env sigma let pr_uconstraint (l, d, r) = - pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ - pr_glob_level r + pr_glob_sort_name l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ + pr_glob_sort_name r let pr_univ_name_list = function | None -> mt () @@ -359,6 +359,8 @@ open Pputils keyword (if many then "Variables" else "Variable") | (DoDischarge,Conjectural) -> anomaly (Pp.str "Don't know how to beautify a local conjecture.") + | (_,Context) -> + anomaly (Pp.str "Context is used only internally.") let pr_params pr_c (xl,(c,t)) = hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++ @@ -628,7 +630,6 @@ open Pputils let pr_showable = function | ShowGoal n -> keyword "Show" ++ pr_goal_reference n | ShowProof -> keyword "Show Proof" - | ShowScript -> keyword "Show Script" | ShowExistentials -> keyword "Show Existentials" | ShowUniverses -> keyword "Show Universes" | ShowProofNames -> keyword "Show Conjectures" diff --git a/vernac/ppvernac.mli b/vernac/ppvernac.mli index 4aa24bf5db..d4d49a09a3 100644 --- a/vernac/ppvernac.mli +++ b/vernac/ppvernac.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index 1d089d0a55..094e2c1184 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/proof_using.mli b/vernac/proof_using.mli index 702043a4a9..a0567eef47 100644 --- a/vernac/proof_using.mli +++ b/vernac/proof_using.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index 4d9157089c..da28e260b3 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli index 41a2e7fd6f..c9eb979a90 100644 --- a/vernac/pvernac.mli +++ b/vernac/pvernac.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/record.ml b/vernac/record.ml index f737a8c524..9e3353bc54 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -125,7 +125,7 @@ let typecheck_params_and_fields finite def poly pl ps records = let env = EConstr.push_rel_context newps env0 in let poly = match t with - | { CAst.v = CSort (Glob_term.GType []) } -> true | _ -> false in + | { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true | _ -> false in let sigma, s = interp_type_evars ~program_mode:false env sigma ~impls:empty_internalization_env t in let sred = Reductionops.whd_allnolet env sigma s in (match EConstr.kind sigma sred with @@ -342,16 +342,17 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name flags f let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in try + let open Proof_global in let entry = { - const_entry_body = - Future.from_val (Safe_typing.mk_pure_proof proj); - const_entry_secctx = None; - const_entry_type = Some projtyp; - const_entry_universes = ctx; - const_entry_opaque = false; - const_entry_inline_code = false; - const_entry_feedback = None } in - let k = (DefinitionEntry entry,IsDefinition kind) in + 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 k = (Declare.DefinitionEntry entry,IsDefinition kind) in let kn = declare_constant ~internal:InternalTacticRequest fid k in let constr_fip = let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in @@ -476,21 +477,15 @@ let declare_structure ~cum finite ubinders univs paramimpls params template ?(ki List.mapi map record_data let implicits_of_context ctx = - List.map_i (fun i name -> - let explname = - match name with - | Name n -> Some n - | Anonymous -> None - in ExplByPos (i, explname), (true, true, true)) - 1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) + List.map (fun name -> CAst.make (Some (name,true))) + (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) let declare_class def cum ubinders univs id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) coers priorities = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) - let len = List.length params in let impls = implicits_of_context params in - List.map (fun x -> impls @ Impargs.lift_implicits (succ len) x) fieldimpls + List.map (fun x -> impls @ x) fieldimpls in let binder_name = Namegen.next_ident_away id (Termops.vars_of_env (Global.env())) in let data = @@ -588,12 +583,14 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity let add_constant_class env sigma cst = let ty, univs = Typeops.type_of_global_in_context env (ConstRef cst) in let r = (Environ.lookup_constant cst env).const_relevance in - let ctx, arity = decompose_prod_assum ty in + let ctx, _ = decompose_prod_assum ty in + let args = Context.Rel.to_extended_vect Constr.mkRel 0 ctx in + let t = mkApp (mkConstU (cst, Univ.make_abstract_instance univs), args) in let tc = { cl_univs = univs; cl_impl = ConstRef cst; cl_context = (List.map (const None) ctx, ctx); - cl_props = [LocalAssum (make_annot Anonymous r, arity)]; + cl_props = [LocalAssum (make_annot Anonymous r, t)]; cl_projs = []; cl_strict = !typeclasses_strict; cl_unique = !typeclasses_unique @@ -702,7 +699,7 @@ let definition_structure udecl kind ~template cum poly finite records = declare_class def cum ubinders univs id.CAst.v idbuild implpars params arity template implfs fields coers priorities | _ -> - let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in + let map impls = implpars @ [CAst.make None] @ impls in let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) = let coe = List.map (fun (_, { rf_subclass ; rf_canonical }) -> diff --git a/vernac/record.mli b/vernac/record.mli index 24bb27e107..11d9a833e2 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/search.ml b/vernac/search.ml index 2e3a95bed2..a7f1dd33c2 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/search.mli b/vernac/search.mli index 0f94ddc5b6..029e8cf7b9 100644 --- a/vernac/search.mli +++ b/vernac/search.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index bf2efb2542..7644f4c5b6 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 3d522a9e0f..dc4642dc65 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 57c56a58f9..d28eeb341d 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -11,15 +11,16 @@ Egramml Vernacextend Ppvernac Proof_using -Lemmas -Canonical -Class Egramcoq Metasyntax +DeclareDef +DeclareObl +Canonical +Lemmas +Class Auto_ind_decl Search Indschemes -DeclareDef Obligations ComDefinition Classes diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 22427621e6..222f727f8e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -38,24 +38,25 @@ module NamedDecl = Context.Named.Declaration let (f_interp_redexp, interp_redexp_hook) = Hook.make () let debug = false + (* XXX Should move to a common library *) let vernac_pperr_endline pp = if debug then Format.eprintf "@[%a@]@\n%!" Pp.pp_with (pp ()) else () -(* Misc *) - -let there_are_pending_proofs ~pstate = - not Option.(is_empty pstate) - -let check_no_pending_proof ~pstate = - if there_are_pending_proofs ~pstate then - user_err Pp.(str "Command not supported (Open proofs remain)") +(* Utility functions, at some point they should all disappear and + instead enviroment/state selection should be done at the Vernac DSL + level. *) -let vernac_require_open_proof ~pstate f = - match pstate with - | Some pstate -> f ~pstate +(* EJGA: Only used in close_proof, can remove once the ?proof hack is no more *) +let vernac_require_open_lemma ~stack f = + match stack with + | Some stack -> f ~stack | None -> user_err Pp.(str "Command not supported (No proof-editing in progress)") +let with_pstate ~stack f = + vernac_require_open_lemma ~stack + (fun ~stack -> Stack.with_top_pstate stack ~f:(fun pstate -> f ~pstate)) + let get_current_or_global_context ~pstate = match pstate with | None -> let env = Global.env () in Evd.(from_env env, env) @@ -80,7 +81,7 @@ module DefAttributes = struct locality : bool option; polymorphic : bool; program : bool; - deprecated : deprecation option; + deprecated : Deprecation.t option; } let parse f = @@ -91,6 +92,26 @@ module DefAttributes = struct { polymorphic; program; locality; deprecated } end +let module_locality = Attributes.Notations.(locality >>= fun l -> return (make_module_locality l)) + +let with_locality ~atts f = + let local = Attributes.(parse locality atts) in + f ~local + +let with_section_locality ~atts f = + let local = Attributes.(parse locality atts) in + let section_local = make_section_locality local in + f ~section_local + +let with_module_locality ~atts f = + let module_local = Attributes.(parse module_locality atts) in + f ~module_local + +let with_def_attributes ~atts f = + let atts = DefAttributes.parse atts in + if atts.DefAttributes.program then Obligations.check_program_libraries (); + f ~atts + (*******************) (* "Show" commands *) @@ -98,7 +119,7 @@ let show_proof ~pstate = (* spiwack: this would probably be cooler with a bit of polishing. *) try let pstate = Option.get pstate in - let p = Proof_global.give_me_the_proof pstate in + let p = Proof_global.get_proof pstate in let sigma, env = Pfedit.get_current_context pstate in let pprf = Proof.partial_proof p in Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf @@ -108,24 +129,21 @@ let show_proof ~pstate = | Option.IsNone -> user_err (str "No goals to show.") -let show_top_evars ~pstate = +let show_top_evars ~proof = (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) - let pfts = Proof_global.give_me_the_proof pstate in - let Proof.{goals;shelf;given_up;sigma} = Proof.data pfts in + let Proof.{goals;shelf;given_up;sigma} = Proof.data proof in pr_evars_int sigma ~shelf ~given_up 1 (Evd.undefined_map sigma) -let show_universes ~pstate = - let pfts = Proof_global.give_me_the_proof pstate in - let Proof.{goals;sigma} = Proof.data pfts in +let show_universes ~proof = + let Proof.{goals;sigma} = Proof.data proof in let ctx = Evd.universe_context_set (Evd.minimize_universes sigma) in Termops.pr_evar_universe_context (Evd.evar_universe_context sigma) ++ fnl () ++ str "Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx (* Simulate the Intro(s) tactic *) -let show_intro ~pstate all = +let show_intro ~proof all = let open EConstr in - let pf = Proof_global.give_me_the_proof pstate in - let Proof.{goals;sigma} = Proof.data pf in + let Proof.{goals;sigma} = Proof.data proof in if not (List.is_empty goals) then begin let gl = {Evd.it=List.hd goals ; sigma = sigma; } in let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in @@ -405,7 +423,7 @@ let universe_subgraph ?loc g univ = let open Univ in let sigma = Evd.from_env (Global.env()) in let univs_of q = - let q = Glob_term.(GType (UNamed q)) in + let q = Glob_term.(GType q) in (* this function has a nice error message for not found univs *) LSet.singleton (Pretyping.interp_known_glob_level ?loc sigma q) in @@ -487,7 +505,7 @@ let dump_global r = let vernac_syntax_extension ~module_local infix l = if infix then Metasyntax.check_infix_modifiers (snd l); - Metasyntax.add_syntax_extension module_local l + Metasyntax.add_syntax_extension ~local:module_local l let vernac_declare_scope ~module_local sc = Metasyntax.declare_scope module_local sc @@ -506,11 +524,13 @@ let vernac_open_close_scope ~section_local (b,s) = let vernac_arguments_scope ~section_local r scl = Notation.declare_arguments_scope section_local (smart_global r) scl -let vernac_infix ~module_local = - Metasyntax.add_infix module_local (Global.env()) +let vernac_infix ~atts = + let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in + Metasyntax.add_infix ~local:module_local deprecation (Global.env()) -let vernac_notation ~module_local = - Metasyntax.add_notation module_local (Global.env()) +let vernac_notation ~atts = + let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in + Metasyntax.add_notation ~local:module_local deprecation (Global.env()) let vernac_custom_entry ~module_local s = Metasyntax.declare_custom_entry module_local s @@ -540,7 +560,7 @@ let () = (***********) (* Gallina *) -let start_proof_and_print ~program_mode ~pstate ?hook k l = +let start_proof_and_print ~program_mode ?hook k l = let inference_hook = if program_mode then let hook env sigma ev = @@ -562,82 +582,97 @@ let start_proof_and_print ~program_mode ~pstate ?hook k l = in Some hook else None in - start_proof_com ~program_mode ~ontop:pstate ?inference_hook ?hook k l + start_lemma_com ~program_mode ?inference_hook ?hook k l let vernac_definition_hook p = function | Coercion -> Some (Class.add_coercion_hook p) | CanonicalStructure -> - Some (Lemmas.mk_hook (fun _ _ _ -> Canonical.declare_canonical_structure)) + Some (DeclareDef.Hook.make (fun _ _ _ -> Canonical.declare_canonical_structure)) | SubClass -> Some (Class.add_subclass_hook p) | _ -> None -let vernac_definition ~atts ~pstate discharge kind ({loc;v=id}, pl) def = +let fresh_name_for_anonymous_theorem () = + Namegen.next_global_ident_away Lemmas.default_thm_id Id.Set.empty + +let vernac_definition_name lid local = + let lid = + match lid with + | { v = Name.Anonymous; loc } -> + CAst.make ?loc (fresh_name_for_anonymous_theorem ()) + | { v = Name.Name n; loc } -> CAst.make ?loc n in + let () = + match local with + | Discharge -> Dumpglob.dump_definition lid true "var" + | Global _ -> Dumpglob.dump_definition lid false "def" + in + lid + +let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t = let open DefAttributes in let local = enforce_locality_exp atts.locality discharge in let hook = vernac_definition_hook atts.polymorphic kind in - let () = - match id with - | Anonymous -> () - | Name n -> let lid = CAst.make ?loc n in - match local with - | Discharge -> Dumpglob.dump_definition lid true "var" - | Local | Global -> Dumpglob.dump_definition lid false "def" - in let program_mode = atts.program in - let name = - match id with - | Anonymous -> fresh_name_for_anonymous_theorem ~pstate - | Name n -> n - in - (match def with - | ProveBody (bl,t) -> (* local binders, typ *) - Some (start_proof_and_print ~program_mode ~pstate (local, atts.polymorphic, DefinitionBody kind) - ?hook [(CAst.make ?loc name, pl), (bl, t)]) - | DefineBody (bl,red_option,c,typ_opt) -> - let red_option = match red_option with - | None -> None - | Some r -> - let sigma, env = get_current_or_global_context ~pstate in - Some (snd (Hook.get f_interp_redexp env sigma r)) in - ComDefinition.do_definition ~program_mode name - (local, atts.polymorphic, kind) pl bl red_option c typ_opt ?hook; - pstate - ) - -let vernac_start_proof ~atts ~pstate kind l = + let name = vernac_definition_name lid local in + start_proof_and_print ~program_mode (local, atts.polymorphic, DefinitionBody kind) ?hook [(name, pl), (bl, t)] + +let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt = + let open DefAttributes in + let local = enforce_locality_exp atts.locality discharge in + let hook = vernac_definition_hook atts.polymorphic kind in + let program_mode = atts.program in + let name = vernac_definition_name lid local in + let red_option = match red_option with + | None -> None + | Some r -> + let env = Global.env () in + let sigma = Evd.from_env env in + Some (snd (Hook.get f_interp_redexp env sigma r)) in + ComDefinition.do_definition ~program_mode name.v + (local, atts.polymorphic, kind) pl bl red_option c typ_opt ?hook + +(* NB: pstate argument to use combinators easily *) +let vernac_start_proof ~atts kind l = let open DefAttributes in let local = enforce_locality_exp atts.locality NoDischarge in if Dumpglob.dump () then List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l; - Some (start_proof_and_print ~pstate ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l) + start_proof_and_print ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l -let vernac_end_proof ?pstate ?proof = function +let vernac_end_proof ?stack ?proof = let open Vernacexpr in function | Admitted -> - vernac_require_open_proof ~pstate (save_proof_admitted ?proof); - pstate + vernac_require_open_lemma ~stack (fun ~stack -> + let lemma, stack = Stack.pop stack in + save_lemma_admitted ?proof ~lemma; + stack) | Proved (opaque,idopt) -> - save_proof_proved ?pstate ?proof ~opaque ~idopt + let lemma, stack = match stack with + | None -> None, None + | Some stack -> + let lemma, stack = Stack.pop stack in + Some lemma, stack + in + save_lemma_proved ?lemma ?proof ~opaque ~idopt; + stack -let vernac_exact_proof ~pstate c = +let vernac_exact_proof ~lemma c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the beginning of a proof. *) - let pstate, status = Pfedit.by (Tactics.exact_proof c) pstate in - let pstate = save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Opaque ~idopt:None in - if not status then Feedback.feedback Feedback.AddedAxiom; - pstate + let lemma, status = Lemmas.by (Tactics.exact_proof c) lemma in + let () = save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Opaque ~idopt:None in + if not status then Feedback.feedback Feedback.AddedAxiom let vernac_assumption ~atts discharge kind l nl = let open DefAttributes in let local = enforce_locality_exp atts.locality discharge in - let global = local == Global in let kind = local, atts.polymorphic, kind in List.iter (fun (is_coe,(idl,c)) -> if Dumpglob.dump () then List.iter (fun (lid, _) -> - if global then Dumpglob.dump_definition lid false "ax" - else Dumpglob.dump_definition lid true "var") idl) l; + match local with + | Global _ -> Dumpglob.dump_definition lid false "ax" + | Discharge -> Dumpglob.dump_definition lid true "var") idl) l; let status = ComAssumption.do_assumptions ~program_mode:atts.program kind nl l in if not status then Feedback.feedback Feedback.AddedAxiom @@ -804,30 +839,46 @@ let vernac_inductive ~atts cum lo finite indl = in vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]] *) -let vernac_fixpoint ~atts ~pstate discharge l : Proof_global.t option = - let open DefAttributes in - let local = enforce_locality_exp atts.locality discharge in +let vernac_fixpoint_common ~atts discharge l = if Dumpglob.dump () then List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; - (* XXX: Switch to the attribute system and match on ~atts *) - let do_fixpoint = if atts.program then - fun local sign l -> ComProgramFixpoint.do_fixpoint local sign l; None - else - ComFixpoint.do_fixpoint ~ontop:pstate - in - do_fixpoint local atts.polymorphic l + enforce_locality_exp atts.DefAttributes.locality discharge -let vernac_cofixpoint ~atts ~pstate discharge l = +let vernac_fixpoint_interactive ~atts discharge l = let open DefAttributes in - let local = enforce_locality_exp atts.locality discharge in + let local = vernac_fixpoint_common ~atts discharge l in + if atts.program then + CErrors.user_err Pp.(str"Program Fixpoint requires a body"); + ComFixpoint.do_fixpoint_interactive local atts.polymorphic l + +let vernac_fixpoint ~atts discharge l = + let open DefAttributes in + let local = vernac_fixpoint_common ~atts discharge l in + if atts.program then + (* XXX: Switch to the attribute system and match on ~atts *) + ComProgramFixpoint.do_fixpoint local atts.polymorphic l + else + ComFixpoint.do_fixpoint local atts.polymorphic l + +let vernac_cofixpoint_common ~atts discharge l = if Dumpglob.dump () then List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; - let do_cofixpoint = if atts.program then - fun local sign l -> ComProgramFixpoint.do_cofixpoint local sign l; None - else - ComFixpoint.do_cofixpoint ~ontop:pstate - in - do_cofixpoint local atts.polymorphic l + enforce_locality_exp atts.DefAttributes.locality discharge + +let vernac_cofixpoint_interactive ~atts discharge l = + let open DefAttributes in + let local = vernac_cofixpoint_common ~atts discharge l in + if atts.program then + CErrors.user_err Pp.(str"Program CoFixpoint requires a body"); + ComFixpoint.do_cofixpoint_interactive local atts.polymorphic l + +let vernac_cofixpoint ~atts discharge l = + let open DefAttributes in + let local = vernac_cofixpoint_common ~atts discharge l in + if atts.program then + ComProgramFixpoint.do_cofixpoint local atts.polymorphic l + else + ComFixpoint.do_cofixpoint local atts.polymorphic l let vernac_scheme l = if Dumpglob.dump () then @@ -883,14 +934,13 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast = Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared"); Option.iter (fun export -> vernac_import export [qualid_of_ident id]) export -let vernac_define_module ~pstate export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l = +let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l = (* We check the state of the system (in section, in module type) and what module information is supplied *) if Lib.sections_are_opened () then user_err Pp.(str "Modules and Module Types are not allowed inside sections."); match mexpr_ast_l with | [] -> - check_no_pending_proof ~pstate; let binders_ast,argsexport = List.fold_right (fun (export,idl,ty) (args,argsexport) -> @@ -930,13 +980,12 @@ let vernac_end_module export {loc;v=id} = Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined"); Option.iter (fun export -> vernac_import export [qualid_of_ident ?loc id]) export -let vernac_declare_module_type ~pstate {loc;v=id} binders_ast mty_sign mty_ast_l = +let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l = if Lib.sections_are_opened () then user_err Pp.(str "Modules and Module Types are not allowed inside sections."); match mty_ast_l with | [] -> - check_no_pending_proof ~pstate; let binders_ast,argsexport = List.fold_right (fun (export,idl,ty) (args,argsexport) -> @@ -983,8 +1032,7 @@ let vernac_include l = (* Sections *) -let vernac_begin_section ~pstate ({v=id} as lid) = - check_no_pending_proof ~pstate; +let vernac_begin_section ({v=id} as lid) = Dumpglob.dump_definition lid true "sec"; Lib.open_section id @@ -997,8 +1045,7 @@ let vernac_name_sec_hyp {v=id} set = Proof_using.name_set id set (* Dispatcher of the "End" command *) -let vernac_end_segment ~pstate ({v=id} as lid) = - check_no_pending_proof ~pstate; +let vernac_end_segment ({v=id} as lid) = match Lib.find_opening_node id with | Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid | Lib.OpenedModule (true,_,_,_) -> vernac_end_modtype lid @@ -1058,18 +1105,42 @@ let vernac_identity_coercion ~atts id qids qidt = (* Type classes *) -let vernac_instance ~atts name bl t props pri = - let open DefAttributes in - let global = not (make_section_locality atts.locality) in +let vernac_instance_program ~atts name bl t props info = Dumpglob.dump_constraint (fst name) false "inst"; - let program_mode = atts.program in - Classes.new_instance ~program_mode ~global atts.polymorphic name bl t props pri + let (program, locality), polymorphic = + Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts + in + let global = not (make_section_locality locality) in + let _id : Id.t = Classes.new_instance_program ~global polymorphic name bl t props info in + () + +let vernac_instance_interactive ~atts name bl t info = + Dumpglob.dump_constraint (fst name) false "inst"; + let (program, locality), polymorphic = + Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts + in + let global = not (make_section_locality locality) in + let _id, pstate = + Classes.new_instance_interactive ~global polymorphic name bl t info in + pstate + +let vernac_instance ~atts name bl t props info = + Dumpglob.dump_constraint (fst name) false "inst"; + let (program, locality), polymorphic = + Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts + in + let global = not (make_section_locality locality) in + let _id : Id.t = + Classes.new_instance ~global polymorphic name bl t props info in + () let vernac_declare_instance ~atts id bl inst pri = - let open DefAttributes in - let global = not (make_section_locality atts.locality) in Dumpglob.dump_definition (fst id) false "inst"; - Classes.declare_new_instance ~program_mode:atts.program ~global atts.polymorphic id bl inst pri + let (program, locality), polymorphic = + Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts + in + let global = not (make_section_locality locality) in + Classes.declare_new_instance ~program_mode:program ~global polymorphic id bl inst pri let vernac_context ~poly l = if not (ComAssumption.context poly l) then Feedback.feedback Feedback.AddedAxiom @@ -1094,7 +1165,7 @@ let focus_command_cond = Proof.no_cond command_focus all tactics fail if there are no further goals to prove. *) let vernac_solve_existential ~pstate n com = - Proof_global.simple_with_current_proof (fun _ p -> + Proof_global.map_proof (fun p -> let intern env sigma = Constrintern.intern_constr env sigma com in Proof.V82.instantiate_evar (Global.env ()) n intern p) pstate @@ -1104,23 +1175,20 @@ let vernac_set_end_tac ~pstate tac = (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*) Proof_global.set_endline_tactic tac pstate -let vernac_set_used_variables ~(pstate : Proof_global.t) e : Proof_global.t = +let vernac_set_used_variables ~pstate e : Proof_global.t = let env = Global.env () in let initial_goals pf = Proofview.initial_goals Proof.(data pf).Proof.entry in - let tys = - List.map snd (initial_goals (Proof_global.give_me_the_proof pstate)) in + let tys = List.map snd (initial_goals (Proof_global.get_proof pstate)) in let tys = List.map EConstr.Unsafe.to_constr tys in let l = Proof_using.process_expr env e tys in let vars = Environ.named_context env in - List.iter (fun id -> + List.iter (fun id -> if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then user_err ~hdr:"vernac_set_used_variables" (str "Unknown variable: " ++ Id.print id)) l; let _, pstate = Proof_global.set_used_variables pstate l in - fst @@ Proof_global.with_current_proof begin fun _ p -> - (p, ()) - end pstate + pstate (*****************************) (* Auxiliary file management *) @@ -1200,9 +1268,10 @@ let vernac_hints ~atts dbnames h = let local = enforce_module_locality local in Hints.add_hints ~local dbnames (Hints.interp_hints poly h) -let vernac_syntactic_definition ~module_local lid x y = +let vernac_syntactic_definition ~atts lid x compat = + let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in Dumpglob.dump_definition lid false "syndef"; - Metasyntax.add_syntactic_definition (Global.env()) lid.v x module_local y + Metasyntax.add_syntactic_definition ~local:module_local deprecation (Global.env()) lid.v x compat let cache_bidi_hints (_name, (gr, ohint)) = match ohint with @@ -1817,10 +1886,10 @@ let get_current_context_of_args ~pstate = match pstate with | None -> fun _ -> let env = Global.env () in Evd.(from_env env, env) - | Some pstate -> + | Some lemma -> function - | Some n -> Pfedit.get_goal_context pstate n - | None -> Pfedit.get_current_context pstate + | Some n -> Pfedit.get_goal_context lemma n + | None -> Pfedit.get_current_context lemma let query_command_selector ?loc = function | None -> None @@ -1885,7 +1954,7 @@ let vernac_global_check c = let get_nth_goal ~pstate n = - let pf = Proof_global.give_me_the_proof pstate in + let pf = Proof_global.get_proof pstate in let Proof.{goals;sigma} = Proof.data pf in let gl = {Evd.it=List.nth goals (n-1) ; sigma = sigma; } in gl @@ -1928,7 +1997,7 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt = let sigma, env = get_current_or_global_context ~pstate in print_about env sigma ref_or_by_not udecl -let vernac_print ~(pstate : Proof_global.t option) ~atts = +let vernac_print ~pstate ~atts = let sigma, env = get_current_or_global_context ~pstate in function | PrintTables -> print_tables () @@ -1961,9 +2030,9 @@ let vernac_print ~(pstate : Proof_global.t option) ~atts = | PrintHintGoal -> begin match pstate with | Some pstate -> - Hints.pr_applicable_hint pstate + Hints.pr_applicable_hint pstate | None -> - str "No proof in progress" + str "No proof in progress" end | PrintHintDbName s -> Hints.pr_hint_db_by_name env sigma s | PrintHintDb -> Hints.pr_searchtable env sigma @@ -2085,10 +2154,8 @@ let vernac_locate ~pstate = function | LocateOther (s, qid) -> print_located_other s qid | LocateFile f -> locate_file f -let vernac_register ~pstate qid r = +let vernac_register qid r = let gr = Smartlocate.global_with_alias qid in - if there_are_pending_proofs ~pstate then - user_err Pp.(str "Cannot register a primitive while in proof editing mode."); match r with | RegisterInline -> begin match gr with @@ -2116,85 +2183,89 @@ let vernac_register ~pstate qid r = (********************) (* Proof management *) -let vernac_focus gln = - Proof_global.simple_with_current_proof (fun _ p -> +let vernac_focus ~pstate gln = + Proof_global.map_proof (fun p -> match gln with | None -> Proof.focus focus_command_cond () 1 p | Some 0 -> user_err Pp.(str "Invalid goal number: 0. Goal numbering starts with 1.") | Some n -> Proof.focus focus_command_cond () n p) + pstate (* Unfocuses one step in the focus stack. *) -let vernac_unfocus () = - Proof_global.simple_with_current_proof - (fun _ p -> Proof.unfocus command_focus p ()) +let vernac_unfocus ~pstate = + Proof_global.map_proof + (fun p -> Proof.unfocus command_focus p ()) + pstate (* Checks that a proof is fully unfocused. Raises an error if not. *) let vernac_unfocused ~pstate = - let p = Proof_global.give_me_the_proof pstate in + let p = Proof_global.get_proof pstate in if Proof.unfocused p then str"The proof is indeed fully unfocused." else user_err Pp.(str "The proof is not fully unfocused.") - (* "{" focuses on the first goal, "n: {" focuses on the n-th goal "}" unfocuses, provided that the proof of the goal has been completed. *) let subproof_kind = Proof.new_focus_kind () let subproof_cond = Proof.done_cond subproof_kind -let vernac_subproof gln = - Proof_global.simple_with_current_proof (fun _ p -> +let vernac_subproof gln ~pstate = + Proof_global.map_proof (fun p -> match gln with | None -> Proof.focus subproof_cond () 1 p | Some (Goal_select.SelectNth n) -> Proof.focus subproof_cond () n p | Some (Goal_select.SelectId id) -> Proof.focus_id subproof_cond () id p | _ -> user_err ~hdr:"bracket_selector" (str "Brackets do not support multi-goal selectors.")) + pstate -let vernac_end_subproof () = - Proof_global.simple_with_current_proof (fun _ p -> - Proof.unfocus subproof_kind p ()) +let vernac_end_subproof ~pstate = + Proof_global.map_proof (fun p -> + Proof.unfocus subproof_kind p ()) + pstate -let vernac_bullet (bullet : Proof_bullet.t) = - Proof_global.simple_with_current_proof (fun _ p -> - Proof_bullet.put p bullet) +let vernac_bullet (bullet : Proof_bullet.t) ~pstate = + Proof_global.map_proof (fun p -> + Proof_bullet.put p bullet) pstate +(* Stack is needed due to show proof names, should deprecate / remove + and take pstate *) let vernac_show ~pstate = match pstate with (* Show functions that don't require a proof state *) | None -> begin function - | ShowProof -> show_proof ~pstate + | ShowProof -> show_proof ~pstate:None | ShowMatch id -> show_match id - | ShowScript -> assert false (* Only the stm knows the script *) | _ -> user_err (str "This command requires an open proof.") end (* Show functions that require a proof state *) | Some pstate -> + let proof = Proof_global.get_proof pstate in begin function | ShowGoal goalref -> - let proof = Proof_global.give_me_the_proof pstate in begin match goalref with | OpenSubgoals -> pr_open_subgoals ~proof | NthGoal n -> pr_nth_open_subgoal ~proof n | GoalId id -> pr_goal_by_id ~proof id end - | ShowExistentials -> show_top_evars ~pstate - | ShowUniverses -> show_universes ~pstate + | ShowExistentials -> show_top_evars ~proof + | ShowUniverses -> show_universes ~proof + (* Deprecate *) | ShowProofNames -> - pr_sequence Id.print (Proof_global.get_all_proof_names pstate) - | ShowIntros all -> show_intro ~pstate all + Id.print (Proof_global.get_proof_name pstate) + | ShowIntros all -> show_intro ~proof all | ShowProof -> show_proof ~pstate:(Some pstate) | ShowMatch id -> show_match id - | ShowScript -> assert false (* Only the stm knows the script *) end let vernac_check_guard ~pstate = - let pts = Proof_global.give_me_the_proof pstate in + let pts = Proof_global.get_proof pstate in let pfterm = List.hd (Proof.partial_proof pts) in let message = try @@ -2205,26 +2276,6 @@ let vernac_check_guard ~pstate = (str ("Condition violated: ") ++s) in message -(* Attributes *) -let with_locality ~atts f = - let local = Attributes.(parse locality atts) in - f ~local - -let with_section_locality ~atts f = - let local = Attributes.(parse locality atts) in - let section_local = make_section_locality local in - f ~section_local - -let with_module_locality ~atts f = - let local = Attributes.(parse locality atts) in - let module_local = make_module_locality local in - f ~module_local - -let with_def_attributes ~atts f = - let atts = DefAttributes.parse atts in - if atts.DefAttributes.program then Obligations.check_program_libraries (); - f ~atts - (** A global default timeout, controlled by option "Set Default Timeout n". Use "Unset Default Timeout" to deactivate it (or set it to 0). *) @@ -2257,8 +2308,7 @@ let with_fail ~st f = | HasNotFailed as e -> raise e | e when CErrors.noncritical e || e = Timeout -> let e = CErrors.push e in - raise (HasFailed (CErrors.iprint - (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e))) + raise (HasFailed (CErrors.iprint (ExplainErr.process_vernac_interp_error e))) with e when CErrors.noncritical e -> (* Restore the previous state XXX Careful here with the cache! *) Vernacstate.invalidate_cache (); @@ -2279,338 +2329,388 @@ let locate_if_not_already ?loc (e, info) = exception End_of_input -(* "locality" is the prefix "Local" attribute, while the "local" component - * is the outdated/deprecated "Local" attribute of some vernacular commands - * still parsed as the obsolete_locality grammar entry for retrocompatibility. - * loc is the Loc.t of the vernacular command being interpreted. *) -let rec interp_expr ?proof ~atts ~st c : Proof_global.t option = - let pstate = st.Vernacstate.proof in - vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c); +let interp_typed_vernac c ~stack = + let open Vernacextend in match c with - - (* The STM should handle that, but LOAD bypasses the STM... *) - | VernacAbortAll -> CErrors.user_err (str "AbortAll cannot be used through the Load command") - | VernacRestart -> CErrors.user_err (str "Restart cannot be used through the Load command") - | VernacUndo _ -> CErrors.user_err (str "Undo cannot be used through the Load command") - | VernacUndoTo _ -> CErrors.user_err (str "UndoTo cannot be used through the Load command") - - (* Resetting *) - | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm.") - | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm.") - | VernacBack _ -> anomaly (str "VernacBack not handled by Stm.") - | VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm.") - - (* This one is possible to handle here *) - | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command") - - (* Loading a file requires access to the control interpreter so - [vernac_load] is mutually-recursive with [interp_expr] *) - | VernacLoad (verbosely,fname) -> - unsupported_attributes atts; - vernac_load ?proof ~verbosely ~st fname - + | VtDefault f -> f (); stack + | VtNoProof f -> + if Option.has_some stack then + user_err Pp.(str "Command not supported (Open proofs remain)"); + let () = f () in + stack + | VtCloseProof f -> + vernac_require_open_lemma ~stack (fun ~stack -> + let lemma, stack = Stack.pop stack in + f ~lemma; + stack) + | VtOpenProof f -> + Some (Stack.push stack (f ())) + | VtModifyProof f -> + Option.map (Stack.map_top_pstate ~f:(fun pstate -> f ~pstate)) stack + | VtReadProofOpt f -> + let pstate = Option.map (Stack.with_top_pstate ~f:(fun x -> x)) stack in + f ~pstate; + stack + | VtReadProof f -> + with_pstate ~stack f; + stack + +(* We interpret vernacular commands to a DSL that specifies their + allowed actions on proof states *) +let translate_vernac ~atts v = let open Vernacextend in match v with + | VernacEndProof _ + | VernacAbortAll + | VernacRestart + | VernacUndo _ + | VernacUndoTo _ + | VernacResetName _ + | VernacResetInitial + | VernacBack _ + | VernacBackTo _ + | VernacAbort _ + | VernacLoad _ -> + anomaly (str "type_vernac") (* Syntax *) | VernacSyntaxExtension (infix, sl) -> - with_module_locality ~atts vernac_syntax_extension infix sl; - pstate + VtDefault(fun () -> with_module_locality ~atts vernac_syntax_extension infix sl) | VernacDeclareScope sc -> - with_module_locality ~atts vernac_declare_scope sc; - pstate + VtDefault(fun () -> with_module_locality ~atts vernac_declare_scope sc) | VernacDelimiters (sc,lr) -> - with_module_locality ~atts vernac_delimiters sc lr; - pstate + VtDefault(fun () -> with_module_locality ~atts vernac_delimiters sc lr) | VernacBindScope (sc,rl) -> - with_module_locality ~atts vernac_bind_scope sc rl; - pstate + VtDefault(fun () -> with_module_locality ~atts vernac_bind_scope sc rl) | VernacOpenCloseScope (b, s) -> - with_section_locality ~atts vernac_open_close_scope (b,s); - pstate + VtDefault(fun () -> with_section_locality ~atts vernac_open_close_scope (b,s)) | VernacInfix (mv,qid,sc) -> - with_module_locality ~atts vernac_infix mv qid sc; - pstate + VtDefault(fun () -> vernac_infix ~atts mv qid sc) | VernacNotation (c,infpl,sc) -> - with_module_locality ~atts vernac_notation c infpl sc; - pstate + VtDefault(fun () -> vernac_notation ~atts c infpl sc) | VernacNotationAddFormat(n,k,v) -> - unsupported_attributes atts; - Metasyntax.add_notation_extra_printing_rule n k v; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + Metasyntax.add_notation_extra_printing_rule n k v) | VernacDeclareCustomEntry s -> - with_module_locality ~atts vernac_custom_entry s; - pstate + VtDefault(fun () -> with_module_locality ~atts vernac_custom_entry s) (* Gallina *) - | VernacDefinition ((discharge,kind),lid,d) -> - with_def_attributes ~atts vernac_definition ~pstate discharge kind lid d + + | VernacDefinition (discharge,lid,DefineBody (bl,red_option,c,typ)) -> + VtDefault (fun () -> + with_def_attributes ~atts + vernac_definition discharge lid bl red_option c typ) + | VernacDefinition (discharge,lid,ProveBody(bl,typ)) -> + VtOpenProof(fun () -> + with_def_attributes ~atts + vernac_definition_interactive discharge lid bl typ) + | VernacStartTheoremProof (k,l) -> - with_def_attributes ~atts vernac_start_proof ~pstate k l - | VernacEndProof e -> - unsupported_attributes atts; - vernac_end_proof ?proof ?pstate e + VtOpenProof(fun () -> with_def_attributes ~atts vernac_start_proof k l) | VernacExactProof c -> - unsupported_attributes atts; - vernac_require_open_proof ~pstate (vernac_exact_proof c) + VtCloseProof (fun ~lemma -> + unsupported_attributes atts; + vernac_exact_proof ~lemma c) + + | VernacDefineModule (export,lid,bl,mtys,mexprl) -> + let i () = + unsupported_attributes atts; + vernac_define_module export lid bl mtys mexprl in + (* XXX: We should investigate if eventually this should be made + VtNoProof in all cases. *) + if List.is_empty mexprl then VtNoProof i else VtDefault i + + | VernacDeclareModuleType (lid,bl,mtys,mtyo) -> + VtNoProof(fun () -> + unsupported_attributes atts; + vernac_declare_module_type lid bl mtys mtyo) | VernacAssumption ((discharge,kind),nl,l) -> - with_def_attributes ~atts vernac_assumption discharge kind l nl; - pstate + VtDefault(fun () -> with_def_attributes ~atts vernac_assumption discharge kind l nl) | VernacInductive (cum, priv, finite, l) -> - vernac_inductive ~atts cum priv finite l; - pstate + VtDefault(fun () -> vernac_inductive ~atts cum priv finite l) | VernacFixpoint (discharge, l) -> - with_def_attributes ~atts vernac_fixpoint ~pstate discharge l + let opens = List.exists (fun ((_,_,_,_,p),_) -> Option.is_empty p) l in + if opens then + VtOpenProof (fun () -> + with_def_attributes ~atts vernac_fixpoint_interactive discharge l) + else + VtDefault (fun () -> + with_def_attributes ~atts vernac_fixpoint discharge l) | VernacCoFixpoint (discharge, l) -> - with_def_attributes ~atts vernac_cofixpoint ~pstate discharge l + let opens = List.exists (fun ((_,_,_,p),_) -> Option.is_empty p) l in + if opens then + VtOpenProof(fun () -> with_def_attributes ~atts vernac_cofixpoint_interactive discharge l) + else + VtDefault(fun () -> with_def_attributes ~atts vernac_cofixpoint discharge l) + | VernacScheme l -> - unsupported_attributes atts; - vernac_scheme l; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_scheme l) | VernacCombinedScheme (id, l) -> - unsupported_attributes atts; - vernac_combined_scheme id l; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_combined_scheme id l) | VernacUniverse l -> - vernac_universe ~poly:(only_polymorphism atts) l; - pstate + VtDefault(fun () -> vernac_universe ~poly:(only_polymorphism atts) l) | VernacConstraint l -> - vernac_constraint ~poly:(only_polymorphism atts) l; - pstate + VtDefault(fun () -> vernac_constraint ~poly:(only_polymorphism atts) l) (* Modules *) | VernacDeclareModule (export,lid,bl,mtyo) -> - unsupported_attributes atts; - vernac_declare_module export lid bl mtyo; - pstate - | VernacDefineModule (export,lid,bl,mtys,mexprl) -> - unsupported_attributes atts; - vernac_define_module ~pstate export lid bl mtys mexprl; - pstate - | VernacDeclareModuleType (lid,bl,mtys,mtyo) -> - unsupported_attributes atts; - vernac_declare_module_type ~pstate lid bl mtys mtyo; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_declare_module export lid bl mtyo) | VernacInclude in_asts -> - unsupported_attributes atts; - vernac_include in_asts; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_include in_asts) (* Gallina extensions *) | VernacBeginSection lid -> - unsupported_attributes atts; - vernac_begin_section ~pstate lid; - pstate - + VtNoProof(fun () -> + unsupported_attributes atts; + vernac_begin_section lid) | VernacEndSegment lid -> - unsupported_attributes atts; - vernac_end_segment ~pstate lid; - pstate - + VtNoProof(fun () -> + unsupported_attributes atts; + vernac_end_segment lid) | VernacNameSectionHypSet (lid, set) -> - unsupported_attributes atts; - vernac_name_sec_hyp lid set; - pstate - + VtDefault(fun () -> + unsupported_attributes atts; + vernac_name_sec_hyp lid set) | VernacRequire (from, export, qidl) -> - unsupported_attributes atts; - vernac_require from export qidl; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_require from export qidl) | VernacImport (export,qidl) -> - unsupported_attributes atts; - vernac_import export qidl; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_import export qidl) | VernacCanonical qid -> - unsupported_attributes atts; - vernac_canonical qid; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_canonical qid) | VernacCoercion (r,s,t) -> - vernac_coercion ~atts r s t; - pstate + VtDefault(fun () -> vernac_coercion ~atts r s t) | VernacIdentityCoercion ({v=id},s,t) -> - vernac_identity_coercion ~atts id s t; - pstate + VtDefault(fun () -> vernac_identity_coercion ~atts id s t) (* Type classes *) | VernacInstance (name, bl, t, props, info) -> - snd @@ with_def_attributes ~atts (vernac_instance ~pstate name bl t props info) + let { DefAttributes.program } = DefAttributes.parse atts in + if program then + VtDefault (fun () -> vernac_instance_program ~atts name bl t props info) + else begin match props with + | None -> + VtOpenProof(fun () -> + vernac_instance_interactive ~atts name bl t info) + | Some props -> + VtDefault(fun () -> + vernac_instance ~atts name bl t props info) + end + | VernacDeclareInstance (id, bl, inst, info) -> - with_def_attributes ~atts vernac_declare_instance id bl inst info; - pstate + VtDefault(fun () -> vernac_declare_instance ~atts id bl inst info) | VernacContext sup -> - let () = vernac_context ~poly:(only_polymorphism atts) sup in - pstate + VtDefault(fun () -> vernac_context ~poly:(only_polymorphism atts) sup) | VernacExistingInstance insts -> - with_section_locality ~atts vernac_existing_instance insts; - pstate + VtDefault(fun () -> with_section_locality ~atts vernac_existing_instance insts) | VernacExistingClass id -> - unsupported_attributes atts; - vernac_existing_class id; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_existing_class id) (* Solving *) | VernacSolveExistential (n,c) -> - unsupported_attributes atts; - Some (vernac_require_open_proof ~pstate (vernac_solve_existential n c)) - + VtModifyProof(fun ~pstate -> + unsupported_attributes atts; + vernac_solve_existential ~pstate n c) (* Auxiliary file and library management *) | VernacAddLoadPath (isrec,s,alias) -> - unsupported_attributes atts; - vernac_add_loadpath isrec s alias; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_add_loadpath isrec s alias) | VernacRemoveLoadPath s -> - unsupported_attributes atts; - vernac_remove_loadpath s; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_remove_loadpath s) | VernacAddMLPath (isrec,s) -> - unsupported_attributes atts; - vernac_add_ml_path isrec s; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_add_ml_path isrec s) | VernacDeclareMLModule l -> - with_locality ~atts vernac_declare_ml_module l; - pstate + VtDefault(fun () -> with_locality ~atts vernac_declare_ml_module l) | VernacChdir s -> - unsupported_attributes atts; - vernac_chdir s; - pstate + VtDefault(fun () -> unsupported_attributes atts; vernac_chdir s) (* State management *) | VernacWriteState s -> - unsupported_attributes atts; - vernac_write_state s; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_write_state s) | VernacRestoreState s -> - unsupported_attributes atts; - vernac_restore_state s; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_restore_state s) (* Commands *) | VernacCreateHintDb (dbname,b) -> - with_module_locality ~atts vernac_create_hintdb dbname b; - pstate + VtDefault(fun () -> + with_module_locality ~atts vernac_create_hintdb dbname b) | VernacRemoveHints (dbnames,ids) -> - with_module_locality ~atts vernac_remove_hints dbnames ids; - pstate + VtDefault(fun () -> + with_module_locality ~atts vernac_remove_hints dbnames ids) | VernacHints (dbnames,hints) -> - vernac_hints ~atts dbnames hints; - pstate + VtDefault(fun () -> + vernac_hints ~atts dbnames hints) | VernacSyntacticDefinition (id,c,b) -> - with_module_locality ~atts vernac_syntactic_definition id c b; - pstate - | VernacArguments (qid, args, more_implicits, nargs, nargs_before_bidi, flags) -> - with_section_locality ~atts vernac_arguments qid args more_implicits nargs nargs_before_bidi flags; - pstate + VtDefault(fun () -> vernac_syntactic_definition ~atts id c b) + | VernacArguments (qid, args, more_implicits, nargs, bidi, flags) -> + VtDefault(fun () -> + with_section_locality ~atts (vernac_arguments qid args more_implicits nargs bidi flags)) | VernacReserve bl -> - unsupported_attributes atts; - vernac_reserve bl; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_reserve bl) | VernacGeneralizable gen -> - with_locality ~atts vernac_generalizable gen; - pstate + VtDefault(fun () -> with_locality ~atts vernac_generalizable gen) | VernacSetOpacity qidl -> - with_locality ~atts vernac_set_opacity qidl; - pstate + VtDefault(fun () -> with_locality ~atts vernac_set_opacity qidl) | VernacSetStrategy l -> - with_locality ~atts vernac_set_strategy l; - pstate + VtDefault(fun () -> with_locality ~atts vernac_set_strategy l) | VernacSetOption (export, key,v) -> - vernac_set_option ~local:(only_locality atts) export key v; - pstate + VtDefault(fun () -> + vernac_set_option ~local:(only_locality atts) export key v) | VernacRemoveOption (key,v) -> - unsupported_attributes atts; - vernac_remove_option key v; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_remove_option key v) | VernacAddOption (key,v) -> - unsupported_attributes atts; - vernac_add_option key v; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_add_option key v) | VernacMemOption (key,v) -> - unsupported_attributes atts; - vernac_mem_option key v; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_mem_option key v) | VernacPrintOption key -> - unsupported_attributes atts; - vernac_print_option key; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_print_option key) | VernacCheckMayEval (r,g,c) -> - Feedback.msg_notice @@ - vernac_check_may_eval ~pstate ~atts r g c; - pstate + VtReadProofOpt(fun ~pstate -> + Feedback.msg_notice @@ + vernac_check_may_eval ~pstate ~atts r g c) | VernacDeclareReduction (s,r) -> - with_locality ~atts vernac_declare_reduction s r; - pstate + VtDefault(fun () -> + with_locality ~atts vernac_declare_reduction s r) | VernacGlobalCheck c -> - unsupported_attributes atts; - Feedback.msg_notice @@ vernac_global_check c; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + Feedback.msg_notice @@ vernac_global_check c) | VernacPrint p -> - Feedback.msg_notice @@ vernac_print ~pstate ~atts p; - pstate + VtReadProofOpt(fun ~pstate -> + Feedback.msg_notice @@ vernac_print ~pstate ~atts p) | VernacSearch (s,g,r) -> - unsupported_attributes atts; - vernac_search ~pstate ~atts s g r; - pstate + VtReadProofOpt( + unsupported_attributes atts; + vernac_search ~atts s g r) | VernacLocate l -> unsupported_attributes atts; - Feedback.msg_notice @@ vernac_locate ~pstate l; - pstate + VtReadProofOpt(fun ~pstate -> + Feedback.msg_notice @@ vernac_locate ~pstate l) | VernacRegister (qid, r) -> - unsupported_attributes atts; - vernac_register ~pstate qid r; - pstate + VtNoProof(fun () -> + unsupported_attributes atts; + vernac_register qid r) | VernacPrimitive (id, prim, typopt) -> - unsupported_attributes atts; - ComAssumption.do_primitive id prim typopt; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + ComAssumption.do_primitive id prim typopt) | VernacComments l -> - unsupported_attributes atts; - Flags.if_verbose Feedback.msg_info (str "Comments ok\n"); - pstate - + VtDefault(fun () -> + unsupported_attributes atts; + Flags.if_verbose Feedback.msg_info (str "Comments ok\n")) (* Proof management *) | VernacFocus n -> - unsupported_attributes atts; - Option.map (vernac_focus n) pstate + VtModifyProof(unsupported_attributes atts;vernac_focus n) | VernacUnfocus -> - unsupported_attributes atts; - Option.map (vernac_unfocus ()) pstate + VtModifyProof(unsupported_attributes atts;vernac_unfocus) | VernacUnfocused -> - unsupported_attributes atts; - Option.iter (fun pstate -> Feedback.msg_notice @@ vernac_unfocused ~pstate) pstate; - pstate + VtReadProof(fun ~pstate -> + unsupported_attributes atts; + Feedback.msg_notice @@ vernac_unfocused ~pstate) | VernacBullet b -> - unsupported_attributes atts; - Option.map (vernac_bullet b) pstate + VtModifyProof( + unsupported_attributes atts; + vernac_bullet b) | VernacSubproof n -> - unsupported_attributes atts; - Option.map (vernac_subproof n) pstate + VtModifyProof( + unsupported_attributes atts; + vernac_subproof n) | VernacEndSubproof -> - unsupported_attributes atts; - Option.map (vernac_end_subproof ()) pstate + VtModifyProof( + unsupported_attributes atts; + vernac_end_subproof) | VernacShow s -> - unsupported_attributes atts; - Feedback.msg_notice @@ vernac_show ~pstate s; - pstate + VtReadProofOpt(fun ~pstate -> + unsupported_attributes atts; + Feedback.msg_notice @@ vernac_show ~pstate s) | VernacCheckGuard -> - unsupported_attributes atts; - Feedback.msg_notice @@ - vernac_require_open_proof ~pstate (vernac_check_guard); - pstate + VtReadProof(fun ~pstate -> + unsupported_attributes atts; + Feedback.msg_notice @@ vernac_check_guard ~pstate) | VernacProof (tac, using) -> + VtModifyProof(fun ~pstate -> unsupported_attributes atts; let using = Option.append using (Proof_using.get_default_proof_using ()) in let tacs = if Option.is_empty tac then "tac:no" else "tac:yes" in let usings = if Option.is_empty using then "using:no" else "using:yes" in Aux_file.record_in_aux_at "VernacProof" (tacs^" "^usings); - let pstate = - vernac_require_open_proof ~pstate (fun ~pstate -> - let pstate = Option.cata (vernac_set_end_tac ~pstate) pstate tac in - Option.cata (vernac_set_used_variables ~pstate) pstate using) - in Some pstate + let pstate = Option.cata (vernac_set_end_tac ~pstate) pstate tac in + Option.cata (vernac_set_used_variables ~pstate) pstate using) | VernacProofMode mn -> - unsupported_attributes atts; - pstate + VtDefault(fun () -> unsupported_attributes atts) (* Extensions *) | VernacExtend (opn,args) -> - (* XXX: Here we are returning the state! :) *) - let st : Vernacstate.t = Vernacextend.call ~atts opn args ~st in - st.Vernacstate.proof + Vernacextend.type_vernac ~atts opn args + +(* "locality" is the prefix "Local" attribute, while the "local" component + * is the outdated/deprecated "Local" attribute of some vernacular commands + * still parsed as the obsolete_locality grammar entry for retrocompatibility. + * loc is the Loc.t of the vernacular command being interpreted. *) +let rec interp_expr ?proof ~atts ~st c = + let stack = st.Vernacstate.lemmas in + vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c); + match c with + + (* The STM should handle that, but LOAD bypasses the STM... *) + | VernacAbortAll -> CErrors.user_err (str "AbortAll cannot be used through the Load command") + | VernacRestart -> CErrors.user_err (str "Restart cannot be used through the Load command") + | VernacUndo _ -> CErrors.user_err (str "Undo cannot be used through the Load command") + | VernacUndoTo _ -> CErrors.user_err (str "UndoTo cannot be used through the Load command") + + (* Resetting *) + | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm.") + | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm.") + | VernacBack _ -> anomaly (str "VernacBack not handled by Stm.") + | VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm.") + + (* This one is possible to handle here *) + | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command") + + (* Loading a file requires access to the control interpreter so + [vernac_load] is mutually-recursive with [interp_expr] *) + | VernacLoad (verbosely,fname) -> + unsupported_attributes atts; + vernac_load ~verbosely ~st fname + + (* Special: ?proof parameter doesn't allow for uniform pstate pop :S *) + | VernacEndProof e -> + unsupported_attributes atts; + vernac_end_proof ?proof ?stack e + + | v -> + let fv = translate_vernac ~atts v in + interp_typed_vernac ~stack fv (* XXX: This won't properly set the proof mode, as of today, it is controlled by the STM. Thus, we would need access information from @@ -2618,9 +2718,10 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option = the way the proof mode is set there makes the task non trivial without a considerable amount of refactoring. *) -and vernac_load ?proof ~verbosely ~st fname = - let pstate = st.Vernacstate.proof in - if there_are_pending_proofs ~pstate then +and vernac_load ~verbosely ~st fname = + let there_are_pending_proofs ~stack = not Option.(is_empty stack) in + let stack = st.Vernacstate.lemmas in + if there_are_pending_proofs ~stack then CErrors.user_err Pp.(str "Load is not supported inside proofs."); (* Open the file *) let fname = @@ -2637,29 +2738,29 @@ and vernac_load ?proof ~verbosely ~st fname = match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with | Some x -> x | None -> raise End_of_input) in - let rec load_loop ~pstate = + let rec load_loop ~stack = try - let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) pstate in - let pstate = - v_mod (interp_control ?proof ~st:{ st with Vernacstate.proof = pstate }) + let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) stack in + let stack = + v_mod (interp_control ?proof:None ~st:{ st with Vernacstate.lemmas = stack }) (parse_sentence proof_mode input) in - load_loop ~pstate + load_loop ~stack with End_of_input -> - pstate + stack in - let pstate = load_loop ~pstate in + let stack = load_loop ~stack in (* If Load left a proof open, we fail too. *) - if there_are_pending_proofs ~pstate then + if there_are_pending_proofs ~stack then CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs."); - pstate + stack and interp_control ?proof ~st v = match v with | { v=VernacExpr (atts, cmd) } -> interp_expr ?proof ~atts ~st cmd | { v=VernacFail v } -> with_fail ~st (fun () -> interp_control ?proof ~st v); - st.Vernacstate.proof + st.Vernacstate.lemmas | { v=VernacTimeout (timeout,v) } -> vernac_timeout ~timeout (interp_control ?proof ~st) v | { v=VernacRedirect (s, v) } -> @@ -2681,8 +2782,8 @@ let interp ?(verbosely=true) ?proof ~st cmd = Vernacstate.unfreeze_interp_state st; try vernac_timeout (fun st -> let v_mod = if verbosely then Flags.verbosely else Flags.silently in - let pstate = v_mod (interp_control ?proof ~st) cmd in - Vernacstate.Proof_global.set pstate [@ocaml.warning "-3"]; + let ontop = v_mod (interp_control ?proof ~st) cmd in + Vernacstate.Proof_global.set ontop [@ocaml.warning "-3"]; Vernacstate.freeze_interp_state ~marshallable:false ) st with exn -> diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 12451370c8..e46212ca1c 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -22,7 +22,7 @@ val vernac_require : (** The main interpretation function of vernacular expressions *) val interp : ?verbosely:bool -> - ?proof:Proof_global.closed_proof -> + ?proof:(Proof_global.proof_object * Lemmas.proof_info) -> st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t (** Prepare a "match" template for a given inductive type. @@ -41,9 +41,6 @@ val command_focus : unit Proof.focus_kind val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr -> Evd.evar_map * Redexpr.red_expr) Hook.t -(** Helper *) -val vernac_require_open_proof : pstate:Proof_global.t option -> (pstate:Proof_global.t -> 'a) -> 'a - (* Flag set when the test-suite is called. Its only effect to display verbose information for `Fail` *) val test_mode : bool ref diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index df1d08ad0f..6a67a49d0a 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -81,7 +81,6 @@ type locatable = type showable = | ShowGoal of goal_reference | ShowProof - | ShowScript | ShowExistentials | ShowUniverses | ShowProofNames diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 730f5fd6da..2725516a76 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -16,7 +16,11 @@ type vernac_keep_as = VtKeepAxiom | VtKeepDefined | VtKeepOpaque type vernac_qed_type = VtKeep of vernac_keep_as | VtDrop -type vernac_type = +type vernac_when = + | VtNow + | VtLater + +type vernac_classification = (* Start of a proof *) | VtStartProof of vernac_start (* Command altering the global state, bad for parallel @@ -37,7 +41,7 @@ type vernac_type = (* To be removed *) | VtMeta and vernac_start = opacity_guarantee * Names.Id.t list -and vernac_sideff_type = Names.Id.t list +and vernac_sideff_type = Names.Id.t list * vernac_when and opacity_guarantee = | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) @@ -48,19 +52,24 @@ and anon_abstracting_tac = bool (** abstracting anonymously its result *) and proof_block_name = string (** open type of delimiters *) -type vernac_when = - | VtNow - | VtLater -type vernac_classification = vernac_type * vernac_when +type typed_vernac = + | VtDefault of (unit -> unit) + + | VtNoProof of (unit -> unit) + | VtCloseProof of (lemma:Lemmas.t -> unit) + | VtOpenProof of (unit -> Lemmas.t) + | VtModifyProof of (pstate:Proof_global.t -> Proof_global.t) + | VtReadProofOpt of (pstate:Proof_global.t option -> unit) + | VtReadProof of (pstate:Proof_global.t -> unit) -type 'a vernac_command = 'a -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t +type vernac_command = atts:Attributes.vernac_flags -> typed_vernac type plugin_args = Genarg.raw_generic_argument list (* Table of vernac entries *) let vernac_tab = (Hashtbl.create 211 : - (Vernacexpr.extend_name, bool * plugin_args vernac_command) Hashtbl.t) + (Vernacexpr.extend_name, bool * (plugin_args -> vernac_command)) Hashtbl.t) let vinterp_add depr s f = try @@ -83,7 +92,7 @@ let warn_deprecated_command = (* Interpretation of a vernac command *) -let call opn converted_args ~atts ~st = +let type_vernac opn converted_args ~atts = let phase = ref "Looking up command" in try let depr, callback = vinterp_map opn in @@ -99,7 +108,7 @@ let call opn converted_args ~atts ~st = phase := "Checking arguments"; let hunk = callback converted_args in phase := "Executing command"; - hunk ~atts ~st + hunk ~atts with | reraise -> let reraise = CErrors.push reraise in @@ -120,12 +129,12 @@ let get_vernac_classifier (name, i) args = let declare_vernac_classifier name f = classifiers := String.Map.add name f !classifiers -let classify_as_query = VtQuery, VtLater -let classify_as_sideeff = VtSideff [], VtLater -let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater +let classify_as_query = VtQuery +let classify_as_sideeff = VtSideff ([], VtLater) +let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None} type (_, _) ty_sig = -| TyNil : (atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, vernac_classification) ty_sig +| TyNil : (vernac_command, vernac_classification) ty_sig | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig | TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig @@ -151,7 +160,7 @@ let rec untype_classifier : type r s. (r, s) ty_sig -> s -> classifier = functio end (** Stupid GADTs forces us to duplicate the definition just for typing *) -let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args vernac_command = function +let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args -> vernac_command = function | TyNil -> fun f args -> begin match args with | [] -> f diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index b37e527f47..3df74e5f2c 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -32,7 +32,11 @@ type vernac_keep_as = VtKeepAxiom | VtKeepDefined | VtKeepOpaque type vernac_qed_type = VtKeep of vernac_keep_as | VtDrop -type vernac_type = +type vernac_when = + | VtNow + | VtLater + +type vernac_classification = (* Start of a proof *) | VtStartProof of vernac_start (* Command altering the global state, bad for parallel @@ -53,7 +57,7 @@ type vernac_type = (* To be removed *) | VtMeta and vernac_start = opacity_guarantee * Names.Id.t list -and vernac_sideff_type = Names.Id.t list +and vernac_sideff_type = Names.Id.t list * vernac_when and opacity_guarantee = | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) @@ -64,25 +68,29 @@ and anon_abstracting_tac = bool (** abstracting anonymously its result *) and proof_block_name = string (** open type of delimiters *) -type vernac_when = - | VtNow - | VtLater -type vernac_classification = vernac_type * vernac_when - (** Interpretation of extended vernac phrases. *) -type 'a vernac_command = 'a -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t +type typed_vernac = + | VtDefault of (unit -> unit) + | VtNoProof of (unit -> unit) + | VtCloseProof of (lemma:Lemmas.t -> unit) + | VtOpenProof of (unit -> Lemmas.t) + | VtModifyProof of (pstate:Proof_global.t -> Proof_global.t) + | VtReadProofOpt of (pstate:Proof_global.t option -> unit) + | VtReadProof of (pstate:Proof_global.t -> unit) + +type vernac_command = atts:Attributes.vernac_flags -> typed_vernac type plugin_args = Genarg.raw_generic_argument list -val call : Vernacexpr.extend_name -> plugin_args -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t +val type_vernac : Vernacexpr.extend_name -> plugin_args -> vernac_command (** {5 VERNAC EXTEND} *) type classifier = Genarg.raw_generic_argument list -> vernac_classification type (_, _) ty_sig = -| TyNil : (atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, vernac_classification) ty_sig +| TyNil : (vernac_command, vernac_classification) ty_sig | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig | TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml index b3490c7dc6..1dd8164ebc 100644 --- a/vernac/vernacprop.ml +++ b/vernac/vernacprop.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/vernacprop.mli b/vernac/vernacprop.mli index 8296a039f9..8875b86d94 100644 --- a/vernac/vernacprop.mli +++ b/vernac/vernacprop.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 77f54361da..2bc20a747d 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -30,16 +30,16 @@ end type t = { parsing : Parser.state; system : States.state; (* summary + libstack *) - proof : Proof_global.t option; (* proof state *) + lemmas : Lemmas.Stack.t option; (* proofs of lemmas currently opened *) shallow : bool (* is the state trimmed down (libstack) *) } let s_cache = ref None -let s_proof = ref None +let s_lemmas = ref None let invalidate_cache () = s_cache := None; - s_proof := None + s_lemmas := None let update_cache rf v = rf := Some v; v @@ -55,14 +55,14 @@ let do_if_not_cached rf f v = let freeze_interp_state ~marshallable = { system = update_cache s_cache (States.freeze ~marshallable); - proof = !s_proof; + lemmas = !s_lemmas; shallow = false; parsing = Parser.cur_state (); } -let unfreeze_interp_state { system; proof; parsing } = +let unfreeze_interp_state { system; lemmas; parsing } = do_if_not_cached s_cache States.unfreeze system; - s_proof := proof; + s_lemmas := lemmas; Pcoq.unfreeze parsing let make_shallow st = @@ -75,11 +75,16 @@ let make_shallow st = (* Compatibility module *) module Proof_global = struct - let get () = !s_proof - let set x = s_proof := x + type t = Lemmas.Stack.t + + let get () = !s_lemmas + let set x = s_lemmas := x + + let get_pstate () = + Option.map (Lemmas.Stack.with_top ~f:(Lemmas.pf_fold (fun x -> x))) !s_lemmas let freeze ~marshallable:_ = get () - let unfreeze x = s_proof := Some x + let unfreeze x = s_lemmas := Some x exception NoCurrentProof @@ -90,49 +95,62 @@ module Proof_global = struct | _ -> raise CErrors.Unhandled end + open Lemmas open Proof_global - let cc f = match !s_proof with + let cc f = match !s_lemmas with + | None -> raise NoCurrentProof + | Some x -> Stack.with_top_pstate ~f x + + let cc_lemma f = match !s_lemmas with + | None -> raise NoCurrentProof + | Some x -> Stack.with_top ~f x + + let cc_stack f = match !s_lemmas with | None -> raise NoCurrentProof | Some x -> f x - let dd f = match !s_proof with + let dd f = match !s_lemmas with | None -> raise NoCurrentProof - | Some x -> s_proof := Some (f x) + | Some x -> s_lemmas := Some (Stack.map_top_pstate ~f x) - let there_are_pending_proofs () = !s_proof <> None + let there_are_pending_proofs () = !s_lemmas <> None let get_open_goals () = cc get_open_goals - let set_terminator x = dd (set_terminator x) - let give_me_the_proof_opt () = Option.map give_me_the_proof !s_proof - let give_me_the_proof () = cc give_me_the_proof - let get_current_proof_name () = cc get_current_proof_name - - let simple_with_current_proof f = - dd (simple_with_current_proof f) + let give_me_the_proof_opt () = Option.map (Stack.with_top_pstate ~f:get_proof) !s_lemmas + let give_me_the_proof () = cc get_proof + let get_current_proof_name () = cc get_proof_name + let map_proof f = dd (map_proof f) let with_current_proof f = - let pf, res = cc (with_current_proof f) in - s_proof := Some pf; res + match !s_lemmas with + | None -> raise NoCurrentProof + | Some stack -> + let pf, res = Stack.with_top_pstate stack ~f:(map_fold_proof_endline f) in + let stack = Stack.map_top_pstate stack ~f:(fun _ -> pf) in + s_lemmas := Some stack; + res + + type closed_proof = Proof_global.proof_object * Lemmas.proof_info - let install_state s = s_proof := Some s - let return_proof ?allow_partial () = - cc (return_proof ?allow_partial) + let return_proof ?allow_partial () = cc (return_proof ?allow_partial) let close_future_proof ~opaque ~feedback_id pf = - cc (fun st -> close_future_proof ~opaque ~feedback_id st pf) + cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~opaque ~feedback_id st pf) pt, + Internal.get_info pt) let close_proof ~opaque ~keep_body_ucst_separate f = - cc (close_proof ~opaque ~keep_body_ucst_separate f) + cc_lemma (fun pt -> pf_fold ((close_proof ~opaque ~keep_body_ucst_separate f)) pt, + Internal.get_info pt) - let discard_all () = s_proof := None - let update_global_env () = dd update_global_env + let discard_all () = s_lemmas := None + let update_global_env () = dd (update_global_env) let get_current_context () = cc Pfedit.get_current_context let get_all_proof_names () = - try cc get_all_proof_names + try cc_stack Lemmas.Stack.get_all_proof_names with NoCurrentProof -> [] let copy_terminators ~src ~tgt = @@ -140,6 +158,6 @@ module Proof_global = struct | None, None -> None | Some _ , None -> None | None, Some x -> Some x - | Some src, Some tgt -> Some (copy_terminators ~src ~tgt) + | Some src, Some tgt -> Some (Stack.copy_info ~src ~tgt) end diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index dff81ad9bb..7e4d5d0315 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -18,12 +18,12 @@ module Parser : sig end -type t = { - parsing : Parser.state; - system : States.state; (* summary + libstack *) - proof : Proof_global.t option; (* proof state *) - shallow : bool (* is the state trimmed down (libstack) *) -} +type t = + { parsing : Parser.state + ; system : States.state (* summary + libstack *) + ; lemmas : Lemmas.Stack.t option (* proofs of lemmas currently opened *) + ; shallow : bool (* is the state trimmed down (libstack) *) + } val freeze_interp_state : marshallable:bool -> t val unfreeze_interp_state : t -> unit @@ -36,41 +36,29 @@ val invalidate_cache : unit -> unit (* Compatibility module: Do Not Use *) module Proof_global : sig - open Proof_global - - (* Low-level stuff *) - val get : unit -> t option - val set : t option -> unit - - val freeze : marshallable:bool -> t option - val unfreeze : t -> unit - exception NoCurrentProof val there_are_pending_proofs : unit -> bool val get_open_goals : unit -> int - val set_terminator : proof_terminator -> unit val give_me_the_proof : unit -> Proof.t val give_me_the_proof_opt : unit -> Proof.t option val get_current_proof_name : unit -> Names.Id.t - val simple_with_current_proof : - (unit Proofview.tactic -> Proof.t -> Proof.t) -> unit - + val map_proof : (Proof.t -> Proof.t) -> unit val with_current_proof : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a - val install_state : t -> unit + val return_proof : ?allow_partial:bool -> unit -> Proof_global.closed_proof_output - val return_proof : ?allow_partial:bool -> unit -> closed_proof_output + type closed_proof = Proof_global.proof_object * Lemmas.proof_info val close_future_proof : - opaque:opacity_flag -> + opaque:Proof_global.opacity_flag -> feedback_id:Stateid.t -> - closed_proof_output Future.computation -> closed_proof + Proof_global.closed_proof_output Future.computation -> closed_proof - val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof + val close_proof : opaque:Proof_global.opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof val discard_all : unit -> unit val update_global_env : unit -> unit @@ -79,7 +67,19 @@ module Proof_global : sig val get_all_proof_names : unit -> Names.Id.t list - val copy_terminators : src:t option -> tgt:t option -> t option + val copy_terminators : src:Lemmas.Stack.t option -> tgt:Lemmas.Stack.t option -> Lemmas.Stack.t option + + (* Handling of the imperative state *) + type t = Lemmas.Stack.t + + (* Low-level stuff *) + val get : unit -> t option + val set : t option -> unit + + val get_pstate : unit -> Proof_global.t option + + val freeze : marshallable:bool -> t option + val unfreeze : t -> unit end [@@ocaml.deprecated "This module is internal and should not be used, instead, thread the proof state"] |