diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2016-02-17 10:32:40 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-02-17 11:13:04 +0100 |
| commit | 06fa0334047a9400d0b5a144601fca35746a53b8 (patch) | |
| tree | c3afdf28353d5ea096b1c6e3aece87ed17015b1c | |
| parent | 9a7afc12e0573c74d0bb0943372dddc3c61a03f1 (diff) | |
CLEANUP: Renaming "Util.compose" function to "%"
I propose to change the name of the "Util.compose" function to "%".
Reasons:
1. If one wants to express function composition,
then the new name enables us to achieve this goal easier.
2. In "Batteries Included" they had made the same choice.
| -rw-r--r-- | lib/util.ml | 8 | ||||
| -rw-r--r-- | lib/util.mli | 10 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 2 |
3 files changed, 17 insertions, 3 deletions
diff --git a/lib/util.ml b/lib/util.ml index b67539918..0f79c10df 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -87,7 +87,13 @@ let matrix_transpose mat = let identity x = x -let compose f g x = f (g x) +(** Function composition: the mathematical [∘] operator. + + So [g % f] is a synonym for [fun x -> g (f x)]. + + Also because [%] is right-associative, [h % g % f] means [fun x -> h (g (f x))]. + *) +let (%) f g x = f (g x) let const x _ = x diff --git a/lib/util.mli b/lib/util.mli index 7923c65a3..559874bb8 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -83,7 +83,15 @@ val matrix_transpose : 'a list list -> 'a list list (** {6 Functions. } *) val identity : 'a -> 'a -val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b + +(** Function composition: the mathematical [∘] operator. + + So [g % f] is a synonym for [fun x -> g (f x)]. + + Also because [%] is right-associative, [h % g % f] means [fun x -> h (g (f x))]. +*) +val (%) : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b + val const : 'a -> 'b -> 'a val iterate : ('a -> 'a) -> int -> 'a -> 'a val repeat : int -> ('a -> unit) -> 'a -> unit diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index a10d8fd2f..1e59c182c 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -99,7 +99,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 = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls) +let pf_hnf_type_of gls = pf_whd_betadeltaiota gls % pf_get_type_of gls let pf_is_matching = pf_apply Constr_matching.is_matching_conv let pf_matches = pf_apply Constr_matching.matches_conv |