{- |
Module: Agda.Unused

Check an Agda project for unused code.
-}
module Agda.Unused.Check
  ( checkUnused
  , checkUnusedLocal
  ) where

import Agda.Unused
  (Unused(..), UnusedItems(..))
import Agda.Unused.Monad.Error
  (Error(..), InternalError(..), UnexpectedError(..), UnsupportedError(..),
    liftLookup)
import Agda.Unused.Monad.Reader
  (Environment(..), askLocal, askRoot, askSkip, localSkip)
import Agda.Unused.Monad.State
  (ModuleState(..), State, modifyDelete, modifyInsert, stateBlock,
    stateCheck, stateEmpty, stateItems, stateLookup, stateModules)
import Agda.Unused.Types.Access
  (Access(..), fromAccess)
import Agda.Unused.Types.Context
  (AccessContext, AccessModule(..), Context, LookupError(..),
    accessContextDefine, accessContextImport, accessContextItem,
    accessContextLookup, accessContextLookupDefining, accessContextLookupModule,
    accessContextLookupSpecial, accessContextMatch, accessContextModule,
    accessContextModule', accessContextUnion, contextDelete,
    contextDeleteModule, contextItem, contextLookup, contextLookupItem,
    contextLookupModule, contextModule, contextRanges, fromContext, item,
    itemConstructor, itemPattern, moduleRanges, toContext)
import qualified Agda.Unused.Types.Context
  as C
import Agda.Unused.Types.Name
  (Name(..), QName(..), isBuiltin, fromAsName, fromName, fromNameRange,
    fromQName, fromQNameRange, nameIds, pathQName, qNamePath)
import Agda.Unused.Types.Range
  (Range'(..), RangeInfo(..), RangeType(..))
import Agda.Unused.Types.Root
  (Root(..), Roots(..))
import Agda.Unused.Utils
  (liftMaybe, mapLeft)

import Agda.Syntax.Common
  (Arg(..), Fixity'(..), GenPart(..), ImportDirective'(..), ImportedName'(..),
    Named(..), Ranged(..), Renaming'(..), RewriteEqn'(..), Using'(..),
    namedThing, unArg, whThing)
import qualified Agda.Syntax.Common
  as Common
import Agda.Syntax.Concrete
  (Binder, Binder'(..), BoundName(..), Declaration, DoStmt(..), Expr(..),
    FieldAssignment, FieldAssignment'(..), ImportDirective, ImportedName,
    LamBinding, LamBinding'(..), LamClause(..), LHS(..), Module,
    ModuleApplication(..), ModuleAssignment(..), OpenShortHand(..), Pattern(..),
    RecordAssignment, Renaming, RewriteEqn, RHS, RHS'(..), TypedBinding,
    TypedBinding'(..), WhereClause, WhereClause'(..), _exprFieldA)
import Agda.Syntax.Concrete.Definitions
  (Clause(..), NiceDeclaration(..), niceDeclarations, runNice)
import Agda.Syntax.Concrete.Fixity
  (DoWarn(..), Fixities, fixitiesAndPolarities)
import Agda.Syntax.Concrete.Name
  (NameInScope(..), NamePart(..))
import qualified Agda.Syntax.Concrete.Name
  as N
import Agda.Syntax.Parser
  (moduleParser, parseFile, runPMIO)
import Agda.Syntax.Position
  (Range, getRange)
import Agda.Utils.FileName
  (AbsolutePath(..))
import Control.Monad
  (foldM, void)
import Control.Monad.Except
  (MonadError, liftEither, runExceptT, throwError)
import Control.Monad.IO.Class
  (MonadIO, liftIO)
import Control.Monad.Reader
  (MonadReader, ReaderT, runReaderT)
import Control.Monad.State
  (MonadState, StateT, gets, modify, runStateT)
import Data.Bool
  (bool)
import qualified Data.Map.Strict
  as Map
import Data.Maybe
  (catMaybes)
import qualified Data.Text
  as T
import System.Directory
  (doesDirectoryExist, doesFileExist, listDirectory)
import System.FilePath
  ((</>))

import Paths_agda_unused
  (getDataFileName)

-- ## Context

-- Do nothing if `askSkip` returns true.
contextInsertRange
  :: MonadReader Environment m
  => Name
  -> Range
  -> Context
  -> m Context
contextInsertRange :: Name -> Range -> Context -> m Context
contextInsertRange n :: Name
n r :: Range
r c :: Context
c
  = m Bool
forall (m :: * -> *). MonadReader Environment m => m Bool
askSkip m Bool -> (Bool -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Context -> m Context
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context -> m Context) -> (Bool -> Context) -> Bool -> m Context
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context -> Bool -> Context
forall a. a -> a -> Bool -> a
bool (Name -> Range -> Context -> Context
C.contextInsertRange Name
n Range
r Context
c) Context
c

-- Do nothing if `askSkip` returns true.
contextInsertRangeModule
  :: MonadReader Environment m
  => Name
  -> Range
  -> Context
  -> m Context
contextInsertRangeModule :: Name -> Range -> Context -> m Context
contextInsertRangeModule n :: Name
n r :: Range
r c :: Context
c
  = m Bool
forall (m :: * -> *). MonadReader Environment m => m Bool
askSkip m Bool -> (Bool -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Context -> m Context
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context -> m Context) -> (Bool -> Context) -> Bool -> m Context
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context -> Bool -> Context
forall a. a -> a -> Bool -> a
bool (Name -> Range -> Context -> Context
C.contextInsertRangeModule Name
n Range
r Context
c) Context
c

-- Do nothing if `askSkip` returns true.
contextInsertRangeAll
  :: MonadReader Environment m
  => Range
  -> Context
  -> m Context
contextInsertRangeAll :: Range -> Context -> m Context
contextInsertRangeAll r :: Range
r c :: Context
c
  = m Bool
forall (m :: * -> *). MonadReader Environment m => m Bool
askSkip m Bool -> (Bool -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Context -> m Context
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context -> m Context) -> (Bool -> Context) -> Bool -> m Context
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Context -> Bool -> Context
forall a. a -> a -> Bool -> a
bool (Range -> Context -> Context
C.contextInsertRangeAll Range
r Context
c) Context
c

-- Do nothing if `askSkip` returns true.
accessContextInsertRangeAll
  :: MonadReader Environment m
  => Range
  -> AccessContext
  -> m AccessContext
accessContextInsertRangeAll :: Range -> AccessContext -> m AccessContext
accessContextInsertRangeAll r :: Range
r c :: AccessContext
c
  = m Bool
forall (m :: * -> *). MonadReader Environment m => m Bool
askSkip m Bool -> (Bool -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext -> m AccessContext)
-> (Bool -> AccessContext) -> Bool -> m AccessContext
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AccessContext -> AccessContext -> Bool -> AccessContext
forall a. a -> a -> Bool -> a
bool (Range -> AccessContext -> AccessContext
C.accessContextInsertRangeAll Range
r AccessContext
c) AccessContext
c

-- Also insert range unless `askSkip` returns true.
contextRename
  :: MonadReader Environment m
  => Name
  -> Name
  -> Range
  -> Context
  -> m Context
contextRename :: Name -> Name -> Range -> Context -> m Context
contextRename n :: Name
n t :: Name
t r :: Range
r c :: Context
c
  = Name -> Range -> Context -> m Context
forall (m :: * -> *).
MonadReader Environment m =>
Name -> Range -> Context -> m Context
contextInsertRange Name
n Range
r Context
c
  m Context -> (Context -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Context -> m Context
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context -> m Context)
-> (Context -> Context) -> Context -> m Context
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name -> Context -> Context
C.contextRename Name
n Name
t

-- Also insert range unless `askSkip` returns true.
contextRenameModule
  :: MonadReader Environment m
  => Name
  -> Name
  -> Range
  -> Context
  -> m Context
contextRenameModule :: Name -> Name -> Range -> Context -> m Context
contextRenameModule n :: Name
n t :: Name
t r :: Range
r c :: Context
c
  = Name -> Range -> Context -> m Context
forall (m :: * -> *).
MonadReader Environment m =>
Name -> Range -> Context -> m Context
contextInsertRangeModule Name
n Range
r Context
c
  m Context -> (Context -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Context -> m Context
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context -> m Context)
-> (Context -> Context) -> Context -> m Context
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name -> Context -> Context
C.contextRenameModule Name
n Name
t

-- ## Syntax

syntax
  :: Fixities
  -> Name
  -> Maybe Name
syntax :: Fixities -> Name -> Maybe Name
syntax fs :: Fixities
fs (Name ps :: [NamePart]
ps)
  = Name -> Fixities -> Maybe Fixity'
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Range -> NameInScope -> [NamePart] -> Name
N.Name Range
forall a. Range' a
NoRange NameInScope
InScope [NamePart]
ps) Fixities
fs Maybe Fixity' -> (Fixity' -> Maybe Name) -> Maybe Name
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Fixity' -> Maybe Name
fromFixity

fromFixity
  :: Fixity'
  -> Maybe Name
fromFixity :: Fixity' -> Maybe Name
fromFixity (Fixity' _ [] _)
  = Maybe Name
forall a. Maybe a
Nothing
fromFixity (Fixity' _ ps :: Notation
ps@(_ : _) _)
  = Name -> Maybe Name
forall a. a -> Maybe a
Just ([NamePart] -> Name
Name (GenPart -> NamePart
fromGenPart (GenPart -> NamePart) -> Notation -> [NamePart]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Notation
ps))

fromGenPart
  :: GenPart
  -> NamePart
fromGenPart :: GenPart -> NamePart
fromGenPart (BindHole _ _)
  = NamePart
Hole
fromGenPart (NormalHole _ _)
  = NamePart
Hole
fromGenPart (WildHole _)
  = NamePart
Hole
fromGenPart (IdPart (Ranged _ s :: RawName
s))
  = RawName -> NamePart
Id RawName
s

-- ## Lists

checkSequence
  :: Monad m
  => Monoid c
  => (a -> b -> m c)
  -> a
  -> [b]
  -> m c
checkSequence :: (a -> b -> m c) -> a -> [b] -> m c
checkSequence f :: a -> b -> m c
f x :: a
x ys :: [b]
ys
  = [c] -> c
forall a. Monoid a => [a] -> a
mconcat ([c] -> c) -> m [c] -> m c
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m c] -> m [c]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (a -> b -> m c
f a
x (b -> m c) -> [b] -> [m c]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [b]
ys)

checkSequence_
  :: Monad m
  => (a -> b -> m ())
  -> a
  -> [b]
  -> m ()
checkSequence_ :: (a -> b -> m ()) -> a -> [b] -> m ()
checkSequence_ f :: a -> b -> m ()
f x :: a
x ys :: [b]
ys
  = m [()] -> m ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void ([m ()] -> m [()]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (a -> b -> m ()
f a
x (b -> m ()) -> [b] -> [m ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [b]
ys))

checkFold
  :: Monad m
  => Monoid a
  => (a -> b -> m a)
  -> a
  -> [b]
  -> m a
checkFold :: (a -> b -> m a) -> a -> [b] -> m a
checkFold
  = a -> (a -> a -> a) -> (a -> b -> m a) -> a -> [b] -> m a
forall (m :: * -> *) a b.
Monad m =>
a -> (a -> a -> a) -> (a -> b -> m a) -> a -> [b] -> m a
checkFoldWith a
forall a. Monoid a => a
mempty a -> a -> a
forall a. Semigroup a => a -> a -> a
(<>)

checkFoldUnion
  :: Monad m
  => (AccessContext -> b -> m AccessContext)
  -> AccessContext
  -> [b]
  -> m AccessContext
checkFoldUnion :: (AccessContext -> b -> m AccessContext)
-> AccessContext -> [b] -> m AccessContext
checkFoldUnion
  = AccessContext
-> (AccessContext -> AccessContext -> AccessContext)
-> (AccessContext -> b -> m AccessContext)
-> AccessContext
-> [b]
-> m AccessContext
forall (m :: * -> *) a b.
Monad m =>
a -> (a -> a -> a) -> (a -> b -> m a) -> a -> [b] -> m a
checkFoldWith AccessContext
forall a. Monoid a => a
mempty AccessContext -> AccessContext -> AccessContext
accessContextUnion

checkFoldWith
  :: Monad m
  => a
  -> (a -> a -> a)
  -> (a -> b -> m a)
  -> a
  -> [b]
  -> m a
checkFoldWith :: a -> (a -> a -> a) -> (a -> b -> m a) -> a -> [b] -> m a
checkFoldWith x :: a
x f :: a -> a -> a
f g :: a -> b -> m a
g x' :: a
x' ys :: [b]
ys
  = (a -> b -> m a) -> a -> [b] -> m a
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\x'' :: a
x'' y :: b
y -> a -> a -> a
f a
x'' (a -> a) -> m a -> m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> b -> m a
g (a -> a -> a
f a
x' a
x'') b
y) a
x [b]
ys

-- ## Names

checkName
  :: MonadReader Environment m
  => MonadState State m
  => Bool
  -- ^ Whether to treat names as pattern synonyms.
  -> Fixities
  -> Access
  -> RangeType
  -> Range
  -> Name
  -> m AccessContext
checkName :: Bool
-> Fixities
-> Access
-> RangeType
-> Range
-> Name
-> m AccessContext
checkName _ _ _ _ NoRange _
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkName _ _ _ _ _ (Name [Hole])
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkName p :: Bool
p fs :: Fixities
fs a :: Access
a t :: RangeType
t r :: Range
r@(Range _ _) n :: Name
n
  = Range -> RangeInfo -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Range -> RangeInfo -> m ()
modifyInsert Range
r (RangeType -> QName -> RangeInfo
RangeNamed RangeType
t (Name -> QName
QName Name
n))
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> Access -> Item -> AccessContext
accessContextItem Name
n Access
a (([Range] -> Maybe Name -> Item)
-> ([Range] -> Maybe Name -> Item)
-> Bool
-> [Range]
-> Maybe Name
-> Item
forall a. a -> a -> Bool -> a
bool [Range] -> Maybe Name -> Item
item [Range] -> Maybe Name -> Item
itemPattern Bool
p [Range
r] (Fixities -> Name -> Maybe Name
syntax Fixities
fs Name
n)))

checkName'
  :: MonadReader Environment m
  => MonadState State m
  => Bool
  -- ^ Whether to treat names as pattern synonyms.
  -> Fixities
  -> Access
  -> RangeType
  -> N.Name
  -> m AccessContext
checkName' :: Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
checkName' p :: Bool
p fs :: Fixities
fs a :: Access
a t :: RangeType
t n :: Name
n
  = m AccessContext
-> ((Range, Name) -> m AccessContext)
-> Maybe (Range, Name)
-> m AccessContext
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty) ((Range -> Name -> m AccessContext)
-> (Range, Name) -> m AccessContext
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Bool
-> Fixities
-> Access
-> RangeType
-> Range
-> Name
-> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool
-> Fixities
-> Access
-> RangeType
-> Range
-> Name
-> m AccessContext
checkName Bool
p Fixities
fs Access
a RangeType
t)) (Name -> Maybe (Range, Name)
fromNameRange Name
n)

checkNames'
  :: MonadReader Environment m
  => MonadState State m
  => Bool
  -- ^ Whether to treat names as pattern synonyms.
  -> Access
  -> RangeType
  -> [N.Name]
  -> m AccessContext
checkNames' :: Bool -> Access -> RangeType -> [Name] -> m AccessContext
checkNames' p :: Bool
p a :: Access
a
  = (RangeType -> Name -> m AccessContext)
-> RangeType -> [Name] -> m AccessContext
forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence (Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
checkName' Bool
p Fixities
forall a. Monoid a => a
mempty Access
a)

checkQNameP
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => AccessContext
  -> Range
  -> QName
  -> m AccessContext
checkQNameP :: AccessContext -> Range -> QName -> m AccessContext
checkQNameP c :: AccessContext
c r :: Range
r n :: QName
n
  = Maybe Bool -> AccessContext -> Range -> QName -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
Maybe Bool -> AccessContext -> Range -> QName -> m AccessContext
checkQNamePWith (QName -> AccessContext -> Maybe Bool
accessContextLookupSpecial QName
n AccessContext
c) AccessContext
c Range
r QName
n

checkQNamePWith
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => Maybe Bool
  -> AccessContext
  -> Range
  -> QName
  -> m AccessContext
checkQNamePWith :: Maybe Bool -> AccessContext -> Range -> QName -> m AccessContext
checkQNamePWith Nothing _ r :: Range
r n :: QName
n
  = Access -> RangeType -> Range -> QName -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Access -> RangeType -> Range -> QName -> m AccessContext
