{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.Syntax.Scope.Flat
( FlatScope
, flattenScope
, getDefinedNames
, localNames
) where
import Data.Bifunctor
import Data.Either (partitionEithers)
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Agda.Syntax.Abstract.Name as A
import Agda.Syntax.Concrete
import Agda.Syntax.Notation
import Agda.Syntax.Scope.Base
import Agda.Syntax.Scope.Monad
import Agda.TypeChecking.Monad.Debug
import Agda.Utils.Impossible
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.List1 (List1)
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Syntax.Common.Pretty
newtype FlatScope = Flat (Map QName (List1 AbstractName))
deriving Int -> FlatScope -> Doc
[FlatScope] -> Doc
FlatScope -> Doc
forall a.
(a -> Doc) -> (Int -> a -> Doc) -> ([a] -> Doc) -> Pretty a
prettyList :: [FlatScope] -> Doc
$cprettyList :: [FlatScope] -> Doc
prettyPrec :: Int -> FlatScope -> Doc
$cprettyPrec :: Int -> FlatScope -> Doc
pretty :: FlatScope -> Doc
$cpretty :: FlatScope -> Doc
Pretty
flattenScope :: [[Name]] -> ScopeInfo -> FlatScope
flattenScope :: [[Name]] -> ScopeInfo -> FlatScope
flattenScope [[Name]]
ms ScopeInfo
scope =
Map QName (List1 AbstractName) -> FlatScope
Flat forall a b. (a -> b) -> a -> b
$
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith forall a. Semigroup a => a -> a -> a
(<>)
([[Name]]
-> (forall a. InScope a => Scope -> ThingsInScope a)
-> Scope
-> Map QName (List1 AbstractName)
build [[Name]]
ms forall a. InScope a => Scope -> ThingsInScope a
allNamesInScope Scope
root)
Map QName (List1 AbstractName)
imported
where
current :: Scope
current = ModuleName -> Scope
moduleScope forall a b. (a -> b) -> a -> b
$ ScopeInfo
scope forall o i. o -> Lens' o i -> i
^. Lens' ScopeInfo ModuleName
scopeCurrent
root :: Scope
root = [Scope] -> Scope
mergeScopes forall a b. (a -> b) -> a -> b
$ Scope
current forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map ModuleName -> Scope
moduleScope (Scope -> [ModuleName]
scopeParents Scope
current)
imported :: Map QName (List1 AbstractName)
imported = forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith forall a. Semigroup a => a -> a -> a
(<>)
[ forall {a}. QName -> Map QName a -> Map QName a
qual QName
c ([[Name]]
-> (forall a. InScope a => Scope -> ThingsInScope a)
-> Scope
-> Map QName (List1 AbstractName)
build [[Name]]
ms' forall a. InScope a => Scope -> ThingsInScope a
exportedNamesInScope forall a b. (a -> b) -> a -> b
$ ModuleName -> Scope
moduleScope ModuleName
a)
| (QName
c, ModuleName
a) <- forall k a. Map k a -> [(k, a)]
Map.toList forall a b. (a -> b) -> a -> b
$ Scope -> Map QName ModuleName
scopeImports Scope
root
, let
ms' :: [[Name]]
ms' = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (forall a. Eq a => [a] -> [a] -> Maybe [a]
List.stripPrefix forall a b. (a -> b) -> a -> b
$ forall l. IsList l => l -> [Item l]
List1.toList forall a b. (a -> b) -> a -> b
$ QName -> List1 Name
qnameParts QName
c) [[Name]]
ms
, Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Name]]
ms' ]
qual :: QName -> Map QName a -> Map QName a
qual QName
c = forall k1 k2 a. (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeysMonotonic (QName -> QName -> QName
q QName
c)
where
q :: QName -> QName -> QName
q (QName Name
x) = Name -> QName -> QName
Qual Name
x
q (Qual Name
m QName
x) = Name -> QName -> QName
Qual Name
m forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> QName -> QName
q QName
x
build :: [[Name]] -> (forall a. InScope a => Scope -> ThingsInScope a) -> Scope -> Map QName (List1 AbstractName)
build :: [[Name]]
-> (forall a. InScope a => Scope -> ThingsInScope a)
-> Scope
-> Map QName (List1 AbstractName)
build [[Name]]
ms forall a. InScope a => Scope -> ThingsInScope a
getNames Scope
s = forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith forall a. Semigroup a => a -> a -> a
(<>) forall a b. (a -> b) -> a -> b
$
forall k1 k2 a. (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeysMonotonic Name -> QName
QName (forall a. InScope a => Scope -> ThingsInScope a
getNames Scope
s) forall a. a -> [a] -> [a]
:
[ forall k1 k2 a. (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeysMonotonic (\ QName
y -> Name -> QName -> QName
Qual Name
x QName
y) forall a b. (a -> b) -> a -> b
$
[[Name]]
-> (forall a. InScope a => Scope -> ThingsInScope a)
-> Scope
-> Map QName (List1 AbstractName)
build [[Name]]
ms' forall a. InScope a => Scope -> ThingsInScope a
exportedNamesInScope forall a b. (a -> b) -> a -> b
$ ModuleName -> Scope
moduleScope ModuleName
m
| (Name
x, List1 AbstractModule
mods) <- forall k a. Map k a -> [(k, a)]
Map.toList (forall a. InScope a => Scope -> ThingsInScope a
getNames Scope
s)
, let ms' :: [[Name]]
ms' = [ [Name]
tl | Name
hd:[Name]
tl <- [[Name]]
ms, Name
hd forall a. Eq a => a -> a -> Bool
== Name
x ]
, Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Name]]
ms'
, AbsModule ModuleName
m WhyInScope
_ <- forall l. IsList l => l -> [Item l]
List1.toList List1 AbstractModule
mods
]
moduleScope :: A.ModuleName -> Scope
moduleScope :: ModuleName -> Scope
moduleScope ModuleName
m = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ModuleName
m forall a b. (a -> b) -> a -> b
$ ScopeInfo
scope forall o i. o -> Lens' o i -> i
^. Lens' ScopeInfo (Map ModuleName Scope)
scopeModules
getDefinedNames :: KindsOfNames -> FlatScope -> [List1 NewNotation]
getDefinedNames :: KindsOfNames -> FlatScope -> [List1 NewNotation]
getDefinedNames KindsOfNames
kinds (Flat Map QName (List1 AbstractName)
names) =
[ List1 NewNotation -> List1 NewNotation
mergeNotations forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (QName -> Name -> NewNotation
namesToNotation QName
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
A.qnameName forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> QName
anameName) List1 AbstractName
ds
| (QName
x, List1 AbstractName
ds) <- forall k a. Map k a -> [(k, a)]
Map.toList Map QName (List1 AbstractName)
names
, forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((KindOfName -> KindsOfNames -> Bool
`elemKindsOfNames` KindsOfNames
kinds) forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> KindOfName
anameKind) List1 AbstractName
ds
]
localNames :: FlatScope -> ScopeM ([QName], [NewNotation])
localNames :: FlatScope -> ScopeM ([QName], [NewNotation])
localNames FlatScope
flat = do
let defs :: [List1 NewNotation]
defs = KindsOfNames -> FlatScope -> [List1 NewNotation]
getDefinedNames KindsOfNames
allKindsOfNames FlatScope
flat
[(Name, Name)]
locals <- forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocalVars -> [(Name, Name)]
notShadowedLocals forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m LocalVars
getLocalVars
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
[Char] -> Int -> a -> m ()
reportS [Char]
"scope.operators" Int
50
[ [Char]
"flat = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow FlatScope
flat
, [Char]
"defs = " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow [List1 NewNotation]
defs
, [Char]
"locals= " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow [(Name, Name)]
locals
]
let localNots :: [NewNotation]
localNots = forall a b. (a -> b) -> [a] -> [b]
map (Name, Name) -> NewNotation
localOp [(Name, Name)]
locals
notLocal :: NewNotation -> Bool
notLocal = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> a -> Bool
hasElem (forall a b. (a -> b) -> [a] -> [b]
map NewNotation -> QName
notaName [NewNotation]
localNots) forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> QName
notaName
otherNots :: [NewNotation]
otherNots = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a. (a -> Bool) -> NonEmpty a -> [a]
List1.filter NewNotation -> Bool
notLocal) [List1 NewNotation]
defs
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall a b. (a -> b) -> [a] -> [b]
map NewNotation -> NewNotation
useDefaultFixity) forall a b. (a -> b) -> a -> b
$ [NewNotation] -> ([QName], [NewNotation])
split forall a b. (a -> b) -> a -> b
$ [NewNotation]
localNots forall a. [a] -> [a] -> [a]
++ [NewNotation]
otherNots
where
localOp :: (Name, Name) -> NewNotation
localOp (Name
x, Name
y) = QName -> Name -> NewNotation
namesToNotation (Name -> QName
QName Name
x) Name
y
split :: [NewNotation] -> ([QName], [NewNotation])
split = forall a b. [Either a b] -> ([a], [b])
partitionEithers forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NewNotation -> [Either QName NewNotation]
opOrNot
opOrNot :: NewNotation -> [Either QName NewNotation]
opOrNot NewNotation
n = forall a b. a -> Either a b
Left (NewNotation -> QName
notaName NewNotation
n) forall a. a -> [a] -> [a]
:
[forall a b. b -> Either a b
Right NewNotation
n | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null (NewNotation -> Notation
notation NewNotation
n))]