summaryrefslogtreecommitdiff
path: root/toplevel/ind_tables.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/ind_tables.ml')
-rw-r--r--toplevel/ind_tables.ml254
1 files changed, 164 insertions, 90 deletions
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 4b97f8b2..492b21e0 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -6,97 +6,171 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ind_tables.ml 10739 2008-04-01 14:45:20Z herbelin $ i*)
+(*i $Id$ i*)
-open Names
-open Mod_subst
-
-let eq_scheme_map = ref Indmap.empty
-
-let cache_scheme (_,(ind,const)) =
- eq_scheme_map := Indmap.add ind const (!eq_scheme_map)
-
-let export_scheme obj =
- Some obj
-
-
-
-let _ = Summary.declare_summary "eqscheme"
- { Summary.freeze_function = (fun () -> !eq_scheme_map);
- Summary.unfreeze_function = (fun fs -> eq_scheme_map := fs);
- Summary.init_function = (fun () -> eq_scheme_map := Indmap.empty);
- Summary.survive_module = false;
- Summary.survive_section = true}
-
-let find_eq_scheme ind =
- Indmap.find ind !eq_scheme_map
-
-let check_eq_scheme ind =
- Indmap.mem ind !eq_scheme_map
-
-let bl_map = ref Indmap.empty
-let lb_map = ref Indmap.empty
-let dec_map = ref Indmap.empty
-
-
-let cache_bl (_,(ind,const)) =
- bl_map := Indmap.add ind const (!bl_map)
-
-let cache_lb (_,(ind,const)) =
- lb_map := Indmap.add ind const (!lb_map)
-
-let cache_dec (_,(ind,const)) =
- dec_map := Indmap.add ind const (!dec_map)
-
-let export_bool_leib obj =
- Some obj
-
-let export_leib_bool obj =
- Some obj
-
-let export_dec_proof obj =
- Some obj
-
-
-
-let _ = Summary.declare_summary "bl_proof"
- { Summary.freeze_function = (fun () -> !bl_map);
- Summary.unfreeze_function = (fun fs -> bl_map := fs);
- Summary.init_function = (fun () -> bl_map := Indmap.empty);
- Summary.survive_module = false;
- Summary.survive_section = true}
-
-let find_bl_proof ind =
- Indmap.find ind !bl_map
-
-let check_bl_proof ind =
- Indmap.mem ind !bl_map
-
-let _ = Summary.declare_summary "lb_proof"
- { Summary.freeze_function = (fun () -> !lb_map);
- Summary.unfreeze_function = (fun fs -> lb_map := fs);
- Summary.init_function = (fun () -> lb_map := Indmap.empty);
- Summary.survive_module = false;
- Summary.survive_section = true}
-
-let find_lb_proof ind =
- Indmap.find ind !lb_map
-
-let check_lb_proof ind =
- Indmap.mem ind !lb_map
-
-let _ = Summary.declare_summary "eq_dec_proof"
- { Summary.freeze_function = (fun () -> !dec_map);
- Summary.unfreeze_function = (fun fs -> dec_map := fs);
- Summary.init_function = (fun () -> dec_map := Indmap.empty);
- Summary.survive_module = false;
- Summary.survive_section = true}
-
-let find_eq_dec_proof ind =
- Indmap.find ind !dec_map
-
-let check_dec_proof ind =
- Indmap.mem ind !dec_map
+(* 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 Util
+open Declare
+open Entries
+open Decl_kinds
+
+(**********************************************************************)
+(* Registering schemes in the environment *)
+
+type mutual_scheme_object_function = mutual_inductive -> constr array
+type individual_scheme_object_function = inductive -> constr
+
+type 'a scheme_kind = string
+
+let scheme_map = ref Indmap.empty
+
+let cache_one_scheme kind (ind,const) =
+ let map = try Indmap.find ind !scheme_map with Not_found -> Stringmap.empty in
+ scheme_map := Indmap.add ind (Stringmap.add kind const map) !scheme_map
+
+let cache_scheme (_,(kind,l)) =
+ Array.iter (cache_one_scheme kind) l
+
+let subst_one_scheme subst ((mind,i),const) =
+ (* Remark: const is a def: the result of substitution is a constant *)
+ ((subst_ind subst mind,i),fst (subst_con 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,_) =
+ 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}
+
+(**********************************************************************)
+(* Saving/restoring the table of scheme *)
+
+let freeze_schemes () = !scheme_map
+let unfreeze_schemes sch = scheme_map := sch
+let init_schemes () = scheme_map := Indmap.empty
+
+let _ =
+ Summary.declare_summary "Schemes"
+ { Summary.freeze_function = freeze_schemes;
+ Summary.unfreeze_function = unfreeze_schemes;
+ Summary.init_function = init_schemes }
+
+(**********************************************************************)
+(* The table of scheme building functions *)
+
+type individual
+type mutual
+
+type scheme_object_function =
+ | MutualSchemeFunction of (mutual_inductive -> constr array)
+ | IndividualSchemeFunction of (inductive -> constr)
+
+let scheme_object_table =
+ (Hashtbl.create 17 : (string, string * scheme_object_function) Hashtbl.t)
+
+let declare_scheme_object s aux f =
+ (try check_ident ("ind"^s) with _ ->
+ error ("Illegal induction scheme suffix: "^s));
+ let key = if 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*)
+ error ("Scheme object "^key^" 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 define internal id c =
+ (* 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;
+ const_entry_type = None;
+ const_entry_opaque = false;
+ const_entry_boxed = Flags.boxed_definitions() },
+ Decl_kinds.IsDefinition Scheme) in
+ (match internal with
+ | KernelSilent -> ()
+ | _-> definition_message id);
+ kn
+
+let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) =
+ let c = f 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 internal id c in
+ declare_scheme kind [|ind,const|];
+ const
+
+let define_individual_scheme kind internal 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 internal names ind
+
+let define_mutual_scheme_base kind suff f internal names mind =
+ let cl = f mind in
+ let mib = Global.lookup_mind mind in
+ let ids = Array.init (Array.length mib.mind_packets) (fun i ->
+ try List.assoc i names
+ with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
+ let consts = array_map2 (define internal) ids cl in
+ declare_scheme kind (Array.mapi (fun i cst -> ((mind,i),cst)) consts);
+ consts
+
+let define_mutual_scheme kind internal names mind =
+ match Hashtbl.find scheme_object_table kind with
+ | _,IndividualSchemeFunction _ -> assert false
+ | s,MutualSchemeFunction f ->
+ define_mutual_scheme_base kind s f internal names mind
+
+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 KernelSilent None ind
+ | s,MutualSchemeFunction f ->
+ (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
+ with Not_found -> false
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 11:13:34 +0000