checkQName Access
Public RangeType
RangeVariable Range
r QName
n
checkQNamePWith (Just False) _ _ _
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkQNamePWith (Just True) c :: AccessContext
c r :: Range
r n :: QName
n
  = AccessContext -> Range -> QName -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
AccessContext -> Range -> QName -> m ()
touchQName AccessContext
c Range
r QName
n m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty

checkQNameP'
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => AccessContext
  -> N.QName
  -> m AccessContext
checkQNameP' :: AccessContext -> QName -> m AccessContext
checkQNameP' c :: AccessContext
c n :: QName
n
  = m AccessContext
-> ((Range, QName) -> m AccessContext)
-> Maybe (Range, QName)
-> m AccessContext
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty) ((Range -> QName -> m AccessContext)
-> (Range, QName) -> m AccessContext
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (AccessContext -> Range -> QName -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
AccessContext -> Range -> QName -> m AccessContext
checkQNameP AccessContext
c)) (QName -> Maybe (Range, QName)
fromQNameRange QName
n)

checkQName
  :: MonadReader Environment m
  => MonadState State m
  => Access
  -> RangeType
  -> Range
  -> QName
  -> m AccessContext
checkQName :: Access -> RangeType -> Range -> QName -> m AccessContext
checkQName a :: Access
a t :: RangeType
t r :: Range
r (QName n :: Name
n)
  = Bool
-> Fixities
-> Access
-> RangeType
-> Range
-> Name
-> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool
-> Fixities
-> Access
-> RangeType
-> Range
-> Name
-> m AccessContext
checkName Bool
False Fixities
forall a. Monoid a => a
mempty Access
a RangeType
t Range
r Name
n
checkQName _ _ _ (Qual _ _)
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty

checkModuleName
  :: MonadReader Environment m
  => MonadState State m
  => Context
  -> Access
  -> Range
  -> Name
  -> m AccessContext
checkModuleName :: Context -> Access -> Range -> Name -> m AccessContext
checkModuleName c :: Context
c a :: Access
a r :: Range
r n :: Name
n
  = Range -> RangeInfo -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Range -> RangeInfo -> m ()
modifyInsert Range
r (RangeType -> QName -> RangeInfo
RangeNamed RangeType
RangeModule (Name -> QName
QName Name
n))
  m () -> m Context -> m Context
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Range -> Context -> m Context
forall (m :: * -> *).
MonadReader Environment m =>
Range -> Context -> m Context
contextInsertRangeAll Range
r Context
c
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c' :: Context
c' -> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> AccessModule -> AccessContext
accessContextModule Name
n (Access -> [Range] -> Context -> AccessModule
AccessModule Access
a [Range
r] Context
c'))

touchName
  :: MonadReader Environment m
  => MonadState State m
  => AccessContext
  -> Name
  -> m ()
touchName :: AccessContext -> Name -> m ()
touchName c :: AccessContext
c n :: Name
n
  = m Bool
forall (m :: * -> *). MonadReader Environment m => m Bool
askSkip m Bool -> (Bool -> m ()) -> m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Either LookupError (Bool, [Range]) -> Bool -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Either LookupError (Bool, [Range]) -> Bool -> m ()
touchNameWith (QName -> AccessContext -> Either LookupError (Bool, [Range])
accessContextLookupDefining (Name -> QName
QName Name
n) AccessContext
c)

touchNameWith
  :: MonadReader Environment m
  => MonadState State m
  => Either LookupError (Bool, [Range])
  -> Bool
  -> m ()
touchNameWith :: Either LookupError (Bool, [Range]) -> Bool -> m ()
touchNameWith (Right (False, rs :: [Range]
rs)) False
  = [Range] -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
[Range] -> m ()
modifyDelete [Range]
rs
touchNameWith _ _
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

touchNames
  :: MonadReader Environment m
  => MonadState State m
  => AccessContext
  -> [Name]
  -> m ()
touchNames :: AccessContext -> [Name] -> m ()
touchNames
  = (AccessContext -> Name -> m ()) -> AccessContext -> [Name] -> m ()
forall (m :: * -> *) a b.
Monad m =>
(a -> b -> m ()) -> a -> [b] -> m ()
checkSequence_ AccessContext -> Name -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
AccessContext -> Name -> m ()
touchName

touchQName
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => AccessContext
  -> Range
  -> QName
  -> m ()
touchQName :: AccessContext -> Range -> QName -> m ()
touchQName c :: AccessContext
c r :: Range
r n :: QName
n
  = m Bool
forall (m :: * -> *). MonadReader Environment m => m Bool
askSkip m Bool -> (Bool -> m ()) -> m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Range
-> QName -> Either LookupError (Bool, [Range]) -> Bool -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
Range
-> QName -> Either LookupError (Bool, [Range]) -> Bool -> m ()
touchQNameWith Range
r QName
n (QName -> AccessContext -> Either LookupError (Bool, [Range])
accessContextLookupDefining QName
n AccessContext
c)

touchQNameWith
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => Range
  -> QName
  -> Either LookupError (Bool, [Range])
  -> Bool
  -> m ()
touchQNameWith :: Range
-> QName -> Either LookupError (Bool, [Range]) -> Bool -> m ()
touchQNameWith r :: Range
r n :: QName
n (Left LookupAmbiguous) False
  = Error -> m ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Range -> QName -> Error
ErrorAmbiguous Range
r QName
n)
touchQNameWith _ _ rs :: Either LookupError (Bool, [Range])
rs b :: Bool
b
  = Either LookupError (Bool, [Range]) -> Bool -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Either LookupError (Bool, [Range]) -> Bool -> m ()
touchNameWith Either LookupError (Bool, [Range])
rs Bool
b

touchQNameContext
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => Context
  -> QName
  -> QName
  -> m ()
touchQNameContext :: Context -> QName -> QName -> m ()
touchQNameContext c :: Context
c m :: QName
m n :: QName
n
  = m () -> ([Range] -> m ()) -> Maybe [Range] -> m ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Error -> m ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (QName -> QName -> Error
ErrorRoot QName
m QName
n)) [Range] -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
[Range] -> m ()
modifyDelete (QName -> Context -> Maybe [Range]
contextLookup QName
n Context
c)

touchQNamesContext
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => Context
  -> QName
  -> [QName]
  -> m ()
touchQNamesContext :: Context -> QName -> [QName] -> m ()
touchQNamesContext m :: Context
m p :: QName
p
  = m [()] -> m ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (m [()] -> m ()) -> ([QName] -> m [()]) -> [QName] -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName -> m ()) -> [QName] -> m [()]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Context -> QName -> QName -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
Context -> QName -> QName -> m ()
touchQNameContext Context
m QName
p)

touchQName'
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => AccessContext
  -> N.QName
  -> m ()
touchQName' :: AccessContext -> QName -> m ()
touchQName' c :: AccessContext
c n :: QName
n
  = m () -> ((Range, QName) -> m ()) -> Maybe (Range, QName) -> m ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) ((Range -> QName -> m ()) -> (Range, QName) -> m ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (AccessContext -> Range -> QName -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
AccessContext -> Range -> QName -> m ()
touchQName AccessContext
c)) (QName -> Maybe (Range, QName)
fromQNameRange QName
n)

-- ## Bindings

checkBinder
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Bool
  -- ^ Whether to check bound names.
  -> AccessContext
  -> Binder
  -> m AccessContext
checkBinder :: Bool -> AccessContext -> Binder -> m AccessContext
checkBinder b :: Bool
b c :: AccessContext
c (Binder p :: Maybe Pattern
p (BName n :: Name
n _ _))
  = (m AccessContext -> m AccessContext)
-> (m AccessContext -> m AccessContext)
-> Bool
-> m AccessContext
-> m AccessContext
forall a. a -> a -> Bool -> a
bool m AccessContext -> m AccessContext
forall (m :: * -> *) a. MonadReader Environment m => m a -> m a
localSkip m AccessContext -> m AccessContext
forall a. a -> a
id Bool
b (Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
checkName' Bool
False Fixities
forall a. Monoid a => a
mempty Access
Public RangeType
RangeVariable Name
n)
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c' :: AccessContext
c' -> AccessContext -> Maybe Pattern -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Maybe Pattern -> m AccessContext
checkPatternMay AccessContext
c Maybe Pattern
p
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'' :: AccessContext
c'' -> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
c' AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c'')

checkBinders
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Bool
  -- ^ Whether to check bound names.
  -> AccessContext
  -> [Binder]
  -> m AccessContext
checkBinders :: Bool -> AccessContext -> [Binder] -> m AccessContext
checkBinders b :: Bool
b
  = (AccessContext -> Binder -> m AccessContext)
-> AccessContext -> [Binder] -> m AccessContext
forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence (Bool -> AccessContext -> Binder -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> Binder -> m AccessContext
checkBinder Bool
b)

checkLamBinding
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Bool
  -- ^ Whether to check bound names.
  -> AccessContext
  -> LamBinding
  -> m AccessContext
checkLamBinding :: Bool -> AccessContext -> LamBinding -> m AccessContext
checkLamBinding b :: Bool
b c :: AccessContext
c (DomainFree (Arg _ (Named _ b' :: Binder
b')))
  = Bool -> AccessContext -> Binder -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> Binder -> m AccessContext
checkBinder Bool
b AccessContext
c Binder
b'
checkLamBinding b :: Bool
b c :: AccessContext
c (DomainFull b' :: TypedBinding
b')
  = Bool -> AccessContext -> TypedBinding -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> TypedBinding -> m AccessContext
checkTypedBinding Bool
b AccessContext
c TypedBinding
b'

checkLamBindings
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Bool
  -- ^ Whether to check bound names.
  -> AccessContext
  -> [LamBinding]
  -> m AccessContext
checkLamBindings :: Bool -> AccessContext -> [LamBinding] -> m AccessContext
checkLamBindings b :: Bool
b
  = (AccessContext -> LamBinding -> m AccessContext)
-> AccessContext -> [LamBinding] -> m AccessContext
forall (m :: * -> *) a b.
(Monad m, Monoid a) =>
(a -> b -> m a) -> a -> [b] -> m a
checkFold (Bool -> AccessContext -> LamBinding -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> LamBinding -> m AccessContext
checkLamBinding Bool
b)

checkTypedBinding
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Bool
  -- ^ Whether to check bound names.
  -> AccessContext
  -> TypedBinding
  -> m AccessContext
checkTypedBinding :: Bool -> AccessContext -> TypedBinding -> m AccessContext
checkTypedBinding b :: Bool
b c :: AccessContext
c (TBind _ bs :: [Arg (Named_ Binder)]
bs e :: Expr
e)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> AccessContext -> [Binder] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> [Binder] -> m AccessContext
checkBinders Bool
b AccessContext
c (Named_ Binder -> Binder
forall name a. Named name a -> a
namedThing (Named_ Binder -> Binder)
-> (Arg (Named_ Binder) -> Named_ Binder)
-> Arg (Named_ Binder)
-> Binder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Named_ Binder) -> Named_ Binder
forall e. Arg e -> e
unArg (Arg (Named_ Binder) -> Binder)
-> [Arg (Named_ Binder)] -> [Binder]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg (Named_ Binder)]
bs)
checkTypedBinding _ c :: AccessContext
c (TLet _ ds :: [Declaration]
ds)
  = AccessContext -> [Declaration] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Declaration] -> m AccessContext
checkDeclarations AccessContext
c [Declaration]
ds

checkTypedBindings
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Bool
  -- ^ Whether to check bound names.
  -> AccessContext
  -> [TypedBinding]
  -> m AccessContext
checkTypedBindings :: Bool -> AccessContext -> [TypedBinding] -> m AccessContext
checkTypedBindings b :: Bool
b
  = (AccessContext -> TypedBinding -> m AccessContext)
-> AccessContext -> [TypedBinding] -> m AccessContext
forall (m :: * -> *) a b.
(Monad m, Monoid a) =>
(a -> b -> m a) -> a -> [b] -> m a
checkFold (Bool -> AccessContext -> TypedBinding -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> TypedBinding -> m AccessContext
checkTypedBinding Bool
b)

-- ## Patterns
 
checkPattern
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> Pattern
  -> m AccessContext
checkPattern :: AccessContext -> Pattern -> m AccessContext
checkPattern c :: AccessContext
c (IdentP n :: QName
n)
  = AccessContext -> QName -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
AccessContext -> QName -> m AccessContext
checkQNameP' AccessContext
c QName
n
checkPattern _ (QuoteP _)
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkPattern c :: AccessContext
c (RawAppP _ ps :: [Pattern]
ps)
  = AccessContext -> [Pattern] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Pattern] -> m AccessContext
checkRawAppP AccessContext
c [Pattern]
ps
checkPattern _ (OpAppP r :: Range
r _ _ _)
  = Error -> m AccessContext
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Range -> Error
ErrorInternal (UnexpectedError -> InternalError
ErrorUnexpected UnexpectedError
UnexpectedOpAppP) Range
r)
checkPattern c :: AccessContext
c (HiddenP _ (Named _ p :: Pattern
p))
  = AccessContext -> Pattern -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern AccessContext
c Pattern
p
checkPattern c :: AccessContext
c (InstanceP _ (Named _ p :: Pattern
p))
  = AccessContext -> Pattern -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern AccessContext
c Pattern
p
checkPattern c :: AccessContext
c (ParenP _ p :: Pattern
p)
  = AccessContext -> Pattern -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern AccessContext
c Pattern
p
checkPattern _ (WildP _)
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkPattern _ (AbsurdP _)
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkPattern c :: AccessContext
c (DotP _ e :: Expr
e)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkPattern _ (LitP _)
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkPattern c :: AccessContext
c (RecP _ as :: [FieldAssignment' Pattern]
as)
  = AccessContext -> [Pattern] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Pattern] -> m AccessContext
