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, 226 insertions, 130 deletions

diff --git a/kernel/context.ml b/kernel/context.ml
index 5923048fa..372f16a8d 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -15,137 +15,233 @@
 (* This file defines types and combinators regarding indexes-based and
    names-based contexts *)
 
-open Util
-open Names
-
-(***************************************************************************)
-(*     Type of assumptions                                                 *)
-(***************************************************************************)
-
-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
-
-let map_named_declaration_skel f (id, (v : Constr.t option), ty) =
-  (id, Option.map f v, f ty)
-let map_named_list_declaration = map_named_declaration_skel
-let map_named_declaration = map_named_declaration_skel
-
-let map_rel_declaration = map_named_declaration
-
-let fold_named_declaration f (_, v, ty) a = f ty (Option.fold_right f v a)
-let fold_rel_declaration = fold_named_declaration
-
-let exists_named_declaration f (_, v, ty) = Option.cata f false v || f ty
-let exists_rel_declaration f (_, v, ty) = Option.cata f false v || f ty
-
-let for_all_named_declaration f (_, v, ty) = Option.cata f true v && f ty
-let for_all_rel_declaration f (_, v, ty) = Option.cata f true v && f ty
-
-let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
-  Id.equal i1 i2 && Option.equal Constr.equal c1 c2 && Constr.equal t1 t2
-
-let eq_rel_declaration (n1, c1, t1) (n2, c2, t2) =
-  Name.equal n1 n2 && Option.equal Constr.equal c1 c2 && Constr.equal t1 t2
-
-(***************************************************************************)
-(*     Type of local contexts (telescopes)                                 *)
-(***************************************************************************)
-
-(*s Signatures of ordered optionally named variables, intended to be
-   accessed by de Bruijn indices (to represent bound variables) *)
-
-type rel_context = rel_declaration list
-
-let empty_rel_context = []
-
-let add_rel_decl d ctxt = d::ctxt
-
-let rec lookup_rel n sign =
-  match n, sign with
-  | 1, decl :: _ -> decl
-  | n, _ :: sign -> lookup_rel (n-1) sign
-  | _, []        -> raise Not_found
-
-let rel_context_length = List.length
+(** The modules defined below represent a {e local context}
+    as defined by Chapter 4 in the Reference Manual:
 
-let rel_context_nhyps hyps =
-  let rec nhyps acc = function
-    | [] -> acc
-    | (_,None,_)::hyps -> nhyps (1+acc) hyps
-    | (_,Some _,_)::hyps -> nhyps acc hyps in
-  nhyps 0 hyps
+    A {e local context} is an ordered list of of {e local declarations}
+    of names that we call {e variables}.
 
-let rel_context_tags ctx =
-  let rec aux l = function
-  | [] -> l
-  | (_,Some _,_)::ctx -> aux (true::l) ctx
-  | (_,None,_)::ctx -> aux (false::l) ctx
-  in aux [] ctx
+    A {e local declaration} of some variable can be either:
+    - a {e local assumption}, or
+    - a {e local definition}.
+*)
 
