From 4f21c45748816c9e0cd4f93fa6f6d167e9757f81 Mon Sep 17 00:00:00 2001
From: Matej Kosik <m4tej.kosik@gmail.com>
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).
---
 tactics/tacticals.ml | 4 ++--
 tactics/tactics.ml   | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'tactics')

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 }
-- 
cgit v1.2.3