aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--library/declare.ml16
-rw-r--r--library/declare.mli11
-rw-r--r--plugins/funind/merge.ml2
-rw-r--r--plugins/xml/xmlcommand.ml21
-rw-r--r--toplevel/command.ml2
-rw-r--r--toplevel/command.mli2
-rw-r--r--toplevel/ind_tables.ml15
-rw-r--r--toplevel/ind_tables.mli5
-rw-r--r--toplevel/indschemes.ml53
-rw-r--r--toplevel/record.ml3
10 files changed, 85 insertions, 45 deletions
diff --git a/library/declare.ml b/library/declare.ml
index b571ecf3a..2886c63d8 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -25,11 +25,17 @@ open Cooking
open Decls
open Decl_kinds
+(** flag for internal message display *)
+type internal_flag =
+ | KernelVerbose (* kernel action, a message is displayed *)
+ | KernelSilent (* kernel action, no message is displayed *)
+ | UserVerbose (* user action, a message is displayed *)
+
(** XML output hooks *)
let xml_declare_variable = ref (fun (sp:object_name) -> ())
-let xml_declare_constant = ref (fun (sp:bool * constant)-> ())
-let xml_declare_inductive = ref (fun (sp:bool * object_name) -> ())
+let xml_declare_constant = ref (fun (sp:internal_flag * constant)-> ())
+let xml_declare_inductive = ref (fun (sp:internal_flag * object_name) -> ())
let if_xml f x = if !Flags.xml_export then f x else ()
@@ -172,8 +178,10 @@ let declare_constant_gen internal id (cd,kind) =
!xml_declare_constant (internal,kn);
kn
-let declare_internal_constant = declare_constant_gen true
-let declare_constant = declare_constant_gen false
+(* TODO: add a third function to distinguish between KernelVerbose
+ * and user Verbose *)
+let declare_internal_constant = declare_constant_gen KernelSilent
+let declare_constant = declare_constant_gen UserVerbose
(** Declaration of inductive blocks *)
diff --git a/library/declare.mli b/library/declare.mli
index 3ff91cc5e..3847a4ab9 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -44,6 +44,11 @@ type constant_declaration = constant_entry * logical_kind
(** [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 *)
+type internal_flag =
+ | KernelVerbose
+ | KernelSilent
+ | UserVerbose
+
val declare_constant :
identifier -> constant_declaration -> constant
@@ -53,12 +58,12 @@ val declare_internal_constant :
(** [declare_mind me] declares a block of inductive types with
their constructors in the current section; it returns the path of
the whole block (boolean must be true iff it is a record) *)
-val declare_mind : bool -> mutual_inductive_entry -> object_name
+val declare_mind : internal_flag -> mutual_inductive_entry -> object_name
(** Hooks for XML output *)
val set_xml_declare_variable : (object_name -> unit) -> unit
-val set_xml_declare_constant : (bool * constant -> unit) -> unit
-val set_xml_declare_inductive : (bool * object_name -> unit) -> unit
+val set_xml_declare_constant : (internal_flag * constant -> unit) -> unit
+val set_xml_declare_inductive : (internal_flag * object_name -> unit) -> unit
(** Hook for the cache function of constants and inductives *)
val add_cache_hook : (full_path -> unit) -> unit
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 1cf74025a..a64ae57f5 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -906,7 +906,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
let mie,impls = Command.interp_mutual_inductive indl [] true (* means: not coinductive *) in
(* Declare the mutual inductive block with its associated schemes *)
- ignore (Command.declare_mutual_inductive_with_eliminations false mie impls)
+ ignore (Command.declare_mutual_inductive_with_eliminations Declare.UserVerbose mie impls)
(* Find infos on identifier id. *)
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 676863b78..336ae2ccd 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -408,7 +408,11 @@ let kind_of_global_goal = function
let kind_of_inductive isrecord kn =
"DEFINITION",
if (fst (Global.lookup_inductive (kn,0))).Declarations.mind_finite
- then if isrecord then "Record" else "Inductive"
+ then begin
+ match isrecord with
+ | Declare.KernelSilent -> "Record"
+ | _ -> "Inductive"
+ end
else "CoInductive"
;;
@@ -478,8 +482,8 @@ let kind_of_global r =
match r with
| Ln.IndRef kn | Ln.ConstructRef (kn,_) ->
let isrecord =
- try let _ = Recordops.lookup_projections kn in true
- with Not_found -> false in
+ try let _ = Recordops.lookup_projections kn in Declare.KernelSilent
+ with Not_found -> Declare.KernelVerbose in
kind_of_inductive isrecord (fst kn)
| Ln.VarRef id -> kind_of_variable id
| Ln.ConstRef kn -> kind_of_constant kn
@@ -539,13 +543,15 @@ let print internal glob_ref kind xml_library_root =
in
let fn = filename_of_path xml_library_root tag in
let uri = Cic2acic.uri_of_kernel_name tag in
- if not internal then print_object_kind uri kind;
+ (match internal with
+ | Declare.KernelSilent -> ()
+ | _ -> print_object_kind uri kind);
print_object uri obj Evd.empty None fn
;;
let print_ref qid fn =
let ref = Nametab.global qid in
- print false ref (kind_of_global ref) fn
+ print Declare.UserVerbose ref (kind_of_global ref) fn
(* show dest *)
(* where dest is either None (for stdout) or (Some filename) *)
@@ -580,7 +586,7 @@ let _ =
Declare.set_xml_declare_variable
(function (sp,kn) ->
let id = Libnames.basename sp in
- print false (Libnames.VarRef id) (kind_of_variable id) xml_library_root ;
+ print Declare.UserVerbose (Libnames.VarRef id) (kind_of_variable id) xml_library_root ;
proof_to_export := None)
;;
@@ -603,7 +609,8 @@ let _ =
let _ =
Declare.set_xml_declare_inductive
(function (isrecord,(sp,kn)) ->
- print false (Libnames.IndRef (Names.mind_of_kn kn,0)) (kind_of_inductive isrecord (Names.mind_of_kn kn))
+ print Declare.UserVerbose (Libnames.IndRef (Names.mind_of_kn kn,0))
+ (kind_of_inductive isrecord (Names.mind_of_kn kn))
xml_library_root)
;;
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 4259ccb81..21fb277e2 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -363,7 +363,7 @@ let do_mutual_inductive indl finite =
(* Interpret the types *)
let mie,impls = interp_mutual_inductive indl ntns finite in
(* Declare the mutual inductive block with its associated schemes *)
- ignore (declare_mutual_inductive_with_eliminations false mie impls);
+ ignore (declare_mutual_inductive_with_eliminations UserVerbose mie impls);
(* Declare the possible notations of inductive types *)
List.iter Metasyntax.add_notation_interpretation ntns;
(* Declare the coercions *)
diff --git a/toplevel/command.mli b/toplevel/command.mli
index b056afa58..779e77f31 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -82,7 +82,7 @@ val interp_mutual_inductive :
associated schemes *)
val declare_mutual_inductive_with_eliminations :
- bool -> mutual_inductive_entry -> one_inductive_impls list ->
+ Declare.internal_flag -> mutual_inductive_entry -> one_inductive_impls list ->
mutual_inductive
(** Entry points for the vernacular commands Inductive and CoInductive *)
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 8e3d9437f..4e8d86100 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -110,7 +110,11 @@ let declare_scheme kind indcl =
Lib.add_anonymous_leaf (inScheme (kind,indcl))
let define internal id c =
- let fd = if internal then declare_internal_constant else declare_constant in
+ (* TODO: specify even more by distinguish between KernelVerbose and
+ * UserVerbose *)
+ let fd = match internal with
+ | KernelSilent -> declare_internal_constant
+ | _ -> declare_constant in
let kn = fd id
(DefinitionEntry
{ const_entry_body = c;
@@ -118,7 +122,9 @@ let define internal id c =
const_entry_opaque = false;
const_entry_boxed = Flags.boxed_definitions() },
Decl_kinds.IsDefinition Scheme) in
- if not internal then definition_message id;
+ (match internal with
+ | KernelSilent -> ()
+ | _-> definition_message id);
kn
let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) =
@@ -153,14 +159,15 @@ let define_mutual_scheme kind internal names mind =
| s,MutualSchemeFunction f ->
define_mutual_scheme_base kind s f internal names mind
+(* TODO: change KernelSilent here to the right behaviour *)
let find_scheme kind (mind,i as ind) =
try Stringmap.find kind (Indmap.find ind !scheme_map)
with Not_found ->
match Hashtbl.find scheme_object_table kind with
| s,IndividualSchemeFunction f ->
- define_individual_scheme_base kind s f true None ind
+ define_individual_scheme_base kind s f KernelSilent None ind
| s,MutualSchemeFunction f ->
- (define_mutual_scheme_base kind s f true [] mind).(i)
+ (define_mutual_scheme_base kind s f KernelSilent [] mind).(i)
let check_scheme kind ind =
try let _ = Stringmap.find kind (Indmap.find ind !scheme_map) in true
diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli
index 0d3a250c9..babc2d920 100644
--- a/toplevel/ind_tables.mli
+++ b/toplevel/ind_tables.mli
@@ -39,10 +39,11 @@ val declare_scheme : 'a scheme_kind -> (inductive * constant) array -> unit
(** Force generation of a (mutually) scheme with possibly user-level names *)
-val define_individual_scheme : individual scheme_kind -> bool (** internal *) ->
+val define_individual_scheme : individual scheme_kind ->
+ Declare.internal_flag (** internal *) ->
identifier option -> inductive -> constant
-val define_mutual_scheme : mutual scheme_kind -> bool (** internal *) ->
+val define_mutual_scheme : mutual scheme_kind -> Declare.internal_flag (** internal *) ->
(int * identifier) list -> mutual_inductive -> constant array
(** Main function to retrieve a scheme in the cache or to generate it *)
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index a02b01351..03813c9d4 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -100,7 +100,10 @@ let _ =
(* Util *)
let define id internal c t =
- let f = if internal then declare_internal_constant else declare_constant in
+ (* TODO: specify even more by distinguish KernelVerbose and UserVerbose *)
+ let f = match internal with
+ | KernelSilent -> declare_internal_constant
+ | _ -> declare_constant in
let kn = f id
(DefinitionEntry
{ const_entry_body = c;
@@ -118,12 +121,13 @@ let declare_beq_scheme_gen internal names kn =
let alarm what internal msg =
let debug = false in
- if internal then
+ (* TODO: specify even more by distinguish KernelVerbose and UserVerbose *)
+ match internal with
+ | KernelSilent ->
(if debug then
Flags.if_verbose Pp.msg_warning
(hov 0 msg ++ fnl () ++ what ++ str " not defined."))
- else
- errorlabstrm "" msg
+ | _ -> errorlabstrm "" msg
let try_declare_scheme what f internal names kn =
try f internal names kn
@@ -164,18 +168,19 @@ let beq_scheme_msg mind =
(list_tabulate (fun i -> (mind,i)) (Array.length mib.mind_packets))
let declare_beq_scheme_with l kn =
- try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen false l kn
+ try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserVerbose l kn
+(* TODO : maybe switch to KernelVerbose to have the right behaviour *)
let try_declare_beq_scheme kn =
(* TODO: handle Fix, see e.g. TheoryList.In_spec, eventually handle
proof-irrelevance; improve decidability by depending on decidability
for the parameters rather than on the bl and lb properties *)
- try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen true [] kn
+ try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen KernelSilent [] kn
let declare_beq_scheme = declare_beq_scheme_with []
(* Case analysis schemes *)
-
+(* TODO: maybe switch to KernelVerbose *)
let declare_one_case_analysis_scheme ind =
let (mib,mip) = Global.lookup_inductive ind in
let kind = inductive_sort_family mip in
@@ -185,7 +190,7 @@ let declare_one_case_analysis_scheme ind =
induction scheme, the other ones share the same code with the
apropriate type *)
if List.mem InType kelim then
- ignore (define_individual_scheme dep true None ind)
+ ignore (define_individual_scheme dep KernelSilent None ind)
(* Induction/recursion schemes *)
@@ -199,6 +204,7 @@ let kinds_from_type =
InProp,ind_dep_scheme_kind_from_type;
InSet,rec_dep_scheme_kind_from_type]
+(* TODO: maybe switch to kernel verbose *)
let declare_one_induction_scheme ind =
let (mib,mip) = Global.lookup_inductive ind in
let kind = inductive_sort_family mip in
@@ -208,7 +214,7 @@ let declare_one_induction_scheme ind =
list_map_filter (fun (sort,kind) ->
if List.mem sort kelim then Some kind else None)
(if from_prop then kinds_from_prop else kinds_from_type) in
- List.iter (fun kind -> ignore (define_individual_scheme kind true None ind))
+ List.iter (fun kind -> ignore (define_individual_scheme kind KernelSilent None ind))
elims
let declare_induction_schemes kn =
@@ -231,45 +237,50 @@ let eq_dec_scheme_msg ind = (* TODO: mutual inductive case *)
let declare_eq_decidability_scheme_with l kn =
try_declare_scheme (eq_dec_scheme_msg (kn,0))
- declare_eq_decidability_gen false l kn
+ declare_eq_decidability_gen UserVerbose l kn
+(* TODO: maybe switch to kernel verbose *)
let try_declare_eq_decidability kn =
try_declare_scheme (eq_dec_scheme_msg (kn,0))
- declare_eq_decidability_gen true [] kn
+ declare_eq_decidability_gen KernelSilent [] kn
let declare_eq_decidability = declare_eq_decidability_scheme_with []
let ignore_error f x = try ignore (f x) with _ -> ()
+(* TODO: maybe switch to kernel verbose *)
let declare_rewriting_schemes ind =
if Hipattern.is_inductive_equality ind then begin
- ignore (define_individual_scheme rew_r2l_scheme_kind true None ind);
- ignore (define_individual_scheme rew_r2l_dep_scheme_kind true None ind);
- ignore (define_individual_scheme rew_r2l_forward_dep_scheme_kind true None ind);
+ ignore (define_individual_scheme rew_r2l_scheme_kind KernelSilent None ind);
+ ignore (define_individual_scheme rew_r2l_dep_scheme_kind KernelSilent None ind);
+ ignore (define_individual_scheme rew_r2l_forward_dep_scheme_kind
+ KernelSilent None ind);
(* These ones expect the equality to be symmetric; the first one also *)
(* needs eq *)
- ignore_error (define_individual_scheme rew_l2r_scheme_kind true None) ind;
+ ignore_error (define_individual_scheme rew_l2r_scheme_kind KernelSilent None) ind;
ignore_error
- (define_individual_scheme rew_l2r_dep_scheme_kind true None) ind;
+ (define_individual_scheme rew_l2r_dep_scheme_kind KernelSilent None) ind;
ignore_error
- (define_individual_scheme rew_l2r_forward_dep_scheme_kind true None) ind
+ (define_individual_scheme rew_l2r_forward_dep_scheme_kind KernelSilent None) ind
end
+(* TODO: maybe switch to kernel verbose *)
let declare_congr_scheme ind =
if Hipattern.is_equality_type (mkInd ind) then begin
if
try Coqlib.check_required_library Coqlib.logic_module_name; true
with _ -> false
then
- ignore (define_individual_scheme congr_scheme_kind true None ind)
+ ignore (define_individual_scheme congr_scheme_kind KernelSilent None ind)
else
warning "Cannot build congruence scheme because eq is not found"
end
+(* TODO: maybe switch to kernel verbose *)
let declare_sym_scheme ind =
if Hipattern.is_inductive_equality ind then
(* Expect the equality to be symmetric *)
- ignore_error (define_individual_scheme sym_scheme_kind true None) ind
+ ignore_error (define_individual_scheme sym_scheme_kind KernelSilent None) ind
(* Scheme command *)
@@ -337,7 +348,7 @@ let do_mutual_induction_scheme lnamedepindsort =
let rec declare decl fi lrecref =
let decltype = Retyping.get_type_of env0 Evd.empty decl in
let decltype = refresh_universes decltype in
- let cst = define fi false decl (Some decltype) in
+ let cst = define fi UserVerbose decl (Some decltype) in
ConstRef cst :: lrecref
in
let _ = List.fold_right2 declare listdecl lrecnames [] in
@@ -432,7 +443,7 @@ let do_combined_scheme name schemes =
schemes
in
let body,typ = build_combined_scheme (Global.env ()) csts in
- ignore (define (snd name) false body (Some typ));
+ ignore (define (snd name) UserVerbose body (Some typ));
fixpoint_message None [snd name]
(**********************************************************************)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index e4177b0fc..89bf76911 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -259,7 +259,8 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls
mind_entry_record = true;
mind_entry_finite = recursivity_flag_of_kind finite;
mind_entry_inds = [mie_ind] } in
- let kn = Command.declare_mutual_inductive_with_eliminations true mie [(paramimpls,[])] in
+(* TODO : maybe switch to KernelVerbose *)
+ let kn = Command.declare_mutual_inductive_with_eliminations KernelSilent mie [(paramimpls,[])] in
let rsp = (kn,0) in (* This is ind path of idstruc *)
let cstr = (rsp,1) in
let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 03:36:48 +0000