Follow stan hint, explicit fixity (default is infixl 9).

.stan.toml

@@ -118,12 +118,6 @@
   scope = "all"
   type = "Exclude"
 
-# Missing fixity declaration for operator
-[[check]]
-  id = "STAN-0301"
-  scope = "all"
-  type = "Exclude"
-
 # Using tuples of big size (>= 4) can decrease code readability
 [[check]]
   id = "STAN-0302"

src/Language/Fixpoint/Misc.hs

@@ -5,7 +5,6 @@
 {-# LANGUAGE TupleSections             #-}
 {-# LANGUAGE ConstraintKinds           #-}
 {-# LANGUAGE TypeOperators             #-}
-{-# LANGUAGE BangPatterns              #-}
 {-# LANGUAGE ImplicitParams            #-} -- ignore hlint
 
 
@@ -308,16 +307,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
 
@@ -425,27 +414,14 @@ 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 (=>>)
 
-(<$$>) ::  (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,13 +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
 
-(<$$>) :: (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`.
@@ -805,6 +802,7 @@ withCtx cfg file env k = do
   _   <- SMT.cleanupContext ctx
   return res
 
+infixl 9 ~>
 (~>) :: (Expr, String) -> Expr -> EvalST Expr
 (e, _str) ~> e' = do
   let msg = "PLE: " ++ _str ++ showpp (e, e')

src/Language/Fixpoint/Solver/PLE.hs

@@ -545,6 +545,7 @@ feVal (FE f) = f
 feAny :: [FinalExpand] -> FinalExpand
 feAny xs = FE $ any feVal xs
 
+infixl 9 <|>
 (<|>) :: FinalExpand -> FinalExpand -> FinalExpand
 (<|>) (FE True) _ = expand
 (<|>) _         f = f
@@ -598,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)
@@ -776,10 +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
 
-(<$$>) :: (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/Solver/Sanitize.hs

@@ -492,6 +492,7 @@ dropFuncSortedShadowedBinders fi = dropBinders ok (const True) fi
     ok x t  = M.member x defs ==> (F.allowHO fi || isFirstOrder t)
     defs    = M.fromList $ F.toListSEnv $ F.gLits fi
 
+infixl 9 ==>
 (==>) :: Bool -> Bool -> Bool
 p ==> q = not p || q
 

src/Language/Fixpoint/Types/Constraints.hs

@@ -805,6 +805,7 @@ toFixpoint cfg x' =    cfgDoc   cfg
       | mdata     = vcat     . map metaDoc . M.toList . bindInfo
       | otherwise = \_ -> text "\n"
 
+infixl 9 $++$
 ($++$) :: Doc -> Doc -> Doc
 x $++$ y = x $+$ text "\n" $+$ y
 

src/Language/Fixpoint/Types/Refinements.hs

@@ -892,9 +892,11 @@ pAndNoDedup = simplifyExpr id . PAnd
 
 pOr           = simplify . POr
 
+infixl 9 &.&
 (&.&) :: Pred -> Pred -> Pred
 (&.&) p q = pAnd [p, q]
 
+infixl 9 |.|
 (|.|) :: Pred -> Pred -> Pred
 (|.|) p q = pOr [p, q]
 

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,17 +98,6 @@ accum !z = modify (mappend z)
   -- !cur <- get
   -- put ((mappend $!! z) $!! cur)
 
-(<$$>) :: (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
 
@@ -185,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
@@ -280,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 () ()

src/Language/Fixpoint/Utils/Builder.hs

@@ -62,6 +62,7 @@ fromText = Leaf . B.fromText
 parens :: Builder -> Builder
 parens b = "(" <>  b <> ")"
 
+infixl 9 <+>
 (<+>) :: Builder -> Builder -> Builder
 x <+> y = x <> " " <> y