[ change ] Format all code

agda · Dec 6, 2024 · 33a62df · 33a62df
1 parent e9651ad
commit 33a62df
Show file tree

Hide file tree

Showing 21 changed files with 591 additions and 558 deletions.
diff --git a/src/Agda/Convert.hs b/src/Agda/Convert.hs
@@ -2,8 +2,6 @@
 
 module Agda.Convert where
 
-import Render ( Block(..), Inlines, renderATop, Render(..) )
-
 import Agda.IR (FromAgda (..))
 import qualified Agda.IR as IR
 import Agda.Interaction.Base
@@ -14,6 +12,9 @@ import Agda.Interaction.Highlighting.Common (chooseHighlightingMethod, toAtoms)
 import Agda.Interaction.Highlighting.Precise (Aspects (..), DefinitionSite (..), HighlightingInfo, TokenBased (..))
 import qualified Agda.Interaction.Highlighting.Range as Highlighting
 import Agda.Interaction.InteractionTop (localStateCommandM)
+#if MIN_VERSION_Agda(2,7,0)
+import Agda.Interaction.Output ( OutputConstraint )
+#endif
 import Agda.Interaction.Response as R
 import Agda.Syntax.Abstract as A
 import Agda.Syntax.Abstract.Pretty (prettyATop)
@@ -22,7 +23,7 @@ import Agda.Syntax.Concrete as C
 import Agda.Syntax.Internal (alwaysUnblock)
 import Agda.Syntax.Position (HasRange (getRange), Range, noRange)
 import Agda.Syntax.Scope.Base
-import Agda.TypeChecking.Errors (getAllWarningsOfTCErr, prettyError, explainWhyInScope)
+import Agda.TypeChecking.Errors (explainWhyInScope, getAllWarningsOfTCErr, prettyError)
 import Agda.TypeChecking.Monad hiding (Function)
 import Agda.TypeChecking.Monad.MetaVars (withInteractionId)
 import Agda.TypeChecking.Pretty (prettyTCM)
@@ -35,14 +36,7 @@ import Agda.Utils.IO.TempFile (writeToTempFile)
 import Agda.Utils.Impossible (__IMPOSSIBLE__)
 import Agda.Utils.Maybe (catMaybes)
 import Agda.Utils.Null (empty)
-#if MIN_VERSION_Agda(2,6,4)
-import Agda.Syntax.Common.Pretty hiding (render)
--- import Prettyprinter hiding (Doc)
-import qualified Prettyprinter
-#else
-import Agda.Utils.Pretty hiding (render)
-#endif
-import Agda.Utils.RangeMap ( IsBasicRangeMap(toList) )
+import Agda.Utils.RangeMap (IsBasicRangeMap (toList))
 import Agda.Utils.String (delimiter)
 import Agda.Utils.Time (CPUTime)
 import Agda.VersionCommit (versionWithCommitInfo)
@@ -53,13 +47,17 @@ import qualified Data.ByteString.Lazy.Char8 as BS8
 import qualified Data.List as List
 import qualified Data.Map as Map
 import Data.String (IsString)
+import Render (Block (..), Inlines, Render (..), renderATop)
 import qualified Render
 
-#if MIN_VERSION_Agda(2,7,0)
-import Agda.Interaction.Output ( OutputConstraint )
+#if MIN_VERSION_Agda(2,6,4)
+import Agda.Syntax.Common.Pretty hiding (render)
+import qualified Prettyprinter
+#else
+import Agda.Utils.Pretty hiding (render)
 #endif
 
-responseAbbr :: IsString a => Response -> a
+responseAbbr :: (IsString a) => Response -> a
 responseAbbr res = case res of
   Resp_HighlightingInfo {} -> "Resp_HighlightingInfo"
   Resp_Status {} -> "Resp_Status"
@@ -273,7 +271,8 @@ fromDisplayInfo = \case
       return (prettyShow x, ":" <+> doc)
     let doc =
           "Definitions about"
-            <+> text (List.intercalate ", " $ words names) $$ nest 2 (align 10 hitDocs)
+            <+> text (List.intercalate ", " $ words names)
+            $$ nest 2 (align 10 hitDocs)
     return $ IR.DisplayInfoGeneric "Search About" [Unlabeled (Render.text $ show doc) Nothing Nothing]
   Info_WhyInScope why -> do
     doc <- explainWhyInScope why
@@ -331,18 +330,19 @@ lispifyGoalSpecificDisplayInfo ii kind = localTCState $
               if null boundaries
                 then []
                 else
