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, 25 insertions, 23 deletions

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index fb45be663..713c99597 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -28,6 +28,7 @@ open Environ
 open Reductionops
 open Nametab
 open Sigma.Notations
+open Context.Rel.Declaration
 
 type dep_flag = bool
 
@@ -77,7 +78,6 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
   (* mais pas très joli ... (mais manque get_sort_of à ce niveau) *)
   let env' = push_rel_context lnamespar env in
 
-
   let rec add_branch env k =
     if Int.equal k (Array.length mip.mind_consnames) then
       let nbprod = k+1 in
@@ -85,7 +85,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
       let indf' = lift_inductive_family nbprod indf in
       let arsign,_ = get_arity env indf' in
       let depind = build_dependent_inductive env indf' in
-      let deparsign = (Anonymous,None,depind)::arsign in
+      let deparsign = LocalAssum (Anonymous,depind)::arsign in
 
       let ci = make_case_info env (fst pind) RegularStyle in
       let pbody =
@@ -118,14 +118,14 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
       let cs = lift_constructor (k+1) constrs.(k) in
       let t = build_branch_type env dep (mkRel (k+1)) cs in
       mkLambda_string "f" t
-	(add_branch (push_rel (Anonymous, None, t) env) (k+1))
+	(add_branch (push_rel (LocalAssum (Anonymous, t)) env) (k+1))
   in
   let Sigma (s, sigma, p) = Sigma.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env sigma kind in
   let typP = make_arity env' dep indf s in
   let c = 
     it_mkLambda_or_LetIn_name env
     (mkLambda_string "P" typP
-     (add_branch (push_rel (Anonymous,None,typP) env') 0)) lnamespar
+     (add_branch (push_rel (LocalAssum (Anonymous,typP)) env') 0)) lnamespar
   in
   Sigma (c, sigma, p)
 
@@ -154,10 +154,10 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
       let p',largs = whd_betadeltaiota_nolet_stack env sigma p in
       match kind_of_term p' with
 	| Prod (n,t,c) ->
-	    let d = (n,None,t) in
+	    let d = LocalAssum (n,t) in
 	    make_prod env (n,t,prec (push_rel d env) (i+1) (d::sign) c)
 	| LetIn (n,b,t,c) when List.is_empty largs ->
-	    let d = (n,Some b,t) in
+	    let d = LocalDef (n,b,t) in
 	    mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::sign) c)
      	| Ind (_,_) ->
 	    let realargs = List.skipn nparams largs in
@@ -192,22 +192,22 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
 	     | None ->
 		 make_prod env
 		   (n,t,
-		    process_constr (push_rel (n,None,t) env) (i+1) c_0 rest
+		    process_constr (push_rel (LocalAssum (n,t)) env) (i+1) c_0 rest
 		      (nhyps-1) (i::li))
              | Some(dep',p) ->
 		 let nP = lift (i+1+decP) p in
-                 let env' = push_rel (n,None,t) env in
+                 let env' = push_rel (LocalAssum (n,t)) env in
 		 let t_0 = process_pos env' dep' nP (lift 1 t) in
 		 make_prod_dep (dep || dep') env
                    (n,t,
 		    mkArrow t_0
 		      (process_constr
-			(push_rel (Anonymous,None,t_0) env')
+			(push_rel (LocalAssum (Anonymous,t_0)) env')
 			 (i+2) (lift 1 c_0) rest (nhyps-1) (i::li))))
       | LetIn (n,b,t,c_0) ->
 	  mkLetIn (n,b,t,
 		   process_constr
-		     (push_rel (n,Some b,t) env)
+		     (push_rel (LocalDef (n,b,t)) env)
 		     (i+1) c_0 recargs (nhyps-1) li)
       | _ -> assert false
     else
@@ -232,10 +232,10 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
       let p',largs = whd_betadeltaiota_nolet_stack env sigma p in
       match kind_of_term p' with
 	| Prod (n,t,c) ->
-	    let d = (n,None,t) in
+	    let d = LocalAssum (n,t) in
 	    mkLambda_name env (n,t,prec (push_rel d env) (i+1) (d::hyps) c)
 	| LetIn (n,b,t,c) when List.is_empty largs ->
-	    let d = (n,Some b,t) in
+	    let d = LocalDef (n,b,t) in
 	    mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c)
      	| Ind _ ->
             let realargs = List.skipn nparrec largs
@@ -250,7 +250,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
   in
   (* ici, cstrprods est la liste des produits du constructeur instantié *)
   let rec process_constr env i f = function
-    | (n,None,t as d)::cprest, recarg::rest ->
+    | (LocalAssum (n,t) as d)::cprest, recarg::rest ->
         let optionpos =
 	  match dest_recarg recarg with
             | Norec   -> None
@@ -271,7 +271,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
 		 (n,t,process_constr env' (i+1)
 		    (whd_beta Evd.empty (applist (lift 1 f, [(mkRel 1); arg])))
 		    (cprest,rest)))
-    | (n,Some c,t as d)::cprest, rest ->
+    | (LocalDef (n,c,t) as d)::cprest, rest ->
 	mkLetIn
 	  (n,c,t,
 	   process_constr (push_rel d env) (i+1) (lift 1 f)
@@ -322,7 +322,7 @@ let mis_make_indrec env sigma listdepkind mib u =
 
 	    let arsign,_ = get_arity env indf in
 	    let depind = build_dependent_inductive env indf in
-	    let deparsign = (Anonymous,None,depind)::arsign in
+	    let deparsign = LocalAssum (Anonymous,depind)::arsign in
 
 	    let nonrecpar = Context.Rel.length lnonparrec in
 	    let larsign = Context.Rel.length deparsign in
@@ -357,7 +357,7 @@ let mis_make_indrec env sigma listdepkind mib u =
 
 	    let depind' = build_dependent_inductive env indf' in
 	    let arsign',_ = get_arity env indf' in
-	    let deparsign' = (Anonymous,None,depind')::arsign' in
+	    let deparsign' = LocalAssum (Anonymous,depind')::arsign' in
 
 	    let pargs =
 	      let nrpar = Context.Rel.to_extended_list (2*ndepar) lnonparrec
@@ -387,11 +387,13 @@ let mis_make_indrec env sigma listdepkind mib u =
 		    let branch = branches.(0) in
 		    let ctx, br = decompose_lam_assum branch in
 		    let n, subst = 
-		      List.fold_right (fun (na,b,t) (i, subst) ->
-			if b == None then 
-			  let t = mkProj (Projection.make ps.(i) true, mkRel 1) in
-			    (i + 1, t :: subst)
-			else (i, mkRel 0 :: subst))
+		      List.fold_right (fun decl (i, subst) ->
+			match decl with
+			| LocalAssum (na,t) ->
+			    let t = mkProj (Projection.make ps.(i) true, mkRel 1) in
+			    i + 1, t :: subst
+			| LocalDef (na,b,t) ->
+			    i, mkRel 0 :: subst)
 			ctx (0, [])
 		    in
 		    let term = substl subst br in
@@ -440,7 +442,7 @@ let mis_make_indrec env sigma listdepkind mib u =
                   true dep env !evdref (vargs,depPvec,i+j) tyi cs recarg
 	      in
 		mkLambda_string "f" p_0
-		  (onerec (push_rel (Anonymous,None,p_0) env) (j+1))
+		  (onerec (push_rel (LocalAssum (Anonymous,p_0)) env) (j+1))
 	  in onerec env 0
       | [] ->
 	  makefix i listdepkind
@@ -454,7 +456,7 @@ let mis_make_indrec env sigma listdepkind mib u =
 	  in
 	  let typP = make_arity env dep indf s in
 	    mkLambda_string "P" typP
-	      (put_arity (push_rel (Anonymous,None,typP) env) (i+1) rest)
+	      (put_arity (push_rel (LocalAssum (Anonymous,typP)) env) (i+1) rest)
       | [] ->
 	  make_branch env 0 listdepkind
     in