From 4f21c45748816c9e0cd4f93fa6f6d167e9757f81 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Tue, 30 Aug 2016 11:47:35 +0200 Subject: 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). --- plugins/funind/functional_principles_proofs.ml | 22 +++++++++++----------- plugins/funind/merge.ml | 4 ++-- 2 files changed, 13 insertions(+), 13 deletions(-) (limited to 'plugins') 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 = -- cgit v1.2.3