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.

7 files changed, 70 insertions, 46 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index 1dd5be0e7..84ffee23c 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -9,6 +9,7 @@
 open Util
 open Pp
 open Term
+open Context.Named.Declaration
 
 (* This module implements the abstract interface to goals *)
 (* A general invariant of the module, is that a goal whose associated
@@ -73,7 +74,7 @@ module V82 = struct
     let (evars, evk) = Evarutil.new_pure_evar_full evars evi in
     let evars = Evd.restore_future_goals evars prev_future_goals prev_principal_goal in
     let ctxt = Environ.named_context_of_val hyps in
-    let inst = Array.map_of_list (fun (id, _, _) -> mkVar id) ctxt in
+    let inst = Array.map_of_list (mkVar % get_id) ctxt in
     let ev = Term.mkEvar (evk,inst) in
     (evk, ev, evars)
 
@@ -139,7 +140,7 @@ module V82 = struct
     let env = env sigma gl in
     let genv = Global.env () in
     let is_proof_var decl =
-      try ignore (Environ.lookup_named (Util.pi1 decl) genv); false
+      try ignore (Environ.lookup_named (get_id decl) genv); false
       with Not_found -> true in
     Environ.fold_named_context_reverse (fun t decl ->
 					  if is_proof_var decl then
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 99e32db04..09f308abe 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -22,6 +22,7 @@ open Proof_type
 open Type_errors
 open Retyping
 open Misctypes
+open Context.Named.Declaration
 
 type refiner_error =
 
@@ -160,7 +161,8 @@ let reorder_context env sign ord =
       | _ ->
           (match ctxt_head with
             | [] -> error_no_such_hypothesis (List.hd ord)
-            | (x,_,_ as d) :: ctxt ->
+            | d :: ctxt ->
+                let x = get_id d in
                 if Id.Set.mem x expected then
                   step ord (Id.Set.remove x expected)
                     ctxt (push_item x d moved_hyps) ctxt_tail
@@ -175,7 +177,8 @@ let reorder_val_context env sign ord =
 
 
 
-let check_decl_position env sign (x,_,_ as d) =
+let check_decl_position env sign d =
+  let x = get_id d in
   let needed = global_vars_set_of_decl env d in
   let deps = dependency_closure env (named_context_of_val sign) needed in
   if Id.List.mem x deps then
@@ -200,16 +203,17 @@ let move_location_eq m1 m2 = match m1, m2 with
 
 let rec get_hyp_after h = function
   | [] -> error_no_such_hypothesis h
-  | (hyp,_,_) :: right ->
-      if Id.equal hyp h then
-	match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveFirst
+  | d :: right ->
+      if Id.equal (get_id d) h then
+	match right with d' ::_ -> MoveBefore (get_id d') | [] -> MoveFirst
       else
        get_hyp_after h right
 
 let split_sign hfrom hto l =
   let rec splitrec left toleft = function
     | [] -> error_no_such_hypothesis hfrom
-    | (hyp,c,typ) as d :: right ->
+    | d :: right ->
+        let hyp,_,typ = to_tuple d in
       	if Id.equal hyp hfrom then
 	  (left,right,d, toleft || move_location_eq hto MoveLast)
       	else
@@ -227,27 +231,28 @@ let hyp_of_move_location = function
   | MoveBefore id -> id
   | _ -> assert false
 
-let move_hyp toleft (left,(idfrom,_,_ as declfrom),right) hto =
+let move_hyp toleft (left,declfrom,right) hto =
   let env = Global.env() in
-  let test_dep (hyp,c,typ as d) (hyp2,c,typ2 as d2) =
+  let test_dep d d2 =
     if toleft
-    then occur_var_in_decl env hyp2 d
-    else occur_var_in_decl env hyp d2
+    then occur_var_in_decl env (get_id d2) d
+    else occur_var_in_decl env (get_id d) d2
   in
   let rec moverec first middle = function
     | [] ->
 	if match hto with MoveFirst | MoveLast -> false | _ -> true then
 	  error_no_such_hypothesis (hyp_of_move_location hto);
 	List.rev first @ List.rev middle
-    | (hyp,_,_) :: _ as right when move_location_eq hto (MoveBefore hyp) ->
+    | d :: _ as right when move_location_eq hto (MoveBefore (get_id d)) ->
 	List.rev first @ List.rev middle @ right
-    | (hyp,_,_) as d :: right ->
+    | d :: right ->
+        let hyp = get_id d in
 	let (first',middle') =
       	  if List.exists (test_dep d) middle then
 	    if not (move_location_eq hto (MoveAfter hyp)) then
 	      (first, d::middle)
             else
-	      errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id idfrom ++
+	      errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id (get_id declfrom) ++
 	        Miscprint.pr_move_location pr_id hto ++
 	        str (if toleft then ": it occurs in " else ": it depends on ")
 	        ++ pr_id hyp ++ str ".")
@@ -483,12 +488,14 @@ and mk_casegoals sigma goal goalacc p c =
   (acc'',lbrty,conclty,sigma,p',c')
 
 
-let convert_hyp check sign sigma (id,b,bt as d) =
+let convert_hyp check sign sigma d =
+  let id,b,bt = to_tuple d in
   let env = Global.env() in
   let reorder = ref [] in
   let sign' =
     apply_to_hyp sign id
-      (fun _ (_,c,ct) _ ->
+      (fun _ d' _ ->
+        let _,c,ct = to_tuple d' in
         let env = Global.env_of_context sign in
         if check && not (is_conv env sigma bt ct) then
 	  errorlabstrm "Logic.convert_hyp"
@@ -522,14 +529,14 @@ let prim_refiner r sigma goal =
 	  if replace then
 	    let nexthyp = get_hyp_after id (named_context_of_val sign) in
 	    let sign,t,cl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t cl in
-	    move_hyp false ([],(id,None,t),named_context_of_val sign)
+	    move_hyp false ([], LocalAssum (id,t),named_context_of_val sign)
 	      nexthyp,
 	      t,cl,sigma
 	  else
             (if !check && mem_named_context id (named_context_of_val sign) then
 	      errorlabstrm "Logic.prim_refiner"
                 (str "Variable " ++ pr_id id ++ str " is already declared.");
-	     push_named_context_val (id,None,t) sign,t,cl,sigma) in
+	     push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in
         let (sg2,ev2,sigma) = 
 	  Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in
 	let oterm = Term.mkNamedLetIn id ev1 t ev2 in
@@ -546,7 +553,8 @@ let prim_refiner r sigma goal =
 		  with Not_found ->
 		    error "Cannot do a fixpoint on a non inductive type."
             	else
-		  check_ind (push_rel (na,None,c1) env) (k-1) b
+                  let open Context.Rel.Declaration in
+		  check_ind (push_rel (LocalAssum (na,c1)) env) (k-1) b
             | _ -> error "Not enough products."
 	in
 	let ((sp,_),u) = check_ind env n cl in
@@ -560,7 +568,7 @@ let prim_refiner r sigma goal =
 	      if !check && mem_named_context f (named_context_of_val sign) then
 		errorlabstrm "Logic.prim_refiner"
 		  (str "Name " ++ pr_id f ++ str " already used in the environment");
-	      mk_sign (push_named_context_val (f,None,ar) sign) oth
+	      mk_sign (push_named_context_val (LocalAssum (f,ar)) sign) oth
 	  | [] ->
 	      Evd.Monad.List.map (fun (_,_,c) sigma ->
                 let gl,ev,sig' =
@@ -584,7 +592,8 @@ let prim_refiner r sigma goal =
      	let rec check_is_coind env cl =
 	  let b = whd_betadeltaiota env sigma cl in
           match kind_of_term b with
-            | Prod (na,c1,b) -> check_is_coind (push_rel (na,None,c1) env) b
+            | Prod (na,c1,b) -> let open Context.Rel.Declaration in
+                                check_is_coind (push_rel (LocalAssum (na,c1)) env) b
             | _ ->
 		try
 		  let _ = find_coinductive env sigma b in ()
@@ -601,7 +610,7 @@ let prim_refiner r sigma goal =
                 error "Name already used in the environment.")
               with
               |	Not_found ->
-                  mk_sign (push_named_context_val (f,None,ar) sign) oth)
+                  mk_sign (push_named_context_val (LocalAssum (f,ar)) sign) oth)
 	  | [] -> 
               Evd.Monad.List.map (fun (_,c) sigma ->
                 let gl,ev,sigma =
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index fc33e9a65..403a36141 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -267,18 +267,19 @@ let _ = Goptions.declare_bool_option
       Goptions.optwrite = (fun b -> proof_using_auto_clear := b) }
 
 let set_used_variables l =
+  let open Context.Named.Declaration in
   let env = Global.env () in
   let ids = List.fold_right Id.Set.add l Id.Set.empty in
   let ctx = Environ.keep_hyps env ids in
   let ctx_set =
-    List.fold_right Id.Set.add (List.map pi1 ctx) Id.Set.empty in
+    List.fold_right Id.Set.add (List.map get_id ctx) Id.Set.empty in
   let vars_of = Environ.global_vars_set in
   let aux env entry (ctx, all_safe, to_clear as orig) =
     match entry with
-    | (x,None,_) ->
+    | LocalAssum (x,_) ->
        if Id.Set.mem x all_safe then orig
        else (ctx, all_safe, (Loc.ghost,x)::to_clear) 
-    | (x,Some bo, ty) as decl ->
+    | LocalDef (x,bo, ty) as decl ->
        if Id.Set.mem x all_safe then orig else
        let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
        if Id.Set.subset vars all_safe
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index a69645b11..681a7fa1a 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -10,6 +10,7 @@ open Names
 open Environ
 open Util
 open Vernacexpr
+open Context.Named.Declaration
 
 let to_string e =
   let rec aux = function
@@ -33,7 +34,8 @@ let in_nameset =
 
 let rec close_fwd e s =
   let s' =
-    List.fold_left (fun s (id,b,ty) ->      
+    List.fold_left (fun s decl ->
+      let (id,b,ty) = Context.Named.Declaration.to_tuple decl in
       let vb = Option.(default Id.Set.empty (map (global_vars_set e) b)) in
       let vty = global_vars_set e ty in
       let vbty = Id.Set.union vb vty in
@@ -61,13 +63,13 @@ and set_of_id env ty id =
         Id.Set.union (global_vars_set env ty) acc)
       Id.Set.empty ty
   else if Id.to_string id = "All" then
-    List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty
+    List.fold_right Id.Set.add (List.map get_id (named_context env)) Id.Set.empty
   else if CList.mem_assoc_f Id.equal id !known_names then
     process_expr env (CList.assoc_f Id.equal id !known_names) []
   else Id.Set.singleton id
 
 and full_set env =
-  List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty
+  List.fold_right Id.Set.add (List.map get_id (named_context env)) Id.Set.empty
 
 let process_expr env e ty =
   let ty_expr = SsSingl(Loc.ghost, Id.of_string "Type") in
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index ff8effcda..ebce25d29 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -17,6 +17,7 @@ open Pp
 open Util
 open Proofview_monad
 open Sigma.Notations
+open Context.Named.Declaration
 
 (** Main state of tactics *)
 type proofview = Proofview_monad.proofview
@@ -750,9 +751,15 @@ module Progress = struct
   let eq_named_context_val sigma1 sigma2 ctx1 ctx2 =
     let open Environ in
     let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in
-    let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
-      Names.Id.equal i1 i2 && Option.equal (eq_constr sigma1 sigma2) c1 c2 
-      && (eq_constr sigma1 sigma2) t1 t2
+    let eq_named_declaration d1 d2 =
+      match d1, d2 with
+      | LocalAssum (i1,t1), LocalAssum (i2,t2) ->
+         Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 t1 t2
+      | LocalDef (i1,c1,t1), LocalDef (i2,c2,t2) ->
+         Names.Id.equal i1 i2 && eq_constr sigma1 sigma2 c1 c2
+         && eq_constr sigma1 sigma2 t1 t2
+      | _ ->
+         false
     in List.equal eq_named_declaration c1 c2
 
   let eq_evar_body sigma1 sigma2 b1 b2 =
@@ -1075,12 +1082,13 @@ struct
   let typecheck_evar ev env sigma =
     let info = Evd.find sigma ev in
     (** Typecheck the hypotheses. *)
-    let type_hyp (sigma, env) (na, body, t as decl) =
+    let type_hyp (sigma, env) decl =
+      let t = get_type decl in
       let evdref = ref sigma in
       let _ = Typing.sort_of env evdref t in
-      let () = match body with
-      | None -> ()
-      | Some body -> Typing.check env evdref body t
+      let () = match decl with
+      | LocalAssum _ -> ()
+      | LocalDef (_,body,_) -> Typing.check env evdref body t
       in
       (!evdref, Environ.push_named decl env)
     in
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 8d6bdf6ae..186525e15 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -13,7 +13,7 @@ open Evd
 open Environ
 open Proof_type
 open Logic
-
+open Context.Named.Declaration
 
 let sig_it x = x.it
 let project x = x.sigma
@@ -202,7 +202,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
   let { it = gls; sigma = sigma; } = rslt in
   let hyps:Context.Named.t list =
     List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in
-  let cmp (i1, c1, t1) (i2, c2, t2) = Names.Id.equal i1 i2 in
+  let cmp d1 d2 = Names.Id.equal (get_id d1) (get_id d2) in
   let newhyps =
     List.map
       (fun hypl -> List.subtract cmp hypl oldhyps)
@@ -215,7 +215,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
     List.fold_left
     (fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ")
       ^ (List.fold_left
-	   (fun acc (nm,_,_) -> (Names.Id.to_string nm) ^ " " ^ acc)
+	   (fun acc d -> (Names.Id.to_string (get_id d)) ^ " " ^ acc)
 	   "" lh))
     "" newhyps in
   pp (str (emacs_str "<infoH>")
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index a1ebacea8..429bd2774 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -18,6 +18,7 @@ open Tacred
 open Proof_type
 open Logic
 open Refiner
+open Context.Named.Declaration
 
 let re_sig it  gc = { it = it; sigma = gc; }
 
@@ -40,9 +41,11 @@ let pf_hyps  = Refiner.pf_hyps
 let pf_concl gls = Goal.V82.concl (project gls) (sig_it gls)
 let pf_hyps_types gls  =
   let sign = Environ.named_context (pf_env gls) in
-  List.map (fun (id,_,x) -> (id, x)) sign
+  List.map (function LocalAssum (id,x)
+                   | LocalDef (id,_,x) -> id, x)
+           sign
 
-let pf_nth_hyp_id gls n = let (id,c,t) = List.nth (pf_hyps gls) (n-1) in id
+let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> get_id
 
 let pf_last_hyp gl = List.hd (pf_hyps gl)
 
@@ -53,8 +56,7 @@ let pf_get_hyp gls id =
     raise (RefinerError (NoSuchHyp id))
 
 let pf_get_hyp_typ gls id =
-  let (_,_,ty)= (pf_get_hyp gls id) in
-  ty
+  pf_get_hyp gls id |> get_type
 
 let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls)
 
@@ -204,13 +206,14 @@ module New = struct
     sign
 
   let pf_get_hyp_typ id gl =
-    let (_,_,ty) = pf_get_hyp id gl in
-    ty
+    pf_get_hyp id gl |> get_type
 
   let pf_hyps_types gl =
     let env = Proofview.Goal.env gl in
     let sign = Environ.named_context env in
-    List.map (fun (id,_,x) -> (id, x)) sign
+    List.map (function LocalAssum (id,x)
+                     | LocalDef (id,_,x) -> id, x)
+             sign
 
   let pf_last_hyp gl =
     let hyps = Proofview.Goal.hyps gl in