-- | 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
(FlatScope -> Doc)
-> (Int -> FlatScope -> Doc)
-> ([FlatScope] -> Doc)
-> Pretty FlatScope
forall a.
(a -> Doc) -> (Int -> a -> Doc) -> ([a] -> Doc) -> Pretty a
$cpretty :: FlatScope -> Doc
pretty :: FlatScope -> Doc
$cprettyPrec :: Int -> FlatScope -> Doc
prettyPrec :: Int -> FlatScope -> Doc
$cprettyList :: [FlatScope] -> Doc
prettyList :: [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 (Map QName [AbstractName] -> FlatScope)
-> Map QName [AbstractName] -> FlatScope
forall a b. (a -> b) -> a -> b
$
  ([AbstractName] -> [AbstractName] -> [AbstractName])
-> Map QName [AbstractName]
-> Map QName [AbstractName]
-> Map QName [AbstractName]
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith [AbstractName] -> [AbstractName] -> [AbstractName]
forall a. [a] -> [a] -> [a]
(++)
    ([[Name]]
-> (forall a. InScope a => Scope -> ThingsInScope a)
-> Scope
-> Map QName [AbstractName]
build [[Name]]
ms Scope -> ThingsInScope a
forall a. InScope a => Scope -> ThingsInScope a
allNamesInScope Scope
root)
    Map QName [AbstractName]
imported
  where
    current :: Scope
current = ModuleName -> Scope
moduleScope (ModuleName -> Scope) -> ModuleName -> Scope
forall a b. (a -> b) -> a -> b
$ ScopeInfo
scope ScopeInfo -> Lens' ModuleName ScopeInfo -> ModuleName
forall o i. o -> Lens' i o -> i
^. (ModuleName -> f ModuleName) -> ScopeInfo -> f ScopeInfo
Lens' ModuleName ScopeInfo
scopeCurrent
    root :: Scope
root    = [Scope] -> Scope
mergeScopes ([Scope] -> Scope) -> [Scope] -> Scope
forall a b. (a -> b) -> a -> b
$ Scope
current Scope -> [Scope] -> [Scope]
forall a. a -> [a] -> [a]
: (ModuleName -> Scope) -> [ModuleName] -> [Scope]
forall a b. (a -> b) -> [a] -> [b]
map ModuleName -> Scope
moduleScope (Scope -> [ModuleName]
scopeParents Scope
current)

    imported :: Map QName [AbstractName]
imported = ([AbstractName] -> [AbstractName] -> [AbstractName])
-> [Map QName [AbstractName]] -> Map QName [AbstractName]
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith [AbstractName] -> [AbstractName] -> [AbstractName]
forall a. [a] -> [a] -> [a]
(++)
               [ QName -> Map QName [AbstractName] -> Map QName [AbstractName]
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' Scope -> ThingsInScope a
forall a. InScope a => Scope -> ThingsInScope a
exportedNamesInScope (Scope -> Map QName [AbstractName])
-> Scope -> Map QName [AbstractName]
forall a b. (a -> b) -> a -> b
$ ModuleName -> Scope
moduleScope ModuleName
a)
               | (QName
c, ModuleName
a) <- Map QName ModuleName -> [(QName, ModuleName)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map QName ModuleName -> [(QName, ModuleName)])
-> Map QName ModuleName -> [(QName, ModuleName)]
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' = ([Name] -> Maybe [Name]) -> [[Name]] -> [[Name]]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ([Name] -> [Name] -> Maybe [Name]
forall a. Eq a => [a] -> [a] -> Maybe [a]
List.stripPrefix ([Name] -> [Name] -> Maybe [Name])
-> [Name] -> [Name] -> Maybe [Name]
forall a b. (a -> b) -> a -> b
$ List1 Name -> [Item (List1 Name)]
forall l. IsList l => l -> [Item l]
List1.toList (List1 Name -> [Item (List1 Name)])
-> List1 Name -> [Item (List1 Name)]
forall a b. (a -> b) -> a -> b
$ QName -> List1 Name
qnameParts QName
c) [[Name]]
ms
               , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [[Name]] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Name]]
ms' ]
    qual :: QName -> Map QName a -> Map QName a
