Remove (<$$>) and use traverse instead.

src/Language/Fixpoint/Misc.hs

@@ -308,16 +308,6 @@ writeLoud s = whenLoud $ putStrLn s >> hFlush stdout
 ensurePath :: FilePath -> IO ()
 ensurePath = createDirectoryIfMissing True . takeDirectory
 
-singleton :: a -> [a]
-singleton x = [x]
-
-pair :: a -> a -> [a]
-pair x1 x2 = [x1, x2]
-
-triple :: a -> a -> a -> [a]
-triple x1 x2 x3 = [x1, x2, x3]
-
-
 fM :: (Monad m) => (a -> b) -> a -> m b
 fM f = return . f
 
@@ -433,22 +423,6 @@ infixl 9 <<=
 (<<=) :: Monad m => (b -> m a) -> m b -> m b
 (<<=) = flip (=>>)
 
-infixl 9 <$$>
-(<$$>) ::  (Monad m) => (a -> m b) -> [a] -> m [b]
-_ <$$> []           = return []
-f <$$> [x1]         = singleton <$> f x1
-f <$$> [x1, x2]     = pair      <$> f x1 <*> f x2
-f <$$> [x1, x2, x3] = triple    <$> f x1 <*> f x2 <*> f x3
-f <$$> xs           = revMapM f {- trace msg -} xs
-  where
-    _msg            = "<$$> on " ++ show (length xs)
-
-revMapM  :: (Monad m) => (a -> m b) -> [a] -> m [b]
-revMapM f          = go []
-  where
-    go !acc []     = return (reverse acc)
-    go !acc (x:xs) = do {!y <- f x; go (y:acc) xs}
-
 -- Null if first is a subset of second
 nubDiff :: (Eq a, Hashable a) => [a] -> [a] -> S.HashSet a
 nubDiff a b = a' `S.difference` b'

src/Language/Fixpoint/Solver/Extensionality.hs

@@ -15,7 +15,7 @@ import           Language.Fixpoint.Types.Config
 import           Language.Fixpoint.SortCheck
 import           Language.Fixpoint.Solver.Sanitize (symbolEnv)
 import           Language.Fixpoint.Types hiding (mapSort, Pos)
-import           Language.Fixpoint.Types.Visitor ( (<$$>), mapSort )
+import           Language.Fixpoint.Types.Visitor (mapSort)
 
 mytracepp :: (PPrint a) => String -> a -> a
 mytracepp = notracepp
@@ -140,13 +140,13 @@ mapMPosExpr p f = go p
     go p (PAtom r e1 e2) = f p =<< (PAtom r     <$>  go p e1 <*> go p e2            )
 
     go p (PImp p1 p2)    = f p =<< (PImp        <$>  go (negatePos p) p1 <*> go p p2)
-    go p (PAnd ps)       = f p . PAnd =<< (go p <$$> ps)
+    go p (PAnd ps)       = f p . PAnd =<< (go p `traverse` ps)
 
     -- The below cannot appear due to normalization
     go p (PNot e)        = f p . PNot =<< go p e
     go p (PIff p1 p2)    = f p =<< (PIff        <$>  go p p1 <*> go p p2            )
     go p (EIte e e1 e2)  = f p =<< (EIte        <$>  go p e  <*> go p e1 <*> go p e2)
-    go p (POr  ps)       = f p . POr =<< (go p <$$> ps)
+    go p (POr  ps)       = f p . POr =<< (go p `traverse` ps)
 
     -- The following canot appear in general
     go p (PAll xts e)    = f p . PAll   xts =<< go p e

src/Language/Fixpoint/Solver/Instantiate.hs

@@ -451,14 +451,10 @@ eval γ stk = go
     go (PNot e)         = PNot         <$> go e
     go (PImp e1 e2)     = PImp         <$> go e1 <*> go e2
     go (PIff e1 e2)     = PIff         <$> go e1 <*> go e2
-    go (PAnd es)        = PAnd         <$> (go  <$$> es)
-    go (POr es)         = POr          <$> (go  <$$> es)
+    go (PAnd es)        = PAnd         <$> (go `traverse` es)
+    go (POr es)         = POr          <$> (go `traverse` es)
     go e                = return e
 
-infixl 9 <$$>
-(<$$>) :: (Monad m) => (a -> m b) -> [a] -> m [b]
-f <$$> xs = f Misc.<$$> xs
-
 -- | `evalArgs` also evaluates all the partial applications for hacky reasons,
 --   suppose `foo g = id` then we want `foo g 10 = 10` and for that we need
 --   to `eval` the term `foo g` into `id` to tickle the `eval` on `id 10`.

