agda · andreasabel · Oct 19, 2023 · Oct 19, 2023
diff --git a/Agda.cabal b/Agda.cabal
@@ -289,7 +289,7 @@ common language
 
   if impl(ghc >= 9.2)
     ghc-options:
---      -Werror=operator-whitespace
+      -Werror=operator-whitespace
       -Werror=redundant-bang-patterns
 
   if impl(ghc >= 9.4)

diff --git a/src/full/Agda/Auto/Auto.hs b/src/full/Agda/Auto/Auto.hs
@@ -414,8 +414,8 @@ auto ii rng argstr = liftTCM $ locallyTC eMakeCase (const True) $ do
 
       hits <- if "-a" `elem` hints then do
         st <- liftTCM $ join $ pureTCM $ \st _ -> return st
-        let defs = st^.stSignature.sigDefinitions
-            idefs = st^.stImports.sigDefinitions
+        let defs    = st ^. stSignature . sigDefinitions
+            idefs   = st ^. stImports   . sigDefinitions
             alldefs = HMap.keys defs ++ HMap.keys idefs
         catMaybes <$> mapM (\n ->
           case thisdefinfo of

diff --git a/src/full/Agda/Auto/Syntax.hs b/src/full/Agda/Auto/Syntax.hs
@@ -373,7 +373,7 @@ instance Weakening (ICArgList o) where
     CALConcat a as -> CALConcat (weak' n a) (weak' n as)
 
 instance Weakening (Elr o) where
-  weak' n = rename (n+)
+  weak' n = rename (n +)
 
 -- | Substituting for a variable.
 doclos :: [CAction o] -> Nat -> Either Nat (ICExp o)

diff --git a/src/full/Agda/Auto/Typecheck.hs b/src/full/Agda/Auto/Typecheck.hs
@@ -31,7 +31,7 @@ tcExp isdep ctx typ@(TrBr typtrs ityp@(Clos _ itypexp)) trm =
               Var v ->
                 case ctx !!! v of
                   Nothing     -> return Nothing
-                  Just (_, a) -> return $ Just (weak (v+1) a, id)
+                  Just (_, a) -> return $ Just (weak (v + 1) a, id)
               Const c -> do
                cdef <- readIORef c
                return $ Just (closify (cdtype cdef), mpret . And (Just [Term args]) (noiotastep_term c args))

diff --git a/src/full/Agda/Compiler/JS/Compiler.hs b/src/full/Agda/Compiler/JS/Compiler.hs
@@ -443,7 +443,7 @@ definition' kit q d t ls =
         let (body, given) = lamView funBody
               where
                 lamView :: T.TTerm -> (T.TTerm, Int)
-                lamView (T.TLam t) = (+1) <$> lamView t
+                lamView (T.TLam t) = (+ 1) <$> lamView t
                 lamView t = (t, 0)
 
             -- number of eta expanded args
@@ -609,7 +609,7 @@ compileTerm kit t = go t
     unit = return Null
 
     mkArray xs
-        | 2 * length (filter ((==Null) . snd) xs) <= length xs = Array xs
+        | 2 * length (filter ((== Null) . snd) xs) <= length xs = Array xs
         | otherwise = Object $ Map.fromListWith __IMPOSSIBLE__
             [ (MemberIndex i c, x) | (i, (c, x)) <- zip [0..] xs, x /= Null ]
 

diff --git a/src/full/Agda/Compiler/JS/Pretty.hs b/src/full/Agda/Compiler/JS/Pretty.hs
@@ -87,7 +87,7 @@ render minify = intercalate "\n" . joinLines . map (uncurry mkIndent) . go 0
     go i (Doc s) = [(i, s)]
     go i (Beside d d') = joinBy (\(i, s) (_, s') -> [(i, s ++ s')]) (go i d) (go i d')
     go i (Above d d') = joinBy overlay (go i d) (go i d')
-    go i (Indent j d) = go (i+j) d
+    go i (Indent j d) = go (i + j) d
     go i (Enclose open close d) = go i $ Group $ Above open $ Above d close
     go i (Group d)
         | size ss < 40 = compact ss
@@ -143,7 +143,7 @@ group = Group
 
 indentBy :: Int -> Doc -> Doc
 indentBy i Empty = Empty
-indentBy i (Indent j d) = Indent (i+j) d
+indentBy i (Indent j d) = Indent (i + j) d
 indentBy i d = Indent i d
 
 enclose :: Doc -> Doc -> Doc -> Doc
@@ -261,8 +261,8 @@ instance Pretty Exp where
   pretty n (Integer x)       = "agdaRTS.primIntegerFromString(\"" <> text (show x) <> "\")"
   pretty n (Double x)        = text $ show x
   pretty (n, min, ms) (Lambda x e) =
-    mparens (x /= 1) (punctuate "," (pretties (n+x, min, ms) (map LocalId [x-1, x-2 .. 0])))
-    <+> "=>" <+> block (n+x, min, ms) e
+    mparens (x /= 1) (punctuate "," (pretties (n + x, min, ms) (map LocalId [x-1, x-2 .. 0])))
+    <+> "=>" <+> block (n + x, min, ms) e
   pretty n (Object o)        = braces $ punctuate "," $ pretties n o
   pretty n (Array es)        = brackets $ punctuate "," [pretty n c <> pretty n e | (c, e) <- es]
   pretty n (Apply f es)      = pretty n f <> parens (punctuate "," $ pretties n es)

diff --git a/src/full/Agda/Compiler/ToTreeless.hs b/src/full/Agda/Compiler/ToTreeless.hs
@@ -210,7 +210,7 @@ type CCContext = [Int]
 type CC = ReaderT CCEnv TCM
 
 shift :: Int -> CCContext -> CCContext
-shift n = map (+n)
+shift n = map (+ n)
 
 -- | Term variables are de Bruijn indices.
 lookupIndex :: Int -- ^ Case tree de bruijn index.
@@ -468,7 +468,7 @@ replaceVar x n cont = do
          (ys, _:zs) = splitAt i cxt
          -- compute the de-bruijn indexes of the newly inserted variables
          ixs = [0..(n - 1)]
-  local (\e -> e { ccCxt = upd (ccCxt e) , ccCatchAll = (+n) <$> ccCatchAll e }) $
+  local (\e -> e { ccCxt = upd (ccCxt e) , ccCatchAll = (+ n) <$> ccCatchAll e }) $
     cont
 
 

diff --git a/src/full/Agda/Compiler/Treeless/Simplify.hs b/src/full/Agda/Compiler/Treeless/Simplify.hs
@@ -218,7 +218,7 @@ simplify FunctionKit{..} = simpl
         k == j = tOp PLt v u
       | Just (PAdd, k, v) <- constArithView v,
         TApp (TPrim P64ToI) [u] <- u,
-        k >= 2^64, Just trueCon <- true = TCon trueCon
+        k >= 2 ^ 64, Just trueCon <- true = TCon trueCon
       | Just k <- intView u
       , Just j <- intView v
       , Just trueCon <- true
@@ -458,7 +458,7 @@ simplify FunctionKit{..} = simpl
           literal _ _ = False
 
           -- k + fromWord x ≤ y  if  k + 2^64 - 1 ≤ y
-          wordUpperBound (k, [Pos (TApp (TPrim P64ToI) _)]) y = go (k + 2^64 - 1, []) y
+          wordUpperBound (k, [Pos (TApp (TPrim P64ToI) _)]) y = go (k + 2 ^ 64 - 1, []) y
           wordUpperBound _ _ = False
 
           -- x ≤ k + fromWord y  if  x ≤ k

diff --git a/src/full/Agda/Interaction/Base.hs b/src/full/Agda/Interaction/Base.hs
@@ -374,7 +374,7 @@ parseToReadsPrec p i s = case runIdentity . flip runStateT s . runExceptT $ pare
 -- | Demand an exact string.
 
 exact :: String -> Parse ()
-exact s = readsToParse (show s) $ fmap ((),) . List.stripPrefix s . dropWhile (==' ')
+exact s = readsToParse (show s) $ fmap ((),) . List.stripPrefix s . dropWhile (== ' ')
 
 readParse :: Read a => Parse a
 readParse = readsToParse "read failed" $ listToMaybe . reads

diff --git a/src/full/Agda/Interaction/Highlighting/Vim.hs b/src/full/Agda/Interaction/Highlighting/Vim.hs
@@ -71,9 +71,9 @@ matches cons icons defs idefs flds iflds =
 toVim :: NamesInScope -> String
 toVim ns = unlines $ matches mcons micons mdefs midefs mflds miflds
     where
-        cons = [ x | (x, con:|_) <- Map.toList ns, isJust $ isConName $ anameKind con ]
-        defs = [ x | (x, def:|_) <- Map.toList ns, isDefName (anameKind def) ]
-        flds = [ x | (x, fld:|_) <- Map.toList ns, anameKind fld == FldName  ]
+        cons = [ x | (x, con :| _) <- Map.toList ns, isJust $ isConName $ anameKind con ]
+        defs = [ x | (x, def :| _) <- Map.toList ns, isDefName (anameKind def) ]
+        flds = [ x | (x, fld :| _) <- Map.toList ns, anameKind fld == FldName  ]
 
         mcons = map prettyShow cons
         mdefs = map prettyShow defs

diff --git a/src/full/Agda/Interaction/Library/Parse.hs b/src/full/Agda/Interaction/Library/Parse.hs
@@ -251,7 +251,7 @@ parseLine l s@(c:_)
   | isSpace c   = pure [Content l $ ltrim s]
     -- Non-indented lines are 'Header'.
   | otherwise   =
-    case break (==':') s of
+    case break (== ':') s of
       -- Headers are single words followed by a colon.
       -- Anything after the colon that is not whitespace is 'Content'.
       (h, ':' : r) ->

diff --git a/src/full/Agda/Interaction/Options/Lenses.hs b/src/full/Agda/Interaction/Options/Lenses.hs
@@ -45,7 +45,7 @@ instance LensPragmaOptions CommandLineOptions where
   lensPragmaOptions f st = f (optPragmaOptions st) <&> \ opts -> st { optPragmaOptions = opts }
 
 instance LensPragmaOptions TCState where
-  getPragmaOptions = (^.stPragmaOptions)
+  getPragmaOptions = (^. stPragmaOptions)
   setPragmaOptions = set stPragmaOptions
   lensPragmaOptions = stPragmaOptions
 

diff --git a/src/full/Agda/Syntax/Abstract.hs b/src/full/Agda/Syntax/Abstract.hs
@@ -622,10 +622,10 @@ instance LensHiding LamBinding where
   mapHiding f (DomainFull tb)  = DomainFull $ mapHiding f tb
 
 instance LensHiding TypedBinding where
-  getHiding (TBind _ _ (x :|_) _) = getHiding x   -- Slightly dubious
-  getHiding TLet{}                = mempty
-  mapHiding f (TBind r t xs e)    = TBind r t ((fmap . mapHiding) f xs) e
-  mapHiding f b@TLet{}            = b
+  getHiding (TBind _ _ (x :| _) _) = getHiding x   -- Slightly dubious
+  getHiding TLet{}                 = mempty
+  mapHiding f (TBind r t xs e)     = TBind r t ((fmap . mapHiding) f xs) e
+  mapHiding f b@TLet{}             = b
 
 instance HasRange a => HasRange (Binder' a) where
   getRange (Binder p n) = fuseRange p n

diff --git a/src/full/Agda/Syntax/Concrete.hs b/src/full/Agda/Syntax/Concrete.hs
@@ -841,13 +841,13 @@ instance LensHiding LamBinding where
 
 instance LensHiding TypedBinding where
   getHiding (TBind _ (x :| _) _) = getHiding x   -- Slightly dubious
-  getHiding TLet{}              = mempty
+  getHiding TLet{}               = mempty
   mapHiding f (TBind r xs e) = TBind r (fmap (mapHiding f) xs) e
   mapHiding f b@TLet{}       = b
 
 instance LensRelevance TypedBinding where
-  getRelevance (TBind _ (x :|_) _) = getRelevance x   -- Slightly dubious
-  getRelevance TLet{}              = unitRelevance
+  getRelevance (TBind _ (x :| _) _) = getRelevance x   -- Slightly dubious
+  getRelevance TLet{}               = unitRelevance
   mapRelevance f (TBind r xs e) = TBind r (fmap (mapRelevance f) xs) e
   mapRelevance f b@TLet{}       = b
 

diff --git a/src/full/Agda/Syntax/Concrete/Definitions.hs b/src/full/Agda/Syntax/Concrete/Definitions.hs
@@ -878,7 +878,7 @@ niceDeclarations fixs ds = do
         addType n c mc = do
           (m, checks, i) <- get
           when (isJust $ Map.lookup n m) $ lift $ declarationException $ DuplicateDefinition n
-          put (Map.insert n (c i) m, mc <> checks, i+1)
+          put (Map.insert n (c i) m, mc <> checks, i + 1)
 
         addFunType d@(FunSig _ _ _ _ _ _ tc cc n _) = do
            let checks = MutualChecks [tc] [cc] []
@@ -905,7 +905,7 @@ niceDeclarations fixs ds = do
               lift $ removeLoneSig n
               -- add the constructors to the existing ones (if any)
               let (cs', i') = case cs of
-                    Nothing        -> ((i , ds :| [] ), i+1)
+                    Nothing        -> ((i , ds :| [] ), i + 1)
                     Just (i1, ds1) -> ((i1, ds <| ds1), i)
               put (Map.insert n (InterleavedData i0 sig (Just cs')) m, checks, i')
             _ -> lift $ declarationWarning $ MissingDeclarations $ case mr of
@@ -938,7 +938,7 @@ niceDeclarations fixs ds = do
           case Map.lookup n m of
             Just (InterleavedFun i0 sig cs0) -> do
               let (cs', i') = case cs0 of
-                    Nothing        -> ((i,  (ds, cs) :| [] ), i+1)
+                    Nothing        -> ((i,  (ds, cs) :| [] ), i + 1)
                     Just (i1, cs1) -> ((i1, (ds, cs) <| cs1), i)
               put (Map.insert n (InterleavedFun i0 sig (Just cs')) m, check <> checks, i')
             _ -> __IMPOSSIBLE__ -- A FunDef always come after an existing FunSig!
@@ -959,7 +959,7 @@ niceDeclarations fixs ds = do
             -- no candidate: keep the isolated fun clause, we'll complain about it later
             [] -> do
               let check = MutualChecks [tc] [cc] []
-              put (m, check <> checks, i+1)
+              put (m, check <> checks, i + 1)
               ((i,nd) :) <$> groupByBlocks r ds
             -- exactly one candidate: attach the funclause to the definition
             [(n, fits0, rest)] -> do
@@ -969,7 +969,7 @@ niceDeclarations fixs ds = do
               case Map.lookup n m of
                 Just (InterleavedFun i0 sig cs0) -> do
                   let (cs', i') = case cs0 of
-                        Nothing        -> ((i,  (fits,cs) :| [] ), i+1)
+                        Nothing        -> ((i,  (fits,cs) :| [] ), i + 1)
                         Just (i1, cs1) -> ((i1, (fits,cs) <| cs1), i)
                   let checks' = Fold.fold checkss
                   put (Map.insert n (InterleavedFun i0 sig (Just cs')) m, checks' <> checks, i')
@@ -1001,7 +1001,7 @@ niceDeclarations fixs ds = do
             -- of each for record definitions and leaving them in place should be enough!
             _ -> oneOff $ do
               (m, c, i) <- get -- TODO: grab checks from c?
-              put (m, c, i+1)
+              put (m, c, i + 1)
               pure [(i,d)]
 
     -- Extract the name of the return type (if any) of a potential constructor.

diff --git a/src/full/Agda/Syntax/Parser.hs b/src/full/Agda/Syntax/Parser.hs
@@ -90,7 +90,7 @@ readFilePM file =
 
 wrapIOM :: (MonadError e m, MonadIO m) => (IOError -> e) -> IO a -> m a
 wrapIOM f m = do
-  a <- liftIO$ (Right <$> m) `catch` (\err -> return$ Left (err :: IOError))
+  a <- liftIO $ (Right <$> m) `catch` (\ err -> return $ Left (err :: IOError))
   case a of
     Right x  -> return x
     Left err -> throwError (f err)

diff --git a/src/full/Agda/Syntax/Scope/Monad.hs b/src/full/Agda/Syntax/Scope/Monad.hs
@@ -250,7 +250,7 @@ addVarToBind x y = modifyScope_ $ updateVarsToBind $ AssocList.insert x y
 bindVarsToBind :: ScopeM ()
 bindVarsToBind = do
   vars <- getVarsToBind
-  modifyLocalVars (vars++)
+  modifyLocalVars (vars ++)
   printLocals 10 "bound variables:"
   modifyScope_ $ setVarsToBind []
 
@@ -311,7 +311,7 @@ freshConcreteName r i s = do
   let cname = C.Name r C.NotInScope $ singleton $ Id $ stringToRawName $ s ++ show i
   resolveName (C.QName cname) >>= \case
     UnknownName -> return cname
-    _           -> freshConcreteName r (i+1) s
+    _           -> freshConcreteName r (i + 1) s
 
 ---------------------------------------------------------------------------
 -- * Resolving names
@@ -1029,7 +1029,7 @@ openModule kind mam cm dir = do
               where ks = fmap anameKind qs
         -- We report the first clashing exported identifier.
         unlessNull (filter defClash defClashes) $
-          \ ((x, q:|_) : _) -> typeError $ ClashingDefinition (C.QName x) (anameName q) Nothing
+          \ ((x, q :| _) : _) -> typeError $ ClashingDefinition (C.QName x) (anameName q) Nothing
 
         unlessNull modClashes $ \ ((_, ms) : _) -> do
           caseMaybe (List1.last2 ms) __IMPOSSIBLE__ $ \ (m0, m1) -> do

diff --git a/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs b/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs
@@ -634,7 +634,7 @@ instance ToConcrete a => ToConcrete [a] where
 
     toConcrete     = mapM toConcrete
     bindToConcrete []     ret = ret []
-    bindToConcrete (a:as) ret = bindToConcrete (a:|as) $ \ (c:|cs) -> ret (c:cs)
+    bindToConcrete (a:as) ret = bindToConcrete (a :| as) $ \ (c :| cs) -> ret (c:cs)
 
 instance ToConcrete a => ToConcrete (List1 a) where
     type ConOfAbs (List1 a) = List1 (ConOfAbs a)

diff --git a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
@@ -2805,7 +2805,7 @@ instance ToAbstract RightHandSide where
     ns <- toAbstract ns
     lvars1 <- getLocalVars
     let lv' = dropEnd (length lvars0) lvars1 ++ lv
-    let cs' = for (c:|cs) $ \ c -> setLocalVars lv' $> c
+    let cs' = for (c :| cs) $ \ c -> setLocalVars lv' $> c
     let nes = zipWith Named ns es
     return $ WithRHS' nes cs'
   -- TODO: some of these might be possible

diff --git a/src/full/Agda/Termination/SparseMatrix.hs b/src/full/Agda/Termination/SparseMatrix.hs
@@ -238,7 +238,7 @@ class Diagonal m e | m -> e where
 instance (Integral i, HasZero b) => Diagonal (Matrix i b) b where
   diagonal (Matrix (Size r c) m) =
     blowUpSparseVec zeroElement (min r c) $
-      mapMaybe (\ ((MIx i j), b) -> if i==j then Just (i,b) else Nothing) m
+      mapMaybe (\ (MIx i j, b) -> if i == j then Just (i, b) else Nothing) m
 
 -- | Transposable things.
 
@@ -400,7 +400,7 @@ instance (Ord i, PartialOrd a) => PartialOrd (Matrix i a) where
       both    = comparable
       -- The zero element of the result sparse matrix is the
       -- neutral element of the monoid.
-      trivial = (==mempty)
+      trivial = (== mempty)
 
 ------------------------------------------------------------------------
 -- Modifying matrices

diff --git a/src/full/Agda/Termination/TermCheck.hs b/src/full/Agda/Termination/TermCheck.hs
@@ -1217,7 +1217,7 @@ compareProj d d'
           case def of
             Record{ recFields = fs } -> do
               fs <- return $ map unDom fs
-              case (List.find (d==) fs, List.find (d'==) fs) of
+              case (List.find (d ==) fs, List.find (d' ==) fs) of
                 (Just i, Just i')
                   -- earlier field is smaller
                   | i < i'    -> return Order.lt

diff --git a/src/full/Agda/TypeChecking/Conversion.hs b/src/full/Agda/TypeChecking/Conversion.hs
@@ -1414,7 +1414,7 @@ leqLevel a b = catchConstraint (LevelCmp CmpLeq a b) $ do
           | all neutralOrClosed bs , levelLowerBound a > levelLowerBound b -> notok
 
         -- ⊔ as ≤ single
-        (as@(_:|_:_), b :| []) ->
+        (as@(_ :| _ : _), b :| []) ->
           forM_ as $ \ a' -> leqLevel (unSingleLevel $ ignoreBlocking <$> a')
                                       (unSingleLevel $ ignoreBlocking <$> b)
 
@@ -1586,9 +1586,9 @@ equalLevel a b = do
         (_ , SingleClosed n :| []) | n < levelLowerBound a -> notok
 
         -- 0 == a ⊔ b
-        (SingleClosed 0 :| [] , bs@(_:|_:_)) ->
+        (SingleClosed 0 :| [] , bs@(_ :| _ : _)) ->
           forM_ bs $ \ b' ->  equalLevel (ClosedLevel 0) (unSingleLevel $ ignoreBlocking <$> b')
-        (as@(_:|_:_) , SingleClosed 0 :| []) ->
+        (as@(_ :| _ : _) , SingleClosed 0 :| []) ->
           forM_ as $ \ a' -> equalLevel (unSingleLevel $ ignoreBlocking <$> a') (ClosedLevel 0)
 
         -- meta == any

diff --git a/src/full/Agda/TypeChecking/Coverage.hs b/src/full/Agda/TypeChecking/Coverage.hs
@@ -630,13 +630,13 @@ cover f cs sc@(SClause tel ps _ _ target) = updateRelevance $ do
     addEtaSplits :: Int -> [NamedArg SplitPattern] -> SplitTree -> SplitTree
     addEtaSplits k []     t = t
     addEtaSplits k (p:ps) t = case namedArg p of
-      VarP  _ _     -> addEtaSplits (k+1) ps t
-      DotP  _ _     -> addEtaSplits (k+1) ps t
+      VarP  _ _     -> addEtaSplits (k + 1) ps t
+      DotP  _ _     -> addEtaSplits (k + 1) ps t
       ConP c cpi qs -> SplitAt (p $> k) LazySplit [(SplitCon (conName c) , addEtaSplits k (qs ++ ps) t)]
       LitP{}        -> __IMPOSSIBLE__
       ProjP{}       -> __IMPOSSIBLE__
       DefP{}        -> __IMPOSSIBLE__ -- Andrea: maybe?
-      IApplyP{}     -> addEtaSplits (k+1) ps t
+      IApplyP{}     -> addEtaSplits (k + 1) ps t
 
     etaRecordSplits :: Int -> [NamedArg SplitPattern] -> (SplitTag,SplitClause)
                     -> SplitTree -> (SplitTag,SplitTree)