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

Author: Matej Kosik

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 () ++

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
 

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

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 =

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
 

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

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)

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

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

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'