From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 21 Nov 2006 21:38:49 +0000 Subject: Imported Upstream version 8.1~gamma --- library/declare.ml | 26 ++++++++++++------------ library/global.ml | 6 +++--- library/goptions.ml | 4 ++-- library/impargs.ml | 12 +++++------ library/lib.ml | 57 ++++++++++++++++++++++++++-------------------------- library/libobject.ml | 4 ++-- library/library.ml | 6 +++--- library/nameops.ml | 6 +++++- library/nameops.mli | 4 +++- library/states.ml | 17 +++++++--------- 10 files changed, 73 insertions(+), 69 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index 81401a8e..e9e54cd3 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: declare.ml 8752 2006-04-27 19:37:33Z herbelin $ *) +(* $Id: declare.ml 9104 2006-09-01 11:04:44Z notin $ *) open Pp open Util @@ -150,18 +150,18 @@ let open_constant i ((sp,kn),_) = let cache_constant ((sp,kn),(cdt,dhyps,imps,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 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 (*s Registration as global tables and rollback. *) diff --git a/library/global.ml b/library/global.ml index 863d26b7..ab5d8956 100644 --- a/library/global.ml +++ b/library/global.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: global.ml 8723 2006-04-16 15:51:02Z herbelin $ *) +(* $Id: global.ml 9310 2006-10-28 19:35:09Z herbelin $ *) open Util open Names @@ -141,10 +141,10 @@ open Libnames let type_of_reference env = function | VarRef id -> Environ.named_type id env - | ConstRef c -> Environ.constant_type env c + | ConstRef c -> Typeops.type_of_constant env c | IndRef ind -> let specif = Inductive.lookup_mind_specif env ind in - Inductive.type_of_inductive specif + Inductive.type_of_inductive env specif | ConstructRef cstr -> let specif = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in diff --git a/library/goptions.ml b/library/goptions.ml index c220544c..4d36e1c5 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: goptions.ml 6304 2004-11-16 15:49:08Z sacerdot $ *) +(* $Id: goptions.ml 9060 2006-07-27 15:30:35Z notin $ *) (* This module manages customization parameters at the vernacular level *) @@ -253,7 +253,7 @@ let declare_option cast uncast unfreeze_function = write; init_function = (fun () -> write default); survive_module = false; - survive_section = true} + survive_section = false} in fun v -> add_anonymous_leaf (decl_obj v) else write diff --git a/library/impargs.ml b/library/impargs.ml index 68fc046c..67848d8f 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: impargs.ml 8845 2006-05-23 07:41:58Z herbelin $ *) +(* $Id: impargs.ml 9310 2006-10-28 19:35:09Z herbelin $ *) open Util open Names @@ -259,10 +259,9 @@ let list_of_implicits = function let constants_table = ref Cmap.empty -let compute_constant_implicits kn = +let compute_constant_implicits cst = let env = Global.env () in - let cb = lookup_constant kn env in - auto_implicits env (body_of_type cb.const_type) + auto_implicits env (Typeops.type_of_constant env cst) let constant_implicits sp = try Cmap.find sp !constants_table with Not_found -> No_impl @@ -282,12 +281,13 @@ let compute_mib_implicits kn = let ar = Array.to_list (Array.map (* No need to lift, arities contain no de Bruijn *) - (fun mip -> (Name mip.mind_typename, None, type_of_inductive (mib,mip))) + (fun mip -> + (Name mip.mind_typename, None, type_of_inductive env (mib,mip))) mib.mind_packets) in let env_ar = push_rel_context ar env in let imps_one_inductive i mip = let ind = (kn,i) in - let ar = type_of_inductive (mib,mip) 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)) mip.mind_nf_lc) diff --git a/library/lib.ml b/library/lib.ml index ba6b9c79..09200a5c 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: lib.ml 8852 2006-05-23 17:52:43Z notin $ *) +(* $Id: lib.ml 9133 2006-09-12 14:52:07Z notin $ *) open Pp open Util @@ -186,9 +186,9 @@ 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_leaves id objs = let oname = make_oname id in @@ -319,7 +319,7 @@ let end_compilation dir = | _, OpenedModtype _ -> error "There are some open module types" | _ -> assert false with - Not_found -> () + Not_found -> () in let module_p = function (_,CompilingLibrary _) -> true | x -> is_something_opened x @@ -331,16 +331,17 @@ let end_compilation dir = with Not_found -> anomaly "No module declared" in - let _ = match !comp_name with + let _ = + match !comp_name with | None -> anomaly "There should be a module name..." | Some m -> if m <> dir then anomaly ("The current open module has name "^ (string_of_dirpath m) ^ - " and not " ^ (string_of_dirpath m)); + " and not " ^ (string_of_dirpath m)); in let (after,_,before) = split_lib oname in - comp_name := None; - !path_prefix,after + comp_name := None; + !path_prefix,after (* Returns true if we are inside an opened module type *) let is_modtype () = @@ -444,15 +445,15 @@ let open_section id = let dir = extend_dirpath olddir id in let prefix = dir, (mp, extend_dirpath oldsec id) in let name = make_path id, make_kn id (* this makes little sense however *) in - if Nametab.exists_section dir then - errorlabstrm "open_section" (pr_id id ++ str " already exists"); - let sum = freeze_summaries() in - add_entry name (OpenedSection (prefix, sum)); - (*Pushed for the lifetime of the section: removed by unfrozing the summary*) - Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix); - path_prefix := prefix; - if !Options.xml_export then !xml_open_section id; - add_section () + if Nametab.exists_section dir then + errorlabstrm "open_section" (pr_id id ++ str " already exists"); + let sum = freeze_summaries() in + add_entry name (OpenedSection (prefix, sum)); + (*Pushed for the lifetime of the section: removed by unfrozing the summary*) + Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix); + path_prefix := prefix; + if !Options.xml_export then !xml_open_section id; + add_section () (* Restore lib_stk and summaries as before the section opening, and @@ -476,16 +477,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) -> ignore (add_leaf id o))) newdecls; + Cooking.clear_cooking_sharing (); + Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir) (*****************) (* Backtracking. *) diff --git a/library/libobject.ml b/library/libobject.ml index 7f383a3b..709fb1bb 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: libobject.ml 8752 2006-04-27 19:37:33Z herbelin $ *) +(* $Id: libobject.ml 9104 2006-09-01 11:04:44Z notin $ *) open Util open Names @@ -144,7 +144,7 @@ let apply_dyn_fun deflt f lobj = else anomaly ("Cannot find library functions for an object with tag "^tag) in - f dodecl + f dodecl with Failure "local to_apply_dyn_fun" -> deflt;; diff --git a/library/library.ml b/library/library.ml index cfd88ca0..43eeb695 100644 --- a/library/library.ml +++ b/library/library.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: library.ml 8877 2006-05-30 16:37:04Z notin $ *) +(* $Id: library.ml 9352 2006-11-07 16:12:10Z 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 = 08003 (* V8.0 final new syntax + new params in ind *) +let vo_magic_number = 080999 (* V8.1gamma *) let (raw_extern_library, raw_intern_library) = System.raw_extern_intern vo_magic_number ".vo" @@ -606,7 +606,7 @@ let save_library_to dir f = let di = Digest.file f' in System.marshal_out ch di; close_out ch - with e -> (warning ("Removed file "^f');close_out ch; Sys.remove f'; raise e) + with e -> (warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise e) (************************************************************************) (*s Display the memory use of a library. *) diff --git a/library/nameops.ml b/library/nameops.ml index 1c6a7d56..779f3389 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: nameops.ml 8727 2006-04-24 09:48:06Z herbelin $ *) +(* $Id: nameops.ml 9225 2006-10-09 15:59:23Z herbelin $ *) open Pp open Util @@ -154,6 +154,10 @@ let name_app f = function | Name id -> Name (f id) | Anonymous -> Anonymous +let name_fold_map f e = function + | Name id -> let (e,id) = f e id in (e,Name id) + | Anonymous -> e,Anonymous + let next_name_away_with_default default name l = match name with | Name str -> next_ident_away str l diff --git a/library/nameops.mli b/library/nameops.mli index 9d1722d4..8e291761 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 6616 2005-01-21 17:18:23Z herbelin $ i*) +(*i $Id: nameops.mli 9225 2006-10-09 15:59:23Z herbelin $ i*) open Names @@ -38,6 +38,8 @@ val out_name : name -> identifier val name_fold : (identifier -> 'a -> 'a) -> name -> 'a -> 'a val name_cons : name -> identifier list -> identifier list val name_app : (identifier -> identifier) -> name -> name +val name_fold_map : ('a -> identifier -> 'a * identifier) -> 'a -> name -> 'a * name + val pr_lab : label -> Pp.std_ppcmds diff --git a/library/states.ml b/library/states.ml index 3bb37a4d..169a3857 100644 --- a/library/states.ml +++ b/library/states.ml @@ -6,16 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: states.ml 6692 2005-02-06 13:03:51Z herbelin $ *) +(* $Id: states.ml 9100 2006-08-31 18:04:26Z herbelin $ *) open System type state = Lib.frozen * Summary.frozen -let get_state () = +let freeze () = (Lib.freeze(), Summary.freeze_summaries()) -let set_state (fl,fs) = +let unfreeze (fl,fs) = Lib.unfreeze fl; Summary.unfreeze_summaries fs @@ -23,17 +23,14 @@ let state_magic_number = 19764 let (extern_state,intern_state) = let (raw_extern, raw_intern) = extern_intern state_magic_number ".coq" in - (fun s -> raw_extern s (get_state())), - (fun s -> set_state (raw_intern (Library.get_load_paths ()) s)) + (fun s -> raw_extern s (freeze())), + (fun s -> unfreeze (raw_intern (Library.get_load_paths ()) s)) (* Rollback. *) -let freeze = get_state -let unfreeze = set_state - let with_heavy_rollback f x = - let st = get_state () in + let st = freeze () in try f x with reraise -> - (set_state st; raise reraise) + (unfreeze st; raise reraise) -- cgit v1.2.3