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, 15 insertions, 14 deletions

diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index e0bea7770..a03489c80 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -58,6 +58,7 @@ open Inductiveops
 open Ind_tables
 open Indrec
 open Sigma.Notations
+open Context.Rel.Declaration
 
 let hid = Id.of_string "H"
 let xid = Id.of_string "X"
@@ -104,7 +105,7 @@ let get_sym_eq_data env (ind,u) =
     error "Not an inductive type with a single constructor.";
   let arityctxt = Vars.subst_instance_context u mip.mind_arity_ctxt in
   let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in
-  if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then
+  if List.exists is_local_def realsign then
     error "Inductive equalities with local definitions in arity not supported.";
   let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
@@ -139,7 +140,7 @@ let get_non_sym_eq_data env (ind,u) =
     error "Not an inductive type with a single constructor.";
   let arityctxt = Vars.subst_instance_context u mip.mind_arity_ctxt in
   let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in
-  if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then
+  if List.exists is_local_def realsign then
     error "Inductive equalities with local definitions in arity not supported";
   let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
@@ -173,7 +174,7 @@ let build_sym_scheme env ind =
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let applied_ind = build_dependent_inductive indu specif in
   let realsign_ind =
-    name_context env ((Name varH,None,applied_ind)::realsign) in
+    name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in
   let ci = make_case_info (Global.env()) ind RegularStyle in
   let c = 
   (my_it_mkLambda_or_LetIn paramsctxt
@@ -232,7 +233,7 @@ let build_sym_involutive_scheme env ind =
          (Context.Rel.to_extended_vect (nrealargs+1) mib.mind_params_ctxt)
          (rel_vect (nrealargs+1) nrealargs)) in
   let realsign_ind =
-    name_context env ((Name varH,None,applied_ind)::realsign) in
+    name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in
   let ci = make_case_info (Global.env()) ind RegularStyle in
   let c = 
     (my_it_mkLambda_or_LetIn paramsctxt
@@ -352,9 +353,9 @@ let build_l2r_rew_scheme dep env ind kind =
         rel_vect 0 nrealargs]) in
   let realsign_P = lift_rel_context nrealargs realsign in
   let realsign_ind_P =
-    name_context env ((Name varH,None,applied_ind_P)::realsign_P) in
+    name_context env ((LocalAssum (Name varH,applied_ind_P))::realsign_P) in
   let realsign_ind_G =
-    name_context env ((Name varH,None,applied_ind_G)::
+    name_context env ((LocalAssum (Name varH,applied_ind_G))::
                       lift_rel_context (nrealargs+3) realsign) in
   let applied_sym_C n =
      mkApp(sym,
@@ -465,9 +466,9 @@ let build_l2r_forward_rew_scheme dep env ind kind =
         rel_vect (2*nrealargs+1) nrealargs]) in
   let realsign_P n = lift_rel_context (nrealargs*n+n) realsign in
   let realsign_ind =
-    name_context env ((Name varH,None,applied_ind)::realsign) in
+    name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in
   let realsign_ind_P n aP =
-    name_context env ((Name varH,None,aP)::realsign_P n) in
+    name_context env ((LocalAssum (Name varH,aP))::realsign_P n) in
   let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in
   let ctx = Univ.ContextSet.union ctx ctx' in
   let s = mkSort s in
@@ -545,7 +546,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
   let varP = fresh env (Id.of_string "P") in
   let applied_ind = build_dependent_inductive indu specif in
   let realsign_ind =
-    name_context env ((Name varH,None,applied_ind)::realsign) in
+    name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in
   let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in
   let ctx = Univ.ContextSet.union ctx ctx' in
   let s = mkSort s in
@@ -599,9 +600,9 @@ let fix_r2l_forward_rew_scheme (c, ctx') =
   | hp :: p :: ind :: indargs ->
      let c' = 
       my_it_mkLambda_or_LetIn indargs
-	(mkLambda_or_LetIn (Context.Rel.Declaration.map (liftn (-1) 1) p)
-	  (mkLambda_or_LetIn (Context.Rel.Declaration.map (liftn (-1) 2) hp)
-	    (mkLambda_or_LetIn (Context.Rel.Declaration.map (lift 2) ind)
+        (mkLambda_or_LetIn (map_constr (liftn (-1) 1) p)
+	  (mkLambda_or_LetIn (map_constr (liftn (-1) 2) hp)
+	    (mkLambda_or_LetIn (map_constr (lift 2) ind)
 	      (Reductionops.whd_beta Evd.empty
 		(applist (c,
 	          Context.Rel.to_extended_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))
@@ -737,10 +738,10 @@ let build_congr env (eq,refl,ctx) ind =
   let arityctxt = Vars.subst_instance_context u mip.mind_arity_ctxt in
   let paramsctxt = Vars.subst_instance_context u mib.mind_params_ctxt in
   let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in
-  if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then
+  if List.exists is_local_def realsign then
     error "Inductive equalities with local definitions in arity not supported.";
   let env_with_arity = push_rel_context arityctxt env in
-  let (_,_,ty) = lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity in
+  let ty = get_type (lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity) in
   let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
   if Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt) then