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, 8 insertions, 6 deletions

diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 8b9c2d6c9..7ea9b9063 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -15,6 +15,7 @@ open Environ
 open Inductive
 open Reduction
 open Vm
+open Context.Rel.Declaration
 
 (*******************************************)
 (* Calcul de la forme normal d'un terme    *)
@@ -134,7 +135,7 @@ and nf_whd env whd typ =
       let dom = nf_vtype env (dom p) in
       let name = Name (Id.of_string "x") in
       let vc = body_of_vfun (nb_rel env) (codom p) in
-      let codom = nf_vtype (push_rel (name,None,dom) env) vc  in
+      let codom = nf_vtype (push_rel (LocalAssum (name,dom)) env) vc  in
       mkProd(name,dom,codom)
   | Vfun f -> nf_fun env f typ
   | Vfix(f,None) -> nf_fix env f
@@ -202,11 +203,12 @@ and constr_type_of_idkey env (idkey : Vars.id_key) stk =
      in
      nf_univ_args ~nb_univs mk env stk
    | VarKey id ->
-      let (_,_,ty) = lookup_named id env in
+      let open Context.Named.Declaration in
+      let ty = get_type (lookup_named id env) in
       nf_stk env (mkVar id) ty stk
   | RelKey i ->
       let n = (nb_rel env - i) in
-      let (_,_,ty) = lookup_rel n env in
+      let ty = get_type (lookup_rel n env) in
       nf_stk env (mkRel n) (lift n ty) stk
 
 and nf_stk ?from:(from=0) env c t stk  =
@@ -260,7 +262,7 @@ and nf_predicate env ind mip params v pT =
       let vb = body_of_vfun k f in
       let name,dom,codom = decompose_prod env pT in
       let dep,body =
-	nf_predicate (push_rel (name,None,dom) env) ind mip params vb codom in
+	nf_predicate (push_rel (LocalAssum (name,dom)) env) ind mip params vb codom in
       dep, mkLambda(name,dom,body)
   | Vfun f, _ ->
       let k = nb_rel env in
@@ -270,7 +272,7 @@ and nf_predicate env ind mip params v pT =
       let rargs = Array.init n (fun i -> mkRel (n-i)) in
       let params = if Int.equal n 0 then params else Array.map (lift n) params in
       let dom = mkApp(mkIndU ind,Array.append params rargs) in
-      let body = nf_vtype (push_rel (name,None,dom) env) vb in
+      let body = nf_vtype (push_rel (LocalAssum (name,dom)) env) vb in
       true, mkLambda(name,dom,body)
   | _, _ -> false, nf_val env v crazy_type
 
@@ -306,7 +308,7 @@ and nf_fun env f typ =
       Errors.anomaly
         (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
   in
-  let body = nf_val (push_rel (name,None,dom) env) vb codom in
+  let body = nf_val (push_rel (LocalAssum (name,dom)) env) vb codom in
   mkLambda(name,dom,body)
 
 and nf_fix env f =