From 7b385b480c4bfc32d9468e4750648e35e1960be8 Mon Sep 17 00:00:00 2001 From: Andreas Abel Date: Mon, 17 May 2021 08:55:48 +0200 Subject: [PATCH] [ #4547 ] use List1/2 in Concrete.Definition.Errors.ShadowingInTelescope --- .../Agda/Interaction/Highlighting/Generate.hs | 6 ++-- .../Syntax/Concrete/Definitions/Errors.hs | 5 ++-- src/full/Agda/Syntax/Scope/Monad.hs | 19 ++++++------ .../Serialise/Instances/Common.hs | 6 ++++ src/full/Agda/Utils/List2.hs | 29 ++++++++++++++----- 5 files changed, 44 insertions(+), 21 deletions(-) diff --git a/src/full/Agda/Interaction/Highlighting/Generate.hs b/src/full/Agda/Interaction/Highlighting/Generate.hs index d73f3f1783b..2177a51d73a 100644 --- a/src/full/Agda/Interaction/Highlighting/Generate.hs +++ b/src/full/Agda/Interaction/Highlighting/Generate.hs @@ -71,6 +71,8 @@ import Agda.Syntax.Abstract.Views ( KName, declaredNames ) import Agda.Utils.FileName import Agda.Utils.List ( caseList, initWithDefault, last1 ) +import Agda.Utils.List2 ( List2 ) +import qualified Agda.Utils.List2 as List2 import Agda.Utils.Maybe import qualified Agda.Utils.Maybe.Strict as Strict import Agda.Utils.Null @@ -548,11 +550,11 @@ coverageErrorHighlighting :: Range -> HighlightingInfoBuilder coverageErrorHighlighting r = H.singleton (rToR $ P.continuousPerLine r) m where m = parserBased { otherAspects = Set.singleton CoverageProblem } -shadowingTelHighlighting :: [Range] -> HighlightingInfoBuilder +shadowingTelHighlighting :: List2 Range -> HighlightingInfoBuilder shadowingTelHighlighting = -- we do not want to highlight the one variable in scope so we take -- the @init@ segment of the ranges in question - foldMap (\r -> H.singleton (rToR $ P.continuous r) m) . initWithDefault __IMPOSSIBLE__ + foldMap (\r -> H.singleton (rToR $ P.continuous r) m) . List2.init where m = parserBased { otherAspects = Set.singleton H.ShadowingInTelescope } diff --git a/src/full/Agda/Syntax/Concrete/Definitions/Errors.hs b/src/full/Agda/Syntax/Concrete/Definitions/Errors.hs index 337fff9cbf9..bf6b01dd705 100644 --- a/src/full/Agda/Syntax/Concrete/Definitions/Errors.hs +++ b/src/full/Agda/Syntax/Concrete/Definitions/Errors.hs @@ -15,6 +15,7 @@ import Agda.Interaction.Options.Warnings import Agda.Utils.CallStack ( CallStack ) import Agda.Utils.List1 (List1, pattern (:|)) +import Agda.Utils.List2 (List2, pattern List2) import qualified Agda.Utils.List1 as List1 import Agda.Utils.Pretty @@ -102,7 +103,7 @@ data DeclarationWarning' -- by @{-\# TERMINATING \#-}@ and @{-\# NON_TERMINATING \#-}@. | PragmaCompiled Range -- ^ @COMPILE@ pragmas are not allowed in safe mode - | ShadowingInTelescope [(Name, [Range])] + | ShadowingInTelescope (List1 (Name, List2 Range)) | UnknownFixityInMixfixDecl [Name] | UnknownNamesInFixityDecl [Name] | UnknownNamesInPolarityPragmas [Name] @@ -357,7 +358,7 @@ instance Pretty DeclarationWarning' where pwords "public does not have any effect in a private block." pretty (ShadowingInTelescope nrs) = fsep $ pwords "Shadowing in telescope, repeated variable names:" - ++ punctuate comma (map (pretty . fst) nrs) + ++ punctuate comma (fmap (pretty . fst) nrs) instance NFData DeclarationWarning instance NFData DeclarationWarning' diff --git a/src/full/Agda/Syntax/Scope/Monad.hs b/src/full/Agda/Syntax/Scope/Monad.hs index ef8bd5728ba..a34a8b337ea 100644 --- a/src/full/Agda/Syntax/Scope/Monad.hs +++ b/src/full/Agda/Syntax/Scope/Monad.hs @@ -53,7 +53,9 @@ import Agda.Utils.Functor import Agda.Utils.Lens import Agda.Utils.List import Agda.Utils.List1 (List1, pattern (:|), nonEmpty) +import Agda.Utils.List2 (List2(List2)) import qualified Agda.Utils.List1 as List1 +import qualified Agda.Utils.List2 as List2 import Agda.Utils.Maybe import Agda.Utils.Monad import Agda.Utils.Null @@ -225,17 +227,16 @@ checkNoShadowing old new = do -- Filter out the underscores. let newNames = filter (not . isNoName) $ AssocList.keys diff -- Associate each name to its occurrences. - let nameOccs = Map.toList $ Map.fromListWith (++) $ map pairWithRange newNames + let nameOccs1 :: [(C.Name, List1 Range)] + nameOccs1 = Map.toList $ Map.fromListWith (<>) $ map pairWithRange newNames -- Warn if we have two or more occurrences of the same name. - unlessNull (filter (atLeastTwo . snd) nameOccs) $ \ conflicts -> do - scopeWarning $ ShadowingInTelescope conflicts + let nameOccs2 :: [(C.Name, List2 Range)] + nameOccs2 = mapMaybe (traverseF List2.fromList1Maybe) nameOccs1 + caseList nameOccs2 (return ()) $ \ c conflicts -> do + scopeWarning $ ShadowingInTelescope $ c :| conflicts where - pairWithRange :: C.Name -> (C.Name, [Range]) - pairWithRange n = (n, [getRange n]) - - atLeastTwo :: [a] -> Bool - atLeastTwo (_ : _ : _) = True - atLeastTwo _ = False + pairWithRange :: C.Name -> (C.Name, List1 Range) + pairWithRange n = (n, singleton $ getRange n) getVarsToBind :: ScopeM LocalVars getVarsToBind = useScope scopeVarsToBind diff --git a/src/full/Agda/TypeChecking/Serialise/Instances/Common.hs b/src/full/Agda/TypeChecking/Serialise/Instances/Common.hs index 38fd5dfa421..5dc73b639bf 100644 --- a/src/full/Agda/TypeChecking/Serialise/Instances/Common.hs +++ b/src/full/Agda/TypeChecking/Serialise/Instances/Common.hs @@ -48,6 +48,8 @@ import Agda.Utils.BiMap (BiMap) import qualified Agda.Utils.BiMap as BiMap import qualified Agda.Utils.Empty as Empty import Agda.Utils.FileName +import Agda.Utils.List2 (List2(List2)) +import qualified Agda.Utils.List2 as List2 import Agda.Utils.Maybe import qualified Agda.Utils.Maybe.Strict as Strict import Agda.Utils.Trie (Trie(..)) @@ -234,6 +236,10 @@ instance EmbPrj a => EmbPrj (NonEmpty a) where icod_ = icod_ . NonEmpty.toList value = maybe malformed return . nonEmpty <=< value +instance EmbPrj a => EmbPrj (List2 a) where + icod_ = icod_ . List2.toList + value = maybe malformed return . List2.fromListMaybe <=< value + instance (EmbPrj k, EmbPrj v, EmbPrj (BiMap.Tag v)) => EmbPrj (BiMap k v) where icod_ m = icode (BiMap.toDistinctAscendingLists m) diff --git a/src/full/Agda/Utils/List2.hs b/src/full/Agda/Utils/List2.hs index fbb81f7b695..6adec9b7c4f 100644 --- a/src/full/Agda/Utils/List2.hs +++ b/src/full/Agda/Utils/List2.hs @@ -13,6 +13,7 @@ module Agda.Utils.List2 ) where import Control.DeepSeq +import Control.Monad ( (<=<) ) import Data.Data ( Data ) import qualified Data.List as List @@ -21,6 +22,7 @@ import GHC.Exts ( IsList(..) ) import qualified GHC.Exts as Reexport ( toList ) import Agda.Utils.List1 ( List1, pattern (:|) ) +import qualified Agda.Utils.List1 as List1 import Agda.Utils.Impossible @@ -28,22 +30,32 @@ import Agda.Utils.Impossible data List2 a = List2 a a [a] deriving (Eq, Ord, Show, Data, Functor, Foldable, Traversable) --- | Safe. +-- | Safe. O(1). head :: List2 a -> a head (List2 a _ _) = a --- | Safe. -tail :: List2 a -> [a] -tail (List2 a b cs) = b : cs +-- | Safe. O(1). +tail :: List2 a -> List1 a +tail (List2 a b cs) = b :| cs --- | Safe. -tail1 :: List2 a -> List1 a -tail1 (List2 a b cs) = b :| cs +-- | Safe. O(n). +init :: List2 a -> List1 a +init (List2 a b cs) = a :| List1.init (b :| cs) + +-- | Safe. O(1). +fromListMaybe :: [a] -> Maybe (List2 a) +fromListMaybe = fromList1Maybe <=< List1.nonEmpty + +-- | Safe. O(1). +fromList1Maybe :: List1 a -> Maybe (List2 a) +fromList1Maybe = \case + (a :| b : cs) -> Just (List2 a b cs) + _ -> Nothing instance IsList (List2 a) where type Item (List2 a) = a - -- | Unsafe! + -- | Unsafe! O(1). fromList :: [a] -> List2 a fromList (a : b : cs) = List2 a b cs fromList _ = __IMPOSSIBLE__ @@ -51,6 +63,7 @@ instance IsList (List2 a) where toList :: List2 a -> [a] toList (List2 a b cs) = a : b : cs +-- | Safe. O(1). toList1 :: List2 a -> List1 a toList1 (List2 a b cs) = a :| b : cs