CLEANUP: Context.{Rel,Named}.Declaration.t

  Originally, rel-context was represented as:

    Context.rel_context = Names.Name.t * Constr.t option * Constr.t

  Now it is represented as:

    Context.Rel.t = LocalAssum of Names.Name.t * Constr.t
                  | LocalDef of Names.Name.t * Constr.t * Constr.t

  Originally, named-context was represented as:

    Context.named_context = Names.Id.t * Constr.t option * Constr.t

  Now it is represented as:

    Context.Named.t = LocalAssum of Names.Id.t * Constr.t
                    | LocalDef of Names.Id.t * Constr.t * Constr.t

Motivation:

  (1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction"
      function which looked like this:

        let test_strict_disjunction n lc =
          Array.for_all_i (fun i c ->
            match (prod_assum (snd (decompose_prod_n_assum n c))) with
            | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i)
            | _ -> false) 0 lc

      Suppose that you do not know about rel-context and named-context.
      (that is the case of people who just started to read the source code)
      Merlin would tell you that the type of the value you are destructing
      by "match" is:

        'a * 'b option * Constr.t                    (* worst-case scenario *)

      or

        Named.Name.t * Constr.t option * Constr.t    (* best-case scenario (?) *)

      To me, this is akin to wearing an opaque veil.
      It is hard to figure out the meaning of the values you are looking at.
      In particular, it is hard to discover the connection between the value
      we are destructing above and the datatypes and functions defined
      in the "kernel/context.ml" file.

      In this case, the connection is there, but it is not visible
      (between the function above and the "Context" module).

      ------------------------------------------------------------------------

      Now consider, what happens when the reader see the same function
      presented in the following form:

        let test_strict_disjunction n lc =
          Array.for_all_i (fun i c ->
            match (prod_assum (snd (decompose_prod_n_assum n c))) with
            | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i)
            | _ -> false) 0 lc

      If the reader haven't seen "LocalAssum" before, (s)he can use Merlin
      to jump to the corresponding definition and learn more.

      In this case, the connection is there, and it is directly visible
      (between the function above and the "Context" module).

  (2) Also, if we already have the concepts such as:
      - local declaration
      - local assumption
      - local definition
      and we describe these notions meticulously in the Reference Manual,
      then it is a real pity not to reinforce the connection
      of the actual code with the abstract description we published.

1 files changed, 110 insertions, 41 deletions

diff --git a/kernel/context.mli b/kernel/context.mli
index 1976e46d3..a69754cc2 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -26,21 +26,32 @@ open Names
     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
+    (* local declaration *)
+    type t = LocalAssum of Name.t * Constr.t            (* local assumption *)
+	   | LocalDef of Name.t * Constr.t * Constr.t   (* local definition *)
 
-    (** Map all terms in a given declaration. *)
-    val map : (Constr.t -> Constr.t) -> t -> t
+    (** Return the name bound by a given declaration. *)
+    val get_name : t -> Name.t
 
-    (** Reduce all terms in a given declaration to a single value. *)
-    val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
+    (** Return [Some value] for local-declarations and [None] for local-assumptions. *)
+    val get_value : t -> Constr.t option
+
+    (** Return the type of the name bound by a given declaration. *)
+    val get_type : t -> Constr.t
+
+    (** Set the name that is bound by a given declaration. *)
+    val set_name : Name.t -> t -> t
+
+    (** Set the type of the bound variable in a given declaration. *)
+    val set_type : Constr.t -> t -> t
+
+    (** Return [true] iff a given declaration is a local assumption. *)
+    val is_local_assum : t -> bool
+
+    (** Return [true] iff a given declaration is a local definition. *)
+    val is_local_def : t -> bool
 
     (** Check whether any term in a given declaration satisfies a given predicate. *)
     val exists : (Constr.t -> bool) -> t -> bool
@@ -50,6 +61,28 @@ sig
 
     (** Check whether the two given declarations are equal. *)
     val equal : t -> t -> bool
