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).

2 files changed, 13 insertions, 13 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 04c2c51e7e..527f4f0b12 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 f8aa21e954..14550a9fc7 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 =