aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/class.ml4
-rw-r--r--vernac/classes.ml10
-rw-r--r--vernac/comAssumption.ml6
-rw-r--r--vernac/comDefinition.ml40
-rw-r--r--vernac/comProgramFixpoint.ml8
-rw-r--r--vernac/declareDef.ml14
-rw-r--r--vernac/declareDef.mli28
-rw-r--r--vernac/g_vernac.mlg7
-rw-r--r--vernac/lemmas.ml56
-rw-r--r--vernac/lemmas.mli38
-rw-r--r--vernac/obligations.ml60
-rw-r--r--vernac/obligations.mli29
-rw-r--r--vernac/ppvernac.ml6
-rw-r--r--vernac/record.ml4
-rw-r--r--vernac/vernacentries.ml84
-rw-r--r--vernac/vernacentries.mli4
-rw-r--r--vernac/vernacexpr.ml12
17 files changed, 190 insertions, 220 deletions
diff --git a/vernac/class.ml b/vernac/class.ml
index 823177d4d1..a6b3242cae 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -302,7 +302,7 @@ let try_add_new_identity_coercion id ~local poly ~source ~target =
let try_add_new_coercion_with_source ref ~local poly ~source =
try_add_new_coercion_core ref ~local poly (Some source) None false
-let add_coercion_hook poly local ref =
+let add_coercion_hook poly _uctx _trans local ref =
let local = match local with
| Discharge
| Local -> true
@@ -314,7 +314,7 @@ let add_coercion_hook poly local ref =
let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly)
-let add_subclass_hook poly local ref =
+let add_subclass_hook poly _uctx _trans local ref =
let stre = match local with
| Local -> true
| Global -> false
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 27d8b7390d..453b863be6 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -106,7 +106,7 @@ let id_of_class cl =
| _ -> assert false
let instance_hook k info global imps ?hook cst =
- Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps;
+ Impargs.maybe_declare_manual_implicits false cst imps;
let info = intern_info info in
Typeclasses.declare_instance (Some info) (not global) cst;
(match hook with Some h -> h cst | None -> ())
@@ -149,7 +149,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
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 ~enriching:false [imps];
+ Impargs.declare_manual_implicits false gr imps;
let pri = intern_info pri in
Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst)
in
@@ -161,10 +161,10 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
in obls, Some constr, typ
| None -> [||], None, termtype
in
- let univ_hook = Obligations.mk_univ_hook hook in
+ let hook = Lemmas.mk_hook hook in
let ctx = Evd.evar_universe_context sigma in
ignore (Obligations.add_definition id ?term:constr
- ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~univ_hook obls)
+ ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls)
else
Flags.silently (fun () ->
(* spiwack: it is hard to reorder the actions to do
@@ -175,7 +175,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
let sigma = Evd.reset_future_goals sigma in
Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype)
~hook:(Lemmas.mk_hook
- (fun _ -> instance_hook k pri global imps ?hook));
+ (fun _ _ _ -> instance_hook k pri global imps ?hook));
(* spiwack: I don't know what to do with the status here. *)
if not (Option.is_empty term) then
let init_refine =
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 466757c6bd..35d8be5c56 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -8,7 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Pp
open CErrors
open Util
open Vars
@@ -54,10 +53,11 @@ match local with
let () = assumption_message ident in
let () =
if not !Flags.quiet && Proof_global.there_are_pending_proofs () then
- Feedback.msg_info (str"Variable" ++ spc () ++ Id.print ident ++
+ Feedback.msg_info Pp.(str"Variable" ++ spc () ++ Id.print ident ++
strbrk " is not visible from current goals")
in
let r = VarRef ident in
+ let () = maybe_declare_manual_implicits true r imps in
let () = Typeclasses.declare_instance None true r in
let () = if is_coe then Class.try_add_new_coercion r ~local:true false in
(r,Univ.Instance.empty,true)
@@ -203,4 +203,4 @@ let do_primitive id prim typopt =
}
in
let _kn = declare_constant id.CAst.v (PrimitiveEntry entry,IsPrimitive) in
- register_message id.CAst.v
+ Flags.if_verbose Feedback.msg_info Pp.(Id.print id.CAst.v ++ str " is declared")
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 5eb19eef54..28773a3965 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -94,22 +94,24 @@ let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
let (ce, evd, univdecl, imps as def) =
interp_definition ~program_mode univdecl bl (pi2 k) 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);
- assert(Univ.ContextSet.is_empty ctx);
- let typ = match ce.const_entry_type with
- | Some t -> t
- | None -> EConstr.to_constr ~abort_on_undefined_evars:false evd (Retyping.get_type_of env evd (EConstr.of_constr c))
- in
- Obligations.check_evars env evd;
- let obls, _, c, cty =
- Obligations.eterm_obligations env ident evd 0 c typ
- in
- let ctx = Evd.evar_universe_context evd in
- let univ_hook = Obligations.mk_univ_hook (fun _ _ l r -> Lemmas.call_hook ?hook l r) in
- ignore(Obligations.add_definition
- ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~univ_hook obls)
- else let ce = check_definition ~program_mode def in
- ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps ?hook)
+ 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);
+ assert(Univ.ContextSet.is_empty ctx);
+ let typ = match ce.const_entry_type with
+ | Some t -> t
+ | None -> EConstr.to_constr ~abort_on_undefined_evars:false evd (Retyping.get_type_of env evd (EConstr.of_constr c))
+ in
+ Obligations.check_evars env evd;
+ let obls, _, c, cty =
+ Obligations.eterm_obligations env ident evd 0 c typ
+ in
+ let ctx = Evd.evar_universe_context evd in
+ ignore(Obligations.add_definition
+ ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ?hook obls)
+ else
+ let ce = check_definition ~program_mode def in
+ let uctx = Evd.evar_universe_context evd in
+ let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
+ ignore(DeclareDef.declare_definition ident k ?hook_data ce (Evd.universe_binders evd) imps )
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index a30313d37c..ae77cf12e5 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -215,7 +215,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
let gr = ConstRef c in
if Impargs.is_implicit_args () || not (List.is_empty impls) then
- Impargs.declare_manual_implicits false gr [impls]
+ Impargs.declare_manual_implicits false gr impls
in
let typ = it_mkProd_or_LetIn top_arity binders in
hook, name, typ
@@ -223,11 +223,11 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let typ = it_mkProd_or_LetIn top_arity binders_rel in
let hook sigma _ _ l gr =
if Impargs.is_implicit_args () || not (List.is_empty impls) then
- Impargs.declare_manual_implicits false gr [impls]
+ Impargs.declare_manual_implicits false gr impls
in hook, recname, typ
in
(* XXX: Capturing sigma here... bad bad *)
- let univ_hook = Obligations.mk_univ_hook (hook sigma) in
+ let hook = Lemmas.mk_hook (hook sigma) in
(* XXX: Grounding non-ground terms here... bad bad *)
let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in
let fullctyp = EConstr.to_constr sigma typ in
@@ -237,7 +237,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
in
let ctx = Evd.evar_universe_context sigma in
ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl
- evars_typ ctx evars ~univ_hook)
+ evars_typ ctx evars ~hook)
let out_def = function
| Some def -> def
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 361ed1a737..7dcd098183 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -33,7 +33,7 @@ let get_locality id ~kind = function
| Local -> true
| Global -> false
-let declare_definition ident (local, p, k) ?hook ce pl imps =
+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 gr = match local with
| Discharge when Lib.sections_are_opened () ->
@@ -49,11 +49,17 @@ let declare_definition ident (local, p, k) ?hook ce pl imps =
in
let () = maybe_declare_manual_implicits false gr imps in
let () = definition_message ident in
- Lemmas.call_hook ~fix_exn ?hook local gr; gr
+ begin
+ match hook_data with
+ | None -> ()
+ | Some (hook, uctx, extra_defs) ->
+ Lemmas.call_hook ~fix_exn ~hook uctx extra_defs local gr
+ end;
+ gr
-let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
+let declare_fix ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
- declare_definition f kind ce pl imps
+ declare_definition f kind ?hook_data ce pl imps
let check_definition_evars ~allow_evars sigma =
let env = Global.env () in
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index e455b59ab2..3f95ec7107 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -13,16 +13,26 @@ open Decl_kinds
val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool
-val declare_definition : Id.t -> definition_kind ->
- ?hook:Lemmas.declaration_hook ->
- Safe_typing.private_constants Entries.definition_entry -> UnivNames.universe_binders -> Impargs.manual_implicits ->
- GlobRef.t
+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
+ -> UnivNames.universe_binders
+ -> Impargs.manual_implicits
+ -> GlobRef.t
-val declare_fix : ?opaque:bool -> definition_kind ->
- UnivNames.universe_binders -> Entries.universes_entry ->
- Id.t -> Safe_typing.private_constants Entries.proof_output ->
- Constr.types -> Impargs.manual_implicits ->
- GlobRef.t
+val declare_fix
+ : ?opaque:bool
+ -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
+ -> definition_kind
+ -> UnivNames.universe_binders
+ -> Entries.universes_entry
+ -> Id.t
+ -> Safe_typing.private_constants Entries.proof_output
+ -> Constr.types
+ -> Impargs.manual_implicits
+ -> GlobRef.t
val prepare_definition : allow_evars:bool ->
?opaque:bool -> ?inline:bool -> poly:bool ->
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 42bee25da3..589b15fd41 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -16,6 +16,7 @@ open Util
open Names
open Glob_term
open Vernacexpr
+open Impargs
open Constrexpr
open Constrexpr_ops
open Extend
@@ -836,11 +837,11 @@ GRAMMAR EXTEND Gram
];
(* Same as [argument_spec_block], but with only implicit status and names *)
more_implicits_block: [
- [ name = name -> { [(name.CAst.v, Vernacexpr.NotImplicit)] }
+ [ name = name -> { [(name.CAst.v, NotImplicit)] }
| "["; items = LIST1 name; "]" ->
- { List.map (fun name -> (name.CAst.v, Vernacexpr.Implicit)) items }
+ { List.map (fun name -> (name.CAst.v, Impargs.Implicit)) items }
| "{"; items = LIST1 name; "}" ->
- { List.map (fun name -> (name.CAst.v, Vernacexpr.MaximallyImplicit)) items }
+ { List.map (fun name -> (name.CAst.v, MaximallyImplicit)) items }
]
];
strategy_level:
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 83dd1aa8e4..77f125e878 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -34,10 +34,13 @@ open Impargs
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
-type declaration_hook = Decl_kinds.locality -> GlobRef.t -> unit
+type hook_type = UState.t -> (Id.t * Constr.t) list -> Decl_kinds.locality -> GlobRef.t -> unit
+type declaration_hook = hook_type
+
let mk_hook hook = hook
-let call_hook ?hook ?fix_exn l c =
- try Option.iter (fun hook -> hook l c) hook
+
+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
@@ -174,7 +177,7 @@ let look_for_possibly_mutual_statements sigma = function
(* Saving a goal *)
-let save ?export_seff id const uctx do_guard (locality,poly,kind) hook =
+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
@@ -203,7 +206,7 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook =
gr
in
definition_message id;
- call_hook ?hook locality r
+ call_hook ?hook universes [] locality r
with e when CErrors.noncritical e ->
let e = CErrors.push e in
iraise (fix_exn e)
@@ -289,7 +292,7 @@ let warn_let_as_axiom =
(fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++
spc () ++ strbrk "declared as an axiom.")
-let admit ?hook (id,k,e) pl () =
+let admit ?hook ctx (id,k,e) pl () =
let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in
let () = match k with
| Global, _, _ -> ()
@@ -297,16 +300,15 @@ let admit ?hook (id,k,e) pl () =
in
let () = assumption_message id in
Declare.declare_univ_binders (ConstRef kn) pl;
- call_hook ?hook Global (ConstRef kn)
+ call_hook ?hook ctx [] Global (ConstRef kn)
(* Starting a goal *)
-let universe_proof_terminator ?univ_hook compute_guard =
+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 hook = Option.map (fun univ_hook -> univ_hook (Some ctx)) univ_hook in
- admit ?hook (id,k,pe) (UState.universe_binders 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
@@ -317,16 +319,12 @@ let universe_proof_terminator ?univ_hook compute_guard =
let id = match idopt with
| None -> id
| Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in
- let hook = Option.map (fun univ_hook -> univ_hook (Some universes)) univ_hook in
- save ~export_seff id const universes compute_guard persistence hook
+ 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
-let standard_proof_terminator ?hook compute_guard =
- let univ_hook = Option.map (fun hook _ -> hook) hook in
- universe_proof_terminator ?univ_hook compute_guard
-
let initialize_named_context_for_proof () =
let sign = Global.named_context () in
List.fold_right
@@ -335,7 +333,7 @@ let initialize_named_context_for_proof () =
let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in
Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
-let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c =
+let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?(hook : declaration_hook option) c =
let terminator = match terminator with
| None -> standard_proof_terminator ?hook compute_guard
| Some terminator -> terminator ?hook compute_guard
@@ -348,20 +346,6 @@ let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c
let goals = [ Global.env_of_context sign , c ] in
Proof_global.start_proof sigma id ?pl kind goals terminator
-let start_proof_univs id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?univ_hook c =
- let terminator = match terminator with
- | None ->
- universe_proof_terminator ?univ_hook compute_guard
- | Some terminator -> terminator ?univ_hook compute_guard
- in
- let sign =
- match sign with
- | Some sign -> sign
- | None -> initialize_named_context_for_proof ()
- in
- let goals = [ Global.env_of_context sign , c ] in
- Proof_global.start_proof sigma id ?pl kind goals terminator
-
let rec_tac_initializer finite guard thms snl =
if finite then
match List.map (fun (id,(t,_)) -> (id,t)) thms with
@@ -394,11 +378,7 @@ let start_proof_with_initialization ?hook kind sigma decl recguard thms snl =
match thms with
| [] -> anomaly (Pp.str "No proof to start.")
| (id,(t,(_,imps)))::other_thms ->
- let hook ctx strength ref =
- let ctx = match ctx with
- | None -> UState.empty
- | Some ctx -> ctx
- in
+ let hook ctx _ strength ref =
let other_thms_data =
if List.is_empty other_thms then [] else
(* there are several theorems defined mutually *)
@@ -410,8 +390,8 @@ let start_proof_with_initialization ?hook kind sigma decl recguard thms snl =
let thms_data = (strength,ref,imps)::other_thms_data in
List.iter (fun (strength,ref,imps) ->
maybe_declare_manual_implicits false ref imps;
- call_hook ?hook strength ref) thms_data in
- start_proof_univs id ~pl:decl kind sigma t ~univ_hook:(fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard;
+ call_hook ?hook ctx [] strength ref) thms_data in
+ start_proof id ~pl:decl kind sigma t ~hook ~compute_guard:guard;
ignore (Proof_global.with_current_proof (fun _ p ->
match init_tac with
| None -> p,(true,[])
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index a9a10a6e38..72c666e903 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -13,10 +13,29 @@ open Decl_kinds
type declaration_hook
-val mk_hook : (Decl_kinds.locality -> GlobRef.t -> unit) -> declaration_hook
-val call_hook :
- ?hook:declaration_hook -> ?fix_exn:Future.fix_exn ->
- Decl_kinds.locality -> GlobRef.t -> unit
+(* 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 : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) ->
@@ -24,12 +43,6 @@ val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map
?compute_guard:Proof_global.lemma_possible_guards ->
?hook:declaration_hook -> EConstr.types -> unit
-val start_proof_univs : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
- ?terminator:(?univ_hook:(UState.t option -> declaration_hook) -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) ->
- ?sign:Environ.named_context_val ->
- ?compute_guard:Proof_global.lemma_possible_guards ->
- ?univ_hook:(UState.t option -> declaration_hook) -> EConstr.types -> unit
-
val start_proof_com :
program_mode:bool -> ?inference_hook:Pretyping.inference_hook ->
?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list ->
@@ -43,11 +56,6 @@ val start_proof_with_initialization :
(EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list ->
int list option -> unit
-val universe_proof_terminator :
- ?univ_hook:(UState.t option -> declaration_hook) ->
- Proof_global.lemma_possible_guards ->
- Proof_global.proof_terminator
-
val standard_proof_terminator :
?hook:declaration_hook -> Proof_global.lemma_possible_guards ->
Proof_global.proof_terminator
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index ba78c73131..38cdfc2d7a 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -20,15 +20,6 @@ open Pp
open CErrors
open Util
-type univ_declaration_hook = UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit
-let mk_univ_hook f = f
-let call_univ_hook ?univ_hook ?fix_exn uctx trans l c =
- try Option.iter (fun hook -> hook uctx trans l c) univ_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 NamedDecl = Context.Named.Declaration
let get_fix_exn, stm_get_fix_exn = Hook.make ()
@@ -321,7 +312,7 @@ type program_info_aux = {
prg_notations : notations ;
prg_kind : definition_kind;
prg_reduce : constr -> constr;
- prg_hook : univ_declaration_hook option;
+ prg_hook : Lemmas.declaration_hook option;
prg_opaque : bool;
prg_sign: named_context_val;
}
@@ -482,9 +473,9 @@ let declare_definition prg =
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 = Lemmas.mk_hook (fun l r -> call_univ_hook ?univ_hook:prg.prg_hook ~fix_exn uctx obls l r; ()) 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
+ prg.prg_kind ce ubinders prg.prg_implicits ?hook_data
let rec lam_index n t acc =
match Constr.kind t with
@@ -559,14 +550,16 @@ let declare_mutual_definition l =
(* 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
- call_univ_hook ?univ_hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr;
- List.iter progmap_remove l; gr
+ 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
@@ -663,7 +656,7 @@ let declare_obligation prg obl body ty uctx =
in
true, { obl with obl_body = body }
-let init_prog_info ?(opaque = false) ?univ_hook sign n udecl b t ctx deps fixkind
+let init_prog_info ?(opaque = false) ?hook sign n udecl b t ctx deps fixkind
notations obls impls kind reduce =
let obls', b =
match b with
@@ -689,7 +682,7 @@ let init_prog_info ?(opaque = false) ?univ_hook sign n udecl b t ctx deps fixkin
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_hook = univ_hook; prg_opaque = opaque;
+ prg_hook = hook; prg_opaque = opaque;
prg_sign = sign }
let map_cardinal m =
@@ -844,9 +837,9 @@ let solve_by_tac ?loc name evi t poly ctx =
warn_solve_errored ?loc err;
None
-let obligation_terminator ?univ_hook name num guard auto pf =
+let obligation_terminator ?hook name num guard auto pf =
let open Proof_global in
- let term = Lemmas.universe_proof_terminator ?univ_hook guard 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
@@ -912,7 +905,7 @@ let obligation_terminator ?univ_hook name num guard auto pf =
| 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 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
@@ -922,7 +915,6 @@ let obligation_hook prg obl num auto ctx' _ gr =
if not transparent then err_not_transp ()
| _ -> ()
in
- let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in
let inst, ctx' =
if not (pi2 prg.prg_kind) (* Not polymorphic *) then
(* The universe context was declared globally, we continue
@@ -969,11 +961,11 @@ let rec solve_obligation prg num tac =
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 ?univ_hook guard =
+ let terminator ?hook guard =
Proof_global.make_terminator
- (obligation_terminator ?univ_hook prg.prg_name num guard auto) in
- let univ_hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in
- let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~univ_hook in
+ (obligation_terminator ?hook prg.prg_name num guard auto) in
+ let hook = Lemmas.mk_hook (obligation_hook prg obl num auto) in
+ let () = Lemmas.start_proof ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in
let _ = Pfedit.by !default_tactic in
Option.iter (fun tac -> Proof_global.set_endline_tactic tac) tac
@@ -1110,10 +1102,10 @@ let show_term n =
let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
- ?(reduce=reduce) ?univ_hook ?(opaque = false) obls =
+ ?(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
- let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce ?univ_hook in
+ let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce ?hook in
let obls,_ = prg.prg_obligations in
if Int.equal (Array.length obls) 0 then (
Flags.if_verbose Feedback.msg_info (info ++ str ".");
@@ -1130,13 +1122,13 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
?(kind=Global,false,Definition) ?(reduce=reduce)
- ?univ_hook ?(opaque = false) notations fixkind =
+ ?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
List.iter
(fun (n, b, t, imps, obls) ->
let prg = init_prog_info sign ~opaque n univdecl (Some b) t ctx deps (Some fixkind)
- notations obls imps kind reduce ?univ_hook
+ notations obls imps kind reduce ?hook
in progmap_add n (CEphemeron.create prg)) l;
let _defined =
List.fold_left (fun finished x ->
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 4eef668f56..c5720363b4 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -13,12 +13,6 @@ open Constr
open Evd
open Names
-type univ_declaration_hook
-val mk_univ_hook : (UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit) ->
- univ_declaration_hook
-val call_univ_hook : ?univ_hook:univ_declaration_hook -> ?fix_exn:Future.fix_exn ->
- UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> 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 *)
@@ -58,14 +52,19 @@ type progress = (* Resolution status of a program *)
val default_tactic : unit Proofview.tactic ref
-val add_definition : Names.Id.t -> ?term:constr -> types ->
- UState.t ->
- ?univdecl:UState.universe_decl -> (* Universe binders and constraints *)
- ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list ->
- ?kind:Decl_kinds.definition_kind ->
- ?tactic:unit Proofview.tactic ->
- ?reduce:(constr -> constr) ->
- ?univ_hook:univ_declaration_hook -> ?opaque:bool -> obligation_info -> progress
+val add_definition
+ : Names.Id.t
+ -> ?term:constr -> types
+ -> UState.t
+ -> ?univdecl:UState.universe_decl (* Universe binders and constraints *)
+ -> ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list
+ -> ?kind:Decl_kinds.definition_kind
+ -> ?tactic:unit Proofview.tactic
+ -> ?reduce:(constr -> constr)
+ -> ?hook:Lemmas.declaration_hook
+ -> ?opaque:bool
+ -> obligation_info
+ -> progress
type notations =
(lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
@@ -82,7 +81,7 @@ val add_mutual_definitions :
?tactic:unit Proofview.tactic ->
?kind:Decl_kinds.definition_kind ->
?reduce:(constr -> constr) ->
- ?univ_hook:univ_declaration_hook -> ?opaque:bool ->
+ ?hook:Lemmas.declaration_hook -> ?opaque:bool ->
notations ->
fixpoint_kind -> unit
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index d22e52e960..f705f347a3 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1033,9 +1033,9 @@ open Pputils
let pr_s = function None -> str"" | Some {v=s} -> str "%" ++ str s in
let pr_if b x = if b then x else str "" in
let pr_br imp x = match imp with
- | Vernacexpr.Implicit -> str "[" ++ x ++ str "]"
- | Vernacexpr.MaximallyImplicit -> str "{" ++ x ++ str "}"
- | Vernacexpr.NotImplicit -> x in
+ | Impargs.Implicit -> str "[" ++ x ++ str "]"
+ | Impargs.MaximallyImplicit -> str "{" ++ x ++ str "}"
+ | Impargs.NotImplicit -> x in
let rec print_arguments n l =
match n, l with
| Some 0, l -> spc () ++ str"/" ++ print_arguments None l
diff --git a/vernac/record.ml b/vernac/record.ml
index b8ed67463d..3202c9bed2 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -487,8 +487,8 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
(DefinitionEntry proj_entry, IsDefinition Definition)
in
let cref = ConstRef cst in
- Impargs.declare_manual_implicits false cref [paramimpls];
- Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls];
+ Impargs.declare_manual_implicits false cref paramimpls;
+ Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls);
Classes.set_typeclass_transparency (EvalConstRef cst) false false;
let sub = match List.hd coers with
| Some b -> Some ((if b then Backward else Forward), List.hd priorities)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6c4b0acd52..d227834fcf 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -16,7 +16,6 @@ open CAst
open Util
open Names
open Nameops
-open Term
open Tacmach
open Constrintern
open Prettyp
@@ -32,6 +31,7 @@ open Lemmas
open Locality
open Attributes
+module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
(** TODO: make this function independent of Ltac *)
@@ -133,22 +133,23 @@ let show_intro all =
*)
let make_cases_aux glob_ref =
+ let open Declarations in
match glob_ref with
| Globnames.IndRef ind ->
- let {Declarations.mind_nparams = np} , {Declarations.mind_nf_lc = tarr} = Global.lookup_inductive ind in
+ let mib, mip = Global.lookup_inductive ind in
Util.Array.fold_right_i
- (fun i typ l ->
- let al = List.rev (fst (decompose_prod typ)) in
- let al = Util.List.skipn np al in
+ (fun i (ctx, _) l ->
+ let al = Util.List.skipn (List.length mib.mind_params_ctxt) (List.rev ctx) in
let rec rename avoid = function
| [] -> []
- | (n,_)::l ->
+ | RelDecl.LocalDef _ :: l -> "_" :: rename avoid l
+ | RelDecl.LocalAssum (n, _)::l ->
let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n avoid in
Id.to_string n' :: rename (Id.Set.add n' avoid) l in
let al' = rename Id.Set.empty al in
let consref = ConstructRef (ith_constructor_of_inductive ind (i + 1)) in
(Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l)
- tarr []
+ mip.mind_nf_lc []
| _ -> raise Not_found
let make_cases s =
@@ -542,7 +543,7 @@ let vernac_definition_hook p = function
| Coercion ->
Some (Class.add_coercion_hook p)
| CanonicalStructure ->
- Some (Lemmas.mk_hook (fun _ -> Recordops.declare_canonical_structure))
+ Some (Lemmas.mk_hook (fun _ _ _ -> Recordops.declare_canonical_structure))
| SubClass ->
Some (Class.add_subclass_hook p)
| _ -> None
@@ -609,6 +610,11 @@ let vernac_assumption ~atts discharge kind l nl =
let status = ComAssumption.do_assumptions ~program_mode:atts.program kind nl l in
if not status then Feedback.feedback Feedback.AddedAxiom
+let is_polymorphic_inductive_cumulativity =
+ declare_bool_option_and_ref ~depr:false ~value:false
+ ~name:"Polymorphic inductive cumulativity"
+ ~key:["Polymorphic"; "Inductive"; "Cumulativity"]
+
let should_treat_as_cumulative cum poly =
match cum with
| Some VernacCumulative ->
@@ -617,7 +623,7 @@ let should_treat_as_cumulative cum poly =
| Some VernacNonCumulative ->
if poly then false
else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.")
- | None -> poly && Flags.is_polymorphic_inductive_cumulativity ()
+ | None -> poly && is_polymorphic_inductive_cumulativity ()
let get_uniform_inductive_parameters =
Goptions.declare_bool_option_and_ref
@@ -1168,14 +1174,6 @@ let vernac_syntactic_definition ~module_local lid x y =
Dumpglob.dump_definition lid false "syndef";
Metasyntax.add_syntactic_definition (Global.env()) lid.v x module_local y
-let vernac_declare_implicits ~section_local r l =
- match l with
- | [] ->
- Impargs.declare_implicits section_local (smart_global r)
- | _::_ as imps ->
- Impargs.declare_manual_implicits section_local (smart_global r) ~enriching:false
- (List.map (List.map (fun (ex,b,f) -> ex, (b,true,f))) imps)
-
let warn_arguments_assert =
CWarnings.create ~name:"arguments-assert" ~category:"vernacular"
(fun sr ->
@@ -1331,43 +1329,15 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
user_err (strbrk "Some argument names are duplicated: " ++ duplicates)
end;
- (* Parts of this code are overly complicated because the implicit arguments
- API is completely crazy: positions (ExplByPos) are elaborated to
- names. This is broken by design, since not all arguments have names. So
- even though we eventually want to map only positions to implicit statuses,
- we have to check whether the corresponding arguments have names, not to
- trigger an error in the impargs code. Even better, the names we have to
- check are not the current ones (after previous renamings), but the original
- ones (inferred from the type). *)
-
let implicits =
List.map (fun { name; implicit_status = i } -> (name,i)) args
in
let implicits = implicits :: more_implicits in
- let open Vernacexpr in
- let rec build_implicits inf_names implicits =
- match inf_names, implicits with
- | _, [] -> []
- | _ :: inf_names, (_, NotImplicit) :: implicits ->
- build_implicits inf_names implicits
-
- (* With the current impargs API, it is impossible to make an originally
- anonymous argument implicit *)
- | Anonymous :: _, (name, _) :: _ ->
- user_err ~hdr:"vernac_declare_arguments"
- (strbrk"Argument "++ Name.print name ++
- strbrk " cannot be declared implicit.")
-
- | Name id :: inf_names, (name, impl) :: implicits ->
- let max = impl = MaximallyImplicit in
- (ExplByName id,max,false) :: build_implicits inf_names implicits
-
- | _ -> assert false (* already checked in [names_union] *)
- in
-
- let implicits = List.map (build_implicits inf_names) implicits in
- let implicits_specified = match implicits with [[]] -> false | _ -> true in
+ let implicits = List.map (List.map snd) implicits in
+ let implicits_specified = match implicits with
+ | [l] -> List.exists (function Impargs.NotImplicit -> false | _ -> true) l
+ | _ -> true in
if implicits_specified && clear_implicits_flag then
user_err Pp.(str "The \"clear implicits\" flag is incompatible with implicit annotations");
@@ -1410,10 +1380,10 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
end;
if implicits_specified || clear_implicits_flag then
- vernac_declare_implicits ~section_local reference implicits;
+ Impargs.set_implicits section_local (smart_global reference) implicits;
if default_implicits_flag then
- vernac_declare_implicits ~section_local reference [];
+ Impargs.declare_implicits section_local (smart_global reference);
if red_modifiers_specified then begin
match sr with
@@ -1564,14 +1534,6 @@ let () =
optwrite = (fun b -> Flags.raw_print := b) }
let () =
- declare_bool_option
- { optdepr = false;
- optname = "Polymorphic inductive cumulativity";
- optkey = ["Polymorphic"; "Inductive"; "Cumulativity"];
- optread = Flags.is_polymorphic_inductive_cumulativity;
- optwrite = Flags.make_polymorphic_inductive_cumulativity }
-
-let () =
declare_int_option
{ optdepr = false;
optname = "the level of inlining during functor application";
@@ -2380,6 +2342,8 @@ let locate_if_not_already ?loc (e, info) =
exception HasNotFailed
exception HasFailed of Pp.t
+let test_mode = ref false
+
(* XXX STATE: this type hints that restoring the state should be the
caller's responsibility *)
let with_fail st b f =
@@ -2405,7 +2369,7 @@ let with_fail st b f =
| HasNotFailed ->
user_err ~hdr:"Fail" (str "The command has not failed!")
| HasFailed msg ->
- if not !Flags.quiet || !Flags.test_mode then Feedback.msg_info
+ if not !Flags.quiet || !test_mode then Feedback.msg_info
(str "The command has indeed failed with message:" ++ fnl () ++ msg)
| _ -> assert false
end
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 4fbd3849b0..f43cec48e9 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -41,3 +41,7 @@ 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
+
+(* 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 2eb901890b..d1da7c0602 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -237,13 +237,11 @@ type vernac_cumulative = VernacCumulative | VernacNonCumulative
(** {6 The type of vernacular expressions} *)
-type vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit
-
type vernac_argument_status = {
name : Name.t;
recarg_like : bool;
notation_scope : string CAst.t option;
- implicit_status : vernac_implicit_status;
+ implicit_status : Impargs.implicit_kind;
}
type extend_name =
@@ -355,7 +353,7 @@ type nonrec vernac_expr =
onlyparsing_flag
| VernacArguments of qualid or_by_notation *
vernac_argument_status list (* Main arguments status list *) *
- (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) *
+ (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) *
int option (* Number of args to trigger reduction *) *
[ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename |
`ExtraScopes | `Assert | `ClearImplicits | `ClearScopes |
@@ -409,3 +407,9 @@ type vernac_control =
| VernacRedirect of string * vernac_control CAst.t
| VernacTimeout of int * vernac_control
| VernacFail of vernac_control
+
+(** Deprecated *)
+
+type vernac_implicit_status = Impargs.implicit_kind =
+ | Implicit [@ocaml.deprecated] | MaximallyImplicit [@ocaml.deprecated] | NotImplicit [@ocaml.deprecated]
+[@@ocaml.deprecated "Use [Impargs.implicit_kind]"]
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 08:22:39 +0000