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

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index cb4e588ee..1a6f7832a 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -18,6 +18,7 @@ open Reductionops
 open Environ
 open Termops
 open Arguments_renaming
+open Context.Rel.Declaration
 
 type retype_error =
   | NotASort
@@ -71,13 +72,14 @@ let rec subst_type env sigma typ = function
 let sort_of_atomic_type env sigma ft args =
   let rec concl_of_arity env n ar args =
     match kind_of_term (whd_betadeltaiota env sigma ar), args with
-    | Prod (na, t, b), h::l -> concl_of_arity (push_rel (na,Some (lift n h),t) env) (n + 1) b l
+    | Prod (na, t, b), h::l -> concl_of_arity (push_rel (LocalDef (na, lift n h, t)) env) (n + 1) b l
     | Sort s, [] -> s
     | _ -> retype_error NotASort
   in concl_of_arity env 0 ft (Array.to_list args)
 
 let type_of_var env id =
-  try let (_,_,ty) = lookup_named id env in ty
+  let open Context.Named.Declaration in
+  try get_type (lookup_named id env)
   with Not_found -> retype_error (BadVariable id)
 
 let decomp_sort env sigma t =
@@ -86,13 +88,13 @@ let decomp_sort env sigma t =
   | _ -> retype_error NotASort
 
 let retype ?(polyprop=true) sigma =
-  let rec type_of env cstr=
+  let rec type_of env cstr =
     match kind_of_term cstr with
     | Meta n ->
       (try strip_outer_cast (Evd.meta_ftype sigma n).Evd.rebus
        with Not_found -> retype_error (BadMeta n))
     | Rel n ->
-        let (_,_,ty) = lookup_rel n env in
+	let ty = get_type (lookup_rel n env) in
         lift n ty
     | Var id -> type_of_var env id
     | Const cst -> rename_type_of_constant env cst
@@ -115,9 +117,9 @@ let retype ?(polyprop=true) sigma =
           | Prod _ -> whd_beta sigma (applist (t, [c]))
           | _ -> t)
     | Lambda (name,c1,c2) ->
-          mkProd (name, c1, type_of (push_rel (name,None,c1) env) c2)
+          mkProd (name, c1, type_of (push_rel (LocalAssum (name,c1)) env) c2)
     | LetIn (name,b,c1,c2) ->
-         subst1 b (type_of (push_rel (name,Some b,c1) env) c2)
+         subst1 b (type_of (push_rel (LocalDef (name,b,c1)) env) c2)
     | Fix ((_,i),(_,tys,_)) -> tys.(i)
     | CoFix (i,(_,tys,_)) -> tys.(i)
     | App(f,args) when is_template_polymorphic env f ->
@@ -140,7 +142,7 @@ let retype ?(polyprop=true) sigma =
     | Sort (Prop c) -> type1_sort
     | Sort (Type u) -> Type (Univ.super u)
     | Prod (name,t,c2) ->
-        (match (sort_of env t, sort_of (push_rel (name,None,t) env) c2) with
+        (match (sort_of env t, sort_of (push_rel (LocalAssum (name,t)) env) c2) with
 	  | _, (Prop Null as s) -> s
           | Prop _, (Prop Pos as s) -> s
           | Type _, (Prop Pos as s) when is_impredicative_set env -> s
@@ -161,7 +163,7 @@ let retype ?(polyprop=true) sigma =
     | Sort (Prop c) -> InType
     | Sort (Type u) -> InType
     | Prod (name,t,c2) ->
-	let s2 = sort_family_of (push_rel (name,None,t) env) c2 in
+	let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in
 	if not (is_impredicative_set env) &&
 	   s2 == InSet && sort_family_of env t == InType then InType else s2
     | App(f,args) when is_template_polymorphic env f ->
@@ -235,9 +237,9 @@ let get_judgment_of env evc c = { uj_val = c; uj_type = get_type_of env evc c }
 let sorts_of_context env evc ctxt =
   let rec aux = function
   | [] -> env,[]
-  | (_,_,t as d)::ctxt ->
+  | d :: ctxt ->
       let env,sorts = aux ctxt in
-      let s = get_sort_of env evc t in
+      let s = get_sort_of env evc (get_type d) in
       (push_rel d env,s::sorts) in
   snd (aux ctxt)