Creating a module Nameops.Name extending module Names.Name.

This module collects the functions of Nameops which are about Name.t
and somehow standardize or improve their name, resulting in particular
from discussions in working group.

Note the use of a dedicated exception rather than a failwith for
Nameops.Name.out.

Drawback of the approach: one needs to open Nameops, or to use long
prefix Nameops.Name.

5 files changed, 32 insertions, 32 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 434fb14a6..0041797de 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -944,7 +944,7 @@ let generalize_non_dep hyp g =
     ((* observe_tac "thin" *) (thin to_revert))
     g
 
-let id_of_decl = RelDecl.get_name %> Nameops.out_name
+let id_of_decl = RelDecl.get_name %> Nameops.Name.get_id
 let var_of_decl = id_of_decl %> mkVar
 let revert idl =
   tclTHEN
@@ -1127,11 +1127,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	)
     in
     observe (str "full_params := " ++
-	       prlist_with_sep spc (RelDecl.get_name %> Nameops.out_name %> Ppconstr.pr_id)
+	       prlist_with_sep spc (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id)
 	       full_params
 	    );
     observe (str "princ_params := " ++
-	       prlist_with_sep spc (RelDecl.get_name %> Nameops.out_name %> Ppconstr.pr_id)
+	       prlist_with_sep spc (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id)
 	       princ_params
 	    );
     observe (str "fbody_with_full_params := " ++
@@ -1158,7 +1158,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		(fun i types ->
 		   let types = prod_applist (project g) types (List.rev_map var_of_decl princ_params) in
 		   { idx = idxs.(i)  - fix_offset;
-		     name = Nameops.out_name (fresh_id names.(i));
+		     name = Nameops.Name.get_id (fresh_id names.(i));
 		     types = types;
 		     offset = fix_offset;
 		     nb_realargs =
@@ -1181,7 +1181,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		   let first_args = Array.init nargs (fun i -> mkRel (nargs -i)) in
 		   let app_f = mkApp(f,first_args) in
 		   let pte_args = (Array.to_list first_args)@[app_f] in
-		   let app_pte = applist(mkVar (Nameops.out_name pte),pte_args) in
+		   let app_pte = applist(mkVar (Nameops.Name.get_id pte),pte_args) in
 		   let body_with_param,num =
 		     let body = get_body fnames.(i) in
 		     let body_with_full_params =
@@ -1208,9 +1208,9 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 			 num_in_block = num
 		     }
 		   in
-(* 		   observe (str "binding " ++ Ppconstr.pr_id (Nameops.out_name pte) ++  *)
+(* 		   observe (str "binding " ++ Ppconstr.pr_id (Nameops.Name.get_id pte) ++  *)
 (* 			      str " to " ++ Ppconstr.pr_id info.name); *)
-		   (Id.Map.add (Nameops.out_name pte) info acc_map,info::acc_info)
+		   (Id.Map.add (Nameops.Name.get_id pte) info acc_map,info::acc_info)
 		   )
 		0
 		(Id.Map.empty,[])
@@ -1284,7 +1284,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		       (do_replace evd
 			  full_params
 			  (fix_info.idx + List.length princ_params)
-			  (args_id@(List.map (RelDecl.get_name %> Nameops.out_name) princ_params))
+			  (args_id@(List.map (RelDecl.get_name %> Nameops.Name.get_id) princ_params))
 			  (all_funs.(fix_info.num_in_block))
 			  fix_info.num_in_block
 			  all_funs
@@ -1563,17 +1563,17 @@ let prove_principle_for_gen
       | _ -> assert false
   in
 (*   observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *)
-  let subst_constrs = List.map (get_name %> Nameops.out_name %> mkVar) (pre_rec_arg@princ_info.params) in
+  let subst_constrs = List.map (get_name %> Nameops.Name.get_id %> mkVar) (pre_rec_arg@princ_info.params) in
   let relation = substl subst_constrs relation in
   let input_type = substl subst_constrs rec_arg_type in
-  let wf_thm_id = Nameops.out_name (fresh_id (Name (Id.of_string "wf_R"))) in
+  let wf_thm_id = Nameops.Name.get_id (fresh_id (Name (Id.of_string "wf_R"))) in
   let acc_rec_arg_id =
-    Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))))
+    Nameops.Name.get_id (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))))
   in
   let revert l =
     tclTHEN (Proofview.V82.of_tactic (Tactics.generalize (List.map mkVar l))) (Proofview.V82.of_tactic (clear l))
   in
