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, 26 insertions, 24 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index dd49c4a1b..ca29d83f6 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -17,6 +17,7 @@ open Declareops
 open Environ
 open Reduction
 open Type_errors
+open Context.Rel.Declaration
 
 type mind_specif = mutual_inductive_body * one_inductive_body
 
@@ -77,10 +78,10 @@ let instantiate_params full t u args sign =
     anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in
   let (rem_args, subs, ty) =
     Context.Rel.fold_outside
-      (fun (_,copt,_) (largs,subs,ty) ->
-        match (copt, largs, kind_of_term ty) with
-          | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t)
-          | (Some b,_,LetIn(_,_,_,t))    ->
+      (fun decl (largs,subs,ty) ->
+        match (decl, largs, kind_of_term ty) with
+          | (LocalAssum _, a::args, Prod(_,_,t)) -> (args, a::subs, t)
+          | (LocalDef (_,b,_), _, LetIn(_,_,_,t))    ->
 	     (largs, (substl subs (subst_instance_constr u b))::subs, t)
 	  | (_,[],_)                -> if full then fail() else ([], subs, ty)
 	  | _                       -> fail ())
@@ -152,7 +153,7 @@ let remember_subst u subst =
 (* Propagate the new levels in the signature *)
 let make_subst env =
   let rec make subst = function
-    | (_,Some _,_)::sign, exp, args ->
+    | LocalDef _ :: sign, exp, args ->
         make subst (sign, exp, args)
     | d::sign, None::exp, args ->
         let args = match args with _::args -> args | [] -> [] in
@@ -165,7 +166,7 @@ let make_subst env =
         (* a useless extra constraint *)
         let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in
           make (cons_subst u s subst) (sign, exp, args)
-    | (na,None,t)::sign, Some u::exp, [] ->
+    | LocalAssum (na,t) :: sign, Some u::exp, [] ->
         (* No more argument here: we add the remaining universes to the *)
         (* substitution (when [u] is distinct from all other universes in the *)
         (* template, it is identity substitution  otherwise (ie. when u is *)
@@ -314,14 +315,14 @@ let is_correct_arity env c pj ind specif params =
   let rec srec env pt ar =
     let pt' = whd_betadeltaiota env pt in
     match kind_of_term pt', ar with
-      | Prod (na1,a1,t), (_,None,a1')::ar' ->
+      | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
           let () =
             try conv env a1 a1'
             with NotConvertible -> raise (LocalArity None) in
-          srec (push_rel (na1,None,a1) env) t ar' 
+          srec (push_rel (LocalAssum (na1,a1)) env) t ar' 
       (* The last Prod domain is the type of the scrutinee *)
       | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *)
-	 let env' = push_rel (na1,None,a1) env in
+	 let env' = push_rel (LocalAssum (na1,a1)) env in
 	 let ksort = match kind_of_term (whd_betadeltaiota env' a2) with
 	 | Sort s -> family_of_sort s
 	 | _ -> raise (LocalArity None) in
@@ -330,7 +331,7 @@ let is_correct_arity env c pj ind specif params =
            try conv env a1 dep_ind
            with NotConvertible -> raise (LocalArity None) in
 	   check_allowed_sort ksort specif
-      | _, (_,Some _,_ as d)::ar' ->
+      | _, (LocalDef _ as d)::ar' ->
 	  srec (push_rel d env) (lift 1 pt') ar'
       | _ ->
 	  raise (LocalArity None)
@@ -482,7 +483,7 @@ let make_renv env recarg tree =
     genv = [Lazy.lazy_from_val(Subterm(Large,tree))] }
 
 let push_var renv (x,ty,spec) =
-  { env = push_rel (x,None,ty) renv.env;
+  { env = push_rel (LocalAssum (x,ty)) renv.env;
     rel_min = renv.rel_min+1;
     genv = spec:: renv.genv }
 
@@ -568,14 +569,14 @@ let check_inductive_codomain env p =
 (* The following functions are almost duplicated from indtypes.ml, except
 that they carry here a poorer environment (containing less information). *)
 let ienv_push_var (env, lra) (x,a,ra) =
-  (push_rel (x,None,a) env, (Norec,ra)::lra)
+  (push_rel (LocalAssum (x,a)) env, (Norec,ra)::lra)
 
 let ienv_push_inductive (env, ra_env) ((mind,u),lpar) =
   let mib = Environ.lookup_mind mind env in
   let ntypes = mib.mind_ntypes in
   let push_ind specif env =
-     push_rel (Anonymous,None,
-		hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) env
+    let decl = LocalAssum (Anonymous, hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) in
+    push_rel decl env
   in
   let env = Array.fold_right push_ind mib.mind_packets env in
   let rc = Array.mapi (fun j t -> (Imbr (mind,j),t)) (Rtree.mk_rec_calls ntypes) in
@@ -848,7 +849,7 @@ let filter_stack_domain env ci p stack =
     let t = whd_betadeltaiota env ar in
     match stack, kind_of_term t with
     | elt :: stack', Prod (n,a,c0) ->
-      let d = (n,None,a) in
+      let d = LocalAssum (n,a) in
       let ty, args = decompose_app (whd_betadeltaiota env a) in
       let elt = match kind_of_term ty with
       | Ind ind -> 
@@ -905,10 +906,10 @@ let check_one_fix renv recpos trees def =
               end
             else
               begin
-                match pi2 (lookup_rel p renv.env) with
-                | None ->
+                match lookup_rel p renv.env with
+                | LocalAssum _ ->
                     List.iter (check_rec_call renv []) l
-                | Some c ->
+                | LocalDef (_,c,_) ->
                     try List.iter (check_rec_call renv []) l
                     with FixGuardError _ ->
                       check_rec_call renv stack (applist(lift p c,l))
@@ -983,10 +984,11 @@ let check_one_fix renv recpos trees def =
 
         | Var id ->
             begin
-              match pi2 (lookup_named id renv.env) with
-              | None ->
+              let open Context.Named.Declaration in
+              match lookup_named id renv.env with
+              | LocalAssum _ ->
                   List.iter (check_rec_call renv []) l
-              | Some c ->
+              | LocalDef (_,c,_) ->
                   try List.iter (check_rec_call renv []) l
                   with (FixGuardError _) -> 
 		    check_rec_call renv stack (applist(c,l))
@@ -1040,7 +1042,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
       match kind_of_term (whd_betadeltaiota env def) with
         | Lambda (x,a,b) ->
 	    if noccur_with_meta n nbfix a then
-	      let env' = push_rel (x, None, a) env in
+	      let env' = push_rel (LocalAssum (x,a)) env in
               if Int.equal n (k + 1) then
                 (* get the inductive type of the fixpoint *)
                 let (mind, _) =
@@ -1090,7 +1092,7 @@ let rec codomain_is_coind env c =
   let b = whd_betadeltaiota env c in
   match kind_of_term b with
     | Prod (x,a,b) ->
-	codomain_is_coind (push_rel (x, None, a) env) b
+	codomain_is_coind (push_rel (LocalAssum (x,a)) env) b
     | _ ->
 	(try find_coinductive env b
         with Not_found ->
@@ -1131,7 +1133,7 @@ let check_one_cofix env nbfix def deftype =
 	| Lambda (x,a,b) ->
 	    let () = assert (List.is_empty args) in
             if noccur_with_meta n nbfix a then
-              let env' = push_rel (x, None, a) env in
+              let env' = push_rel (LocalAssum (x,a)) env in
               check_rec_call env' alreadygrd (n+1) tree vlra b
             else
 	      raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a))