From 9051c1618062ce014719de5c3f73832e9a282a4d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 13 Jul 2017 19:53:54 +0200 Subject: [general] Move files to directories matching linking order. We move a bunch of modules (`Impargs`, `Declare`, `Ind_tables`, `Miscprint`) to their proper place as they were declared in different `mllib` files than the one in their directory. In some cases this could be refined but we don't do anything fancy, we just reflect the status quo. --- vernac/ind_tables.ml | 203 -------------------------------------------------- vernac/ind_tables.mli | 51 ------------- 2 files changed, 254 deletions(-) delete mode 100644 vernac/ind_tables.ml delete mode 100644 vernac/ind_tables.mli (limited to 'vernac') diff --git a/vernac/ind_tables.ml b/vernac/ind_tables.ml deleted file mode 100644 index 0407c1e36..000000000 --- a/vernac/ind_tables.ml +++ /dev/null @@ -1,203 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants -type individual_scheme_object_function = - internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants - -type 'a scheme_kind = string - -let scheme_map = Summary.ref Indmap.empty ~name:"Schemes" - -let pr_scheme_kind = Pp.str - -let cache_one_scheme kind (ind,const) = - let map = try Indmap.find ind !scheme_map with Not_found -> String.Map.empty in - scheme_map := Indmap.add ind (String.Map.add kind const map) !scheme_map - -let cache_scheme (_,(kind,l)) = - Array.iter (cache_one_scheme kind) l - -let subst_one_scheme subst (ind,const) = - (* Remark: const is a def: the result of substitution is a constant *) - (subst_ind subst ind,subst_constant subst const) - -let subst_scheme (subst,(kind,l)) = - (kind,Array.map (subst_one_scheme subst) l) - -let discharge_scheme (_,(kind,l)) = - Some (kind,Array.map (fun (ind,const) -> - (Lib.discharge_inductive ind,Lib.discharge_con const)) l) - -let inScheme : string * (inductive * constant) array -> obj = - declare_object {(default_object "SCHEME") with - cache_function = cache_scheme; - load_function = (fun _ -> cache_scheme); - subst_function = subst_scheme; - classify_function = (fun obj -> Substitute obj); - discharge_function = discharge_scheme} - -(**********************************************************************) -(* The table of scheme building functions *) - -type individual -type mutual - -type scheme_object_function = - | MutualSchemeFunction of mutual_scheme_object_function - | IndividualSchemeFunction of individual_scheme_object_function - -let scheme_object_table = - (Hashtbl.create 17 : (string, string * scheme_object_function) Hashtbl.t) - -let declare_scheme_object s aux f = - let () = - if not (Id.is_valid ("ind" ^ s)) then - user_err Pp.(str ("Illegal induction scheme suffix: " ^ s)) - in - let key = if String.is_empty aux then s else aux in - try - let _ = Hashtbl.find scheme_object_table key in -(* let aux_msg = if aux="" then "" else " (with key "^aux^")" in*) - user_err ~hdr:"IndTables.declare_scheme_object" - (str "Scheme object " ++ str key ++ str " already declared.") - with Not_found -> - Hashtbl.add scheme_object_table key (s,f); - key - -let declare_mutual_scheme_object s ?(aux="") f = - declare_scheme_object s aux (MutualSchemeFunction f) - -let declare_individual_scheme_object s ?(aux="") f = - declare_scheme_object s aux (IndividualSchemeFunction f) - -(**********************************************************************) -(* Defining/retrieving schemes *) - -let declare_scheme kind indcl = - Lib.add_anonymous_leaf (inScheme (kind,indcl)) - -let () = Declare.set_declare_scheme declare_scheme - -let is_visible_name id = - try ignore (Nametab.locate (Libnames.qualid_of_ident id)); true - with Not_found -> false - -let compute_name internal id = - match internal with - | UserAutomaticRequest | UserIndividualRequest -> id - | InternalTacticRequest -> - Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name - -let define internal id c p univs = - let fd = declare_constant ~internal in - let id = compute_name internal id in - let ctx = Evd.normalize_evar_universe_context univs in - let c = Vars.subst_univs_fn_constr - (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in - let entry = { - const_entry_body = - Future.from_val ((c,Univ.ContextSet.empty), - Safe_typing.empty_private_constants); - const_entry_secctx = None; - const_entry_type = None; - const_entry_polymorphic = p; - const_entry_universes = Evd.evar_context_universe_context ctx; - const_entry_opaque = false; - const_entry_inline_code = false; - const_entry_feedback = None; - } in - let kn = fd id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in - let () = match internal with - | InternalTacticRequest -> () - | _-> definition_message id - in - kn - -let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = - let (c, ctx), eff = f mode ind in - let mib = Global.lookup_mind mind in - let id = match idopt with - | Some id -> id - | None -> add_suffix mib.mind_packets.(i).mind_typename suff in - let const = define mode id c (Declareops.inductive_is_polymorphic mib) ctx in - declare_scheme kind [|ind,const|]; - const, Safe_typing.add_private - (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff - -let define_individual_scheme kind mode names (mind,i as ind) = - match Hashtbl.find scheme_object_table kind with - | _,MutualSchemeFunction f -> assert false - | s,IndividualSchemeFunction f -> - define_individual_scheme_base kind s f mode names ind - -let define_mutual_scheme_base kind suff f mode names mind = - let (cl, ctx), eff = f mode mind in - let mib = Global.lookup_mind mind in - let ids = Array.init (Array.length mib.mind_packets) (fun i -> - try Int.List.assoc i names - with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in - let consts = Array.map2 (fun id cl -> - define mode id cl (Declareops.inductive_is_polymorphic mib) ctx) ids cl in - let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in - declare_scheme kind schemes; - consts, - Safe_typing.add_private - (Safe_typing.private_con_of_scheme - ~kind (Global.safe_env()) (Array.to_list schemes)) - eff - -let define_mutual_scheme kind mode names mind = - match Hashtbl.find scheme_object_table kind with - | _,IndividualSchemeFunction _ -> assert false - | s,MutualSchemeFunction f -> - define_mutual_scheme_base kind s f mode names mind - -let find_scheme_on_env_too kind ind = - let s = String.Map.find kind (Indmap.find ind !scheme_map) in - s, Safe_typing.add_private - (Safe_typing.private_con_of_scheme - ~kind (Global.safe_env()) [ind, s]) - Safe_typing.empty_private_constants - -let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) = - try find_scheme_on_env_too kind ind - with Not_found -> - match Hashtbl.find scheme_object_table kind with - | s,IndividualSchemeFunction f -> - define_individual_scheme_base kind s f mode None ind - | s,MutualSchemeFunction f -> - let ca, eff = define_mutual_scheme_base kind s f mode [] mind in - ca.(i), eff - -let check_scheme kind ind = - try let _ = find_scheme_on_env_too kind ind in true - with Not_found -> false diff --git a/vernac/ind_tables.mli b/vernac/ind_tables.mli deleted file mode 100644 index 005555caa..000000000 --- a/vernac/ind_tables.mli +++ /dev/null @@ -1,51 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants -type individual_scheme_object_function = - internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants - -(** Main functions to register a scheme builder *) - -val declare_mutual_scheme_object : string -> ?aux:string -> - mutual_scheme_object_function -> mutual scheme_kind - -val declare_individual_scheme_object : string -> ?aux:string -> - individual_scheme_object_function -> - individual scheme_kind - -(** Force generation of a (mutually) scheme with possibly user-level names *) - -val define_individual_scheme : individual scheme_kind -> - internal_flag (** internal *) -> - Id.t option -> inductive -> constant * Safe_typing.private_constants - -val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) -> - (int * Id.t) list -> mutual_inductive -> constant array * Safe_typing.private_constants - -(** Main function to retrieve a scheme in the cache or to generate it *) -val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Safe_typing.private_constants - -val check_scheme : 'a scheme_kind -> inductive -> bool - - -val pr_scheme_kind : 'a scheme_kind -> Pp.std_ppcmds -- cgit v1.2.3