checkPatterns AccessContext
c (FieldAssignment' Pattern -> Pattern
forall a. FieldAssignment' a -> a
_exprFieldA (FieldAssignment' Pattern -> Pattern)
-> [FieldAssignment' Pattern] -> [Pattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FieldAssignment' Pattern]
as)
checkPattern c :: AccessContext
c (EqualP _ es :: [(Expr, Expr)]
es)
  = AccessContext -> [(Expr, Expr)] -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [(Expr, Expr)] -> m ()
checkExprPairs AccessContext
c [(Expr, Expr)]
es m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkPattern _ (EllipsisP _)
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkPattern c :: AccessContext
c (WithP _ p :: Pattern
p)
  = AccessContext -> Pattern -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern AccessContext
c Pattern
p

checkPattern c :: AccessContext
c (AppP p :: Pattern
p (Arg _ (Named _ p' :: Pattern
p')))
  = AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
(<>)
  (AccessContext -> AccessContext -> AccessContext)
-> m AccessContext -> m (AccessContext -> AccessContext)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AccessContext -> Pattern -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern AccessContext
c Pattern
p
  m (AccessContext -> AccessContext)
-> m AccessContext -> m AccessContext
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> AccessContext -> Pattern -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern AccessContext
c Pattern
p'

checkPattern c :: AccessContext
c (AsP _ n :: Name
n p :: Pattern
p)
  = AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
(<>)
  (AccessContext -> AccessContext -> AccessContext)
-> m AccessContext -> m (AccessContext -> AccessContext)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
checkName' Bool
False Fixities
forall a. Monoid a => a
mempty Access
Public RangeType
RangeVariable Name
n
  m (AccessContext -> AccessContext)
-> m AccessContext -> m AccessContext
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> AccessContext -> Pattern -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern AccessContext
c Pattern
p

checkPatternMay
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> Maybe Pattern
  -> m AccessContext
checkPatternMay :: AccessContext -> Maybe Pattern -> m AccessContext
checkPatternMay _ Nothing
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkPatternMay c :: AccessContext
c (Just p :: Pattern
p)
  = AccessContext -> Pattern -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern AccessContext
c Pattern
p

checkPatterns
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [Pattern]
  -> m AccessContext
checkPatterns :: AccessContext -> [Pattern] -> m AccessContext
checkPatterns
  = (AccessContext -> Pattern -> m AccessContext)
-> AccessContext -> [Pattern] -> m AccessContext
forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence AccessContext -> Pattern -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern

checkRawAppP
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [Pattern]
  -> m AccessContext
checkRawAppP :: AccessContext -> [Pattern] -> m AccessContext
checkRawAppP c :: AccessContext
c ps :: [Pattern]
ps
  = [Name] -> m [Name]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([RawName] -> AccessContext -> [Name]
accessContextMatch ([Pattern] -> [RawName]
patternNames [Pattern]
ps) AccessContext
c)
  m [Name] -> ([Name] -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ns :: [Name]
ns -> AccessContext -> [Name] -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
AccessContext -> [Name] -> m ()
touchNames AccessContext
c [Name]
ns
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> [Pattern] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Pattern] -> m AccessContext
checkPatterns AccessContext
c ([Name] -> [Pattern] -> [Pattern]
patternDelete [Name]
ns [Pattern]
ps)

patternMatch
  :: [Name]
  -> Pattern
  -> Bool
patternMatch :: [Name] -> Pattern -> Bool
patternMatch ns :: [Name]
ns p :: Pattern
p
  = Bool -> (RawName -> Bool) -> Maybe RawName -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ((RawName -> [RawName] -> Bool) -> [RawName] -> RawName -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip RawName -> [RawName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem ([[RawName]] -> [RawName]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Name -> [RawName]
nameIds (Name -> [RawName]) -> [Name] -> [[RawName]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
ns))) (Pattern -> Maybe RawName
patternName Pattern
p)

patternDelete
  :: [Name]
  -> [Pattern]
  -> [Pattern]
patternDelete :: [Name] -> [Pattern] -> [Pattern]
patternDelete ns :: [Name]
ns
  = (Pattern -> Bool) -> [Pattern] -> [Pattern]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Pattern -> Bool) -> Pattern -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> Pattern -> Bool
patternMatch [Name]
ns)

patternName
  :: Pattern
  -> Maybe String
patternName :: Pattern -> Maybe RawName
patternName (IdentP (N.QName (N.Name _ _ [Id n :: RawName
n])))
  = RawName -> Maybe RawName
forall a. a -> Maybe a
Just RawName
n
patternName _
  = Maybe RawName
forall a. Maybe a
Nothing

patternNames
  :: [Pattern]
  -> [String]
patternNames :: [Pattern] -> [RawName]
patternNames
  = [Maybe RawName] -> [RawName]
forall a. [Maybe a] -> [a]
catMaybes
  ([Maybe RawName] -> [RawName])
-> ([Pattern] -> [Maybe RawName]) -> [Pattern] -> [RawName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pattern -> Maybe RawName) -> [Pattern] -> [Maybe RawName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> Maybe RawName
patternName

-- ## Expressions

checkExpr
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> Expr
  -> m ()
checkExpr :: AccessContext -> Expr -> m ()
checkExpr c :: AccessContext
c (Ident n :: QName
n)
  = AccessContext -> QName -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
AccessContext -> QName -> m ()
touchQName' AccessContext
c QName
n
checkExpr _ (Lit _)
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr _ (QuestionMark _ _)
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr _ (Underscore _ _)
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr c :: AccessContext
c (RawApp _ es :: [Expr]
es)
  = AccessContext -> [Expr] -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkRawApp AccessContext
c [Expr]
es
checkExpr c :: AccessContext
c (App _ e :: Expr
e (Arg _ (Named _ e' :: Expr
e')))
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e'
checkExpr _ (OpApp r :: Range
r _ _ _)
  = Error -> m ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Range -> Error
ErrorInternal (UnexpectedError -> InternalError
ErrorUnexpected UnexpectedError
UnexpectedOpApp) Range
r)
checkExpr c :: AccessContext
c (WithApp _ e :: Expr
e es :: [Expr]
es)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> [Expr] -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkExprs AccessContext
c [Expr]
es
checkExpr c :: AccessContext
c (HiddenArg _ (Named _ e :: Expr
e))
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e
checkExpr c :: AccessContext
c (InstanceArg _ (Named _ e :: Expr
e))
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e
checkExpr c :: AccessContext
c (Lam _ bs :: [LamBinding]
bs e :: Expr
e)
  = Bool -> AccessContext -> [LamBinding] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> [LamBinding] -> m AccessContext
checkLamBindings Bool
True AccessContext
c [LamBinding]
bs m AccessContext -> (AccessContext -> m ()) -> m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c' :: AccessContext
c' -> AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c') Expr
e
checkExpr _ (AbsurdLam _ _)
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr c :: AccessContext
c (ExtendedLam _ ls :: [LamClause]
ls)
  = AccessContext -> [LamClause] -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [LamClause] -> m ()
checkLamClauses_ AccessContext
c [LamClause]
ls
checkExpr c :: AccessContext
c (Fun _ (Arg _ e :: Expr
e) e' :: Expr
e')
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e'
checkExpr c :: AccessContext
c (Pi bs :: [TypedBinding]
bs e :: Expr
e)
  = Bool -> AccessContext -> [TypedBinding] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> [TypedBinding] -> m AccessContext
checkTypedBindings Bool
True AccessContext
c [TypedBinding]
bs m AccessContext -> (AccessContext -> m ()) -> m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c' :: AccessContext
c' -> AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c') Expr
e
checkExpr _ (Set _)
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr _ (Prop _)
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr _ (SetN _ _)
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr _ (PropN _ _)
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr c :: AccessContext
c (Rec _ rs :: RecordAssignments
rs)
  = AccessContext -> RecordAssignments -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> RecordAssignments -> m ()
checkRecordAssignments AccessContext
c RecordAssignments
rs
checkExpr c :: AccessContext
c (RecUpdate _ e :: Expr
e fs :: [FieldAssignment]
fs)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> [FieldAssignment] -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [FieldAssignment] -> m ()
checkFieldAssignments AccessContext
c [FieldAssignment]
fs
checkExpr c :: AccessContext
c (Paren _ e :: Expr
e)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e
checkExpr c :: AccessContext
c (IdiomBrackets _ es :: [Expr]
es)
  = AccessContext -> [Expr] -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkExprs AccessContext
c [Expr]
es
checkExpr c :: AccessContext
c (DoBlock _ ss :: [DoStmt]
ss)
  = m AccessContext -> m ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (AccessContext -> [DoStmt] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [DoStmt] -> m AccessContext
checkDoStmts AccessContext
c [DoStmt]
ss)
checkExpr _ (Absurd r :: Range
r)
  = Error -> m ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Range -> Error
ErrorInternal (UnexpectedError -> InternalError
ErrorUnexpected UnexpectedError
UnexpectedAbsurd) Range
r)
checkExpr _ (As r :: Range
r _ _)
  = Error -> m ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Range -> Error
ErrorInternal (UnexpectedError -> InternalError
ErrorUnexpected UnexpectedError
UnexpectedAs) Range
r)
checkExpr c :: AccessContext
c (Dot _ e :: Expr
e)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e
checkExpr c :: AccessContext
c (DoubleDot _ e :: Expr
e)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e
checkExpr _ e :: Expr
e@(ETel _)
  = Error -> m ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Range -> Error
ErrorInternal (UnexpectedError -> InternalError
ErrorUnexpected UnexpectedError
UnexpectedETel) (Expr -> Range
forall t. HasRange t => t -> Range
getRange Expr
e))
checkExpr _ (Quote _)
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr _ (QuoteTerm _)
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr c :: AccessContext
c (Tactic _ e :: Expr
e)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e
checkExpr _ (Unquote _)
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkExpr _ e :: Expr
e@(DontCare _)
  = Error -> m ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Range -> Error
ErrorInternal (UnexpectedError -> InternalError
ErrorUnexpected UnexpectedError
UnexpectedDontCare) (Expr -> Range
forall t. HasRange t => t -> Range
getRange Expr
e))
checkExpr _ (Equal r :: Range
r _ _)
  = Error -> m ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Range -> Error
ErrorInternal (UnexpectedError -> InternalError
ErrorUnexpected UnexpectedError
UnexpectedEqual) Range
r)
checkExpr _ (Ellipsis r :: Range
r)
  = Error -> m ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Range -> Error
ErrorInternal (UnexpectedError -> InternalError
ErrorUnexpected UnexpectedError
UnexpectedEllipsis) Range
r)
checkExpr c :: AccessContext
c (Generalized e :: Expr
e)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e

checkExpr c :: AccessContext
c (Let _ ds :: [Declaration]
ds e :: Maybe Expr
e)
  = AccessContext -> [Declaration] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Declaration] -> m AccessContext
checkDeclarations AccessContext
c [Declaration]
ds
  m AccessContext -> (AccessContext -> m ()) -> m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c' :: AccessContext
c' -> m () -> (Expr -> m ()) -> Maybe Expr -> m ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) (AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c')) Maybe Expr
e

checkExprs
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [Expr]
  -> m ()
checkExprs :: AccessContext -> [Expr] -> m ()
checkExprs
  = (AccessContext -> Expr -> m ()) -> AccessContext -> [Expr] -> m ()
forall (m :: * -> *) a b.
Monad m =>
(a -> b -> m ()) -> a -> [b] -> m ()
checkSequence_ AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr

checkExprPair
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> (Expr, Expr)
  -> m ()
checkExprPair :: AccessContext -> (Expr, Expr) -> m ()
checkExprPair c :: AccessContext
c (e1 :: Expr
e1, e2 :: Expr
e2)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e1 m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e2

checkExprPairs
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [(Expr, Expr)]
  -> m ()
checkExprPairs :: AccessContext -> [(Expr, Expr)] -> m ()
checkExprPairs
  = (AccessContext -> (Expr, Expr) -> m ())
-> AccessContext -> [(Expr, Expr)] -> m ()
forall (m :: * -> *) a b.
Monad m =>
(a -> b -> m ()) -> a -> [b] -> m ()
checkSequence_ AccessContext -> (Expr, Expr) -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> (Expr, Expr) -> m ()
checkExprPair

checkRawApp
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [Expr]
  -> m ()
checkRawApp :: AccessContext -> [Expr] -> m ()
checkRawApp c :: AccessContext
c es :: [Expr]
es
  = AccessContext -> [Name] -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
AccessContext -> [Name] -> m ()
touchNames AccessContext
c ([RawName] -> AccessContext -> [Name]
accessContextMatch ([Expr] -> [RawName]
exprNames [Expr]
es) AccessContext
c)
  m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> [Expr] -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkExprs AccessContext
c [Expr]
es

exprName
  :: Expr
  -> Maybe String
exprName :: Expr -> Maybe RawName
exprName (Ident (N.QName (N.Name _ _ [Id n :: RawName
n])))
  = RawName -> Maybe RawName
forall a. a -> Maybe a
Just RawName
n
exprName _
  = Maybe RawName
forall a. Maybe a
Nothing

exprNames
  :: [Expr]
  -> [String]
exprNames :: [Expr] -> [RawName]
exprNames
  = [Maybe RawName] -> [RawName]
forall a. [Maybe a] -> [a]
catMaybes
  ([Maybe RawName] -> [RawName])
-> ([Expr] -> [Maybe RawName]) -> [Expr] -> [RawName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Maybe RawName) -> [Expr] -> [Maybe RawName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr -> Maybe RawName
exprName

-- ## Assignments

checkRecordAssignment
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> RecordAssignment
  -> m ()
checkRecordAssignment :: AccessContext -> RecordAssignment -> m ()
checkRecordAssignment c :: AccessContext
c (Left f :: FieldAssignment
f)
  = AccessContext -> FieldAssignment -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> FieldAssignment -> m ()
checkFieldAssignment AccessContext
c FieldAssignment
f
checkRecordAssignment c :: AccessContext
c (Right m :: ModuleAssignment
m)
  = AccessContext -> ModuleAssignment -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> ModuleAssignment -> m ()
checkModuleAssignment AccessContext
c ModuleAssignment
m

checkRecordAssignments
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [RecordAssignment]
  -> m ()
checkRecordAssignments :: AccessContext -> RecordAssignments -> m ()
checkRecordAssignments
  = (AccessContext -> RecordAssignment -> m ())
-> AccessContext -> RecordAssignments -> m ()
forall (m :: * -> *) a b.
Monad m =>
(a -> b -> m ()) -> a -> [b] -> m ()
checkSequence_ AccessContext -> RecordAssignment -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> RecordAssignment -> m ()
checkRecordAssignment

checkFieldAssignment
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> FieldAssignment
  -> m ()
checkFieldAssignment :: AccessContext -> FieldAssignment -> m ()
checkFieldAssignment c :: AccessContext
c (FieldAssignment _ e :: Expr
e)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e

checkFieldAssignments
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [FieldAssignment]
  -> m ()
checkFieldAssignments :: AccessContext -> [FieldAssignment] -> m ()
checkFieldAssignments
  = (AccessContext -> FieldAssignment -> m ())
-> AccessContext -> [FieldAssignment] -> m ()
forall (m :: * -> *) a b.
Monad m =>
(a -> b -> m ()) -> a -> [b] -> m ()
checkSequence_ AccessContext -> FieldAssignment -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> FieldAssignment -> m ()
checkFieldAssignment

checkModuleAssignment
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> ModuleAssignment
  -> m ()
checkModuleAssignment :: AccessContext -> ModuleAssignment -> m ()
checkModuleAssignment c :: AccessContext
c a :: ModuleAssignment
a@(ModuleAssignment n :: QName
n es :: [Expr]
es _)
  = AccessContext -> [Expr] -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkExprs AccessContext
c [Expr]
es
  m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> m () -> (QName -> m ()) -> Maybe QName -> m ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) (AccessContext -> Range -> QName -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
AccessContext -> Range -> QName -> m ()
touchModule AccessContext
c (ModuleAssignment -> Range
forall t. HasRange t => t -> Range
getRange ModuleAssignment
a)) (QName -> Maybe QName
fromQName QName
n)

-- ## Definitions

checkLHS
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> LHS
  -> m AccessContext
checkLHS :: AccessContext -> LHS -> m AccessContext
checkLHS c :: AccessContext
c (LHS p :: Pattern
p rs :: [RewriteEqn]
rs ws :: [WithHiding Expr]
ws _)
  = AccessContext -> Pattern -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern AccessContext
c Pattern
p
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c' :: AccessContext
c' -> AccessContext -> [RewriteEqn] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [RewriteEqn] -> m AccessContext
checkRewriteEqns (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c') [RewriteEqn]
rs
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'' :: AccessContext
c'' -> AccessContext -> [Expr] -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkExprs (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c' AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c'') (WithHiding Expr -> Expr
forall a. WithHiding a -> a
whThing (WithHiding Expr -> Expr) -> [WithHiding Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [WithHiding Expr]
ws)
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
c' AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c'')

checkRHS
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> RHS
  -> m ()
checkRHS :: AccessContext -> RHS -> m ()
checkRHS _ AbsurdRHS
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
checkRHS c :: AccessContext
c (RHS e :: Expr
e)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e

checkClause
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> Clause
  -> m AccessContext
checkClause :: AccessContext -> Clause -> m AccessContext
checkClause c :: AccessContext
c (Clause n :: Name
n _ l :: LHS
l r :: RHS
r w :: WhereClause
w cs :: [Clause]
cs)
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((AccessContext -> AccessContext)
-> (Name -> AccessContext -> AccessContext)
-> Maybe Name
-> AccessContext
-> AccessContext
forall b a. b -> (a -> b) -> Maybe a -> b
maybe AccessContext -> AccessContext
forall a. a -> a
id Name -> AccessContext -> AccessContext
accessContextDefine (Name -> Maybe Name
fromName Name
n) AccessContext
c)
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c' :: AccessContext
c' -> AccessContext -> LHS -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> LHS -> m AccessContext
checkLHS AccessContext
c' LHS
l
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'' :: AccessContext
c'' -> AccessContext -> WhereClause -> m (AccessContext, AccessContext)
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> WhereClause -> m (AccessContext, AccessContext)
checkWhereClause (AccessContext
c' AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c'') WhereClause
w
  m (AccessContext, AccessContext)
-> ((AccessContext, AccessContext) -> m AccessContext)
-> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(m :: AccessContext
m, c''' :: AccessContext
c''') -> AccessContext -> RHS -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> RHS -> m ()
checkRHS (AccessContext
c' AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c'' AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c''') RHS
r
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> [Clause] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Clause] -> m AccessContext
checkClauses (AccessContext
c' AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c'' AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c''') [Clause]
cs
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \m' :: AccessContext
m' -> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
m AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
m')

checkClauses
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [Clause]
  -> m AccessContext
checkClauses :: AccessContext -> [Clause] -> m AccessContext
checkClauses
  = (AccessContext -> Clause -> m AccessContext)
-> AccessContext -> [Clause] -> m AccessContext
forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence AccessContext -> Clause -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Clause -> m AccessContext
checkClause

checkLamClause
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> LamClause
  -> m AccessContext
checkLamClause :: AccessContext -> LamClause -> m AccessContext
checkLamClause c :: AccessContext
c (LamClause l :: LHS
l r :: RHS
r _ _)
  = AccessContext -> LHS -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> LHS -> m AccessContext
checkLHS AccessContext
c LHS
l
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c' :: AccessContext
c' -> AccessContext -> RHS -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> RHS -> m ()
checkRHS (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c') RHS
r
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
c'

checkLamClauses
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [LamClause]
  -> m AccessContext
checkLamClauses :: AccessContext -> [LamClause] -> m AccessContext
checkLamClauses
  = (AccessContext -> LamClause -> m AccessContext)
-> AccessContext -> [LamClause] -> m AccessContext
forall (m :: * -> *) a b.
(Monad m, Monoid a) =>
(a -> b -> m a) -> a -> [b] -> m a
checkFold AccessContext -> LamClause -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> LamClause -> m AccessContext
checkLamClause

checkLamClause_
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> LamClause
  -> m ()
checkLamClause_ :: AccessContext -> LamClause -> m ()
checkLamClause_ c :: AccessContext
c ls :: LamClause
ls
  = m AccessContext -> m ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (AccessContext -> LamClause -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> LamClause -> m AccessContext
checkLamClause AccessContext
c LamClause
ls)

-- Do not propogate context from one clause to the next.
checkLamClauses_
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [LamClause]
  -> m ()
checkLamClauses_ :: AccessContext -> [LamClause] -> m ()
checkLamClauses_
  = (AccessContext -> LamClause -> m ())
-> AccessContext -> [LamClause] -> m ()
forall (m :: * -> *) a b.
Monad m =>
(a -> b -> m ()) -> a -> [b] -> m ()
checkSequence_ AccessContext -> LamClause -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> LamClause -> m ()
checkLamClause_

checkWhereClause
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> WhereClause
  -> m (AccessContext, AccessContext)
  -- ^ A context for the named where block, then the full context.
checkWhereClause :: AccessContext -> WhereClause -> m (AccessContext, AccessContext)
checkWhereClause _ NoWhere
  = (AccessContext, AccessContext) -> m (AccessContext, AccessContext)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
forall a. Monoid a => a
mempty, AccessContext
forall a. Monoid a => a
mempty)
checkWhereClause c :: AccessContext
c (AnyWhere ds :: [Declaration]
ds)
  = AccessContext -> [Declaration] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Declaration] -> m AccessContext
checkDeclarations AccessContext
c [Declaration]
ds
  m AccessContext
-> (AccessContext -> m (AccessContext, AccessContext))
-> m (AccessContext, AccessContext)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c' :: AccessContext
c' -> (AccessContext, AccessContext) -> m (AccessContext, AccessContext)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
forall a. Monoid a => a
mempty, AccessContext
c')
checkWhereClause c :: AccessContext
c (SomeWhere n :: Name
n a :: Access
a ds :: [Declaration]
ds)
  = Error -> Maybe Name -> m Name
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
n)) (Name -> Maybe Name
fromName Name
n)
  m Name
