-- | Flattened scopes.
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 qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Pretty

-- | Flattened scopes.
newtype FlatScope = Flat (Map QName [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

-- | Compute a flattened scope. Only include unqualified names or names
-- qualified by modules in the first argument.
flattenScope :: [[Name]] -> ScopeInfo -> FlatScope
flattenScope :: [[Name]] -> ScopeInfo -> FlatScope
flattenScope [[Name]]
ms ScopeInfo
scope =
  Map QName [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. [a] -> [a] -> [a]
(++)
    ([[Name]]
-> (forall a. InScope a => Scope -> ThingsInScope a)
-> Scope
-> Map QName [AbstractName]
build [[Name]]
ms forall a. InScope a => Scope -> ThingsInScope a
allNamesInScope Scope
root)
    Map QName [AbstractName]
imported
  where
    current :: Scope
current = ModuleName -> Scope
moduleScope forall a b. (a -> b) -> a -> b
$ ScopeInfo
scope forall o i. o -> Lens' i o -> i
^. Lens' ModuleName ScopeInfo
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 [AbstractName]
imported = forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith forall 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 [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 -- get the suffixes of c in ms
                     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 [AbstractName]
    build :: [[Name]]
-> (forall a. InScope a => Scope -> ThingsInScope a)
-> Scope
-> Map QName [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. [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 [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, [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
_ <- [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' i o -> i
^. Lens' (Map ModuleName Scope) ScopeInfo
scopeModules

-- | Compute all defined names in scope and their fixities/notations.
-- Note that overloaded names (constructors) can have several
-- fixities/notations. Then we 'mergeNotations'. (See issue 1194.)
getDefinedNames :: KindsOfNames -> FlatScope -> [[NewNotation]]
getDefinedNames :: KindsOfNames -> FlatScope -> [[NewNotation]]
getDefinedNames KindsOfNames
kinds (Flat Map QName [AbstractName]
names) =
  [ [NewNotation] -> [NewNotation]
mergeNotations forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (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) [AbstractName]
ds
  | (QName
x, [AbstractName]
ds) <- forall k a. Map k a -> [(k, a)]
Map.toList Map QName [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) [AbstractName]
ds
  , Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [AbstractName]
ds)
  ]
  -- Andreas, 2013-03-21 see Issue 822
  -- Names can have different kinds, i.e., 'defined' and 'constructor'.
  -- We need to consider all names that have *any* matching kind,
  -- not only those whose first appearing kind is matching.

-- | Compute all names (first component) and operators/notations
-- (second component) in scope.
localNames :: FlatScope -> ScopeM ([QName], [NewNotation])
localNames :: FlatScope -> ScopeM ([QName], [NewNotation])
localNames FlatScope
flat = do
  let defs :: [[NewNotation]]
defs = KindsOfNames -> FlatScope -> [[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
  -- Note: Debug printout aligned with the one in
  -- Agda.Syntax.Concrete.Operators.buildParsers.
  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 [[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) -> [a] -> [a]
filter NewNotation -> Bool
notLocal) [[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))]