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, 18 insertions, 19 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 3d6196c352..6c62bd08fc 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -16,6 +16,7 @@ open Evd
 open Util
 open Typeclasses_errors
 open Libobject
+open Context.Rel.Declaration
 (*i*)
 
 let typeclasses_unique_solutions = ref false
@@ -180,9 +181,7 @@ let subst_class (subst,cl) =
   let do_subst_con c = Mod_subst.subst_constant subst c
   and do_subst c = Mod_subst.subst_mps subst c
   and do_subst_gr gr = fst (subst_global subst gr) in
-  let do_subst_ctx ctx = List.smartmap
-    (fun (na, b, t) -> (na, Option.smartmap do_subst b, do_subst t))
-    ctx in
+  let do_subst_ctx = List.smartmap (map_constr do_subst) in
   let do_subst_context (grs,ctx) =
     List.smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs,
     do_subst_ctx ctx in
@@ -199,15 +198,19 @@ let discharge_class (_,cl) =
   let repl = Lib.replacement_context () in
   let rel_of_variable_context ctx = List.fold_right
     ( fun (n,_,b,t) (ctx', subst) ->
-	let decl = (Name n, Option.map (substn_vars 1 subst) b, substn_vars 1 subst t) in
+        let decl = match b with
+                   | None -> LocalAssum (Name n, substn_vars 1 subst t)
+		   | Some b -> LocalDef (Name n, substn_vars 1 subst b, substn_vars 1 subst t)
+	in
 	(decl :: ctx', n :: subst)
     ) ctx ([], []) in
   let discharge_rel_context subst n rel =
     let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in
     let ctx, _ =
       List.fold_right
-	(fun (id, b, t) (ctx, k) ->
-	   (id, Option.smartmap (substn_vars k subst) b, substn_vars k subst t) :: ctx, succ k)
+	(fun decl (ctx, k) ->
+	   map_constr (substn_vars k subst) decl :: ctx, succ k
+	)
 	rel ([], n)
     in ctx
   in
@@ -217,15 +220,15 @@ let discharge_class (_,cl) =
       | ConstRef cst -> Lib.section_segment_of_constant cst
       | IndRef (ind,_) -> Lib.section_segment_of_mutual_inductive ind in
   let discharge_context ctx' subst (grs, ctx) =
-    let grs' = 
-      let newgrs = List.map (fun (_, _, t) -> 
-	match class_of_constr t with
-	| None -> None
-	| Some (_, ((tc,_), _)) -> Some (tc.cl_impl, true))
-	ctx' 
+    let grs' =
+      let newgrs = List.map (fun decl ->
+			     match decl |> get_type |> class_of_constr with
+			     | None -> None
+			     | Some (_, ((tc,_), _)) -> Some (tc.cl_impl, true))
+			    ctx'
       in
-	List.smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs
-	  @ newgrs
+      List.smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs
+      @ newgrs
     in grs', discharge_rel_context subst 1 ctx @ ctx' in
   let cl_impl' = Lib.discharge_global cl.cl_impl in
   if cl_impl' == cl.cl_impl then cl else
@@ -431,11 +434,7 @@ let add_class cl =
  *)
 
 let instance_constructor (cl,u) args =
-  let filter (_, b, _) = match b with
-  | None -> true
-  | Some _ -> false
-  in
-  let lenpars = List.count filter (snd cl.cl_context) in
+  let lenpars = List.count is_local_assum (snd cl.cl_context) in
   let pars = fst (List.chop lenpars args) in
     match cl.cl_impl with
       | IndRef ind ->