CLEANUP: kernel/context.ml{,i}

The structure of the Context module was refined in such a way that:
- Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module.
- Types and functions related to rel-context were put into the Context.Rel module.
- Types and functions related to named-context declarations were put into the Context.Named.Declaration module.
- Types and functions related to named-context were put into the Context.Named module.
- Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module.
- Types and functions related to named-list-context were put into Context.NamedList module.

Some missing comments were added to the *.mli file.

The output of ocamldoc was checked whether it looks in a reasonable way.

"TODO: cleanup" was removed

The order in which are exported functions listed in the *.mli file was changed.
(as in a mature modules, this order usually is not random)

The order of exported functions in Context.{Rel,Named} modules is now consistent.
(as there is no special reason why that order should be different)

The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file.
(as there is no special reason to define them in a different order)

The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do.
(Now they are called Context.{Rel,Named}.fold_{inside,outside})

The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated.

Thrown exceptions are now documented.

Naming of formal parameters was made more consistent across different functions.

Comments of similar functions in different modules are now consistent.

Comments from *.mli files were copied to *.ml file.
(We need that information in *.mli files because that is were ocamldoc needs it.
 It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function,
 we can see the comments also there and do not need to open a different file if we want to see it.)

When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1.
(UTF-8 characters are used in our ocamldoc markup)

"open Context" was removed from all *.mli and *.ml files.
(Originally, it was OK to do that. Now it is not.)

An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed.

1 files changed, 149 insertions, 94 deletions

diff --git a/kernel/context.mli b/kernel/context.mli
index 735467747..0db82beb5 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -6,131 +6,186 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** The modules defined below represent a {e local context}
+    as defined by Chapter 4 in the Reference Manual:
+
+    A {e local context} is an ordered list of of {e local declarations}
+    of names that we call {e variables}.
+
+    A {e local declaration} of some variable can be either:
+    - a {e local assumption}, or
+    - a {e local definition}.
+
+    {e Local assumptions} are denoted in the Reference Manual as [(name : typ)] and
+    {e local definitions} are there denoted as [(name := value : typ)].
+*)
+
 open Names
 
-(** TODO: cleanup *)
+(** Representation of contexts that can capture anonymous as well as non-anonymous variables.
+    Individual declarations are then designated by de Bruijn indexes. *)
+module Rel :
+sig
+  (** Representation of {e local declarations}.
+
+      [(name, None, typ)] represents a {e local assumption}.
+
+      [(name, Some value, typ)] represents a {e local definition}.
+   *)
+  module Declaration :
+  sig
+    type t = Name.t * Constr.t option * Constr.t
+
+    (** Map all terms in a given declaration. *)
+    val map : (Constr.t -> Constr.t) -> t -> t
+
+    (** Reduce all terms in a given declaration to a single value. *)
+    val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
+
+    (** Check whether any term in a given declaration satisfies a given predicate. *)
+    val exists : (Constr.t -> bool) -> t -> bool
+
+    (** Check whether all terms in a given declaration satisfy a given predicate. *)
+    val for_all : (Constr.t -> bool) -> t -> bool
+
+    (** Check whether the two given declarations are equal. *)
+    val equal : t -> t -> bool
+  end
+
+  (** Rel-context is represented as a list of declarations.
+      Inner-most declarations are at the beginning of the list.
+      Outer-most declarations are at the end of the list. *)
+  type t = Declaration.t list
+
+  (** empty rel-context *)
+  val empty : t
+
+  (** Return a new rel-context enriched by with a given inner-most declaration. *)
+  val add : Declaration.t -> t -> t
+
+  (** Return a declaration designated by a given de Bruijn index.
+      @raise Not_found if the designated de Bruijn index outside the range. *)
+  val lookup : int -> t -> Declaration.t
+
+  (** Map all terms in a given rel-context. *)
+  val map : (Constr.t -> Constr.t) -> t -> t
 
-(** {6 Declarations} *)
-(** A {e declaration} has the form [(name,body,type)]. It is either an
-    {e assumption} if [body=None] or a {e definition} if
-    [body=Some actualbody]. It is referred by {e name} if [na] is an
-    identifier or by {e relative index} if [na] is not an identifier
-    (in the latter case, [na] is of type [name] but just for printing
-    purpose) *)
+  (** Reduce all terms in a given rel-context to a single value.
+      Innermost declarations are processed first. *)
+  val fold_inside : ('a -> Declaration.t -> 'a) -> init:'a -> t -> 'a
 