qual QName
c = (QName -> QName) -> Map QName a -> Map QName a
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 (QName -> QName) -> (QName -> QName) -> QName -> QName
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 = ([AbstractName] -> [AbstractName] -> [AbstractName])
-> [Map QName [AbstractName]] -> Map QName [AbstractName]
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith [AbstractName] -> [AbstractName] -> [AbstractName]
forall a. [a] -> [a] -> [a]
(++) ([Map QName [AbstractName]] -> Map QName [AbstractName])
-> [Map QName [AbstractName]] -> Map QName [AbstractName]
forall a b. (a -> b) -> a -> b
$
        (Name -> QName)
-> Map Name [AbstractName] -> Map QName [AbstractName]
forall k1 k2 a. (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeysMonotonic Name -> QName
QName (Scope -> Map Name [AbstractName]
forall a. InScope a => Scope -> ThingsInScope a
getNames Scope
s) Map QName [AbstractName]
-> [Map QName [AbstractName]] -> [Map QName [AbstractName]]
forall a. a -> [a] -> [a]
:
          [ (QName -> QName)
-> Map QName [AbstractName] -> Map QName [AbstractName]
forall k1 k2 a. (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeysMonotonic (\ QName
y -> Name -> QName -> QName
Qual Name
x QName
y) (Map QName [AbstractName] -> Map QName [AbstractName])
-> Map QName [AbstractName] -> Map QName [AbstractName]
forall a b. (a -> b) -> a -> b
$
              [[Name]]
-> (forall a. InScope a => Scope -> ThingsInScope a)
-> Scope
-> Map QName [AbstractName]
build [[Name]]
ms' Scope -> ThingsInScope a
forall a. InScope a => Scope -> ThingsInScope a
exportedNamesInScope (Scope -> Map QName [AbstractName])
-> Scope -> Map QName [AbstractName]
forall a b. (a -> b) -> a -> b
$ ModuleName -> Scope
moduleScope ModuleName
m
          | (Name
x, [AbstractModule]
mods) <- Map Name [AbstractModule] -> [(Name, [AbstractModule])]
forall k a. Map k a -> [(k, a)]
Map.toList (Scope -> Map Name [AbstractModule]
forall a. InScope a => Scope -> ThingsInScope a
getNames Scope
s)
          , let ms' :: [[Name]]
ms' = [ [Name]
tl | Name
hd:[Name]
tl <- [[Name]]
ms, Name
hd Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x ]
          , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [[Name]] -> Bool
forall a. [a] -> Bool
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 = Scope -> Maybe Scope -> Scope
forall a. a -> Maybe a -> a
fromMaybe Scope
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Scope -> Scope) -> Maybe Scope -> Scope
forall a b. (a -> b) -> a -> b
$ ModuleName -> Map ModuleName Scope -> Maybe Scope
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ModuleName
m (Map ModuleName Scope -> Maybe Scope)
-> Map ModuleName Scope -> Maybe Scope
forall a b. (a -> b) -> a -> b
$ ScopeInfo
scope ScopeInfo
-> Lens' (Map ModuleName Scope) ScopeInfo -> Map ModuleName Scope
forall o i. o -> Lens' i o -> i
^. (Map ModuleName Scope -> f (Map ModuleName Scope))
-> ScopeInfo -> f ScopeInfo
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 ([NewNotation] -> [NewNotation]) -> [NewNotation] -> [NewNotation]
forall a b. (a -> b) -> a -> b
$ (AbstractName -> NewNotation) -> [AbstractName] -> [NewNotation]
forall a b. (a -> b) -> [a] -> [b]
map (QName -> Name -> NewNotation
namesToNotation QName
x (Name -> NewNotation)
-> (AbstractName -> Name) -> AbstractName -> NewNotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
A.qnameName (QName -> Name) -> (AbstractName -> QName) -> AbstractName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> QName
anameName) [AbstractName]
ds
  | (QName
x, [AbstractName]
ds) <- Map QName [AbstractName] -> [(QName, [AbstractName])]
forall k a. Map k a -> [(k, a)]
Map.toList Map QName [AbstractName]
names
  , (AbstractName -> Bool) -> [AbstractName] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((KindOfName -> KindsOfNames -> Bool
`elemKindsOfNames` KindsOfNames
kinds) (KindOfName -> Bool)
-> (AbstractName -> KindOfName) -> AbstractName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> KindOfName
anameKind) [AbstractName]
ds
  , Bool -> Bool
not ([AbstractName] -> Bool
forall a. [a] -> Bool
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 <- ((Name, Name) -> Name) -> [(Name, Name)] -> [(Name, Name)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn (Name, Name) -> Name
forall a b. (a, b) -> a
fst ([(Name, Name)] -> [(Name, Name)])
-> (LocalVars -> [(Name, Name)]) -> LocalVars -> [(Name, Name)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocalVars -> [(Name, Name)]
notShadowedLocals (LocalVars -> [(Name, Name)])
-> TCMT IO LocalVars -> TCMT IO [(Name, Name)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO LocalVars
forall (m :: * -> *). ReadTCState m => m LocalVars
getLocalVars
  -- Note: Debug printout aligned with the one in
  -- Agda.Syntax.Concrete.Operators.buildParsers.
  [Char] -> Int -> [[Char]] -> TCMT IO ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
[Char] -> Int -> a -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [[Char]] -> m ()
reportS [Char]
"scope.operators" Int
50
    [ [Char]
"flat  = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ FlatScope -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow FlatScope
flat
    , [Char]
"defs  = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [[NewNotation]] -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow [[NewNotation]]
defs
    , [Char]
"locals= " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [(Name, Name)] -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow [(Name, Name)]
locals
    ]
  let localNots :: [NewNotation]
localNots  = ((Name, Name) -> NewNotation) -> [(Name, Name)] -> [NewNotation]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Name) -> NewNotation
localOp [(Name, Name)]
locals
      notLocal :: NewNotation -> Bool
notLocal   = Bool -> Bool
not (Bool -> Bool) -> (NewNotation -> Bool) -> NewNotation -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [QName] -> QName -> Bool
forall a. Ord a => [a] -> a -> Bool
hasElem ((NewNotation -> QName) -> [NewNotation] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map NewNotation -> QName
notaName [NewNotation]
localNots) (QName -> Bool) -> (NewNotation -> QName) -> NewNotation -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> QName
notaName
      otherNots :: [NewNotation]
otherNots  = ([NewNotation] -> [NewNotation])
-> [[NewNotation]] -> [NewNotation]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((NewNotation -> Bool) -> [NewNotation] -> [NewNotation]
forall a. (a -> Bool) -> [a] -> [a]
filter NewNotation -> Bool
notLocal) [[NewNotation]]
defs
  ([QName], [NewNotation]) -> ScopeM ([QName], [NewNotation])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (([QName], [NewNotation]) -> ScopeM ([QName], [NewNotation]))
-> ([QName], [NewNotation]) -> ScopeM ([QName], [NewNotation])
forall a b. (a -> b) -> a -> b
$ ([NewNotation] -> [NewNotation])
-> ([QName], [NewNotation]) -> ([QName], [NewNotation])
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((NewNotation -> NewNotation) -> [NewNotation] -> [NewNotation]
forall a b. (a -> b) -> [a] -> [b]
map NewNotation -> NewNotation
useDefaultFixity) (([QName], [NewNotation]) -> ([QName], [NewNotation]))
-> ([QName], [NewNotation]) -> ([QName], [NewNotation])
forall a b. (a -> b) -> a -> b
$ [NewNotation] -> ([QName], [NewNotation])
split ([NewNotation] -> ([QName], [NewNotation]))
-> [NewNotation] -> ([QName], [NewNotation])
forall a b. (a -> b) -> a -> b
$ [NewNotation]
localNots [NewNotation] -> [NewNotation] -> [NewNotation]
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          = [Either QName NewNotation] -> ([QName], [NewNotation])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either QName NewNotation] -> ([QName], [NewNotation]))
-> ([NewNotation] -> [Either QName NewNotation])
-> [NewNotation]
-> ([QName], [NewNotation])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NewNotation -> [Either QName NewNotation])
-> [NewNotation] -> [Either QName NewNotation]
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      = QName -> Either QName NewNotation
forall a b. a -> Either a b
Left (NewNotation -> QName
notaName NewNotation
n) Either QName NewNotation
-> [Either QName NewNotation] -> [Either QName NewNotation]
forall a. a -> [a] -> [a]
:
                     [NewNotation -> Either QName NewNotation
forall a b. b -> Either a b
Right NewNotation
n | Bool -> Bool
not ([NotationPart] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (NewNotation -> [NotationPart]
notation NewNotation
n))]