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, 30 insertions, 34 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 847e1d08f..1089dff92 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -72,9 +72,8 @@ let lookup_rel n env =
   Context.Rel.lookup n env.env_rel_context
 
 let evaluable_rel n env =
-  match lookup_rel n env with
-  | (_,Some _,_) -> true
-  | _ -> false
+  let open Context.Rel.Declaration in
+  lookup_rel n env |> is_local_def
 
 let nb_rel env = env.env_nb_rel
 
@@ -83,7 +82,8 @@ let push_rel = push_rel
 let push_rel_context ctxt x = Context.Rel.fold_outside push_rel ctxt ~init:x
 
 let push_rec_types (lna,typarray,_) env =
-  let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
+  let open Context.Rel.Declaration in
+  let ctxt = Array.map2_i (fun i na t -> LocalAssum (na, lift i t)) lna typarray in
   Array.fold_left (fun e assum -> push_rel assum e) env ctxt
 
 let fold_rel_context f env ~init =
@@ -107,17 +107,8 @@ let named_vals_of_val = snd
 (* [map_named_val f ctxt] apply [f] to the body and the type of
    each declarations.
    *** /!\ ***   [f t] should be convertible with t *)
-let map_named_val f (ctxt,ctxtv) =
-  let rec map ctx = match ctx with
-  | [] -> []
-  | (id, body, typ) :: rem ->
-    let body' = Option.smartmap f body in
-    let typ' = f typ in
-    let rem' = map rem in
-    if body' == body && typ' == typ && rem' == rem then ctx
-    else (id, body', typ') :: rem'
-  in
-  (map ctxt, ctxtv)
+let map_named_val f =
+  on_fst (Context.Named.map f)
 
 let empty_named_context = Context.Named.empty
 
@@ -138,10 +129,10 @@ let eq_named_context_val c1 c2 =
 (* A local const is evaluable if it is defined  *)
 
 let named_type id env =
-  let (_,_,t) = lookup_named id env in t
+  lookup_named id env |> Context.Named.Declaration.get_type
 
 let named_body id env =
-  let (_,b,_) = lookup_named id env in b
+  lookup_named id env |> Context.Named.Declaration.get_value
 
 let evaluable_named id env =
   match named_body id env with
@@ -426,15 +417,16 @@ let global_vars_set env constr =
    contained in the types of the needed variables. *)
 
 let really_needed env needed =
+  let open Context.Named.Declaration in
   Context.Named.fold_inside
-    (fun need (id,copt,t) ->
-      if Id.Set.mem id need then
+    (fun need decl ->
+      if Id.Set.mem (get_id decl) need then
         let globc =
-          match copt with
-            | None -> Id.Set.empty
-            | Some c -> global_vars_set env c in
+          match decl with
+            | LocalAssum _ -> Id.Set.empty
+            | LocalDef (_,c,_) -> global_vars_set env c in
         Id.Set.union
-          (global_vars_set env t)
+          (global_vars_set env (get_type decl))
           (Id.Set.union globc need)
       else need)
     ~init:needed
@@ -443,8 +435,9 @@ let really_needed env needed =
 let keep_hyps env needed =
   let really_needed = really_needed env needed in
   Context.Named.fold_outside
-    (fun (id,_,_ as d) nsign ->
-      if Id.Set.mem id really_needed then Context.Named.add d nsign
+    (fun d nsign ->
+      let open Context.Named.Declaration in
+      if Id.Set.mem (get_id d) really_needed then Context.Named.add d nsign
       else nsign)
     (named_context env)
     ~init:empty_named_context
@@ -494,11 +487,12 @@ let compile_constant_body = Cbytegen.compile_constant_body false
 exception Hyp_not_found
 
 let apply_to_hyp (ctxt,vals) id f =
+  let open Context.Named.Declaration in
   let rec aux rtail ctxt vals =
     match ctxt, vals with
-    | (idc,c,ct as d)::ctxt, v::vals ->
-	if Id.equal idc id then
-	  (f ctxt d rtail)::ctxt, v::vals
+    | d::ctxt, v::vals ->
+	if Id.equal (get_id d) id then
+          (f ctxt d rtail)::ctxt, v::vals
 	else
 	  let ctxt',vals' = aux (d::rtail) ctxt vals in
 	  d::ctxt', v::vals'
@@ -507,10 +501,11 @@ let apply_to_hyp (ctxt,vals) id f =
   in aux [] ctxt vals
 
 let apply_to_hyp_and_dependent_on (ctxt,vals) id f g =
+  let open Context.Named.Declaration in
   let rec aux ctxt vals =
     match ctxt,vals with
-    | (idc,c,ct as d)::ctxt, v::vals ->
-	if Id.equal idc id then
+    | d::ctxt, v::vals ->
+	if Id.equal (get_id d) id then
 	  let sign = ctxt,vals in
 	  push_named_context_val (f d sign) sign
 	else
@@ -521,10 +516,11 @@ let apply_to_hyp_and_dependent_on (ctxt,vals) id f g =
   in aux ctxt vals
 
 let insert_after_hyp (ctxt,vals) id d check =
+  let open Context.Named.Declaration in
   let rec aux ctxt vals =
     match  ctxt, vals with
-    | (idc,c,ct)::ctxt', v::vals' ->
-	if Id.equal idc id then begin
+    | decl::ctxt', v::vals' ->
+	if Id.equal (get_id decl) id then begin
 	  check ctxt;
 	  push_named_context_val d (ctxt,vals)
 	end else
@@ -537,12 +533,12 @@ let insert_after_hyp (ctxt,vals) id d check =
 
 (* To be used in Logic.clear_hyps *)
 let remove_hyps ids check_context check_value (ctxt, vals) =
+  let open Context.Named.Declaration in
   let rec remove_hyps ctxt vals = match ctxt, vals with
   | [], [] -> [], []
   | d :: rctxt, (nid, v) :: rvals ->
-    let (id, _, _) = d in
     let ans = remove_hyps rctxt rvals in
-    if Id.Set.mem id ids then ans
+    if Id.Set.mem (get_id d) ids then ans
     else
       let (rctxt', rvals') = ans in
       let d' = check_context d in