From 55ce117e8083477593cf1ff2e51a3641c7973830 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 13 Feb 2007 13:48:12 +0000 Subject: Imported Upstream version 8.1+dfsg --- library/declare.ml | 62 +++++---- library/dischargedhypsmap.ml | 16 +-- library/impargs.ml | 301 +++++++++++++++++++------------------------ library/impargs.mli | 13 +- library/lib.ml | 86 +++++++------ library/lib.mli | 8 +- library/libnames.ml | 19 ++- library/libnames.mli | 10 +- library/libobject.ml | 12 +- library/libobject.mli | 4 +- library/library.ml | 12 +- library/nameops.ml | 9 +- library/nameops.mli | 4 +- 13 files changed, 277 insertions(+), 279 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index e9e54cd3..02bdb1cf 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: declare.ml 9104 2006-09-01 11:04:44Z notin $ *) +(* $Id: declare.ml 9488 2007-01-17 11:11:58Z herbelin $ *) open Pp open Util @@ -136,7 +136,7 @@ let _ = Summary.declare_summary "CONSTANT" (* At load-time, the segment starting from the module name to the discharge *) (* section (if Remark or Fact) is needed to access a construction *) -let load_constant i ((sp,kn),(_,_,_,kind)) = +let load_constant i ((sp,kn),(_,_,kind)) = if Nametab.exists_cci sp then errorlabstrm "cache_constant" (pr_id (basename sp) ++ str " already exists"); @@ -147,21 +147,17 @@ let load_constant i ((sp,kn),(_,_,_,kind)) = let open_constant i ((sp,kn),_) = Nametab.push (Nametab.Exactly i) sp (ConstRef (constant_of_kn kn)) -let cache_constant ((sp,kn),(cdt,dhyps,imps,kind)) = +let cache_constant ((sp,kn),(cdt,dhyps,kind)) = let id = basename sp in let _,dir,_ = repr_kn kn in - if Idmap.mem id !vartab then - errorlabstrm "cache_constant" (pr_id id ++ str " already exists"); - if Nametab.exists_cci sp then - errorlabstrm "cache_constant" (pr_id id ++ str " already exists"); - let kn' = Global.add_constant dir id cdt in - assert (kn' = constant_of_kn kn); - Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn)); - add_section_constant kn' (Global.lookup_constant kn').const_hyps; - Dischargedhypsmap.set_discharged_hyps sp dhyps; - with_implicits imps declare_constant_implicits kn'; - Notation.declare_ref_arguments_scope (ConstRef kn'); - csttab := Spmap.add sp kind !csttab + if Idmap.mem id !vartab or Nametab.exists_cci sp then + errorlabstrm "cache_constant" (pr_id id ++ str " already exists"); + let kn' = Global.add_constant dir id cdt in + assert (kn' = constant_of_kn kn); + Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn)); + add_section_constant kn' (Global.lookup_constant kn').const_hyps; + Dischargedhypsmap.set_discharged_hyps sp dhyps; + csttab := Spmap.add sp kind !csttab (*s Registration as global tables and rollback. *) @@ -172,18 +168,18 @@ let discharged_hyps kn sechyps = let args = array_map_to_list destVar (instance_from_named_context sechyps) in List.rev (List.map (Libnames.make_path dir) args) -let discharge_constant ((sp,kn),(cdt,dhyps,imps,kind)) = +let discharge_constant ((sp,kn),(cdt,dhyps,kind)) = let con = constant_of_kn kn in let cb = Global.lookup_constant con in - let (repl1,_ as repl) = replacement_context () in - let sechyps = section_segment (ConstRef con) in + let repl = replacement_context () in + let sechyps = section_segment_of_constant con in let recipe = { d_from=cb; d_modlist=repl; d_abstract=sechyps } in - Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,imps,kind) + Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,kind) (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant_entry = ConstantEntry (ParameterEntry mkProp) -let dummy_constant (ce,_,imps,mk) = dummy_constant_entry,[],imps,mk +let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk let export_constant cst = Some (dummy_constant cst) @@ -210,9 +206,10 @@ let hcons_constant_declaration = function | cd -> cd let declare_constant_common id dhyps (cd,kind) = - let imps = implicits_flags () in - let (sp,kn) = add_leaf id (in_constant (cd,dhyps,imps,kind)) in + let (sp,kn) = add_leaf id (in_constant (cd,dhyps,kind)) in let kn = constant_of_kn kn in + declare_constant_implicits kn; + Notation.declare_ref_arguments_scope (ConstRef kn); kn let declare_constant_gen internal id (cd,kind) = @@ -261,16 +258,16 @@ let check_exists_inductive (sp,_) = let (_,id) = repr_path sp in errorlabstrm "" (pr_id id ++ str " already exists") -let load_inductive i ((sp,kn),(_,_,mie)) = +let load_inductive i ((sp,kn),(_,mie)) = let names = inductive_names sp kn mie in List.iter check_exists_inductive names; List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref) names -let open_inductive i ((sp,kn),(_,_,mie)) = +let open_inductive i ((sp,kn),(_,mie)) = let names = inductive_names sp kn mie in List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names -let cache_inductive ((sp,kn),(dhyps,imps,mie)) = +let cache_inductive ((sp,kn),(dhyps,mie)) = let names = inductive_names sp kn mie in List.iter check_exists_inductive names; let id = basename sp in @@ -279,15 +276,13 @@ let cache_inductive ((sp,kn),(dhyps,imps,mie)) = assert (kn'=kn); add_section_kn kn (Global.lookup_mind kn').mind_hyps; Dischargedhypsmap.set_discharged_hyps sp dhyps; - with_implicits imps declare_mib_implicits kn; - declare_inductive_argument_scopes kn mie; List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names -let discharge_inductive ((sp,kn),(dhyps,imps,mie)) = +let discharge_inductive ((sp,kn),(dhyps,mie)) = let mie = Global.lookup_mind kn in let repl = replacement_context () in - let sechyps = section_segment (IndRef (kn,0)) in - Some (discharged_hyps kn sechyps,imps, + let sechyps = section_segment_of_mutual_inductive kn in + Some (discharged_hyps kn sechyps, Discharge.process_inductive sechyps repl mie) let dummy_one_inductive_entry mie = { @@ -298,7 +293,7 @@ let dummy_one_inductive_entry mie = { } (* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_inductive_entry (_,imps,m) = ([],imps,{ +let dummy_inductive_entry (_,m) = ([],{ mind_entry_params = []; mind_entry_record = false; mind_entry_finite = true; @@ -318,11 +313,12 @@ let (in_inductive, out_inductive) = (* for initial declaration *) let declare_mind isrecord mie = - let imps = implicits_flags () in let id = match mie.mind_entry_inds with | ind::_ -> ind.mind_entry_typename | [] -> anomaly "cannot declare an empty list of inductives" in - let oname = add_leaf id (in_inductive ([],imps,mie)) in + let (sp,kn as oname) = add_leaf id (in_inductive ([],mie)) in + declare_mib_implicits kn; + declare_inductive_argument_scopes kn mie; !xml_declare_inductive (isrecord,oname); oname diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml index 2a3abda8..255f5e75 100644 --- a/library/dischargedhypsmap.ml +++ b/library/dischargedhypsmap.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: dischargedhypsmap.ml 6748 2005-02-18 22:17:50Z herbelin $ *) +(* $Id: dischargedhypsmap.ml 9488 2007-01-17 11:11:58Z herbelin $ *) open Util open Libnames @@ -24,21 +24,9 @@ type discharged_hyps = section_path list let discharged_hyps_map = ref Spmap.empty -let load_discharged_hyps_map _ (_,(sp,hyps)) = +let set_discharged_hyps sp hyps = discharged_hyps_map := Spmap.add sp hyps !discharged_hyps_map -let cache_discharged_hyps_map o = - load_discharged_hyps_map 1 o - -let (in_discharged_hyps_map, _) = - declare_object { (default_object "DISCHARGED-HYPS-MAP") with - cache_function = cache_discharged_hyps_map; - load_function = load_discharged_hyps_map; - export_function = (fun x -> Some x) } - -let set_discharged_hyps sp hyps = - add_anonymous_leaf (in_discharged_hyps_map (sp,hyps)) - let get_discharged_hyps sp = try Spmap.find sp !discharged_hyps_map diff --git a/library/impargs.ml b/library/impargs.ml index 67848d8f..8cea4737 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: impargs.ml 9310 2006-10-28 19:35:09Z herbelin $ *) +(* $Id: impargs.ml 9488 2007-01-17 11:11:58Z herbelin $ *) open Util open Names @@ -45,7 +45,7 @@ let is_contextual_implicit_args () = !contextual_implicit_args type implicits_flags = bool * bool * bool -let implicits_flags () = +let implicit_flags () = (!implicit_args, !strict_implicit_args, !contextual_implicit_args) let with_implicits (a,b,c) f x = @@ -167,12 +167,6 @@ let add_free_rels_until strict bound env m pos acc = (* calcule la liste des arguments implicites *) -let my_concrete_name avoid names t = function - | Anonymous -> Anonymous, avoid, Anonymous::names - | na -> - let id = Termops.next_name_not_occuring false na avoid names t in - Name id, id::avoid, Name id::names - let compute_implicits_gen strict contextual env t = let rec aux env avoid n names t = let t = whd_betadeltaiota env t in @@ -194,15 +188,50 @@ let compute_implicits_gen strict contextual env t = Array.to_list v | _ -> [] -let compute_implicits env t = - let strict = !strict_implicit_args in - let contextual = !contextual_implicit_args in +let compute_implicits_auto env (_,strict,contextual) t = let l = compute_implicits_gen strict contextual env t in List.map (function | (Name id, Some imp) -> Some (id,imp) | (Anonymous, Some _) -> anomaly "Unnamed implicit" | _ -> None) l +let compute_implicits env t = compute_implicits_auto env (implicit_flags()) t + +let set_implicit id imp = + Some (id,match imp with None -> Manual | Some imp -> imp) + +let compute_manual_implicits flags ref l = + let t = Global.type_of_global ref in + let autoimps = compute_implicits_gen false true (Global.env()) t in + let n = List.length autoimps in + if not (list_distinct l) then + error ("Some parameters are referred more than once"); + (* Compare with automatic implicits to recover printing data and names *) + let rec merge k l = function + | (Name id,imp)::imps -> + let l',imp = + try list_remove_first (ExplByPos k) l, set_implicit id imp + with Not_found -> + try list_remove_first (ExplByName id) l, set_implicit id imp + with Not_found -> + l, None in + imp :: merge (k+1) l' imps + | (Anonymous,imp)::imps -> + None :: merge (k+1) l imps + | [] when l = [] -> [] + | _ -> + match List.hd l with + | ExplByName id -> + error ("Wrong or not dependent implicit argument name: "^(string_of_id id)) + | ExplByPos i -> + if i<1 or i>n then + error ("Bad implicit argument number: "^(string_of_int i)) + else + errorlabstrm "" + (str "Cannot set implicit argument number " ++ int i ++ + str ": it has no name") in + merge 1 l autoimps + type implicit_status = (* None = Not implicit *) (identifier * implicit_explanation) option @@ -238,44 +267,18 @@ let positions_of_implicits = type strict_flag = bool (* true = strict *) type contextual_flag = bool (* true = contextual *) -type implicits = - | Impl_auto of strict_flag * contextual_flag * implicits_list - | Impl_manual of implicits_list - | No_impl - -let auto_implicits env ty = - if !implicit_args then - let l = compute_implicits env ty in - Impl_auto (!strict_implicit_args,!contextual_implicit_args,l) - else - No_impl - -let list_of_implicits = function - | Impl_auto (_,_,l) -> l - | Impl_manual l -> l - | No_impl -> [] - (*s Constants. *) -let constants_table = ref Cmap.empty - -let compute_constant_implicits cst = +let compute_constant_implicits flags cst = let env = Global.env () in - auto_implicits env (Typeops.type_of_constant env cst) - -let constant_implicits sp = - try Cmap.find sp !constants_table with Not_found -> No_impl + compute_implicits_auto env flags (Typeops.type_of_constant env cst) (*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 Indmap.empty - -let constructors_table = ref Constrmap.empty - -let compute_mib_implicits kn = +let compute_mib_implicits flags kn = let env = Global.env () in let mib = lookup_mind kn env in let ar = @@ -288,54 +291,55 @@ let compute_mib_implicits kn = let imps_one_inductive i mip = let ind = (kn,i) in let ar = type_of_inductive env (mib,mip) in - ((IndRef ind,auto_implicits env ar), - Array.mapi (fun j c -> (ConstructRef (ind,j+1),auto_implicits env_ar c)) + ((IndRef ind,compute_implicits_auto env flags ar), + Array.mapi (fun j c -> + (ConstructRef (ind,j+1),compute_implicits_auto env_ar flags c)) mip.mind_nf_lc) in Array.mapi imps_one_inductive mib.mind_packets -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 compute_all_mib_implicits flags kn = + let imps = compute_mib_implicits flags kn in + List.flatten + (array_map_to_list (fun (ind,cstrs) -> ind::Array.to_list cstrs) imps) (*s Variables. *) -let var_table = ref Idmap.empty - -let compute_var_implicits id = +let compute_var_implicits flags id = let env = Global.env () in let (_,_,ty) = lookup_named id env in - auto_implicits env ty - -let var_implicits id = - try Idmap.find id !var_table with Not_found -> No_impl + compute_implicits_auto env flags ty (* Implicits of a global reference. *) -let compute_global_implicits = function - | VarRef id -> compute_var_implicits id - | ConstRef kn -> compute_constant_implicits kn +let compute_global_implicits flags = function + | VarRef id -> compute_var_implicits flags id + | ConstRef kn -> compute_constant_implicits flags kn | IndRef (kn,i) -> - let ((_,imps),_) = (compute_mib_implicits kn).(i) in imps + let ((_,imps),_) = (compute_mib_implicits flags kn).(i) in imps | ConstructRef ((kn,i),j) -> - let (_,cimps) = (compute_mib_implicits kn).(i) in snd cimps.(j-1) + let (_,cimps) = (compute_mib_implicits flags kn).(i) in snd cimps.(j-1) (* Caching implicits *) -let cache_implicits_decl (r,imps) = - match r with - | VarRef id -> - var_table := Idmap.add id imps !var_table - | ConstRef kn -> - constants_table := Cmap.add kn imps !constants_table - | IndRef indp -> - inductives_table := Indmap.add indp imps !inductives_table; - | ConstructRef consp -> - constructors_table := Constrmap.add consp imps !constructors_table +type implicit_interactive_request = ImplAuto | ImplManual of explicitation list + +type implicit_discharge_request = + | ImplNoDischarge + | ImplConstant of constant * implicits_flags + | ImplMutualInductive of kernel_name * implicits_flags + | ImplInteractive of global_reference * implicits_flags * + implicit_interactive_request -let load_implicits _ (_,l) = List.iter cache_implicits_decl l +let implicits_table = ref Refmap.empty + +let implicits_of_global ref = + try Refmap.find ref !implicits_table with Not_found -> [] + +let cache_implicits_decl (ref,imps) = + implicits_table := Refmap.add ref imps !implicits_table + +let load_implicits _ (_,(_,l)) = List.iter cache_implicits_decl l let cache_implicits o = load_implicits 1 o @@ -343,121 +347,88 @@ let cache_implicits o = let subst_implicits_decl subst (r,imps as o) = let r' = fst (subst_global subst r) in if r==r' then o else (r',imps) -let subst_implicits (_,subst,l) = - list_smartmap (subst_implicits_decl subst) l - -let (in_implicits, _) = +let subst_implicits (_,subst,(req,l)) = + (ImplNoDischarge,list_smartmap (subst_implicits_decl subst) l) + +let discharge_implicits (_,(req,l)) = + match req with + | ImplNoDischarge -> None + | ImplInteractive (ref,flags,exp) -> + Some (ImplInteractive (pop_global_reference ref,flags,exp),l) + | ImplConstant (con,flags) -> + Some (ImplConstant (pop_con con,flags),l) + | ImplMutualInductive (kn,flags) -> + Some (ImplMutualInductive (pop_kn kn,flags),l) + +let rebuild_implicits (req,l) = + let l' = match req with + | ImplNoDischarge -> assert false + | ImplConstant (con,flags) -> + [ConstRef con,compute_constant_implicits flags con] + | ImplMutualInductive (kn,flags) -> + compute_all_mib_implicits flags kn + | ImplInteractive (ref,flags,o) -> + match o with + | ImplAuto -> [ref,compute_global_implicits flags ref] + | ImplManual l -> + error "Discharge of global manually given implicit arguments not implemented" in + (req,l') + + +let (inImplicits, _) = declare_object {(default_object "IMPLICITS") with cache_function = cache_implicits; load_function = load_implicits; subst_function = subst_implicits; classify_function = (fun (_,x) -> Substitute x); + discharge_function = discharge_implicits; + rebuild_function = rebuild_implicits; export_function = (fun x -> Some x) } -let declare_implicits_gen r = - add_anonymous_leaf (in_implicits [r,compute_global_implicits r]) +let declare_implicits_gen req flags ref = + let imps = compute_global_implicits flags ref in + add_anonymous_leaf (inImplicits (req,[ref,imps])) -let declare_implicits r = - with_implicits - (true,!strict_implicit_args,!contextual_implicit_args) - declare_implicits_gen r +let declare_implicits local ref = + let flags = (true,!strict_implicit_args,!contextual_implicit_args) in + let req = + if local then ImplNoDischarge else ImplInteractive(ref,flags,ImplAuto) in + declare_implicits_gen req flags ref let declare_var_implicits id = - if !implicit_args then declare_implicits_gen (VarRef id) + if !implicit_args then + declare_implicits_gen ImplNoDischarge (implicit_flags ()) (VarRef id) -let declare_constant_implicits kn = - if !implicit_args then declare_implicits_gen (ConstRef kn) +let declare_constant_implicits con = + if !implicit_args then + let flags = implicit_flags () in + declare_implicits_gen (ImplConstant (con,flags)) flags (ConstRef con) let declare_mib_implicits kn = if !implicit_args then - let imps = compute_mib_implicits kn in - let imps = array_map_to_list - (fun (ind,cstrs) -> ind::(Array.to_list cstrs)) imps in - add_anonymous_leaf (in_implicits (List.flatten imps)) - -let implicits_of_global_gen = function - | VarRef id -> var_implicits id - | ConstRef sp -> constant_implicits sp - | IndRef isp -> inductive_implicits isp - | ConstructRef csp -> constructor_implicits csp - -let implicits_of_global r = - list_of_implicits (implicits_of_global_gen r) + let flags = implicit_flags () in + let imps = array_map_to_list + (fun (ind,cstrs) -> ind::(Array.to_list cstrs)) + (compute_mib_implicits flags kn) in + add_anonymous_leaf + (inImplicits (ImplMutualInductive (kn,flags),List.flatten imps)) (* Declare manual implicits *) -let set_implicit id imp = - Some (id,match imp with None -> Manual | Some imp -> imp) - -let declare_manual_implicits r l = - let t = Global.type_of_global r in - let autoimps = compute_implicits_gen false true (Global.env()) t in - let n = List.length autoimps in - if not (list_distinct l) then - error ("Some parameters are referred more than once"); - (* Compare with automatic implicits to recover printing data and names *) - let rec merge k l = function - | (Name id,imp)::imps -> - let l',imp = - try list_remove_first (ExplByPos k) l, set_implicit id imp - with Not_found -> - try list_remove_first (ExplByName id) l, set_implicit id imp - with Not_found -> - l, None in - imp :: merge (k+1) l' imps - | (Anonymous,imp)::imps -> - None :: merge (k+1) l imps - | [] when l = [] -> [] - | _ -> - match List.hd l with - | ExplByName id -> - error ("Wrong or not dependent implicit argument name: "^(string_of_id id)) - | ExplByPos i -> - if i<1 or i>n then - error ("Bad implicit argument number: "^(string_of_int i)) - else - errorlabstrm "" - (str "Cannot set implicit argument number " ++ int i ++ - str ": it has no name") in - let l = Impl_manual (merge 1 l autoimps) in - add_anonymous_leaf (in_implicits [r,l]) - -(* Tests if declared implicit *) - -let test = function - | No_impl | Impl_manual _ -> false,false,false - | Impl_auto (s,c,_) -> true,s,c - -let test_if_implicit find a = - try let b = find a in test b - with Not_found -> (false,false,false) - -let is_implicit_constant sp = - test_if_implicit (Cmap.find sp) !constants_table - -let is_implicit_inductive_definition indp = - test_if_implicit (Indmap.find (indp,0)) !inductives_table - -let is_implicit_var id = - test_if_implicit (Idmap.find id) !var_table +let declare_manual_implicits local ref l = + let flags = !implicit_args,!strict_implicit_args,!contextual_implicit_args in + let l' = compute_manual_implicits flags ref l in + let req = + if local or isVarRef ref then ImplNoDischarge + else ImplInteractive(ref,flags,ImplManual l) + in + add_anonymous_leaf (inImplicits (req,[ref,l'])) (*s Registration as global tables *) -let init () = - constants_table := Cmap.empty; - inductives_table := Indmap.empty; - constructors_table := Constrmap.empty; - var_table := Idmap.empty - -let freeze () = - (!constants_table, !inductives_table, - !constructors_table, !var_table) - -let unfreeze (ct,it,const,vt) = - constants_table := ct; - inductives_table := it; - constructors_table := const; - var_table := vt +let init () = implicits_table := Refmap.empty +let freeze () = !implicits_table +let unfreeze t = implicits_table := t let _ = Summary.declare_summary "implicits" diff --git a/library/impargs.mli b/library/impargs.mli index 671d195c..64ce0360 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: impargs.mli 7732 2005-12-26 13:51:24Z herbelin $ i*) +(*i $Id: impargs.mli 9488 2007-01-17 11:11:58Z herbelin $ i*) (*i*) open Names @@ -51,17 +51,10 @@ val declare_var_implicits : variable -> unit val declare_constant_implicits : constant -> unit val declare_mib_implicits : mutual_inductive -> unit -val declare_implicits : global_reference -> unit +val declare_implicits : bool -> global_reference -> unit (* Manual declaration of which arguments are expected implicit *) -val declare_manual_implicits : global_reference -> +val declare_manual_implicits : bool -> global_reference -> Topconstr.explicitation list -> unit -(* Get implicit arguments *) -val is_implicit_constant : constant -> implicits_flags -val is_implicit_inductive_definition : mutual_inductive -> implicits_flags -val is_implicit_var : variable -> implicits_flags - val implicits_of_global : global_reference -> implicits_list - -val implicits_flags : unit -> implicits_flags diff --git a/library/lib.ml b/library/lib.ml index 09200a5c..213a1d19 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: lib.ml 9133 2006-09-12 14:52:07Z notin $ *) +(* $Id: lib.ml 9488 2007-01-17 11:11:58Z herbelin $ *) open Pp open Util @@ -186,9 +186,15 @@ let add_leaf id obj = if fst (current_prefix ()) = initial_path then error ("No session module started (use -top dir)"); let oname = make_oname id in - cache_object (oname,obj); - add_entry oname (Leaf obj); - oname + cache_object (oname,obj); + add_entry oname (Leaf obj); + oname + +let add_discharged_leaf id obj = + let oname = make_oname id in + let newobj = rebuild_object obj in + cache_object (oname,newobj); + add_entry oname (Leaf newobj) let add_leaves id objs = let oname = make_oname id in @@ -371,10 +377,17 @@ let what_is_opened () = find_entry_p is_something_opened (* Discharge tables *) +(* At each level of section, we remember + - the list of variables in this section + - the list of variables on which each constant depends in this section + - the list of variables on which each inductive depends in this section + - the list of substitution to do at section closing +*) + +type abstr_list = Sign.named_context Cmap.t * Sign.named_context KNmap.t + let sectab = - ref ([] : (identifier list * - (identifier array Cmap.t * identifier array KNmap.t) * - (Sign.named_context Cmap.t * Sign.named_context KNmap.t)) list) + ref ([] : (identifier list * Cooking.work_list * abstr_list) list) let add_section () = sectab := ([],(Cmap.empty,KNmap.empty),(Cmap.empty,KNmap.empty)) :: !sectab @@ -407,16 +420,18 @@ let add_section_constant kn = let replacement_context () = pi2 (List.hd !sectab) -let section_segment = function - | VarRef id -> - [] - | ConstRef con -> - Cmap.find con (fst (pi3 (List.hd !sectab))) - | IndRef (kn,_) | ConstructRef ((kn,_),_) -> - KNmap.find kn (snd (pi3 (List.hd !sectab))) +let section_segment_of_constant con = + Cmap.find con (fst (pi3 (List.hd !sectab))) + +let section_segment_of_mutual_inductive kn = + KNmap.find kn (snd (pi3 (List.hd !sectab))) -let section_instance r = - Sign.instance_from_named_context (List.rev (section_segment r)) +let section_instance = function + | VarRef id -> [||] + | ConstRef con -> + Cmap.find con (fst (pi2 (List.hd !sectab))) + | IndRef (kn,_) | ConstructRef ((kn,_),_) -> + KNmap.find kn (snd (pi2 (List.hd !sectab))) let init () = sectab := [] let freeze () = !sectab @@ -459,11 +474,14 @@ let open_section id = (* Restore lib_stk and summaries as before the section opening, and add a ClosedSection object. *) -let discharge_item = function - | ((sp,_ as oname),Leaf lobj) -> +let discharge_item ((sp,_ as oname),e) = + match e with + | Leaf lobj -> option_map (fun o -> (basename sp,o)) (discharge_object (oname,lobj)) - | _ -> - None + | FrozenState _ -> None + | ClosedSection -> None + | OpenedSection _ | OpenedModtype _ | OpenedModule _ | CompilingLibrary _ -> + anomaly "discharge_item" let close_section id = let oname,fs = @@ -477,16 +495,16 @@ let close_section id = error "no opened section" in let (secdecls,_,before) = split_lib oname in - lib_stk := before; - let full_olddir = fst !path_prefix in - pop_path_prefix (); - add_entry (make_oname id) ClosedSection; - if !Options.xml_export then !xml_close_section id; - let newdecls = List.map discharge_item secdecls in - Summary.section_unfreeze_summaries fs; - List.iter (option_iter (fun (id,o) -> ignore (add_leaf id o))) newdecls; - Cooking.clear_cooking_sharing (); - Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir) + lib_stk := before; + let full_olddir = fst !path_prefix in + pop_path_prefix (); + add_entry (make_oname id) ClosedSection; + if !Options.xml_export then !xml_close_section id; + let newdecls = List.map discharge_item secdecls in + Summary.section_unfreeze_summaries fs; + List.iter (option_iter (fun (id,o) -> add_discharged_leaf id o)) newdecls; + Cooking.clear_cooking_sharing (); + Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir) (*****************) (* Backtracking. *) @@ -660,14 +678,6 @@ let remove_section_part ref = (************************) (* Discharging names *) -let pop_kn kn = - let (mp,dir,l) = Names.repr_kn kn in - Names.make_kn mp (dirpath_prefix dir) l - -let pop_con con = - let (mp,dir,l) = Names.repr_con con in - Names.make_con mp (dirpath_prefix dir) l - let con_defined_in_sec kn = let _,dir,_ = repr_con kn in dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ()) diff --git a/library/lib.mli b/library/lib.mli index e33c3aca..ec896de5 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: lib.mli 8852 2006-05-23 17:52:43Z notin $ i*) +(*i $Id: lib.mli 9488 2007-01-17 11:11:58Z herbelin $ i*) (*i*) open Util @@ -160,8 +160,10 @@ val set_xml_close_section : (identifier -> unit) -> unit (*s Section management for discharge *) -val section_segment : global_reference -> Sign.named_context -val section_instance : global_reference -> Term.constr array +val section_segment_of_constant : constant -> Sign.named_context +val section_segment_of_mutual_inductive: mutual_inductive -> Sign.named_context + +val section_instance : global_reference -> identifier array val add_section_variable : identifier -> unit val add_section_constant : constant -> Sign.named_context -> unit diff --git a/library/libnames.ml b/library/libnames.ml index 48a7565e..07c9ad23 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: libnames.ml 8768 2006-04-28 14:25:31Z notin $ i*) +(*i $Id: libnames.ml 9488 2007-01-17 11:11:58Z herbelin $ i*) open Pp open Util @@ -21,6 +21,8 @@ type global_reference = | IndRef of inductive | ConstructRef of constructor +let isVarRef = function VarRef _ -> true | _ -> false + let subst_global subst ref = match ref with | VarRef var -> ref, mkVar var | ConstRef kn -> @@ -264,3 +266,18 @@ let loc_of_reference = function | Qualid (loc,qid) -> loc | Ident (loc,id) -> loc +(* popping one level of section in global names *) + +let pop_con con = + let (mp,dir,l) = repr_con con in + Names.make_con mp (dirpath_prefix dir) l + +let pop_kn kn = + let (mp,dir,l) = repr_kn kn in + Names.make_kn mp (dirpath_prefix dir) l + +let pop_global_reference = function + | ConstRef con -> ConstRef (pop_con con) + | IndRef (kn,i) -> IndRef (pop_kn kn,i) + | ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j) + | VarRef id -> anomaly "VarRef not poppable" diff --git a/library/libnames.mli b/library/libnames.mli index ab2185a6..9bf6918e 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: libnames.mli 8768 2006-04-28 14:25:31Z notin $ i*) +(*i $Id: libnames.mli 9488 2007-01-17 11:11:58Z herbelin $ i*) (*i*) open Pp @@ -23,6 +23,8 @@ type global_reference = | IndRef of inductive | ConstructRef of constructor +val isVarRef : global_reference -> bool + val subst_global : substitution -> global_reference -> global_reference * constr (* Turn a global reference into a construction *) @@ -141,3 +143,9 @@ val qualid_of_reference : reference -> qualid located val string_of_reference : reference -> string val pr_reference : reference -> std_ppcmds val loc_of_reference : reference -> loc + +(* popping one level of section in global names *) + +val pop_con : constant -> constant +val pop_kn : kernel_name -> kernel_name +val pop_global_reference : global_reference -> global_reference diff --git a/library/libobject.ml b/library/libobject.ml index 709fb1bb..eaaa1be1 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: libobject.ml 9104 2006-09-01 11:04:44Z notin $ *) +(* $Id: libobject.ml 9488 2007-01-17 11:11:58Z herbelin $ *) open Util open Names @@ -37,6 +37,7 @@ type 'a object_declaration = { classify_function : object_name * 'a -> 'a substitutivity; subst_function : object_name * substitution * 'a -> 'a; discharge_function : object_name * 'a -> 'a option; + rebuild_function : 'a -> 'a; export_function : 'a -> 'a option } let yell s = anomaly s @@ -50,6 +51,7 @@ let default_object s = { yell ("The object "^s^" does not know how to substitute!")); classify_function = (fun (_,obj) -> Keep obj); discharge_function = (fun _ -> None); + rebuild_function = (fun x -> x); export_function = (fun _ -> None)} @@ -75,6 +77,7 @@ type dynamic_object_declaration = { dyn_subst_function : object_name * substitution * obj -> obj; dyn_classify_function : object_name * obj -> obj substitutivity; dyn_discharge_function : object_name * obj -> obj option; + dyn_rebuild_function : obj -> obj; dyn_export_function : obj -> obj option } let object_tag lobj = Dyn.tag lobj @@ -112,6 +115,9 @@ let declare_object odecl = option_map infun (odecl.discharge_function (oname,outfun lobj)) else anomaly "somehow we got the wrong dynamic object in the dischargefun" + and rebuild lobj = + if Dyn.tag lobj = na then infun (odecl.rebuild_function (outfun lobj)) + else anomaly "somehow we got the wrong dynamic object in the rebuildfun" and exporter lobj = if Dyn.tag lobj = na then option_map infun (odecl.export_function (outfun lobj)) @@ -125,6 +131,7 @@ let declare_object odecl = dyn_subst_function = substituter; dyn_classify_function = classifier; dyn_discharge_function = discharge; + dyn_rebuild_function = rebuild; dyn_export_function = exporter }; (infun,outfun) @@ -166,5 +173,8 @@ let classify_object ((_,lobj) as node) = let discharge_object ((_,lobj) as node) = apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj +let rebuild_object lobj = + apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function lobj) lobj + let export_object lobj = apply_dyn_fun None (fun d -> d.dyn_export_function lobj) lobj diff --git a/library/libobject.mli b/library/libobject.mli index 88a12db9..376da1f5 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: libobject.mli 6748 2005-02-18 22:17:50Z herbelin $ i*) +(*i $Id: libobject.mli 9488 2007-01-17 11:11:58Z herbelin $ i*) (*i*) open Names @@ -71,6 +71,7 @@ type 'a object_declaration = { classify_function : object_name * 'a -> 'a substitutivity; subst_function : object_name * substitution * 'a -> 'a; discharge_function : object_name * 'a -> 'a option; + rebuild_function : 'a -> 'a; export_function : 'a -> 'a option } (* The default object is a "Keep" object with empty methods. @@ -105,4 +106,5 @@ val subst_object : object_name * substitution * obj -> obj val classify_object : object_name * obj -> obj substitutivity val export_object : obj -> obj option val discharge_object : object_name * obj -> obj option +val rebuild_object : obj -> obj val relax : bool -> unit diff --git a/library/library.ml b/library/library.ml index 43eeb695..b68c3eb5 100644 --- a/library/library.ml +++ b/library/library.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: library.ml 9352 2006-11-07 16:12:10Z notin $ *) +(* $Id: library.ml 9637 2007-02-10 08:32:28Z notin $ *) open Pp open Util @@ -300,7 +300,7 @@ let (in_import, out_import) = (*s Loading from disk to cache (preparation phase) *) -let vo_magic_number = 080999 (* V8.1gamma *) +let vo_magic_number = 080100 (* V8.1 *) let (raw_extern_library, raw_intern_library) = System.raw_extern_intern vo_magic_number ".vo" @@ -591,6 +591,12 @@ let current_deps () = let current_reexports () = List.map (fun m -> m.library_name) !libraries_exports_list +let error_recursively_dependent_library dir = + errorlabstrm "" + (str "Unable to use logical name" ++ spc() ++ pr_dirpath dir ++ spc() ++ + str "to save current library" ++ spc() ++ str"because" ++ spc() ++ + str "it already depends on a library of this name.") + let save_library_to dir f = let cenv, seg = Declaremods.end_library dir in let md = { @@ -599,6 +605,8 @@ let save_library_to dir f = md_objects = seg; md_deps = current_deps (); md_imports = current_reexports () } in + if List.mem_assoc dir md.md_deps then + error_recursively_dependent_library dir; let (f',ch) = raw_extern_library f in try System.marshal_out ch md; diff --git a/library/nameops.ml b/library/nameops.ml index 779f3389..6d0ad8ef 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: nameops.ml 9225 2006-10-09 15:59:23Z herbelin $ *) +(* $Id: nameops.ml 9429 2006-12-12 08:01:03Z herbelin $ *) open Pp open Util @@ -20,8 +20,6 @@ let pr_name = function | Anonymous -> str "_" | Name id -> pr_id id -let wildcard = id_of_string "_" - (* Utilities *) let code_of_0 = Char.code '0' @@ -163,10 +161,7 @@ let next_name_away_with_default default name l = | Name str -> next_ident_away str l | Anonymous -> next_ident_away (id_of_string default) l -let next_name_away name l = - match name with - | Name str -> next_ident_away str l - | Anonymous -> id_of_string "_" +let next_name_away = next_name_away_with_default "H" let pr_lab l = str (string_of_label l) diff --git a/library/nameops.mli b/library/nameops.mli index 8e291761..25c4ea56 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: nameops.mli 9225 2006-10-09 15:59:23Z herbelin $ i*) +(*i $Id: nameops.mli 9429 2006-12-12 08:01:03Z herbelin $ i*) open Names @@ -14,8 +14,6 @@ open Names val pr_id : identifier -> Pp.std_ppcmds val pr_name : name -> Pp.std_ppcmds -val wildcard : identifier - val make_ident : string -> int option -> identifier val repr_ident : identifier -> string * int option -- cgit v1.2.3