- un effort sur la doc (ocamlweb)

 - module Nametab
 - module Impargs
 - correction bug : Parameter id : t => vérification que t est bien un type


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@76 85f007b7-540e-0410-9357-904b9bb8a0f7

10 files changed, 200 insertions, 16 deletions

diff --git a/library/doc.tex b/library/doc.tex
index fd1a8bbf9..33af59336 100644
--- a/library/doc.tex
+++ b/library/doc.tex
@@ -1,11 +1,16 @@
 
+\newpage
 \section*{The Coq library}
 
 \ocwsection \label{library}
-This section describes the \Coq\ library, which is made of two parts:
+This chapter describes the \Coq\ library, which is made of two parts:
 \begin{itemize}
   \item a general mechanism to keep a trace of all operations and of
-    the state of the system, with backtrack possibilities;
+    the state of the system, with backtrack capabilities;
   \item a global environment for the CCI, with functions to export and 
     import compiled modules.
 \end{itemize}
+The modules of the library are organized as follows.
+
+\bigskip
+\begin{center}\epsfig{file=library.dep.ps}\end{center}
diff --git a/library/global.ml b/library/global.ml
index d7267a96d..7ffbd2110 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -9,6 +9,8 @@ open Summary
 
 let global_env = ref empty_environment
 
+let env () = !global_env
+
 let _ = 
   declare_summary "Global environment"
     { freeze_function = (fun () -> !global_env);
diff --git a/library/global.mli b/library/global.mli
index d21509e32..9436e446b 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -10,12 +10,15 @@ open Evd
 open Constant
 open Inductive
 open Environ
+open Typing
 (*i*)
 
 (* This module defines the global environment of Coq. 
    The functions below are the exactly the same as the ones in [Typing],
    operating on that global environment. *)
 
+val env : unit -> unit environment
+
 val evar_map : unit -> unit evar_map
 val universes : unit -> universes
 val metamap : unit -> (int * constr) list
diff --git a/library/impargs.ml b/library/impargs.ml
new file mode 100644
index 000000000..95b322e4e
--- /dev/null
+++ b/library/impargs.ml
@@ -0,0 +1,87 @@
+
+(* $Id$ *)
+
+open Names
+open Generic
+open Term
+open Reduction
+open Constant
+open Inductive
+open Typing
+
+type implicits =
+  | Impl_auto of int list
+  | Impl_manual of int list
+  | No_impl
+
+let implicit_args = ref false
+
+let auto_implicits ty =
+  if !implicit_args then
+    let genv = unsafe_env_of_env (Global.env()) in
+    Impl_auto (poly_args genv ty)
+  else
+    No_impl
+
+(* Constants. *)
+
+let constants_table = ref Spmap.empty
+
+let declare_constant_implicits sp =
+  let cb = Global.lookup_constant sp in
+  let imps = auto_implicits cb.const_type.body in
+  constants_table := Spmap.add sp imps !constants_table
+
+let declare_constant_manual_implicits sp imps =
+  constants_table := Spmap.add sp (Impl_manual imps) !constants_table
+
+let constant_implicits sp =
+  Spmap.find sp !constants_table
+
+(* Inductives and constructors. Their implicit arguments are stored
+   in an array, indexed by the inductive number, of pairs $(i,v)$ where
+   $i$ are the implicit arguments of the inductive and $v$ the array of 
+   implicit arguments of the constructors. *)
+
+let inductives_table = ref Spmap.empty
+
+let declare_inductive_implicits sp =
+  let mib = Global.lookup_mind sp in
+  let imps_one_inductive mip =
+    (auto_implicits mip.mind_arity.body,
+     let (_,lc) = decomp_all_DLAMV_name mip.mind_lc in
+     Array.map auto_implicits lc)
+  in
+  let imps = Array.map imps_one_inductive mib.mind_packets in
+  inductives_table := Spmap.add sp imps !inductives_table
+    
+let inductive_implicits (sp,i) =
+  let imps = Spmap.find sp !inductives_table in
+  fst imps.(i)
+
+let constructor_implicits ((sp,i),j) =
+  let imps = Spmap.find sp !inductives_table in
+  (snd imps.(i)).(pred j)
+
+(* Registration as global tables and roolback. *)
+
+type frozen = implicits Spmap.t
+
+let init () =
+  constants_table := Spmap.empty
+
+let freeze () =
+  !constants_table
+
+let unfreeze ct =
+  constants_table := ct
+
+let _ = 
+  Summary.declare_summary "names"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init }
+
+let rollback f x =
+  let fs = freeze () in
+  try f x with e -> begin unfreeze fs; raise e end
diff --git a/library/impargs.mli b/library/impargs.mli
new file mode 100644
index 000000000..84ea98da3
--- /dev/null
+++ b/library/impargs.mli
@@ -0,0 +1,26 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+(*i*)
+
+(* Implicit arguments. Here we store the implicit arguments. Notice that we 
+   are outside the kernel, which knows nothing about implicit arguments. *)
+
+type implicits =
+  | Impl_auto of int list
+  | Impl_manual of int list
+  | No_impl
+
+val implicit_args : bool ref
+
+val declare_constant_implicits : section_path -> unit
+val declare_constant_manual_implicits : section_path -> int list -> unit
+val constant_implicits : section_path -> implicits
+
+val declare_inductive_implicits : section_path -> unit
+val inductive_implicits : section_path * int -> implicits
+val constructor_implicits : (section_path * int) * int -> implicits
+
+
diff --git a/library/lib.ml b/library/lib.ml
index 42850bc05..9c434fdf1 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -126,7 +126,7 @@ let close_section s =
   in
   let (after,_,before) = split_lib sp in
   lib_stk := before;
