CLEANUP: kernel/context.ml{,i}

The structure of the Context module was refined in such a way that:
- Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module.
- Types and functions related to rel-context were put into the Context.Rel module.
- Types and functions related to named-context declarations were put into the Context.Named.Declaration module.
- Types and functions related to named-context were put into the Context.Named module.
- Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module.
- Types and functions related to named-list-context were put into Context.NamedList module.

Some missing comments were added to the *.mli file.

The output of ocamldoc was checked whether it looks in a reasonable way.

"TODO: cleanup" was removed

The order in which are exported functions listed in the *.mli file was changed.
(as in a mature modules, this order usually is not random)

The order of exported functions in Context.{Rel,Named} modules is now consistent.
(as there is no special reason why that order should be different)

The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file.
(as there is no special reason to define them in a different order)

The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do.
(Now they are called Context.{Rel,Named}.fold_{inside,outside})

The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated.

Thrown exceptions are now documented.

Naming of formal parameters was made more consistent across different functions.

Comments of similar functions in different modules are now consistent.

Comments from *.mli files were copied to *.ml file.
(We need that information in *.mli files because that is were ocamldoc needs it.
 It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function,
 we can see the comments also there and do not need to open a different file if we want to see it.)

When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1.
(UTF-8 characters are used in our ocamldoc markup)

"open Context" was removed from all *.mli and *.ml files.
(Originally, it was OK to do that. Now it is not.)

An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed.

1 files changed, 35 insertions, 36 deletions

diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 64a68ba6b..2c713a021 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -49,7 +49,6 @@ open Util
 open Names
 open Term
 open Vars
-open Context
 open Declarations
 open Environ
 open Inductive
@@ -71,8 +70,8 @@ let build_dependent_inductive ind (mib,mip) =
   let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
   applist
     (mkIndU ind,
-       extended_rel_list mip.mind_nrealdecls mib.mind_params_ctxt
-       @ extended_rel_list 0 realargs)
+       Context.Rel.to_extended_list mip.mind_nrealdecls mib.mind_params_ctxt
+       @ Context.Rel.to_extended_list 0 realargs)
 
 let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn c s
 let my_it_mkProd_or_LetIn s c = it_mkProd_or_LetIn c s
@@ -109,7 +108,7 @@ let get_sym_eq_data env (ind,u) =
     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
-  if not (Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt)) then
+  if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then
     error "Constructor must have no arguments"; (* This can be relaxed... *)
   let params,constrargs = List.chop mib.mind_nparams constrargs in
   if mip.mind_nrealargs > mib.mind_nparams then
@@ -144,7 +143,7 @@ let get_non_sym_eq_data env (ind,u) =
     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
-  if not (Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt)) then
+  if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then
     error "Constructor must have no arguments";
   let _,constrargs = List.chop mib.mind_nparams constrargs in
   let constrargs = List.map (Vars.subst_instance_constr u) constrargs in
@@ -170,7 +169,7 @@ let build_sym_scheme env ind =
   let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
     get_sym_eq_data env indu in
   let cstr n =
-    mkApp (mkConstructUi(indu,1),extended_rel_vect n mib.mind_params_ctxt) in
+    mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect n mib.mind_params_ctxt) in
   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 =