-type named_declaration = Id.t * Constr.t option * Constr.t
-type named_list_declaration = Id.t list * Constr.t option * Constr.t
-type rel_declaration = Name.t * Constr.t option * Constr.t
+  (** Reduce all terms in a given rel-context to a single value.
+      Outermost declarations are processed first. *)
+  val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a
 
-val map_named_declaration :
-  (Constr.t -> Constr.t) -> named_declaration -> named_declaration
-val map_named_list_declaration :
-  (Constr.t -> Constr.t) -> named_list_declaration -> named_list_declaration
-val map_rel_declaration :
-  (Constr.t -> Constr.t) -> rel_declaration -> rel_declaration
+  (** Perform a given action on every declaration in a given rel-context. *)
+  val iter : (Constr.t -> unit) -> t -> unit
 
-val fold_named_declaration :
-  (Constr.t -> 'a -> 'a) -> named_declaration -> 'a -> 'a
-val fold_rel_declaration :
-  (Constr.t -> 'a -> 'a) -> rel_declaration -> 'a -> 'a
+  (** Return the number of {e local declarations} in a given context. *)
+  val length : t -> int
 
-val exists_named_declaration :
-  (Constr.t -> bool) -> named_declaration -> bool
-val exists_rel_declaration :
-  (Constr.t -> bool) -> rel_declaration -> bool
+  (** Return the number of {e local assumptions} in a given rel-context. *)
+  val nhyps : t -> int
 
-val for_all_named_declaration :
-  (Constr.t -> bool) -> named_declaration -> bool
-val for_all_rel_declaration :
-  (Constr.t -> bool) -> rel_declaration -> bool
+  (** Map a given rel-context to a list where each {e local assumption} is mapped to [true]
+      and each {e local definition} is mapped to [false]. *)
+  val to_tags : t -> bool list
 
