CLEANUP: switching from "right-to-left" to "left-to-right" function composition operator.

Short story:

    This pull-request:

    (1) removes the definition of the "right-to-left" function composition operator

    (2) adds the definition of the "left-to-right" function composition operator

    (3) rewrites the code relying on "right-to-left" function composition to rely on "left-to-right" function composition operator instead.

Long story:

    In mathematics, function composition is traditionally denoted with ∘ operator.

    Ocaml standard library does not provide analogous operator under any name.

    Batteries Included provides provides two alternatives:

    	_ % _

    and

    	_ %> _

    The first operator one corresponds to the classical ∘ operator routinely used in mathematics.
    I.e.:

    	(f4 % f3 % f2 % f1) x  ≜  (f4 ∘ f3 ∘ f2 ∘ f1) x

    We can call it "right-to-left" composition because:
    - the function we write as first (f4) will be called as last
    - and the function write as last (f1) will be called as first.

    The meaning of the second operator is this:

    	(f1 %> f2 %> f3 %> f4) x  ≜  (f4 ∘ f3 ∘ f2 ∘ f1) x

    We can call it "left-to-right" composition because:
    - the function we write as first (f1) will be called first
    - and the function we write as last (f4) will be called last
    That is, the functions are written in the same order in which we write and read them.

    I think that it makes sense to prefer the "left-to-right" variant because
    it enables us to write functions in the same order in which they will be actually called
    and it thus better fits our culture
    (we read/write from left to right).

20 files changed, 51 insertions, 43 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 3aab39eda..913856a8d 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -246,7 +246,7 @@ let evar_instance_array test_id info args =
     instrec filter (evar_context info) 0
 
 let make_evar_instance_array info args =
-  evar_instance_array (isVarId % NamedDecl.get_id) info args
+  evar_instance_array (NamedDecl.get_id %> isVarId) info args
 
 let instantiate_evar_array info c args =
   let inst = make_evar_instance_array info args in
@@ -684,7 +684,7 @@ let restrict evk filter ?candidates evd =
       evar_extra = Store.empty } in
   let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in
   let ctxt = Filter.filter_list filter (evar_context evar_info) in
-  let id_inst = Array.map_of_list (mkVar % NamedDecl.get_id) ctxt in
+  let id_inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in
   let body = mkEvar(evk',id_inst) in
   let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
   { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
@@ -1403,7 +1403,7 @@ let print_env_short env =
     | RelDecl.LocalAssum (n,_) -> pr_name n
     | RelDecl.LocalDef (n,b,_) -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")"
   in
-  let pr_named_decl = pr_rel_decl % NamedDecl.to_rel_decl in
+  let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl in
   let nc = List.rev (named_context env) in
   let rc = List.rev (rel_context env) in
     str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 8943de404..0a822d6fa 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -147,7 +147,7 @@ let subst_const_body sub cb =
     themselves. But would it really bring substantial gains ? *)
 
 let hcons_rel_decl =
-  RelDecl.map_type Term.hcons_types % RelDecl.map_value Term.hcons_constr % RelDecl.map_name Names.Name.hcons
+  RelDecl.map_name Names.Name.hcons %> RelDecl.map_value Term.hcons_constr %> RelDecl.map_type Term.hcons_types
 
 let hcons_rel_context l = List.smartmap hcons_rel_decl l
 
diff --git a/kernel/names.ml b/kernel/names.ml
index d673c91e8..1313bae7b 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -89,7 +89,7 @@ struct
     | Anonymous -> true
     | Name _ -> false
 
-  let is_name = not % is_anonymous
+  let is_name = is_anonymous %> not
 
   let compare n1 n2 = match n1, n2 with
     | Anonymous, Anonymous -> 0
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 8db65e33c..7a5ac7a39 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -262,7 +262,7 @@ let record_aux env s_ty s_bo suggested_expr =
     String.concat " "
       (CList.map_filter (fun decl ->
           let id = NamedDecl.get_id decl in
-          if List.exists (Id.equal id % NamedDecl.get_id) in_ty then None
+          if List.exists (NamedDecl.get_id %> Id.equal id) in_ty then None
           else Some (Id.to_string id))
         (keep_hyps env s_bo)) in
   Aux_file.record_in_aux "context_used" (v ^ ";" ^ suggested_expr)
@@ -285,7 +285,7 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
   let sort evn l =
     List.filter (fun decl ->
       let id = NamedDecl.get_id decl in
-      List.exists (Names.Id.equal id % NamedDecl.get_id) l)
+      List.exists (NamedDecl.get_id %> Names.Id.equal id) l)
     (named_context env) in
   (* We try to postpone the computation of used section variables *)
   let hyps, def =