-> (Name -> m (AccessContext, AccessContext))
-> m (AccessContext, AccessContext)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \n' :: Name
n' -> AccessContext -> [Declaration] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Declaration] -> m AccessContext
checkDeclarations AccessContext
c [Declaration]
ds
  m AccessContext
-> (AccessContext -> m (AccessContext, AccessContext))
-> m (AccessContext, AccessContext)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c' :: AccessContext
c' -> Context -> Access -> Range -> Name -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Context -> Access -> Range -> Name -> m AccessContext
checkModuleName (AccessContext -> Context
toContext AccessContext
c') (Access -> Access
fromAccess Access
a) (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
n) Name
n'
  m AccessContext
-> (AccessContext -> m (AccessContext, AccessContext))
-> m (AccessContext, AccessContext)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'' :: AccessContext
c'' -> (AccessContext, AccessContext) -> m (AccessContext, AccessContext)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
c'' , AccessContext
c')

checkRewriteEqn
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> RewriteEqn
  -> m AccessContext
checkRewriteEqn :: AccessContext -> RewriteEqn -> m AccessContext
checkRewriteEqn c :: AccessContext
c (Rewrite rs :: [((), Expr)]
rs)
  = AccessContext -> [Expr] -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkExprs AccessContext
c (((), Expr) -> Expr
forall a b. (a, b) -> b
snd (((), Expr) -> Expr) -> [((), Expr)] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [((), Expr)]
rs) m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkRewriteEqn c :: AccessContext
c (Invert _ ws :: [(Pattern, Expr)]
ws)
  = AccessContext -> [(Pattern, Expr)] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [(Pattern, Expr)] -> m AccessContext
checkIrrefutableWiths AccessContext
c [(Pattern, Expr)]
ws

checkRewriteEqns
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [RewriteEqn]
  -> m AccessContext
checkRewriteEqns :: AccessContext -> [RewriteEqn] -> m AccessContext
checkRewriteEqns
  = (AccessContext -> RewriteEqn -> m AccessContext)
-> AccessContext -> [RewriteEqn] -> m AccessContext
forall (m :: * -> *) a b.
(Monad m, Monoid a) =>
(a -> b -> m a) -> a -> [b] -> m a
checkFold AccessContext -> RewriteEqn -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> RewriteEqn -> m AccessContext
checkRewriteEqn

checkIrrefutableWith
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> (Pattern, Expr)
  -> m AccessContext
checkIrrefutableWith :: AccessContext -> (Pattern, Expr) -> m AccessContext
checkIrrefutableWith c :: AccessContext
c (p :: Pattern
p, e :: Expr
e)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> Pattern -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern AccessContext
c Pattern
p

checkIrrefutableWiths
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [(Pattern, Expr)]
  -> m AccessContext
checkIrrefutableWiths :: AccessContext -> [(Pattern, Expr)] -> m AccessContext
checkIrrefutableWiths
  = (AccessContext -> (Pattern, Expr) -> m AccessContext)
-> AccessContext -> [(Pattern, Expr)] -> m AccessContext
forall (m :: * -> *) a b.
(Monad m, Monoid a) =>
(a -> b -> m a) -> a -> [b] -> m a
checkFold AccessContext -> (Pattern, Expr) -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> (Pattern, Expr) -> m AccessContext
checkIrrefutableWith

checkDoStmt
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> DoStmt
  -> m AccessContext
checkDoStmt :: AccessContext -> DoStmt -> m AccessContext
checkDoStmt c :: AccessContext
c (DoBind _ p :: Pattern
p e :: Expr
e cs :: [LamClause]
cs)
  = AccessContext -> [LamClause] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [LamClause] -> m AccessContext
checkLamClauses AccessContext
c [LamClause]
cs
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c' :: AccessContext
c' -> AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c') Expr
e
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> Pattern -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c') Pattern
p
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'' :: AccessContext
c'' -> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
c' AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c'')
checkDoStmt c :: AccessContext
c (DoThen e :: Expr
e)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkDoStmt c :: AccessContext
c (DoLet _ ds :: [Declaration]
ds)
  = AccessContext -> [Declaration] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Declaration] -> m AccessContext
checkDeclarations AccessContext
c [Declaration]
ds

checkDoStmts
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [DoStmt]
  -> m AccessContext
checkDoStmts :: AccessContext -> [DoStmt] -> m AccessContext
checkDoStmts c :: AccessContext
c ss :: [DoStmt]
ss
  = m () -> m () -> Bool -> m ()
forall a. a -> a -> Bool -> a
bool (() -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) (AccessContext -> Name -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
AccessContext -> Name -> m ()
touchName AccessContext
c Name
bind) ([DoStmt] -> Bool
hasBind [DoStmt]
ss)
  m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> m () -> m () -> Bool -> m ()
forall a. a -> a -> Bool -> a
bool (() -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) (AccessContext -> Name -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
AccessContext -> Name -> m ()
touchName AccessContext
c Name
bind_) ([DoStmt] -> Bool
hasBind_ [DoStmt]
ss)
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (AccessContext -> DoStmt -> m AccessContext)
-> AccessContext -> [DoStmt] -> m AccessContext
forall (m :: * -> *) a b.
(Monad m, Monoid a) =>
(a -> b -> m a) -> a -> [b] -> m a
checkFold AccessContext -> DoStmt -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> DoStmt -> m AccessContext
checkDoStmt AccessContext
c [DoStmt]
ss

hasBind
  :: [DoStmt]
  -> Bool
hasBind :: [DoStmt] -> Bool
hasBind []
  = Bool
False
hasBind (_ : [])
  = Bool
False
hasBind (DoBind _ _ _ _ : _ : _)
  = Bool
True
hasBind (_ : ss :: [DoStmt]
ss)
  = [DoStmt] -> Bool
hasBind [DoStmt]
ss

hasBind_
  :: [DoStmt]
  -> Bool
hasBind_ :: [DoStmt] -> Bool
hasBind_ []
  = Bool
False
hasBind_ (_ : [])
  = Bool
False
hasBind_ (DoThen _ : _ : _)
  = Bool
True
hasBind_ (_ : ss :: [DoStmt]
ss)
  = [DoStmt] -> Bool
hasBind_ [DoStmt]
ss

bind
  :: Name
bind :: Name
bind
  = [NamePart] -> Name
Name
  [ NamePart
Hole
  , RawName -> NamePart
Id ">>="
  , NamePart
Hole
  ]

bind_
  :: Name
bind_ :: Name
bind_
  = [NamePart] -> Name
Name
  [ NamePart
Hole
  , RawName -> NamePart
Id ">>"
  , NamePart
Hole
  ]

-- ## Declarations

checkDeclarations
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [Declaration]
  -> m AccessContext
checkDeclarations :: AccessContext -> [Declaration] -> m AccessContext
checkDeclarations
  = (Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext)
-> AccessContext -> [Declaration] -> m AccessContext
forall (m :: * -> *).
MonadError Error m =>
(Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext)
-> AccessContext -> [Declaration] -> m AccessContext
checkDeclarationsWith Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
checkNiceDeclarations

checkDeclarationsRecord
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Name
  -> [Range]
  -- ^ Ranges associated with parent record.
  -> AccessContext
  -> [Declaration]
  -> m AccessContext
checkDeclarationsRecord :: Name
-> [Range] -> AccessContext -> [Declaration] -> m AccessContext
checkDeclarationsRecord n :: Name
n rs :: [Range]
rs
  = (Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext)
-> AccessContext -> [Declaration] -> m AccessContext
forall (m :: * -> *).
MonadError Error m =>
(Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext)
-> AccessContext -> [Declaration] -> m AccessContext
checkDeclarationsWith (Name
-> [Range]
-> Fixities
-> AccessContext
-> [NiceDeclaration]
-> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Name
-> [Range]
-> Fixities
-> AccessContext
-> [NiceDeclaration]
-> m AccessContext
checkNiceDeclarationsRecord Name
n [Range]
rs)

checkDeclarationsTop
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> [Declaration]
  -> m AccessContext
checkDeclarationsTop :: AccessContext -> [Declaration] -> m AccessContext
checkDeclarationsTop
  = (Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext)
-> AccessContext -> [Declaration] -> m AccessContext
forall (m :: * -> *).
MonadError Error m =>
(Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext)
-> AccessContext -> [Declaration] -> m AccessContext
checkDeclarationsWith Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
checkNiceDeclarationsTop

checkDeclarationsWith
  :: MonadError Error m
  => (Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext)
  -> AccessContext
  -> [Declaration]
  -> m AccessContext
checkDeclarationsWith :: (Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext)
-> AccessContext -> [Declaration] -> m AccessContext
checkDeclarationsWith f :: Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
f c :: AccessContext
c ds :: [Declaration]
ds = do
  (fixities :: Fixities
fixities, _)
    <- DoWarn -> [Declaration] -> m (Fixities, Polarities)
forall (m :: * -> *).
MonadFixityError m =>
DoWarn -> [Declaration] -> m (Fixities, Polarities)
fixitiesAndPolarities DoWarn
NoWarn [Declaration]
ds
  (niceDeclsEither :: Either DeclarationException [NiceDeclaration]
niceDeclsEither, _) 
    <- (Either DeclarationException [NiceDeclaration], NiceWarnings)
-> m (Either DeclarationException [NiceDeclaration], NiceWarnings)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Nice [NiceDeclaration]
-> (Either DeclarationException [NiceDeclaration], NiceWarnings)
forall a. Nice a -> (Either DeclarationException a, NiceWarnings)
runNice (Fixities -> [Declaration] -> Nice [NiceDeclaration]
niceDeclarations Fixities
fixities [Declaration]
ds))
  [NiceDeclaration]
niceDecls
    <- Either Error [NiceDeclaration] -> m [NiceDeclaration]
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither ((DeclarationException -> Error)
-> Either DeclarationException [NiceDeclaration]
-> Either Error [NiceDeclaration]
forall e f a. (e -> f) -> Either e a -> Either f a
mapLeft DeclarationException -> Error
ErrorDeclaration Either DeclarationException [NiceDeclaration]
niceDeclsEither)
  Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
f Fixities
fixities AccessContext
c [NiceDeclaration]
niceDecls

checkNiceDeclaration
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Fixities
  -> AccessContext
  -> NiceDeclaration
  -> m AccessContext

checkNiceDeclaration :: Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration fs :: Fixities
fs c :: AccessContext
c (Axiom _ a :: Access
a _ _ _ n :: Name
n e :: Expr
e)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
checkName' Bool
False Fixities
fs (Access -> Access
fromAccess Access
a) RangeType
RangePostulate Name
n
checkNiceDeclaration _ _ (NiceField r :: Range
r _ _ _ _ _ _)
  = Error -> m AccessContext
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Range -> Error
ErrorInternal (UnexpectedError -> InternalError
ErrorUnexpected UnexpectedError
UnexpectedField) Range
r)
checkNiceDeclaration fs :: Fixities
fs c :: AccessContext
c (PrimitiveFunction _ a :: Access
a _ n :: Name
n e :: Expr
e)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
checkName' Bool
False Fixities
fs (Access -> Access
fromAccess Access
a) RangeType
RangeDefinition Name
n
checkNiceDeclaration _ c :: AccessContext
c (NiceModule r :: Range
r a :: Access
a _ (N.QName n :: Name
n) bs :: [TypedBinding]
bs ds :: [Declaration]
ds)
  = AccessContext
-> Access
-> Range
-> Maybe Name
-> [TypedBinding]
-> [Declaration]
-> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext
-> Access
-> Range
-> Maybe Name
-> [TypedBinding]
-> [Declaration]
-> m AccessContext
checkNiceModule AccessContext
c (Access -> Access
fromAccess Access
a) Range
r (Name -> Maybe Name
fromName Name
n) [TypedBinding]
bs [Declaration]
ds
checkNiceDeclaration _ _ (NiceModule _ _ _ n :: QName
n@(N.Qual _ _) _ _)
  = Error -> m AccessContext
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
n))
checkNiceDeclaration _ _ (NicePragma _ _)
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkNiceDeclaration fs :: Fixities
fs c :: AccessContext
c (NiceRecSig _ a :: Access
a _ _ _ n :: Name
n bs :: [LamBinding]
bs e :: Expr
e)
  = Fixities
-> AccessContext
-> Access
-> RangeType
-> Name
-> [LamBinding]
-> Expr
-> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities
-> AccessContext
-> Access
-> RangeType
-> Name
-> [LamBinding]
-> Expr
-> m AccessContext
checkNiceSig Fixities
fs AccessContext
c Access
a RangeType
RangeRecord Name
n [LamBinding]
bs Expr
e
checkNiceDeclaration fs :: Fixities
fs c :: AccessContext
c (NiceDataSig _ a :: Access
a _ _ _ n :: Name
n bs :: [LamBinding]
bs e :: Expr
e)
  = Fixities
-> AccessContext
-> Access
-> RangeType
-> Name
-> [LamBinding]
-> Expr
-> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities
-> AccessContext
-> Access
-> RangeType
-> Name
-> [LamBinding]
-> Expr
-> m AccessContext
checkNiceSig Fixities
fs AccessContext
c Access
a RangeType
RangeData Name
n [LamBinding]
bs Expr
e
checkNiceDeclaration _ _ (NiceFunClause r :: Range
r _ _ _ _ _ _)
  = Error -> m AccessContext
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Range -> Error
ErrorInternal (UnexpectedError -> InternalError
ErrorUnexpected UnexpectedError
UnexpectedNiceFunClause) Range
r)
checkNiceDeclaration fs :: Fixities
fs c :: AccessContext
c (FunSig _ a :: Access
a _ _ _ _ _ _ n :: Name
n e :: Expr
e)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
checkName' Bool
False Fixities
fs (Access -> Access
fromAccess Access
a) RangeType
RangeDefinition Name
n
checkNiceDeclaration _ c :: AccessContext
c (FunDef _ _ _ _ _ _ _ cs :: [Clause]
cs)
  = AccessContext -> [Clause] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Clause] -> m AccessContext
