aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/.ocamlformat-enable1
-rw-r--r--vernac/classes.mli10
-rw-r--r--vernac/comAssumption.ml6
-rw-r--r--vernac/comHints.ml174
-rw-r--r--vernac/comHints.mli29
-rw-r--r--vernac/declare.ml888
-rw-r--r--vernac/declare.mli284
-rw-r--r--vernac/declareDef.ml2
-rw-r--r--vernac/declareUniv.ml4
-rw-r--r--vernac/g_proofs.mlg1
-rw-r--r--vernac/g_vernac.mlg16
-rw-r--r--vernac/himsg.ml12
-rw-r--r--vernac/indschemes.ml5
-rw-r--r--vernac/library.ml63
-rw-r--r--vernac/ppvernac.ml7
-rw-r--r--vernac/pvernac.mli2
-rw-r--r--vernac/retrieveObl.ml2
-rw-r--r--vernac/vernac.mllib2
-rw-r--r--vernac/vernacentries.ml40
-rw-r--r--vernac/vernacentries.mli1
-rw-r--r--vernac/vernacexpr.ml18
21 files changed, 1468 insertions, 99 deletions
diff --git a/vernac/.ocamlformat-enable b/vernac/.ocamlformat-enable
new file mode 100644
index 0000000000..ffaa7e70f4
--- /dev/null
+++ b/vernac/.ocamlformat-enable
@@ -0,0 +1 @@
+comHints.ml
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 9698c14452..f410cddfef 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -22,7 +22,7 @@ val declare_instance : ?warn:bool -> env -> Evd.evar_map ->
Does nothing — or emit a “not-a-class” warning if the [warn] argument is set —
when said type is not a registered type class. *)
-val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit
+val existing_instance : bool -> qualid -> ComHints.hint_info_expr option -> unit
(** globality, reference, optional priority and pattern information *)
val new_instance_interactive
@@ -34,7 +34,7 @@ val new_instance_interactive
-> ?generalize:bool
-> ?tac:unit Proofview.tactic
-> ?hook:(GlobRef.t -> unit)
- -> Hints.hint_info_expr
+ -> ComHints.hint_info_expr
-> (bool * constr_expr) option
-> Id.t * Lemmas.t
@@ -47,7 +47,7 @@ val new_instance
-> (bool * constr_expr)
-> ?generalize:bool
-> ?hook:(GlobRef.t -> unit)
- -> Hints.hint_info_expr
+ -> ComHints.hint_info_expr
-> Id.t
val new_instance_program
@@ -59,7 +59,7 @@ val new_instance_program
-> (bool * constr_expr) option
-> ?generalize:bool
-> ?hook:(GlobRef.t -> unit)
- -> Hints.hint_info_expr
+ -> ComHints.hint_info_expr
-> Id.t
val declare_new_instance
@@ -69,7 +69,7 @@ val declare_new_instance
-> ident_decl
-> local_binder_expr list
-> constr_expr
- -> Hints.hint_info_expr
+ -> ComHints.hint_info_expr
-> unit
(** {6 Low level interface used by Add Morphism, do not use } *)
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 43e86fa9bd..776ffd6b9f 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -91,7 +91,7 @@ let declare_assumptions ~poly ~scope ~kind univs nl l =
let () = match scope with
| Discharge ->
(* declare universes separately for variables *)
- Declare.declare_universe_context ~poly (context_set_of_entry (fst univs))
+ DeclareUctx.declare_universe_context ~poly (context_set_of_entry (fst univs))
| Global _ -> ()
in
let _, _ = List.fold_left (fun (subst,univs) ((is_coe,idl),typ,imps) ->
@@ -191,7 +191,7 @@ let context_subst subst (name,b,t,impl) =
let context_insection sigma ~poly ctx =
let uctx = Evd.universe_context_set sigma in
- let () = Declare.declare_universe_context ~poly uctx in
+ let () = DeclareUctx.declare_universe_context ~poly uctx in
let fn subst (name,_,_,_ as d) =
let d = context_subst subst d in
let () = match d with
@@ -226,7 +226,7 @@ let context_nosection sigma ~poly ctx =
(* Multiple monomorphic axioms: declare universes separately to
avoid redeclaring them. *)
let uctx = Evd.universe_context_set sigma in
- let () = Declare.declare_universe_context ~poly uctx in
+ let () = DeclareUctx.declare_universe_context ~poly uctx in
Monomorphic_entry Univ.ContextSet.empty
in
let fn subst d =
diff --git a/vernac/comHints.ml b/vernac/comHints.ml
new file mode 100644
index 0000000000..5a48e9c16c
--- /dev/null
+++ b/vernac/comHints.ml
@@ -0,0 +1,174 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Util
+
+(** (Partial) implementation of the [Hint] command; some more
+ functionality still lives in tactics/hints.ml *)
+
+type hint_info_expr = Constrexpr.constr_pattern_expr Typeclasses.hint_info_gen
+
+type reference_or_constr =
+ | HintsReference of Libnames.qualid
+ | HintsConstr of Constrexpr.constr_expr
+
+type hints_expr =
+ | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
+ | HintsResolveIFF of bool * Libnames.qualid list * int option
+ | HintsImmediate of reference_or_constr list
+ | HintsUnfold of Libnames.qualid list
+ | HintsTransparency of Libnames.qualid Hints.hints_transparency_target * bool
+ | HintsMode of Libnames.qualid * Hints.hint_mode list
+ | HintsConstructors of Libnames.qualid list
+ | HintsExtern of
+ int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
+
+let project_hint ~poly pri l2r r =
+ let open EConstr in
+ let open Coqlib in
+ let gr = Smartlocate.global_with_alias r in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let sigma, c = Evd.fresh_global env sigma gr in
+ let t = Retyping.get_type_of env sigma c in
+ let t =
+ Tacred.reduce_to_quantified_ref env sigma (lib_ref "core.iff.type") t
+ in
+ let sign, ccl = decompose_prod_assum sigma t in
+ let a, b =
+ match snd (decompose_app sigma ccl) with
+ | [a; b] -> (a, b)
+ | _ -> assert false
+ in
+ let p = if l2r then lib_ref "core.iff.proj1" else lib_ref "core.iff.proj2" in
+ let sigma, p = Evd.fresh_global env sigma p in
+ let c =
+ Reductionops.whd_beta sigma
+ (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign))
+ in
+ let c =
+ it_mkLambda_or_LetIn
+ (mkApp
+ ( p
+ , [| mkArrow a Sorts.Relevant (Vars.lift 1 b)
+ ; mkArrow b Sorts.Relevant (Vars.lift 1 a)
+ ; c |] ))
+ sign
+ in
+ let name =
+ Nameops.add_suffix
+ (Nametab.basename_of_global gr)
+ ("_proj_" ^ if l2r then "l2r" else "r2l")
+ in
+ let ctx = Evd.univ_entry ~poly sigma in
+ let c = EConstr.to_constr sigma c in
+ let cb =
+ Declare.(DefinitionEntry (definition_entry ~univs:ctx ~opaque:false c))
+ in
+ let c =
+ Declare.declare_constant ~local:Declare.ImportDefaultBehavior ~name
+ ~kind:Decls.(IsDefinition Definition)
+ cb
+ in
+ let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
+ (info, false, true, Hints.PathAny, Hints.IsGlobRef (Names.GlobRef.ConstRef c))
+
+let warn_deprecated_hint_constr =
+ CWarnings.create ~name:"deprecated-hint-constr" ~category:"deprecated"
+ (fun () ->
+ Pp.strbrk
+ "Declaring arbitrary terms as hints is deprecated; declare a global \
+ reference instead")
+
+let interp_hints ~poly h =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let f poly c =
+ let evd, c = Constrintern.interp_open_constr env sigma c in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let c, diff = Hints.prepare_hint true env sigma (evd, c) in
+ if poly then (Hints.IsConstr (c, diff) [@ocaml.warning "-3"])
+ else
+ let () = DeclareUctx.declare_universe_context ~poly:false diff in
+ (Hints.IsConstr (c, Univ.ContextSet.empty) [@ocaml.warning "-3"])
+ in
+ let fref r =
+ let gr = Smartlocate.global_with_alias r in
+ Dumpglob.add_glob ?loc:r.CAst.loc gr;
+ gr
+ in
+ let fr r = Tacred.evaluable_of_global_reference env (fref r) in
+ let fi c =
+ let open Hints in
+ match c with
+ | HintsReference c ->
+ let gr = Smartlocate.global_with_alias c in
+ (PathHints [gr], poly, IsGlobRef gr)
+ | HintsConstr c ->
+ let () = warn_deprecated_hint_constr () in
+ (PathAny, poly, f poly c)
+ in
+ let fp = Constrintern.intern_constr_pattern env sigma in
+ let fres (info, b, r) =
+ let path, poly, gr = fi r in
+ let info =
+ { info with
+ Typeclasses.hint_pattern = Option.map fp info.Typeclasses.hint_pattern
+ }
+ in
+ (info, poly, b, path, gr)
+ in
+ let ft =
+ let open Hints in
+ function
+ | HintsVariables -> HintsVariables
+ | HintsConstants -> HintsConstants
+ | HintsReferences lhints -> HintsReferences (List.map fr lhints)
+ in
+ let fp = Constrintern.intern_constr_pattern (Global.env ()) in
+ let open Hints in
+ match h with
+ | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints)
+ | HintsResolveIFF (l2r, lc, n) ->
+ HintsResolveEntry (List.map (project_hint ~poly n l2r) lc)
+ | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints)
+ | HintsUnfold lhints -> HintsUnfoldEntry (List.map fr lhints)
+ | HintsTransparency (t, b) -> HintsTransparencyEntry (ft t, b)
+ | HintsMode (r, l) -> HintsModeEntry (fref r, l)
+ | HintsConstructors lqid ->
+ let constr_hints_of_ind qid =
+ let ind = Smartlocate.global_inductive_with_alias qid in
+ let mib, _ = Global.lookup_inductive ind in
+ Dumpglob.dump_reference ?loc:qid.CAst.loc "<>"
+ (Libnames.string_of_qualid qid)
+ "ind";
+ List.init (Inductiveops.nconstructors env ind) (fun i ->
+ let c = (ind, i + 1) in
+ let gr = Names.GlobRef.ConstructRef c in
+ ( empty_hint_info
+ , Declareops.inductive_is_polymorphic mib
+ , true
+ , PathHints [gr]
+ , IsGlobRef gr ))
+ in
+ HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
+ | HintsExtern (pri, patcom, tacexp) ->
+ let pat = Option.map (fp sigma) patcom in
+ let l = match pat with None -> [] | Some (l, _) -> l in
+ let ltacvars =
+ List.fold_left
+ (fun accu x -> Names.Id.Set.add x accu)
+ Names.Id.Set.empty l
+ in
+ let env = Genintern.{(empty_glob_sign env) with ltacvars} in
+ let _, tacexp = Genintern.generic_intern env tacexp in
+ HintsExternEntry
+ ({Typeclasses.hint_priority = Some pri; hint_pattern = pat}, tacexp)
diff --git a/vernac/comHints.mli b/vernac/comHints.mli
new file mode 100644
index 0000000000..77fbef5387
--- /dev/null
+++ b/vernac/comHints.mli
@@ -0,0 +1,29 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Typeclasses
+
+type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
+
+type reference_or_constr =
+ | HintsReference of Libnames.qualid
+ | HintsConstr of Constrexpr.constr_expr
+
+type hints_expr =
+ | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
+ | HintsResolveIFF of bool * Libnames.qualid list * int option
+ | HintsImmediate of reference_or_constr list
+ | HintsUnfold of Libnames.qualid list
+ | HintsTransparency of Libnames.qualid Hints.hints_transparency_target * bool
+ | HintsMode of Libnames.qualid * Hints.hint_mode list
+ | HintsConstructors of Libnames.qualid list
+ | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
+
+val interp_hints : poly:bool -> hints_expr -> Hints.hints_entry
diff --git a/vernac/declare.ml b/vernac/declare.ml
new file mode 100644
index 0000000000..366dd2d026
--- /dev/null
+++ b/vernac/declare.ml
@@ -0,0 +1,888 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(** This module is about the low-level declaration of logical objects *)
+
+open Pp
+open Util
+open Names
+open Safe_typing
+module NamedDecl = Context.Named.Declaration
+
+type opacity_flag = Opaque | Transparent
+
+type t =
+ { endline_tactic : Genarg.glob_generic_argument option
+ ; section_vars : Id.Set.t option
+ ; proof : Proof.t
+ ; udecl: UState.universe_decl
+ (** Initial universe declarations *)
+ ; initial_euctx : UState.t
+ (** The initial universe context (for the statement) *)
+ }
+
+(*** Proof Global manipulation ***)
+
+let get_proof ps = ps.proof
+let get_proof_name ps = (Proof.data ps.proof).Proof.name
+
+let get_initial_euctx ps = ps.initial_euctx
+
+let map_proof f p = { p with proof = f p.proof }
+let map_fold_proof f p = let proof, res = f p.proof in { p with proof }, res
+
+let map_fold_proof_endline f ps =
+ let et =
+ match ps.endline_tactic with
+ | None -> Proofview.tclUNIT ()
+ | Some tac ->
+ let open Geninterp in
+ let {Proof.poly} = Proof.data ps.proof in
+ let ist = { lfun = Id.Map.empty; poly; extra = TacStore.empty } in
+ let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in
+ let tac = Geninterp.interp tag ist tac in
+ Ftactic.run tac (fun _ -> Proofview.tclUNIT ())
+ in
+ let (newpr,ret) = f et ps.proof in
+ let ps = { ps with proof = newpr } in
+ ps, ret
+
+let compact_the_proof pf = map_proof Proof.compact pf
+
+(* Sets the tactic to be used when a tactic line is closed with [...] *)
+let set_endline_tactic tac ps =
+ { ps with endline_tactic = Some tac }
+
+(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of
+ name [name] with goals [goals] (a list of pairs of environment and
+ conclusion). The proof is started in the evar map [sigma] (which
+ can typically contain universe constraints), and with universe
+ bindings [udecl]. *)
+let start_proof ~name ~udecl ~poly sigma goals =
+ let proof = Proof.start ~name ~poly sigma goals in
+ let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
+ { proof
+ ; endline_tactic = None
+ ; section_vars = None
+ ; udecl
+ ; initial_euctx
+ }
+
+let start_dependent_proof ~name ~udecl ~poly goals =
+ let proof = Proof.dependent_start ~name ~poly goals in
+ let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
+ { proof
+ ; endline_tactic = None
+ ; section_vars = None
+ ; udecl
+ ; initial_euctx
+ }
+
+let get_used_variables pf = pf.section_vars
+let get_universe_decl pf = pf.udecl
+
+let set_used_variables ps l =
+ let open Context.Named.Declaration in
+ let env = Global.env () in
+ let ids = List.fold_right Id.Set.add l Id.Set.empty in
+ let ctx = Environ.keep_hyps env ids in
+ let ctx_set =
+ List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in
+ let vars_of = Environ.global_vars_set in
+ let aux env entry (ctx, all_safe as orig) =
+ match entry with
+ | LocalAssum ({Context.binder_name=x},_) ->
+ if Id.Set.mem x all_safe then orig
+ else (ctx, all_safe)
+ | LocalDef ({Context.binder_name=x},bo, ty) as decl ->
+ if Id.Set.mem x all_safe then orig else
+ let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
+ if Id.Set.subset vars all_safe
+ then (decl :: ctx, Id.Set.add x all_safe)
+ else (ctx, all_safe) in
+ let ctx, _ =
+ Environ.fold_named_context aux env ~init:(ctx,ctx_set) in
+ if not (Option.is_empty ps.section_vars) then
+ CErrors.user_err Pp.(str "Used section variables can be declared only once");
+ ctx, { ps with section_vars = Some (Context.Named.to_vars ctx) }
+
+let get_open_goals ps =
+ let Proof.{ goals; stack; shelf } = Proof.data ps.proof in
+ List.length goals +
+ List.fold_left (+) 0
+ (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) +
+ List.length shelf
+
+(* object_kind , id *)
+exception AlreadyDeclared of (string option * Id.t)
+
+let _ = CErrors.register_handler (function
+ | AlreadyDeclared (kind, id) ->
+ Some
+ (seq [ Pp.pr_opt_no_spc (fun s -> str s ++ spc ()) kind
+ ; Id.print id; str " already exists."])
+ | _ ->
+ None)
+
+type import_status = ImportDefaultBehavior | ImportNeedQualified
+
+(** Declaration of constants and parameters *)
+
+type constant_obj = {
+ cst_kind : Decls.logical_kind;
+ cst_locl : import_status;
+}
+
+type 'a proof_entry = {
+ proof_entry_body : 'a Entries.const_entry_body;
+ (* List of section variables *)
+ proof_entry_secctx : Id.Set.t option;
+ (* State id on which the completion of type checking is reported *)
+ proof_entry_feedback : Stateid.t option;
+ proof_entry_type : Constr.types option;
+ proof_entry_universes : Entries.universes_entry;
+ proof_entry_opaque : bool;
+ proof_entry_inline_code : bool;
+}
+
+let default_univ_entry = Entries.Monomorphic_entry Univ.ContextSet.empty
+
+let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types
+ ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univsbody=Univ.ContextSet.empty) body =
+ { proof_entry_body = Future.from_val ?fix_exn ((body,univsbody), eff);
+ proof_entry_secctx = section_vars;
+ proof_entry_type = types;
+ proof_entry_universes = univs;
+ proof_entry_opaque = opaque;
+ proof_entry_feedback = feedback_id;
+ proof_entry_inline_code = inline}
+
+type proof_object =
+ { name : Names.Id.t
+ (* [name] only used in the STM *)
+ ; entries : Evd.side_effects proof_entry list
+ ; uctx: UState.t
+ }
+
+let private_poly_univs =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Private";"Polymorphic";"Universes"]
+ ~value:true
+
+(* XXX: This is still separate from close_proof below due to drop_pt in the STM *)
+(* XXX: Unsafe_typ:true is needed by vio files, see bf0499bc507d5a39c3d5e3bf1f69191339270729 *)
+let prepare_proof ~unsafe_typ { proof } =
+ let Proof.{name=pid;entry;poly} = Proof.data proof in
+ let initial_goals = Proofview.initial_goals entry in
+ let evd = Proof.return ~pid proof in
+ let eff = Evd.eval_side_effects evd in
+ let evd = Evd.minimize_universes evd in
+ let to_constr_body c =
+ match EConstr.to_constr_opt evd c with
+ | Some p -> p
+ | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain")
+ in
+ let to_constr_typ t =
+ if unsafe_typ then EConstr.Unsafe.to_constr t else to_constr_body t
+ in
+ (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
+ side-effects... This may explain why one need to uniquize side-effects
+ thereafter... *)
+ (* EJGA: actually side-effects de-duplication and this codepath is
+ unrelated. Duplicated side-effects arise from incorrect scheme
+ generation code, the main bulk of it was mostly fixed by #9836
+ but duplication can still happen because of rewriting schemes I
+ think; however the code below is mostly untested, the only
+ code-paths that generate several proof entries are derive and
+ equations and so far there is no code in the CI that will
+ actually call those and do a side-effect, TTBOMK *)
+ (* EJGA: likely the right solution is to attach side effects to the first constant only? *)
+ let proofs = List.map (fun (body, typ) -> (to_constr_body body, eff), to_constr_typ typ) initial_goals in
+ proofs, Evd.evar_universe_context evd
+
+let close_proof ~opaque ~keep_body_ucst_separate ps =
+
+ let { section_vars; proof; udecl; initial_euctx } = ps in
+ let { Proof.name; poly } = Proof.data proof in
+ let unsafe_typ = keep_body_ucst_separate && not poly in
+ let elist, uctx = prepare_proof ~unsafe_typ ps in
+ let opaque = match opaque with Opaque -> true | Transparent -> false in
+
+ let make_entry ((body, eff), typ) =
+
+ let allow_deferred =
+ not poly &&
+ (keep_body_ucst_separate
+ || not (Safe_typing.is_empty_private_constants eff.Evd.seff_private))
+ in
+ let used_univs_body = Vars.universes_of_constr body in
+ let used_univs_typ = Vars.universes_of_constr typ in
+ let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+ let utyp, ubody =
+ if allow_deferred then
+ let utyp = UState.univ_entry ~poly initial_euctx in
+ let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in
+ (* For vi2vo compilation proofs are computed now but we need to
+ complement the univ constraints of the typ with the ones of
+ the body. So we keep the two sets distinct. *)
+ let uctx_body = UState.restrict uctx used_univs in
+ let ubody = UState.check_mono_univ_decl uctx_body udecl in
+ utyp, ubody
+ else if poly && opaque && private_poly_univs () then
+ let universes = UState.restrict uctx used_univs in
+ let typus = UState.restrict universes used_univs_typ in
+ let utyp = UState.check_univ_decl ~poly typus udecl in
+ let ubody = Univ.ContextSet.diff
+ (UState.context_set universes)
+ (UState.context_set typus)
+ in
+ utyp, ubody
+ else
+ (* Since the proof is computed now, we can simply have 1 set of
+ constraints in which we merge the ones for the body and the ones
+ for the typ. We recheck the declaration after restricting with
+ the actually used universes.
+ TODO: check if restrict is really necessary now. *)
+ let ctx = UState.restrict uctx used_univs in
+ let utyp = UState.check_univ_decl ~poly ctx udecl in
+ utyp, Univ.ContextSet.empty
+ in
+ definition_entry ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
+ in
+ let entries = CList.map make_entry elist in
+ { name; entries; uctx }
+
+type 'a constant_entry =
+ | DefinitionEntry of 'a proof_entry
+ | ParameterEntry of Entries.parameter_entry
+ | PrimitiveEntry of Entries.primitive_entry
+
+(* At load-time, the segment starting from the module name to the discharge *)
+(* section (if Remark or Fact) is needed to access a construction *)
+let load_constant i ((sp,kn), obj) =
+ if Nametab.exists_cci sp then
+ raise (AlreadyDeclared (None, Libnames.basename sp));
+ let con = Global.constant_of_delta_kn kn in
+ Nametab.push (Nametab.Until i) sp (GlobRef.ConstRef con);
+ Dumpglob.add_constant_kind con obj.cst_kind
+
+(* Opening means making the name without its module qualification available *)
+let open_constant f i ((sp,kn), obj) =
+ (* Never open a local definition *)
+ match obj.cst_locl with
+ | ImportNeedQualified -> ()
+ | ImportDefaultBehavior ->
+ let con = Global.constant_of_delta_kn kn in
+ if Libobject.in_filter_ref (GlobRef.ConstRef con) f then
+ Nametab.push (Nametab.Exactly i) sp (GlobRef.ConstRef con)
+
+let exists_name id =
+ Decls.variable_exists id || Global.exists_objlabel (Label.of_id id)
+
+let check_exists id =
+ if exists_name id then
+ raise (AlreadyDeclared (None, id))
+
+let cache_constant ((sp,kn), obj) =
+ (* Invariant: the constant must exist in the logical environment, except when
+ redefining it when exiting a section. See [discharge_constant]. *)
+ let kn' =
+ if Global.exists_objlabel (Label.of_id (Libnames.basename sp))
+ then Constant.make1 kn
+ else CErrors.anomaly Pp.(str"Missing constant " ++ Id.print(Libnames.basename sp) ++ str".")
+ in
+ assert (Constant.equal kn' (Constant.make1 kn));
+ Nametab.push (Nametab.Until 1) sp (GlobRef.ConstRef (Constant.make1 kn));
+ Dumpglob.add_constant_kind (Constant.make1 kn) obj.cst_kind
+
+let discharge_constant ((sp, kn), obj) =
+ Some obj
+
+(* Hack to reduce the size of .vo: we keep only what load/open needs *)
+let dummy_constant cst = {
+ cst_kind = cst.cst_kind;
+ cst_locl = cst.cst_locl;
+}
+
+let classify_constant cst = Libobject.Substitute (dummy_constant cst)
+
+let (objConstant : constant_obj Libobject.Dyn.tag) =
+ let open Libobject in
+ declare_object_full { (default_object "CONSTANT") with
+ cache_function = cache_constant;
+ load_function = load_constant;
+ open_function = open_constant;
+ classify_function = classify_constant;
+ subst_function = ident_subst_function;
+ discharge_function = discharge_constant }
+
+let inConstant v = Libobject.Dyn.Easy.inj v objConstant
+
+let update_tables c =
+ Impargs.declare_constant_implicits c;
+ Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstRef c)
+
+let register_constant kn kind local =
+ let o = inConstant {
+ cst_kind = kind;
+ cst_locl = local;
+ } in
+ let id = Label.to_id (Constant.label kn) in
+ let _ = Lib.add_leaf id o in
+ update_tables kn
+
+let register_side_effect (c, role) =
+ let () = register_constant c Decls.(IsProof Theorem) ImportDefaultBehavior in
+ match role with
+ | None -> ()
+ | Some (Evd.Schema (ind, kind)) -> DeclareScheme.declare_scheme kind [|ind,c|]
+
+let get_roles export eff =
+ let map c =
+ let role = try Some (Cmap.find c eff.Evd.seff_roles) with Not_found -> None in
+ (c, role)
+ in
+ List.map map export
+
+let export_side_effects eff =
+ let export = Global.export_private_constants eff.Evd.seff_private in
+ let export = get_roles export eff in
+ List.iter register_side_effect export
+
+let record_aux env s_ty s_bo =
+ let open Environ in
+ let in_ty = keep_hyps env s_ty in
+ let v =
+ String.concat " "
+ (CList.map_filter (fun decl ->
+ let id = NamedDecl.get_id decl in
+ if List.exists (NamedDecl.get_id %> Id.equal id) in_ty then None
+ else Some (Id.to_string id))
+ (keep_hyps env s_bo)) in
+ Aux_file.record_in_aux "context_used" v
+
+let pure_definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
+ ?(univs=default_univ_entry) body =
+ { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), ());
+ proof_entry_secctx = None;
+ proof_entry_type = types;
+ proof_entry_universes = univs;
+ proof_entry_opaque = opaque;
+ proof_entry_feedback = None;
+ proof_entry_inline_code = inline}
+
+let delayed_definition_entry ~opaque ?feedback_id ~section_vars ~univs ?types body =
+ { proof_entry_body = body
+ ; proof_entry_secctx = section_vars
+ ; proof_entry_type = types
+ ; proof_entry_universes = univs
+ ; proof_entry_opaque = opaque
+ ; proof_entry_feedback = feedback_id
+ ; proof_entry_inline_code = false
+ }
+
+let cast_proof_entry e =
+ let (body, ctx), () = Future.force e.proof_entry_body in
+ let univs =
+ if Univ.ContextSet.is_empty ctx then e.proof_entry_universes
+ else match e.proof_entry_universes with
+ | Entries.Monomorphic_entry ctx' ->
+ (* This can actually happen, try compiling EqdepFacts for instance *)
+ Entries.Monomorphic_entry (Univ.ContextSet.union ctx' ctx)
+ | Entries.Polymorphic_entry _ ->
+ CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.");
+ in
+ { Entries.const_entry_body = body;
+ const_entry_secctx = e.proof_entry_secctx;
+ const_entry_feedback = e.proof_entry_feedback;
+ const_entry_type = e.proof_entry_type;
+ const_entry_universes = univs;
+ const_entry_inline_code = e.proof_entry_inline_code;
+ }
+
+type ('a, 'b) effect_entry =
+| EffectEntry : (private_constants, private_constants Entries.const_entry_body) effect_entry
+| PureEntry : (unit, Constr.constr) effect_entry
+
+let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proof_entry) : b Entries.opaque_entry =
+ let typ = match e.proof_entry_type with
+ | None -> assert false
+ | Some typ -> typ
+ in
+ let secctx = match e.proof_entry_secctx with
+ | None ->
+ let open Environ in
+ let env = Global.env () in
+ let hyp_typ, hyp_def =
+ if List.is_empty (Environ.named_context env) then
+ Id.Set.empty, Id.Set.empty
+ else
+ let ids_typ = global_vars_set env typ in
+ let pf, env = match entry with
+ | PureEntry ->
+ let (pf, _), () = Future.force e.proof_entry_body in
+ pf, env
+ | EffectEntry ->
+ let (pf, _), eff = Future.force e.proof_entry_body in
+ let env = Safe_typing.push_private_constants env eff in
+ pf, env
+ in
+ let vars = global_vars_set env pf in
+ ids_typ, vars
+ in
+ let () = if Aux_file.recording () then record_aux env hyp_typ hyp_def in
+ Environ.really_needed env (Id.Set.union hyp_typ hyp_def)
+ | Some hyps -> hyps
+ in
+ let (body, univs : b * _) = match entry with
+ | PureEntry ->
+ let (body, uctx), () = Future.force e.proof_entry_body in
+ let univs = match e.proof_entry_universes with
+ | Entries.Monomorphic_entry uctx' ->
+ Entries.Monomorphic_entry (Univ.ContextSet.union uctx uctx')
+ | Entries.Polymorphic_entry _ ->
+ assert (Univ.ContextSet.is_empty uctx);
+ e.proof_entry_universes
+ in
+ body, univs
+ | EffectEntry -> e.proof_entry_body, e.proof_entry_universes
+ in
+ { Entries.opaque_entry_body = body;
+ opaque_entry_secctx = secctx;
+ opaque_entry_feedback = e.proof_entry_feedback;
+ opaque_entry_type = typ;
+ opaque_entry_universes = univs;
+ }
+
+let feedback_axiom () = Feedback.(feedback AddedAxiom)
+
+let is_unsafe_typing_flags () =
+ let open Declarations in
+ let flags = Environ.typing_flags (Global.env()) in
+ not (flags.check_universes && flags.check_guarded && flags.check_positive)
+
+let define_constant ~name cd =
+ (* Logically define the constant and its subproofs, no libobject tampering *)
+ let decl, unsafe = match cd with
+ | DefinitionEntry de ->
+ (* We deal with side effects *)
+ if not de.proof_entry_opaque then
+ let body, eff = Future.force de.proof_entry_body in
+ (* This globally defines the side-effects in the environment
+ and registers their libobjects. *)
+ let () = export_side_effects eff in
+ let de = { de with proof_entry_body = Future.from_val (body, ()) } in
+ let cd = Entries.DefinitionEntry (cast_proof_entry de) in
+ ConstantEntry cd, false
+ else
+ let map (body, eff) = body, eff.Evd.seff_private in
+ let body = Future.chain de.proof_entry_body map in
+ let de = { de with proof_entry_body = body } in
+ let de = cast_opaque_proof_entry EffectEntry de in
+ OpaqueEntry de, false
+ | ParameterEntry e ->
+ ConstantEntry (Entries.ParameterEntry e), not (Lib.is_modtype_strict())
+ | PrimitiveEntry e ->
+ ConstantEntry (Entries.PrimitiveEntry e), false
+ in
+ let kn = Global.add_constant name decl in
+ if unsafe || is_unsafe_typing_flags() then feedback_axiom();
+ kn
+
+let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd =
+ let () = check_exists name in
+ let kn = define_constant ~name cd in
+ (* Register the libobjects attached to the constants *)
+ let () = register_constant kn kind local in
+ kn
+
+let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind de =
+ let kn, eff =
+ let de =
+ if not de.proof_entry_opaque then
+ DefinitionEff (cast_proof_entry de)
+ else
+ let de = cast_opaque_proof_entry PureEntry de in
+ OpaqueEff de
+ in
+ Global.add_private_constant name de
+ in
+ let () = register_constant kn kind local in
+ let seff_roles = match role with
+ | None -> Cmap.empty
+ | Some r -> Cmap.singleton kn r
+ in
+ let eff = { Evd.seff_private = eff; Evd.seff_roles; } in
+ kn, eff
+
+let inline_private_constants ~uctx env ce =
+ let body, eff = Future.force ce.proof_entry_body in
+ let cb, ctx = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in
+ let uctx = UState.merge ~sideff:true Evd.univ_rigid uctx ctx in
+ cb, uctx
+
+(** Declaration of section variables and local definitions *)
+type variable_declaration =
+ | SectionLocalDef of Evd.side_effects proof_entry
+ | SectionLocalAssum of { typ:Constr.types; impl:Glob_term.binding_kind; }
+
+(* This object is only for things which iterate over objects to find
+ variables (only Prettyp.print_context AFAICT) *)
+let objVariable : unit Libobject.Dyn.tag =
+ let open Libobject in
+ declare_object_full { (default_object "VARIABLE") with
+ classify_function = (fun () -> Dispose)}
+
+let inVariable v = Libobject.Dyn.Easy.inj v objVariable
+
+let declare_variable ~name ~kind d =
+ (* Variables are distinguished by only short names *)
+ if Decls.variable_exists name then
+ raise (AlreadyDeclared (None, name));
+
+ let impl,opaque = match d with (* Fails if not well-typed *)
+ | SectionLocalAssum {typ;impl} ->
+ let () = Global.push_named_assum (name,typ) in
+ impl, true
+ | SectionLocalDef (de) ->
+ (* The body should already have been forced upstream because it is a
+ section-local definition, but it's not enforced by typing *)
+ let ((body, body_ui), eff) = Future.force de.proof_entry_body in
+ let () = export_side_effects eff in
+ let poly, entry_ui = match de.proof_entry_universes with
+ | Entries.Monomorphic_entry uctx -> false, uctx
+ | Entries.Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
+ in
+ let univs = Univ.ContextSet.union body_ui entry_ui in
+ (* We must declare the universe constraints before type-checking the
+ term. *)
+ let () = DeclareUctx.declare_universe_context ~poly univs in
+ let se = {
+ Entries.secdef_body = body;
+ secdef_secctx = de.proof_entry_secctx;
+ secdef_feedback = de.proof_entry_feedback;
+ secdef_type = de.proof_entry_type;
+ } in
+ let () = Global.push_named_def (name, se) in
+ Glob_term.Explicit, de.proof_entry_opaque
+ in
+ Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name);
+ Decls.(add_variable_data name {opaque;kind});
+ ignore(Lib.add_leaf name (inVariable ()) : Libobject.object_name);
+ Impargs.declare_var_implicits ~impl name;
+ Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name)
+
+(* Declaration messages *)
+
+let pr_rank i = pr_nth (i+1)
+
+let fixpoint_message indexes l =
+ Flags.if_verbose Feedback.msg_info (match l with
+ | [] -> CErrors.anomaly (Pp.str "no recursive definition.")
+ | [id] -> Id.print id ++ str " is recursively defined" ++
+ (match indexes with
+ | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)"
+ | _ -> mt ())
+ | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++
+ spc () ++ str "are recursively defined" ++
+ match indexes with
+ | Some a -> spc () ++ str "(decreasing respectively on " ++
+ prvect_with_sep pr_comma pr_rank a ++
+ str " arguments)"
+ | None -> mt ()))
+
+let cofixpoint_message l =
+ Flags.if_verbose Feedback.msg_info (match l with
+ | [] -> CErrors.anomaly (Pp.str "No corecursive definition.")
+ | [id] -> Id.print id ++ str " is corecursively defined"
+ | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++
+ spc () ++ str "are corecursively defined"))
+
+let recursive_message isfix i l =
+ (if isfix then fixpoint_message i else cofixpoint_message) l
+
+let definition_message id =
+ Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined")
+
+let assumption_message id =
+ (* Changing "assumed" to "declared", "assuming" referring more to
+ the type of the object than to the name of the object (see
+ discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *)
+ Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared")
+
+module Internal = struct
+
+ let map_entry_body ~f entry =
+ { entry with proof_entry_body = Future.chain entry.proof_entry_body f }
+
+ let map_entry_type ~f entry =
+ { entry with proof_entry_type = f entry.proof_entry_type }
+
+ let set_opacity ~opaque entry =
+ { entry with proof_entry_opaque = opaque }
+
+ let get_fix_exn entry = Future.fix_exn_of entry.proof_entry_body
+
+ let rec decompose len c t accu =
+ let open Constr in
+ let open Context.Rel.Declaration in
+ if len = 0 then (c, t, accu)
+ else match kind c, kind t with
+ | Lambda (na, u, c), Prod (_, _, t) ->
+ decompose (pred len) c t (LocalAssum (na, u) :: accu)
+ | LetIn (na, b, u, c), LetIn (_, _, _, t) ->
+ decompose (pred len) c t (LocalDef (na, b, u) :: accu)
+ | _ -> assert false
+
+ let rec shrink ctx sign c t accu =
+ let open Constr in
+ let open Vars in
+ match ctx, sign with
+ | [], [] -> (c, t, accu)
+ | p :: ctx, decl :: sign ->
+ if noccurn 1 c && noccurn 1 t then
+ let c = subst1 mkProp c in
+ let t = subst1 mkProp t in
+ shrink ctx sign c t accu
+ else
+ let c = Term.mkLambda_or_LetIn p c in
+ let t = Term.mkProd_or_LetIn p t in
+ let accu = if Context.Rel.Declaration.is_local_assum p
+ then mkVar (NamedDecl.get_id decl) :: accu
+ else accu
+ in
+ shrink ctx sign c t accu
+ | _ -> assert false
+
+ let shrink_entry sign const =
+ let typ = match const.proof_entry_type with
+ | None -> assert false
+ | Some t -> t
+ in
+ (* The body has been forced by the call to [build_constant_by_tactic] *)
+ let () = assert (Future.is_over const.proof_entry_body) in
+ let ((body, uctx), eff) = Future.force const.proof_entry_body in
+ let (body, typ, ctx) = decompose (List.length sign) body typ [] in
+ let (body, typ, args) = shrink ctx sign body typ [] in
+ { const with
+ proof_entry_body = Future.from_val ((body, uctx), eff)
+ ; proof_entry_type = Some typ
+ }, args
+
+ type nonrec constant_obj = constant_obj
+
+ let objVariable = objVariable
+ let objConstant = objConstant
+
+end
+(*** Proof Global Environment ***)
+
+type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t
+
+let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.computation) =
+ let { section_vars; proof; udecl; initial_euctx } = ps in
+ let { Proof.name; poly; entry; sigma } = Proof.data proof in
+
+ (* We don't allow poly = true in this path *)
+ if poly then
+ CErrors.anomaly (Pp.str "Cannot delay universe-polymorphic constants.");
+
+ let fpl, uctx = Future.split2 fpl in
+ (* Because of dependent subgoals at the beginning of proofs, we could
+ have existential variables in the initial types of goals, we need to
+ normalise them for the kernel. *)
+ let subst_evar k = Evd.existential_opt_value0 sigma k in
+ let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar (UState.subst initial_euctx) in
+
+ (* We only support opaque proofs, this will be enforced by using
+ different entries soon *)
+ let opaque = true in
+ let make_entry p (_, types) =
+ (* Already checked the univ_decl for the type universes when starting the proof. *)
+ let univs = UState.univ_entry ~poly:false initial_euctx in
+ let types = nf (EConstr.Unsafe.to_constr types) in
+
+ Future.chain p (fun (pt,eff) ->
+ (* Deferred proof, we already checked the universe declaration with
+ the initial universes, ensure that the final universes respect
+ the declaration as well. If the declaration is non-extensible,
+ this will prevent the body from adding universes and constraints. *)
+ let uctx = Future.force uctx in
+ let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in
+ let used_univs = Univ.LSet.union
+ (Vars.universes_of_constr types)
+ (Vars.universes_of_constr pt)
+ in
+ let univs = UState.restrict uctx used_univs in
+ let univs = UState.check_mono_univ_decl univs udecl in
+ (pt,univs),eff)
+ |> delayed_definition_entry ~opaque ~feedback_id ~section_vars ~univs ~types
+ in
+ let entries = Future.map2 make_entry fpl (Proofview.initial_goals entry) in
+ { name; entries; uctx = initial_euctx }
+
+let close_future_proof = close_proof_delayed
+
+let return_partial_proof { proof } =
+ let proofs = Proof.partial_proof proof in
+ let Proof.{sigma=evd} = Proof.data proof in
+ let eff = Evd.eval_side_effects evd in
+ (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
+ side-effects... This may explain why one need to uniquize side-effects
+ thereafter... *)
+ let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in
+ proofs, Evd.evar_universe_context evd
+
+let return_proof ps =
+ let p, uctx = prepare_proof ~unsafe_typ:false ps in
+ List.map fst p, uctx
+
+let update_global_env =
+ map_proof (fun p ->
+ let { Proof.sigma } = Proof.data p in
+ let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
+ let p, (status,info), _ = Proof.run_tactic (Global.env ()) tac p in
+ p)
+
+let next = let n = ref 0 in fun () -> incr n; !n
+
+let by tac = map_fold_proof (Proof.solve (Goal_select.SelectNth 1) None tac)
+
+let build_constant_by_tactic ~name ?(opaque=Transparent) ~uctx ~sign ~poly typ tac =
+ let evd = Evd.from_ctx uctx in
+ let goals = [ (Global.env_of_context sign , typ) ] in
+ let pf = start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in
+ let pf, status = by tac pf in
+ let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false pf in
+ match entries with
+ | [entry] ->
+ entry, status, uctx
+ | _ ->
+ CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term")
+
+let build_by_tactic ?(side_eff=true) env ~uctx ~poly ~typ tac =
+ let name = Id.of_string ("temporary_proof"^string_of_int (next())) in
+ let sign = Environ.(val_of_named_context (named_context env)) in
+ let ce, status, univs = build_constant_by_tactic ~name ~uctx ~sign ~poly typ tac in
+ let cb, uctx =
+ if side_eff then inline_private_constants ~uctx env ce
+ else
+ (* GG: side effects won't get reset: no need to treat their universes specially *)
+ let (cb, ctx), _eff = Future.force ce.proof_entry_body in
+ cb, UState.merge ~sideff:false Evd.univ_rigid uctx ctx
+ in
+ cb, ce.proof_entry_type, status, univs
+
+let declare_abstract ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma concl =
+ (* EJGA: flush_and_check_evars is only used in abstract, could we
+ use a different API? *)
+ let concl =
+ try Evarutil.flush_and_check_evars sigma concl
+ with Evarutil.Uninstantiated_evar _ ->
+ CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials.")
+ in
+ let sigma, concl =
+ (* FIXME: should be done only if the tactic succeeds *)
+ let sigma = Evd.minimize_universes sigma in
+ sigma, Evarutil.nf_evars_universes sigma concl
+ in
+ let concl = EConstr.of_constr concl in
+ let uctx = Evd.evar_universe_context sigma in
+ let (const, safe, uctx) =
+ try build_constant_by_tactic ~name ~opaque:Transparent ~poly ~uctx ~sign:secsign concl solve_tac
+ with Logic_monad.TacticFailure e as src ->
+ (* if the tactic [tac] fails, it reports a [TacticFailure e],
+ which is an error irrelevant to the proof system (in fact it
+ means that [e] comes from [tac] failing to yield enough
+ success). Hence it reraises [e]. *)
+ let (_, info) = Exninfo.capture src in
+ Exninfo.iraise (e, info)
+ in
+ let sigma = Evd.set_universe_context sigma uctx in
+ let body, effs = Future.force const.proof_entry_body in
+ (* We drop the side-effects from the entry, they already exist in the ambient environment *)
+ let const = Internal.map_entry_body const ~f:(fun _ -> body, ()) in
+ (* EJGA: Hack related to the above call to
+ `build_constant_by_tactic` with `~opaque:Transparent`. Even if
+ the abstracted term is destined to be opaque, if we trigger the
+ `if poly && opaque && private_poly_univs ()` in `Proof_global`
+ kernel will boom. This deserves more investigation. *)
+ let const = Internal.set_opacity ~opaque const in
+ let const, args = Internal.shrink_entry sign const in
+ let cst () =
+ (* do not compute the implicit arguments, it may be costly *)
+ let () = Impargs.make_implicit_args false in
+ (* ppedrot: seems legit to have abstracted subproofs as local*)
+ declare_private_constant ~local:ImportNeedQualified ~name ~kind const
+ in
+ let cst, eff = Impargs.with_implicit_protection cst () in
+ let inst = match const.proof_entry_universes with
+ | Entries.Monomorphic_entry _ -> EConstr.EInstance.empty
+ | Entries.Polymorphic_entry (_, ctx) ->
+ (* We mimic what the kernel does, that is ensuring that no additional
+ constraints appear in the body of polymorphic constants. Ideally this
+ should be enforced statically. *)
+ let (_, body_uctx), _ = Future.force const.proof_entry_body in
+ let () = assert (Univ.ContextSet.is_empty body_uctx) in
+ EConstr.EInstance.make (Univ.UContext.instance ctx)
+ in
+ let args = List.map EConstr.of_constr args in
+ let lem = EConstr.mkConstU (cst, inst) in
+ let effs = Evd.concat_side_effects eff effs in
+ effs, sigma, lem, args, safe
+
+let get_goal_context pf i =
+ let p = get_proof pf in
+ Proof.get_goal_context_gen p i
+
+let get_current_goal_context pf =
+ let p = get_proof pf in
+ try Proof.get_goal_context_gen p 1
+ with
+ | Proof.NoSuchGoal _ ->
+ (* spiwack: returning empty evar_map, since if there is no goal,
+ under focus, there is no accessible evar either. EJGA: this
+ seems strange, as we have pf *)
+ let env = Global.env () in
+ Evd.from_env env, env
+
+let get_current_context pf =
+ let p = get_proof pf in
+ Proof.get_proof_context p
+
+module Proof = struct
+ type nonrec t = t
+ let get_proof = get_proof
+ let get_proof_name = get_proof_name
+ let get_used_variables = get_used_variables
+ let get_universe_decl = get_universe_decl
+ let get_initial_euctx = get_initial_euctx
+ let map_proof = map_proof
+ let map_fold_proof = map_fold_proof
+ let map_fold_proof_endline = map_fold_proof_endline
+ let set_endline_tactic = set_endline_tactic
+ let set_used_variables = set_used_variables
+ let compact = compact_the_proof
+ let update_global_env = update_global_env
+ let get_open_goals = get_open_goals
+end
+
+let declare_definition_scheme ~internal ~univs ~role ~name c =
+ let kind = Decls.(IsDefinition Scheme) in
+ let entry = pure_definition_entry ~univs c in
+ let kn, eff = declare_private_constant ~role ~kind ~name entry in
+ let () = if internal then () else definition_message name in
+ kn, eff
+
+let _ = Ind_tables.declare_definition_scheme := declare_definition_scheme
+let _ = Abstract.declare_abstract := declare_abstract
+
+let declare_universe_context = DeclareUctx.declare_universe_context
diff --git a/vernac/declare.mli b/vernac/declare.mli
new file mode 100644
index 0000000000..e23e148ddc
--- /dev/null
+++ b/vernac/declare.mli
@@ -0,0 +1,284 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Names
+open Constr
+open Entries
+
+(** This module provides the official functions to declare new
+ variables, parameters, constants and inductive types in the global
+ environment. It also updates some accesory tables such as [Nametab]
+ (name resolution), [Impargs], and [Notations]. *)
+
+(** We provide two kind of fuctions:
+
+ - one go functions, that will register a constant in one go, suited
+ for non-interactive definitions where the term is given.
+
+ - two-phase [start/declare] functions which will create an
+ interactive proof, allow its modification, and saving when
+ complete.
+
+ Internally, these functions mainly differ in that usually, the first
+ case doesn't require setting up the tactic engine.
+
+ *)
+
+(** [Declare.Proof.t] Construction of constants using interactive proofs. *)
+module Proof : sig
+
+ type t
+
+ (** XXX: These are internal and will go away from publis API once
+ lemmas is merged here *)
+ val get_proof : t -> Proof.t
+ val get_proof_name : t -> Names.Id.t
+
+ (** XXX: These 3 are only used in lemmas *)
+ val get_used_variables : t -> Names.Id.Set.t option
+ val get_universe_decl : t -> UState.universe_decl
+ val get_initial_euctx : t -> UState.t
+
+ val map_proof : (Proof.t -> Proof.t) -> t -> t
+ val map_fold_proof : (Proof.t -> Proof.t * 'a) -> t -> t * 'a
+ val map_fold_proof_endline : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a
+
+ (** Sets the tactic to be used when a tactic line is closed with [...] *)
+ val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
+
+ (** Sets the section variables assumed by the proof, returns its closure
+ * (w.r.t. type dependencies and let-ins covered by it) *)
+ val set_used_variables : t ->
+ Names.Id.t list -> Constr.named_context * t
+
+ val compact : t -> t
+
+ (** Update the proofs global environment after a side-effecting command
+ (e.g. a sublemma definition) has been run inside it. Assumes
+ there_are_pending_proofs. *)
+ val update_global_env : t -> t
+
+ val get_open_goals : t -> int
+
+end
+
+type opacity_flag = Opaque | Transparent
+
+(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of
+ name [name] with goals [goals] (a list of pairs of environment and
+ conclusion); [poly] determines if the proof is universe
+ polymorphic. The proof is started in the evar map [sigma] (which
+ can typically contain universe constraints), and with universe
+ bindings [udecl]. *)
+val start_proof
+ : name:Names.Id.t
+ -> udecl:UState.universe_decl
+ -> poly:bool
+ -> Evd.evar_map
+ -> (Environ.env * EConstr.types) list
+ -> Proof.t
+
+(** Like [start_proof] except that there may be dependencies between
+ initial goals. *)
+val start_dependent_proof
+ : name:Names.Id.t
+ -> udecl:UState.universe_decl
+ -> poly:bool
+ -> Proofview.telescope
+ -> Proof.t
+
+(** Proof entries represent a proof that has been finished, but still
+ not registered with the kernel.
+
+ XXX: Scheduled for removal from public API, don't rely on it *)
+type 'a proof_entry = private {
+ proof_entry_body : 'a Entries.const_entry_body;
+ (* List of section variables *)
+ proof_entry_secctx : Id.Set.t option;
+ (* State id on which the completion of type checking is reported *)
+ proof_entry_feedback : Stateid.t option;
+ proof_entry_type : Constr.types option;
+ proof_entry_universes : Entries.universes_entry;
+ proof_entry_opaque : bool;
+ proof_entry_inline_code : bool;
+}
+
+(** XXX: Scheduled for removal from public API, don't rely on it *)
+type proof_object = private
+ { name : Names.Id.t
+ (** name of the proof *)
+ ; entries : Evd.side_effects proof_entry list
+ (** list of the proof terms (in a form suitable for definitions). *)
+ ; uctx: UState.t
+ (** universe state *)
+ }
+
+val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Proof.t -> proof_object
+
+(** Declaration of local constructions (Variable/Hypothesis/Local) *)
+
+(** XXX: Scheduled for removal from public API, don't rely on it *)
+type variable_declaration =
+ | SectionLocalDef of Evd.side_effects proof_entry
+ | SectionLocalAssum of { typ:types; impl:Glob_term.binding_kind; }
+
+(** XXX: Scheduled for removal from public API, don't rely on it *)
+type 'a constant_entry =
+ | DefinitionEntry of 'a proof_entry
+ | ParameterEntry of parameter_entry
+ | PrimitiveEntry of primitive_entry
+
+val declare_variable
+ : name:variable
+ -> kind:Decls.logical_kind
+ -> variable_declaration
+ -> unit
+
+(** Declaration of global constructions
+ i.e. Definition/Theorem/Axiom/Parameter/...
+
+ XXX: Scheduled for removal from public API, use `DeclareDef` instead *)
+val definition_entry
+ : ?fix_exn:Future.fix_exn
+ -> ?opaque:bool
+ -> ?inline:bool
+ -> ?feedback_id:Stateid.t
+ -> ?section_vars:Id.Set.t
+ -> ?types:types
+ -> ?univs:Entries.universes_entry
+ -> ?eff:Evd.side_effects
+ -> ?univsbody:Univ.ContextSet.t
+ (** Universe-constraints attached to the body-only, used in
+ vio-delayed opaque constants and private poly universes *)
+ -> constr
+ -> Evd.side_effects proof_entry
+
+type import_status = ImportDefaultBehavior | ImportNeedQualified
+
+(** [declare_constant id cd] declares a global declaration
+ (constant/parameter) with name [id] in the current section; it returns
+ the full path of the declaration
+
+ internal specify if the constant has been created by the kernel or by the
+ user, and in the former case, if its errors should be silent
+
+ XXX: Scheduled for removal from public API, use `DeclareDef` instead *)
+val declare_constant
+ : ?local:import_status
+ -> name:Id.t
+ -> kind:Decls.logical_kind
+ -> Evd.side_effects constant_entry
+ -> Constant.t
+
+(** [inline_private_constants ~sideff ~uctx env ce] will inline the
+ constants in [ce]'s body and return the body plus the updated
+ [UState.t].
+
+ XXX: Scheduled for removal from public API, don't rely on it *)
+val inline_private_constants
+ : uctx:UState.t
+ -> Environ.env
+ -> Evd.side_effects proof_entry
+ -> Constr.t * UState.t
+
+(** Declaration messages *)
+
+(** XXX: Scheduled for removal from public API, do not use *)
+val definition_message : Id.t -> unit
+val assumption_message : Id.t -> unit
+val fixpoint_message : int array option -> Id.t list -> unit
+val recursive_message : bool (** true = fixpoint *) ->
+ int array option -> Id.t list -> unit
+
+val check_exists : Id.t -> unit
+
+(* Used outside this module only in indschemes *)
+exception AlreadyDeclared of (string option * Id.t)
+
+(** {6 For legacy support, do not use} *)
+
+module Internal : sig
+
+ val map_entry_body : f:('a Entries.proof_output -> 'b Entries.proof_output) -> 'a proof_entry -> 'b proof_entry
+ val map_entry_type : f:(Constr.t option -> Constr.t option) -> 'a proof_entry -> 'a proof_entry
+ (* Overriding opacity is indeed really hacky *)
+ val set_opacity : opaque:bool -> 'a proof_entry -> 'a proof_entry
+
+ (* TODO: This is only used in DeclareDef to forward the fix to
+ hooks, should eventually go away *)
+ val get_fix_exn : 'a proof_entry -> Future.fix_exn
+
+ val shrink_entry : EConstr.named_context -> 'a proof_entry -> 'a proof_entry * Constr.constr list
+
+ type constant_obj
+
+ val objConstant : constant_obj Libobject.Dyn.tag
+ val objVariable : unit Libobject.Dyn.tag
+
+end
+
+(* Intermediate step necessary to delegate the future.
+ * Both access the current proof state. The former is supposed to be
+ * chained with a computation that completed the proof *)
+type closed_proof_output
+
+(** Requires a complete proof. *)
+val return_proof : Proof.t -> closed_proof_output
+
+(** An incomplete proof is allowed (no error), and a warn is given if
+ the proof is complete. *)
+val return_partial_proof : Proof.t -> closed_proof_output
+val close_future_proof : feedback_id:Stateid.t -> Proof.t -> closed_proof_output Future.computation -> proof_object
+
+(** [by tac] applies tactic [tac] to the 1st subgoal of the current
+ focused proof.
+ Returns [false] if an unsafe tactic has been used. *)
+val by : unit Proofview.tactic -> Proof.t -> Proof.t * bool
+
+val build_by_tactic
+ : ?side_eff:bool
+ -> Environ.env
+ -> uctx:UState.t
+ -> poly:bool
+ -> typ:EConstr.types
+ -> unit Proofview.tactic
+ -> Constr.constr * Constr.types option * bool * UState.t
+
+(** {6 Helpers to obtain proof state when in an interactive proof } *)
+
+(** [get_goal_context n] returns the context of the [n]th subgoal of
+ the current focused proof or raises a [UserError] if there is no
+ focused proof or if there is no more subgoals *)
+
+val get_goal_context : Proof.t -> int -> Evd.evar_map * Environ.env
+
+(** [get_current_goal_context ()] works as [get_goal_context 1] *)
+val get_current_goal_context : Proof.t -> Evd.evar_map * Environ.env
+
+(** [get_current_context ()] returns the context of the
+ current focused goal. If there is no focused goal but there
+ is a proof in progress, it returns the corresponding evar_map.
+ If there is no pending proof then it returns the current global
+ environment and empty evar_map. *)
+val get_current_context : Proof.t -> Evd.evar_map * Environ.env
+
+(** Temporarily re-exported for 3rd party code; don't use *)
+val build_constant_by_tactic :
+ name:Names.Id.t ->
+ ?opaque:opacity_flag ->
+ uctx:UState.t ->
+ sign:Environ.named_context_val ->
+ poly:bool ->
+ EConstr.types ->
+ unit Proofview.tactic ->
+ Evd.side_effects proof_entry * bool * UState.t
+
+val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
+[@@ocaml.deprecated "Use DeclareUctx.declare_universe_context"]
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 601e7e060c..1809c2bc91 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -112,7 +112,7 @@ let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~re
declare_entry ~name ~scope ~kind ~impargs ~uctx entry)
fixitems fixdecls
in
- let isfix = Option.is_empty possible_indexes in
+ let isfix = Option.has_some possible_indexes in
let fixnames = List.map (fun { Recthm.name } -> name) fixitems in
Declare.recursive_message isfix indexes fixnames;
List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml
index 20fa43c8e7..89f3503f4d 100644
--- a/vernac/declareUniv.ml
+++ b/vernac/declareUniv.ml
@@ -94,7 +94,7 @@ let do_universe ~poly l =
in
let src = if poly then BoundUniv else UnqualifiedUniv in
let () = Lib.add_anonymous_leaf (input_univ_names (src, l)) in
- Declare.declare_universe_context ~poly ctx
+ DeclareUctx.declare_universe_context ~poly ctx
let do_constraint ~poly l =
let open Univ in
@@ -107,4 +107,4 @@ let do_constraint ~poly l =
Constraint.empty l
in
let uctx = ContextSet.add_constraints constraints ContextSet.empty in
- Declare.declare_universe_context ~poly uctx
+ DeclareUctx.declare_universe_context ~poly uctx
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index 058fa691ee..e84fce5504 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -14,6 +14,7 @@ open Glob_term
open Constrexpr
open Vernacexpr
open Hints
+open ComHints
open Pcoq
open Pcoq.Prim
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 08ba49f92b..13145d3757 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -938,23 +938,23 @@ GRAMMAR EXTEND Gram
| IDENT "Print"; IDENT "Table"; table = option_table ->
{ VernacPrintOption table }
- | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 option_ref_value
+ | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 table_value
-> { VernacAddOption ([table;field], v) }
(* A global value below will be hidden by a field above! *)
(* In fact, we give priority to secondary tables *)
(* No syntax for tertiary tables due to conflict *)
(* (but they are unused anyway) *)
- | IDENT "Add"; table = IDENT; v = LIST1 option_ref_value ->
+ | IDENT "Add"; table = IDENT; v = LIST1 table_value ->
{ VernacAddOption ([table], v) }
- | IDENT "Test"; table = option_table; "for"; v = LIST1 option_ref_value
+ | IDENT "Test"; table = option_table; "for"; v = LIST1 table_value
-> { VernacMemOption (table, v) }
| IDENT "Test"; table = option_table ->
{ VernacPrintOption table }
- | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value
+ | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 table_value
-> { VernacRemoveOption ([table;field], v) }
- | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value ->
+ | IDENT "Remove"; table = IDENT; v = LIST1 table_value ->
{ VernacRemoveOption ([table], v) } ]]
;
query_command: (* TODO: rapprocher Eval et Check *)
@@ -1047,9 +1047,9 @@ GRAMMAR EXTEND Gram
| n = integer -> { OptionSetInt n }
| s = STRING -> { OptionSetString s } ] ]
;
- option_ref_value:
- [ [ id = global -> { QualidRefValue id }
- | s = STRING -> { StringRefValue s } ] ]
+ table_value:
+ [ [ id = global -> { Goptions.QualidRefValue id }
+ | s = STRING -> { Goptions.StringRefValue s } ] ]
;
option_table:
[ [ fl = LIST1 [ x = IDENT -> { x } ] -> { fl } ]]
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 5555a2c68e..fddc84b398 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -57,16 +57,16 @@ let contract3 env sigma a b c = match contract env sigma [a;b;c] with
let contract4 env sigma a b c d = match contract env sigma [a;b;c;d] with
| env, [a;b;c;d] -> (env,a,b,c),d | _ -> assert false
-let contract1_vect env sigma a v =
- match contract env sigma (a :: Array.to_list v) with
- | env, a::l -> env,a,Array.of_list l
+let contract1 env sigma a v =
+ match contract env sigma (a :: v) with
+ | env, a::l -> env,a,l
| _ -> assert false
let rec contract3' env sigma a b c = function
| OccurCheck (evk,d) ->
let x,d = contract4 env sigma a b c d in x,OccurCheck(evk, d)
| NotClean ((evk,args),env',d) ->
- let env',d,args = contract1_vect env' sigma d args in
+ let env',d,args = contract1 env' sigma d args in
contract3 env sigma a b c,NotClean((evk,args),env',d)
| ConversionFailed (env',t1,t2) ->
let (env',t1,t2) = contract2 env' sigma t1 t2 in
@@ -299,9 +299,9 @@ let explain_unification_error env sigma p1 p2 = function
[str "cannot instantiate " ++ quote (pr_existential_key sigma evk)
++ strbrk " because " ++ pr_leconstr_env env sigma c ++
strbrk " is not in its scope" ++
- (if Array.is_empty args then mt() else
+ (if List.is_empty args then mt() else
strbrk ": available arguments are " ++
- pr_sequence (pr_leconstr_env env sigma) (List.rev (Array.to_list args)))]
+ pr_sequence (pr_leconstr_env env sigma) (List.rev args))]
| NotSameArgSize | NotSameHead | NoCanonicalStructure ->
(* Error speaks from itself *) []
| ConversionFailed (env,t1,t2) ->
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 7260b13ff6..6ffa88874b 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -91,12 +91,11 @@ let () =
optwrite = (fun b -> rewriting_flag := b) }
(* Util *)
-
let define ~poly name sigma c types =
- let f = declare_constant ~kind:Decls.(IsDefinition Scheme) in
let univs = Evd.univ_entry ~poly sigma in
let entry = Declare.definition_entry ~univs ?types c in
- let kn = f ~name (DefinitionEntry entry) in
+ let kind = Decls.(IsDefinition Scheme) in
+ let kn = declare_constant ~kind ~name (DefinitionEntry entry) in
definition_message name;
kn
diff --git a/vernac/library.ml b/vernac/library.ml
index 01f5101764..35b2a18871 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -20,11 +20,11 @@ open Libobject
(*s Low-level interning/externing of libraries to files *)
let raw_extern_library f =
- System.raw_extern_state Coq_config.vo_magic_number f
+ ObjFile.open_out ~file:f
let raw_intern_library f =
System.with_magic_number_check
- (System.raw_intern_state Coq_config.vo_magic_number) f
+ (fun file -> ObjFile.open_in ~file) f
(************************************************************************)
(** Serialized objects loaded on-the-fly *)
@@ -35,7 +35,7 @@ module Delayed :
sig
type 'a delayed
-val in_delayed : string -> in_channel -> 'a delayed * Digest.t
+val in_delayed : string -> ObjFile.in_handle -> segment:string -> 'a delayed * Digest.t
val fetch_delayed : 'a delayed -> 'a
end =
@@ -43,14 +43,14 @@ struct
type 'a delayed = {
del_file : string;
- del_off : int;
+ del_off : int64;
del_digest : Digest.t;
}
-let in_delayed f ch =
- let pos = pos_in ch in
- let _, digest = System.skip_in_segment f ch in
- ({ del_file = f; del_digest = digest; del_off = pos; }, digest)
+let in_delayed f ch ~segment =
+ let seg = ObjFile.get_segment ch ~segment in
+ let digest = seg.ObjFile.hash in
+ { del_file = f; del_digest = digest; del_off = seg.ObjFile.pos; }, digest
(** Fetching a table of opaque terms at position [pos] in file [f],
expecting to find first a copy of [digest]. *)
@@ -58,10 +58,10 @@ let in_delayed f ch =
let fetch_delayed del =
let { del_digest = digest; del_file = f; del_off = pos; } = del in
try
- let ch = raw_intern_library f in
- let () = seek_in ch pos in
- let obj, _, digest' = System.marshal_in_segment f ch in
- let () = close_in ch in
+ let ch = open_in_bin f in
+ let () = LargeFile.seek_in ch pos in
+ let obj = System.marshal_in f ch in
+ let digest' = Digest.input ch in
if not (String.equal digest digest') then raise (Faulty f);
obj
with e when CErrors.noncritical e -> raise (Faulty f)
@@ -242,12 +242,11 @@ let mk_summary m = {
let intern_from_file f =
let ch = raw_intern_library f in
- let (lsd : seg_sum), _, digest_lsd = System.marshal_in_segment f ch in
- let ((lmd : seg_lib delayed), digest_lmd) = in_delayed f ch in
- let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in
- let _ = System.skip_in_segment f ch in
- let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch in
- close_in ch;
+ let (lsd : seg_sum), digest_lsd = ObjFile.marshal_in_segment ch ~segment:"summary" in
+ let ((lmd : seg_lib delayed), digest_lmd) = in_delayed f ch ~segment:"library" in
+ let (univs : seg_univ option), digest_u = ObjFile.marshal_in_segment ch ~segment:"universes" in
+ let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch ~segment:"opaques" in
+ ObjFile.close_in ch;
register_library_filename lsd.md_name f;
add_opaque_table lsd.md_name (ToFetch del_opaque);
let open Safe_typing in
@@ -297,7 +296,7 @@ let rec_intern_library ~lib_resolver libs (dir, f) =
let native_name_from_filename f =
let ch = raw_intern_library f in
- let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in
+ let (lmd : seg_sum), digest_lmd = ObjFile.marshal_in_segment ch ~segment:"summary" in
Nativecode.mod_uid_of_dirpath lmd.md_name
(**********************************************************************)
@@ -392,12 +391,12 @@ let require_library_from_dirpath ~lib_resolver modrefl export =
let load_library_todo f =
let ch = raw_intern_library f in
- let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in
- let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in
- let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in
- let tasks, _, _ = System.marshal_in_segment f ch in
- let (s4 : seg_proofs), _, _ = System.marshal_in_segment f ch in
- close_in ch;
+ let (s0 : seg_sum), _ = ObjFile.marshal_in_segment ch ~segment:"summary" in
+ let (s1 : seg_lib), _ = ObjFile.marshal_in_segment ch ~segment:"library" in
+ let (s2 : seg_univ option), _ = ObjFile.marshal_in_segment ch ~segment:"universes" in
+ let tasks, _ = ObjFile.marshal_in_segment ch ~segment:"tasks" in
+ let (s4 : seg_proofs), _ = ObjFile.marshal_in_segment ch ~segment:"opaques" in
+ ObjFile.close_in ch;
if tasks = None then user_err ~hdr:"restart" (str"not a .vio file");
if s2 = None then user_err ~hdr:"restart" (str"not a .vio file");
if snd (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");
@@ -433,15 +432,15 @@ let error_recursively_dependent_library dir =
let save_library_base f sum lib univs tasks proofs =
let ch = raw_extern_library f in
try
- System.marshal_out_segment f ch (sum : seg_sum);
- System.marshal_out_segment f ch (lib : seg_lib);
- System.marshal_out_segment f ch (univs : seg_univ option);
- System.marshal_out_segment f ch (tasks : 'tasks option);
- System.marshal_out_segment f ch (proofs : seg_proofs);
- close_out ch
+ ObjFile.marshal_out_segment ch ~segment:"summary" (sum : seg_sum);
+ ObjFile.marshal_out_segment ch ~segment:"library" (lib : seg_lib);
+ ObjFile.marshal_out_segment ch ~segment:"universes" (univs : seg_univ option);
+ ObjFile.marshal_out_segment ch ~segment:"tasks" (tasks : 'tasks option);
+ ObjFile.marshal_out_segment ch ~segment:"opaques" (proofs : seg_proofs);
+ ObjFile.close_out ch
with reraise ->
let reraise = Exninfo.capture reraise in
- close_out ch;
+ ObjFile.close_out ch;
Feedback.msg_warning (str "Removed file " ++ str f);
Sys.remove f;
Exninfo.iraise reraise
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 7a2e6d8b03..f1aae239aa 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -168,8 +168,8 @@ open Pputils
keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search sl ++ pr_in_out_modules b
let pr_option_ref_value = function
- | QualidRefValue id -> pr_qualid id
- | StringRefValue s -> qs s
+ | Goptions.QualidRefValue id -> pr_qualid id
+ | Goptions.StringRefValue s -> qs s
let pr_printoption table b =
prlist_with_sep spc str table ++
@@ -185,7 +185,7 @@ open Pputils
| [] -> mt()
| _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z
- let pr_reference_or_constr pr_c = let open Hints in function
+ let pr_reference_or_constr pr_c = let open ComHints in function
| HintsReference r -> pr_qualid r
| HintsConstr c -> pr_c c
@@ -202,6 +202,7 @@ open Pputils
let opth = pr_opt_hintbases db in
let pph =
let open Hints in
+ let open ComHints in
match h with
| HintsResolve l ->
keyword "Resolve " ++ prlist_with_sep sep
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index 4de12f5e3b..2b6beaf2e3 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -28,7 +28,7 @@ module Vernac_ :
val command_entry : vernac_expr Entry.t
val main_entry : vernac_control option Entry.t
val red_expr : raw_red_expr Entry.t
- val hint_info : Hints.hint_info_expr Entry.t
+ val hint_info : ComHints.hint_info_expr Entry.t
end
(* To be removed when the parser is made functional wrt the tactic
diff --git a/vernac/retrieveObl.ml b/vernac/retrieveObl.ml
index c529972b8d..b8564037e0 100644
--- a/vernac/retrieveObl.ml
+++ b/vernac/retrieveObl.ml
@@ -72,7 +72,7 @@ let subst_evar_constr evm evs n idf t =
*)
let args =
let n = match chop with None -> 0 | Some c -> c in
- let l, r = CList.chop n (List.rev (Array.to_list args)) in
+ let l, r = CList.chop n (List.rev args) in
List.rev r
in
let args =
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index b7728fe699..6d5d16d94a 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -9,6 +9,8 @@ Himsg
Locality
Egramml
Vernacextend
+Declare
+ComHints
Ppvernac
Proof_using
Egramcoq
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 044e479aeb..df39c617d3 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1275,7 +1275,7 @@ let vernac_hints ~atts dbnames h =
"This command does not support the export attribute in sections.");
| OptDefault | OptLocal -> ()
in
- Hints.add_hints ~locality dbnames (Hints.interp_hints ~poly h)
+ Hints.add_hints ~locality dbnames (ComHints.interp_hints ~poly h)
let vernac_syntactic_definition ~atts lid x only_parsing =
let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in
@@ -1302,6 +1302,7 @@ let vernac_generalizable ~local =
Implicit_quantifiers.declare_generalizable ~local
let allow_sprop_opt_name = ["Allow";"StrictProp"]
+let cumul_sprop_opt_name = ["Cumulative";"StrictProp"]
let () =
declare_bool_option
@@ -1313,6 +1314,13 @@ let () =
let () =
declare_bool_option
{ optdepr = false;
+ optkey = cumul_sprop_opt_name;
+ optread = Global.is_cumulative_sprop;
+ optwrite = Global.set_cumulative_sprop }
+
+let () =
+ declare_bool_option
+ { optdepr = false;
optkey = ["Silent"];
optread = (fun () -> !Flags.quiet);
optwrite = ((:=) Flags.quiet) }
@@ -1487,21 +1495,21 @@ let () =
optread = CWarnings.get_flags;
optwrite = CWarnings.set_flags }
-let _ =
+let () =
declare_bool_option
{ optdepr = false;
optkey = ["Guard"; "Checking"];
optread = (fun () -> (Global.typing_flags ()).Declarations.check_guarded);
optwrite = (fun b -> Global.set_check_guarded b) }
-let _ =
+let () =
declare_bool_option
{ optdepr = false;
optkey = ["Positivity"; "Checking"];
optread = (fun () -> (Global.typing_flags ()).Declarations.check_positive);
optwrite = (fun b -> Global.set_check_positive b) }
-let _ =
+let () =
declare_bool_option
{ optdepr = false;
optkey = ["Universe"; "Checking"];
@@ -1554,26 +1562,11 @@ let vernac_set_option ~locality table v = match v with
vernac_set_option0 ~locality table v
| _ -> vernac_set_option0 ~locality table v
-let vernac_add_option key lv =
- let f = function
- | StringRefValue s -> (get_string_table key).add (Global.env()) s
- | QualidRefValue locqid -> (get_ref_table key).add (Global.env()) locqid
- in
- try List.iter f lv with Not_found -> error_undeclared_key key
+let vernac_add_option = iter_table { aux = fun table -> table.add }
-let vernac_remove_option key lv =
- let f = function
- | StringRefValue s -> (get_string_table key).remove (Global.env()) s
- | QualidRefValue locqid -> (get_ref_table key).remove (Global.env()) locqid
- in
- try List.iter f lv with Not_found -> error_undeclared_key key
+let vernac_remove_option = iter_table { aux = fun table -> table.remove }
-let vernac_mem_option key lv =
- let f = function
- | StringRefValue s -> (get_string_table key).mem (Global.env()) s
- | QualidRefValue locqid -> (get_ref_table key).mem (Global.env()) locqid
- in
- try List.iter f lv with Not_found -> error_undeclared_key key
+let vernac_mem_option = iter_table { aux = fun table -> table.mem }
let vernac_print_option key =
try (get_ref_table key).print ()
@@ -1734,7 +1727,8 @@ let vernac_print ~pstate ~atts =
| PrintHintGoal ->
begin match pstate with
| Some pstate ->
- Hints.pr_applicable_hint pstate
+ let pf = Declare.Proof.get_proof pstate in
+ Hints.pr_applicable_hint pf
| None ->
str "No proof in progress"
end
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 2ac8458ad5..cf233248d7 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -26,3 +26,4 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr
val command_focus : unit Proof.focus_kind
val allow_sprop_opt_name : string list
+val cumul_sprop_opt_name : string list
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index c32ac414ba..b65a0da1cc 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -121,10 +121,6 @@ type option_setting =
| OptionSetInt of int
| OptionSetString of string
-type option_ref_value =
- | StringRefValue of string
- | QualidRefValue of qualid
-
(** Identifier and optional list of bound universes and constraints. *)
type sort_expr = Sorts.family
@@ -340,18 +336,18 @@ type nonrec vernac_expr =
local_binder_expr list * (* binders *)
constr_expr * (* type *)
(bool * constr_expr) option * (* body (bool=true when using {}) *)
- Hints.hint_info_expr
+ ComHints.hint_info_expr
| VernacDeclareInstance of
ident_decl * (* name *)
local_binder_expr list * (* binders *)
constr_expr * (* type *)
- Hints.hint_info_expr
+ ComHints.hint_info_expr
| VernacContext of local_binder_expr list
| VernacExistingInstance of
- (qualid * Hints.hint_info_expr) list (* instances names, priorities and patterns *)
+ (qualid * ComHints.hint_info_expr) list (* instances names, priorities and patterns *)
| VernacExistingClass of qualid (* inductive or definition name *)
@@ -391,7 +387,7 @@ type nonrec vernac_expr =
(* Commands *)
| VernacCreateHintDb of string * bool
| VernacRemoveHints of string list * qualid list
- | VernacHints of string list * Hints.hints_expr
+ | VernacHints of string list * ComHints.hints_expr
| VernacSyntacticDefinition of
lident * (Id.t list * constr_expr) *
onlyparsing_flag
@@ -406,9 +402,9 @@ type nonrec vernac_expr =
| VernacSetStrategy of
(Conv_oracle.level * qualid or_by_notation list) list
| VernacSetOption of bool (* Export modifier? *) * Goptions.option_name * option_setting
- | VernacAddOption of Goptions.option_name * option_ref_value list
- | VernacRemoveOption of Goptions.option_name * option_ref_value list
- | VernacMemOption of Goptions.option_name * option_ref_value list
+ | VernacAddOption of Goptions.option_name * Goptions.table_value list
+ | VernacRemoveOption of Goptions.option_name * Goptions.table_value list
+ | VernacMemOption of Goptions.option_name * Goptions.table_value list
| VernacPrintOption of Goptions.option_name
| VernacCheckMayEval of Genredexpr.raw_red_expr option * Goal_select.t option * constr_expr
| VernacGlobalCheck of constr_expr
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 00:47:17 +0000