diff --git a/lib/util.ml b/lib/util.ml
index 009dfbe1c..9fb0d48ee 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -87,13 +87,17 @@ let matrix_transpose mat =
 
 let identity x = x
 
-(** Function composition: the mathematical [∘] operator.
+(** Left-to-right function composition:
+    
+    [f1 %> f2] is [fun x -> f2 (f1 x)].
 
-    So [g % f] is a synonym for [fun x -> g (f x)].
+    [f1 %> f2 %> f3] is [fun x -> f3 (f2 (f1 x))].
 
-    Also because [%] is right-associative, [h % g % f] means [fun x -> h (g (f x))].
- *)
-let (%) f g x = f (g x)
+    [f1 %> f2 %> f3 %> f4] is [fun x -> f4 (f3 (f2 (f1 x)))]
+
+    etc.
+*)
+let (%>) f g x = g (f x)
 
 let const x _ = x
 
diff --git a/lib/util.mli b/lib/util.mli
index 6bed7e355..cf8041a0d 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -84,13 +84,17 @@ val matrix_transpose : 'a list list -> 'a list list
 
 val identity : 'a -> 'a
 
-(** Function composition: the mathematical [∘] operator.
+(** Left-to-right function composition:
+    
+    [f1 %> f2] is [fun x -> f2 (f1 x)].
 
-    So [g % f] is a synonym for [fun x -> g (f x)].
+    [f1 %> f2 %> f3] is [fun x -> f3 (f2 (f1 x))].
 
-    Also because [%] is right-associative, [h % g % f] means [fun x -> h (g (f x))].
+    [f1 %> f2 %> f3 %> f4] is [fun x -> f4 (f3 (f2 (f1 x)))]
+
+    etc.
 *)
-val (%) : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
+val ( %> ) : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c
 
 val const : 'a -> 'b -> 'a
 val iterate : ('a -> 'a) -> int -> 'a -> 'a
diff --git a/library/impargs.ml b/library/impargs.ml
index 2997f94ed..07b6b2bae 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -520,7 +520,7 @@ let impls_of_context ctx =
   | Implicit -> Some (NamedDecl.get_id decl, Manual, (true, true))
   | _ -> None
   in
-  List.rev_map map (List.filter (is_local_assum % fst) ctx)
+  List.rev_map map (List.filter (fst %> is_local_assum) ctx)
 
 let adjust_side_condition p = function
   | LessArgsThan n -> LessArgsThan (n+p)
diff --git a/library/lib.ml b/library/lib.ml
index 412772e8a..a5a9a0194 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -445,7 +445,7 @@ let extract_hyps (secs,ohyps) =
   in aux (secs,ohyps)
 
 let instance_from_variable_context =
-  Array.of_list % List.map NamedDecl.get_id % List.filter is_local_assum % List.map fst
+  List.map fst %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list
 
 let named_of_variable_context =
   List.map fst
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index ad052cdd1..09454f3e8 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1540,7 +1540,7 @@ let assert_replacing id newt tac =
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     let ctx = Environ.named_context env in
-    let after, before = List.split_when (Id.equal id % NamedDecl.get_id) ctx in
+    let after, before = List.split_when (NamedDecl.get_id %> Id.equal id) ctx in
     let nc = match before with
     | [] -> assert false
     | d :: rem -> insert_dependent env (LocalAssum (NamedDecl.get_id d, newt)) [] after @ rem
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 04c2c51e7..527f4f0b1 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -940,8 +940,8 @@ let generalize_non_dep hyp g =
     ((* observe_tac "thin" *) (thin to_revert))
     g
 
-let id_of_decl = Nameops.out_name % RelDecl.get_name
-let var_of_decl = mkVar % id_of_decl
+let id_of_decl = RelDecl.get_name %> Nameops.out_name
+let var_of_decl = id_of_decl %> mkVar
 let revert idl =
   tclTHEN
     (Proofview.V82.of_tactic (generalize (List.map mkVar idl)))
@@ -1121,11 +1121,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 (Ppconstr.pr_id % Nameops.out_name % RelDecl.get_name)
+	       prlist_with_sep spc (RelDecl.get_name %> Nameops.out_name %> Ppconstr.pr_id)
 	       full_params
 	    );
     observe (str "princ_params := " ++
-	       prlist_with_sep spc (Ppconstr.pr_id % Nameops.out_name % RelDecl.get_name)
+	       prlist_with_sep spc (RelDecl.get_name %> Nameops.out_name %> Ppconstr.pr_id)
 	       princ_params
 	    );
     observe (str "fbody_with_full_params := " ++
@@ -1279,7 +1279,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 (Nameops.out_name % RelDecl.get_name) princ_params))
+			  (args_id@(List.map (RelDecl.get_name %> Nameops.out_name) princ_params))
 			  (all_funs.(fix_info.num_in_block))
 			  fix_info.num_in_block
 			  all_funs