checkClauses AccessContext
c [Clause]
cs m AccessContext -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkNiceDeclaration _ c :: AccessContext
c (NiceGeneralize _ _ _ _ _ e :: Expr
e)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkNiceDeclaration _ _ (NiceUnquoteDecl r :: Range
r _ _ _ _ _ _ _)
  = Error -> m AccessContext
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnsupportedError -> Range -> Error
ErrorUnsupported UnsupportedError
UnsupportedUnquote Range
r)
checkNiceDeclaration _ _ (NiceUnquoteDef r :: Range
r _ _ _ _ _ _)
  = Error -> m AccessContext
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnsupportedError -> Range -> Error
ErrorUnsupported UnsupportedError
UnsupportedUnquote Range
r)

checkNiceDeclaration fs :: Fixities
fs c :: AccessContext
c
  (NiceMutual _ _ _ _
    ds :: [NiceDeclaration]
ds@(NiceRecSig _ _ _ _ _ _ _ _ : NiceRecDef _ _ _ _ _ _ _ _ _ _ _ : _))
  = Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
checkNiceDeclarations Fixities
fs AccessContext
c [NiceDeclaration]
ds
checkNiceDeclaration fs :: Fixities
fs c :: AccessContext
c
  (NiceMutual _ _ _ _
    ds :: [NiceDeclaration]
ds@(NiceDataSig _ _ _ _ _ _ _ _ : NiceDataDef _ _ _ _ _ _ _ _ : _))
  = Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
checkNiceDeclarations Fixities
fs AccessContext
c [NiceDeclaration]
ds
checkNiceDeclaration fs :: Fixities
fs c :: AccessContext
c
  (NiceMutual _ _ _ _
    ds :: [NiceDeclaration]
ds@(FunSig _ _ _ _ _ _ _ _ _ _ : FunDef _ _ _ _ _ _ _ _ : _))
  = Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
checkNiceDeclarations Fixities
fs AccessContext
c [NiceDeclaration]
ds
checkNiceDeclaration fs :: Fixities
fs c :: AccessContext
c (NiceMutual r :: Range
r _ _ _ ds :: [NiceDeclaration]
ds)
  = Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
checkNiceDeclarations Fixities
fs AccessContext
c [NiceDeclaration]
ds
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c' :: AccessContext
c' -> Range -> RangeInfo -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Range -> RangeInfo -> m ()
modifyInsert Range
r RangeInfo
RangeMutual
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Range -> AccessContext -> m AccessContext
forall (m :: * -> *).
MonadReader Environment m =>
Range -> AccessContext -> m AccessContext
accessContextInsertRangeAll Range
r AccessContext
c'

checkNiceDeclaration _ c :: AccessContext
c
  (NiceModuleMacro r :: Range
r _ (N.NoName _ _)
    (SectionApp _ [] (RawApp _ (Ident n :: QName
n : es :: [Expr]
es))) DoOpen i :: ImportDirective
i)
  = Error -> Maybe QName -> m QName
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
n)) (QName -> Maybe QName
fromQName QName
n)
  m QName -> (QName -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \n' :: QName
n' -> Range -> QName -> Either LookupError Module -> m Module
forall (m :: * -> *) a.
MonadError Error m =>
Range -> QName -> Either LookupError a -> m a
liftLookup Range
r QName
n' (QName -> AccessContext -> Either LookupError Module
accessContextLookupModule QName
n' AccessContext
c)
  m Module -> (Module -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(C.Module rs :: [Range]
rs c' :: Context
c') -> [Range] -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
[Range] -> m ()
modifyDelete [Range]
rs
  m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> [Expr] -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkExprs AccessContext
c [Expr]
es
  m () -> m Context -> m Context
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
checkImportDirective DirectiveType
Open Range
r QName
n' Context
c' ImportDirective
i
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext -> m AccessContext)
-> (Context -> AccessContext) -> Context -> m AccessContext
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Access -> Context -> AccessContext
fromContext (ImportDirective -> Access
importDirectiveAccess ImportDirective
i)
checkNiceDeclaration _ c :: AccessContext
c
  (NiceModuleMacro r :: Range
r a :: Access
a a' :: Name
a'
    (SectionApp _ bs :: [TypedBinding]
bs (RawApp _ (Ident n :: QName
n : es :: [Expr]
es))) DontOpen i :: ImportDirective
i)
  = Error -> Maybe QName -> m QName
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
n)) (QName -> Maybe QName
fromQName QName
n)
  m QName -> (QName -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \n' :: QName
n' -> Error -> Maybe Name -> m Name
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
a')) (Name -> Maybe Name
fromName Name
a')
  m Name -> (Name -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a'' :: Name
a'' -> Range -> QName -> Either LookupError Module -> m Module
forall (m :: * -> *) a.
MonadError Error m =>
Range -> QName -> Either LookupError a -> m a
liftLookup Range
r QName
n' (QName -> AccessContext -> Either LookupError Module
accessContextLookupModule QName
n' AccessContext
c)
  m Module -> (Module -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(C.Module rs :: [Range]
rs c' :: Context
c') -> [Range] -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
[Range] -> m ()
modifyDelete [Range]
rs
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> AccessContext -> [TypedBinding] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> [TypedBinding] -> m AccessContext
checkTypedBindings Bool
True AccessContext
c [TypedBinding]
bs
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'' :: AccessContext
c'' -> AccessContext -> [Expr] -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkExprs (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c'') [Expr]
es
  m () -> m Context -> m Context
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
checkImportDirective DirectiveType
Module Range
r (Name -> QName
QName Name
a'') Context
c' ImportDirective
i
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c''' :: Context
c''' -> Context -> Access -> Range -> Name -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Context -> Access -> Range -> Name -> m AccessContext
checkModuleName Context
c''' (Access -> Access
fromAccess Access
a) Range
r Name
a''
checkNiceDeclaration _ c :: AccessContext
c
  (NiceModuleMacro r :: Range
r a :: Access
a a' :: Name
a'
    (SectionApp _ bs :: [TypedBinding]
bs (RawApp _ (Ident n :: QName
n : es :: [Expr]
es))) DoOpen i :: ImportDirective
i)
  = Error -> Maybe QName -> m QName
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
n)) (QName -> Maybe QName
fromQName QName
n)
  m QName -> (QName -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \n' :: QName
n' -> Error -> Maybe Name -> m Name
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
a')) (Name -> Maybe Name
fromName Name
a')
  m Name -> (Name -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a'' :: Name
a'' -> Range -> QName -> Either LookupError Module -> m Module
forall (m :: * -> *) a.
MonadError Error m =>
Range -> QName -> Either LookupError a -> m a
liftLookup Range
r QName
n' (QName -> AccessContext -> Either LookupError Module
accessContextLookupModule QName
n' AccessContext
c)
  m Module -> (Module -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(C.Module rs :: [Range]
rs c' :: Context
c') -> [Range] -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
[Range] -> m ()
modifyDelete [Range]
rs
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> AccessContext -> [TypedBinding] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> [TypedBinding] -> m AccessContext
checkTypedBindings Bool
True AccessContext
c [TypedBinding]
bs
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'' :: AccessContext
c'' -> AccessContext -> [Expr] -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Expr] -> m ()
checkExprs (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c'') [Expr]
es
  m () -> m Context -> m Context
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
checkImportDirective DirectiveType
Module Range
r (Name -> QName
QName Name
a'') Context
c' ImportDirective
i
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c''' :: Context
c''' -> Context -> Access -> Range -> Name -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Context -> Access -> Range -> Name -> m AccessContext
checkModuleName Context
c''' (Access -> Access
fromAccess Access
a) Range
r Name
a''
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'''' :: AccessContext
c'''' -> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
c'''' AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> Access -> Context -> AccessContext
fromContext (ImportDirective -> Access
importDirectiveAccess ImportDirective
i) Context
c''')
checkNiceDeclaration _ _
  (NiceModuleMacro _ _ _
    (SectionApp r :: Range
r _ _) _ _)
  = Error -> m AccessContext
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorMacro Range
r)
checkNiceDeclaration _ _
  (NiceModuleMacro r :: Range
r _ _
    (RecordModuleInstance _ _) _ _)
  = Error -> m AccessContext
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnsupportedError -> Range -> Error
ErrorUnsupported UnsupportedError
UnsupportedMacro Range
r)

checkNiceDeclaration _ c :: AccessContext
c (NiceOpen r :: Range
r n :: QName
n i :: ImportDirective
i)
  = Error -> Maybe QName -> m QName
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
n)) (QName -> Maybe QName
fromQName QName
n)
  m QName -> (QName -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \n' :: QName
n' -> Range -> QName -> Either LookupError Module -> m Module
forall (m :: * -> *) a.
MonadError Error m =>
Range -> QName -> Either LookupError a -> m a
liftLookup Range
r QName
n' (QName -> AccessContext -> Either LookupError Module
accessContextLookupModule QName
n' AccessContext
c)
  m Module -> (Module -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(C.Module rs :: [Range]
rs c' :: Context
c') -> [Range] -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
[Range] -> m ()
modifyDelete [Range]
rs
  m () -> m Context -> m Context
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
checkImportDirective DirectiveType
Open Range
r QName
n' Context
c' ImportDirective
i
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'' :: Context
c'' -> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Access -> Context -> AccessContext
fromContext (ImportDirective -> Access
importDirectiveAccess ImportDirective
i) Context
c'')

checkNiceDeclaration _ _ (NiceImport r :: Range
r n :: QName
n Nothing DontOpen i :: ImportDirective
i)
  = Error -> Maybe QName -> m QName
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
n)) (QName -> Maybe QName
fromQName QName
n)
  m QName -> (QName -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \n' :: QName
n' -> Maybe Range -> QName -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Maybe Range -> QName -> m Context
checkFile (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
r) QName
n'
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c' :: Context
c' -> DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
checkImportDirective DirectiveType
Import Range
r QName
n' Context
c' ImportDirective
i
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'' :: Context
c'' -> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName -> Context -> AccessContext
accessContextImport QName
n' Context
c'')
checkNiceDeclaration _ _ (NiceImport r :: Range
r n :: QName
n Nothing DoOpen i :: ImportDirective
i)
  = Error -> Maybe QName -> m QName
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
n)) (QName -> Maybe QName
fromQName QName
n)
  m QName -> (QName -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \n' :: QName
n' -> Maybe Range -> QName -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Maybe Range -> QName -> m Context
checkFile (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
r) QName
n'
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c' :: Context
c' -> DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
checkImportDirective DirectiveType
Import Range
r QName
n' Context
c' ImportDirective
i
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'' :: Context
c'' -> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QName -> Context -> AccessContext
accessContextImport QName
n' Context
c'
    AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> Access -> Context -> AccessContext
fromContext (ImportDirective -> Access
importDirectiveAccess ImportDirective
i) Context
c'')
checkNiceDeclaration _ _ (NiceImport r :: Range
r n :: QName
n (Just a :: AsName
a) DontOpen i :: ImportDirective
i)
  = Error -> Maybe QName -> m QName
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
n)) (QName -> Maybe QName
fromQName QName
n)
  m QName -> (QName -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \n' :: QName
n' -> Error -> Maybe Name -> m Name
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (AsName -> Range
forall t. HasRange t => t -> Range
getRange AsName
a)) (AsName -> Maybe Name
fromAsName AsName
a)
  m Name -> (Name -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a' :: Name
a' -> Maybe Range -> QName -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Maybe Range -> QName -> m Context
checkFile (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
r) QName
n'
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c' :: Context
c' -> DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
checkImportDirective DirectiveType
Import Range
r QName
n' Context
c' ImportDirective
i
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'' :: Context
c'' -> Context -> Access -> Range -> Name -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Context -> Access -> Range -> Name -> m AccessContext
checkModuleName Context
c'' Access
Public (AsName -> Range
forall t. HasRange t => t -> Range
getRange AsName
a) Name
a'
checkNiceDeclaration _ _ (NiceImport r :: Range
r n :: QName
n (Just a :: AsName
a) DoOpen i :: ImportDirective
i)
  = Error -> Maybe QName -> m QName
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
n)) (QName -> Maybe QName
fromQName QName
n)
  m QName -> (QName -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \n' :: QName
n' -> Error -> Maybe Name -> m Name
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (AsName -> Range
forall t. HasRange t => t -> Range
getRange AsName
a)) (AsName -> Maybe Name
fromAsName AsName
a)
  m Name -> (Name -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a' :: Name
a' -> Maybe Range -> QName -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Maybe Range -> QName -> m Context
checkFile (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
r) QName
n'
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c' :: Context
c' -> DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
checkImportDirective DirectiveType
Import Range
r QName
n' Context
c' ImportDirective
i
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'' :: Context
c'' -> Context -> Access -> Range -> Name -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Context -> Access -> Range -> Name -> m AccessContext
checkModuleName Context
c' Access
Public (AsName -> Range
forall t. HasRange t => t -> Range
getRange AsName
a) Name
a'
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c''' :: AccessContext
c''' -> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext
c''' AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> Access -> Context -> AccessContext
fromContext (ImportDirective -> Access
importDirectiveAccess ImportDirective
i) Context
c'')

checkNiceDeclaration fs :: Fixities
fs c :: AccessContext
c (NiceDataDef _ _ _ _ _ n :: Name
n bs :: [LamBinding]
bs cs :: [NiceDeclaration]
cs)
  = Error -> Maybe Name -> m Name
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
n)) (Name -> Maybe Name
fromName Name
n)
  m Name -> (Name -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \n' :: Name
n' -> [Range] -> m [Range]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((LookupError -> [Range])
-> ([Range] -> [Range]) -> Either LookupError [Range] -> [Range]
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ([Range] -> LookupError -> [Range]
forall a b. a -> b -> a
const []) [Range] -> [Range]
forall a. a -> a
id (QName -> AccessContext -> Either LookupError [Range]
accessContextLookup (Name -> QName
QName Name
n') AccessContext
c))
  m [Range] -> ([Range] -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \rs :: [Range]
rs -> Bool -> AccessContext -> [LamBinding] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> [LamBinding] -> m AccessContext
checkLamBindings Bool
False AccessContext
c [LamBinding]
bs
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c' :: AccessContext
c' -> Fixities
-> [Range] -> AccessContext -> [NiceDeclaration] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities
-> [Range] -> AccessContext -> [NiceDeclaration] -> m AccessContext
checkNiceConstructors Fixities
fs [Range]
rs (Name -> AccessContext -> AccessContext
accessContextDefine Name
n' AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c') [NiceDeclaration]
cs
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'' :: AccessContext
c'' -> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> Access -> [Range] -> AccessContext -> AccessContext
accessContextModule' Name
n' Access
Public [Range]
rs AccessContext
c'' AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c'')

checkNiceDeclaration fs :: Fixities
fs c :: AccessContext
c (NiceRecDef _ _ _ _ _ n :: Name
n _ _ m :: Maybe (Name, IsInstance)
m bs :: [LamBinding]
bs ds :: [Declaration]
ds)
  = Error -> Maybe Name -> m Name
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
n)) (Name -> Maybe Name
fromName Name
n)
  m Name -> (Name -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \n' :: Name
n' -> [Range] -> m [Range]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((LookupError -> [Range])
-> ([Range] -> [Range]) -> Either LookupError [Range] -> [Range]
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ([Range] -> LookupError -> [Range]
forall a b. a -> b -> a
const []) [Range] -> [Range]
forall a. a -> a
id (QName -> AccessContext -> Either LookupError [Range]
accessContextLookup (Name -> QName
QName Name
n') AccessContext
c))
  m [Range] -> ([Range] -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \rs :: [Range]
rs -> Bool -> AccessContext -> [LamBinding] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> [LamBinding] -> m AccessContext
checkLamBindings Bool
False AccessContext
c [LamBinding]
bs
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c' :: AccessContext
c' -> Fixities -> [Range] -> Maybe (Range, Name) -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Fixities -> [Range] -> Maybe (Range, Name) -> m AccessContext
checkNiceConstructorRecordMay Fixities
fs [Range]
rs (Maybe (Name, IsInstance)
m Maybe (Name, IsInstance)
-> ((Name, IsInstance) -> Maybe (Range, Name))
-> Maybe (Range, Name)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Name -> Maybe (Range, Name)
fromNameRange (Name -> Maybe (Range, Name))
-> ((Name, IsInstance) -> Name)
-> (Name, IsInstance)
-> Maybe (Range, Name)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, IsInstance) -> Name
forall a b. (a, b) -> a
fst)
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'' :: AccessContext
c'' -> Name
-> [Range] -> AccessContext -> [Declaration] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Name
-> [Range] -> AccessContext -> [Declaration] -> m AccessContext
checkDeclarationsRecord Name
n' [Range]
rs (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c') [Declaration]
ds
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c''' :: AccessContext
c''' -> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> Access -> [Range] -> AccessContext -> AccessContext
accessContextModule' Name
n' Access
Public [Range]
rs (AccessContext
c'' AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c''') AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c'')