-                  Header "Boundary" :
-                  fmap (\boundary -> Unlabeled (render boundary) (Just $ show $ pretty boundary) Nothing) boundaries
+                  Header "Boundary"
+                    : fmap (\boundary -> Unlabeled (render boundary) (Just $ show $ pretty boundary) Nothing) boundaries
         contextSect <- reverse . concat <$> mapM (renderResponseContext ii) resCtxs
         let constraintSect =
-                if null constraints
-                  then []
-                  else
-                    Header "Constraints" :
-                    fmap (\constraint -> Unlabeled (render constraint) (Just $ show $ pretty constraint) Nothing) constraints
+              if null constraints
+                then []
+                else
+                  Header "Constraints"
+                    : fmap (\constraint -> Unlabeled (render constraint) (Just $ show $ pretty constraint) Nothing) constraints
 
         return $
-          IR.DisplayInfoGeneric "Goal type etc" $ goalSect ++ auxSect ++ boundarySect ++ contextSect ++ constraintSect
+          IR.DisplayInfoGeneric "Goal type etc" $
+            goalSect ++ auxSect ++ boundarySect ++ contextSect ++ constraintSect
       Goal_CurrentGoal norm -> do
         (rendered, raw) <- prettyTypeOfMeta norm ii
         return $ IR.DisplayInfoCurrentGoal (Unlabeled rendered (Just raw) Nothing)
@@ -443,8 +443,7 @@ renderResponseContext ii (ResponseContextEntry n x (Arg ai expr) letv nis) = wit
   modality <- asksTC getModality
 #endif
   do
-    let
-        rawCtxName :: String
+    let rawCtxName :: String
         rawCtxName
           | n == x = prettyShow x
           | isInScope n == InScope = prettyShow n ++ " = " ++ prettyShow x
@@ -468,7 +467,7 @@ renderResponseContext ii (ResponseContextEntry n x (Arg ai expr) letv nis) = wit
           where
             c = render (getCohesion ai)
 
