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, 269 insertions, 95 deletions

diff --git a/kernel/context.ml b/kernel/context.ml
index 3be1e8323..cc1e6f176 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -33,33 +33,122 @@ open Names
     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)].
-    *)
+    (** Representation of {e local declarations}. *)
     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)
+	(* local declaration *)
+	type t = LocalAssum of Name.t * Constr.t            (* local assumption *)
+	       | LocalDef of Name.t * Constr.t * Constr.t   (* local definition *)
+
+	(** Return the name bound by a given declaration. *)
+	let get_name = function
+	  | LocalAssum (na,_)
+	  | LocalDef (na,_,_) -> na
+
+	(** Return [Some value] for local-declarations and [None] for local-assumptions. *)
+	let get_value = function
+	  | LocalAssum _ -> None
+	  | LocalDef (_,v,_) -> Some v
+
+	(** Return the type of the name bound by a given declaration. *)
+	let get_type = function
+	  | LocalAssum (_,ty)
+	  | LocalDef (_,_,ty) -> ty
+
+	(** Set the name that is bound by a given declaration. *)
+	let set_name na = function
+	  | LocalAssum (_,ty) -> LocalAssum (na, ty)
+	  | LocalDef (_,v,ty) -> LocalDef (na, v, ty)
+
+        (** Set the type of the bound variable in a given declaration. *)
+        let set_type ty = function
+          | LocalAssum (na,_) -> LocalAssum (na, ty)
+          | LocalDef (na,v,_) -> LocalDef (na, v, ty)
+
+	(** Return [true] iff a given declaration is a local assumption. *)
+	let is_local_assum = function
+	  | LocalAssum _ -> true
+	  | LocalDef _ -> false
+
+	(** Return [true] iff a given declaration is a local definition. *)
+	let is_local_def = function
+	  | LocalAssum _ -> false
+	  | LocalDef _ -> true
 
 	(** Check whether any term in a given declaration satisfies a given predicate. *)
