diff options
Diffstat (limited to 'library/impargs.ml')
| -rw-r--r-- | library/impargs.ml | 140 |
1 files changed, 110 insertions, 30 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index e2ec4a4762..cf2d09d610 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -81,9 +81,53 @@ let constant_implicits_list sp = $i$ are the implicit arguments of the inductive and $v$ the array of implicit arguments of the constructors. *) -let inductives_table = ref Spmap.empty +module Inductive_path = struct + type t = inductive_path + let compare (spx,ix) (spy,iy) = + let c = ix - iy in if c = 0 then sp_ord spx spy else c +end -let compute_inductive_implicits sp = +module Indmap = Map.Make(Inductive_path) + +let inductives_table = ref Indmap.empty + +module Construtor_path = struct + type t = constructor_path + let compare (indx,ix) (indy,iy) = + let c = ix - iy in if c = 0 then Inductive_path.compare indx indy else c +end + +module Constrmap = Map.Make(Construtor_path) + +let inductives_table = ref Indmap.empty + +let constructors_table = ref Constrmap.empty + +let cache_inductive_implicits (_,(indp,imps)) = + inductives_table := Indmap.add indp 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 cache_constructor_implicits (_,(consp,imps)) = + constructors_table := Constrmap.add consp imps !constructors_table + +let (in_constructor_implicits, _) = + let od = { + cache_function = cache_constructor_implicits; + load_function = cache_constructor_implicits; + open_function = (fun _ -> ()); + export_function = (fun x -> Some x) } + in + declare_object ("CONSTRUCTOR-IMPLICITS", od) + +let compute_mib_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 @@ -94,33 +138,35 @@ let compute_inductive_implicits sp = 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 cache_mib_implicits (_,(sp,mibimps)) = + Array.iteri + (fun i (imps,v) -> + let indp = (sp,i) in + inductives_table := Indmap.add indp imps !inductives_table; + Array.iteri + (fun j imps -> + constructors_table := + Constrmap.add (indp,succ j) imps !constructors_table) v) + mibimps + +let (in_mib_implicits, _) = let od = { - cache_function = cache_inductive_implicits; - load_function = cache_inductive_implicits; + cache_function = cache_mib_implicits; + load_function = cache_mib_implicits; open_function = (fun _ -> ()); export_function = (fun x -> Some x) } in - declare_object ("INDUCTIVE-IMPLICITS", od) + declare_object ("MIB-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) - with Not_found -> - No_impl - -let constructor_implicits ((sp,i),j) = - try - let imps = Spmap.find sp !inductives_table in (snd imps.(i)).(pred j) - with Not_found -> - No_impl +let declare_mib_implicits sp = + let imps = compute_mib_implicits sp in + add_anonymous_leaf (in_mib_implicits (sp,imps)) + +let inductive_implicits indp = + try Indmap.find indp !inductives_table with Not_found -> No_impl + +let constructor_implicits consp = + try Constrmap.find consp !constructors_table with Not_found -> No_impl let constructor_implicits_list constr_sp = list_of_implicits (constructor_implicits constr_sp) @@ -156,13 +202,43 @@ let declare_var_implicits sp = let implicits_of_var sp = list_of_implicits (try Spmap.find sp !var_table with Not_found -> No_impl) +(*s Implicits of a global reference. *) + +let declare_implicits = function + | VarRef sp -> + declare_var_implicits sp + | ConstRef sp -> + declare_constant_implicits sp + | IndRef ((sp,i) as indp) -> + let mib_imps = compute_mib_implicits sp in + let imps = fst mib_imps.(i) in + add_anonymous_leaf (in_inductive_implicits (indp, imps)) + | ConstructRef (((sp,i),j) as consp) -> + let mib_imps = compute_mib_implicits sp in + let imps = (snd mib_imps.(i)).(j-1) in + add_anonymous_leaf (in_constructor_implicits (consp, imps)) + | EvarRef _ -> assert false + +let declare_manual_implicits r l = match r with + | VarRef sp -> + add_anonymous_leaf (in_var_implicits (sp,Impl_manual l)) + | ConstRef sp -> + add_anonymous_leaf (in_constant_implicits (sp,Impl_manual l)) + | IndRef indp -> + add_anonymous_leaf (in_inductive_implicits (indp,Impl_manual l)) + | ConstructRef consp -> + add_anonymous_leaf (in_constructor_implicits (consp,Impl_manual l)) + | EvarRef _ -> + assert false + (*s Tests if declared implicit *) let is_implicit_constant sp = try let _ = Spmap.find sp !constants_table in true with Not_found -> false -let is_implicit_inductive_definition sp = - try let _ = Spmap.find sp !inductives_table in true with Not_found -> false +let is_implicit_inductive_definition indp = + try let _ = Indmap.find indp !inductives_table in true + with Not_found -> false let is_implicit_var sp = try let _ = Spmap.find sp !var_table in true with Not_found -> false @@ -178,21 +254,25 @@ let implicits_of_global = function type frozen_t = bool * implicits Spmap.t - * (implicits * implicits array) array Spmap.t + * implicits Indmap.t + * implicits Constrmap.t * implicits Spmap.t let init () = constants_table := Spmap.empty; - inductives_table := Spmap.empty; + inductives_table := Indmap.empty; + constructors_table := Constrmap.empty; var_table := Spmap.empty let freeze () = - (!implicit_args, !constants_table, !inductives_table, !var_table) + (!implicit_args, !constants_table, !inductives_table, + !constructors_table, !var_table) -let unfreeze (imps,ct,it,vt) = +let unfreeze (imps,ct,it,const,vt) = implicit_args := imps; constants_table := ct; inductives_table := it; + constructors_table := const; var_table := vt let _ = |