diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 2 | ||||
| -rw-r--r-- | toplevel/command.mli | 2 | ||||
| -rw-r--r-- | toplevel/ind_tables.ml | 15 | ||||
| -rw-r--r-- | toplevel/ind_tables.mli | 5 | ||||
| -rw-r--r-- | toplevel/indschemes.ml | 53 | ||||
| -rw-r--r-- | toplevel/record.ml | 3 |
6 files changed, 50 insertions, 30 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 4259ccb81c..21fb277e2b 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 b056afa58d..779e77f313 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 8e3d9437f8..4e8d861000 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 0d3a250c95..babc2d9209 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 a02b01351f..03813c9d48 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 e4177b0fc1..89bf769114 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 |