From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 16 Jun 2006 14:41:51 +0000 Subject: Imported Upstream version 8.0pl3+8.1beta --- library/declare.ml | 4 +- library/declaremods.ml | 123 ++++++++++++++++++++++++------------------------- library/global.ml | 21 +++++---- library/global.mli | 19 +++----- library/impargs.ml | 9 ++-- library/lib.ml | 24 ++++++++-- library/lib.mli | 5 +- library/libnames.ml | 10 +++- library/libnames.mli | 4 +- library/libobject.ml | 6 +-- library/library.ml | 53 +++++++++++---------- library/library.mli | 3 +- library/nameops.ml | 4 +- 13 files changed, 157 insertions(+), 128 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index b1e55c20..81401a8e 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: declare.ml 7941 2006-01-28 23:07:59Z herbelin $ *) +(* $Id: declare.ml 8752 2006-04-27 19:37:33Z herbelin $ *) open Pp open Util @@ -204,7 +204,7 @@ let hcons_constant_declaration = function let (hcons1_constr,_) = hcons_constr (hcons_names()) in DefinitionEntry { const_entry_body = hcons1_constr ce.const_entry_body; - const_entry_type = option_app hcons1_constr ce.const_entry_type; + const_entry_type = option_map hcons1_constr ce.const_entry_type; const_entry_opaque = ce.const_entry_opaque; const_entry_boxed = ce.const_entry_boxed } | cd -> cd diff --git a/library/declaremods.ml b/library/declaremods.ml index 3b2196a5..aac2b599 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declaremods.ml 7720 2005-12-24 00:25:55Z herbelin $ i*) +(*i $Id: declaremods.ml 8752 2006-04-27 19:37:33Z herbelin $ i*) open Pp open Util @@ -122,6 +122,18 @@ let msid_of_prefix (_,(mp,sec)) = anomaly ("Non-empty section in module name!" ^ string_of_mp mp ^ "." ^ string_of_dirpath sec) +(* Check that a module type is not functorial *) + +let rec check_sig env = function + | MTBident kn -> check_sig env (Environ.lookup_modtype kn env) + | MTBsig _ -> () + | MTBfunsig _ -> Modops.error_result_must_be_signature () + +let rec check_sig_entry env = function + | MTEident kn -> check_sig env (Environ.lookup_modtype kn env) + | MTEsig _ -> () + | MTEfunsig _ -> Modops.error_result_must_be_signature () + | MTEwith (mte,_) -> check_sig_entry env mte (* This function checks if the type calculated for the module [mp] is a subtype of [sub_mtb]. Uses only the global environment. *) @@ -434,58 +446,47 @@ let rec get_some_body mty env = match mty with replace_module (get_some_body mty env) id (Environ.lookup_module mp env) -let intern_args interp_modtype (env,oldargs) (idl,arg) = +let intern_args interp_modtype (idl,arg) = let lib_dir = Lib.library_dp() in let mbids = List.map (fun (_,id) -> make_mbid lib_dir (string_of_id id)) idl in - let mty = interp_modtype env arg in + let mty = interp_modtype (Global.env()) arg in let dirs = List.map (fun (_,id) -> make_dirpath [id]) idl in - let mps = List.map (fun mbid -> MPbound mbid) mbids in let substobjs = get_modtype_substobjs mty in - let substituted's = - List.map2 - (fun dir mp -> dir, mp, subst_substobjs dir mp substobjs) - dirs mps - in - List.iter - (fun (dir, mp, substituted) -> - do_module false "interp" load_objects 1 dir mp substobjs substituted) - substituted's; - let body = Modops.module_body_of_type (get_some_body mty env) in - let env = - List.fold_left (fun env mp -> Modops.add_module mp body env) env mps - in - env, List.map (fun mbid -> mbid,mty) mbids :: oldargs - + List.map2 + (fun dir mbid -> + Global.add_module_parameter mbid mty; + let mp = MPbound mbid in + let substituted = subst_substobjs dir mp substobjs in + do_module false "interp" load_objects 1 dir mp substobjs substituted; + (mbid,mty)) + dirs mbids + let start_module interp_modtype export id args res_o = let fs = Summary.freeze_summaries () in - let env = Global.env () in - let env,arg_entries_revlist = - List.fold_left (intern_args interp_modtype) (env,[]) args - in - let arg_entries = List.concat (List.rev arg_entries_revlist) in + + let mp = Global.start_module id in + let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in let res_entry_o, sub_body_o = match res_o with None -> None, None - | Some (res, true) -> - Some (interp_modtype env res), None - | Some (res, false) -> - (* If the module type is non-restricting, we must translate it - here to catch errors as early as possible. If it is - estricting, the kernel takes care of it. *) - let sub_mte = - List.fold_right - (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte)) - arg_entries - (interp_modtype env res) - in - let sub_mtb = - Mod_typing.translate_modtype (Global.env()) sub_mte - in + | Some (res, restricted) -> + (* we translate the module here to catch errors as early as possible *) + let mte = interp_modtype (Global.env()) res in + check_sig_entry (Global.env()) mte; + if restricted then + Some mte, None + else + let mtb = Mod_typing.translate_modtype (Global.env()) mte in + let sub_mtb = + List.fold_right + (fun (arg_id,arg_t) mte -> + let arg_t = Mod_typing.translate_modtype (Global.env()) arg_t + in MTBfunsig(arg_id,arg_t,mte)) + arg_entries mtb + in None, Some sub_mtb in - let mp = Global.start_module id arg_entries res_entry_o in - let mbids = List.map fst arg_entries in openmod_info:=(mbids,res_entry_o,sub_body_o); let prefix = Lib.start_module export id mp fs in @@ -496,8 +497,8 @@ let start_module interp_modtype export id args res_o = let end_module id = let oldoname,oldprefix,fs,lib_stack = Lib.end_module id in - let mp = Global.end_module id in let mbids, res_o, sub_o = !openmod_info in + let mp = Global.end_module id res_o in begin match sub_o with None -> () @@ -584,7 +585,7 @@ let register_library dir cenv objs digest = let msid,substitute,keep = objs in let substobjs = empty_subst, [], msid, substitute in let substituted = subst_substobjs dir mp substobjs in - let objects = option_app (fun seg -> seg@keep) substituted in + let objects = option_map (fun seg -> seg@keep) substituted in let modobjs = substobjs, objects in Hashtbl.add library_cache dir modobjs; modobjs @@ -644,13 +645,9 @@ let import_module export mp = let start_modtype interp_modtype id args = let fs = Summary.freeze_summaries () in - let env = Global.env () in - let env,arg_entries_revlist = - List.fold_left (intern_args interp_modtype) (env,[]) args - in - let arg_entries = List.concat (List.rev arg_entries_revlist) in - let mp = Global.start_modtype id arg_entries in + let mp = Global.start_modtype id in + let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in let mbids = List.map fst arg_entries in openmodtype_info := mbids; @@ -685,12 +682,11 @@ let end_modtype id = let declare_modtype interp_modtype id args mty = let fs = Summary.freeze_summaries () in - let env = Global.env () in - let env,arg_entries_revlist = - List.fold_left (intern_args interp_modtype) (env,[]) args - in - let arg_entries = List.concat (List.rev arg_entries_revlist) in - let base_mty = interp_modtype env mty in + + let _ = Global.start_modtype id in + let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in + + let base_mty = interp_modtype (Global.env()) mty in let entry = List.fold_right (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte)) @@ -730,27 +726,25 @@ let rec get_module_substobjs env = function let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = - let fs = Summary.freeze_summaries () in - let env = Global.env () in - let env,arg_entries_revlist = - List.fold_left (intern_args interp_modtype) (env,[]) args - in - let arg_entries = List.concat (List.rev arg_entries_revlist) in + + let _ = Global.start_module id in + let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in + let mty_entry_o, mty_sub_o = match mty_o with None -> None, None | (Some (mty, true)) -> Some (List.fold_right (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte)) arg_entries - (interp_modtype env mty)), + (interp_modtype (Global.env()) mty)), None | (Some (mty, false)) -> None, Some (List.fold_right (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte)) arg_entries - (interp_modtype env mty)) + (interp_modtype (Global.env()) mty)) in let mexpr_entry_o = match mexpr_o with None -> None @@ -758,12 +752,13 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = Some (List.fold_right (fun (mbid,mte) me -> MEfunctor(mbid,mte,me)) arg_entries - (interp_modexpr env mexpr)) + (interp_modexpr (Global.env()) mexpr)) in let entry = {mod_entry_type = mty_entry_o; mod_entry_expr = mexpr_entry_o } in + let env = Global.env() in let substobjs = match entry with | {mod_entry_type = Some mte} -> get_modtype_substobjs mte diff --git a/library/global.ml b/library/global.ml index b4d3a7ff..863d26b7 100644 --- a/library/global.ml +++ b/library/global.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: global.ml 7639 2005-12-02 10:01:15Z gregoire $ *) +(* $Id: global.ml 8723 2006-04-16 15:51:02Z herbelin $ *) open Util open Names @@ -73,22 +73,27 @@ let add_constraints c = global_env := add_constraints c !global_env let set_engagement c = global_env := set_engagement c !global_env -let start_module id params mtyo = +let start_module id = let l = label_of_id id in - let mp,newenv = start_module l params mtyo !global_env in + let mp,newenv = start_module l !global_env in global_env := newenv; mp - -let end_module id = + +let end_module id mtyo = let l = label_of_id id in - let mp,newenv = end_module l !global_env in + let mp,newenv = end_module l mtyo !global_env in global_env := newenv; mp -let start_modtype id params = +let add_module_parameter mbid mte = + let newenv = add_module_parameter mbid mte !global_env in + global_env := newenv + + +let start_modtype id = let l = label_of_id id in - let mp,newenv = start_modtype l params !global_env in + let mp,newenv = start_modtype l !global_env in global_env := newenv; mp diff --git a/library/global.mli b/library/global.mli index 278b9e65..96965465 100644 --- a/library/global.mli +++ b/library/global.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: global.mli 7899 2006-01-20 16:35:03Z barras $ i*) +(*i $Id: global.mli 8723 2006-04-16 15:51:02Z herbelin $ i*) (*i*) open Names @@ -63,20 +63,13 @@ val set_engagement : engagement -> unit (* [start_*] functions return the [module_path] valid for components of the started module / module type *) -val start_module : - identifier -> (mod_bound_id * module_type_entry) list - -> module_type_entry option - -> module_path +val start_module : identifier -> module_path +val end_module : identifier -> module_type_entry option -> module_path -val end_module : - identifier -> module_path +val add_module_parameter : mod_bound_id -> module_type_entry -> unit -val start_modtype : - identifier -> (mod_bound_id * module_type_entry) list - -> module_path - -val end_modtype : - identifier -> kernel_name +val start_modtype : identifier -> module_path +val end_modtype : identifier -> kernel_name (* Queries *) diff --git a/library/impargs.ml b/library/impargs.ml index 08ae2aa5..68fc046c 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: impargs.ml 8672 2006-03-29 21:06:33Z herbelin $ *) +(* $Id: impargs.ml 8845 2006-05-23 07:41:58Z herbelin $ *) open Util open Names @@ -282,14 +282,15 @@ 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, mip.mind_user_arity)) + (fun mip -> (Name mip.mind_typename, None, type_of_inductive (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 - ((IndRef ind,auto_implicits env (body_of_type mip.mind_user_arity)), + let ar = type_of_inductive (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_user_lc) + mip.mind_nf_lc) in Array.mapi imps_one_inductive mib.mind_packets diff --git a/library/lib.ml b/library/lib.ml index ee553cad..ba6b9c79 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: lib.ml 7710 2005-12-23 10:16:42Z herbelin $ *) +(* $Id: lib.ml 8852 2006-05-23 17:52:43Z notin $ *) open Pp open Util @@ -460,7 +460,7 @@ let open_section id = let discharge_item = function | ((sp,_ as oname),Leaf lobj) -> - option_app (fun o -> (basename sp,o)) (discharge_object (oname,lobj)) + option_map (fun o -> (basename sp,o)) (discharge_object (oname,lobj)) | _ -> None @@ -624,12 +624,30 @@ let reset_initial () = (* Misc *) +let mp_of_global ref = + match ref with + | VarRef id -> fst (current_prefix ()) + | ConstRef cst -> con_modpath cst + | IndRef ind -> ind_modpath ind + | ConstructRef constr -> constr_modpath constr + +let rec dp_of_mp modp = + match modp with + | MPfile dp -> dp + | MPbound _ | MPself _ -> library_dp () + | MPdot (mp,_) -> dp_of_mp mp + let library_part ref = + match ref with + | VarRef id -> library_dp () + | _ -> dp_of_mp (mp_of_global ref) + +let remove_section_part ref = let sp = Nametab.sp_of_global ref in let dir,_ = repr_path sp in match ref with | VarRef id -> - anomaly "library_part not supported on local variables" + anomaly "remove_section_part not supported on local variables" | _ -> if is_dirpath_prefix_of dir (cwd ()) then (* Not yet (fully) discharged *) diff --git a/library/lib.mli b/library/lib.mli index 22b6b6d8..e33c3aca 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 6758 2005-02-20 18:13:28Z herbelin $ i*) +(*i $Id: lib.mli 8852 2006-05-23 17:52:43Z notin $ i*) (*i*) open Util @@ -122,7 +122,8 @@ val end_compilation : dir_path -> object_prefix * library_segment val library_dp : unit -> dir_path (* Extract the library part of a name even if in a section *) -val library_part : global_reference -> dir_path +val library_part : global_reference -> dir_path +val remove_section_part : global_reference -> dir_path (*s Sections *) diff --git a/library/libnames.ml b/library/libnames.ml index 536a382d..48a7565e 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 7052 2005-05-20 15:54:50Z herbelin $ i*) +(*i $Id: libnames.ml 8768 2006-04-28 14:25:31Z notin $ i*) open Pp open Util @@ -78,6 +78,14 @@ let dirpath_prefix p = match repr_dirpath p with let is_dirpath_prefix_of d1 d2 = list_prefix_of (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) +let chop_dirpath n d = + let d1,d2 = list_chop n (List.rev (repr_dirpath d)) in + make_dirpath (List.rev d1), make_dirpath (List.rev d2) + +let drop_dirpath_prefix d1 d2 = + let d = Util.list_drop_prefix (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) in + make_dirpath (List.rev d) + (* To know how qualified a name should be to be understood in the current env*) let add_dirpath_prefix id d = make_dirpath (repr_dirpath d @ [id]) diff --git a/library/libnames.mli b/library/libnames.mli index 06595e81..ab2185a6 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 7052 2005-05-20 15:54:50Z herbelin $ i*) +(*i $Id: libnames.mli 8768 2006-04-28 14:25:31Z notin $ i*) (*i*) open Pp @@ -53,6 +53,8 @@ val split_dirpath : dir_path -> dir_path * identifier val extend_dirpath : dir_path -> module_ident -> dir_path val add_dirpath_prefix : module_ident -> dir_path -> dir_path +val chop_dirpath : int -> dir_path -> dir_path * dir_path +val drop_dirpath_prefix : dir_path -> dir_path -> dir_path val extract_dirpath_prefix : int -> dir_path -> dir_path val is_dirpath_prefix_of : dir_path -> dir_path -> bool diff --git a/library/libobject.ml b/library/libobject.ml index 708c19b1..7f383a3b 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: libobject.ml 6748 2005-02-18 22:17:50Z herbelin $ *) +(* $Id: libobject.ml 8752 2006-04-27 19:37:33Z herbelin $ *) open Util open Names @@ -109,12 +109,12 @@ let declare_object odecl = anomaly "somehow we got the wrong dynamic object in the classifyfun" and discharge (oname,lobj) = if Dyn.tag lobj = na then - option_app infun (odecl.discharge_function (oname,outfun lobj)) + option_map infun (odecl.discharge_function (oname,outfun lobj)) else anomaly "somehow we got the wrong dynamic object in the dischargefun" and exporter lobj = if Dyn.tag lobj = na then - option_app infun (odecl.export_function (outfun lobj)) + option_map infun (odecl.export_function (outfun lobj)) else anomaly "somehow we got the wrong dynamic object in the exportfun" diff --git a/library/library.ml b/library/library.ml index 760b6f07..cfd88ca0 100644 --- a/library/library.ml +++ b/library/library.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: library.ml 7732 2005-12-26 13:51:24Z herbelin $ *) +(* $Id: library.ml 8877 2006-05-30 16:37:04Z notin $ *) open Pp open Util @@ -57,7 +57,6 @@ let canonical_path_name p = (* We give up to find a canonical name and just simplify it... *) strip_path p - let find_logical_path phys_dir = let phys_dir = canonical_path_name phys_dir in match list_filter2 (fun p d -> p = phys_dir) !load_paths with @@ -65,38 +64,44 @@ let find_logical_path phys_dir = | _,[] -> Nameops.default_root_prefix | _,l -> anomaly ("Two logical paths are associated to "^phys_dir) +let is_in_load_paths phys_dir = + let dir = canonical_path_name phys_dir in + let lp = get_load_paths () in + let check_p = fun p -> (String.compare dir p) == 0 in + List.exists check_p lp + let remove_load_path dir = load_paths := list_filter2 (fun p d -> p <> dir) !load_paths let add_load_path (phys_path,coq_path) = let phys_path = canonical_path_name phys_path in - match list_filter2 (fun p d -> p = phys_path) !load_paths with - | _,[dir] -> - if coq_path <> dir - (* If this is not the default -I . to coqtop *) - && not - (phys_path = canonical_path_name Filename.current_dir_name - && coq_path = Nameops.default_root_prefix) - then - begin - (* Assume the user is concerned by library naming *) - if dir <> Nameops.default_root_prefix then - (Options.if_verbose warning (phys_path^" was previously bound to " - ^(string_of_dirpath dir) - ^("\nIt is remapped to "^(string_of_dirpath coq_path))); - flush_all ()); - remove_load_path phys_path; - load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths) - end - | _,[] -> - load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths) - | _ -> anomaly ("Two logical paths are associated to "^phys_path) + match list_filter2 (fun p d -> p = phys_path) !load_paths with + | _,[dir] -> + if coq_path <> dir + (* If this is not the default -I . to coqtop *) + && not + (phys_path = canonical_path_name Filename.current_dir_name + && coq_path = Nameops.default_root_prefix) + then + begin + (* Assume the user is concerned by library naming *) + if dir <> Nameops.default_root_prefix then + (Options.if_verbose warning (phys_path^" was previously bound to " + ^(string_of_dirpath dir) + ^("\nIt is remapped to "^(string_of_dirpath coq_path))); + flush_all ()); + remove_load_path phys_path; + load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths) + end + | _,[] -> + load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths) + | _ -> anomaly ("Two logical paths are associated to "^phys_path) let physical_paths (dp,lp) = dp let load_paths_of_dir_path dir = fst (list_filter2 (fun p d -> d = dir) !load_paths) - + let get_full_load_paths () = List.combine (fst !load_paths) (snd !load_paths) (************************************************************************) diff --git a/library/library.mli b/library/library.mli index f7620682..27ace544 100644 --- a/library/library.mli +++ b/library/library.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: library.mli 6748 2005-02-18 22:17:50Z herbelin $ i*) +(*i $Id: library.mli 8877 2006-05-30 16:37:04Z notin $ i*) (*i*) open Util @@ -64,6 +64,7 @@ val get_full_load_paths : unit -> (System.physical_path * dir_path) list val add_load_path : System.physical_path * dir_path -> unit val remove_load_path : System.physical_path -> unit val find_logical_path : System.physical_path -> dir_path +val is_in_load_paths : System.physical_path -> bool val load_paths_of_dir_path : dir_path -> System.physical_path list (*s Locate a library in the load paths *) diff --git a/library/nameops.ml b/library/nameops.ml index 6db5f75d..1c6a7d56 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: nameops.ml 6205 2004-10-12 10:13:15Z herbelin $ *) +(* $Id: nameops.ml 8727 2006-04-24 09:48:06Z herbelin $ *) open Pp open Util @@ -138,7 +138,7 @@ let next_ident_away_from id avoid = let out_name = function | Name id -> id - | Anonymous -> anomaly "out_name: expects a defined name" + | Anonymous -> failwith "out_name: expects a defined name" let name_fold f na a = match na with -- cgit v1.2.3