-val eq_named_declaration :
-  named_declaration -> named_declaration -> bool
+  (** [extended_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
+      with n = |Δ| and with the {e local definitions} of [Γ] skipped in
+      [args]. Example: for [x:T, y:=c, z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
+  val to_extended_list : int -> t -> Constr.t list
 
-val eq_rel_declaration :
-    rel_declaration -> rel_declaration -> bool
+  (** [extended_vect n Γ] does the same, returning instead an array. *)
+  val to_extended_vect : int -> t -> Constr.t array
+end
 
-(** {6 Signatures of ordered named declarations } *)
+(** This module represents contexts that can capture non-anonymous variables.
+    Individual declarations are then designated by the identifiers they bind. *)
+module Named :
+sig
+  (** Representation of {e local declarations}.
 
-type named_context = named_declaration list
-type section_context = named_context
-type named_list_context = named_list_declaration list
-type rel_context = rel_declaration list
-(** In [rel_context], more recent declaration is on top *)
+      [(id, None, typ)] represents a {e local assumption}.
 
-val empty_named_context : named_context
-val add_named_decl : named_declaration -> named_context -> named_context
-val vars_of_named_context : named_context -> Id.Set.t
+      [(id, Some value, typ)] represents a {e local definition}.
+   *)
+  module Declaration :
+  sig
+    type t = Id.t * Constr.t option * Constr.t
 
-val lookup_named : Id.t -> named_context -> named_declaration
+    (** Map all terms in a given declaration. *)
+    val map : (Constr.t -> Constr.t) -> t -> t
 
-(** number of declarations *)
-val named_context_length : named_context -> int
+    (** Reduce all terms in a given declaration to a single value. *)
+    val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
 
-(** named context equality *)
-val named_context_equal : named_context -> named_context -> bool
+    (** Check whether any term in a given declaration satisfies a given predicate. *)
+    val exists : (Constr.t -> bool) -> t -> bool
 
-(** {6 Recurrence on [named_context]: older declarations processed first } *)
-val fold_named_context :
-  (named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a
+    (** Check whether all terms in a given declaration satisfy a given predicate. *)
+    val for_all : (Constr.t -> bool) -> t -> bool
 
-val fold_named_list_context :
-  (named_list_declaration -> 'a -> 'a) -> named_list_context -> init:'a -> 'a
+    (** Check whether the two given declarations are equal. *)
+    val equal : t -> t -> bool
+  end
 
-(** newer declarations first *)
-val fold_named_context_reverse :
-  ('a -> named_declaration -> 'a) -> init:'a -> named_context -> 'a
+  (** Rel-context is represented as a list of declarations.
+      Inner-most declarations are at the beginning of the list.
+      Outer-most declarations are at the end of the list. *)
+  type t = Declaration.t list
 
-(** {6 Section-related auxiliary functions } *)
+  (** empty named-context *)
+  val empty : t
 
-(** [instance_from_named_context Ω] builds an instance [args] such
-    that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local
-    definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it
-    gives [Var id1, Var id3]. All [idj] are supposed distinct. *)
-val instance_from_named_context : named_context -> Constr.t list
+  (** Return a new rel-context enriched by with a given inner-most declaration. *)
+  val add : Declaration.t -> t -> t
 
-(** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
-   with n = |Δ| and with the local definitions of [Γ] skipped in
-   [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
-val extended_rel_list : int -> rel_context -> Constr.t list
+  (** Return a declaration designated by an identifier of the variable bound in that declaration.
+      @raise Not_found if the designated identifier is not bound in a given named-context. *)
+  val lookup : Id.t -> t -> Declaration.t
 
-(** [extended_rel_vect n Γ] does the same, returning instead an array. *)
-val extended_rel_vect : int -> rel_context -> Constr.t array
+  (** Map all terms in a given named-context. *)
+  val map : (Constr.t -> Constr.t) -> t -> t
 
-(** {6 ... } *)
-(** Signatures of ordered optionally named variables, intended to be
-   accessed by de Bruijn indices *)
+  (** Reduce all terms in a given named-context to a single value.
+      Innermost declarations are processed first. *)
+  val fold_inside : ('a -> Declaration.t -> 'a) -> init:'a -> t -> 'a
 
-(** {6 Recurrence on [rel_context]: older declarations processed first } *)
-val fold_rel_context :
-  (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
+  (** Reduce all terms in a given named-context to a single value.
+      Outermost declarations are processed first. *)
+  val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a
 
-(** newer declarations first *)
-val fold_rel_context_reverse :
-  ('a -> rel_declaration -> 'a) -> init:'a -> rel_context -> 'a
+  (** Perform a given action on every declaration in a given named-context. *)
+  val iter : (Constr.t -> unit) -> t -> unit
 
-(** {6 Map function of [rel_context] } *)
-val map_rel_context : (Constr.t -> Constr.t) -> rel_context -> rel_context
+  (** Return the number of {e local declarations} in a given named-context. *)
+  val length : t -> int
 
-(** {6 Map function of [named_context] } *)
-val map_named_context : (Constr.t -> Constr.t) -> named_context -> named_context
+  (** Check whether given two named-contexts are equal. *)
+  val equal : t -> t -> bool
 
-(** {6 Map function of [rel_context] } *)
-val iter_rel_context : (Constr.t -> unit) -> rel_context -> unit
+  (** Return the set of all identifiers bound in a given named-context. *)
+  val to_vars : t -> Id.Set.t
 
-(** {6 Map function of [named_context] } *)
-val iter_named_context : (Constr.t -> unit) -> named_context -> unit
+  (** [instance_from_named_context Ω] builds an instance [args] such
+      that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local
+      definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it
+      gives [Var id1, Var id3]. All [idj] are supposed distinct. *)
+  val to_instance : t -> Constr.t list
+end
 
-(** {6 Contexts of declarations referred to by de Bruijn indices } *)
+module NamedList :
+sig
+  module Declaration :
+  sig
+    type t = Id.t list * Constr.t option * Constr.t
+    val map : (Constr.t -> Constr.t) -> t -> t
+  end
 
-val empty_rel_context : rel_context
-val add_rel_decl : rel_declaration -> rel_context -> rel_context
+  type t = Declaration.t list
 
-val lookup_rel : int -> rel_context -> rel_declaration
-(** Size of the [rel_context] including LetIns *)
-val rel_context_length : rel_context -> int
-(** Size of the [rel_context] without LetIns *)
-val rel_context_nhyps : rel_context -> int
-(** Indicates whether a LetIn or a Lambda, starting from oldest declaration *)
-val rel_context_tags : rel_context -> bool list
+  val fold : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a
+end
 
+type section_context = Named.t