From bb6f20a2ee88f264fa2c73c5a3ed306008791f7d Mon Sep 17 00:00:00 2001 From: coq Date: Thu, 19 Dec 2002 16:57:45 +0000 Subject: Petit netoyage dans lib git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3463 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/lib.mli | 98 ++++++++++++++++++++++++--------------------------------- 1 file changed, 41 insertions(+), 57 deletions(-) (limited to 'library/lib.mli') diff --git a/library/lib.mli b/library/lib.mli index 022ddb5cd..7f22250f1 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -22,57 +22,36 @@ open Summary type node = | Leaf of obj - | CompilingModule of object_prefix + | CompilingLibrary of object_prefix | OpenedModule of object_prefix * Summary.frozen | OpenedModtype of object_prefix * Summary.frozen | OpenedSection of object_prefix * Summary.frozen | ClosedSection of bool * dir_path * library_segment | FrozenState of Summary.frozen -and library_entry = object_name * node - -and library_segment = library_entry list +and library_segment = (object_name * node) list type lib_objects = (identifier * obj) list -(*s These functions iterate (or map) object functions. - - [subst_segment prefix subst seg] makes an assumption that all - objects in [seg] have the same prefix. This prefix is universally - changed to [prefix]. - - [classify_segment seg] divides segment into objects which responded - with [Substitute], [Keep], [Anticipate] respectively, to the - [classify_object] function. The order of each returned list is the - same as in the input list. - - [change_kns mp lib] only changes the prefix of the [kernel_name] - part of the [object_name] of every object to [(mp,empty_dirpath)]. - The [section_path] part of the [object_name] and the object itself - are unchanged. -*) - - -val open_segment : int -> library_segment -> unit -val load_segment : int -> library_segment -> unit -val subst_segment : - object_prefix -> substitution -> library_segment -> library_segment -val classify_segment : - library_segment -> library_segment * library_segment * library_segment -val change_kns : module_path -> library_segment -> library_segment - - +(*s Object iteratation functions. *) val open_objects : int -> object_prefix -> lib_objects -> unit val load_objects : int -> object_prefix -> lib_objects -> unit -val subst_objects : - object_prefix -> substitution -> lib_objects -> lib_objects -val classify_objects : +val subst_objects : object_prefix -> substitution -> lib_objects -> lib_objects + +(* [classify_segment seg] verifies that there are no OpenedThings, + clears ClosedSections and FrozenStates and divides Leafs according + to their answers to the [classify_object] function in three groups: + [Substitute], [Keep], [Anticipate] respectively. The order of each + returned list is the same as in the input list. *) +val classify_segment : library_segment -> lib_objects * lib_objects * obj list +(* [segment_of_objects prefix objs] forms a list of Leafs *) val segment_of_objects : object_prefix -> lib_objects -> library_segment + (*s Adding operations (which call the [cache] method, and getting the current list of operations (most recent ones coming first). *) @@ -87,41 +66,33 @@ val add_leaves : identifier -> obj list -> object_name val add_frozen_state : unit -> unit val mark_end_of_command : unit -> unit + (*s The function [contents_after] returns the current library segment, starting from a given section path. If not given, the entire segment is returned. *) val contents_after : object_name option -> library_segment -(* Returns true if we are inside an opened module type *) -val is_specification : unit -> bool - -(* Returns the most recent OpenedThing node *) -val what_is_opened : unit -> library_entry - -(*s Opening and closing a section. *) - -val open_section : identifier -> object_prefix - -val close_section : export:bool -> identifier -> - object_prefix * library_segment * Summary.frozen - -val sections_are_opened : unit -> bool +(*s Functions relative to current path *) +(* User-side names *) +val cwd : unit -> dir_path val make_path : identifier -> section_path + +(* Kernel-side names *) +val current_prefix : unit -> module_path * dir_path val make_kn : identifier -> kernel_name -val cwd : unit -> dir_path +(* Are we inside an opened section *) +val sections_are_opened : unit -> bool val sections_depth : unit -> int -val is_section_p : dir_path -> bool -(*s Compilation units *) +(* Are we inside an opened module type *) +val is_specification : unit -> bool -val start_compilation : dir_path -> module_path -> unit -val end_compilation : dir_path -> object_prefix * library_segment +(* Returns the most recent OpenedThing node *) +val what_is_opened : unit -> object_name * node -(* The function [module_dp] returns the [dir_path] of the current module *) -val module_dp : unit -> dir_path (*s Modules and module types *) @@ -134,10 +105,23 @@ val start_modtype : module_ident -> module_path -> Summary.frozen -> object_prefix val end_modtype : module_ident -> object_name * object_prefix * Summary.frozen * library_segment +(* Lib.add_frozen_state must be called after each of the above functions *) -(* Lib.add_frozen_state must be called after all of the above functions *) +(*s Compilation units *) -val current_prefix : unit -> module_path * dir_path +val start_compilation : dir_path -> module_path -> unit +val end_compilation : dir_path -> object_prefix * library_segment + +(* The function [library_dp] returns the [dir_path] of the current + compiling library (or [default_library]) *) +val library_dp : unit -> dir_path + +(*s Sections *) + +val open_section : identifier -> object_prefix + +val close_section : export:bool -> identifier -> + object_prefix * library_segment * Summary.frozen (*s Backtracking (undo). *) -- cgit v1.2.3