-	let exists f (_, v, ty) = Option.cata f false v || f ty
+	let exists f = function
+	  | LocalAssum (_, ty) -> f ty
+	  | LocalDef (_, v, ty) -> f 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
+	let for_all f = function
+	  | LocalAssum (_, ty) -> f ty
+	  | LocalDef (_, v, ty) -> f 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
+	let equal decl1 decl2 =
+	  match decl1, decl2 with
+	  | LocalAssum (n1,ty1), LocalAssum (n2, ty2) ->
+	     Name.equal n1 n2 && Constr.equal ty1 ty2
+	  | LocalDef (n1,v1,ty1), LocalDef (n2,v2,ty2) ->
+	     Name.equal n1 n2 && Constr.equal v1 v2 && Constr.equal ty1 ty2
+	  | _ ->
+	     false
+
+	(** Map the name bound by a given declaration. *)
+	let map_name f = function
+          | LocalAssum (na, ty) as decl ->
+             let na' = f na in
+             if na == na' then decl else LocalAssum (na', ty)
+          | LocalDef (na, v, ty) as decl ->
+             let na' = f na in
+             if na == na' then decl else LocalDef (na', v, ty)
+
+        (** For local assumptions, this function returns the original local assumptions.
+            For local definitions, this function maps the value in the local definition. *)
+        let map_value f = function
+          | LocalAssum _ as decl -> decl
+          | LocalDef (na, v, t) as decl ->
+             let v' = f v in
+             if v == v' then decl else LocalDef (na, v', t)
+
+	(** Map the type of the name bound by a given declaration. *)
+	let map_type f = function
+	  | LocalAssum (na, ty) as decl ->
+             let ty' = f ty in
+             if ty == ty' then decl else LocalAssum (na, ty')
+	  | LocalDef (na, v, ty) as decl ->
+             let ty' = f ty in
+             if ty == ty' then decl else LocalDef (na, v, ty')
+
+	(** Map all terms in a given declaration. *)
+	let map_constr f = function
+          | LocalAssum (na, ty) as decl ->
+             let ty' = f ty in
+             if ty == ty' then decl else LocalAssum (na, ty')
+          | LocalDef (na, v, ty) as decl ->
+             let v' = f v in
+             let ty' = f ty in
+             if v == v' && ty == ty' then decl else LocalDef (na, v', ty')
+
+	(** Perform a given action on all terms in a given declaration. *)
+	let iter_constr f = function
+	  | LocalAssum (_,ty) -> f ty
+	  | LocalDef (_,v,ty) -> f v; f ty
+
+	(** Reduce all terms in a given declaration to a single value. *)
+	let fold f decl acc =
+	  match decl with
+	  | LocalAssum (n,ty) -> f ty acc
+	  | LocalDef (n,v,ty) -> f ty (f v acc)
+
+        let to_tuple = function
+          | LocalAssum (na, ty) -> na, None, ty
+          | LocalDef (na, v, ty) -> na, Some v, ty
+
+	let of_tuple = function
+	  | n, None, ty -> LocalAssum (n,ty)
+	  | n, Some v, ty -> LocalDef (n,v,ty)
       end
 
     (** Rel-context is represented as a list of declarations.
@@ -73,6 +162,21 @@ module Rel =
     (** Return a new rel-context enriched by with a given inner-most declaration. *)
     let add d ctx = d :: ctx
 
+    (** 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 open Declaration in
+      let rec nhyps acc = function
+	| [] -> acc
+	| LocalAssum _ :: hyps -> nhyps (succ acc) hyps
+	| LocalDef _ :: hyps -> nhyps acc hyps
+      in
+      nhyps 0
+
     (** 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 =
@@ -81,15 +185,14 @@ module Rel =
       | n, _ :: sign -> lookup (n-1) sign
       | _, []        -> raise Not_found
 
+    (** Check whether given two rel-contexts are equal. *)
+    let equal = List.equal Declaration.equal
+
     (** 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
+    let map f = List.smartmap (Declaration.map_constr f)
+
+    (** Perform a given action on every declaration in a given rel-context. *)
+    let iter f = List.iter (Declaration.iter_constr f)
 
     (** Reduce all terms in a given rel-context to a single value.
         Innermost declarations are processed first. *)
@@ -99,29 +202,13 @@ module Rel =
         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
+	| Declaration.LocalDef _ :: ctx -> aux (true::l) ctx
+	| Declaration.LocalAssum _ :: ctx -> aux (false::l) ctx
       in aux []
 
     (** [extended_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
@@ -129,8 +216,8 @@ module Rel =
         [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
+	| Declaration.LocalAssum _ :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps
+	| Declaration.LocalDef _ :: hyps -> reln l (p+1) hyps
 	| [] -> l
       in
       reln [] 1
@@ -143,38 +230,127 @@ module Rel =
     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)].
-   *)
+    (** Representation of {e local declarations}. *)
     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)
+        (** local declaration *)
+	type t = LocalAssum of Id.t * Constr.t
+               | LocalDef of Id.t * Constr.t * Constr.t
+
+        (** Return the identifier bound by a given declaration. *)
+	let get_id = function
+          | LocalAssum (id,_) -> id
+          | LocalDef (id,_,_) -> id
+
+	(** Return [Some value] for local-declarations and [None] for local-assumptions. *)
+	let get_value = function
+	  | LocalAssum _ -> None
+	  | LocalDef (_,v,_) -> Some v
+
+	(** Return the type of the name bound by a given declaration. *)
+	let get_type = function
+          | LocalAssum (_,ty)
+          | LocalDef (_,_,ty) -> ty
+
+	(** Set the identifier that is bound by a given declaration. *)
+	let set_id id = function
+          | LocalAssum (_,ty) -> LocalAssum (id, ty)
+          | LocalDef (_, v, ty) -> LocalDef (id, v, ty)
+
+        (** Set the type of the bound variable in a given declaration. *)
+        let set_type ty = function
+          | LocalAssum (id,_) -> LocalAssum (id, ty)
+          | LocalDef (id,v,_) -> LocalDef (id, v, ty)
+
+	(** Return [true] iff a given declaration is a local assumption. *)
+	let is_local_assum = function
+	  | LocalAssum _ -> true
+	  | LocalDef _ -> false
+
+	(** Return [true] iff a given declaration is a local definition. *)
+	let is_local_def = function
+	  | LocalDef _ -> true
+	  | LocalAssum _ -> false
 
 	(** Check whether any term in a given declaration satisfies a given predicate. *)
-	let exists f (_, v, ty) = Option.cata f false v || f ty
+	let exists f = function
+          | LocalAssum (_, ty) -> f ty
+          | LocalDef (_, v, ty) -> f 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
+	let for_all f = function
+          | LocalAssum (_, ty) -> f ty
+          | LocalDef (_, v, ty) -> f 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
+	let equal decl1 decl2 =
+          match decl1, decl2 with
+          | LocalAssum (id1, ty1), LocalAssum (id2, ty2) ->
+             Id.equal id1 id2 && Constr.equal ty1 ty2
+          | LocalDef (id1, v1, ty1), LocalDef (id2, v2, ty2) ->
+             Id.equal id1 id2 && Constr.equal v1 v2 && Constr.equal ty1 ty2
+          | _ ->
+             false
+
+	(** Map the identifier bound by a given declaration. *)
+	let map_id f = function
+          | LocalAssum (id, ty) as decl ->
+             let id' = f id in
+             if id == id' then decl else LocalAssum (id', ty)
+          | LocalDef (id, v, ty) as decl ->
+             let id' = f id in
+             if id == id' then decl else LocalDef (id', v, ty)
+
+        (** For local assumptions, this function returns the original local assumptions.
+            For local definitions, this function maps the value in the local definition. *)
+        let map_value f = function
+          | LocalAssum _ as decl -> decl
+          | LocalDef (na, v, t) as decl ->
+             let v' = f v in
+             if v == v' then decl else LocalDef (na, v', t)
+
+	(** Map the type of the name bound by a given declaration. *)
+	let map_type f = function
+	  | LocalAssum (id, ty) as decl ->
+             let ty' = f ty in
+             if ty == ty' then decl else LocalAssum (id, ty')
+	  | LocalDef (id, v, ty) as decl ->
+             let ty' = f ty in
+             if ty == ty' then decl else LocalDef (id, v, ty')
+
+	(** Map all terms in a given declaration. *)
+	let map_constr f = function
+          | LocalAssum (id, ty) as decl ->
+             let ty' = f ty in
+             if ty == ty' then decl else LocalAssum (id, ty')
+          | LocalDef (id, v, ty) as decl ->
+             let v' = f v in
+             let ty' = f ty in
+             if v == v' && ty == ty' then decl else LocalDef (id, v', ty')
+
+	(** Perform a given action on all terms in a given declaration. *)
+	let iter_constr f = function
+	  | LocalAssum (_, ty) -> f ty
+          | LocalDef (_, v, ty) -> f v; f ty
+
+	(** Reduce all terms in a given declaration to a single value. *)
+	let fold f decl a =
+          match decl with
+          | LocalAssum (_, ty) -> f ty a
+          | LocalDef (_, v, ty) -> a |> f v |> f ty
+
+        let to_tuple = function
+          | LocalAssum (id, ty) -> id, None, ty
+          | LocalDef (id, v, ty) -> id, Some v, ty
+
+        let of_tuple = function
+          | id, None, ty -> LocalAssum (id, ty)
+          | id, Some v, ty -> LocalDef (id, v, ty)
       end
 