-        extras :: IsString a => [a]
+        extras :: (IsString a) => [a]
         extras =
           concat
             [ ["not in scope" | isInScope nis == C.NotInScope],
@@ -498,7 +497,7 @@ renderResponseContext ii (ResponseContextEntry n x (Arg ai expr) letv nis) = wit
     -- rendered
     renderedExpr <- renderATop expr
     let renderedType = (renderedCtxName <> renderedAttribute) Render.<+> ":" Render.<+> renderedExpr Render.<+> parenSep2 extras2
-      -- (Render.fsep $ Render.punctuate "," extras)
+    -- (Render.fsep $ Render.punctuate "," extras)
 
     -- result
     let typeItem = Unlabeled renderedType (Just rawType) Nothing
@@ -526,7 +525,6 @@ renderResponseContext ii (ResponseContextEntry n x (Arg ai expr) letv nis) = wit
       | null docs = mempty
       | otherwise = (" " Render.<+>) $ Render.parens $ Render.fsep $ Render.punctuate "," docs
 
-
 -- | Pretty-prints the type of the meta-variable.
 prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM (Inlines, String)
 prettyTypeOfMeta norm ii = do

diff --git a/src/Agda/IR.hs b/src/Agda/IR.hs
@@ -20,6 +20,7 @@ class FromAgdaTCM a b | a -> b where
   fromAgdaTCM :: a -> TCM b
 
 --------------------------------------------------------------------------------
+
 -- | IR for IOCTM
 data Response
   = -- non-last responses

diff --git a/src/Agda/Parser.hs b/src/Agda/Parser.hs
@@ -6,17 +6,16 @@ module Agda.Parser where
 
 import Agda.Syntax.Parser (parseFile, runPMIO, tokensParser)
 import Agda.Syntax.Parser.Tokens (Token)
-import Agda.Syntax.Position (Position' (posPos), PositionWithoutFile, Range, getRange, rEnd', rStart')
-import Agda.Syntax.Position (RangeFile(RangeFile))
+import Agda.Syntax.Position (Position' (posPos), PositionWithoutFile, Range, RangeFile (RangeFile), getRange, rEnd', rStart')
 import Agda.Utils.FileName (mkAbsolute)
-import Monad ( ServerM )
 import Control.Monad.State
 import Data.List (find)
 import Data.Maybe (fromMaybe)
 import Data.Text (Text, unpack)
 import qualified Data.Text as Text
+import qualified Language.LSP.Protocol.Types as LSP
 import Language.LSP.Server (LspM)
-import qualified Language.LSP.Protocol.Types   as LSP
+import Monad (ServerM)
 import Options (Config)
 
 --------------------------------------------------------------------------------

diff --git a/src/Agda/Position.hs b/src/Agda/Position.hs
@@ -1,59 +1,66 @@
 {-# LANGUAGE CPP #-}
 
 module Agda.Position
-  ( ToOffset(..)
-  , makeToOffset
-  , toOffset
-  , FromOffset(..)
-  , makeFromOffset
-  , fromOffset
-  , toAgdaPositionWithoutFile
-  , toAgdaRange
-  , prettyPositionWithoutFile
-  -- , toLSPRange
-  -- , toLSPPosition
-  ) where
-
-import           Agda.Syntax.Position
-import           Agda.Utils.FileName            ( AbsolutePath(AbsolutePath) )
-import           Data.IntMap                    ( IntMap )
-import qualified Data.IntMap                   as IntMap
-import qualified Data.Sequence                 as Seq
-import qualified Data.Strict.Maybe             as Strict
-import           Data.Text                      ( Text )
-import qualified Data.Text                     as Text
-import qualified Language.LSP.Protocol.Types   as LSP
+  ( ToOffset (..),
+    makeToOffset,
+    toOffset,
+    FromOffset (..),
+    makeFromOffset,
+    fromOffset,
+    toAgdaPositionWithoutFile,
+    toAgdaRange,
+    prettyPositionWithoutFile,
+    -- , toLSPRange
+    -- , toLSPPosition
+  )
+where
+
+import Agda.Syntax.Position
+import Agda.Utils.FileName (AbsolutePath (AbsolutePath))
+import Data.IntMap (IntMap)
+import qualified Data.IntMap as IntMap
+import qualified Data.Sequence as Seq
+import qualified Data.Strict.Maybe as Strict
+import Data.Text (Text)
+import qualified Data.Text as Text
+import qualified Language.LSP.Protocol.Types as LSP
 
 -- Note:  LSP srclocs are 0-base
 --        Agda srclocs are 1-base
 
 --------------------------------------------------------------------------------
+
 -- | LSP source locations => Agda source locations
 
 -- | LSP Range -> Agda Range
 toAgdaRange :: ToOffset -> Text -> LSP.Range -> Range
-toAgdaRange table path (LSP.Range start end) = Range
-  (Strict.Just $ mkRangeFile $ AbsolutePath path)
-  (Seq.singleton interval)
- where
-  interval :: IntervalWithoutFile
-  interval = Interval (toAgdaPositionWithoutFile table start)
-                      (toAgdaPositionWithoutFile table end)
-  mkRangeFile path = RangeFile path Nothing
+toAgdaRange table path (LSP.Range start end) =
+  Range
+    (Strict.Just $ mkRangeFile $ AbsolutePath path)
+    (Seq.singleton interval)
+  where
+    interval :: IntervalWithoutFile
+    interval =
+      Interval
+        (toAgdaPositionWithoutFile table start)
+        (toAgdaPositionWithoutFile table end)
+    mkRangeFile path = RangeFile path Nothing
 
 -- | LSP Position -> Agda PositionWithoutFile
 toAgdaPositionWithoutFile :: ToOffset -> LSP.Position -> PositionWithoutFile
-toAgdaPositionWithoutFile table (LSP.Position line col) = Pn
-  ()
-  (fromIntegral (toOffset table (fromIntegral line, fromIntegral col)) + 1)
-  (fromIntegral line + 1)
-  (fromIntegral col + 1)
+toAgdaPositionWithoutFile table (LSP.Position line col) =
+  Pn
+    ()
+    (fromIntegral (toOffset table (fromIntegral line, fromIntegral col)) + 1)
+    (fromIntegral line + 1)
+    (fromIntegral col + 1)
 
 prettyPositionWithoutFile :: PositionWithoutFile -> String
 prettyPositionWithoutFile pos@(Pn () offset _line _col) =
   "[" <> show pos <> "-" <> show offset <> "]"
 
 --------------------------------------------------------------------------------
+
 -- | Positon => Offset convertion
 
 -- Keeps record of offsets of every line break ("\n", "\r" and "\r\n")
@@ -63,38 +70,39 @@ prettyPositionWithoutFile pos@(Pn () offset _line _col) =
 --  >def123\r\n          (2, 11)
 --  >ghi\r               (3, 15)
 --
-newtype ToOffset = ToOffset { unToOffset :: IntMap Int }
+newtype ToOffset = ToOffset {unToOffset :: IntMap Int}
 
 data Accum = Accum
-  { accumPreviousChar  :: Maybe Char
-  , accumCurrentOffset :: Int
-  , accumCurrentLine   :: Int
-  , accumResult        :: IntMap Int
+  { accumPreviousChar :: Maybe Char,
+    accumCurrentOffset :: Int,
+    accumCurrentLine :: Int,
+    accumResult :: IntMap Int
   }
 
 -- | Return a list of offsets of linebreaks ("\n", "\r" or "\r\n")
 makeToOffset :: Text -> ToOffset
 makeToOffset = ToOffset . accumResult . Text.foldl' go initAccum
- where
-  initAccum :: Accum
-  initAccum = Accum Nothing 0 0 IntMap.empty
-
-  go :: Accum -> Char -> Accum
-  go (Accum (Just '\r') n l table) '\n' =
-    Accum (Just '\n') (1 + n) l (IntMap.updateMax (Just . succ) table)
-  go (Accum previous n l table) '\n' =
-    Accum (Just '\n') (1 + n) (1 + l) (IntMap.insert (1 + l) (1 + n) table)
-  go (Accum previous n l table) '\r' =
-    Accum (Just '\r') (1 + n) (1 + l) (IntMap.insert (1 + l) (1 + n) table)
-  go (Accum previous n l table) char = Accum (Just char) (1 + n) l table
+  where
+    initAccum :: Accum
+    initAccum = Accum Nothing 0 0 IntMap.empty
+
+    go :: Accum -> Char -> Accum
+    go (Accum (Just '\r') n l table) '\n' =
+      Accum (Just '\n') (1 + n) l (IntMap.updateMax (Just . succ) table)
+    go (Accum previous n l table) '\n' =
+      Accum (Just '\n') (1 + n) (1 + l) (IntMap.insert (1 + l) (1 + n) table)
+    go (Accum previous n l table) '\r' =
+      Accum (Just '\r') (1 + n) (1 + l) (IntMap.insert (1 + l) (1 + n) table)
+    go (Accum previous n l table) char = Accum (Just char) (1 + n) l table
 
 -- | (line, col) => offset (zero-based)
 toOffset :: ToOffset -> (Int, Int) -> Int
 toOffset (ToOffset table) (line, col) = case IntMap.lookup line table of
-  Nothing     -> col
+  Nothing -> col
   Just offset -> offset + col
 
 --------------------------------------------------------------------------------
+
 -- | Offset => Position convertion
 
 -- An IntMap for speeding up Offset => Position convertion
@@ -105,29 +113,32 @@ toOffset (ToOffset table) (line, col) = case IntMap.lookup line table of
 --  >def123\r\n          (11, 2)
 --  >ghi\r               (15, 3)
 --
-newtype FromOffset = FromOffset { unFromOffset :: IntMap Int }
+newtype FromOffset = FromOffset {unFromOffset :: IntMap Int}
 
 fromOffset :: FromOffset -> Int -> (Int, Int)
 fromOffset (FromOffset table) offset = case IntMap.lookupLE offset table of
-  Nothing                          -> (0, offset) -- no previous lines
+  Nothing -> (0, offset) -- no previous lines
   Just (offsetOfFirstChar, lineNo) -> (lineNo, offset - offsetOfFirstChar)
 
 makeFromOffset :: Text -> FromOffset
-makeFromOffset = FromOffset . accumResult . Text.foldl'
-  go
-  (Accum Nothing 0 0 IntMap.empty)
- where
-  go :: Accum -> Char -> Accum
-  -- encountered a "\r\n", update the latest entry
-  go (Accum (Just '\r') n l table) '\n' = case IntMap.deleteFindMax table of
-    ((offset, lineNo), table') ->
-      Accum (Just '\n') (1 + n) l (IntMap.insert (1 + offset) lineNo table')
-  -- encountered a line break, add a new entry
-  go (Accum previous n l table) '\n' =
-    Accum (Just '\n') (1 + n) (1 + l) (IntMap.insert (1 + n) (1 + l) table)
-  go (Accum previous n l table) '\r' =
-    Accum (Just '\r') (1 + n) (1 + l) (IntMap.insert (1 + n) (1 + l) table)
-  go (Accum previous n l table) char = Accum (Just char) (1 + n) l table
+makeFromOffset =
+  FromOffset
+    . accumResult
+    . Text.foldl'
+      go
+      (Accum Nothing 0 0 IntMap.empty)
+  where
+    go :: Accum -> Char -> Accum
+    -- encountered a "\r\n", update the latest entry
+    go (Accum (Just '\r') n l table) '\n' = case IntMap.deleteFindMax table of
+      ((offset, lineNo), table') ->
+        Accum (Just '\n') (1 + n) l (IntMap.insert (1 + offset) lineNo table')
+    -- encountered a line break, add a new entry
+    go (Accum previous n l table) '\n' =
+      Accum (Just '\n') (1 + n) (1 + l) (IntMap.insert (1 + n) (1 + l) table)
+    go (Accum previous n l table) '\r' =
+      Accum (Just '\r') (1 + n) (1 + l) (IntMap.insert (1 + n) (1 + l) table)
+    go (Accum previous n l table) char = Accum (Just char) (1 + n) l table
 
 -- --------------------------------------------------------------------------------
 -- -- | Agda Highlighting Range -> Agda Range