Merge pull request #713 from ucsd-progsys/fd/remove-miscs

Remove unused or redundant functions

src/Language/Fixpoint/Defunctionalize.hs

@@ -26,7 +26,7 @@ import qualified Data.HashMap.Strict as M
 import           Data.Hashable
 import           Control.Monad ((>=>))
 import           Control.Monad.State
-import           Language.Fixpoint.Misc            (fM, secondM, mapSnd)
+import           Language.Fixpoint.Misc            (fM, secondM)
 import           Language.Fixpoint.Solver.Sanitize (symbolEnv)
 import           Language.Fixpoint.Types        hiding (GInfo(..), allowHO, fi)
 import qualified Language.Fixpoint.Types           as Types (GInfo(..))
@@ -80,8 +80,8 @@ normalizeLamsFromTo i   = go
     go (EApp e1 e2)     = let (i1, e1') = go e1
                               (i2, e2') = go e2
                           in (max i1 i2, EApp e1' e2')
-    go (ECst e s)       = mapSnd (`ECst` s) (go e)
-    go (PAll bs e)      = mapSnd (PAll bs) (go e)
+    go (ECst e s)       = fmap (`ECst` s) (go e)
+    go (PAll bs e)      = fmap (PAll bs) (go e)
     go e                = (i, e)
 
 

src/Language/Fixpoint/Misc.hs

@@ -326,18 +326,6 @@ ifM c t e = do
   b <- c
   if b then t else e
 
-mapEither :: (a -> Either b c) -> [a] -> ([b], [c])
-mapEither _ []     = ([], [])
-mapEither f (x:xs) = case f x of
-                       Left y  -> (y:ys, zs)
-                       Right z -> (ys, z:zs)
-                     where
-                       (ys, zs) = mapEither f xs
-
-isRight :: Either a b -> Bool
-isRight (Right _) = True
-isRight _         = False
-
 dbgFalse :: Bool
 dbgFalse = 1 > (2 :: Int)
 
@@ -394,21 +382,6 @@ coalesceEdges vss = [ (u, u, vs) | (u, vs) <- groupList (uvs ++ vus) ]
     vus           = swap <$> uvs
     uvs           = [ (u, v) | (u : vs) <- vss, v <- vs ]
 
-{-
-exitColorStrLn :: Moods -> String -> IO ()
-exitColorStrLn c s = do
-  writeIORef pbRef Nothing --(Just pr)
-  putStrLn "\n"
-  colorStrLn c s
--}
-
-mapFst :: (a -> c) -> (a, b) -> (c, b)
-mapFst f (x, y) = (f x, y)
-
-mapSnd :: (b -> c) -> (a, b) -> (a, c)
-mapSnd f (x, y) = (x, f y)
-
-
 {-@ allCombinations :: xss:[[a]] -> [{v:[a]| len v == len xss}] @-}
 allCombinations :: [[a]] -> [[a]]
 allCombinations xs = assert (all ((length xs == ) . length)) $ go xs
@@ -423,14 +396,6 @@ allCombinations xs = assert (all ((length xs == ) . length)) $ go xs
 powerset :: [a] -> [[a]]
 powerset xs = filterM (const [False, True]) xs
 
-infixl 9 =>>
-(=>>) :: Monad m => m b -> (b -> m a) -> m b
-(=>>) m f = m >>= (\x -> f x >> return x)
-
-infixl 9 <<=
-(<<=) :: Monad m => (b -> m a) -> m b -> m b
-(<<=) = flip (=>>)
-
 -- 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/Smt/Interface.hs

@@ -474,7 +474,7 @@ declare me = do
     ess        = distinctLiterals  lts
     axs        = Thy.axiomLiterals lts
     thyXTs     =                    filter (isKind 1) xts
-    qryXTs     = Misc.mapSnd tx <$> filter (isKind 2) xts
+    qryXTs     = fmap tx <$> filter (isKind 2) xts
     isKind n   = (n ==)  . symKind env . fst
     xts        = {- tracepp "symbolSorts" $ -} symbolSorts (F.seSort env)
     tx         = elaborate    "declare" env

src/Language/Fixpoint/Solver/Instantiate.hs

@@ -35,7 +35,7 @@ import qualified Language.Fixpoint.Solver.Common as Common (toSMT)
 import           Language.Fixpoint.Solver.Common          (askSMT)
 import           Control.Monad ((>=>), foldM, forM, forM_, join)
 import           Control.Monad.State
-import           Data.Bifunctor (second)
+import           Data.Bifunctor (first, second)
 import qualified Data.Text            as T
 import qualified Data.HashMap.Strict  as M
 import qualified Data.HashSet         as S
@@ -728,8 +728,8 @@ getDCEquality sEnv e1 e2
   | otherwise
   = Nothing
   where
-    (f1, es1) = Misc.mapFst (getDC sEnv) (splitEApp e1)
-    (f2, es2) = Misc.mapFst (getDC sEnv) (splitEApp e2)
+    (f1, es1) = first (getDC sEnv) (splitEApp e1)
+    (f2, es2) = first (getDC sEnv) (splitEApp e2)
 
 -- TODO: Stringy hacks
 getDC :: SymEnv -> Expr -> Maybe Symbol

src/Language/Fixpoint/Solver/Sanitize.hs

@@ -27,6 +27,7 @@ import qualified Language.Fixpoint.Types.Config as Cfg
 import qualified Language.Fixpoint.Types.Errors                    as E
 import qualified Language.Fixpoint.Smt.Theories                    as Thy
 import           Language.Fixpoint.Graph (kvEdges, CVertex (..))
+import qualified Data.Bifunctor as Bifunctor (first)
 import qualified Data.HashMap.Strict                               as M
 import qualified Data.HashSet                                      as S
 import qualified Data.List                                         as L
@@ -341,7 +342,7 @@ cNoFreeVars fi knownSym c = if S.null fv then Nothing else Just (S.toList fv)
     fv   = (`Misc.nubDiff` cDom) . filter (not . knownSym) $ cRng
 
 badCs :: Misc.ListNE (F.SimpC a, [F.Symbol]) -> E.Error
-badCs = E.catErrors . map (E.errFreeVarInConstraint . Misc.mapFst F.subcId)
+badCs = E.catErrors . map (E.errFreeVarInConstraint . Bifunctor.first F.subcId)
 
 --------------------------------------------------------------------------------
 -- | check that every DataDecl is regular

src/Language/Fixpoint/SortCheck.hs

@@ -70,6 +70,7 @@ import           Control.Exception (Exception, catch, try, throwIO)
 import           Control.Monad
 import           Control.Monad.Reader
 
+import           Data.Bifunctor (first)
 import qualified Data.HashMap.Strict       as M
 import           Data.IORef
 import qualified Data.List                 as L
@@ -295,7 +296,7 @@ elabApply env = go
   where
     go e                  = case splitArgs e of
                              (e', []) -> step e'
-                             (f , es) -> defuncEApp env (go f) (mapFst go <$> es)
+                             (f , es) -> defuncEApp env (go f) (first go <$> es)
     step (PAnd [])        = PTrue
     step (POr [])         = PFalse
     step (ENeg e)         = ENeg (go  e)

src/Language/Fixpoint/Types/Sorts.hs

@@ -92,6 +92,7 @@ import           Data.Generics             (Data)
 import           Data.Typeable             (Typeable)
 import           GHC.Generics              (Generic)
 import           Data.Aeson
+import           Data.Bifunctor (first)
 
 import           Data.Hashable
 import           Data.HashSet (HashSet)
@@ -682,7 +683,7 @@ instance (Eq a, Hashable a) => Monoid (TCEmb a) where
 
 
 tceMap :: (Eq b, Hashable b) => (a -> b) -> TCEmb a -> TCEmb b
-tceMap f = tceFromList . fmap (mapFst f) . tceToList
+tceMap f = tceFromList . fmap (first f) . tceToList
 
 tceFromList :: (Eq a, Hashable a) => [(a, (Sort, TCArgs))] -> TCEmb a
 tceFromList = TCE . M.fromList