+
+    (** Map the name bound by a given declaration. *)
+    val map_name : (Name.t -> Name.t) -> t -> t
+
+    (** For local assumptions, this function returns the original local assumptions.
+        For local definitions, this function maps the value in the local definition. *)
+    val map_value : (Constr.t -> Constr.t) -> t -> t
+
+    (** Map the type of the name bound by a given declaration. *)
+    val map_type : (Constr.t -> Constr.t) -> t -> t
+
+    (** Map all terms in a given declaration. *)
+    val map_constr : (Constr.t -> Constr.t) -> t -> t
+
+    (** Perform a given action on all terms in a given declaration. *)
+    val iter_constr : (Constr.t -> unit) -> t -> unit
+
+    (** Reduce all terms in a given declaration to a single value. *)
+    val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
+
+    val to_tuple : t -> Name.t * Constr.t option * Constr.t
+    val of_tuple : Name.t * Constr.t option * Constr.t -> t
   end
 
   (** Rel-context is represented as a list of declarations.
@@ -63,6 +96,15 @@ sig
   (** Return a new rel-context enriched by with a given inner-most declaration. *)
   val add : Declaration.t -> t -> t
 
+  (** Return the number of {e local declarations} in a given context. *)
+  val length : t -> int
+
+  (** Check whether given two rel-contexts are equal. *)
+  val equal : t -> t -> bool
+
+  (** Return the number of {e local assumptions} in a given rel-context. *)
+  val nhyps : t -> int
+
   (** 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
@@ -70,6 +112,9 @@ sig
   (** Map all terms in a given rel-context. *)
   val map : (Constr.t -> Constr.t) -> t -> t
 
+  (** Perform a given action on every declaration in a given rel-context. *)
+  val iter : (Constr.t -> unit) -> t -> unit
+
   (** 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
@@ -78,15 +123,6 @@ sig
       Outermost declarations are processed first. *)
   val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a
 
-  (** Perform a given action on every declaration in a given rel-context. *)
-  val iter : (Constr.t -> unit) -> t -> unit
-
-  (** Return the number of {e local declarations} in a given context. *)
-  val length : t -> int
-
-  (** Return the number of {e local assumptions} in a given rel-context. *)
-  val nhyps : t -> int
-
   (** 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
@@ -104,21 +140,32 @@ end
     Individual declarations are then designated by the identifiers they bind. *)
 module Named :
 sig
-  (** Representation of {e local declarations}.
-
-      [(id, None, typ)] represents a {e local assumption}.
-
-      [(id, Some value, typ)] represents a {e local definition}.
-   *)
+  (** Representation of {e local declarations}. *)
   module Declaration :
   sig
-    type t = Id.t * Constr.t option * Constr.t
+    type t = LocalAssum of Id.t * Constr.t
+           | LocalDef of Id.t * Constr.t * Constr.t
 
-    (** Map all terms in a given declaration. *)
-    val map : (Constr.t -> Constr.t) -> t -> t
+    (** Return the identifier bound by a given declaration. *)
+    val get_id : t -> Id.t
 
-    (** Reduce all terms in a given declaration to a single value. *)
-    val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
+    (** Return [Some value] for local-declarations and [None] for local-assumptions. *)
+    val get_value : t -> Constr.t option
+
+    (** Return the type of the name bound by a given declaration. *)
+    val get_type : t -> Constr.t
+
+    (** Set the identifier that is bound by a given declaration. *)
+    val set_id : Id.t -> t -> t
+
+    (** Set the type of the bound variable in a given declaration. *)
+    val set_type : Constr.t -> t -> t
+
+    (** Return [true] iff a given declaration is a local assumption. *)
+    val is_local_assum : t -> bool
+
+    (** Return [true] iff a given declaration is a local definition. *)
+    val is_local_def : t -> bool
 
     (** Check whether any term in a given declaration satisfies a given predicate. *)
     val exists : (Constr.t -> bool) -> t -> bool
@@ -128,6 +175,28 @@ sig
 
     (** Check whether the two given declarations are equal. *)
     val equal : t -> t -> bool
+
+    (** Map the identifier bound by a given declaration. *)
+    val map_id : (Id.t -> Id.t) -> t -> t
+
+    (** For local assumptions, this function returns the original local assumptions.
+        For local definitions, this function maps the value in the local definition. *)
+    val map_value : (Constr.t -> Constr.t) -> t -> t
+
+    (** Map the type of the name bound by a given declaration. *)
+    val map_type : (Constr.t -> Constr.t) -> t -> t
+
+    (** Map all terms in a given declaration. *)
+    val map_constr : (Constr.t -> Constr.t) -> t -> t
+
+    (** Perform a given action on all terms in a given declaration. *)
+    val iter_constr : (Constr.t -> unit) -> t -> unit
+
+    (** Reduce all terms in a given declaration to a single value. *)
+    val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a
+
+    val to_tuple : t -> Id.t * Constr.t option * Constr.t
+    val of_tuple : Id.t * Constr.t option * Constr.t -> t
   end
 
   (** Rel-context is represented as a list of declarations.
@@ -141,13 +210,22 @@ sig
   (** Return a new rel-context enriched by with a given inner-most declaration. *)
   val add : Declaration.t -> t -> t
 
+  (** Return the number of {e local declarations} in a given named-context. *)
+  val length : t -> int
+
   (** 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
 
+  (** Check whether given two rel-contexts are equal. *)
+  val equal : t -> t -> bool
+
   (** Map all terms in a given named-context. *)
   val map : (Constr.t -> Constr.t) -> t -> t
 
+  (** Perform a given action on every declaration in a given named-context. *)
+  val iter : (Constr.t -> unit) -> t -> unit
+
   (** 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
@@ -156,15 +234,6 @@ sig
       Outermost declarations are processed first. *)
   val fold_outside : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a
 
-  (** Perform a given action on every declaration in a given named-context. *)
-  val iter : (Constr.t -> unit) -> t -> unit
-
-  (** Return the number of {e local declarations} in a given named-context. *)
-  val length : t -> int
-
-  (** Check whether given two named-contexts are equal. *)
-  val equal : t -> t -> bool
-
   (** Return the set of all identifiers bound in a given named-context. *)
   val to_vars : t -> Id.Set.t
 
@@ -180,7 +249,7 @@ sig
   module Declaration :
   sig
     type t = Id.t list * Constr.t option * Constr.t
-    val map : (Constr.t -> Constr.t) -> t -> t
+    val map_constr : (Constr.t -> Constr.t) -> t -> t
   end
 
   type t = Declaration.t list