src/Language/Fixpoint/Solver/PLE.hs

@@ -599,8 +599,8 @@ eval γ ctx et = go
     go (PNot e')        = mapFE PNot <$> go e'
     go (PImp e1 e2)     = binOp PImp e1 e2
     go (PIff e1 e2)     = binOp PIff e1 e2
-    go (PAnd es)        = efAll PAnd (go  <$$> es)
-    go (POr es)         = efAll POr (go <$$> es)
+    go (PAnd es)        = efAll PAnd (go `traverse` es)
+    go (POr es)         = efAll POr (go `traverse` es)
     go e | EVar _ <- dropECst e = do
       (me', fe) <- evalApp γ ctx e [] et
       return (Mb.fromMaybe e me', fe)
@@ -777,11 +777,6 @@ evalRESTWithCache cacheRef γ ctx acc rp =
     addConst (e,e') = if isConstant (knDCs γ) e'
                       then ctx { icSimpl = M.insert e e' $ icSimpl ctx} else ctx
 
-infixl 9 <$$>
-(<$$>) :: (Monad m) => (a -> m b) -> [a] -> m [b]
-f <$$> xs = f Misc.<$$> xs
-
-
 -- | @evalApp kn ctx e es@ unfolds expressions in @eApps e es@ using rewrites
 -- and equations
 evalApp :: Knowledge -> ICtx -> Expr -> [Expr] -> EvalType -> EvalST (Maybe Expr, FinalExpand)

src/Language/Fixpoint/Types/Visitor.hs

@@ -45,10 +45,6 @@ module Language.Fixpoint.Types.Visitor (
   , foldSort
   , mapSort
   , foldDataDecl
-
-  , (<$$>)
-
-
   ) where
 
 -- import           Control.Monad.Trans.State.Strict (State, modify, runState)
@@ -102,18 +98,6 @@ accum !z = modify (mappend z)
   -- !cur <- get
   -- put ((mappend $!! z) $!! cur)
 
-infixl 9 <$$>
-(<$$>) :: (Monad m) => (a -> m b) -> [a] -> m [b]
-f <$$> xs = f Misc.<$$> xs
-
--- (<$$>) ::  (Applicative f) => (a -> f b) -> [a] -> f [b]
--- f <$$> x = traverse f x
--- _ <$$> []     = return []
--- f <$$> (x:xs) = do
-  -- !y  <- f x
-  -- !ys <- f <$$> xs
-  -- return (y:ys)
-------------------------------------------------------------------------------
 class Visitable t where
   visit :: (Monoid a) => Visitor a c -> c -> t -> VisitM a t
 
@@ -186,8 +170,8 @@ visitExpr !v    = vE
     step !c (EBin o e1 e2)  = EBin o      <$> vE c e1 <*> vE c e2
     step !c (EIte p e1 e2)  = EIte        <$> vE c p  <*> vE c e1 <*> vE c e2
     step !c (ECst e t)      = (`ECst` t)  <$> vE c e
-    step !c (PAnd  ps)      = PAnd        <$> (vE c <$$> ps)
-    step !c (POr  ps)       = POr         <$> (vE c <$$> ps)
+    step !c (PAnd  ps)      = PAnd        <$> (vE c `traverse` ps)
+    step !c (POr  ps)       = POr         <$> (vE c `traverse` ps)
     step !c (PNot p)        = PNot        <$> vE c p
     step !c (PImp p1 p2)    = PImp        <$> vE c p1 <*> vE c p2
     step !c (PIff p1 p2)    = PIff        <$> vE c p1 <*> vE c p2
@@ -281,8 +265,8 @@ mapMExpr f = go
     go (PIff p1 p2)    = f =<< (PIff        <$>  go p1 <*> go p2          )
     go (PAtom r e1 e2) = f =<< (PAtom r     <$>  go e1 <*> go e2          )
     go (EIte p e1 e2)  = f =<< (EIte        <$>  go p  <*> go e1 <*> go e2)
-    go (PAnd  ps)      = f . PAnd =<< (go <$$> ps)
-    go (POr  ps)       = f . POr =<< (go <$$> ps)
+    go (PAnd ps)       = f . PAnd =<< (go `traverse` ps)
+    go (POr ps)        = f . POr =<< (go `traverse` ps)
 
 mapKVarSubsts :: Visitable t => (KVar -> Subst -> Subst) -> t -> t
 mapKVarSubsts f          = trans kvVis () ()