checkNiceDeclaration fs :: Fixities
fs c :: AccessContext
c (NicePatternSyn _ a :: Access
a n :: Name
n ns :: [Arg Name]
ns p :: Pattern
p)
  = m AccessContext -> m AccessContext
forall (m :: * -> *) a. MonadReader Environment m => m a -> m a
localSkip (Bool -> Access -> RangeType -> [Name] -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool -> Access -> RangeType -> [Name] -> m AccessContext
checkNames' Bool
False Access
Public RangeType
RangeVariable (Arg Name -> Name
forall e. Arg e -> e
unArg (Arg Name -> Name) -> [Arg Name] -> [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg Name]
ns))
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c' :: AccessContext
c' -> AccessContext -> Pattern -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Pattern -> m AccessContext
checkPattern (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c') Pattern
p
  m AccessContext -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
checkName' Bool
True Fixities
fs (Access -> Access
fromAccess Access
a) RangeType
RangePatternSynonym Name
n

checkNiceDeclarationRecord
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Name
  -> [Range]
  -- ^ Ranges associated with parent record.
  -> Fixities
  -> AccessContext
  -> NiceDeclaration
  -> m AccessContext
checkNiceDeclarationRecord :: Name
-> [Range]
-> Fixities
-> AccessContext
-> NiceDeclaration
-> m AccessContext
checkNiceDeclarationRecord _ rs :: [Range]
rs fs :: Fixities
fs c :: AccessContext
c d :: NiceDeclaration
d@(Axiom _ _ _ _ _ _ _)
  = [Range] -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
[Range] -> m ()
modifyDelete [Range]
rs m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord _ rs :: [Range]
rs fs :: Fixities
fs c :: AccessContext
c d :: NiceDeclaration
d@(PrimitiveFunction _ _ _ _ _)
  = [Range] -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
[Range] -> m ()
modifyDelete [Range]
rs m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord n :: Name
n rs :: [Range]
rs fs :: Fixities
fs c :: AccessContext
c (NiceMutual _ _ _ _ ds :: [NiceDeclaration]
ds)
  = Name
-> [Range]
-> Fixities
-> AccessContext
-> [NiceDeclaration]
-> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Name
-> [Range]
-> Fixities
-> AccessContext
-> [NiceDeclaration]
-> m AccessContext
checkNiceDeclarationsRecord Name
n [Range]
rs Fixities
fs AccessContext
c [NiceDeclaration]
ds
checkNiceDeclarationRecord _ rs :: [Range]
rs fs :: Fixities
fs c :: AccessContext
c d :: NiceDeclaration
d@(NiceModule _ _ _ _ _ _)
  = [Range] -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
[Range] -> m ()
modifyDelete [Range]
rs m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord _ _ fs :: Fixities
fs c :: AccessContext
c d :: NiceDeclaration
d@(NiceModuleMacro _ _ _ _ _ _)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord _ _ fs :: Fixities
fs c :: AccessContext
c d :: NiceDeclaration
d@(NiceOpen _ _ _)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord _ _ fs :: Fixities
fs c :: AccessContext
c d :: NiceDeclaration
d@(NiceImport _ _ _ _ _)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord _ _ fs :: Fixities
fs c :: AccessContext
c d :: NiceDeclaration
d@(NicePragma _ _)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord _ rs :: [Range]
rs fs :: Fixities
fs c :: AccessContext
c d :: NiceDeclaration
d@(NiceRecSig _ _ _ _ _ _ _ _)
  = [Range] -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
[Range] -> m ()
modifyDelete [Range]
rs m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord _ rs :: [Range]
rs fs :: Fixities
fs c :: AccessContext
c d :: NiceDeclaration
d@(NiceDataSig _ _ _ _ _ _ _ _)
  = [Range] -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
[Range] -> m ()
modifyDelete [Range]
rs m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord _ _ fs :: Fixities
fs c :: AccessContext
c d :: NiceDeclaration
d@(NiceFunClause _ _ _ _ _ _ _)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord _ rs :: [Range]
rs fs :: Fixities
fs c :: AccessContext
c d :: NiceDeclaration
d@(FunSig _ _ _ _ _ _ _ _ _ _)
  = [Range] -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
[Range] -> m ()
modifyDelete [Range]
rs m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord _ _ fs :: Fixities
fs c :: AccessContext
c d :: NiceDeclaration
d@(FunDef _ _ _ _ _ _ _ _)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord _ _ fs :: Fixities
fs c :: AccessContext
c d :: NiceDeclaration
d@(NiceDataDef _ _ _ _ _ _ _ _)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord _ _ fs :: Fixities
fs c :: AccessContext
c d :: NiceDeclaration
d@(NiceRecDef _ _ _ _ _ _ _ _ _ _ _)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord _ _ fs :: Fixities
fs c :: AccessContext
c d :: NiceDeclaration
d@(NicePatternSyn _ _ _ _ _)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord _ _ fs :: Fixities
fs c :: AccessContext
c d :: NiceDeclaration
d@(NiceGeneralize _ _ _ _ _ _)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord _ _ fs :: Fixities
fs c :: AccessContext
c d :: NiceDeclaration
d@(NiceUnquoteDecl _ _ _ _ _ _ _ _)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
checkNiceDeclarationRecord _ _ fs :: Fixities
fs c :: AccessContext
c d :: NiceDeclaration
d@(NiceUnquoteDef _ _ _ _ _ _ _)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d

checkNiceDeclarationRecord n :: Name
n rs :: [Range]
rs fs :: Fixities
fs c :: AccessContext
c (NiceField _ a :: Access
a _ _ _ n' :: Name
n' (Arg _ e :: Expr
e))
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr (Name -> AccessContext -> AccessContext
accessContextDefine Name
n AccessContext
c) Expr
e
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> m AccessContext
-> (Name -> m AccessContext) -> Maybe Name -> m AccessContext
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
    (AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty)
    (\n'' :: Name
n'' -> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> Access -> Item -> AccessContext
accessContextItem Name
n'' (Access -> Access
fromAccess Access
a)
      ([Range] -> Maybe Name -> Item
item [Range]
rs (Fixities -> Name -> Maybe Name
syntax Fixities
fs Name
n''))))
    (Name -> Maybe Name
fromName Name
n')

checkNiceDeclarations
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Fixities
  -> AccessContext
  -> [NiceDeclaration]
  -> m AccessContext
checkNiceDeclarations :: Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
checkNiceDeclarations fs :: Fixities
fs
  = (AccessContext -> NiceDeclaration -> m AccessContext)
-> AccessContext -> [NiceDeclaration] -> m AccessContext
forall (m :: * -> *) b.
Monad m =>
(AccessContext -> b -> m AccessContext)
-> AccessContext -> [b] -> m AccessContext
checkFoldUnion (Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs)

checkNiceDeclarationsRecord
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Name
  -> [Range]
  -- ^ Ranges associated with parent record.
  -> Fixities
  -> AccessContext
  -> [NiceDeclaration]
  -> m AccessContext
checkNiceDeclarationsRecord :: Name
-> [Range]
-> Fixities
-> AccessContext
-> [NiceDeclaration]
-> m AccessContext
checkNiceDeclarationsRecord n :: Name
n rs :: [Range]
rs fs :: Fixities
fs
  = (AccessContext -> NiceDeclaration -> m AccessContext)
-> AccessContext -> [NiceDeclaration] -> m AccessContext
forall (m :: * -> *) b.
Monad m =>
(AccessContext -> b -> m AccessContext)
-> AccessContext -> [b] -> m AccessContext
checkFoldUnion (Name
-> [Range]
-> Fixities
-> AccessContext
-> NiceDeclaration
-> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Name
-> [Range]
-> Fixities
-> AccessContext
-> NiceDeclaration
-> m AccessContext
checkNiceDeclarationRecord Name
n [Range]
rs Fixities
fs)

checkNiceDeclarationsTop
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Fixities
  -> AccessContext
  -> [NiceDeclaration]
  -> m AccessContext
checkNiceDeclarationsTop :: Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
checkNiceDeclarationsTop _ _ []
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkNiceDeclarationsTop _ c :: AccessContext
c (NiceModule r :: Range
r a :: Access
a _ _ bs :: [TypedBinding]
bs ds :: [Declaration]
ds : _)
  = AccessContext
-> Access
-> Range
-> Maybe Name
-> [TypedBinding]
-> [Declaration]
-> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext
-> Access
-> Range
-> Maybe Name
-> [TypedBinding]
-> [Declaration]
-> m AccessContext
checkNiceModule AccessContext
c (Access -> Access
fromAccess Access
a) Range
r Maybe Name
forall a. Maybe a
Nothing [TypedBinding]
bs [Declaration]
ds
checkNiceDeclarationsTop fs :: Fixities
fs c :: AccessContext
c (d :: NiceDeclaration
d : ds :: [NiceDeclaration]
ds)
  = Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceDeclaration Fixities
fs AccessContext
c NiceDeclaration
d
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c' :: AccessContext
c' -> Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities -> AccessContext -> [NiceDeclaration] -> m AccessContext
checkNiceDeclarations Fixities
fs (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c') [NiceDeclaration]
ds

checkNiceSig
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Fixities
  -> AccessContext
  -> Common.Access
  -> RangeType
  -> N.Name
  -> [LamBinding]
  -> Expr
  -> m AccessContext
checkNiceSig :: Fixities
-> AccessContext
-> Access
-> RangeType
-> Name
-> [LamBinding]
-> Expr
-> m AccessContext
checkNiceSig fs :: Fixities
fs c :: AccessContext
c a :: Access
a t :: RangeType
t n :: Name
n bs :: [LamBinding]
bs e :: Expr
e
  = Bool -> AccessContext -> [LamBinding] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> [LamBinding] -> m AccessContext
checkLamBindings Bool
False AccessContext
c [LamBinding]
bs
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c' :: AccessContext
c' -> AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c') Expr
e
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Bool -> Fixities -> Access -> RangeType -> Name -> m AccessContext
checkName' Bool
False Fixities
fs (Access -> Access
fromAccess Access
a) RangeType
t Name
n

checkNiceConstructor
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Fixities
  -> [Range]
  -- ^ Ranges associated with parent type.
  -> AccessContext
  -> NiceDeclaration
  -> m AccessContext
checkNiceConstructor :: Fixities
-> [Range] -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceConstructor fs :: Fixities
fs rs :: [Range]
rs c :: AccessContext
c (Axiom _ a :: Access
a _ _ _ n :: Name
n e :: Expr
e)
  = AccessContext -> Expr -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> Expr -> m ()
checkExpr AccessContext
c Expr
e
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> m AccessContext
-> (Name -> m AccessContext) -> Maybe Name -> m AccessContext
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
    (AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty)
    (\n'' :: Name
n'' -> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> Access -> Item -> AccessContext
accessContextItem Name
n'' (Access -> Access
fromAccess Access
a)
      ([Range] -> Maybe Name -> Item
itemConstructor [Range]
rs (Fixities -> Name -> Maybe Name
syntax Fixities
fs Name
n''))))
    (Name -> Maybe Name
fromName Name
n)
checkNiceConstructor _ _ _ d :: NiceDeclaration
d
  = Error -> m AccessContext
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorConstructor (NiceDeclaration -> Range
forall t. HasRange t => t -> Range
getRange NiceDeclaration
d))

checkNiceConstructors
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Fixities
  -> [Range]
  -- ^ Ranges associated with parent type.
  -> AccessContext
  -> [NiceDeclaration]
  -> m AccessContext
checkNiceConstructors :: Fixities
-> [Range] -> AccessContext -> [NiceDeclaration] -> m AccessContext
checkNiceConstructors fs :: Fixities
fs rs :: [Range]
rs
  = (AccessContext -> NiceDeclaration -> m AccessContext)
-> AccessContext -> [NiceDeclaration] -> m AccessContext
forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence (Fixities
-> [Range] -> AccessContext -> NiceDeclaration -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Fixities
-> [Range] -> AccessContext -> NiceDeclaration -> m AccessContext
checkNiceConstructor Fixities
fs [Range]
rs)

checkNiceConstructorRecord
  :: MonadReader Environment m
  => MonadState State m
  => Fixities
  -> [Range]
  -- ^ Ranges associated with record type.
  -> Range
  -> Name
  -> m AccessContext
checkNiceConstructorRecord :: Fixities -> [Range] -> Range -> Name -> m AccessContext
checkNiceConstructorRecord fs :: Fixities
fs rs :: [Range]
rs r :: Range
r n :: Name
n
  = Range -> RangeInfo -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Range -> RangeInfo -> m ()
modifyInsert Range
r (RangeType -> QName -> RangeInfo
RangeNamed RangeType
RangeRecordConstructor (Name -> QName
QName Name
n))
  m () -> m AccessContext -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> Access -> Item -> AccessContext
accessContextItem Name
n Access
Public ([Range] -> Maybe Name -> Item
itemConstructor (Range
r Range -> [Range] -> [Range]
forall a. a -> [a] -> [a]
: [Range]
rs) (Fixities -> Name -> Maybe Name
syntax Fixities
fs Name
n)))

checkNiceConstructorRecordMay
  :: MonadReader Environment m
  => MonadState State m
  => Fixities
  -> [Range]
  -- ^ Ranges associated with record type.
  -> Maybe (Range, Name)
  -> m AccessContext
checkNiceConstructorRecordMay :: Fixities -> [Range] -> Maybe (Range, Name) -> m AccessContext
checkNiceConstructorRecordMay _ _ Nothing
  = AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure AccessContext
forall a. Monoid a => a
mempty
checkNiceConstructorRecordMay fs :: Fixities
fs rs :: [Range]
rs (Just (r :: Range
r, n :: Name
n))
  = Fixities -> [Range] -> Range -> Name -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Fixities -> [Range] -> Range -> Name -> m AccessContext
checkNiceConstructorRecord Fixities
fs [Range]
rs Range
r Name
n

checkNiceModule
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => AccessContext
  -> Access
  -> Range
  -> Maybe Name
  -- ^ If `Nothing`, the module is anonymous.
  -> [TypedBinding]
  -> [Declaration]
  -> m AccessContext
checkNiceModule :: AccessContext
-> Access
-> Range
-> Maybe Name
-> [TypedBinding]
-> [Declaration]
-> m AccessContext
checkNiceModule c :: AccessContext
c a :: Access
a r :: Range
r n :: Maybe Name
n bs :: [TypedBinding]
bs ds :: [Declaration]
ds
  = Bool -> AccessContext -> [TypedBinding] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Bool -> AccessContext -> [TypedBinding] -> m AccessContext
