- 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

11 files changed, 82 insertions, 69 deletions

diff --git a/kernel/closure.mli b/kernel/closure.mli
index b64f2794b..62caafe55 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -10,12 +10,12 @@ open Evd
 open Environ
 (*i*)
 
-(* flags for profiling... *)
+(* Flags for profiling reductions. *)
 val stats : bool ref
 val share : bool ref
 
 
-(* sets of reduction kinds *)
+(*s The set of reduction kinds. *)
 type red_kind = BETA | DELTA of sorts oper | IOTA
 
 type reds = { 
@@ -31,16 +31,17 @@ val betadeltaiota_red : reds
 val red_set : reds -> red_kind -> bool
 
 
-(* reduction function specification *)
+(*s Reduction function specification. *)
 
 type red_mode = UNIFORM | SIMPL | WITHBACK
 
 type flags = red_mode * reds
 
-(* (UNIFORM,r)  == r-reduce in any context
- * (SIMPL,r)    == bdi-reduce under cases or fix, r otherwise (like hnf does)
- * (WITHBACK,r) == internal use: means we are under a case 
- *                 or in rec. arg. of fix *)
+(* [(UNIFORM,r)]  == [r]-reduce in any context.
+   [(SIMPL,r)]    == bdi-reduce under cases or fix, [r] otherwise 
+   (like hnf does).
+   [(WITHBACK,r)] == internal use: means we are under a case 
+   or in rec. arg. of fix. *)
 
 val flags_under : flags -> flags
 val red_top : flags -> red_kind -> bool
@@ -54,7 +55,7 @@ val betadeltaiota : flags
 val hnf_flags : flags
 
 
-(* Call by value functions *)
+(*s Call by value functions *)
 type cbv_value =
   | VAL of int * constr
   | LAM of name * constr * constr * cbv_value subs
@@ -96,11 +97,10 @@ val apply_stack : 'a cbv_infos -> constr -> stack -> constr
 val cbv_norm_value : 'a cbv_infos -> cbv_value -> constr
 
 
+(*s Lazy reduction. *)
 
-
-
-(* Lazy reduction *)
 type 'a freeze
+
 type 'a frterm =
   | FRel of int
   | FVAR of identifier
diff --git a/kernel/constant.mli b/kernel/constant.mli
index d8aeb7670..890e1f425 100644
--- a/kernel/constant.mli
+++ b/kernel/constant.mli
@@ -7,7 +7,7 @@ open Term
 open Sign
 (*i*)
 
-(* Constants. *)
+(* Constants (internal representation). *)
 
 type discharge_recipe
 
@@ -15,10 +15,6 @@ type recipe =
   | Cooked of constr
   | Recipe of discharge_recipe
 
-type constant_entry = {
-  const_entry_body : constr;
-  const_entry_type : constr option }
-
 type constant_body = {
   const_kind : path_kind;
   const_body : recipe ref option;
@@ -30,3 +26,9 @@ val is_defined : constant_body -> bool
 
 val is_opaque : constant_body -> bool
 
+(*s Constant declaration. *)
+
+type constant_entry= {
+  const_entry_body : constr;
+  const_entry_type : constr option }
+
diff --git a/kernel/doc.tex b/kernel/doc.tex
index 56debc102..4a9fc3550 100644
--- a/kernel/doc.tex
+++ b/kernel/doc.tex
@@ -1,9 +1,11 @@
 
+\newpage
 \section*{The Coq kernel}
 
 \ocwsection \label{kernel}
-This section describes the \Coq\ kernel, which is a type checker for the \CCI.
-
+This chapter describes the \Coq\ kernel, which is a type checker for the \CCI.
 The modules of the kernel are organized as follows.
 
-TODO
+\bigskip
+\begin{center}\epsfig{file=kernel.dep.ps,width=\linewidth}\end{center}
+
diff --git a/kernel/generic.mli b/kernel/generic.mli
index dcd458f8b..b9eb9a512 100644
--- a/kernel/generic.mli
+++ b/kernel/generic.mli
@@ -6,13 +6,8 @@ open Util
 open Names
 (*i*)
 
-(* A generic notion of terms with binders. *)
-
-exception FreeVar
-exception Occur
-
-(* \label{generic_terms}
-   Generic terms, over any kind of operators. *)
+(* \label{generic_terms} A generic notion of terms with binders,
+   over any kind of operators. *)
 
 type 'oper term =
   | DOP0 of 'oper                            (* atomic terms *)
@@ -28,30 +23,42 @@ type 'oper term =
 val isRel  : 'a term -> bool
 val isVAR  : 'a term -> bool
 val free_rels : 'a term -> Intset.t
+
+exception FreeVar
+exception Occur
+
 val closedn : int -> 'a term -> unit
 val closed0 : 'a term -> bool
 val noccurn : int -> 'a term -> bool
 val noccur_bet : int -> int -> 'a term -> bool
 
+(*s Lifts. [ELSHFT(l,n)] == lift of [n], then apply [lift l].
+  [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. *)
 
-(* lifts *)
 type lift_spec =
   | ELID
-  | ELSHFT of lift_spec * int (* ELSHFT(l,n) == lift of n, then apply lift l *)
-  | ELLFT of int * lift_spec  (* ELLFT(n,l)  == apply l to de Bruijn > n *)
-                              (*                 i.e under n binders *)
+  | ELSHFT of lift_spec * int
+  | ELLFT of int * lift_spec
+
 val el_shft : int -> lift_spec -> lift_spec
 val el_lift : lift_spec -> lift_spec
 val el_liftn :  int -> lift_spec -> lift_spec
 val reloc_rel: int -> lift_spec -> int
+val exliftn : lift_spec -> 'a term -> 'a term
+val liftn : int -> int -> 'a term -> 'a term
+val lift : int -> 'a term -> 'a term
+val pop : 'a term -> 'a term
+
+(*s Explicit substitutions of type ['a]. [ESID] = identity. 
+  [CONS(t,S)] = $S.t$ i.e. parallel substitution. [SHIFT(n,S)] = 
+  $(\uparrow n~o~S)$ i.e. terms in S are relocated with n vars. 
+  [LIFT(n,S)] = $(\%n~S)$ stands for $((\uparrow n~o~S).n...1)$. *)
 
-(* explicit substitutions of type 'a *)
 type 'a subs =
-  | ESID                   (* ESID       =          identity *)
-  | CONS of 'a * 'a subs   (* CONS(t,S)  = (S.t)    parallel substitution *)
-  | SHIFT of int * 'a subs (* SHIFT(n,S)= (\^n o S) terms in S are relocated *)
-                           (*                        with n vars *)
-  | LIFT of int * 'a subs  (* LIFT(n,S)=(\%n S) stands for ((\^n o S).n...1) *)
+  | ESID
+  | CONS of 'a * 'a subs
+  | SHIFT of int * 'a subs
+  | LIFT of int * 'a subs
 
 val subs_cons  : 'a * 'a subs -> 'a subs
 val subs_lift  : 'a subs -> 'a subs
@@ -62,10 +69,6 @@ val expand_rel : int -> 'a subs -> (int * 'a, int) union
 type info = Closed | Open | Unknown
 type 'a substituend = { mutable sinfo : info; sit : 'a }
 
-val exliftn : lift_spec -> 'a term -> 'a term
-val liftn : int -> int -> 'a term -> 'a term
-val lift : int -> 'a term -> 'a term
-val pop : 'a term -> 'a term
 val lift_substituend : int -> 'a term substituend -> 'a term
 val make_substituend : 'a term -> 'a term substituend
 val substn_many : 'a term substituend array -> int -> 'a term -> 'a term
@@ -117,7 +120,8 @@ val rel_list : int -> int -> 'a term list
 
 val count_dlam : 'a term -> int
 
-(* For hash-consing use *)
+(*s For hash-consing. *)
+
 val hash_term :
   ('a term -> 'a term)
   * (('a -> 'a) * (name -> name) * (identifier -> identifier))
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index a08136424..d0dee30b9 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -64,6 +64,9 @@ type mutual_inductive_entry = {
   mind_entry_finite : bool;
   mind_entry_inds : (identifier * constr * identifier list * constr) list }
 
+(*s The different kinds of errors that may result of a malformed inductive
+  definition. *)
+
 type inductive_error =
   | NonPos of int   
   | NotEnoughArgs of int
@@ -76,6 +79,9 @@ type inductive_error =
 
 exception InductiveError of inductive_error
 
+(*s The following functions are utility functions to check and to
+  decompose a declaration. *)
+
 (* [mind_check_names] checks the names of an inductive types declaration
    i.e. that all the types and constructors names are distinct. 
    It raises an exception [InductiveError _] if it is not the case. *)
@@ -92,5 +98,4 @@ val mind_extract_and_check_params :
 
 val mind_extract_params : int -> constr -> (name * constr) list * constr
 
-
 val mind_check_lc : (name * constr) list -> mutual_inductive_entry -> unit
diff --git a/kernel/names.ml b/kernel/names.ml
index 6e5835fbb..dc1350fa3 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -78,6 +78,7 @@ module IdOrdered =
   end
 
 module Idset = Set.Make(IdOrdered)
+module Idmap = Map.Make(IdOrdered)
 
 
 (* Fresh names *)
diff --git a/kernel/names.mli b/kernel/names.mli
index c022a84a3..9a7822d11 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -24,6 +24,7 @@ val id_without_number : identifier -> bool
 val first_char : identifier -> string
 
 module Idset : Set.S with type elt = identifier
+module Idmap : Map.S with type key = identifier
 
 val lift_ident : identifier -> identifier
 val next_ident_away_from : identifier -> identifier list -> identifier
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 092e5c078..c67ab11d8 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -7,11 +7,9 @@ open Generic
 open Term
 (*i*)
 
-(* Signatures (with named and de Bruijn variables). *)
+(* Signatures of named variables. *)
 
 type 'a signature = identifier list * 'a list
-type 'a db_signature = (name * 'a) list
-type ('a,'b) env = ENVIRON of 'a signature * 'b db_signature
 
 val nil_sign : 'a signature
 val add_sign : (identifier * 'a) -> 'a signature -> 'a signature
@@ -53,6 +51,10 @@ val dunbindv : identifier -> 'a signature -> 'a -> 'b term
 val dbind : 'a signature -> 'b term -> 'a * 'b term
 val dbindv : 'a signature -> 'b term array -> 'a * 'b term
 
+(*s Signatures with named and de Bruijn variables. *)
+
+type 'a db_signature = (name * 'a) list
+type ('a,'b) env = ENVIRON of 'a signature * 'b db_signature
 
 val gLOB : 'b signature -> ('b,'a) env
 
diff --git a/kernel/term.mli b/kernel/term.mli
index 7c1ee1d33..c36df1f65 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -7,25 +7,20 @@ open Generic
 (*i*)
 
 (*s The operators of the Calculus of Inductive Constructions. 
-  ['a] is the type of sorts. *)
+  ['a] is the type of sorts. ([XTRA] is an extra slot, for putting in 
+  whatever sort of operator we need for whatever sort of application.) *)
 
 type 'a oper = 
-  (* DOP0 *)
   | Meta of int
   | Sort of 'a
-  (* DOP2 *)
   | Cast | Prod | Lambda
-  (* DOPN *)
   | AppL | Const of section_path | Abst of section_path
   | MutInd of section_path * int
   | MutConstruct of (section_path * int) * int
   | MutCase of case_info
   | Fix of int array * int
   | CoFix of int
-
   | XTRA of string
-      (* an extra slot, for putting in whatever sort of
-         operator we need for whatever sort of application *)
 
 and case_info = (section_path * int) option
 
@@ -45,7 +40,7 @@ val mk_Prop : sorts
 
 (*s The type [constr] of the terms of CCI
   is obtained by instanciating the generic terms (type [term], 
-  see \citesec{generic_terms}) on the above operators, themselves instanciated
+  see \refsec{generic_terms}) on the above operators, themselves instanciated
   on the above sorts. *)
 
 type constr = sorts oper term
@@ -295,12 +290,11 @@ val args_of_mconstr : constr -> constr array
 (* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
 val destCase : constr -> case_info * constr * constr * constr array
 
-(* Destructs the ith function of the block  
-    [Fixpoint f1 [ctx1] = b1
-     with     f2 [ctx2] = b2
-     ...
-     with     fn [ctxn] = bn.]
-
+(* Destructs the $i$th function of the block  
+   $\mathit{Fixpoint} ~ f_1 ~ [ctx_1] = b_1
+    \mathit{with}     ~ f_2 ~ [ctx_2] = b_2
+    \dots
+    \mathit{with}     ~ f_n ~ [ctx_n] = b_n$,
    where the lenght of the $j$th context is $ij$.
 *)
 val destGralFix : 
diff --git a/kernel/typing.ml b/kernel/typing.ml
index 1fcf340f3..4a029dfe3 100644
--- a/kernel/typing.ml
+++ b/kernel/typing.ml
@@ -304,18 +304,13 @@ let add_constant sp ce env =
   in
   add_constant sp cb env''
 
-let type_from_judgment env j =
-  match whd_betadeltaiota env j.uj_kind with
-    | DOP0(Sort s) -> { body = j.uj_type; typ = s }
-    | _ -> error_not_type CCI env j.uj_type (* shouldn't happen *)
-
-let add_parameter sp c env =
-  let (j,u) = safe_machine env c in
+let add_parameter sp t env =
+  let (jt,u) = safe_machine env t in
   let env' = set_universes u env in
   let cb = {
     const_kind = kind_of_path sp;
-    const_body = Some (ref (Cooked c));
-    const_type = type_from_judgment env' j;
+    const_body = None;
+    const_type = assumption_of_judgment env' jt;
     const_hyps = get_globals (context env);
     const_opaque = false } 
   in
@@ -424,6 +419,8 @@ let add_mind sp mie env =
 let export = export
 let import = import
 
+let unsafe_env_of_env e = e
+
 (*s Machines with information. *)
 
 type information = Logic | Inf of unsafe_judgment
diff --git a/kernel/typing.mli b/kernel/typing.mli
index 0167c8cd9..639772946 100644
--- a/kernel/typing.mli
+++ b/kernel/typing.mli
@@ -14,7 +14,10 @@ open Environ
 open Typeops
 (*i*)
 
-(*s Safe environments. *)
+(*s Safe environments. Since we are now able to type terms, we can define an
+  abstract type of safe environments, where objects are typed before being
+  added. Internally, the datatype is still [unsafe_env]. We re-export the
+  functions of [Environ] for the new type [environment]. *)
 
 type 'a environment
 
@@ -44,6 +47,8 @@ val lookup_meta : int -> 'a environment -> constr
 val export : 'a environment -> string -> compiled_env
 val import : compiled_env -> 'a environment -> 'a environment
 
+val unsafe_env_of_env : 'a environment -> 'a unsafe_env
+
 (*s Typing without information. *)
 
 type judgment