From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001
From: Samuel Mimram <samuel.mimram@ens-lyon.org>
Date: Wed, 28 Jul 2004 21:54:47 +0000
Subject: Imported Upstream version 8.0pl1

---
 library/lib.mli | 156 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 156 insertions(+)
 create mode 100644 library/lib.mli

(limited to 'library/lib.mli')

diff --git a/library/lib.mli b/library/lib.mli
new file mode 100644
index 00000000..8981754e
--- /dev/null
+++ b/library/lib.mli
@@ -0,0 +1,156 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: lib.mli,v 1.41.2.1 2004/07/16 19:30:35 herbelin Exp $ i*)
+
+(*i*)
+open Util
+open Names
+open Libnames
+open Libobject
+open Summary
+(*i*)
+
+(*s This module provides a general mechanism to keep a trace of all operations
+   and to backtrack (undo) those operations. It provides also the section
+   mechanism (at a low level; discharge is not known at this step). *)
+
+type node = 
+  | Leaf of obj
+  | 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_segment = (object_name * node) list
+
+type lib_objects = (identifier * obj) list
+
+(*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
+
+(* [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). *)
+
+val add_leaf : identifier -> obj -> object_name
+val add_absolutely_named_leaf : object_name -> obj -> unit
+val add_anonymous_leaf : obj -> unit
+
+(* this operation adds all objects with the same name and calls load_object 
+   for each of them *)
+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
+
+(*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
+
+(* Are we inside an opened section *)
+val sections_are_opened : unit -> bool
+val sections_depth : unit -> int
+
+(* Are we inside an opened module type *)
+val is_modtype : unit -> bool
+val is_module : unit -> bool
+
+
+(* Returns the most recent OpenedThing node *)
+val what_is_opened : unit -> object_name * node
+
+
+(*s Modules and module types *)
+
+val start_module : 
+  module_ident -> module_path -> Summary.frozen -> object_prefix
+val end_module : module_ident 
+  -> object_name * object_prefix * Summary.frozen * library_segment
+
+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 *)
+
+(*s Compilation units *)
+
+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
+
+(* Extract the library part of a name even if in a section *)
+val library_part : global_reference -> 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). *)
+
+val reset_to : object_name -> unit
+val reset_name : identifier located -> unit
+val reset_mod : identifier located -> unit
+
+(* [back n] resets to the place corresponding to the $n$-th call of 
+   [mark_end_of_command] (counting backwards) *)
+val back : int -> unit
+
+(*s We can get and set the state of the operations (used in [States]). *)
+
+type frozen
+
+val freeze : unit -> frozen
+val unfreeze : frozen -> unit
+
+val init : unit -> unit
+
+val declare_initial_state : unit -> unit
+val reset_initial : unit -> unit
+
+
+(* XML output hooks *)
+val set_xml_open_section : (identifier -> unit) -> unit
+val set_xml_close_section : (identifier -> unit) -> unit
-- 
cgit v1.2.3