-  add_entry sp (ClosedSection (s,modp,List.rev after));
+  add_entry sp (ClosedSection (s,modp,after));
   add_frozen_state ();
   pop_path_prefix ()
 
diff --git a/library/libobject.mli b/library/libobject.mli
index 7ddac57b2..ff076ee39 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -6,14 +6,14 @@ open Names
 (*i*)
 
 (* [Libobject] declares persistent objects, given with three methods:
-   - a caching function specifying how to add the object in the current
-     scope of theory modules;
-   - a loading function, specifying what to do when the object is loaded
-     from the disk;
-   - an opening function, specifying what to do when the module containing
-     the object is opened;
-   - a specification function, to extract its specification when writing
-     the specification of a module to the disk (.vi) *)
+   a caching function specifying how to add the object in the current
+   scope of theory modules;
+   a loading function, specifying what to do when the object is loaded
+   from the disk;
+   an opening function, specifying what to do when the module containing
+   the object is opened;
+   a specification function, to extract its specification when writing
+   the specification of a module to the disk (.vi) *)
 
 type 'a object_declaration = {
   cache_function : section_path * 'a -> unit;
@@ -21,8 +21,7 @@ type 'a object_declaration = {
   open_function : 'a -> unit;
   specification_function : 'a -> 'a }
 
-(*s Given the object-name, the "loading" function, the "caching" function, 
-   and the "specification" function, the function [declare_object]
+(*s Given an object name and a declaration, the function [declare_object]
    will hand back two functions, the "injection" and "projection"
    functions for dynamically typed library-objects. *)
 
diff --git a/library/library.ml b/library/library.ml
index 7de5a845d..0bd0b895c 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -76,9 +76,8 @@ let open_module s =
    exported in the dependencies (usually it is [true] at the highest level;
    it is always [false] in recursive loadings). *)
 
-let load_objects s =
-  let m = find_module s in
-  segment_iter load_object m.module_declarations
+let load_objects decls =
+  segment_iter load_object decls
 
 let rec load_module_from doexp s f =
   let (fname,ch) = raw_intern_module f in
@@ -95,6 +94,8 @@ let rec load_module_from doexp s f =
   if s <> md.md_name then
     error ("The file " ^ fname ^ " does not contain module " ^ s);
   List.iter (load_mandatory_module doexp s) m.module_deps;
+  Global.import m.module_compiled_env;
+  load_objects m.module_declarations;
   Hashtbl.add modules_table s m;
   m
 
diff --git a/library/nametab.ml b/library/nametab.ml
new file mode 100755
index 000000000..b84eda23a
--- /dev/null
+++ b/library/nametab.ml
@@ -0,0 +1,44 @@
+
+(* $Id$ *)
+
+open Names
+
+let cci_tab = ref Idmap.empty
+let fw_tab = ref Idmap.empty
+
+let fw_sp_of_id id =
+  Idmap.find id !fw_tab
+
+let sp_of_id kind id =
+  match kind with
+    | FW -> Idmap.find id !fw_tab
+    | CCI -> Idmap.find id !cci_tab
+    | OBJ -> invalid_arg "Nametab.sp_of_id"
+	  
+let push id sp =
+  match kind_of_path sp with
+    | FW -> fw_tab := Idmap.add id sp !fw_tab
+    | CCI -> cci_tab := Idmap.add id sp !cci_tab
+    | OBJ -> invalid_arg "Nametab.push"
+
+(* Registration as a global table and roolback. *)
+    
+let init () =
+  cci_tab := Idmap.empty;
+  cci_tab := Idmap.empty
+
+type frozen = section_path Idmap.t * section_path Idmap.t
+
+let freeze () = (!cci_tab, !fw_tab)
+		  
+let unfreeze (cci,fw) = cci_tab := cci; fw_tab := fw
+
+let _ = 
+  Summary.declare_summary "names"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init }
+
+let rollback f x =
+  let fs = freeze () in
+  try f x with e -> begin unfreeze fs; raise e end
diff --git a/library/nametab.mli b/library/nametab.mli
new file mode 100755
index 000000000..2d0cd62eb
--- /dev/null
+++ b/library/nametab.mli
@@ -0,0 +1,17 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+(*i*)
+
+(* This module contains the table for globalization, which associates global
+   names (section paths) to identifiers. *)
+
+val push : identifier -> section_path -> unit
+
+val sp_of_id : path_kind -> identifier -> section_path
+val fw_sp_of_id : identifier -> section_path
+
+val rollback : ('a -> 'b) -> 'a -> 'b
+