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

diff --git a/checker/typeops.ml b/checker/typeops.ml
index d49c40a8b..64afd21b2 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -62,7 +62,7 @@ let judge_of_type u = Sort (Type (Univ.super u))
 
 let judge_of_relative env n =
   try
-    let (_,_,typ) = lookup_rel n env in
+    let LocalAssum (_,typ) | LocalDef (_,_,typ) = lookup_rel n env in
     lift n typ
   with Not_found ->
     error_unbound_rel env n
@@ -296,13 +296,13 @@ let rec execute env cstr =
 
     | Lambda (name,c1,c2) ->
         let _ = execute_type env c1 in
-	let env1 = push_rel (name,None,c1) env in
+	let env1 = push_rel (LocalAssum (name,c1)) env in
         let j' = execute env1 c2 in
         Prod(name,c1,j')
 
     | Prod (name,c1,c2) ->
         let varj = execute_type env c1 in
-	let env1 = push_rel (name,None,c1) env in
+	let env1 = push_rel (LocalAssum (name,c1)) env in
         let varj' = execute_type env1 c2 in
 	Sort (sort_of_product env varj varj')
 
@@ -314,7 +314,7 @@ let rec execute env cstr =
           let env',c2' = (* refresh_arity env *) env, c2 in
           let _ = execute_type env' c2' in
           judge_of_cast env' (c1,j1) DEFAULTcast c2' in
-        let env1 = push_rel (name,Some c1,c2) env in
+        let env1 = push_rel (LocalDef (name,c1,c2)) env in
         let j' = execute env1 c3 in
         subst1 c1 j'
 
@@ -378,10 +378,10 @@ let infer_type env constr = execute_type env constr
 let check_ctxt env rels =
   fold_rel_context (fun d env ->
     match d with
-        (_,None,ty) ->
+      | LocalAssum (_,ty) ->
           let _ = infer_type env ty in
           push_rel d env
-      | (_,Some bd,ty) ->
+      | LocalDef (_,bd,ty) ->
           let j1 = infer env bd in
           let _ = infer env ty in
           conv_leq env j1 ty;
@@ -399,9 +399,9 @@ let check_polymorphic_arity env params par =
   let pl = par.template_param_levels in
   let rec check_p env pl params =
     match pl, params with
-        Some u::pl, (na,None,ty)::params ->
+        Some u::pl, LocalAssum (na,ty)::params ->
           check_kind env ty u;
-          check_p (push_rel (na,None,ty) env) pl params
+          check_p (push_rel (LocalAssum (na,ty)) env) pl params
       | None::pl,d::params -> check_p (push_rel d env) pl params
       | [], _ -> ()
       | _ -> failwith "check_poly: not the right number of params" in