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. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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). --- engine/evd.ml | 6 +++--- kernel/declareops.ml | 2 +- kernel/names.ml | 2 +- kernel/term_typing.ml | 4 ++-- lib/util.ml | 14 +++++++++----- lib/util.mli | 12 ++++++++---- library/impargs.ml | 2 +- library/lib.ml | 2 +- ltac/rewrite.ml | 2 +- plugins/funind/functional_principles_proofs.ml | 22 +++++++++++----------- plugins/funind/merge.ml | 4 ++-- pretyping/arguments_renaming.ml | 2 +- pretyping/evarsolve.ml | 2 +- pretyping/pretyping.ml | 2 +- proofs/goal.ml | 2 +- proofs/tacmach.ml | 2 +- tactics/tacticals.ml | 4 ++-- tactics/tactics.ml | 4 ++-- toplevel/command.ml | 2 +- toplevel/vernacentries.ml | 2 +- 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; -- cgit v1.2.3