-  let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in
+  let fix_id = Nameops.Name.get_id (fresh_id (Name hrec_id)) in
   let prove_rec_arg_acc g =
       ((* observe_tac "prove_rec_arg_acc"  *)
 	 (tclCOMPLETE
@@ -1591,7 +1591,7 @@ let prove_principle_for_gen
       )
       g
   in
-  let args_ids = List.map (get_name %> Nameops.out_name) princ_info.args in
+  let args_ids = List.map (get_name %> Nameops.Name.get_id) princ_info.args in
   let lemma =
     match !tcc_lemma_ref with
      | Undefined -> user_err Pp.(str "No tcc proof !!")
@@ -1639,7 +1639,7 @@ let prove_principle_for_gen
     [
       observe_tac "start_tac" start_tac;
       h_intros
-	(List.rev_map (get_name %> Nameops.out_name)
+	(List.rev_map (get_name %> Nameops.Name.get_id)
 	   (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params)
 	);
       (* observe_tac "" *) Proofview.V82.of_tactic (assert_by
@@ -1677,14 +1677,14 @@ let prove_principle_for_gen
 	 in
 	 let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar  acc_rec_arg_id|])) in
 	 let predicates_names =
-	   List.map (get_name %> Nameops.out_name) princ_info.predicates
+	   List.map (get_name %> Nameops.Name.get_id) princ_info.predicates
 	 in
 	 let pte_info =
 	   { proving_tac =
 	       (fun eqs ->
 (* 		  msgnl (str "tcc_list := "++ prlist_with_sep spc Ppconstr.pr_id  !tcc_list); *)
-(* 		  msgnl (str "princ_info.args := "++ prlist_with_sep spc Ppconstr.pr_id  (List.map  (fun (na,_,_) -> (Nameops.out_name na)) princ_info.args)); *)
-(* 		  msgnl (str "princ_info.params := "++ prlist_with_sep spc Ppconstr.pr_id  (List.map  (fun (na,_,_) -> (Nameops.out_name na)) princ_info.params)); *)
+(* 		  msgnl (str "princ_info.args := "++ prlist_with_sep spc Ppconstr.pr_id  (List.map  (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.args)); *)
+(* 		  msgnl (str "princ_info.params := "++ prlist_with_sep spc Ppconstr.pr_id  (List.map  (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.params)); *)
 (* 		  msgnl (str "acc_rec_arg_id := "++  Ppconstr.pr_id acc_rec_arg_id); *)
 (* 		  msgnl (str "eqs := "++ prlist_with_sep spc Ppconstr.pr_id  eqs); *)
 
@@ -1693,7 +1693,7 @@ let prove_principle_for_gen
 		       is_mes acc_inv fix_id
 
 		       (!tcc_list@(List.map
-			   (get_name %> Nameops.out_name)
+			   (get_name %> Nameops.Name.get_id)
 			   (princ_info.args@princ_info.params)
 			)@ ([acc_rec_arg_id])) eqs
 		    )
@@ -1722,7 +1722,7 @@ let prove_principle_for_gen
 	 (* observe_tac "instanciate_hyps_with_args"  *)
 	   (instanciate_hyps_with_args
 	      make_proof
-	      (List.map (get_name %> Nameops.out_name) princ_info.branches)
+	      (List.map (get_name %> Nameops.Name.get_id) princ_info.branches)
 	      (List.rev args_ids)
 	   )
 	   gl'
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 18d63dd94..942527167 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -62,7 +62,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
       then List.tl args
       else args
     in
-    Context.Named.Declaration.LocalAssum (Nameops.out_name (Context.Rel.Declaration.get_name decl),
+    Context.Named.Declaration.LocalAssum (Nameops.Name.get_id (Context.Rel.Declaration.get_name decl),
                                           Term.compose_prod real_args (mkSort new_sort))
   in
   let new_predicates =
@@ -185,11 +185,11 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 
        with
 	 | Toberemoved ->
-(* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+(* 	    observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b)  in
 	    new_b, List.map pop binders_to_remove_from_b
 	| Toberemoved_with_rel (n,c) ->
-(* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+(* 	    observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b)  in
 	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
     end
@@ -214,11 +214,11 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 
       with
 	| Toberemoved ->
-(* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+(* 	    observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b)  in
 	    new_b, List.map pop binders_to_remove_from_b
 	| Toberemoved_with_rel (n,c) ->
-(* 	    observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+(* 	    observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
 	    let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b)  in
 	    new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
     end
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 74c0eb4cc..4946285e1 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -200,13 +200,13 @@ let is_rec names =
     | GIf(b,_,lhs,rhs) ->
 	(lookup names b) || (lookup names lhs) || (lookup names rhs)
     | GProd(na,_,t,b) | GLambda(na,_,t,b) ->
-	lookup names t || lookup (Nameops.name_fold Id.Set.remove na names) b
+	lookup names t || lookup (Nameops.Name.fold_right Id.Set.remove na names) b
     | GLetIn(na,b,t,c) ->
-	lookup names b || Option.cata (lookup names) true t || lookup (Nameops.name_fold Id.Set.remove na names) c
+	lookup names b || Option.cata (lookup names) true t || lookup (Nameops.Name.fold_right Id.Set.remove na names) c
     | GLetTuple(nal,_,t,b) -> lookup names t ||
 	lookup
 	  (List.fold_left
-	     (fun acc na -> Nameops.name_fold Id.Set.remove na acc)
+	     (fun acc na -> Nameops.Name.fold_right Id.Set.remove na acc)
 	     names
 	     nal
 	  )
@@ -885,7 +885,7 @@ let make_graph (f_ref:global_reference) =
 				  | Constrexpr.CLocalAssum (nal,_,_) ->
 				      List.map
 					(fun (loc,n) -> CAst.make ?loc @@ 
-					   CRef(Libnames.Ident(loc, Nameops.out_name n),None))
+					   CRef(Libnames.Ident(loc, Nameops.Name.get_id n),None))
 					nal
                                   | Constrexpr.CLocalPattern _ -> assert false
 			       )
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d68bdc215..12232dd83 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -421,7 +421,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       let params_bindings,avoid =
 	List.fold_left2
 	  (fun (bindings,avoid) decl p ->
-	     let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in
+	     let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in
 	     p::bindings,id::avoid
 	  )
 	  ([],pf_ids_of_hyps g)
@@ -431,7 +431,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       let lemmas_bindings =
 	List.rev (fst  (List.fold_left2
 	  (fun (bindings,avoid) decl p ->
-	     let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in
+	     let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in
 	     (nf_zeta p)::bindings,id::avoid)
 	  ([],avoid)
 	  princ_infos.predicates
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 2f9f70876..62eba9513 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -879,7 +879,7 @@ let rec make_rewrite_list expr_info max = function
 	    let k_na,_,t = destProd sigma t_eq in
 	    let _,_,t  = destProd sigma t in
 	    let def_na,_,_ = destProd sigma t in
-	    Nameops.out_name k_na,Nameops.out_name def_na
+	    Nameops.Name.get_id k_na,Nameops.Name.get_id def_na
 	  in
 	  Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
 	    true (* dep proofs also: *) true 
@@ -905,7 +905,7 @@ let make_rewrite expr_info l hp max =
 	    let k_na,_,t = destProd sigma t_eq in
 	    let _,_,t  = destProd sigma t in
 	    let def_na,_,_ = destProd sigma t in
-	    Nameops.out_name k_na,Nameops.out_name def_na
+	    Nameops.Name.get_id k_na,Nameops.Name.get_id def_na
 	  in
 	 observe_tac (str "general_rewrite_bindings")
 	   (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences