diff options
Diffstat (limited to 'library/impargs.ml')
| -rw-r--r-- | library/impargs.ml | 72 |
1 files changed, 58 insertions, 14 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index 5248bc4a61..e2ec4a4762 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -7,6 +7,8 @@ open Reduction open Declarations open Environ open Inductive +open Libobject +open Lib type implicits = | Impl_auto of int list @@ -43,18 +45,30 @@ let list_of_implicits = function | Impl_manual l -> l | No_impl -> [] -(* Constants. *) +(*s Constants. *) let constants_table = ref Spmap.empty -let declare_constant_implicits sp = +let compute_constant_implicits sp = let env = Global.env () in let cb = lookup_constant sp env in - let imps = auto_implicits env (body_of_type cb.const_type) in + auto_implicits env (body_of_type cb.const_type) + +let cache_constant_implicits (_,(sp,imps)) = constants_table := Spmap.add sp imps !constants_table -let declare_constant_manual_implicits sp imps = - constants_table := Spmap.add sp (Impl_manual imps) !constants_table +let (in_constant_implicits, _) = + let od = { + cache_function = cache_constant_implicits; + load_function = cache_constant_implicits; + open_function = (fun _ -> ()); + export_function = (fun x -> Some x) } + in + declare_object ("CONSTANT-IMPLICITS", od) + +let declare_constant_implicits sp = + let imps = compute_constant_implicits sp in + add_anonymous_leaf (in_constant_implicits (sp,imps)) let constant_implicits sp = try Spmap.find sp !constants_table with Not_found -> No_impl @@ -62,14 +76,14 @@ let constant_implicits sp = let constant_implicits_list sp = list_of_implicits (constant_implicits sp) -(* Inductives and constructors. Their implicit arguments are stored +(*s Inductives and constructors. Their implicit arguments are stored in an array, indexed by the inductive number, of pairs $(i,v)$ where $i$ are the implicit arguments of the inductive and $v$ the array of implicit arguments of the constructors. *) let inductives_table = ref Spmap.empty -let declare_inductive_implicits sp = +let compute_inductive_implicits sp = let env = Global.env () in let mib = lookup_mind sp env in let env_ar = push_rels (mind_arities_context mib) env in @@ -78,9 +92,24 @@ let declare_inductive_implicits sp = Array.map (fun c -> auto_implicits env_ar (body_of_type c)) (mind_user_lc mip)) in - let imps = Array.map imps_one_inductive mib.mind_packets in + Array.map imps_one_inductive mib.mind_packets + +let cache_inductive_implicits (_,(sp,imps)) = inductives_table := Spmap.add sp imps !inductives_table - + +let (in_inductive_implicits, _) = + let od = { + cache_function = cache_inductive_implicits; + load_function = cache_inductive_implicits; + open_function = (fun _ -> ()); + export_function = (fun x -> Some x) } + in + declare_object ("INDUCTIVE-IMPLICITS", od) + +let declare_inductive_implicits sp = + let imps = compute_inductive_implicits sp in + add_anonymous_leaf (in_inductive_implicits (sp,imps)) + let inductive_implicits (sp,i) = try let imps = Spmap.find sp !inductives_table in fst imps.(i) @@ -99,20 +128,35 @@ let constructor_implicits_list constr_sp = let inductive_implicits_list ind_sp = list_of_implicits (inductive_implicits ind_sp) -(* Variables. *) +(*s Variables. *) let var_table = ref Spmap.empty -let declare_var_implicits sp = +let compute_var_implicits sp = let env = Global.env () in let (_,ty) = lookup_named (basename sp) env in - let imps = auto_implicits env (body_of_type ty) in + auto_implicits env (body_of_type ty) + +let cache_var_implicits (_,(sp,imps)) = var_table := Spmap.add sp imps !var_table +let (in_var_implicits, _) = + let od = { + cache_function = cache_var_implicits; + load_function = cache_var_implicits; + open_function = (fun _ -> ()); + export_function = (fun x -> Some x) } + in + declare_object ("VARIABLE-IMPLICITS", od) + +let declare_var_implicits sp = + let imps = compute_var_implicits sp in + add_anonymous_leaf (in_var_implicits (sp,imps)) + let implicits_of_var sp = list_of_implicits (try Spmap.find sp !var_table with Not_found -> No_impl) -(* Tests if declared implicit *) +(*s Tests if declared implicit *) let is_implicit_constant sp = try let _ = Spmap.find sp !constants_table in true with Not_found -> false @@ -130,7 +174,7 @@ let implicits_of_global = function | ConstructRef csp -> list_of_implicits (constructor_implicits csp) | EvarRef _ -> [] -(* Registration as global tables and roolback. *) +(*s Registration as global tables and rollback. *) type frozen_t = bool * implicits Spmap.t |