diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-05 16:47:03 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-09-05 16:47:03 +0000 |
commit | ac2ca408aef1759e4682d989a40ab332068edcdb (patch) | |
tree | c33bd5f94b5da11544706492d5746e8894c05f0a | |
parent | 98db1b73f6ab89763ef386a2055528db91e4e152 (diff) |
Lib.node: merge OpenedModtype and OpenedModule, same for Closed...
This allows more sharing of code (cf. start_module / end_module)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14452 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | library/lib.ml | 176 | ||||
-rw-r--r-- | library/lib.mli | 28 | ||||
-rw-r--r-- | library/library.ml | 6 | ||||
-rw-r--r-- | parsing/prettyp.ml | 4 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 6 |
5 files changed, 93 insertions, 127 deletions
diff --git a/library/lib.ml b/library/lib.ml index f0eea4355..904824dc1 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -12,13 +12,15 @@ open Libnames open Nameops open Libobject open Summary + +type is_type = bool (* Module Type or just Module *) +type export = bool option (* None for a Module Type *) + type node = | Leaf of obj | CompilingLibrary of object_prefix - | OpenedModule of bool option * object_prefix * Summary.frozen + | OpenedModule of is_type * export * object_prefix * Summary.frozen | ClosedModule of library_segment - | OpenedModtype of object_prefix * Summary.frozen - | ClosedModtype of library_segment | OpenedSection of object_prefix * Summary.frozen | ClosedSection of library_segment | FrozenState of Summary.frozen @@ -29,6 +31,9 @@ and library_segment = library_entry list type lib_objects = (Names.identifier * obj) list +let module_kind is_type = + if is_type then "module type" else "module" + let iter_objects f i prefix = List.iter (fun (id,obj) -> f i (make_oname prefix id, obj)) @@ -67,10 +72,9 @@ let classify_segment seg = (* LEM; TODO: Understand what this does and see if what I do is the correct thing for ClosedMod(ule|type) *) | (_,ClosedModule _) :: stk -> clean acc stk - | (_,ClosedModtype _) :: stk -> clean acc stk | (_,OpenedSection _) :: _ -> error "there are still opened sections" - | (_,OpenedModule _) :: _ -> error "there are still opened modules" - | (_,OpenedModtype _) :: _ -> error "there are still opened module types" + | (_,OpenedModule (ty,_,_,_)) :: _ -> + error ("there are still opened " ^ module_kind ty ^"s") | (_,FrozenState _) :: stk -> clean acc stk in clean ([],[],[]) (List.rev seg) @@ -142,8 +146,7 @@ let make_oname id = make_path id, make_kn id let recalc_path_prefix () = let rec recalc = function | (sp, OpenedSection (dir,_)) :: _ -> dir - | (sp, OpenedModule (_,dir,_)) :: _ -> dir - | (sp, OpenedModtype (dir,_)) :: _ -> dir + | (sp, OpenedModule (_,_,dir,_)) :: _ -> dir | (sp, CompilingLibrary dir) :: _ -> dir | _::l -> recalc l | [] -> initial_prefix @@ -179,7 +182,6 @@ let split_lib_gen test = then Some (collect after [hd] before) else (match hd with | (sp,ClosedModule seg) - | (sp,ClosedModtype seg) | (sp,ClosedSection seg) -> (match findeq after seg with | None -> findeq (hd::after) before @@ -195,11 +197,11 @@ let split_lib_gen test = let split_lib sp = split_lib_gen (fun x -> fst x = sp) let split_lib_at_opening sp = - let a,s,b = split_lib_gen (function - | x,(OpenedSection _|OpenedModule _|OpenedModtype _|CompilingLibrary _) -> - x = sp - | _ -> - false) in + let is_sp = function + | x,(OpenedSection _|OpenedModule _|CompilingLibrary _) -> x = sp + | _ -> false + in + let a,s,b = split_lib_gen is_sp in assert (List.tl s = []); (a,List.hd s,b) @@ -253,96 +255,65 @@ let add_frozen_state () = (* Modules. *) let is_opening_node = function - _,(OpenedSection _ | OpenedModule _ | OpenedModtype _) -> true + | _,(OpenedSection _ | OpenedModule _) -> true | _ -> false let is_opening_node_or_lib = function - _,(CompilingLibrary _ | OpenedSection _ - | OpenedModule _ | OpenedModtype _) -> true + | _,(CompilingLibrary _ | OpenedSection _ | OpenedModule _) -> true | _ -> false let current_mod_id () = try match find_entry_p is_opening_node_or_lib with - | oname,OpenedModule (_,_,fs) -> - basename (fst oname) - | oname,OpenedModtype (_,fs) -> - basename (fst oname) - | oname,CompilingLibrary _ -> - basename (fst oname) + | oname,OpenedModule (_,_,_,fs) -> basename (fst oname) + | oname,CompilingLibrary _ -> basename (fst oname) | _ -> error "you are not in a module" - with Not_found -> - error "no opened modules" + with Not_found -> error "no opened modules" -let start_module export id mp fs = +let start_mod is_type export id mp fs = let dir = add_dirpath_suffix (fst !path_prefix) id in let prefix = dir,(mp,Names.empty_dirpath) in - let oname = make_path id, make_kn id in - if Nametab.exists_module dir then - errorlabstrm "open_module" (pr_id id ++ str " already exists") ; - add_entry oname (OpenedModule (export,prefix,fs)); + let sp = make_path id in + let oname = sp, make_kn id in + let exists = + if is_type then Nametab.exists_cci sp else Nametab.exists_module dir + in + if exists then + errorlabstrm "open_module" (pr_id id ++ str " already exists"); + add_entry oname (OpenedModule (is_type,export,prefix,fs)); path_prefix := prefix; prefix (* add_frozen_state () must be called in declaremods *) +let start_module = start_mod false +let start_modtype = start_mod true None + let error_still_opened string oname = let id = basename (fst oname) in - errorlabstrm "" (str string ++ spc () ++ pr_id id ++ str " is still opened.") + errorlabstrm "" + (str ("The "^string^" ") ++ pr_id id ++ str " is still opened.") -let end_module () = +let end_mod is_type = let oname,fs = try match find_entry_p is_opening_node with - | oname,OpenedModule (_,_,fs) -> oname,fs - | oname,OpenedModtype _ -> error_still_opened "Module Type" oname - | oname,OpenedSection _ -> error_still_opened "Section" oname + | oname,OpenedModule (ty,_,_,fs) -> + if ty = is_type then oname,fs + else error_still_opened (module_kind ty) oname + | oname,OpenedSection _ -> error_still_opened "section" oname | _ -> assert false - with Not_found -> - error "No opened modules." + with Not_found -> error "No opened modules." in let (after,mark,before) = split_lib_at_opening oname in lib_stk := before; add_entry oname (ClosedModule (List.rev (mark::after))); let prefix = !path_prefix in - (* LEM: This module business seems more complicated than sections; - shouldn't a backtrack into a closed module also do something - with global.ml, given that closing a module does? - TODO - *) recalc_path_prefix (); (* add_frozen_state must be called after processing the module, because we cannot recache interactive modules *) (oname, prefix, fs, after) -let start_modtype id mp fs = - let dir = add_dirpath_suffix (fst !path_prefix) id in - let prefix = dir,(mp,Names.empty_dirpath) in - let sp = make_path id in - let name = sp, make_kn id in - if Nametab.exists_cci sp then - errorlabstrm "open_modtype" (pr_id id ++ str " already exists") ; - add_entry name (OpenedModtype (prefix,fs)); - path_prefix := prefix; - prefix - -let end_modtype () = - let oname,fs = - try match find_entry_p is_opening_node with - | oname,OpenedModtype (_,fs) -> oname,fs - | oname,OpenedModule _ -> error_still_opened "Module" oname - | oname,OpenedSection _ -> error_still_opened "Section" oname - | _ -> assert false - with Not_found -> - error "no opened module types" - in - let (after,mark,before) = split_lib_at_opening oname in - lib_stk := before; - add_entry oname (ClosedModtype (List.rev (mark::after))); - let dir = !path_prefix in - recalc_path_prefix (); - (* add_frozen_state must be called after processing the module type. - This is because we cannot recache interactive module types *) - (oname,dir,fs,after) - +let end_module () = end_mod false +let end_modtype () = end_mod true let contents_after = function | None -> !lib_stk @@ -365,21 +336,18 @@ let end_compilation dir = let _ = try match snd (find_entry_p is_opening_node) with | OpenedSection _ -> error "There are some open sections." - | OpenedModule _ -> error "There are some open modules." - | OpenedModtype _ -> error "There are some open module types." + | OpenedModule (ty,_,_,_) -> + error ("There are some open "^module_kind ty^"s.") | _ -> assert false - with - Not_found -> () + with Not_found -> () in - let module_p = - function (_,CompilingLibrary _) -> true | x -> is_opening_node x + let is_opening_lib = function _,CompilingLibrary _ -> true | _ -> false in let oname = - try match find_entry_p module_p with - (oname, CompilingLibrary prefix) -> oname + try match find_entry_p is_opening_lib with + | (oname, CompilingLibrary prefix) -> oname | _ -> assert false - with - Not_found -> anomaly "No module declared" + with Not_found -> anomaly "No module declared" in let _ = match !comp_name with @@ -390,31 +358,23 @@ let end_compilation dir = " and not " ^ (Names.string_of_dirpath m)); in let (after,mark,before) = split_lib_at_opening 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 () = - let opened_p = function - | _, OpenedModtype _ -> true - | _ -> false - in - try - let _ = find_entry_p opened_p in true - with - Not_found -> false - -(* Returns true if we are inside an opened module *) -let is_module () = - let opened_p = function - | _, OpenedModule _ -> true +(* Returns true if we are inside an opened module or module type *) + +let is_module_gen which = + let test = function + | _, OpenedModule (ty,_,_,_) -> which ty | _ -> false in - try - let _ = find_entry_p opened_p in true - with - Not_found -> false + try + let _ = find_entry_p test in true + with Not_found -> false +let is_module_or_modtype () = is_module_gen (fun _ -> true) +let is_modtype () = is_module_gen (fun b -> b) +let is_module () = is_module_gen (fun b -> not b) (* Returns the opening node of a given name *) let find_opening_node id = @@ -552,8 +512,8 @@ let discharge_item ((sp,_ as oname),e) = | Leaf lobj -> Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj)) | FrozenState _ -> None - | ClosedSection _ | ClosedModtype _ | ClosedModule _ -> None - | OpenedSection _ | OpenedModtype _ | OpenedModule _ | CompilingLibrary _ -> + | ClosedSection _ | ClosedModule _ -> None + | OpenedSection _ | OpenedModule _ | CompilingLibrary _ -> anomaly "discharge_item" let close_section () = @@ -629,7 +589,7 @@ let reset_to_state sp = (* LEM: TODO * We will need to muck with frozen states in after, too! - * Not only FrozenState, but also those embedded in Opened(Section|Module|Modtype) + * Not only FrozenState, but also those embedded in Opened(Section|Module) *) let delete_gen test = let (after,equal,before) = split_lib_gen test in @@ -665,8 +625,8 @@ let remove_name (loc,id) = delete sp let is_mod_node = function - | OpenedModule _ | OpenedModtype _ | OpenedSection _ - | ClosedModule _ | ClosedModtype _ | ClosedSection _ -> true + | OpenedModule _ | OpenedSection _ + | ClosedModule _ | ClosedSection _ -> true | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE" || t = "MODULE ALIAS" | _ -> false diff --git a/library/lib.mli b/library/lib.mli index 349cfaa54..8defad867 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -13,13 +13,14 @@ and to backtrack (undo) those operations. It provides also the section mechanism (at a low level; discharge is not known at this step). *) +type is_type = bool (* Module Type or just Module *) +type export = bool option (* None for a Module Type *) + type node = | Leaf of Libobject.obj | CompilingLibrary of Libnames.object_prefix - | OpenedModule of bool option * Libnames.object_prefix * Summary.frozen + | OpenedModule of is_type * export * Libnames.object_prefix * Summary.frozen | ClosedModule of library_segment - | OpenedModtype of Libnames.object_prefix * Summary.frozen - | ClosedModtype of library_segment | OpenedSection of Libnames.object_prefix * Summary.frozen | ClosedSection of library_segment | FrozenState of Summary.frozen @@ -99,6 +100,7 @@ val sections_are_opened : unit -> bool val sections_depth : unit -> int (** Are we inside an opened module type *) +val is_module_or_modtype : unit -> bool val is_modtype : unit -> bool val is_module : unit -> bool val current_mod_id : unit -> Names.module_ident @@ -109,14 +111,22 @@ val find_opening_node : Names.identifier -> node (** {6 Modules and module types } *) val start_module : - bool option -> Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix -val end_module : unit - -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment + export -> Names.module_ident -> Names.module_path -> + Summary.frozen -> Libnames.object_prefix val start_modtype : - Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix -val end_modtype : unit - -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment + Names.module_ident -> Names.module_path -> + Summary.frozen -> Libnames.object_prefix + +val end_module : + unit -> + Libnames.object_name * Libnames.object_prefix * + Summary.frozen * library_segment + +val end_modtype : + unit -> + Libnames.object_name * Libnames.object_prefix * + Summary.frozen * library_segment (** [Lib.add_frozen_state] must be called after each of the above functions *) diff --git a/library/library.ml b/library/library.ml index 447d53610..9c602adbb 100644 --- a/library/library.ml +++ b/library/library.ml @@ -543,7 +543,7 @@ let set_xml_require f = xml_require := f let require_library_from_dirpath modrefl export = let needed = List.rev (List.fold_left rec_intern_library [] modrefl) in let modrefl = List.map fst modrefl in - if Lib.is_modtype () || Lib.is_module () then + if Lib.is_module_or_modtype () then begin add_anonymous_leaf (in_require (needed,modrefl,None)); Option.iter (fun exp -> @@ -562,7 +562,7 @@ let require_library qidl export = let require_library_from_file idopt file export = let modref,needed = rec_intern_library_from_file idopt file in let needed = List.rev needed in - if Lib.is_modtype () || Lib.is_module () then begin + if Lib.is_module_or_modtype () then begin add_anonymous_leaf (in_require (needed,[modref],None)); Option.iter (fun exp -> add_anonymous_leaf (in_import (modref,exp))) export @@ -578,7 +578,7 @@ let import_module export (loc,qid) = try match Nametab.locate_module qid with | MPfile dir -> - if Lib.is_modtype () || Lib.is_module () || not export then + if Lib.is_module_or_modtype () || not export then add_anonymous_leaf (in_import (dir, export)) else add_anonymous_leaf (in_import (dir, export)) diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 38c8a7438..f530870e9 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -430,10 +430,6 @@ let gallina_print_library_entry with_values ent = Some (str " >>>>>>> Module " ++ pr_name oname) | (oname,Lib.ClosedModule _) -> Some (str " >>>>>>> Closed Module " ++ pr_name oname) - | (oname,Lib.OpenedModtype _) -> - Some (str " >>>>>>> Module Type " ++ pr_name oname) - | (oname,Lib.ClosedModtype _) -> - Some (str " >>>>>>> Closed Module Type " ++ pr_name oname) | (_,Lib.FrozenState _) -> None diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 465302a23..1b25fb926 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -594,10 +594,10 @@ let vernac_end_section (loc,_) = let vernac_end_segment (_,id as lid) = check_no_pending_proofs (); match Lib.find_opening_node id with - | Lib.OpenedModule (export,_,_) -> vernac_end_module export lid - | Lib.OpenedModtype _ -> vernac_end_modtype lid + | Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid + | Lib.OpenedModule (true,_,_,_) -> vernac_end_modtype lid | Lib.OpenedSection _ -> vernac_end_section lid - | _ -> anomaly "No more opened things" + | _ -> assert false (* Libraries *) |