-(*s Signatures of named hypotheses. Used for section variables and
-    goal assumptions. *)
-
-type named_context = named_declaration list
-type named_list_context = named_list_declaration list
-
-let empty_named_context = []
-
-let add_named_decl d sign = d::sign
-
-let rec lookup_named id = function
-  | (id',_,_ as decl) :: _ when Id.equal id id' -> decl
-  | _ :: sign -> lookup_named id sign
-  | [] -> raise Not_found
-
-let named_context_length = List.length
-let named_context_equal = List.equal eq_named_declaration
-
-let vars_of_named_context ctx =
-  List.fold_left (fun accu (id, _, _) -> Id.Set.add id accu) Id.Set.empty ctx
-
-let instance_from_named_context sign =
-  let filter = function
-  | (id, None, _) -> Some (Constr.mkVar id)
-  | (_, Some _, _) -> None
-  in
-  List.map_filter filter sign
-
-(** [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]. *)
-
-let extended_rel_list n hyps =
-  let rec reln l p = function
-  | (_, None, _) :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps
-  | (_, Some _, _) :: hyps -> reln l (p+1) hyps
-  | [] -> l
-  in
-  reln [] 1 hyps
-
-let extended_rel_vect n hyps = Array.of_list (extended_rel_list n hyps)
-
-let fold_named_context f l ~init = List.fold_right f l init
-let fold_named_list_context f l ~init = List.fold_right f l init
-let fold_named_context_reverse f ~init l = List.fold_left f init l
-
-(*s Signatures of ordered section variables *)
-type section_context = named_context
-
-let fold_rel_context f l ~init:x = List.fold_right f l x
-let fold_rel_context_reverse f ~init:x l = List.fold_left f x l
-
-let map_context f l =
-  let map_decl (n, body_o, typ as decl) =
-    let body_o' = Option.smartmap f body_o in
-    let typ' = f typ in
-      if body_o' == body_o && typ' == typ then decl else
-        (n, body_o', typ')
-  in
-    List.smartmap map_decl l
-
-let map_rel_context = map_context
-let map_named_context = map_context
+open Util
+open Names
 
-let iter_rel_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b)
-let iter_named_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b)
+(** Representation of contexts that can capture anonymous as well as non-anonymous variables.
+    Individual declarations are then designated by de Bruijn indexes. *)
+module Rel =
+  struct
+    (** Representation of {e local declarations}.
+
+        [(name, None, typ)] represents a {e local assumption}.
+        In the Reference Manual we denote them as [(name:typ)].
+
+        [(name, Some value, typ)] represents a {e local definition}.
+        In the Reference Manual we denote them as [(name := value : typ)].
+    *)
+    module Declaration =
+      struct
+	type t = Name.t * Constr.t option * Constr.t
+
+	(** Map all terms in a given declaration. *)
+	let map f (n, v, ty) = (n, Option.map f v, f ty)
+
+	(** Reduce all terms in a given declaration to a single value. *)
+	let fold f (_, v, ty) a = f ty (Option.fold_right f v a)
+
+	(** Check whether any term in a given declaration satisfies a given predicate. *)
+	let exists f (_, v, ty) = Option.cata f false v || f ty
+
+	(** Check whether all terms in a given declaration satisfy a given predicate. *)
+	let for_all f (_, v, ty) = Option.cata f true v && f ty
+
+	(** Check whether the two given declarations are equal. *)
+	let equal (n1, v1, ty1) (n2, v2, ty2) =
+	  Name.equal n1 n2 && Option.equal Constr.equal v1 v2 && Constr.equal ty1 ty2
+      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 *)
+    let empty = []
+
+    (** Return a new rel-context enriched by with a given inner-most declaration. *)
+    let add d ctx = d :: ctx
+
+    (** Return a declaration designated by a given de Bruijn index.
+        @raise Not_found if the designated de Bruijn index is not present in the designated rel-context. *)
+    let rec lookup n ctx =
+      match n, ctx with
+      | 1, decl :: _ -> decl
+      | n, _ :: sign -> lookup (n-1) sign
+      | _, []        -> raise Not_found
+
+    (** Map all terms in a given rel-context. *)
+    let map f =
+      let map_decl (n, body_o, typ as decl) =
+	let body_o' = Option.smartmap f body_o in
+	let typ' = f typ in
+	if body_o' == body_o && typ' == typ then decl else
+          (n, body_o', typ')
+      in
+      List.smartmap map_decl
+
+    (** Reduce all terms in a given rel-context to a single value.
+        Innermost declarations are processed first. *)
+    let fold_inside f ~init = List.fold_left f init
+
+    (** Reduce all terms in a given rel-context to a single value.
+        Outermost declarations are processed first. *)
+    let fold_outside f l ~init = List.fold_right f l init
+
+    (** Perform a given action on every declaration in a given rel-context. *)
+    let iter f = List.iter (fun (_,b,t) -> f t; Option.iter f b)
+
+    (** Return the number of {e local declarations} in a given context. *)
+    let length = List.length
+
+    (** [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]. *)
+    let nhyps =
+      let rec nhyps acc = function
+	| [] -> acc
+	| (_,None,_)::hyps -> nhyps (1+acc) hyps
+	| (_,Some _,_)::hyps -> nhyps acc hyps in
+      nhyps 0
+
+    (** 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]. *)
+    let to_tags =
+      let rec aux l = function
+	| [] -> l
+	| (_,Some _,_)::ctx -> aux (true::l) ctx
+	| (_,None,_)::ctx -> aux (false::l) ctx
+      in aux []
+
+    (** [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]. *)
+    let to_extended_list n =
+      let rec reln l p = function
+	| (_, None, _) :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps
+	| (_, Some _, _) :: hyps -> reln l (p+1) hyps
+	| [] -> l
+      in
+      reln [] 1
+
+    (** [extended_vect n Γ] does the same, returning instead an array. *)
+    let to_extended_vect n hyps = Array.of_list (to_extended_list n hyps)
+  end
+
+(** This module represents contexts that can capture non-anonymous variables.
+    Individual declarations are then designated by the identifiers they bind. *)
+module Named =
+  struct
+    (** Representation of {e local declarations}.
+
+        [(id, None, typ)] represents a {e local assumption}.
+        In the Reference Manual we denote them as [(name:typ)].
+
+        [(id, Some value, typ)] represents a {e local definition}.
+        In the Reference Manual we denote them as [(name := value : typ)].
+   *)
+    module Declaration =
+      struct
+	(** Named-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 = Id.t * Constr.t option * Constr.t
+
+	(** Map all terms in a given declaration. *)
+	let map = Rel.Declaration.map
+
+	(** Reduce all terms in a given declaration to a single value. *)
+	let fold f (_, v, ty) a = f ty (Option.fold_right f v a)
+
+	(** Check whether any term in a given declaration satisfies a given predicate. *)
+	let exists f (_, v, ty) = Option.cata f false v || f ty
+
+	(** Check whether all terms in a given declaration satisfy a given predicate. *)
+	let for_all f (_, v, ty) = Option.cata f true v && f ty
+
+	(** Check whether the two given declarations are equal. *)
+	let equal (i1, v1, ty1) (i2, v2, ty2) =
+	  Id.equal i1 i2 && Option.equal Constr.equal v1 v2 && Constr.equal ty1 ty2
+      end
+
+    type t = Declaration.t list
+
+    (** empty named-context *)
+    let empty = []
+
+    (** empty named-context *)
+    let add d ctx = d :: ctx
+
+    (** Return a declaration designated by a given de Bruijn index.
+        @raise Not_found if the designated identifier is not present in the designated named-context. *)
+    let rec lookup id = function
+      | (id',_,_ as decl) :: _ when Id.equal id id' -> decl
+      | _ :: sign -> lookup id sign
+      | [] -> raise Not_found
+
+    (** Map all terms in a given named-context. *)
+    let map f =
+      let map_decl (n, body_o, typ as decl) =
+	let body_o' = Option.smartmap f body_o in
+	let typ' = f typ in
+	if body_o' == body_o && typ' == typ then decl else
+          (n, body_o', typ')
+      in
+      List.smartmap map_decl
+
+    (** Reduce all terms in a given named-context to a single value.
+        Innermost declarations are processed first. *)
+    let fold_inside f ~init = List.fold_left f init
+
+    (** Reduce all terms in a given named-context to a single value.
+        Outermost declarations are processed first. *)
+    let fold_outside f l ~init = List.fold_right f l init
+
+    (** Perform a given action on every declaration in a given named-context. *)
+    let iter f = List.iter (fun (_,b,t) -> f t; Option.iter f b)
+
+    (** Return the number of {e local declarations} in a given named-context. *)
+    let length = List.length
+
+    (** Check whether given two named-contexts are equal. *)
+    let equal = List.equal Declaration.equal
+
+    (** Return the set of all identifiers bound in a given named-context. *)
+    let to_vars =
+      List.fold_left (fun accu (id, _, _) -> Id.Set.add id accu) Id.Set.empty
+
+    (** [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. *)
+    let to_instance =
+      let filter = function
+	| (id, None, _) -> Some (Constr.mkVar id)
+	| (_, Some _, _) -> None
+      in
+      List.map_filter filter
+  end
+
+module NamedList =
+  struct
+    module Declaration =
+      struct
+	type t = Id.t list * Constr.t option * Constr.t
+	let map = Named.Declaration.map
+      end
+    type t = Declaration.t list
+    let fold f l ~init = List.fold_right f l init
+  end
+
+type section_context = Named.t