@@ -1558,7 +1558,7 @@ let prove_principle_for_gen
       | _ -> assert false
   in
 (*   observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *)
-  let subst_constrs = List.map (mkVar % Nameops.out_name % get_name) (pre_rec_arg@princ_info.params) in
+  let subst_constrs = List.map (get_name %> Nameops.out_name %> 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
@@ -1586,7 +1586,7 @@ let prove_principle_for_gen
       )
       g
   in
-  let args_ids = List.map (Nameops.out_name % get_name) princ_info.args in
+  let args_ids = List.map (get_name %> Nameops.out_name) princ_info.args in
   let lemma =
     match !tcc_lemma_ref with
      | None -> error "No tcc proof !!"
@@ -1633,7 +1633,7 @@ let prove_principle_for_gen
     [
       observe_tac "start_tac" start_tac;
       h_intros
-	(List.rev_map (Nameops.out_name % get_name)
+	(List.rev_map (get_name %> Nameops.out_name)
 	   (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params)
 	);
       (* observe_tac "" *) Proofview.V82.of_tactic (assert_by
@@ -1671,7 +1671,7 @@ 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 (Nameops.out_name % get_name) princ_info.predicates
+	   List.map (get_name %> Nameops.out_name) princ_info.predicates
 	 in
 	 let pte_info =
 	   { proving_tac =
@@ -1687,7 +1687,7 @@ let prove_principle_for_gen
 		       is_mes acc_inv fix_id
 
 		       (!tcc_list@(List.map
-			   (Nameops.out_name % get_name)
+			   (get_name %> Nameops.out_name)
 			   (princ_info.args@princ_info.params)
 			)@ ([acc_rec_arg_id])) eqs
 		    )
@@ -1716,7 +1716,7 @@ let prove_principle_for_gen
 	 (* observe_tac "instanciate_hyps_with_args"  *)
 	   (instanciate_hyps_with_args
 	      make_proof
-	      (List.map (Nameops.out_name % get_name) princ_info.branches)
+	      (List.map (get_name %> Nameops.out_name) princ_info.branches)
 	      (List.rev args_ids)
 	   )
 	   gl'
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index f8aa21e95..14550a9fc 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -59,8 +59,8 @@ let understand = Pretyping.understand (Global.env()) Evd.empty
 let id_of_name = function
     Anonymous -> Id.of_string "H"
   | Name id   -> id;;
-let name_of_string = Name.mk_name % Id.of_string
-let string_of_name = Id.to_string % id_of_name
+let name_of_string = Id.of_string %> Name.mk_name
+let string_of_name = id_of_name %> Id.to_string
 
 (** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *)
 let isVarf f x =
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index ff6b33c49..077ee4e15 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -50,7 +50,7 @@ let discharge_rename_args = function
      (try 
        let vars,_,_ = section_segment_of_reference c in
        let c' = pop_global_reference c in
-       let var_names = List.map (Name.mk_name % NamedDecl.get_id % fst) vars in
+       let var_names = List.map (fst %> NamedDecl.get_id %> Name.mk_name) vars in
        let names' = List.map (fun l -> var_names @ l) names in
        Some (ReqGlobal (c', names), (c', names'))
      with Not_found -> Some req)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index c0a42ae7d..a744f5ec6 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -169,7 +169,7 @@ type 'a update =
 | NoUpdate
 
 open Context.Named.Declaration
-let inst_of_vars sign = Array.map_of_list (mkVar % get_id) sign
+let inst_of_vars sign = Array.map_of_list (get_id %> mkVar) sign
 
 let restrict_evar_key evd evk filter candidates =
   match filter, candidates with
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 9b4415920..af8bcb3f6 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -105,7 +105,7 @@ let lookup_named id env = lookup_named id env.env
 let e_new_evar env evdref ?src ?naming typ =
   let subst2 subst vsubst c = csubst_subst subst (replace_vars vsubst c) in
   let open Context.Named.Declaration in
-  let inst_vars = List.map (mkVar % get_id) (named_context env.env) in
+  let inst_vars = List.map (get_id %> mkVar) (named_context env.env) in
   let inst_rels = List.rev (rel_list 0 (nb_rel env.env)) in
   let (subst, vsubst, _, nc) = Lazy.force env.extra in
   let typ' = subst2 subst vsubst typ in
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 75f56c6b9..a141708c2 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -78,7 +78,7 @@ module V82 = struct
     let evars = Sigma.to_evar_map evars 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 (mkVar % NamedDecl.get_id) ctxt in
+    let inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in
     let ev = Term.mkEvar (evk,inst) in
     (evk, ev, evars)
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index e90024076..93e276f4b 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -103,7 +103,7 @@ let pf_const_value              = pf_reduce (fun env _ -> constant_value_in env)
 let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
 let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
 
-let pf_hnf_type_of gls          = pf_whd_all gls % pf_get_type_of gls
+let pf_hnf_type_of gls          = pf_get_type_of gls %> pf_whd_all gls
 
 let pf_is_matching              = pf_apply Constr_matching.is_matching_conv
 let pf_matches                  = pf_apply Constr_matching.matches_conv
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 664629f34..ae2307190 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -100,7 +100,7 @@ let onNLastHypsId n tac = onHyps (nLastHypsId n) tac
 let onNLastHyps n tac   = onHyps (nLastHyps n) tac
 
 let afterHyp id gl =
-  fst (List.split_when (Id.equal id % NamedDecl.get_id) (pf_hyps gl))
+  fst (List.split_when (NamedDecl.get_id %> Id.equal id) (pf_hyps gl))
 
 (***************************************)
 (*           Clause Tacticals          *)
@@ -593,7 +593,7 @@ module New = struct
   let afterHyp id tac =
     Proofview.Goal.enter { enter = begin fun gl ->
     let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
-    let rem, _ = List.split_when (Id.equal id % NamedDecl.get_id) hyps in
+    let rem, _ = List.split_when (NamedDecl.get_id %> Id.equal id) hyps in
     tac rem
     end }
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 51bbd9058..7519339ca 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -169,7 +169,7 @@ let unsafe_intro env store decl b =
   Refine.refine ~unsafe:true { run = begin fun sigma ->
     let ctx = named_context_val env in
     let nctx = push_named_context_val decl ctx in
-    let inst = List.map (mkVar % NamedDecl.get_id) (named_context env) in
+    let inst = List.map (NamedDecl.get_id %> mkVar) (named_context env) in
     let ninst = mkRel 1 :: inst in
     let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in
     let Sigma (ev, sigma, p) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in
@@ -366,7 +366,7 @@ let rename_hyp repl =
       let nhyps = List.map map hyps in
       let nconcl = subst concl in
       let nctx = Environ.val_of_named_context nhyps in
-      let instance = List.map (mkVar % NamedDecl.get_id) hyps in
+      let instance = List.map (NamedDecl.get_id %> mkVar) hyps in
       Refine.refine ~unsafe:true { run = begin fun sigma ->
         Evarutil.new_evar_instance nctx sigma nconcl ~store instance
       end }
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 80df7e48d..bd8e870b4 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -578,7 +578,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
       
   (* Names of parameters as arguments of the inductive type (defs removed) *)
   let assums = List.filter is_local_assum ctx_params in
-  let params = List.map (out_name % RelDecl.get_name) assums in
+  let params = List.map (RelDecl.get_name %> out_name) assums in
 
   (* Interpret the arities *)
   let arities = List.map (interp_ind_arity env_params evdref) indl in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index eeb4e26af..40c7c7010 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -856,7 +856,7 @@ let vernac_set_used_variables e =
   let l = Proof_using.process_expr env e tys in
   let vars = Environ.named_context env in
   List.iter (fun id -> 
-    if not (List.exists (Id.equal id % NamedDecl.get_id) vars) then
+    if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then
       errorlabstrm "vernac_set_used_variables"
         (str "Unknown variable: " ++ pr_id id))
     l;