@@ -183,7 +182,7 @@ let build_sym_scheme env ind =
      my_it_mkLambda_or_LetIn_name
        (lift_rel_context (nrealargs+1) realsign_ind)
        (mkApp (mkIndU indu,Array.concat
-	  [extended_rel_vect (3*nrealargs+2) paramsctxt1;
+	  [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1;
 	   rel_vect 1 nrealargs;
 	   rel_vect (2*nrealargs+2) nrealargs])),
      mkRel 1 (* varH *),
@@ -224,13 +223,13 @@ let build_sym_involutive_scheme env ind =
     get_sym_eq_data env indu in
   let eq,eqrefl,ctx = get_coq_eq ctx in
   let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in
-  let cstr n = mkApp (mkConstructUi (indu,1),extended_rel_vect n paramsctxt) in
+  let cstr n = mkApp (mkConstructUi (indu,1),Context.Rel.to_extended_vect n paramsctxt) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let applied_ind = build_dependent_inductive indu specif in
   let applied_ind_C =
     mkApp
       (mkIndU indu, Array.append
-         (extended_rel_vect (nrealargs+1) mib.mind_params_ctxt)
+         (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
@@ -244,15 +243,15 @@ let build_sym_involutive_scheme env ind =
 	       (mkApp (eq,[|
 	       mkApp
 	       (mkIndU indu, Array.concat
-	       [extended_rel_vect (3*nrealargs+2) paramsctxt1;
+	       [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1;
 		rel_vect (2*nrealargs+2) nrealargs;
 		rel_vect 1 nrealargs]);
                mkApp (sym,Array.concat
-	       [extended_rel_vect (3*nrealargs+2) paramsctxt1;
+	       [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1;
 		rel_vect 1 nrealargs;
 		rel_vect (2*nrealargs+2) nrealargs;
 		[|mkApp (sym,Array.concat
-		[extended_rel_vect (3*nrealargs+2) paramsctxt1;
+		[Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1;
 		 rel_vect (2*nrealargs+2) nrealargs;
 		 rel_vect 1 nrealargs;
 		 [|mkRel 1|]])|]]);
@@ -335,7 +334,7 @@ let build_l2r_rew_scheme dep env ind kind =
   let eq,eqrefl,ctx = get_coq_eq ctx in
   let cstr n p =
     mkApp (mkConstructUi(indu,1),
-      Array.concat [extended_rel_vect n paramsctxt1;
+      Array.concat [Context.Rel.to_extended_vect n paramsctxt1;
                     rel_vect p nrealargs]) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let varHC = fresh env (Id.of_string "HC") in
@@ -343,12 +342,12 @@ let build_l2r_rew_scheme dep env ind kind =
   let applied_ind = build_dependent_inductive indu specif in
   let applied_ind_P =
     mkApp (mkIndU indu, Array.concat
-       [extended_rel_vect (3*nrealargs) paramsctxt1;
+       [Context.Rel.to_extended_vect (3*nrealargs) paramsctxt1;
         rel_vect 0 nrealargs;
         rel_vect nrealargs nrealargs]) in
   let applied_ind_G =
     mkApp (mkIndU indu, Array.concat
-       [extended_rel_vect (3*nrealargs+3) paramsctxt1;
+       [Context.Rel.to_extended_vect (3*nrealargs+3) paramsctxt1;
         rel_vect (nrealargs+3) nrealargs;
         rel_vect 0 nrealargs]) in
   let realsign_P = lift_rel_context nrealargs realsign in
@@ -359,10 +358,10 @@ let build_l2r_rew_scheme dep env ind kind =
                       lift_rel_context (nrealargs+3) realsign) in
   let applied_sym_C n =
      mkApp(sym,
-       Array.append (extended_rel_vect n mip.mind_arity_ctxt) [|mkVar varH|]) in
+       Array.append (Context.Rel.to_extended_vect n mip.mind_arity_ctxt) [|mkVar varH|]) in
   let applied_sym_G =
      mkApp(sym,
-       Array.concat [extended_rel_vect (nrealargs*3+4) paramsctxt1;
+       Array.concat [Context.Rel.to_extended_vect (nrealargs*3+4) paramsctxt1;
                      rel_vect (nrealargs+4) nrealargs;
                      rel_vect 1 nrealargs;
 		     [|mkRel 1|]]) in
@@ -372,7 +371,7 @@ let build_l2r_rew_scheme dep env ind kind =
   let ci = make_case_info (Global.env()) ind RegularStyle in
   let cieq = make_case_info (Global.env()) (fst (destInd eq)) RegularStyle in
   let applied_PC =
-    mkApp (mkVar varP,Array.append (extended_rel_vect 1 realsign)
+    mkApp (mkVar varP,Array.append (Context.Rel.to_extended_vect 1 realsign)
            (if dep then [|cstr (2*nrealargs+1) 1|] else [||])) in
   let applied_PG =
     mkApp (mkVar varP,Array.append (rel_vect 1 nrealargs)
@@ -382,11 +381,11 @@ let build_l2r_rew_scheme dep env ind kind =
            (if dep then [|mkRel 2|] else [||])) in
   let applied_sym_sym =
          mkApp (sym,Array.concat
-	   [extended_rel_vect (2*nrealargs+4) paramsctxt1;
+	   [Context.Rel.to_extended_vect (2*nrealargs+4) paramsctxt1;
             rel_vect 4 nrealargs;
             rel_vect (nrealargs+4) nrealargs;
             [|mkApp (sym,Array.concat
-	      [extended_rel_vect (2*nrealargs+4) paramsctxt1;
+	      [Context.Rel.to_extended_vect (2*nrealargs+4) paramsctxt1;
 	       rel_vect (nrealargs+4) nrealargs;
 	       rel_vect 4 nrealargs;
 	       [|mkRel 2|]])|]]) in
@@ -409,7 +408,7 @@ let build_l2r_rew_scheme dep env ind kind =
                    mkApp (eq,[|lift 4 applied_ind;applied_sym_sym;mkRel 1|]),
                    applied_PR)),
        mkApp (sym_involutive,
-         Array.append (extended_rel_vect 3 mip.mind_arity_ctxt) [|mkVar varH|]),
+         Array.append (Context.Rel.to_extended_vect 3 mip.mind_arity_ctxt) [|mkVar varH|]),
        [|main_body|])
    else
      main_body))))))
@@ -448,7 +447,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
     get_sym_eq_data env indu in
   let cstr n p =
     mkApp (mkConstructUi(indu,1),
-      Array.concat [extended_rel_vect n paramsctxt1;
+      Array.concat [Context.Rel.to_extended_vect n paramsctxt1;
                     rel_vect p nrealargs]) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let varHC = fresh env (Id.of_string "HC") in
@@ -456,12 +455,12 @@ let build_l2r_forward_rew_scheme dep env ind kind =
   let applied_ind = build_dependent_inductive indu specif in
   let applied_ind_P =
     mkApp (mkIndU indu, Array.concat
-       [extended_rel_vect (4*nrealargs+2) paramsctxt1;
+       [Context.Rel.to_extended_vect (4*nrealargs+2) paramsctxt1;
         rel_vect 0 nrealargs;
         rel_vect (nrealargs+1) nrealargs]) in
   let applied_ind_P' =
     mkApp (mkIndU indu, Array.concat
-       [extended_rel_vect (3*nrealargs+1) paramsctxt1;
+       [Context.Rel.to_extended_vect (3*nrealargs+1) paramsctxt1;
         rel_vect 0 nrealargs;
         rel_vect (2*nrealargs+1) nrealargs]) in
   let realsign_P n = lift_rel_context (nrealargs*n+n) realsign in
@@ -539,7 +538,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
   let ((mib,mip as specif),constrargs,realsign,paramsctxt,nrealargs) =
     get_non_sym_eq_data env indu in
   let cstr n =
-    mkApp (mkConstructUi(indu,1),extended_rel_vect n mib.mind_params_ctxt) in
+    mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect n mib.mind_params_ctxt) in
   let constrargs_cstr = constrargs@[cstr 0] in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let varHC = fresh env (Id.of_string "HC") in
@@ -555,8 +554,8 @@ let build_r2l_forward_rew_scheme dep env ind kind =
     applist (mkVar varP,if dep then constrargs_cstr else constrargs) in
   let applied_PG =
     mkApp (mkVar varP,
-           if dep then extended_rel_vect 0 realsign_ind
-	   else extended_rel_vect 1 realsign) in
+           if dep then Context.Rel.to_extended_vect 0 realsign_ind
+	   else Context.Rel.to_extended_vect 1 realsign) in
   let c = 
   (my_it_mkLambda_or_LetIn paramsctxt
   (my_it_mkLambda_or_LetIn_name realsign_ind
@@ -600,12 +599,12 @@ let fix_r2l_forward_rew_scheme (c, ctx') =
   | hp :: p :: ind :: indargs ->
      let c' = 
       my_it_mkLambda_or_LetIn indargs
-	(mkLambda_or_LetIn (map_rel_declaration (liftn (-1) 1) p)
-	  (mkLambda_or_LetIn (map_rel_declaration (liftn (-1) 2) hp)
-	    (mkLambda_or_LetIn (map_rel_declaration (lift 2) ind)
+	(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)
 	      (Reductionops.whd_beta Evd.empty
 		(applist (c,
-	          extended_rel_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))
+	          Context.Rel.to_extended_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))
       in c', ctx'
   | _ -> anomaly (Pp.str "Ill-formed non-dependent left-to-right rewriting scheme")
 
@@ -744,7 +743,7 @@ let build_congr env (eq,refl,ctx) ind =
   let (_,_,ty) = 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 (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt) then
+  if Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt) then
     error "Constructor must have no arguments";
   let b = List.nth constrargs (i + mib.mind_nparams - 1) in
   let varB = fresh env (Id.of_string "B") in
@@ -760,8 +759,8 @@ let build_congr env (eq,refl,ctx) ind =
      (mkNamedLambda varH
         (applist
            (mkIndU indu,
-	    extended_rel_list (mip.mind_nrealargs+2) paramsctxt @
-	    extended_rel_list 0 realsign))
+	    Context.Rel.to_extended_list (mip.mind_nrealargs+2) paramsctxt @
+	    Context.Rel.to_extended_list 0 realsign))
      (mkCase (ci,
        my_it_mkLambda_or_LetIn_name
 	 (lift_rel_context (mip.mind_nrealargs+3) realsign)
@@ -769,9 +768,9 @@ let build_congr env (eq,refl,ctx) ind =
            (Anonymous,
             applist
              (mkIndU indu,
-	        extended_rel_list (2*mip.mind_nrealdecls+3)
+	        Context.Rel.to_extended_list (2*mip.mind_nrealdecls+3)
 		  paramsctxt
-	        @ extended_rel_list 0 realsign),
+	        @ Context.Rel.to_extended_list 0 realsign),
             mkApp (eq,
 	      [|mkVar varB;
                 mkApp (mkVar varf, [|lift (2*mip.mind_nrealdecls+4) b|]);