From ebc5de6b2ce340b28116f6061bac6399c98426f9 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Mon, 6 Mar 2023 16:44:26 -0500
Subject: [PATCH] Rename `get*` to `run*`

---
 Data/Profunctor/Closed.idr     |  6 +++---
 Data/Profunctor/Strong.idr     |  4 ++--
 Data/Profunctor/Traversing.idr | 14 +++++++-------
 Data/Profunctor/Types.idr      |  4 ++--
 4 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/Data/Profunctor/Closed.idr b/Data/Profunctor/Closed.idr
index 0452c58..12a44ec 100644
--- a/Data/Profunctor/Closed.idr
+++ b/Data/Profunctor/Closed.idr
@@ -30,7 +30,7 @@ yon h s = (fst h s, snd h s)
 public export
 record Closure p a b where
   constructor MkClosure
-  getClosure : forall x. p (x -> a) (x -> b)
+  runClosure : forall x. p (x -> a) (x -> b)
 
 
 export
@@ -55,7 +55,7 @@ Strong p => GenStrong Pair (Closure p) where
 
 export
 Profunctor p => Closed (Closure p) where
-  closed p = getClosure $ produplicate p
+  closed p = runClosure $ produplicate p
 
 export
 Profunctor p => Functor (Closure p a) where
@@ -68,7 +68,7 @@ close f p = MkClosure $ f $ closed p
 
 export
 unclose : Profunctor q => p :-> Closure q -> p :-> q
-unclose f p = dimap const ($ ()) $ getClosure $ f p
+unclose f p = dimap const ($ ()) $ runClosure $ f p
 
 
 -- Environment
diff --git a/Data/Profunctor/Strong.idr b/Data/Profunctor/Strong.idr
index a184bce..2b7fabc 100644
--- a/Data/Profunctor/Strong.idr
+++ b/Data/Profunctor/Strong.idr
@@ -88,7 +88,7 @@ GenStrong Either Tagged where
 public export
 record GenTambara (ten, p : Type -> Type -> Type) a b where
   constructor MkTambara
-  getTambara : forall c. p (a `ten` c) (b `ten` c)
+  runTambara : forall c. p (a `ten` c) (b `ten` c)
 
 export
 Bifunctor ten => Profunctor p => Profunctor (GenTambara ten p) where
@@ -120,7 +120,7 @@ gentambara @{gs} f x = MkTambara $ f $ strongl @{gs} x
 
 export
 ungentambara : Tensor ten i => Profunctor q => p :-> GenTambara ten q -> p :-> q
-ungentambara f x = dimap unitr.bwd unitr.fwd $ getTambara $ f x
+ungentambara f x = dimap unitr.bwd unitr.fwd $ runTambara $ f x
 
 
 public export
diff --git a/Data/Profunctor/Traversing.idr b/Data/Profunctor/Traversing.idr
index d52efb0..142104b 100644
--- a/Data/Profunctor/Traversing.idr
+++ b/Data/Profunctor/Traversing.idr
@@ -30,38 +30,38 @@ import Data.Profunctor.Closed
 
 record Bazaar a b t where
   constructor MkBazaar
-  getBazaar : forall f. Applicative f => (a -> f b) -> f t
+  runBazaar : forall f. Applicative f => (a -> f b) -> f t
 
 Functor (Bazaar a b) where
   map f (MkBazaar g) = MkBazaar (map f . g)
 
 Applicative (Bazaar a b) where
   pure a = MkBazaar $ \_ => pure a
-  mf <*> ma = MkBazaar $ \k => getBazaar mf k <*> getBazaar ma k
+  mf <*> ma = MkBazaar $ \k => runBazaar mf k <*> runBazaar ma k
 
 sell : a -> Bazaar a b b
 sell a = MkBazaar ($ a)
 
 record Baz t b a where
   constructor MkBaz
-  getBaz : forall f. Applicative f => (a -> f b) -> f t
+  runBaz : forall f. Applicative f => (a -> f b) -> f t
 
 Functor (Baz t b) where
   map f (MkBaz g) = MkBaz (g . (. f))
 
 
 sold : Baz t a a -> t
-sold m = runIdentity (getBaz m Id)
+sold m = runIdentity (runBaz m Id)
 
 Foldable (Baz t b) where
-  foldr f i bz = getBaz bz @{appEndo} f i
+  foldr f i bz = runBaz bz @{appEndo} f i
     where
       -- Equivalent to `Const (Endomorphism acc)`
       appEndo : Applicative (\_ => acc -> acc)
       appEndo = MkApplicative @{MkFunctor (const id)} (const id) (.)
 
 Traversable (Baz t b) where
-  traverse f bz = map (\m => MkBaz (getBazaar m)) $ getBaz bz @{Compose} $ \x => sell <$> f x
+  traverse f bz = map (\m => MkBaz (runBazaar m)) $ runBaz bz @{Compose} $ \x => sell <$> f x
 
 
 public export
@@ -78,7 +78,7 @@ interface (Strong p, Choice p) => Traversing p where
 public export
 record CofreeTraversing p a b where
   constructor MkCFT
-  getCFT : forall f. Traversable f => p (f a) (f b)
+  runCFT : forall f. Traversable f => p (f a) (f b)
 
 export
 Profunctor p => Profunctor (CofreeTraversing p) where
diff --git a/Data/Profunctor/Types.idr b/Data/Profunctor/Types.idr
index 9bc72b4..c5b3310 100644
--- a/Data/Profunctor/Types.idr
+++ b/Data/Profunctor/Types.idr
@@ -109,7 +109,7 @@ Functor f => Profunctor (Costar f) where
 public export
 record Tagged {0 k : Type} (a : k) b where
   constructor Tag
-  getTagged : b
+  runTagged : b
 
 public export
 retag : Tagged a c -> Tagged b c
@@ -126,7 +126,7 @@ Applicative (Tagged a) where
 
 export
 Monad (Tagged a) where
-  join = getTagged
+  join = runTagged
   Tag x >>= f = f x
 
 export