checkTypedBindings Bool
True AccessContext
c [TypedBinding]
bs
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c' :: AccessContext
c' -> AccessContext -> [Declaration] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Declaration] -> m AccessContext
checkDeclarations (AccessContext
c AccessContext -> AccessContext -> AccessContext
forall a. Semigroup a => a -> a -> a
<> AccessContext
c') [Declaration]
ds
  m AccessContext
-> (AccessContext -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'' :: AccessContext
c'' -> Context -> m Context
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AccessContext -> Context
toContext AccessContext
c'')
  m Context -> (Context -> m AccessContext) -> m AccessContext
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c''' :: Context
c''' -> m AccessContext
-> (Name -> m AccessContext) -> Maybe Name -> m AccessContext
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (AccessContext -> m AccessContext
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Access -> Context -> AccessContext
fromContext Access
a Context
c''')) (Context -> Access -> Range -> Name -> m AccessContext
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Context -> Access -> Range -> Name -> m AccessContext
checkModuleName Context
c''' Access
a Range
r) Maybe Name
n

-- ## Imports

data DirectiveType where

  Import
    :: DirectiveType

  Module
    :: DirectiveType

  Open
    :: DirectiveType

  deriving Int -> DirectiveType -> ShowS
[DirectiveType] -> ShowS
DirectiveType -> RawName
(Int -> DirectiveType -> ShowS)
-> (DirectiveType -> RawName)
-> ([DirectiveType] -> ShowS)
-> Show DirectiveType
forall a.
(Int -> a -> ShowS) -> (a -> RawName) -> ([a] -> ShowS) -> Show a
showList :: [DirectiveType] -> ShowS
$cshowList :: [DirectiveType] -> ShowS
show :: DirectiveType -> RawName
$cshow :: DirectiveType -> RawName
showsPrec :: Int -> DirectiveType -> ShowS
$cshowsPrec :: Int -> DirectiveType -> ShowS
Show

directiveStatement
  :: DirectiveType
  -> Maybe RangeType
directiveStatement :: DirectiveType -> Maybe RangeType
directiveStatement Import
  = RangeType -> Maybe RangeType
forall a. a -> Maybe a
Just RangeType
RangeImport
directiveStatement Module
  = Maybe RangeType
forall a. Maybe a
Nothing
directiveStatement Open
  = RangeType -> Maybe RangeType
forall a. a -> Maybe a
Just RangeType
RangeOpen

directiveItem
  :: DirectiveType
  -> RangeType
directiveItem :: DirectiveType -> RangeType
directiveItem Import
  = RangeType
RangeImportItem
directiveItem Module
  = RangeType
RangeModuleItem
directiveItem Open
  = RangeType
RangeOpenItem

checkImportDirective
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => DirectiveType
  -> Range
  -> QName
  -> Context
  -> ImportDirective
  -> m Context
checkImportDirective :: DirectiveType
-> Range -> QName -> Context -> ImportDirective -> m Context
checkImportDirective dt :: DirectiveType
dt r :: Range
r n :: QName
n c :: Context
c (ImportDirective _ UseEverything hs :: [ImportedName' Name Name]
hs rs :: [Renaming' Name Name]
rs _)
  = m () -> (RangeType -> m ()) -> Maybe RangeType -> m ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) (\t :: RangeType
t -> Range -> RangeInfo -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Range -> RangeInfo -> m ()
modifyInsert Range
r (RangeType -> QName -> RangeInfo
RangeNamed RangeType
t QName
n))
    (DirectiveType -> Maybe RangeType
directiveStatement DirectiveType
dt)
  m () -> m Context -> m Context
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Context -> [ImportedName' Name Name] -> m Context
forall (m :: * -> *).
MonadError Error m =>
Context -> [ImportedName' Name Name] -> m Context
modifyHidings Context
c [ImportedName' Name Name]
hs
  m Context -> (Context -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Context -> [Renaming' Name Name] -> m Context)
-> [Renaming' Name Name] -> Context -> m Context
forall a b c. (a -> b -> c) -> b -> a -> c
flip (DirectiveType -> Context -> [Renaming' Name Name] -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType -> Context -> [Renaming' Name Name] -> m Context
modifyRenamings DirectiveType
dt) [Renaming' Name Name]
rs
  m Context -> (Context -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Range -> Context -> m Context
forall (m :: * -> *).
MonadReader Environment m =>
Range -> Context -> m Context
contextInsertRangeAll Range
r
checkImportDirective dt :: DirectiveType
dt r :: Range
r n :: QName
n c :: Context
c (ImportDirective _ (Using ns :: [ImportedName' Name Name]
ns) _ rs :: [Renaming' Name Name]
rs _)
  = m () -> (RangeType -> m ()) -> Maybe RangeType -> m ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) (\t :: RangeType
t -> Range -> RangeInfo -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Range -> RangeInfo -> m ()
modifyInsert Range
r (RangeType -> QName -> RangeInfo
RangeNamed RangeType
t QName
n))
    (DirectiveType -> Maybe RangeType
directiveStatement DirectiveType
dt)
  m () -> m Context -> m Context
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> DirectiveType -> Context -> [ImportedName' Name Name] -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType -> Context -> [ImportedName' Name Name] -> m Context
checkImportedNames DirectiveType
dt Context
c [ImportedName' Name Name]
ns
  m Context -> (Context -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c' :: Context
c' -> DirectiveType -> Context -> [Renaming' Name Name] -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType -> Context -> [Renaming' Name Name] -> m Context
checkRenamings DirectiveType
dt Context
c [Renaming' Name Name]
rs
  m Context -> (Context -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c'' :: Context
c'' -> Range -> Context -> m Context
forall (m :: * -> *).
MonadReader Environment m =>
Range -> Context -> m Context
contextInsertRangeAll Range
r (Context
c' Context -> Context -> Context
forall a. Semigroup a => a -> a -> a
<> Context
c'')

checkRenaming
  :: MonadReader Environment m
  => MonadState State m
  => MonadError Error m
  => DirectiveType
  -> Context
  -> Renaming
  -> m Context
checkRenaming :: DirectiveType -> Context -> Renaming' Name Name -> m Context
checkRenaming dt :: DirectiveType
dt c :: Context
c r :: Renaming' Name Name
r@(Renaming n :: ImportedName' Name Name
n t :: ImportedName' Name Name
t _ _)
  = DirectiveType
-> Context
-> (Range, ImportedName' Name Name, ImportedName' Name Name)
-> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Context
-> (Range, ImportedName' Name Name, ImportedName' Name Name)
-> m Context
checkImportedNamePair DirectiveType
dt Context
c (Renaming' Name Name -> Range
forall t. HasRange t => t -> Range
getRange Renaming' Name Name
r, ImportedName' Name Name
n, ImportedName' Name Name
t)

checkRenamings
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => DirectiveType
  -> Context
  -> [Renaming]
  -> m Context
checkRenamings :: DirectiveType -> Context -> [Renaming' Name Name] -> m Context
checkRenamings dt :: DirectiveType
dt
  = (Context -> Renaming' Name Name -> m Context)
-> Context -> [Renaming' Name Name] -> m Context
forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence (DirectiveType -> Context -> Renaming' Name Name -> m Context
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m,
 MonadError Error m) =>
DirectiveType -> Context -> Renaming' Name Name -> m Context
checkRenaming DirectiveType
dt)

checkImportedName
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => DirectiveType
  -> Context
  -> ImportedName
  -> m Context
checkImportedName :: DirectiveType -> Context -> ImportedName' Name Name -> m Context
checkImportedName dt :: DirectiveType
dt c :: Context
c n :: ImportedName' Name Name
n
  = DirectiveType
-> Context
-> (Range, ImportedName' Name Name, ImportedName' Name Name)
-> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType
-> Context
-> (Range, ImportedName' Name Name, ImportedName' Name Name)
-> m Context
checkImportedNamePair DirectiveType
dt Context
c (ImportedName' Name Name -> Range
forall t. HasRange t => t -> Range
getRange ImportedName' Name Name
n, ImportedName' Name Name
n, ImportedName' Name Name
n)

checkImportedNamePair
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => DirectiveType
  -> Context
  -> (Range, ImportedName, ImportedName)
  -> m Context
checkImportedNamePair :: DirectiveType
-> Context
-> (Range, ImportedName' Name Name, ImportedName' Name Name)
-> m Context
checkImportedNamePair dt :: DirectiveType
dt c :: Context
c (_, ImportedName n :: Name
n, ImportedName t :: Name
t)
  = Error -> Maybe Name -> m Name
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
n)) (Name -> Maybe Name
fromName Name
n)
  m Name -> (Name -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \n' :: Name
n' -> Error -> Maybe (Range, Name) -> m (Range, Name)
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
t)) (Name -> Maybe (Range, Name)
fromNameRange Name
t)
  m (Range, Name) -> ((Range, Name) -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(r :: Range
r, t' :: Name
t') -> Range -> RangeInfo -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Range -> RangeInfo -> m ()
modifyInsert Range
r (RangeType -> QName -> RangeInfo
RangeNamed (DirectiveType -> RangeType
directiveItem DirectiveType
dt) (Name -> QName
QName Name
t'))
  m () -> m Context -> m Context
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Context -> m Context
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context -> (Item -> Context) -> Maybe Item -> Context
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Context
forall a. Monoid a => a
mempty (Name -> Item -> Context
contextItem Name
t') (QName -> Context -> Maybe Item
contextLookupItem (Name -> QName
QName Name
n') Context
c)
    Context -> Context -> Context
forall a. Semigroup a => a -> a -> a
<> Context -> (Module -> Context) -> Maybe Module -> Context
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Context
forall a. Monoid a => a
mempty (Name -> Module -> Context
contextModule Name
t') (QName -> Context -> Maybe Module
contextLookupModule (Name -> QName
QName Name
n') Context
c))
  m Context -> (Context -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Range -> Context -> m Context
forall (m :: * -> *).
MonadReader Environment m =>
Range -> Context -> m Context
contextInsertRangeAll Range
r
checkImportedNamePair dt :: DirectiveType
dt c :: Context
c (_, ImportedModule n :: Name
n, ImportedModule t :: Name
t)
  = Error -> Maybe Name -> m Name
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
n)) (Name -> Maybe Name
fromName Name
n)
  m Name -> (Name -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \n' :: Name
n' -> Error -> Maybe (Range, Name) -> m (Range, Name)
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
t)) (Name -> Maybe (Range, Name)
fromNameRange Name
t)
  m (Range, Name) -> ((Range, Name) -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(r :: Range
r, t' :: Name
t') -> Range -> RangeInfo -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Range -> RangeInfo -> m ()
modifyInsert Range
r (RangeType -> QName -> RangeInfo
RangeNamed (DirectiveType -> RangeType
directiveItem DirectiveType
dt) (Name -> QName
QName Name
t'))
  m () -> m Context -> m Context
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Context -> m Context
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context -> (Module -> Context) -> Maybe Module -> Context
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Context
forall a. Monoid a => a
mempty (Name -> Module -> Context
contextModule Name
t') (QName -> Context -> Maybe Module
contextLookupModule (Name -> QName
QName Name
n') Context
c))
  m Context -> (Context -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Range -> Context -> m Context
forall (m :: * -> *).
MonadReader Environment m =>
Range -> Context -> m Context
contextInsertRangeAll Range
r
checkImportedNamePair _ _ (r :: Range
r, _, _)
  = Error -> m Context
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorRenaming Range
r)

checkImportedNames
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => DirectiveType
  -> Context
  -> [ImportedName]
  -> m Context
checkImportedNames :: DirectiveType -> Context -> [ImportedName' Name Name] -> m Context
checkImportedNames dt :: DirectiveType
dt
  = (Context -> ImportedName' Name Name -> m Context)
-> Context -> [ImportedName' Name Name] -> m Context
forall (m :: * -> *) c a b.
(Monad m, Monoid c) =>
(a -> b -> m c) -> a -> [b] -> m c
checkSequence (DirectiveType -> Context -> ImportedName' Name Name -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType -> Context -> ImportedName' Name Name -> m Context
checkImportedName DirectiveType
dt)

modifyHiding
  :: MonadError Error m
  => Context
  -> ImportedName
  -> m Context
modifyHiding :: Context -> ImportedName' Name Name -> m Context
modifyHiding c :: Context
c (ImportedName n :: Name
n)
  = Error -> Maybe Name -> m Name
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
n)) (Name -> Maybe Name
fromName Name
n)
  m Name -> (Name -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Context -> m Context
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context -> m Context) -> (Name -> Context) -> Name -> m Context
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Context -> Context) -> Context -> Name -> Context
forall a b c. (a -> b -> c) -> b -> a -> c
flip Name -> Context -> Context
contextDelete Context
c
modifyHiding c :: Context
c (ImportedModule n :: Name
n)
  = Error -> Maybe Name -> m Name
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
n)) (Name -> Maybe Name
fromName Name
n)
  m Name -> (Name -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Context -> m Context
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context -> m Context) -> (Name -> Context) -> Name -> m Context
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Context -> Context) -> Context -> Name -> Context
forall a b c. (a -> b -> c) -> b -> a -> c
flip Name -> Context -> Context
contextDeleteModule Context
c

modifyHidings
  :: MonadError Error m
  => Context
  -> [ImportedName]
  -> m Context
modifyHidings :: Context -> [ImportedName' Name Name] -> m Context
modifyHidings
  = (Context -> ImportedName' Name Name -> m Context)
-> Context -> [ImportedName' Name Name] -> m Context
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Context -> ImportedName' Name Name -> m Context
forall (m :: * -> *).
MonadError Error m =>
Context -> ImportedName' Name Name -> m Context
modifyHiding

modifyRenaming
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => DirectiveType
  -> Context
  -> Renaming
  -> m Context
modifyRenaming :: DirectiveType -> Context -> Renaming' Name Name -> m Context
modifyRenaming dt :: DirectiveType
dt c :: Context
c (Renaming (ImportedName n :: Name
n) (ImportedName t :: Name
t) _ _)
  = Error -> Maybe Name -> m Name
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
n)) (Name -> Maybe Name
fromName Name
n)
  m Name -> (Name -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \n' :: Name
n' -> Error -> Maybe (Range, Name) -> m (Range, Name)
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
t)) (Name -> Maybe (Range, Name)
fromNameRange Name
t)
  m (Range, Name) -> ((Range, Name) -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(r :: Range
r, t' :: Name
t') -> Range -> RangeInfo -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Range -> RangeInfo -> m ()
modifyInsert Range
r (RangeType -> QName -> RangeInfo
RangeNamed (DirectiveType -> RangeType
directiveItem DirectiveType
dt) (Name -> QName
QName Name
t'))
  m () -> m Context -> m Context
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Name -> Name -> Range -> Context -> m Context
forall (m :: * -> *).
MonadReader Environment m =>
Name -> Name -> Range -> Context -> m Context
contextRename Name
n' Name
t' Range
r Context
c
  m Context -> (Context -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Name -> Name -> Range -> Context -> m Context
forall (m :: * -> *).
MonadReader Environment m =>
Name -> Name -> Range -> Context -> m Context
contextRenameModule Name
n' Name
t' Range
r
modifyRenaming dt :: DirectiveType
dt c :: Context
c (Renaming (ImportedModule n :: Name
n) (ImportedModule t :: Name
t) _ _)
  = Error -> Maybe Name -> m Name
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
n)) (Name -> Maybe Name
fromName Name
n)
  m Name -> (Name -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \n' :: Name
n' -> Error -> Maybe (Range, Name) -> m (Range, Name)
forall e (m :: * -> *) a. MonadError e m => e -> Maybe a -> m a
liftMaybe (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorName (Name -> Range
forall t. HasRange t => t -> Range
getRange Name
t)) (Name -> Maybe (Range, Name)
fromNameRange Name
t)
  m (Range, Name) -> ((Range, Name) -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(r :: Range
r, t' :: Name
t') -> Range -> RangeInfo -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Range -> RangeInfo -> m ()
modifyInsert Range
r (RangeType -> QName -> RangeInfo
RangeNamed (DirectiveType -> RangeType
directiveItem DirectiveType
dt) (Name -> QName
QName Name
t'))
  m () -> m Context -> m Context
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Name -> Name -> Range -> Context -> m Context
forall (m :: * -> *).
MonadReader Environment m =>
Name -> Name -> Range -> Context -> m Context
contextRenameModule Name
n' Name
t' Range
r Context
c
modifyRenaming _ _ r :: Renaming' Name Name
r
  = Error -> m Context
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InternalError -> Range -> Error
ErrorInternal InternalError
ErrorRenaming (Renaming' Name Name -> Range
forall t. HasRange t => t -> Range
getRange Renaming' Name Name
r))

modifyRenamings
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => DirectiveType
  -> Context
  -> [Renaming]
  -> m Context
modifyRenamings :: DirectiveType -> Context -> [Renaming' Name Name] -> m Context
modifyRenamings dt :: DirectiveType
dt
  = (Context -> Renaming' Name Name -> m Context)
-> Context -> [Renaming' Name Name] -> m Context
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (DirectiveType -> Context -> Renaming' Name Name -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
DirectiveType -> Context -> Renaming' Name Name -> m Context
modifyRenaming DirectiveType
dt)

touchModule
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => AccessContext
  -> Range
  -> QName
  -> m ()
touchModule :: AccessContext -> Range -> QName -> m ()
touchModule c :: AccessContext
c r :: Range
r n :: QName
n
  = Either LookupError Module -> Range -> QName -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
Either LookupError Module -> Range -> QName -> m ()
touchModuleWith (QName -> AccessContext -> Either LookupError Module
accessContextLookupModule QName
n AccessContext
c) Range
r QName
n

touchModuleWith
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => Either LookupError C.Module
  -> Range
  -> QName
  -> m ()
touchModuleWith :: Either LookupError Module -> Range -> QName -> m ()
touchModuleWith (Left LookupNotFound) _ _
  = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
touchModuleWith (Left LookupAmbiguous) r :: Range
r n :: QName
n
  = Error -> m ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Range -> QName -> Error
ErrorAmbiguous Range
r QName
n)
touchModuleWith (Right m :: Module
m) _ _
  = [Range] -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
[Range] -> m ()
modifyDelete (Module -> [Range]
moduleRanges Module
m)

touchContext
  :: MonadReader Environment m
  => MonadState State m
  => Context
  -> m ()
touchContext :: Context -> m ()
touchContext c :: Context
c
  = [Range] -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
[Range] -> m ()
modifyDelete (Context -> [Range]
contextRanges Context
c)

importDirectiveAccess
  :: ImportDirective
  -> Access
importDirectiveAccess :: ImportDirective -> Access
importDirectiveAccess (ImportDirective _ _ _ _ Nothing)
  = Access
Private
importDirectiveAccess (ImportDirective _ _ _ _ (Just _))
  = Access
Public

-- ## Modules

checkModule
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Module
  -> m Context
checkModule :: Module -> m Context
checkModule (_, ds :: [Declaration]
ds)
  = AccessContext -> Context
toContext (AccessContext -> Context) -> m AccessContext -> m Context
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AccessContext -> [Declaration] -> m AccessContext
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
AccessContext -> [Declaration] -> m AccessContext
checkDeclarationsTop AccessContext
forall a. Monoid a => a
mempty [Declaration]
ds

-- ## Files

checkFile
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Maybe Range
  -> QName
  -> m Context
checkFile :: Maybe Range -> QName -> m Context
checkFile r :: Maybe Range
r n :: QName
n
  = (State -> Maybe ModuleState) -> m (Maybe ModuleState)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (QName -> State -> Maybe ModuleState
stateLookup QName
n) m (Maybe ModuleState)
-> (Maybe ModuleState -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \s :: Maybe ModuleState
s -> Maybe ModuleState -> Maybe Range -> QName -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Maybe ModuleState -> Maybe Range -> QName -> m Context
checkFileWith Maybe ModuleState
s Maybe Range
r QName
n

checkFileWith
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Maybe ModuleState
  -> Maybe Range
  -> QName
  -> m Context

checkFileWith :: Maybe ModuleState -> Maybe Range -> QName -> m Context
checkFileWith Nothing r :: Maybe Range
r n :: QName
n | QName -> Bool
isBuiltin QName
n
  = IO RawName -> m RawName
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (RawName -> IO RawName
getDataFileName ("data" RawName -> ShowS
</> QName -> RawName
qNamePath QName
n))
  m RawName -> (RawName -> m Context) -> m Context
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \p :: RawName
p -> m Context -> m Context
forall (m :: * -> *) a. MonadReader Environment m => m a -> m a
localSkip (Maybe Range -> QName -> RawName -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Maybe Range -> QName -> RawName -> m Context
checkFilePath Maybe Range
r QName
n RawName
p)

checkFileWith Nothing r :: Maybe Range
r n :: QName
n = do
  Bool
local
    <- m Bool
forall (m :: * -> *). MonadReader Environment m => m Bool
askLocal
  RawName
rootPath
    <- m RawName
forall (m :: * -> *). MonadReader Environment m => m RawName
askRoot
  Context
context
    <- Maybe Range -> QName -> RawName -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Maybe Range -> QName -> RawName -> m Context
checkFilePath Maybe Range
r QName
n (RawName
rootPath RawName -> ShowS
</> QName -> RawName
qNamePath QName
n)
  ()
_
    <- m () -> m () -> Bool -> m ()
forall a. a -> a -> Bool -> a
bool (() -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) (Context -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Context -> m ()
touchContext Context
context) Bool
local
  Context -> m Context
forall (f :: * -> *) a. Applicative f => a -> f a
pure Context
context

checkFileWith (Just Blocked) r :: Maybe Range
r n :: QName
n
  = Error -> m Context
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Maybe Range -> QName -> Error
ErrorCyclic Maybe Range
r QName
n)
checkFileWith (Just (Checked c :: Context
c)) _ _
  = Context -> m Context
forall (f :: * -> *) a. Applicative f => a -> f a
pure Context
c

checkFilePath
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Maybe Range
  -> QName
  -> FilePath
  -> m Context
checkFilePath :: Maybe Range -> QName -> RawName -> m Context
checkFilePath r :: Maybe Range
r n :: QName
n p :: RawName
p = do
  ()
_
    <- (State -> State) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (QName -> State -> State
stateBlock QName
n)
  AbsolutePath
absolutePath
    <- AbsolutePath -> m AbsolutePath
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> AbsolutePath
AbsolutePath (RawName -> Text
T.pack RawName
p))
  Bool
exists
    <- IO Bool -> m Bool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (RawName -> IO Bool
doesFileExist RawName
p)
  ()
_
    <- m () -> m () -> Bool -> m ()
forall a. a -> a -> Bool -> a
bool (Error -> m ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Maybe Range -> QName -> RawName -> Error
ErrorFile Maybe Range
r QName
n RawName
p)) (() -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) Bool
exists
  RawName
contents
    <- IO RawName -> m RawName
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (RawName -> IO RawName
readFile RawName
p)
  (parseResult :: Either ParseError (Module, FileType)
parseResult, _)
    <- IO (Either ParseError (Module, FileType), [ParseWarning])
-> m (Either ParseError (Module, FileType), [ParseWarning])
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (PM (Module, FileType)
-> IO (Either ParseError (Module, FileType), [ParseWarning])
forall (m :: * -> *) a.
MonadIO m =>
PM a -> m (Either ParseError a, [ParseWarning])
runPMIO (Parser Module -> AbsolutePath -> RawName -> PM (Module, FileType)
forall a.
Show a =>
Parser a -> AbsolutePath -> RawName -> PM (a, FileType)
parseFile Parser Module
moduleParser AbsolutePath
absolutePath RawName
contents))
  (module' :: Module
module', _)
    <- Either Error (Module, FileType) -> m (Module, FileType)
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither ((ParseError -> Error)
-> Either ParseError (Module, FileType)
-> Either Error (Module, FileType)
forall e f a. (e -> f) -> Either e a -> Either f a
mapLeft ParseError -> Error
ErrorParse Either ParseError (Module, FileType)
parseResult)
  Context
context
    <- Module -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Module -> m Context
checkModule Module
module'
  ()
_
    <- (State -> State) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (QName -> Context -> State -> State
stateCheck QName
n Context
context)
  Context -> m Context
forall (f :: * -> *) a. Applicative f => a -> f a
pure Context
context

-- ## Paths

-- Look for unvisited modules at the given path.
checkPath
  :: MonadIO m
  => [QName]
  -- ^ Visited or ignored modules.
  -> FilePath
  -- ^ The project root path.
  -> FilePath
  -- ^ The path at which to look.
  -> m [FilePath]
checkPath :: [QName] -> RawName -> RawName -> m [RawName]
checkPath ms :: [QName]
ms p :: RawName
p p' :: RawName
p'
  = IO Bool -> m Bool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (RawName -> IO Bool
doesDirectoryExist RawName
p')
  m Bool -> (Bool -> m [RawName]) -> m [RawName]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= m [RawName] -> m [RawName] -> Bool -> m [RawName]
forall a. a -> a -> Bool -> a
bool ([RawName] -> m [RawName]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([QName] -> RawName -> RawName -> [RawName]
checkPathFile [QName]
ms RawName
p RawName
p')) ([QName] -> RawName -> RawName -> m [RawName]
forall (m :: * -> *).
MonadIO m =>
[QName] -> RawName -> RawName -> m [RawName]
checkPathDirectory [QName]
ms RawName
p RawName
p')

checkPathFile
  :: [QName]
  -> FilePath
  -> FilePath
  -> [FilePath]
checkPathFile :: [QName] -> RawName -> RawName -> [RawName]
checkPathFile ms :: [QName]
ms p :: RawName
p p' :: RawName
p'
  = [RawName] -> (QName -> [RawName]) -> Maybe QName -> [RawName]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] ([RawName] -> [RawName] -> Bool -> [RawName]
forall a. a -> a -> Bool -> a
bool [RawName
p'] [] (Bool -> [RawName]) -> (QName -> Bool) -> QName -> [RawName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName -> [QName] -> Bool) -> [QName] -> QName -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip QName -> [QName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem [QName]
ms) (RawName -> RawName -> Maybe QName
pathQName RawName
p RawName
p')

checkPathDirectory
  :: MonadIO m
  => [QName]
  -> FilePath
  -> FilePath
  -> m [FilePath]
checkPathDirectory :: [QName] -> RawName -> RawName -> m [RawName]
checkPathDirectory ms :: [QName]
ms p :: RawName
p p' :: RawName
p'
  = ShowS -> [RawName] -> [RawName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (RawName
p' RawName -> ShowS
</>) ([RawName] -> [RawName]) -> m [RawName] -> m [RawName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO [RawName] -> m [RawName]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (RawName -> IO [RawName]
listDirectory RawName
p')
  m [RawName] -> ([RawName] -> m [[RawName]]) -> m [[RawName]]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (RawName -> m [RawName]) -> [RawName] -> m [[RawName]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ([QName] -> RawName -> RawName -> m [RawName]
forall (m :: * -> *).
MonadIO m =>
[QName] -> RawName -> RawName -> m [RawName]
checkPath [QName]
ms RawName
p)
  m [[RawName]] -> ([[RawName]] -> m [RawName]) -> m [RawName]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [RawName] -> m [RawName]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([RawName] -> m [RawName])
-> ([[RawName]] -> [RawName]) -> [[RawName]] -> m [RawName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[RawName]] -> [RawName]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat

-- ## Roots

checkRoot
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => Root
  -> m ()
checkRoot :: Root -> m ()
checkRoot (Root p :: QName
p Nothing)
  = Maybe Range -> QName -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Maybe Range -> QName -> m Context
checkFile Maybe Range
forall a. Maybe a
Nothing QName
p
  m Context -> (Context -> m ()) -> m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Context -> m ()
forall (m :: * -> *).
(MonadReader Environment m, MonadState State m) =>
Context -> m ()
touchContext
checkRoot (Root p :: QName
p (Just ns :: [QName]
ns))
  = Maybe Range -> QName -> m Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Maybe Range -> QName -> m Context
checkFile Maybe Range
forall a. Maybe a
Nothing QName
p
  m Context -> (Context -> m ()) -> m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c :: Context
c -> Context -> QName -> [QName] -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m,
 MonadState State m) =>
Context -> QName -> [QName] -> m ()
touchQNamesContext Context
c QName
p [QName]
ns

checkRoots
  :: MonadError Error m
  => MonadReader Environment m
  => MonadState State m
  => MonadIO m
  => [Root]
  -> m ()
checkRoots :: [Root] -> m ()
checkRoots
  = m [()] -> m ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (m [()] -> m ()) -> ([Root] -> m [()]) -> [Root] -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Root -> m ()) -> [Root] -> m [()]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Root -> m ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Root -> m ()
checkRoot

-- ## Main

-- | Check an Agda file and its dependencies for unused code.
checkUnused
  :: FilePath
  -- ^ The project root path.
  -> Roots
  -- ^ The public entry points for the project.
  -> IO (Either Error Unused)
checkUnused :: RawName -> Roots -> IO (Either Error Unused)
checkUnused p :: RawName
p (Roots rs :: [Root]
rs is :: [QName]
is)
  = ExceptT Error IO Unused -> IO (Either Error Unused)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT
  (ExceptT Error IO Unused -> IO (Either Error Unused))
-> ExceptT Error IO Unused -> IO (Either Error Unused)
forall a b. (a -> b) -> a -> b
$ Bool
-> RawName
-> ReaderT Environment (StateT State (ExceptT Error IO)) ()
-> ExceptT Error IO State
forall (m :: * -> *) a.
(MonadError Error m, MonadIO m) =>
Bool
-> RawName -> ReaderT Environment (StateT State m) a -> m State
checkUnusedItems Bool
False RawName
p ([Root] -> ReaderT Environment (StateT State (ExceptT Error IO)) ()
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
[Root] -> m ()
checkRoots [Root]
rs)
  ExceptT Error IO State
-> (State -> ExceptT Error IO Unused) -> ExceptT Error IO Unused
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \s :: State
s -> [QName] -> RawName -> RawName -> ExceptT Error IO [RawName]
forall (m :: * -> *).
MonadIO m =>
[QName] -> RawName -> RawName -> m [RawName]
checkPath ([QName]
is [QName] -> [QName] -> [QName]
forall a. Semigroup a => a -> a -> a
<> State -> [QName]
stateModules State
s) RawName
p RawName
p
  ExceptT Error IO [RawName]
-> ([RawName] -> ExceptT Error IO Unused)
-> ExceptT Error IO Unused
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \fs :: [RawName]
fs -> Unused -> ExceptT Error IO Unused
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UnusedItems -> [RawName] -> Unused
Unused ([(Range, RangeInfo)] -> UnusedItems
UnusedItems (State -> [(Range, RangeInfo)]
stateItems State
s)) [RawName]
fs)

-- | Check an Agda file for unused code.
checkUnusedLocal
  :: FilePath
  -- ^ The project root path.
  -> QName
  -- ^ The module to check.
  -> IO (Either Error UnusedItems)
checkUnusedLocal :: RawName -> QName -> IO (Either Error UnusedItems)
checkUnusedLocal p :: RawName
p
  = ExceptT Error IO UnusedItems -> IO (Either Error UnusedItems)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT
  (ExceptT Error IO UnusedItems -> IO (Either Error UnusedItems))
-> (QName -> ExceptT Error IO UnusedItems)
-> QName
-> IO (Either Error UnusedItems)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(Range, RangeInfo)] -> UnusedItems)
-> ExceptT Error IO [(Range, RangeInfo)]
-> ExceptT Error IO UnusedItems
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Range, RangeInfo)] -> UnusedItems
UnusedItems
  (ExceptT Error IO [(Range, RangeInfo)]
 -> ExceptT Error IO UnusedItems)
-> (QName -> ExceptT Error IO [(Range, RangeInfo)])
-> QName
-> ExceptT Error IO UnusedItems
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (State -> [(Range, RangeInfo)])
-> ExceptT Error IO State -> ExceptT Error IO [(Range, RangeInfo)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap State -> [(Range, RangeInfo)]
stateItems
  (ExceptT Error IO State -> ExceptT Error IO [(Range, RangeInfo)])
-> (QName -> ExceptT Error IO State)
-> QName
-> ExceptT Error IO [(Range, RangeInfo)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool
-> RawName
-> ReaderT Environment (StateT State (ExceptT Error IO)) Context
-> ExceptT Error IO State
forall (m :: * -> *) a.
(MonadError Error m, MonadIO m) =>
Bool
-> RawName -> ReaderT Environment (StateT State m) a -> m State
checkUnusedItems Bool
True RawName
p
  (ReaderT Environment (StateT State (ExceptT Error IO)) Context
 -> ExceptT Error IO State)
-> (QName
    -> ReaderT Environment (StateT State (ExceptT Error IO)) Context)
-> QName
-> ExceptT Error IO State
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Range
-> QName
-> ReaderT Environment (StateT State (ExceptT Error IO)) Context
forall (m :: * -> *).
(MonadError Error m, MonadReader Environment m, MonadState State m,
 MonadIO m) =>
Maybe Range -> QName -> m Context
checkFile Maybe Range
forall a. Maybe a
Nothing

checkUnusedItems
  :: MonadError Error m
  => MonadIO m
  => Bool
  -- ^ Whether to use local mode.
  -> FilePath
  -> ReaderT Environment (StateT State m) a
  -> m State
checkUnusedItems :: Bool
-> RawName -> ReaderT Environment (StateT State m) a -> m State
checkUnusedItems l :: Bool
l p :: RawName
p
  = ((a, State) -> State) -> m (a, State) -> m State
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a, State) -> State
forall a b. (a, b) -> b
snd
  (m (a, State) -> m State)
-> (ReaderT Environment (StateT State m) a -> m (a, State))
-> ReaderT Environment (StateT State m) a
-> m State
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StateT State m a -> State -> m (a, State))
-> State -> StateT State m a -> m (a, State)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT State m a -> State -> m (a, State)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT State
stateEmpty
  (StateT State m a -> m (a, State))
-> (ReaderT Environment (StateT State m) a -> StateT State m a)
-> ReaderT Environment (StateT State m) a
-> m (a, State)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ReaderT Environment (StateT State m) a
 -> Environment -> StateT State m a)
-> Environment
-> ReaderT Environment (StateT State m) a
-> StateT State m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT Environment (StateT State m) a
-> Environment -> StateT State m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (Bool -> Bool -> RawName -> Environment
Environment Bool
False Bool
l RawName
p)