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, 19 insertions, 17 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 5e21154a67..d7637d1c27 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -15,6 +15,7 @@ open Termops
 open Univ
 open Evd
 open Environ
+open Context.Rel.Declaration
 
 exception Elimconst
 
@@ -607,7 +608,7 @@ let strong whdfun env sigma t =
   strongrec env t
 
 let local_strong whdfun sigma =
-  let rec strongrec t = map_constr strongrec (whdfun sigma t) in
+  let rec strongrec t = Constr.map strongrec (whdfun sigma t) in
   strongrec
 
 let rec strong_prodspine redfun sigma c =
@@ -799,6 +800,7 @@ let equal_stacks (x, l) (y, l') =
     | Some (lft1,lft2) -> f_equal (x, lft1) (y, lft2) 
 
 let rec whd_state_gen ?csts tactic_mode flags env sigma =
+  let open Context.Named.Declaration in
   let rec whrec cst_l (x, stack as s) =
     let () = if !debug_RAKAM then
 	let open Pp in
@@ -815,11 +817,11 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
     match kind_of_term x with
     | Rel n when Closure.RedFlags.red_set flags Closure.RedFlags.fDELTA ->
       (match lookup_rel n env with
-      | (_,Some body,_) -> whrec Cst_stack.empty (lift n body, stack)
+      | LocalDef (_,body,_) -> whrec Cst_stack.empty (lift n body, stack)
       | _ -> fold ())
     | Var id when Closure.RedFlags.red_set flags (Closure.RedFlags.fVAR id) ->
       (match lookup_named id env with
-      | (_,Some body,_) -> whrec (Cst_stack.add_cst (mkVar id) cst_l) (body, stack)
+      | LocalDef (_,body,_) -> whrec (Cst_stack.add_cst (mkVar id) cst_l) (body, stack)
       | _ -> fold ())
     | Evar ev ->
       (match safe_evar_value sigma ev with
@@ -922,7 +924,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
       | Some _ when Closure.RedFlags.red_set flags Closure.RedFlags.fBETA ->
 	apply_subst whrec [] cst_l x stack
       | None when Closure.RedFlags.red_set flags Closure.RedFlags.fETA ->
-	let env' = push_rel (na,None,t) env in
+	let env' = push_rel (LocalAssum (na,t)) env in
 	let whrec' = whd_state_gen tactic_mode flags env' sigma in
         (match kind_of_term (Stack.zip ~refold:true (fst (whrec' (c, Stack.empty)))) with
         | App (f,cl) ->
@@ -1442,7 +1444,7 @@ let splay_prod env sigma =
     let t = whd_betadeltaiota env sigma c in
     match kind_of_term t with
       | Prod (n,a,c0) ->
-	  decrec (push_rel (n,None,a) env)
+	  decrec (push_rel (LocalAssum (n,a)) env)
 	    ((n,a)::m) c0
       | _ -> m,t
   in
@@ -1453,7 +1455,7 @@ let splay_lam env sigma =
     let t = whd_betadeltaiota env sigma c in
     match kind_of_term t with
       | Lambda (n,a,c0) ->
-	  decrec (push_rel (n,None,a) env)
+	  decrec (push_rel (LocalAssum (n,a)) env)
 	    ((n,a)::m) c0
       | _ -> m,t
   in
@@ -1464,11 +1466,11 @@ let splay_prod_assum env sigma =
     let t = whd_betadeltaiota_nolet env sigma c in
     match kind_of_term t with
     | Prod (x,t,c)  ->
-	prodec_rec (push_rel (x,None,t) env)
-	  (Context.Rel.add (x, None, t) l) c
+	prodec_rec (push_rel (LocalAssum (x,t)) env)
+	  (Context.Rel.add (LocalAssum (x,t)) l) c
     | LetIn (x,b,t,c) ->
-	prodec_rec (push_rel (x, Some b, t) env)
-	  (Context.Rel.add (x, Some b, t) l) c
+	prodec_rec (push_rel (LocalDef (x,b,t)) env)
+	  (Context.Rel.add (LocalDef (x,b,t)) l) c
     | Cast (c,_,_)    -> prodec_rec env l c
     | _               -> 
       let t' = whd_betadeltaiota env sigma t in
@@ -1489,8 +1491,8 @@ let splay_prod_n env sigma n =
   let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else
     match kind_of_term (whd_betadeltaiota env sigma c) with
       | Prod (n,a,c0) ->
-	  decrec (push_rel (n,None,a) env)
-	    (m-1) (Context.Rel.add (n,None,a) ln) c0
+	  decrec (push_rel (LocalAssum (n,a)) env)
+	    (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0
       | _                      -> invalid_arg "splay_prod_n"
   in
   decrec env n Context.Rel.empty
@@ -1499,8 +1501,8 @@ let splay_lam_n env sigma n =
   let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else
     match kind_of_term (whd_betadeltaiota env sigma c) with
       | Lambda (n,a,c0) ->
-	  decrec (push_rel (n,None,a) env)
-	    (m-1) (Context.Rel.add (n,None,a) ln) c0
+	  decrec (push_rel (LocalAssum (n,a)) env)
+	    (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0
       | _                      -> invalid_arg "splay_lam_n"
   in
   decrec env n Context.Rel.empty
@@ -1538,8 +1540,8 @@ let find_conclusion env sigma =
   let rec decrec env c =
     let t = whd_betadeltaiota env sigma c in
     match kind_of_term t with
-      | Prod (x,t,c0) -> decrec (push_rel (x,None,t) env) c0
-      | Lambda (x,t,c0) -> decrec (push_rel (x,None,t) env) c0
+      | Prod (x,t,c0) -> decrec (push_rel (LocalAssum (x,t)) env) c0
+      | Lambda (x,t,c0) -> decrec (push_rel (LocalAssum (x,t)) env) c0
       | t -> t
   in
   decrec env
@@ -1623,7 +1625,7 @@ let meta_reducible_instance evd b =
 	  with
 	    | Some g -> irec (mkProj (p,g))
 	    | None -> mkProj (p,c))
-    | _ -> map_constr irec u
+    | _ -> Constr.map irec u
   in
   if Metaset.is_empty fm then (* nf_betaiota? *) b.rebus
   else irec b.rebus