+    (** 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 = Declaration.t list
 
     (** empty named-context *)
@@ -183,22 +359,23 @@ module Named =
     (** empty named-context *)
     let add d ctx = d :: ctx
 
+    (** Return the number of {e local declarations} in a given named-context. *)
+    let length = List.length
+
     (** 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
+        @raise Not_found if the designated identifier is not present in the designated named-context. *)   let rec lookup id = function
+       | decl :: _ when Id.equal id (Declaration.get_id decl) -> decl
+       | _ :: sign -> lookup id sign
+       | [] -> raise Not_found
+
+    (** Check whether given two named-contexts are equal. *)
+    let equal = List.equal Declaration.equal
 
     (** 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
+    let map f = List.smartmap (Declaration.map_constr f)
+
+    (** Perform a given action on every declaration in a given named-context. *)
+    let iter f = List.iter (Declaration.iter_constr f)
 
     (** Reduce all terms in a given named-context to a single value.
         Innermost declarations are processed first. *)
@@ -208,18 +385,9 @@ module Named =
         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
+      List.fold_left (fun accu decl -> Id.Set.add (Declaration.get_id decl) accu) Id.Set.empty
 
     (** [instance_from_named_context Ω] builds an instance [args] such
         that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local
@@ -227,8 +395,8 @@ module Named =
         gives [Var id1, Var id3]. All [idj] are supposed distinct. *)
     let to_instance =
       let filter = function
-	| (id, None, _) -> Some (Constr.mkVar id)
-	| (_, Some _, _) -> None
+        | Declaration.LocalAssum (id, _) -> Some (Constr.mkVar id)
+        | _ -> None
       in
       List.map_filter filter
   end
@@ -238,9 +406,15 @@ module NamedList =
     module Declaration =
       struct
 	type t = Id.t list * Constr.t option * Constr.t
-	let map = Named.Declaration.map
+
+        let map_constr f (ids, copt, ty as decl) =
+          let copt' = Option.map f copt in
+          let ty' = f ty in
+          if copt == copt' && ty == ty' then decl else (ids, copt', ty')
       end
+
     type t = Declaration.t list
+
     let fold f l ~init = List.fold_right f l init
   end