aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evd.ml
diff options
context:
space:
mode:
authorGravatar Matej Kosik <m4tej.kosik@gmail.com>2016-08-30 11:47:35 +0200
committerGravatar Matej Kosik <m4tej.kosik@gmail.com>2016-08-30 11:47:35 +0200
commit4f21c45748816c9e0cd4f93fa6f6d167e9757f81 (patch)
treef22bde63a6522883782ada4c40fa6b5c1ff1cc4c /engine/evd.ml
parent2ff6d31c7a6011b26dfa7f0b2bb593b356833058 (diff)
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).
Diffstat (limited to 'engine/evd.ml')
-rw-r--r--engine/evd.ml6
1 files changed, 3 insertions, 3 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 () ++