aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-07-20 14:50:38 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-07-20 14:50:38 +0200
commit011a2fe3ab6841d9c7ad700e6d298d5cffe72db5 (patch)
tree9b71011ec3cb9aae309b32c3173579632efdc143 /vernac
parent362ed8371062cea08ae2d7e5842091bf184393cb (diff)
parent9051c1618062ce014719de5c3f73832e9a282a4d (diff)
Merge PR #899: [general] Move files to directories so they match linking order.
Diffstat (limited to 'vernac')
-rw-r--r--vernac/ind_tables.ml203
-rw-r--r--vernac/ind_tables.mli51
2 files changed, 0 insertions, 254 deletions
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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* File created by Vincent Siles, Oct 2007, extended into a generic
- support for generation of inductive schemes by Hugo Herbelin, Nov 2009 *)
-
-(* This file provides support for registering inductive scheme builders,
- declaring schemes and generating schemes on demand *)
-
-open Names
-open Mod_subst
-open Libobject
-open Nameops
-open Declarations
-open Term
-open CErrors
-open Util
-open Declare
-open Entries
-open Decl_kinds
-open Pp
-
-(**********************************************************************)
-(* Registering schemes in the environment *)
-
-type mutual_scheme_object_function =
- internal_flag -> 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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Term
-open Names
-open Declare
-
-(** This module provides support for registering inductive scheme builders,
- declaring schemes and generating schemes on demand *)
-
-(** A scheme is either a "mutual scheme_kind" or an "individual scheme_kind" *)
-
-type mutual
-type individual
-type 'a scheme_kind
-
-type mutual_scheme_object_function =
- internal_flag -> 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