From 2e43b03b0bb88bd3b4cb7695d5079c51ca41b0a7 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Thu, 22 Nov 2012 18:09:38 +0000 Subject: Monomorphization (library) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15993 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/declaremods.ml | 65 ++++++++++++++++++++++++++++---------------------- 1 file changed, 37 insertions(+), 28 deletions(-) (limited to 'library/declaremods.ml') diff --git a/library/declaremods.ml b/library/declaremods.ml index fef95bc61..4adf9d02d 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -155,7 +155,7 @@ let _ = Summary.declare_summary "MODULE-INFO" let mp_of_kn kn = let mp,sec,l = repr_kn kn in - if sec=empty_dirpath then + if dir_path_eq sec empty_dirpath then MPdot (mp,l) else anomaly ("Non-empty section in module name!" ^ string_of_kn kn) @@ -230,7 +230,9 @@ let build_subtypes interp_modtype mp args mtys = let compute_visibility exists what i dir dirinfo = if exists then if - try Nametab.locate_dir (qualid_of_dirpath dir) = dirinfo + try + let globref = Nametab.locate_dir (qualid_of_dirpath dir) in + eq_global_dir_reference globref dirinfo with Not_found -> false then Nametab.Exactly i @@ -316,7 +318,7 @@ let load_keep i ((sp,kn),seg) = begin try let prefix',objects = MPmap.find mp !modtab_objects in - if prefix' <> prefix then + if not (eq_op prefix' prefix) then anomaly "Two different modules with the same path!"; modtab_objects := MPmap.add mp (prefix,objects@seg) !modtab_objects; with @@ -366,7 +368,7 @@ let cache_modtype ((sp,kn),(entry,modtypeobjs,sub_mty_l)) = | None -> anomaly "You must not recache interactive module types!" | Some (mte,inl) -> - if mp <> Global.add_modtype (basename sp) mte inl then + if not (mp_eq mp (Global.add_modtype (basename sp) mte inl)) then anomaly "Kernel and Library names do not match" in @@ -384,7 +386,7 @@ let cache_modtype ((sp,kn),(entry,modtypeobjs,sub_mty_l)) = let load_modtype i ((sp,kn),(entry,modtypeobjs,_)) = - assert (entry = None); + assert (Option.is_empty entry); if Nametab.exists_modtype sp then errorlabstrm "cache_modtype" @@ -396,10 +398,12 @@ let load_modtype i ((sp,kn),(entry,modtypeobjs,_)) = let open_modtype i ((sp,kn),(entry,_,_)) = - assert (entry = None); + assert (Option.is_empty entry); if - try Nametab.locate_modtype (qualid_of_path sp) <> (mp_of_kn kn) + try + let mp = Nametab.locate_modtype (qualid_of_path sp) in + not (mp_eq mp (mp_of_kn kn)) with Not_found -> true then errorlabstrm ("open_modtype") @@ -408,7 +412,7 @@ let open_modtype i ((sp,kn),(entry,_,_)) = Nametab.push_modtype (Nametab.Exactly i) sp (mp_of_kn kn) let subst_modtype (subst,(entry,(mbids,mp,objs),_)) = - assert (entry = None); + assert (Option.is_empty entry); (entry,(mbids,subst_mp subst mp,subst_objects subst objs),[]) let classify_modtype (_,substobjs,_) = @@ -428,17 +432,18 @@ let in_modtype : modtype_obj -> obj = classify_function = classify_modtype } let rec replace_module_object idl (mbids,mp,lib_stack) (mbids2,mp2,objs) mp1 = - if mbids<>[] then anomaly "Unexpected functor objects"; + let () = match mbids with + | [] -> () | _ -> anomaly "Unexpected functor objects" in let rec replace_idl = function | _,[] -> [] - | id::idl,(id',obj)::tail when id = id' -> - if object_tag obj <> "MODULE" then anomaly "MODULE expected!"; - let substobjs = - if idl = [] then - let mp' = MPdot(mp, label_of_id id) in - mbids, mp', subst_objects (map_mp mp1 mp' empty_delta_resolver) objs - else - replace_module_object idl (out_module obj) (mbids2,mp2,objs) mp + | id::idl,(id',obj)::tail when id_eq id id' -> + if not (String.equal (object_tag obj) "MODULE") then anomaly "MODULE expected!"; + let substobjs = match idl with + | [] -> + let mp' = MPdot(mp, label_of_id id) in + mbids, mp', subst_objects (map_mp mp1 mp' empty_delta_resolver) objs + | _ -> + replace_module_object idl (out_module obj) (mbids2,mp2,objs) mp in (id, in_module substobjs)::tail | idl,lobj::tail -> lobj::replace_idl (idl,tail) @@ -611,16 +616,17 @@ let end_module () = in let node = in_module substobjs in let objects = - if keep = [] || mbids <> [] then + match keep, mbids with + | [], _ | _, _ :: _ -> special@[node] (* no keep objects or we are defining a functor *) - else + | _ -> special@[node;in_modkeep keep] (* otherwise *) in let newoname = Lib.add_leaves id objects in - if (fst newoname) <> (fst oldoname) then + if not (eq_full_path (fst newoname) (fst oldoname)) then anomaly "Names generated on start_ and end_module do not match"; - if mp_of_kn (snd newoname) <> mp then + if not (mp_eq (mp_of_kn (snd newoname)) mp) then anomaly "Kernel and Library names do not match"; Lib.add_frozen_state () (* to prevent recaching *); @@ -652,7 +658,7 @@ let register_library dir cenv objs digest = (* if it's in the environment, the cached objects should be correct *) Dirmap.find dir !library_cache with Not_found -> - if mp <> Global.import cenv digest then + if not (mp_eq mp (Global.import cenv digest)) then anomaly "Unexpected disk module name"; let mp,substitute,keep = objs in let substobjs = [], mp, substitute in @@ -703,7 +709,7 @@ let subst_import (subst,(export,mp as obj)) = let in_import = declare_object {(default_object "IMPORT MODULE") with cache_function = cache_import; - open_function = (fun i o -> if i=1 then cache_import o); + open_function = (fun i o -> if Int.equal i 1 then cache_import o); subst_function = subst_import; classify_function = classify_import } @@ -735,10 +741,10 @@ let end_modtype () = check_subtypes_mt mp sub_mty_l; let oname = Lib.add_leaves id (special@[in_modtype (None, modtypeobjs,[])]) in - if fst oname <> fst oldoname then + if not (eq_full_path (fst oname) (fst oldoname)) then anomaly "Section paths generated on start_ and end_modtype do not match"; - if (mp_of_kn (snd oname)) <> mp then + if not (mp_eq (mp_of_kn (snd oname)) mp) then anomaly "Kernel and Library names do not match"; @@ -833,10 +839,13 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs = (* and declare the module as a whole *) Summary.unfreeze_summaries fs; let mp = mp_of_kn (Lib.make_kn id) in - let inl = if inl_expr = None then None else inl_res in (*PLTODO *) + let inl = match inl_expr with + | None -> None + | _ -> inl_res + in (* PLTODO *) let mp_env,resolver = Global.add_module id entry inl in - if mp_env <> mp then anomaly "Kernel and Library names do not match"; + if not (mp_eq mp_env mp) then anomaly "Kernel and Library names do not match"; check_subtypes mp subs; @@ -965,7 +974,7 @@ let declare_one_include_inner annot (me,is_mod) = else get_modtype_substobjs env mp1 inl me in let (mbids,mp,objs) = - if mbids <> [] then + if not (List.is_empty mbids) then get_includeself_substobjs env (mbids,mp,objs) me is_mod inl else (mbids,mp,objs) in -- cgit v1.2.3