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, 11 insertions, 10 deletions

diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 6d09d5698..8ddfeaf2f 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -19,6 +19,7 @@ open Util
 open Nativecode
 open Nativevalues
 open Nativelambda
+open Context.Rel.Declaration
 
 (** This module implements normalization by evaluation to OCaml code *)
 
@@ -121,9 +122,8 @@ let build_case_type dep p realargs c =
   else mkApp(p, realargs)
 
 (* TODO move this function *)
-let type_of_rel env n = 
-  let (_,_,ty) = lookup_rel n env in
-  lift n ty
+let type_of_rel env n =
+  lookup_rel n env |> get_type |> lift n
 
 let type_of_prop = mkSort type1_sort
 
@@ -132,8 +132,9 @@ let type_of_sort s =
   | Prop _ -> type_of_prop
   | Type u -> mkType (Univ.super u)
 
-let type_of_var env id = 
-  try let (_,_,ty) = lookup_named id env in ty
+let type_of_var env id =
+  let open Context.Named.Declaration in
+  try lookup_named id env |> get_type
   with Not_found ->
     anomaly ~label:"type_of_var" (str "variable " ++ Id.print id ++ str " unbound")
 
@@ -181,7 +182,7 @@ let rec nf_val env v typ =
           Errors.anomaly
             (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
       in
-      let env = push_rel (name,None,dom) env in
+      let env = push_rel (LocalAssum (name,dom)) env in
       let body = nf_val env (f (mk_rel_accu lvl)) codom in
       mkLambda(name,dom,body)
   | Vconst n -> construct_of_constr_const env n typ
@@ -257,7 +258,7 @@ and nf_atom env atom =
   | Aprod(n,dom,codom) ->
       let dom = nf_type env dom in
       let vn = mk_rel_accu (nb_rel env) in
-      let env = push_rel (n,None,dom) env in
+      let env = push_rel (LocalAssum (n,dom)) env in
       let codom = nf_type env (codom vn) in
       mkProd(n,dom,codom)
   | Ameta (mv,_) -> mkMeta mv
@@ -328,7 +329,7 @@ and nf_atom_type env atom =
   | Aprod(n,dom,codom) ->
       let dom,s1 = nf_type_sort env dom in
       let vn = mk_rel_accu (nb_rel env) in
-      let env = push_rel (n,None,dom) env in
+      let env = push_rel (LocalAssum (n,dom)) env in
       let codom,s2 = nf_type_sort env (codom vn) in
       mkProd(n,dom,codom), mkSort (sort_of_product env s1 s2)
   | Aevar(ev,ty) ->
@@ -356,7 +357,7 @@ and  nf_predicate env ind mip params v pT =
 	    (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
       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
@@ -366,7 +367,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_type (push_rel (name,None,dom) env) vb in
+      let body = nf_type (push_rel (LocalAssum (name,dom)) env) vb in
       true, mkLambda(name,dom,body)
   | _, _ -> false, nf_type env v