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, 15 insertions, 12 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 8f8b29d106..f1f65bd8af 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -16,6 +16,7 @@ open Vars
 open Termops
 open Environ
 open Globnames
+open Context.Named.Declaration
 
 (** Generic filters *)
 module Filter :
@@ -230,20 +231,20 @@ let evar_instance_array test_id info args =
     else instance_mismatch ()
   | false :: filter, _ :: ctxt ->
     instrec filter ctxt i
-  | true :: filter, (id,_,_ as d) :: ctxt ->
+  | true :: filter, d :: ctxt ->
     if i < len then
       let c = Array.unsafe_get args i in
       if test_id d c then instrec filter ctxt (succ i)
-      else (id, c) :: instrec filter ctxt (succ i)
+      else (get_id d, c) :: instrec filter ctxt (succ i)
     else instance_mismatch ()
   | _ -> instance_mismatch ()
   in
   match Filter.repr (evar_filter info) with
   | None ->
-    let map i (id,_,_ as d) =
+     let map i d =
       if (i < len) then
         let c = Array.unsafe_get args i in
-        if test_id d c then None else Some (id,c)
+        if test_id d c then None else Some (get_id d, c)
       else instance_mismatch ()
     in
     List.map_filter_i map (evar_context info)
@@ -251,7 +252,7 @@ let evar_instance_array test_id info args =
     instrec filter (evar_context info) 0
 
 let make_evar_instance_array info args =
-  evar_instance_array (fun (id,_,_) -> isVarId id) info args
+  evar_instance_array (isVarId % get_id) info args
 
 let instantiate_evar_array info c args =
   let inst = make_evar_instance_array info args in
@@ -660,7 +661,7 @@ let restrict evk filter ?candidates evd =
       evar_extra = Store.empty } in
   let evar_names = reassign_name_defined evk evk' evd.evar_names in
   let ctxt = Filter.filter_list filter (evar_context evar_info) in
-  let id_inst = Array.map_of_list (fun (id,_,_) -> mkVar id) ctxt in
+  let id_inst = Array.map_of_list (mkVar % get_id) ctxt in
   let body = mkEvar(evk',id_inst) in
   let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
   { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
@@ -722,10 +723,10 @@ let evars_of_term c =
   evrec Evar.Set.empty c
 
 let evars_of_named_context nc =
-  List.fold_right (fun (_, b, t) s ->
+  List.fold_right (fun decl s ->
     Option.fold_left (fun s t ->
       Evar.Set.union s (evars_of_term t))
-      (Evar.Set.union s (evars_of_term t)) b)
+      (Evar.Set.union s (evars_of_term (get_type decl))) (get_value decl))
     nc Evar.Set.empty
 
 let evars_of_filtered_evar_info evi =
@@ -1228,8 +1229,9 @@ let pr_meta_map mmap =
   in
   prlist pr_meta_binding (metamap_to_list mmap)
 
-let pr_decl ((id,b,_),ok) =
-  match b with
+let pr_decl (decl,ok) =
+  let id = get_id decl in
+  match get_value decl with
   | None -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}")
   | Some c -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++
       print_constr c ++ str (if ok then ")" else "}")
@@ -1346,8 +1348,9 @@ let print_env_short env =
   let pr_body n = function
   | None -> pr_name n
   | Some b -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" in
-  let pr_named_decl (n, b, _) = pr_body (Name n) b in
-  let pr_rel_decl (n, b, _) = pr_body n b in
+  let pr_named_decl decl = pr_body (Name (get_id decl)) (get_value decl) in
+  let pr_rel_decl decl = let open Context.Rel.Declaration in
+                         pr_body (get_name decl) (get_value decl) in
   let nc = List.rev (named_context env) in
   let rc = List.rev (rel_context env) in
     str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++