{-# LANGUAGE CPP #-}
{-# LANGUAGE RecursiveDo #-}
-- {-# LANGUAGE UndecidableInstances #-}  -- ghc >= 8.2, GeneralizedNewtypeDeriving MonadTransControl BlockT

module Agda.TypeChecking.Monad.Base
  ( module Agda.TypeChecking.Monad.Base
  , module Agda.TypeChecking.Monad.Base.Types
  , HasOptions (..)
  , RecordFieldWarning
  ) where

import Prelude hiding (null)

import Control.Applicative hiding (empty)
import qualified Control.Concurrent as C
import Control.DeepSeq
import qualified Control.Exception as E

import qualified Control.Monad.Fail as Fail

import Control.Monad                ( void )
import Control.Monad.Except
import Control.Monad.Fix
import Control.Monad.IO.Class       ( MonadIO(..) )
import Control.Monad.State          ( MonadState(..), modify, StateT(..), runStateT )
import Control.Monad.Reader         ( MonadReader(..), ReaderT(..), runReaderT )
import Control.Monad.Writer         ( WriterT )
import Control.Monad.Trans          ( MonadTrans(..), lift )
import Control.Monad.Trans.Control  ( MonadTransControl(..), liftThrough )
import Control.Monad.Trans.Identity ( IdentityT(..), runIdentityT )
import Control.Monad.Trans.Maybe    ( MaybeT(..) )

import Control.Parallel             ( pseq )

import Data.Array (Ix)
import Data.DList (DList)
import Data.Function (on)
import Data.Int
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import qualified Data.List as List
import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map -- hiding (singleton, null, empty)
import Data.Sequence (Seq)
import Data.Set (Set, toList, fromList)
import qualified Data.Set as Set -- hiding (singleton, null, empty)
import Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as HMap
import qualified Data.HashSet as HashSet
import Data.Hashable
import Data.HashSet (HashSet)
import Data.Semigroup ( Semigroup, (<>)) --, Any(..) )
import Data.Set (Set)
import qualified Data.Set as Set
import Data.String
import Data.Text (Text)
import qualified Data.Text.Lazy as TL

import Data.IORef

import GHC.Generics (Generic)

import System.IO (hFlush, stdout)

import Agda.Benchmarking (Benchmark, Phase)

import {-# SOURCE #-} Agda.Compiler.Treeless.Pretty () -- Instances only
import Agda.Syntax.Common
import Agda.Syntax.Builtin (SomeBuiltin, BuiltinId, PrimitiveId)
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Concrete.Definitions
  (NiceDeclaration, DeclarationWarning, declarationWarningName)
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.MetaVars
import Agda.Syntax.Internal.Generic (TermLike(..))
import Agda.Syntax.Parser (ParseWarning)
import Agda.Syntax.Parser.Monad (parseWarningName)
import Agda.Syntax.TopLevelModuleName
  (RawTopLevelModuleName, TopLevelModuleName)
import Agda.Syntax.Treeless (Compiled)
import Agda.Syntax.Notation
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import Agda.Syntax.Info ( MetaKind(InstanceMeta, UnificationMeta), MetaNameSuggestion, MutualInfo )

import           Agda.TypeChecking.Monad.Base.Types
import qualified Agda.TypeChecking.Monad.Base.Warning as W
import           Agda.TypeChecking.Monad.Base.Warning (RecordFieldWarning)
import           Agda.TypeChecking.SizedTypes.Syntax  (HypSizeConstraint)

import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Coverage.SplitTree
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Free.Lazy (Free(freeVars'), underBinder', underBinder)

import Agda.TypeChecking.DiscrimTree.Types

import Agda.Compiler.Backend.Base

import Agda.Interaction.Options
import Agda.Interaction.Options.Warnings
import Agda.Interaction.Response.Base (Response_boot(..))
import Agda.Interaction.Highlighting.Precise
  (HighlightingInfo, NameKind)
import Agda.Interaction.Library
import Agda.Interaction.Library.Base (LibErrors)

import Agda.Utils.Benchmark (MonadBench(..))
import Agda.Utils.BiMap (BiMap, HasTag(..))
import qualified Agda.Utils.BiMap as BiMap
import Agda.Utils.Boolean   ( fromBool, toBool )
import Agda.Utils.CallStack ( CallStack, HasCallStack, withCallerCallStack )
import Agda.Utils.FileName
import Agda.Utils.Functor
import Agda.Utils.Hash
import Agda.Utils.IO        ( showIOException )
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.ListT
import Agda.Utils.List1 (List1, pattern (:|))
import Agda.Utils.List2 (List2, pattern List2)
import qualified Agda.Utils.List1 as List1
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Syntax.Common.Pretty
import Agda.Utils.SmallSet (SmallSet, SmallSetElement)
import qualified Agda.Utils.SmallSet as SmallSet
import Agda.Utils.Singleton
import Agda.Utils.Update

import Agda.Utils.Impossible

---------------------------------------------------------------------------
-- * Type checking state
---------------------------------------------------------------------------

data TCState = TCSt
  { TCState -> PreScopeState
stPreScopeState   :: !PreScopeState
    -- ^ The state which is frozen after scope checking.
  , TCState -> PostScopeState
stPostScopeState  :: !PostScopeState
    -- ^ The state which is modified after scope checking.
  , TCState -> PersistentTCState
stPersistentState :: !PersistentTCState
    -- ^ State which is forever, like a diamond.
  }
  deriving (forall x. TCState -> Rep TCState x)
-> (forall x. Rep TCState x -> TCState) -> Generic TCState
forall x. Rep TCState x -> TCState
forall x. TCState -> Rep TCState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. TCState -> Rep TCState x
from :: forall x. TCState -> Rep TCState x
$cto :: forall x. Rep TCState x -> TCState
to :: forall x. Rep TCState x -> TCState
Generic

class Monad m => ReadTCState m where
  getTCState :: m TCState
  locallyTCState :: Lens' TCState a -> (a -> a) -> m b -> m b

  withTCState :: (TCState -> TCState) -> m a -> m a
  withTCState = Lens' TCState TCState -> (TCState -> TCState) -> m a -> m a
forall a b. Lens' TCState a -> (a -> a) -> m b -> m b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState (TCState -> f TCState) -> TCState -> f TCState
forall a. a -> a
Lens' TCState TCState
id

  default getTCState :: (MonadTrans t, ReadTCState n, t n ~ m) => m TCState
  getTCState = n TCState -> t n TCState
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift n TCState
forall (m :: * -> *). ReadTCState m => m TCState
getTCState

  default locallyTCState
    :: (MonadTransControl t, ReadTCState n, t n ~ m)
    => Lens' TCState a -> (a -> a) -> m b -> m b
  locallyTCState Lens' TCState a
l = (n (StT t b) -> n (StT t b)) -> m b -> m b
(n (StT t b) -> n (StT t b)) -> t n b -> t n b
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a b.
(MonadTransControl t, Monad (t m), Monad m) =>
(m (StT t a) -> m (StT t b)) -> t m a -> t m b
liftThrough ((n (StT t b) -> n (StT t b)) -> m b -> m b)
-> ((a -> a) -> n (StT t b) -> n (StT t b))
-> (a -> a)
-> m b
-> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' TCState a -> (a -> a) -> n (StT t b) -> n (StT t b)
forall a b. Lens' TCState a -> (a -> a) -> n b -> n b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState (a -> f a) -> TCState -> f TCState
Lens' TCState a
l

instance ReadTCState m => ReadTCState (ListT m) where
  locallyTCState :: forall a b. Lens' TCState a -> (a -> a) -> ListT m b -> ListT m b
locallyTCState Lens' TCState a
l = (m (Maybe (b, ListT m b)) -> m (Maybe (b, ListT m b)))
-> ListT m b -> ListT m b
forall (m :: * -> *) a (n :: * -> *) b.
(m (Maybe (a, ListT m a)) -> n (Maybe (b, ListT n b)))
-> ListT m a -> ListT n b
mapListT ((m (Maybe (b, ListT m b)) -> m (Maybe (b, ListT m b)))
 -> ListT m b -> ListT m b)
-> ((a -> a)
    -> m (Maybe (b, ListT m b)) -> m (Maybe (b, ListT m b)))
-> (a -> a)
-> ListT m b
-> ListT m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' TCState a
-> (a -> a) -> m (Maybe (b, ListT m b)) -> m (Maybe (b, ListT m b))
forall a b. Lens' TCState a -> (a -> a) -> m b -> m b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState (a -> f a) -> TCState -> f TCState
Lens' TCState a
l

instance ReadTCState m => ReadTCState (ChangeT m)
instance ReadTCState m => ReadTCState (ExceptT err m)
instance ReadTCState m => ReadTCState (IdentityT m)
instance ReadTCState m => ReadTCState (MaybeT m)
instance ReadTCState m => ReadTCState (ReaderT r m)
instance ReadTCState m => ReadTCState (StateT s m)
instance (Monoid w, ReadTCState m) => ReadTCState (WriterT w m)


instance Show TCState where
  show :: TCState -> String
show TCState
_ = String
"TCSt{}"

data PreScopeState = PreScopeState
  { PreScopeState -> HighlightingInfo
stPreTokens             :: !HighlightingInfo
    -- ^ Highlighting info for tokens and Happy parser warnings (but
    -- not for those tokens/warnings for which highlighting exists in
    -- 'stPostSyntaxInfo').
  , PreScopeState -> Signature
stPreImports            :: !Signature  -- XX populated by scope checker
    -- ^ Imported declared identifiers.
    --   Those most not be serialized!
  , PreScopeState -> Set TopLevelModuleName
stPreImportedModules    :: !(Set TopLevelModuleName)
      -- Andreas, 2023-08-05, issue #6750, don't make this a 'HashSet'
      -- because then the order of its @toList@ is undefined,
      -- leading to undefined deserialization order.
    -- ^ The top-level modules imported by the current module.
  , PreScopeState -> ModuleToSource
stPreModuleToSource     :: !ModuleToSource   -- imports
  , PreScopeState -> VisitedModules
stPreVisitedModules     :: !VisitedModules   -- imports
  , PreScopeState -> ScopeInfo
stPreScope              :: !ScopeInfo
    -- generated by scope checker, current file:
    -- which modules you have, public definitions, current file, maps concrete names to abstract names.
  , PreScopeState -> PatternSynDefns
stPrePatternSyns        :: !A.PatternSynDefns
    -- ^ Pattern synonyms of the current file.  Serialized.
  , PreScopeState -> PatternSynDefns
stPrePatternSynImports  :: !A.PatternSynDefns
    -- ^ Imported pattern synonyms.  Must not be serialized!
  , PreScopeState -> Maybe (Set QName)
stPreGeneralizedVars    :: !(Strict.Maybe (Set QName))
    -- ^ Collected generalizable variables; used during scope checking of terms
  , PreScopeState -> PragmaOptions
stPrePragmaOptions      :: !PragmaOptions
    -- ^ Options applying to the current file. @OPTIONS@
    -- pragmas only affect this field.
  , PreScopeState -> BuiltinThings PrimFun
stPreImportedBuiltins   :: !(BuiltinThings PrimFun)
  , PreScopeState -> DisplayForms
stPreImportedDisplayForms :: !DisplayForms
    -- ^ Display forms added by someone else to imported identifiers
  , PreScopeState -> InteractionId
stPreFreshInteractionId :: !InteractionId
  , PreScopeState -> Map QName Text
stPreImportedUserWarnings :: !(Map A.QName Text)
    -- ^ Imported @UserWarning@s, not to be stored in the @Interface@
  , PreScopeState -> Map QName Text
stPreLocalUserWarnings    :: !(Map A.QName Text)
    -- ^ Locally defined @UserWarning@s, to be stored in the @Interface@
  , PreScopeState -> Maybe Text
stPreWarningOnImport      :: !(Strict.Maybe Text)
    -- ^ Whether the current module should raise a warning when opened
  , PreScopeState -> Set QName
stPreImportedPartialDefs :: !(Set QName)
    -- ^ Imported partial definitions, not to be stored in the @Interface@
  , PreScopeState -> Map String ProjectConfig
stPreProjectConfigs :: !(Map FilePath ProjectConfig)
    -- ^ Map from directories to paths of closest enclosing .agda-lib
    --   files (or @Nothing@ if there are none).
  , PreScopeState -> Map String AgdaLibFile
stPreAgdaLibFiles   :: !(Map FilePath AgdaLibFile)
    -- ^ Contents of .agda-lib files that have already been parsed.
  , PreScopeState -> RemoteMetaStore
stPreImportedMetaStore :: !RemoteMetaStore
    -- ^ Used for meta-variables from other modules.
  , PreScopeState -> HashMap QName QName
stPreCopiedNames       :: !(HashMap A.QName A.QName)
    -- ^ Associates a copied name (the key) to its original name (the
    -- value). Computed by the scope checker, used to compute opaque
    -- blocks.
  , PreScopeState -> HashMap QName (HashSet QName)
stPreNameCopies        :: !(HashMap A.QName (HashSet A.QName))
    -- ^ Associates an original name (the key) to all its copies (the
    -- value). Computed by the scope checker, used to compute opaque
    -- blocks.
  }
  deriving (forall x. PreScopeState -> Rep PreScopeState x)
-> (forall x. Rep PreScopeState x -> PreScopeState)
-> Generic PreScopeState
forall x. Rep PreScopeState x -> PreScopeState
forall x. PreScopeState -> Rep PreScopeState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PreScopeState -> Rep PreScopeState x
from :: forall x. PreScopeState -> Rep PreScopeState x
$cto :: forall x. Rep PreScopeState x -> PreScopeState
to :: forall x. Rep PreScopeState x -> PreScopeState
Generic

-- | Name disambiguation for the sake of highlighting.
data DisambiguatedName = DisambiguatedName NameKind A.QName
  deriving (forall x. DisambiguatedName -> Rep DisambiguatedName x)
-> (forall x. Rep DisambiguatedName x -> DisambiguatedName)
-> Generic DisambiguatedName
forall x. Rep DisambiguatedName x -> DisambiguatedName
forall x. DisambiguatedName -> Rep DisambiguatedName x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DisambiguatedName -> Rep DisambiguatedName x
from :: forall x. DisambiguatedName -> Rep DisambiguatedName x
$cto :: forall x. Rep DisambiguatedName x -> DisambiguatedName
to :: forall x. Rep DisambiguatedName x -> DisambiguatedName
Generic
type DisambiguatedNames = IntMap DisambiguatedName

type ConcreteNames = Map Name [C.Name]

data PostScopeState = PostScopeState
  { PostScopeState -> HighlightingInfo
stPostSyntaxInfo          :: !HighlightingInfo
    -- ^ Highlighting info.
  , PostScopeState -> DisambiguatedNames
stPostDisambiguatedNames  :: !DisambiguatedNames
    -- ^ Disambiguation carried out by the type checker.
    --   Maps position of first name character to disambiguated @'A.QName'@
    --   for each @'A.AmbiguousQName'@ already passed by the type checker.
  , PostScopeState -> LocalMetaStore
stPostOpenMetaStore       :: !LocalMetaStore
    -- ^ Used for open meta-variables.
  , PostScopeState -> LocalMetaStore
stPostSolvedMetaStore     :: !LocalMetaStore
    -- ^ Used for local, instantiated meta-variables.
  , PostScopeState -> InteractionPoints
stPostInteractionPoints   :: !InteractionPoints -- scope checker first
  , PostScopeState -> Constraints
stPostAwakeConstraints    :: !Constraints
  , PostScopeState -> Constraints
stPostSleepingConstraints :: !Constraints
  , PostScopeState -> Bool
stPostDirty               :: !Bool -- local
    -- ^ Dirty when a constraint is added, used to prevent pointer update.
    -- Currently unused.
  , PostScopeState -> Set QName
stPostOccursCheckDefs     :: !(Set QName) -- local
    -- ^ Definitions to be considered during occurs check.
    --   Initialized to the current mutual block before the check.
    --   During occurs check, we remove definitions from this set
    --   as soon we have checked them.
  , PostScopeState -> Signature
stPostSignature           :: !Signature
    -- ^ Declared identifiers of the current file.
    --   These will be serialized after successful type checking.
  , PostScopeState -> Map ModuleName CheckpointId
stPostModuleCheckpoints   :: !(Map ModuleName CheckpointId)
    -- ^ For each module remember the checkpoint corresponding to the orignal
    --   context of the module parameters.
  , PostScopeState -> DisplayForms
stPostImportsDisplayForms :: !DisplayForms
    -- ^ Display forms we add for imported identifiers
  , PostScopeState -> Map String ForeignCodeStack
stPostForeignCode         :: !(Map BackendName ForeignCodeStack)
    -- ^ @{-\# FOREIGN \#-}@ code that should be included in the compiled output.
    -- Does not include code for imported modules.
  , PostScopeState -> Maybe (ModuleName, TopLevelModuleName)
stPostCurrentModule       ::
      !(Maybe (ModuleName, TopLevelModuleName))
    -- ^ The current module is available after it has been type
    -- checked.

  , PostScopeState -> Set QName
stPostPendingInstances :: !(Set QName)

  , PostScopeState -> Set QName
stPostTemporaryInstances :: !(Set QName)

  , PostScopeState -> ConcreteNames
stPostConcreteNames       :: !ConcreteNames
    -- ^ Map keeping track of concrete names assigned to each abstract name
    --   (can be more than one name in case the first one is shadowed)
  , PostScopeState -> Map String (DList String)
stPostUsedNames           :: !(Map RawName (DList RawName))
    -- ^ Map keeping track for each name root (= name w/o numeric
    -- suffixes) what names with the same root have been used during a
    -- TC computation. This information is used to build the
    -- @ShadowingNames@ map.
  , PostScopeState -> Map Name (DList String)
stPostShadowingNames      :: !(Map Name (DList RawName))
    -- ^ Map keeping track for each (abstract) name the list of all
    -- (raw) names that it could maybe be shadowed by.
  , PostScopeState -> Statistics
stPostStatistics          :: !Statistics
    -- ^ Counters to collect various statistics about meta variables etc.
    --   Only for current file.
  , PostScopeState -> [TCWarning]
stPostTCWarnings          :: ![TCWarning]
  , PostScopeState -> Map MutualId MutualBlock
stPostMutualBlocks        :: !(Map MutualId MutualBlock)
  , PostScopeState -> BuiltinThings PrimFun
stPostLocalBuiltins       :: !(BuiltinThings PrimFun)
  , PostScopeState -> MetaId
stPostFreshMetaId         :: !MetaId
  , PostScopeState -> MutualId
stPostFreshMutualId       :: !MutualId
  , PostScopeState -> ProblemId
stPostFreshProblemId      :: !ProblemId
  , PostScopeState -> CheckpointId
stPostFreshCheckpointId   :: !CheckpointId
  , PostScopeState -> Int
stPostFreshInt            :: !Int
  , PostScopeState -> NameId
stPostFreshNameId         :: !NameId
  , PostScopeState -> OpaqueId
stPostFreshOpaqueId       :: !OpaqueId
  , PostScopeState -> Bool
stPostAreWeCaching        :: !Bool
  , PostScopeState -> Bool
stPostPostponeInstanceSearch :: !Bool
  , PostScopeState -> Bool
stPostConsideringInstance :: !Bool
  , PostScopeState -> Bool
stPostInstantiateBlocking :: !Bool
    -- ^ Should we instantiate away blocking metas?
    --   This can produce ill-typed terms but they are often more readable. See issue #3606.
    --   Best set to True only for calls to pretty*/reify to limit unwanted reductions.
  , PostScopeState -> Set QName
stPostLocalPartialDefs    :: !(Set QName)
    -- ^ Local partial definitions, to be stored in the @Interface@
  , PostScopeState -> Map OpaqueId OpaqueBlock
stPostOpaqueBlocks        :: Map OpaqueId OpaqueBlock
    -- ^ Associates opaque identifiers to their actual blocks.
  , PostScopeState -> Map QName OpaqueId
stPostOpaqueIds           :: Map QName OpaqueId
    -- ^ Associates each opaque QName to the block it was defined in.
  }
  deriving ((forall x. PostScopeState -> Rep PostScopeState x)
-> (forall x. Rep PostScopeState x -> PostScopeState)
-> Generic PostScopeState
forall x. Rep PostScopeState x -> PostScopeState
forall x. PostScopeState -> Rep PostScopeState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PostScopeState -> Rep PostScopeState x
from :: forall x. PostScopeState -> Rep PostScopeState x
$cto :: forall x. Rep PostScopeState x -> PostScopeState
to :: forall x. Rep PostScopeState x -> PostScopeState
Generic)

-- | A mutual block of names in the signature.
data MutualBlock = MutualBlock
  { MutualBlock -> MutualInfo
mutualInfo  :: MutualInfo
    -- ^ The original info of the mutual block.
  , MutualBlock -> Set QName
mutualNames :: Set QName
  } deriving (Int -> MutualBlock -> ShowS
[MutualBlock] -> ShowS
MutualBlock -> String
(Int -> MutualBlock -> ShowS)
-> (MutualBlock -> String)
-> ([MutualBlock] -> ShowS)
-> Show MutualBlock
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MutualBlock -> ShowS
showsPrec :: Int -> MutualBlock -> ShowS
$cshow :: MutualBlock -> String
show :: MutualBlock -> String
$cshowList :: [MutualBlock] -> ShowS
showList :: [MutualBlock] -> ShowS
Show, MutualBlock -> MutualBlock -> Bool
(MutualBlock -> MutualBlock -> Bool)
-> (MutualBlock -> MutualBlock -> Bool) -> Eq MutualBlock
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MutualBlock -> MutualBlock -> Bool
== :: MutualBlock -> MutualBlock -> Bool
$c/= :: MutualBlock -> MutualBlock -> Bool
/= :: MutualBlock -> MutualBlock -> Bool
Eq, (forall x. MutualBlock -> Rep MutualBlock x)
-> (forall x. Rep MutualBlock x -> MutualBlock)
-> Generic MutualBlock
forall x. Rep MutualBlock x -> MutualBlock
forall x. MutualBlock -> Rep MutualBlock x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MutualBlock -> Rep MutualBlock x
from :: forall x. MutualBlock -> Rep MutualBlock x
$cto :: forall x. Rep MutualBlock x -> MutualBlock
to :: forall x. Rep MutualBlock x -> MutualBlock
Generic)

instance Null MutualBlock where
  empty :: MutualBlock
empty = MutualInfo -> Set QName -> MutualBlock
MutualBlock MutualInfo
forall a. Null a => a
empty Set QName
forall a. Null a => a
empty

-- | A part of the state which is not reverted when an error is thrown
-- or the state is reset.
data PersistentTCState = PersistentTCSt
  { PersistentTCState -> VisitedModules
stDecodedModules    :: !DecodedModules
  , PersistentTCState -> BiMap RawTopLevelModuleName ModuleNameHash
stPersistentTopLevelModuleNames ::
      !(BiMap RawTopLevelModuleName ModuleNameHash)
    -- ^ Module name hashes for top-level module names (and vice
    -- versa).
  , PersistentTCState -> CommandLineOptions
stPersistentOptions :: CommandLineOptions
  , PersistentTCState -> InteractionOutputCallback
stInteractionOutputCallback  :: InteractionOutputCallback
    -- ^ Callback function to call when there is a response
    --   to give to the interactive frontend.
    --   See the documentation of 'InteractionOutputCallback'.
  , PersistentTCState -> Benchmark
stBenchmark         :: !Benchmark
    -- ^ Structure to track how much CPU time was spent on which Agda phase.
    --   Needs to be a strict field to avoid space leaks!
  , PersistentTCState -> Statistics
stAccumStatistics   :: !Statistics
    -- ^ Should be strict field.
  , PersistentTCState -> Maybe LoadedFileCache
stPersistLoadedFileCache :: !(Strict.Maybe LoadedFileCache)
    -- ^ Cached typechecking state from the last loaded file.
    --   Should be @Nothing@ when checking imports.
  , PersistentTCState -> [Backend_boot (TCMT IO)]
stPersistBackends   :: [Backend_boot TCM]
    -- ^ Current backends with their options
  }
  deriving (forall x. PersistentTCState -> Rep PersistentTCState x)
-> (forall x. Rep PersistentTCState x -> PersistentTCState)
-> Generic PersistentTCState
forall x. Rep PersistentTCState x -> PersistentTCState
forall x. PersistentTCState -> Rep PersistentTCState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PersistentTCState -> Rep PersistentTCState x
from :: forall x. PersistentTCState -> Rep PersistentTCState x
$cto :: forall x. Rep PersistentTCState x -> PersistentTCState
to :: forall x. Rep PersistentTCState x -> PersistentTCState
Generic

data LoadedFileCache = LoadedFileCache
  { LoadedFileCache -> CachedTypeCheckLog
lfcCached  :: !CachedTypeCheckLog
  , LoadedFileCache -> CachedTypeCheckLog
lfcCurrent :: !CurrentTypeCheckLog
  }
  deriving (forall x. LoadedFileCache -> Rep LoadedFileCache x)
-> (forall x. Rep LoadedFileCache x -> LoadedFileCache)
-> Generic LoadedFileCache
forall x. Rep LoadedFileCache x -> LoadedFileCache
forall x. LoadedFileCache -> Rep LoadedFileCache x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. LoadedFileCache -> Rep LoadedFileCache x
from :: forall x. LoadedFileCache -> Rep LoadedFileCache x
$cto :: forall x. Rep LoadedFileCache x -> LoadedFileCache
to :: forall x. Rep LoadedFileCache x -> LoadedFileCache
Generic

-- | A log of what the type checker does and states after the action is
-- completed.  The cached version is stored first executed action first.
type CachedTypeCheckLog = [(TypeCheckAction, PostScopeState)]

-- | Like 'CachedTypeCheckLog', but storing the log for an ongoing type
-- checking of a module.  Stored in reverse order (last performed action
-- first).
type CurrentTypeCheckLog = [(TypeCheckAction, PostScopeState)]

-- | A complete log for a module will look like this:
--
--   * 'Pragmas'
--
--   * 'EnterSection', entering the main module.
--
--   * 'Decl'/'EnterSection'/'LeaveSection', for declarations and nested
--     modules
--
--   * 'LeaveSection', leaving the main module.
data TypeCheckAction
  = EnterSection !Erased !ModuleName !A.Telescope
  | LeaveSection !ModuleName
  | Decl !A.Declaration
    -- ^ Never a Section or ScopeDecl
  | Pragmas !PragmaOptions
  deriving ((forall x. TypeCheckAction -> Rep TypeCheckAction x)
-> (forall x. Rep TypeCheckAction x -> TypeCheckAction)
-> Generic TypeCheckAction
forall x. Rep TypeCheckAction x -> TypeCheckAction
forall x. TypeCheckAction -> Rep TypeCheckAction x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. TypeCheckAction -> Rep TypeCheckAction x
from :: forall x. TypeCheckAction -> Rep TypeCheckAction x
$cto :: forall x. Rep TypeCheckAction x -> TypeCheckAction
to :: forall x. Rep TypeCheckAction x -> TypeCheckAction
Generic)

-- | Empty persistent state.

initPersistentState :: PersistentTCState
initPersistentState :: PersistentTCState
initPersistentState = PersistentTCSt
  { stPersistentOptions :: CommandLineOptions
stPersistentOptions         = CommandLineOptions
defaultOptions
  , stPersistentTopLevelModuleNames :: BiMap RawTopLevelModuleName ModuleNameHash
stPersistentTopLevelModuleNames = BiMap RawTopLevelModuleName ModuleNameHash
forall a. Null a => a
empty
  , stDecodedModules :: VisitedModules
stDecodedModules            = VisitedModules
forall k a. Map k a
Map.empty
  , stInteractionOutputCallback :: InteractionOutputCallback
stInteractionOutputCallback = InteractionOutputCallback
defaultInteractionOutputCallback
  , stBenchmark :: Benchmark
stBenchmark                 = Benchmark
forall a. Null a => a
empty
  , stAccumStatistics :: Statistics
stAccumStatistics           = Statistics
forall k a. Map k a
Map.empty
  , stPersistLoadedFileCache :: Maybe LoadedFileCache
stPersistLoadedFileCache    = Maybe LoadedFileCache
forall a. Null a => a
empty
  , stPersistBackends :: [Backend_boot (TCMT IO)]
stPersistBackends           = []
  }

-- | An initial 'MetaId'.

initialMetaId :: MetaId
initialMetaId :: MetaId
initialMetaId = MetaId
  { metaId :: Word64
metaId     = Word64
0
  , metaModule :: ModuleNameHash
metaModule = ModuleNameHash
noModuleNameHash
  }

-- | Empty state of type checker.

initPreScopeState :: PreScopeState
initPreScopeState :: PreScopeState
initPreScopeState = PreScopeState
  { stPreTokens :: HighlightingInfo
stPreTokens               = HighlightingInfo
forall a. Monoid a => a
mempty
  , stPreImports :: Signature
stPreImports              = Signature
emptySignature
  , stPreImportedModules :: Set TopLevelModuleName
stPreImportedModules      = Set TopLevelModuleName
forall a. Null a => a
empty
  , stPreModuleToSource :: ModuleToSource
stPreModuleToSource       = ModuleToSource
forall k a. Map k a
Map.empty
  , stPreVisitedModules :: VisitedModules
stPreVisitedModules       = VisitedModules
forall k a. Map k a
Map.empty
  , stPreScope :: ScopeInfo
stPreScope                = ScopeInfo
emptyScopeInfo
  , stPrePatternSyns :: PatternSynDefns
stPrePatternSyns          = PatternSynDefns
forall k a. Map k a
Map.empty
  , stPrePatternSynImports :: PatternSynDefns
stPrePatternSynImports    = PatternSynDefns
forall k a. Map k a
Map.empty
  , stPreGeneralizedVars :: Maybe (Set QName)
stPreGeneralizedVars      = Maybe (Set QName)
forall a. Monoid a => a
mempty
  , stPrePragmaOptions :: PragmaOptions
stPrePragmaOptions        = PragmaOptions
defaultInteractionOptions
  , stPreImportedBuiltins :: BuiltinThings PrimFun
stPreImportedBuiltins     = BuiltinThings PrimFun
forall k a. Map k a
Map.empty
  , stPreImportedDisplayForms :: DisplayForms
stPreImportedDisplayForms = DisplayForms
forall k v. HashMap k v
HMap.empty
  , stPreFreshInteractionId :: InteractionId
stPreFreshInteractionId   = InteractionId
0
  , stPreImportedUserWarnings :: Map QName Text
stPreImportedUserWarnings = Map QName Text
forall k a. Map k a
Map.empty
  , stPreLocalUserWarnings :: Map QName Text
stPreLocalUserWarnings    = Map QName Text
forall k a. Map k a
Map.empty
  , stPreWarningOnImport :: Maybe Text
stPreWarningOnImport      = Maybe Text
forall a. Null a => a
empty
  , stPreImportedPartialDefs :: Set QName
stPreImportedPartialDefs  = Set QName
forall a. Set a
Set.empty
  , stPreProjectConfigs :: Map String ProjectConfig
stPreProjectConfigs       = Map String ProjectConfig
forall k a. Map k a
Map.empty
  , stPreAgdaLibFiles :: Map String AgdaLibFile
stPreAgdaLibFiles         = Map String AgdaLibFile
forall k a. Map k a
Map.empty
  , stPreImportedMetaStore :: RemoteMetaStore
stPreImportedMetaStore    = RemoteMetaStore
forall k v. HashMap k v
HMap.empty
  , stPreCopiedNames :: HashMap QName QName
stPreCopiedNames          = HashMap QName QName
forall k v. HashMap k v
HMap.empty
  , stPreNameCopies :: HashMap QName (HashSet QName)
stPreNameCopies           = HashMap QName (HashSet QName)
forall k v. HashMap k v
HMap.empty
  }

initPostScopeState :: PostScopeState
initPostScopeState :: PostScopeState
initPostScopeState = PostScopeState
  { stPostSyntaxInfo :: HighlightingInfo
stPostSyntaxInfo           = HighlightingInfo
forall a. Monoid a => a
mempty
  , stPostDisambiguatedNames :: DisambiguatedNames
stPostDisambiguatedNames   = DisambiguatedNames
forall a. IntMap a
IntMap.empty
  , stPostOpenMetaStore :: LocalMetaStore
stPostOpenMetaStore        = LocalMetaStore
forall k a. Map k a
Map.empty
  , stPostSolvedMetaStore :: LocalMetaStore
stPostSolvedMetaStore      = LocalMetaStore
forall k a. Map k a
Map.empty
  , stPostInteractionPoints :: InteractionPoints
stPostInteractionPoints    = InteractionPoints
forall a. Null a => a
empty
  , stPostAwakeConstraints :: Constraints
stPostAwakeConstraints     = []
  , stPostSleepingConstraints :: Constraints
stPostSleepingConstraints  = []
  , stPostDirty :: Bool
stPostDirty                = Bool
False
  , stPostOccursCheckDefs :: Set QName
stPostOccursCheckDefs      = Set QName
forall a. Set a
Set.empty
  , stPostSignature :: Signature
stPostSignature            = Signature
emptySignature
  , stPostModuleCheckpoints :: Map ModuleName CheckpointId
stPostModuleCheckpoints    = Map ModuleName CheckpointId
forall k a. Map k a
Map.empty
  , stPostImportsDisplayForms :: DisplayForms
stPostImportsDisplayForms  = DisplayForms
forall k v. HashMap k v
HMap.empty
  , stPostCurrentModule :: Maybe (ModuleName, TopLevelModuleName)
stPostCurrentModule        = Maybe (ModuleName, TopLevelModuleName)
forall a. Null a => a
empty
  , stPostPendingInstances :: Set QName
stPostPendingInstances     = Set QName
forall a. Set a
Set.empty
  , stPostTemporaryInstances :: Set QName
stPostTemporaryInstances     = Set QName
forall a. Set a
Set.empty
  , stPostConcreteNames :: ConcreteNames
stPostConcreteNames        = ConcreteNames
forall k a. Map k a
Map.empty
  , stPostUsedNames :: Map String (DList String)
stPostUsedNames            = Map String (DList String)
forall k a. Map k a
Map.empty
  , stPostShadowingNames :: Map Name (DList String)
stPostShadowingNames       = Map Name (DList String)
forall k a. Map k a
Map.empty
  , stPostStatistics :: Statistics
stPostStatistics           = Statistics
forall k a. Map k a
Map.empty
  , stPostTCWarnings :: [TCWarning]
stPostTCWarnings           = []
  , stPostMutualBlocks :: Map MutualId MutualBlock
stPostMutualBlocks         = Map MutualId MutualBlock
forall k a. Map k a
Map.empty
  , stPostLocalBuiltins :: BuiltinThings PrimFun
stPostLocalBuiltins        = BuiltinThings PrimFun
forall k a. Map k a
Map.empty
  , stPostFreshMetaId :: MetaId
stPostFreshMetaId          = MetaId
initialMetaId
  , stPostFreshMutualId :: MutualId
stPostFreshMutualId        = MutualId
0
  , stPostFreshProblemId :: ProblemId
stPostFreshProblemId       = ProblemId
1
  , stPostFreshCheckpointId :: CheckpointId
stPostFreshCheckpointId    = CheckpointId
1
  , stPostFreshInt :: Int
stPostFreshInt             = Int
0
  , stPostFreshNameId :: NameId
stPostFreshNameId          = Word64 -> ModuleNameHash -> NameId
NameId Word64
0 ModuleNameHash
noModuleNameHash
  , stPostFreshOpaqueId :: OpaqueId
stPostFreshOpaqueId        = Word64 -> ModuleNameHash -> OpaqueId
OpaqueId Word64
0 ModuleNameHash
noModuleNameHash
  , stPostAreWeCaching :: Bool
stPostAreWeCaching         = Bool
False
  , stPostPostponeInstanceSearch :: Bool
stPostPostponeInstanceSearch = Bool
False
  , stPostConsideringInstance :: Bool
stPostConsideringInstance  = Bool
False
  , stPostInstantiateBlocking :: Bool
stPostInstantiateBlocking  = Bool
False
  , stPostLocalPartialDefs :: Set QName
stPostLocalPartialDefs     = Set QName
forall a. Set a
Set.empty
  , stPostOpaqueBlocks :: Map OpaqueId OpaqueBlock
stPostOpaqueBlocks         = Map OpaqueId OpaqueBlock
forall k a. Map k a
Map.empty
  , stPostOpaqueIds :: Map QName OpaqueId
stPostOpaqueIds            = Map QName OpaqueId
forall k a. Map k a
Map.empty
  , stPostForeignCode :: Map String ForeignCodeStack
stPostForeignCode          = Map String ForeignCodeStack
forall k a. Map k a
Map.empty
  }

initState :: TCState
initState :: TCState
initState = TCSt
  { stPreScopeState :: PreScopeState
stPreScopeState   = PreScopeState
initPreScopeState
  , stPostScopeState :: PostScopeState
stPostScopeState  = PostScopeState
initPostScopeState
  , stPersistentState :: PersistentTCState
stPersistentState = PersistentTCState
initPersistentState
  }

-- * st-prefixed lenses
------------------------------------------------------------------------

stTokens :: Lens' TCState HighlightingInfo
stTokens :: Lens' TCState HighlightingInfo
stTokens HighlightingInfo -> f HighlightingInfo
f TCState
s =
  HighlightingInfo -> f HighlightingInfo
f (PreScopeState -> HighlightingInfo
stPreTokens (TCState -> PreScopeState
stPreScopeState TCState
s)) f HighlightingInfo -> (HighlightingInfo -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \HighlightingInfo
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreTokens = x}}

stImports :: Lens' TCState Signature
stImports :: Lens' TCState Signature
stImports Signature -> f Signature
f TCState
s =
  Signature -> f Signature
f (PreScopeState -> Signature
stPreImports (TCState -> PreScopeState
stPreScopeState TCState
s)) f Signature -> (Signature -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \Signature
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreImports = x}}

stImportedModules ::
  Lens' TCState (Set TopLevelModuleName)
stImportedModules :: Lens' TCState (Set TopLevelModuleName)
stImportedModules Set TopLevelModuleName -> f (Set TopLevelModuleName)
f TCState
s =
  Set TopLevelModuleName -> f (Set TopLevelModuleName)
f (PreScopeState -> Set TopLevelModuleName
stPreImportedModules (TCState -> PreScopeState
stPreScopeState TCState
s)) f (Set TopLevelModuleName)
-> (Set TopLevelModuleName -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \Set TopLevelModuleName
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreImportedModules = x}}

stModuleToSource :: Lens' TCState ModuleToSource
stModuleToSource :: Lens' TCState ModuleToSource
stModuleToSource ModuleToSource -> f ModuleToSource
f TCState
s =
  ModuleToSource -> f ModuleToSource
f (PreScopeState -> ModuleToSource
stPreModuleToSource (TCState -> PreScopeState
stPreScopeState TCState
s)) f ModuleToSource -> (ModuleToSource -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \ModuleToSource
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreModuleToSource = x}}

stVisitedModules :: Lens' TCState VisitedModules
stVisitedModules :: Lens' TCState VisitedModules
stVisitedModules VisitedModules -> f VisitedModules
f TCState
s =
  VisitedModules -> f VisitedModules
f (PreScopeState -> VisitedModules
stPreVisitedModules (TCState -> PreScopeState
stPreScopeState TCState
s)) f VisitedModules -> (VisitedModules -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \VisitedModules
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreVisitedModules = x}}

stScope :: Lens' TCState ScopeInfo
stScope :: Lens' TCState ScopeInfo
stScope ScopeInfo -> f ScopeInfo
f TCState
s =
  ScopeInfo -> f ScopeInfo
f (PreScopeState -> ScopeInfo
stPreScope (TCState -> PreScopeState
stPreScopeState TCState
s)) f ScopeInfo -> (ScopeInfo -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \ScopeInfo
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreScope = x}}

stPatternSyns :: Lens' TCState A.PatternSynDefns
stPatternSyns :: Lens' TCState PatternSynDefns
stPatternSyns PatternSynDefns -> f PatternSynDefns
f TCState
s =
  PatternSynDefns -> f PatternSynDefns
f (PreScopeState -> PatternSynDefns
stPrePatternSyns (TCState -> PreScopeState
stPreScopeState TCState
s)) f PatternSynDefns -> (PatternSynDefns -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \PatternSynDefns
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPrePatternSyns = x}}

stPatternSynImports :: Lens' TCState A.PatternSynDefns
stPatternSynImports :: Lens' TCState PatternSynDefns
stPatternSynImports PatternSynDefns -> f PatternSynDefns
f TCState
s =
  PatternSynDefns -> f PatternSynDefns
f (PreScopeState -> PatternSynDefns
stPrePatternSynImports (TCState -> PreScopeState
stPreScopeState TCState
s)) f PatternSynDefns -> (PatternSynDefns -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \PatternSynDefns
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPrePatternSynImports = x}}

stGeneralizedVars :: Lens' TCState (Maybe (Set QName))
stGeneralizedVars :: Lens' TCState (Maybe (Set QName))
stGeneralizedVars Maybe (Set QName) -> f (Maybe (Set QName))
f TCState
s =
  Maybe (Set QName) -> f (Maybe (Set QName))
f (Maybe (Set QName) -> Maybe (Set QName)
forall lazy strict. Strict lazy strict => strict -> lazy
Strict.toLazy (Maybe (Set QName) -> Maybe (Set QName))
-> Maybe (Set QName) -> Maybe (Set QName)
forall a b. (a -> b) -> a -> b
$ PreScopeState -> Maybe (Set QName)
stPreGeneralizedVars (TCState -> PreScopeState
stPreScopeState TCState
s)) f (Maybe (Set QName))
-> (Maybe (Set QName) -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \Maybe (Set QName)
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreGeneralizedVars = Strict.toStrict x}}

stPragmaOptions :: Lens' TCState PragmaOptions
stPragmaOptions :: Lens' TCState PragmaOptions
stPragmaOptions PragmaOptions -> f PragmaOptions
f TCState
s =
  PragmaOptions -> f PragmaOptions
f (PreScopeState -> PragmaOptions
stPrePragmaOptions (TCState -> PreScopeState
stPreScopeState TCState
s)) f PragmaOptions -> (PragmaOptions -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \PragmaOptions
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPrePragmaOptions = x}}

stImportedBuiltins :: Lens' TCState (BuiltinThings PrimFun)
stImportedBuiltins :: Lens' TCState (BuiltinThings PrimFun)
stImportedBuiltins BuiltinThings PrimFun -> f (BuiltinThings PrimFun)
f TCState
s =
  BuiltinThings PrimFun -> f (BuiltinThings PrimFun)
f (PreScopeState -> BuiltinThings PrimFun
stPreImportedBuiltins (TCState -> PreScopeState
stPreScopeState TCState
s)) f (BuiltinThings PrimFun)
-> (BuiltinThings PrimFun -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \BuiltinThings PrimFun
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreImportedBuiltins = x}}

stForeignCode :: Lens' TCState (Map BackendName ForeignCodeStack)
stForeignCode :: Lens' TCState (Map String ForeignCodeStack)
stForeignCode Map String ForeignCodeStack -> f (Map String ForeignCodeStack)
f TCState
s =
  Map String ForeignCodeStack -> f (Map String ForeignCodeStack)
f (PostScopeState -> Map String ForeignCodeStack
stPostForeignCode (TCState -> PostScopeState
stPostScopeState TCState
s)) f (Map String ForeignCodeStack)
-> (Map String ForeignCodeStack -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \Map String ForeignCodeStack
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostForeignCode = x}}

stFreshInteractionId :: Lens' TCState InteractionId
stFreshInteractionId :: Lens' TCState InteractionId
stFreshInteractionId InteractionId -> f InteractionId
f TCState
s =
  InteractionId -> f InteractionId
f (PreScopeState -> InteractionId
stPreFreshInteractionId (TCState -> PreScopeState
stPreScopeState TCState
s)) f InteractionId -> (InteractionId -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \InteractionId
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreFreshInteractionId = x}}

stImportedUserWarnings :: Lens' TCState (Map A.QName Text)
stImportedUserWarnings :: Lens' TCState (Map QName Text)
stImportedUserWarnings Map QName Text -> f (Map QName Text)
f TCState
s =
  Map QName Text -> f (Map QName Text)
f (PreScopeState -> Map QName Text
stPreImportedUserWarnings (TCState -> PreScopeState
stPreScopeState TCState
s)) f (Map QName Text) -> (Map QName Text -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \ Map QName Text
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreImportedUserWarnings = x}}

stLocalUserWarnings :: Lens' TCState (Map A.QName Text)
stLocalUserWarnings :: Lens' TCState (Map QName Text)
stLocalUserWarnings Map QName Text -> f (Map QName Text)
f TCState
s =
  Map QName Text -> f (Map QName Text)
f (PreScopeState -> Map QName Text
stPreLocalUserWarnings (TCState -> PreScopeState
stPreScopeState TCState
s)) f (Map QName Text) -> (Map QName Text -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \ Map QName Text
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreLocalUserWarnings = x}}

getUserWarnings :: ReadTCState m => m (Map A.QName Text)
getUserWarnings :: forall (m :: * -> *). ReadTCState m => m (Map QName Text)
getUserWarnings = do
  Map QName Text
iuw <- Lens' TCState (Map QName Text) -> m (Map QName Text)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Map QName Text -> f (Map QName Text)) -> TCState -> f TCState
Lens' TCState (Map QName Text)
stImportedUserWarnings
  Map QName Text
luw <- Lens' TCState (Map QName Text) -> m (Map QName Text)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Map QName Text -> f (Map QName Text)) -> TCState -> f TCState
Lens' TCState (Map QName Text)
stLocalUserWarnings
  Map QName Text -> m (Map QName Text)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Map QName Text -> m (Map QName Text))
-> Map QName Text -> m (Map QName Text)
forall a b. (a -> b) -> a -> b
$ Map QName Text
iuw Map QName Text -> Map QName Text -> Map QName Text
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Map QName Text
luw

stWarningOnImport :: Lens' TCState (Maybe Text)
stWarningOnImport :: Lens' TCState (Maybe Text)
stWarningOnImport Maybe Text -> f (Maybe Text)
f TCState
s =
  Maybe Text -> f (Maybe Text)
f (Maybe Text -> Maybe Text
forall lazy strict. Strict lazy strict => strict -> lazy
Strict.toLazy (Maybe Text -> Maybe Text) -> Maybe Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$ PreScopeState -> Maybe Text
stPreWarningOnImport (TCState -> PreScopeState
stPreScopeState TCState
s)) f (Maybe Text) -> (Maybe Text -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \ Maybe Text
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreWarningOnImport = Strict.toStrict x}}

stImportedPartialDefs :: Lens' TCState (Set QName)
stImportedPartialDefs :: Lens' TCState (Set QName)
stImportedPartialDefs Set QName -> f (Set QName)
f TCState
s =
  Set QName -> f (Set QName)
f (PreScopeState -> Set QName
stPreImportedPartialDefs (TCState -> PreScopeState
stPreScopeState TCState
s)) f (Set QName) -> (Set QName -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \ Set QName
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreImportedPartialDefs = x}}

stLocalPartialDefs :: Lens' TCState (Set QName)
stLocalPartialDefs :: Lens' TCState (Set QName)
stLocalPartialDefs Set QName -> f (Set QName)
f TCState
s =
  Set QName -> f (Set QName)
f (PostScopeState -> Set QName
stPostLocalPartialDefs (TCState -> PostScopeState
stPostScopeState TCState
s)) f (Set QName) -> (Set QName -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \ Set QName
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostLocalPartialDefs = x}}

getPartialDefs :: ReadTCState m => m (Set QName)
getPartialDefs :: forall (m :: * -> *). ReadTCState m => m (Set QName)
getPartialDefs = do
  Set QName
ipd <- Lens' TCState (Set QName) -> m (Set QName)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Set QName -> f (Set QName)) -> TCState -> f TCState
Lens' TCState (Set QName)
stImportedPartialDefs
  Set QName
lpd <- Lens' TCState (Set QName) -> m (Set QName)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Set QName -> f (Set QName)) -> TCState -> f TCState
Lens' TCState (Set QName)
stLocalPartialDefs
  Set QName -> m (Set QName)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set QName -> m (Set QName)) -> Set QName -> m (Set QName)
forall a b. (a -> b) -> a -> b
$ Set QName
ipd Set QName -> Set QName -> Set QName
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set QName
lpd

stLoadedFileCache :: Lens' TCState (Maybe LoadedFileCache)
stLoadedFileCache :: Lens' TCState (Maybe LoadedFileCache)
stLoadedFileCache Maybe LoadedFileCache -> f (Maybe LoadedFileCache)
f TCState
s =
  Maybe LoadedFileCache -> f (Maybe LoadedFileCache)
f (Maybe LoadedFileCache -> Maybe LoadedFileCache
forall lazy strict. Strict lazy strict => strict -> lazy
Strict.toLazy (Maybe LoadedFileCache -> Maybe LoadedFileCache)
-> Maybe LoadedFileCache -> Maybe LoadedFileCache
forall a b. (a -> b) -> a -> b
$ PersistentTCState -> Maybe LoadedFileCache
stPersistLoadedFileCache (TCState -> PersistentTCState
stPersistentState TCState
s)) f (Maybe LoadedFileCache)
-> (Maybe LoadedFileCache -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \Maybe LoadedFileCache
x -> TCState
s {stPersistentState = (stPersistentState s) {stPersistLoadedFileCache = Strict.toStrict x}}

stBackends :: Lens' TCState [Backend_boot TCM]
stBackends :: Lens' TCState [Backend_boot (TCMT IO)]
stBackends [Backend_boot (TCMT IO)] -> f [Backend_boot (TCMT IO)]
f TCState
s =
  [Backend_boot (TCMT IO)] -> f [Backend_boot (TCMT IO)]
f (PersistentTCState -> [Backend_boot (TCMT IO)]
stPersistBackends (TCState -> PersistentTCState
stPersistentState TCState
s)) f [Backend_boot (TCMT IO)]
-> ([Backend_boot (TCMT IO)] -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \[Backend_boot (TCMT IO)]
x -> TCState
s {stPersistentState = (stPersistentState s) {stPersistBackends = x}}

stProjectConfigs :: Lens' TCState (Map FilePath ProjectConfig)
stProjectConfigs :: Lens' TCState (Map String ProjectConfig)
stProjectConfigs Map String ProjectConfig -> f (Map String ProjectConfig)
f TCState
s =
  Map String ProjectConfig -> f (Map String ProjectConfig)
f (PreScopeState -> Map String ProjectConfig
stPreProjectConfigs (TCState -> PreScopeState
stPreScopeState TCState
s)) f (Map String ProjectConfig)
-> (Map String ProjectConfig -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \ Map String ProjectConfig
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreProjectConfigs = x}}

stAgdaLibFiles :: Lens' TCState (Map FilePath AgdaLibFile)
stAgdaLibFiles :: Lens' TCState (Map String AgdaLibFile)
stAgdaLibFiles Map String AgdaLibFile -> f (Map String AgdaLibFile)
f TCState
s =
  Map String AgdaLibFile -> f (Map String AgdaLibFile)
f (PreScopeState -> Map String AgdaLibFile
stPreAgdaLibFiles (TCState -> PreScopeState
stPreScopeState TCState
s)) f (Map String AgdaLibFile)
-> (Map String AgdaLibFile -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \ Map String AgdaLibFile
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreAgdaLibFiles = x}}

stTopLevelModuleNames ::
  Lens' TCState (BiMap RawTopLevelModuleName ModuleNameHash)
stTopLevelModuleNames :: Lens' TCState (BiMap RawTopLevelModuleName ModuleNameHash)
stTopLevelModuleNames BiMap RawTopLevelModuleName ModuleNameHash
-> f (BiMap RawTopLevelModuleName ModuleNameHash)
f TCState
s =
  BiMap RawTopLevelModuleName ModuleNameHash
-> f (BiMap RawTopLevelModuleName ModuleNameHash)
f (PersistentTCState -> BiMap RawTopLevelModuleName ModuleNameHash
stPersistentTopLevelModuleNames (TCState -> PersistentTCState
stPersistentState TCState
s)) f (BiMap RawTopLevelModuleName ModuleNameHash)
-> (BiMap RawTopLevelModuleName ModuleNameHash -> TCState)
-> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \ BiMap RawTopLevelModuleName ModuleNameHash
x -> TCState
s {stPersistentState =
              (stPersistentState s) {stPersistentTopLevelModuleNames = x}}

stImportedMetaStore :: Lens' TCState RemoteMetaStore
stImportedMetaStore :: Lens' TCState RemoteMetaStore
stImportedMetaStore RemoteMetaStore -> f RemoteMetaStore
f TCState
s =
  RemoteMetaStore -> f RemoteMetaStore
f (PreScopeState -> RemoteMetaStore
stPreImportedMetaStore (TCState -> PreScopeState
stPreScopeState TCState
s)) f RemoteMetaStore -> (RemoteMetaStore -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \RemoteMetaStore
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreImportedMetaStore = x}}

stCopiedNames :: Lens' TCState (HashMap QName QName)
stCopiedNames :: Lens' TCState (HashMap QName QName)
stCopiedNames HashMap QName QName -> f (HashMap QName QName)
f TCState
s =
  HashMap QName QName -> f (HashMap QName QName)
f (PreScopeState -> HashMap QName QName
stPreCopiedNames (TCState -> PreScopeState
stPreScopeState TCState
s)) f (HashMap QName QName)
-> (HashMap QName QName -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \HashMap QName QName
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreCopiedNames = x}}

stNameCopies :: Lens' TCState (HashMap QName (HashSet QName))
stNameCopies :: Lens' TCState (HashMap QName (HashSet QName))
stNameCopies HashMap QName (HashSet QName) -> f (HashMap QName (HashSet QName))
f TCState
s =
  HashMap QName (HashSet QName) -> f (HashMap QName (HashSet QName))
f (PreScopeState -> HashMap QName (HashSet QName)
stPreNameCopies (TCState -> PreScopeState
stPreScopeState TCState
s)) f (HashMap QName (HashSet QName))
-> (HashMap QName (HashSet QName) -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \HashMap QName (HashSet QName)
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreNameCopies = x}}

stFreshNameId :: Lens' TCState NameId
stFreshNameId :: Lens' TCState NameId
stFreshNameId NameId -> f NameId
f TCState
s =
  NameId -> f NameId
f (PostScopeState -> NameId
stPostFreshNameId (TCState -> PostScopeState
stPostScopeState TCState
s)) f NameId -> (NameId -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \NameId
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostFreshNameId = x}}

stFreshOpaqueId :: Lens' TCState OpaqueId
stFreshOpaqueId :: Lens' TCState OpaqueId
stFreshOpaqueId OpaqueId -> f OpaqueId
f TCState
s =
  OpaqueId -> f OpaqueId
f (PostScopeState -> OpaqueId
stPostFreshOpaqueId (TCState -> PostScopeState
stPostScopeState TCState
s)) f OpaqueId -> (OpaqueId -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \OpaqueId
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostFreshOpaqueId = x}}

stOpaqueBlocks :: Lens' TCState (Map OpaqueId OpaqueBlock)
stOpaqueBlocks :: Lens' TCState (Map OpaqueId OpaqueBlock)
stOpaqueBlocks Map OpaqueId OpaqueBlock -> f (Map OpaqueId OpaqueBlock)
f TCState
s =
  Map OpaqueId OpaqueBlock -> f (Map OpaqueId OpaqueBlock)
f (PostScopeState -> Map OpaqueId OpaqueBlock
stPostOpaqueBlocks (TCState -> PostScopeState
stPostScopeState TCState
s)) f (Map OpaqueId OpaqueBlock)
-> (Map OpaqueId OpaqueBlock -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \Map OpaqueId OpaqueBlock
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostOpaqueBlocks = x}}

stOpaqueIds :: Lens' TCState (Map QName OpaqueId)
stOpaqueIds :: Lens' TCState (Map QName OpaqueId)
stOpaqueIds Map QName OpaqueId -> f (Map QName OpaqueId)
f TCState
s =
  Map QName OpaqueId -> f (Map QName OpaqueId)
f (PostScopeState -> Map QName OpaqueId
stPostOpaqueIds (TCState -> PostScopeState
stPostScopeState TCState
s)) f (Map QName OpaqueId)
-> (Map QName OpaqueId -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \Map QName OpaqueId
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostOpaqueIds = x}}

stSyntaxInfo :: Lens' TCState HighlightingInfo
stSyntaxInfo :: Lens' TCState HighlightingInfo
stSyntaxInfo HighlightingInfo -> f HighlightingInfo
f TCState
s =
  HighlightingInfo -> f HighlightingInfo
f (PostScopeState -> HighlightingInfo
stPostSyntaxInfo (TCState -> PostScopeState
stPostScopeState TCState
s)) f HighlightingInfo -> (HighlightingInfo -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \HighlightingInfo
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostSyntaxInfo = x}}

stDisambiguatedNames :: Lens' TCState DisambiguatedNames
stDisambiguatedNames :: Lens' TCState DisambiguatedNames
stDisambiguatedNames DisambiguatedNames -> f DisambiguatedNames
f TCState
s =
  DisambiguatedNames -> f DisambiguatedNames
f (PostScopeState -> DisambiguatedNames
stPostDisambiguatedNames (TCState -> PostScopeState
stPostScopeState TCState
s)) f DisambiguatedNames
-> (DisambiguatedNames -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \DisambiguatedNames
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostDisambiguatedNames = x}}

stOpenMetaStore :: Lens' TCState LocalMetaStore
stOpenMetaStore :: Lens' TCState LocalMetaStore
stOpenMetaStore LocalMetaStore -> f LocalMetaStore
f TCState
s =
  LocalMetaStore -> f LocalMetaStore
f (PostScopeState -> LocalMetaStore
stPostOpenMetaStore (TCState -> PostScopeState
stPostScopeState TCState
s)) f LocalMetaStore -> (LocalMetaStore -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \LocalMetaStore
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostOpenMetaStore = x}}

stSolvedMetaStore :: Lens' TCState LocalMetaStore
stSolvedMetaStore :: Lens' TCState LocalMetaStore
stSolvedMetaStore LocalMetaStore -> f LocalMetaStore
f TCState
s =
  LocalMetaStore -> f LocalMetaStore
f (PostScopeState -> LocalMetaStore
stPostSolvedMetaStore (TCState -> PostScopeState
stPostScopeState TCState
s)) f LocalMetaStore -> (LocalMetaStore -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \LocalMetaStore
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostSolvedMetaStore = x}}

stInteractionPoints :: Lens' TCState InteractionPoints
stInteractionPoints :: Lens' TCState InteractionPoints
stInteractionPoints InteractionPoints -> f InteractionPoints
f TCState
s =
  InteractionPoints -> f InteractionPoints
f (PostScopeState -> InteractionPoints
stPostInteractionPoints (TCState -> PostScopeState
stPostScopeState TCState
s)) f InteractionPoints -> (InteractionPoints -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \InteractionPoints
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostInteractionPoints = x}}

stAwakeConstraints :: Lens' TCState Constraints
stAwakeConstraints :: Lens' TCState Constraints
stAwakeConstraints Constraints -> f Constraints
f TCState
s =
  Constraints -> f Constraints
f (PostScopeState -> Constraints
stPostAwakeConstraints (TCState -> PostScopeState
stPostScopeState TCState
s)) f Constraints -> (Constraints -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \Constraints
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostAwakeConstraints = x}}

stSleepingConstraints :: Lens' TCState Constraints
stSleepingConstraints :: Lens' TCState Constraints
stSleepingConstraints Constraints -> f Constraints
f TCState
s =
  Constraints -> f Constraints
f (PostScopeState -> Constraints
stPostSleepingConstraints (TCState -> PostScopeState
stPostScopeState TCState
s)) f Constraints -> (Constraints -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \Constraints
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostSleepingConstraints = x}}

stDirty :: Lens' TCState Bool
stDirty :: Lens' TCState Bool
stDirty Bool -> f Bool
f TCState
s =
  Bool -> f Bool
f (PostScopeState -> Bool
stPostDirty (TCState -> PostScopeState
stPostScopeState TCState
s)) f Bool -> (Bool -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \Bool
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostDirty = x}}

stOccursCheckDefs :: Lens' TCState (Set QName)
stOccursCheckDefs :: Lens' TCState (Set QName)
stOccursCheckDefs Set QName -> f (Set QName)
f TCState
s =
  Set QName -> f (Set QName)
f (PostScopeState -> Set QName
stPostOccursCheckDefs (TCState -> PostScopeState
stPostScopeState TCState
s)) f (Set QName) -> (Set QName -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \Set QName
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostOccursCheckDefs = x}}

stSignature :: Lens' TCState Signature
stSignature :: Lens' TCState Signature
stSignature Signature -> f Signature
f TCState
s =
  Signature -> f Signature
f (PostScopeState -> Signature
stPostSignature (TCState -> PostScopeState
stPostScopeState TCState
s)) f Signature -> (Signature -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \Signature
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostSignature = x}}

stModuleCheckpoints :: Lens' TCState (Map ModuleName CheckpointId)
stModuleCheckpoints :: Lens' TCState (Map ModuleName CheckpointId)
stModuleCheckpoints Map ModuleName CheckpointId -> f (Map ModuleName CheckpointId)
f TCState
s =
  Map ModuleName CheckpointId -> f (Map ModuleName CheckpointId)
f (PostScopeState -> Map ModuleName CheckpointId
stPostModuleCheckpoints (TCState -> PostScopeState
stPostScopeState TCState
s)) f (Map ModuleName CheckpointId)
-> (Map ModuleName CheckpointId -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \Map ModuleName CheckpointId
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostModuleCheckpoints = x}}

stImportsDisplayForms :: Lens' TCState DisplayForms
stImportsDisplayForms :: Lens' TCState DisplayForms
stImportsDisplayForms DisplayForms -> f DisplayForms
f TCState
s =
  DisplayForms -> f DisplayForms
f (PostScopeState -> DisplayForms
stPostImportsDisplayForms (TCState -> PostScopeState
stPostScopeState TCState
s)) f DisplayForms -> (DisplayForms -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \DisplayForms
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostImportsDisplayForms = x}}

stImportedDisplayForms :: Lens' TCState DisplayForms
stImportedDisplayForms :: Lens' TCState DisplayForms
stImportedDisplayForms DisplayForms -> f DisplayForms
f TCState
s =
  DisplayForms -> f DisplayForms
f (PreScopeState -> DisplayForms
stPreImportedDisplayForms (TCState -> PreScopeState
stPreScopeState TCState
s)) f DisplayForms -> (DisplayForms -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \DisplayForms
x -> TCState
s {stPreScopeState = (stPreScopeState s) {stPreImportedDisplayForms = x}}

-- | Note that the lens is \"strict\".

stCurrentModule ::
  Lens' TCState (Maybe (ModuleName, TopLevelModuleName))
stCurrentModule :: Lens' TCState (Maybe (ModuleName, TopLevelModuleName))
stCurrentModule Maybe (ModuleName, TopLevelModuleName)
-> f (Maybe (ModuleName, TopLevelModuleName))
f TCState
s =
  Maybe (ModuleName, TopLevelModuleName)
-> f (Maybe (ModuleName, TopLevelModuleName))
f (PostScopeState -> Maybe (ModuleName, TopLevelModuleName)
stPostCurrentModule (TCState -> PostScopeState
stPostScopeState TCState
s)) f (Maybe (ModuleName, TopLevelModuleName))
-> (Maybe (ModuleName, TopLevelModuleName) -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \Maybe (ModuleName, TopLevelModuleName)
x -> TCState
s {stPostScopeState =
             (stPostScopeState s)
               {stPostCurrentModule = case x of
                  Maybe (ModuleName, TopLevelModuleName)
Nothing         -> Maybe (ModuleName, TopLevelModuleName)
forall a. Maybe a
Nothing
                  Just (!ModuleName
m, !TopLevelModuleName
top) -> (ModuleName, TopLevelModuleName)
-> Maybe (ModuleName, TopLevelModuleName)
forall a. a -> Maybe a
Just (ModuleName
m, TopLevelModuleName
top)}}

stInstanceDefs :: Lens' TCState TempInstanceTable
stInstanceDefs :: Lens' TCState TempInstanceTable
stInstanceDefs TempInstanceTable -> f TempInstanceTable
f TCState
s =
  TempInstanceTable -> f TempInstanceTable
f ( TCState
s TCState -> Lens' TCState InstanceTable -> InstanceTable
forall o i. o -> Lens' o i -> i
^. (Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stSignature ((Signature -> f Signature) -> TCState -> f TCState)
-> ((InstanceTable -> f InstanceTable) -> Signature -> f Signature)
-> (InstanceTable -> f InstanceTable)
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InstanceTable -> f InstanceTable) -> Signature -> f Signature
Lens' Signature InstanceTable
sigInstances
    , PostScopeState -> Set QName
stPostPendingInstances (TCState -> PostScopeState
stPostScopeState TCState
s)
    )
  f TempInstanceTable -> (TempInstanceTable -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(InstanceTable
t, Set QName
x) ->
    Lens' TCState InstanceTable -> LensSet TCState InstanceTable
forall o i. Lens' o i -> LensSet o i
set ((Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stSignature ((Signature -> f Signature) -> TCState -> f TCState)
-> ((InstanceTable -> f InstanceTable) -> Signature -> f Signature)
-> (InstanceTable -> f InstanceTable)
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InstanceTable -> f InstanceTable) -> Signature -> f Signature
Lens' Signature InstanceTable
sigInstances) InstanceTable
t
      (TCState
s { stPostScopeState = (stPostScopeState s) { stPostPendingInstances = x }})

stTemporaryInstances :: Lens' TCState (Set QName)
stTemporaryInstances :: Lens' TCState (Set QName)
stTemporaryInstances Set QName -> f (Set QName)
f TCState
s = Set QName -> f (Set QName)
f (PostScopeState -> Set QName
stPostTemporaryInstances (TCState -> PostScopeState
stPostScopeState TCState
s)) f (Set QName) -> (Set QName -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Set QName
x -> TCState
s {
  stPostScopeState = (stPostScopeState s) { stPostTemporaryInstances = x } }

stInstanceTree :: Lens' TCState (DiscrimTree QName)
stInstanceTree :: Lens' TCState (DiscrimTree QName)
stInstanceTree = (Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stSignature ((Signature -> f Signature) -> TCState -> f TCState)
-> ((DiscrimTree QName -> f (DiscrimTree QName))
    -> Signature -> f Signature)
-> (DiscrimTree QName -> f (DiscrimTree QName))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InstanceTable -> f InstanceTable) -> Signature -> f Signature
Lens' Signature InstanceTable
sigInstances ((InstanceTable -> f InstanceTable) -> Signature -> f Signature)
-> ((DiscrimTree QName -> f (DiscrimTree QName))
    -> InstanceTable -> f InstanceTable)
-> (DiscrimTree QName -> f (DiscrimTree QName))
-> Signature
-> f Signature
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DiscrimTree QName -> f (DiscrimTree QName))
-> InstanceTable -> f InstanceTable
Lens' InstanceTable (DiscrimTree QName)
itableTree

stConcreteNames :: Lens' TCState ConcreteNames
stConcreteNames :: Lens' TCState ConcreteNames
stConcreteNames ConcreteNames -> f ConcreteNames
f TCState
s =
  ConcreteNames -> f ConcreteNames
f (PostScopeState -> ConcreteNames
stPostConcreteNames (TCState -> PostScopeState
stPostScopeState TCState
s)) f ConcreteNames -> (ConcreteNames -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \ConcreteNames
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostConcreteNames = x}}

stUsedNames :: Lens' TCState (Map RawName (DList RawName))
stUsedNames :: Lens' TCState (Map String (DList String))
stUsedNames Map String (DList String) -> f (Map String (DList String))
f TCState
s =
  Map String (DList String) -> f (Map String (DList String))
f (PostScopeState -> Map String (DList String)
stPostUsedNames (TCState -> PostScopeState
stPostScopeState TCState
s)) f (Map String (DList String))
-> (Map String (DList String) -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \Map String (DList String)
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostUsedNames = x}}

stShadowingNames :: Lens' TCState (Map Name (DList RawName))
stShadowingNames :: Lens' TCState (Map Name (DList String))
stShadowingNames Map Name (DList String) -> f (Map Name (DList String))
f TCState
s =
  Map Name (DList String) -> f (Map Name (DList String))
f (PostScopeState -> Map Name (DList String)
stPostShadowingNames (TCState -> PostScopeState
stPostScopeState TCState
s)) f (Map Name (DList String))
-> (Map Name (DList String) -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \Map Name (DList String)
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostShadowingNames = x}}

stStatistics :: Lens' TCState Statistics
stStatistics :: Lens' TCState Statistics
stStatistics Statistics -> f Statistics
f TCState
s =
  Statistics -> f Statistics
f (PostScopeState -> Statistics
stPostStatistics (TCState -> PostScopeState
stPostScopeState TCState
s)) f Statistics -> (Statistics -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \Statistics
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostStatistics = x}}

stTCWarnings :: Lens' TCState [TCWarning]
stTCWarnings :: Lens' TCState [TCWarning]
stTCWarnings [TCWarning] -> f [TCWarning]
f TCState
s =
  [TCWarning] -> f [TCWarning]
f (PostScopeState -> [TCWarning]
stPostTCWarnings (TCState -> PostScopeState
stPostScopeState TCState
s)) f [TCWarning] -> ([TCWarning] -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \[TCWarning]
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostTCWarnings = x}}

stMutualBlocks :: Lens' TCState (Map MutualId MutualBlock)
stMutualBlocks :: Lens' TCState (Map MutualId MutualBlock)
stMutualBlocks Map MutualId MutualBlock -> f (Map MutualId MutualBlock)
f TCState
s =
  Map MutualId MutualBlock -> f (Map MutualId MutualBlock)
f (PostScopeState -> Map MutualId MutualBlock
stPostMutualBlocks (TCState -> PostScopeState
stPostScopeState TCState
s)) f (Map MutualId MutualBlock)
-> (Map MutualId MutualBlock -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \Map MutualId MutualBlock
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostMutualBlocks = x}}

stLocalBuiltins :: Lens' TCState (BuiltinThings PrimFun)
stLocalBuiltins :: Lens' TCState (BuiltinThings PrimFun)
stLocalBuiltins BuiltinThings PrimFun -> f (BuiltinThings PrimFun)
f TCState
s =
  BuiltinThings PrimFun -> f (BuiltinThings PrimFun)
f (PostScopeState -> BuiltinThings PrimFun
stPostLocalBuiltins (TCState -> PostScopeState
stPostScopeState TCState
s)) f (BuiltinThings PrimFun)
-> (BuiltinThings PrimFun -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \BuiltinThings PrimFun
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostLocalBuiltins = x}}

stFreshMetaId :: Lens' TCState MetaId
stFreshMetaId :: Lens' TCState MetaId
stFreshMetaId MetaId -> f MetaId
f TCState
s =
  MetaId -> f MetaId
f (PostScopeState -> MetaId
stPostFreshMetaId (TCState -> PostScopeState
stPostScopeState TCState
s)) f MetaId -> (MetaId -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \MetaId
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostFreshMetaId = x}}

stFreshMutualId :: Lens' TCState MutualId
stFreshMutualId :: Lens' TCState MutualId
stFreshMutualId MutualId -> f MutualId
f TCState
s =
  MutualId -> f MutualId
f (PostScopeState -> MutualId
stPostFreshMutualId (TCState -> PostScopeState
stPostScopeState TCState
s)) f MutualId -> (MutualId -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \MutualId
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostFreshMutualId = x}}

stFreshProblemId :: Lens' TCState ProblemId
stFreshProblemId :: Lens' TCState ProblemId
stFreshProblemId ProblemId -> f ProblemId
f TCState
s =
  ProblemId -> f ProblemId
f (PostScopeState -> ProblemId
stPostFreshProblemId (TCState -> PostScopeState
stPostScopeState TCState
s)) f ProblemId -> (ProblemId -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \ProblemId
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostFreshProblemId = x}}

stFreshCheckpointId :: Lens' TCState CheckpointId
stFreshCheckpointId :: Lens' TCState CheckpointId
stFreshCheckpointId CheckpointId -> f CheckpointId
f TCState
s =
  CheckpointId -> f CheckpointId
f (PostScopeState -> CheckpointId
stPostFreshCheckpointId (TCState -> PostScopeState
stPostScopeState TCState
s)) f CheckpointId -> (CheckpointId -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \CheckpointId
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostFreshCheckpointId = x}}

stFreshInt :: Lens' TCState Int
stFreshInt :: Lens' TCState Int
stFreshInt Int -> f Int
f TCState
s =
  Int -> f Int
f (PostScopeState -> Int
stPostFreshInt (TCState -> PostScopeState
stPostScopeState TCState
s)) f Int -> (Int -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \Int
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostFreshInt = x}}

-- use @areWeCaching@ from the Caching module instead.
stAreWeCaching :: Lens' TCState Bool
stAreWeCaching :: Lens' TCState Bool
stAreWeCaching Bool -> f Bool
f TCState
s =
  Bool -> f Bool
f (PostScopeState -> Bool
stPostAreWeCaching (TCState -> PostScopeState
stPostScopeState TCState
s)) f Bool -> (Bool -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \Bool
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostAreWeCaching = x}}

stPostponeInstanceSearch :: Lens' TCState Bool
stPostponeInstanceSearch :: Lens' TCState Bool
stPostponeInstanceSearch Bool -> f Bool
f TCState
s =
  Bool -> f Bool
f (PostScopeState -> Bool
stPostPostponeInstanceSearch (TCState -> PostScopeState
stPostScopeState TCState
s)) f Bool -> (Bool -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \Bool
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostPostponeInstanceSearch = x}}

stConsideringInstance :: Lens' TCState Bool
stConsideringInstance :: Lens' TCState Bool
stConsideringInstance Bool -> f Bool
f TCState
s =
  Bool -> f Bool
f (PostScopeState -> Bool
stPostConsideringInstance (TCState -> PostScopeState
stPostScopeState TCState
s)) f Bool -> (Bool -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \Bool
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostConsideringInstance = x}}

stInstantiateBlocking :: Lens' TCState Bool
stInstantiateBlocking :: Lens' TCState Bool
stInstantiateBlocking Bool -> f Bool
f TCState
s =
  Bool -> f Bool
f (PostScopeState -> Bool
stPostInstantiateBlocking (TCState -> PostScopeState
stPostScopeState TCState
s)) f Bool -> (Bool -> TCState) -> f TCState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
  \Bool
x -> TCState
s {stPostScopeState = (stPostScopeState s) {stPostInstantiateBlocking = x}}

stBuiltinThings :: TCState -> BuiltinThings PrimFun
stBuiltinThings :: TCState -> BuiltinThings PrimFun
stBuiltinThings TCState
s = (Builtin PrimFun -> Builtin PrimFun -> Builtin PrimFun)
-> BuiltinThings PrimFun
-> BuiltinThings PrimFun
-> BuiltinThings PrimFun
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Builtin PrimFun -> Builtin PrimFun -> Builtin PrimFun
forall a. Builtin a -> Builtin a -> Builtin a
unionBuiltin (TCState
s TCState
-> Lens' TCState (BuiltinThings PrimFun) -> BuiltinThings PrimFun
forall o i. o -> Lens' o i -> i
^. (BuiltinThings PrimFun -> f (BuiltinThings PrimFun))
-> TCState -> f TCState
Lens' TCState (BuiltinThings PrimFun)
stLocalBuiltins) (TCState
s TCState
-> Lens' TCState (BuiltinThings PrimFun) -> BuiltinThings PrimFun
forall o i. o -> Lens' o i -> i
^. (BuiltinThings PrimFun -> f (BuiltinThings PrimFun))
-> TCState -> f TCState
Lens' TCState (BuiltinThings PrimFun)
stImportedBuiltins)

-- | Union two 'Builtin's.  Only defined for 'BuiltinRewriteRelations'.
unionBuiltin :: Builtin a -> Builtin a -> Builtin a
unionBuiltin :: forall a. Builtin a -> Builtin a -> Builtin a
unionBuiltin = ((Builtin a, Builtin a) -> Builtin a)
-> Builtin a -> Builtin a -> Builtin a
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((Builtin a, Builtin a) -> Builtin a)
 -> Builtin a -> Builtin a -> Builtin a)
-> ((Builtin a, Builtin a) -> Builtin a)
-> Builtin a
-> Builtin a
-> Builtin a
forall a b. (a -> b) -> a -> b
$ \case
  (BuiltinRewriteRelations Set QName
xs, BuiltinRewriteRelations Set QName
ys) -> Set QName -> Builtin a
forall pf. Set QName -> Builtin pf
BuiltinRewriteRelations (Set QName -> Builtin a) -> Set QName -> Builtin a
forall a b. (a -> b) -> a -> b
$ Set QName
xs Set QName -> Set QName -> Set QName
forall a. Semigroup a => a -> a -> a
<> Set QName
ys
  (Builtin a, Builtin a)
_ -> Builtin a
forall a. HasCallStack => a
__IMPOSSIBLE__


-- * Fresh things
------------------------------------------------------------------------

class Enum i => HasFresh i where
    freshLens :: Lens' TCState i
    nextFresh' :: i -> i
    nextFresh' = i -> i
forall a. Enum a => a -> a
succ

{-# INLINE nextFresh #-}
nextFresh :: HasFresh i => TCState -> (i, TCState)
nextFresh :: forall i. HasFresh i => TCState -> (i, TCState)
nextFresh TCState
s =
  let !c :: i
c = TCState
s TCState -> Lens' TCState i -> i
forall o i. o -> Lens' o i -> i
^. (i -> f i) -> TCState -> f TCState
forall i. HasFresh i => Lens' TCState i
Lens' TCState i
freshLens
      !next :: TCState
next = Lens' TCState i -> LensSet TCState i
forall o i. Lens' o i -> LensSet o i
set (i -> f i) -> TCState -> f TCState
forall i. HasFresh i => Lens' TCState i
Lens' TCState i
freshLens (i -> i
forall i. HasFresh i => i -> i
nextFresh' i
c) TCState
s
  in (i
c, TCState
next)

class Monad m => MonadFresh i m where
  fresh :: m i

  default fresh :: (MonadTrans t, MonadFresh i n, t n ~ m) => m i
  fresh = n i -> t n i
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift n i
forall i (m :: * -> *). MonadFresh i m => m i
fresh

instance MonadFresh i m => MonadFresh i (ReaderT r m)
instance MonadFresh i m => MonadFresh i (StateT s m)
instance MonadFresh i m => MonadFresh i (ListT m)
instance MonadFresh i m => MonadFresh i (IdentityT m)

instance HasFresh i => MonadFresh i TCM where
  fresh :: TCM i
fresh = do
        !TCState
s <- TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
        let (!i
c , !TCState
s') = TCState -> (i, TCState)
forall i. HasFresh i => TCState -> (i, TCState)
nextFresh TCState
s
        TCState -> TCMT IO ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
s'
        i -> TCM i
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return i
c
  {-# INLINE fresh #-}

instance HasFresh MetaId where
  freshLens :: Lens' TCState MetaId
freshLens = (MetaId -> f MetaId) -> TCState -> f TCState
Lens' TCState MetaId
stFreshMetaId

instance HasFresh MutualId where
  freshLens :: Lens' TCState MutualId
freshLens = (MutualId -> f MutualId) -> TCState -> f TCState
Lens' TCState MutualId
stFreshMutualId

instance HasFresh InteractionId where
  freshLens :: Lens' TCState InteractionId
freshLens = (InteractionId -> f InteractionId) -> TCState -> f TCState
Lens' TCState InteractionId
stFreshInteractionId

instance HasFresh NameId where
  freshLens :: Lens' TCState NameId
freshLens = (NameId -> f NameId) -> TCState -> f TCState
Lens' TCState NameId
stFreshNameId
  -- nextFresh increments the current fresh name by 2 so @NameId@s used
  -- before caching starts do not overlap with the ones used after.
  nextFresh' :: NameId -> NameId
nextFresh' = NameId -> NameId
forall a. Enum a => a -> a
succ (NameId -> NameId) -> (NameId -> NameId) -> NameId -> NameId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NameId -> NameId
forall a. Enum a => a -> a
succ

instance HasFresh OpaqueId where
  freshLens :: Lens' TCState OpaqueId
freshLens = (OpaqueId -> f OpaqueId) -> TCState -> f TCState
Lens' TCState OpaqueId
stFreshOpaqueId

instance HasFresh Int where
  freshLens :: Lens' TCState Int
freshLens = (Int -> f Int) -> TCState -> f TCState
Lens' TCState Int
stFreshInt

instance HasFresh ProblemId where
  freshLens :: Lens' TCState ProblemId
freshLens = (ProblemId -> f ProblemId) -> TCState -> f TCState
Lens' TCState ProblemId
stFreshProblemId

newtype CheckpointId = CheckpointId Int
  deriving (CheckpointId -> CheckpointId -> Bool
(CheckpointId -> CheckpointId -> Bool)
-> (CheckpointId -> CheckpointId -> Bool) -> Eq CheckpointId
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CheckpointId -> CheckpointId -> Bool
== :: CheckpointId -> CheckpointId -> Bool
$c/= :: CheckpointId -> CheckpointId -> Bool
/= :: CheckpointId -> CheckpointId -> Bool
Eq, Eq CheckpointId
Eq CheckpointId =>
(CheckpointId -> CheckpointId -> Ordering)
-> (CheckpointId -> CheckpointId -> Bool)
-> (CheckpointId -> CheckpointId -> Bool)
-> (CheckpointId -> CheckpointId -> Bool)
-> (CheckpointId -> CheckpointId -> Bool)
-> (CheckpointId -> CheckpointId -> CheckpointId)
-> (CheckpointId -> CheckpointId -> CheckpointId)
-> Ord CheckpointId
CheckpointId -> CheckpointId -> Bool
CheckpointId -> CheckpointId -> Ordering
CheckpointId -> CheckpointId -> CheckpointId
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: CheckpointId -> CheckpointId -> Ordering
compare :: CheckpointId -> CheckpointId -> Ordering
$c< :: CheckpointId -> CheckpointId -> Bool
< :: CheckpointId -> CheckpointId -> Bool
$c<= :: CheckpointId -> CheckpointId -> Bool
<= :: CheckpointId -> CheckpointId -> Bool
$c> :: CheckpointId -> CheckpointId -> Bool
> :: CheckpointId -> CheckpointId -> Bool
$c>= :: CheckpointId -> CheckpointId -> Bool
>= :: CheckpointId -> CheckpointId -> Bool
$cmax :: CheckpointId -> CheckpointId -> CheckpointId
max :: CheckpointId -> CheckpointId -> CheckpointId
$cmin :: CheckpointId -> CheckpointId -> CheckpointId
min :: CheckpointId -> CheckpointId -> CheckpointId
Ord, Int -> CheckpointId
CheckpointId -> Int
CheckpointId -> [CheckpointId]
CheckpointId -> CheckpointId
CheckpointId -> CheckpointId -> [CheckpointId]
CheckpointId -> CheckpointId -> CheckpointId -> [CheckpointId]
(CheckpointId -> CheckpointId)
-> (CheckpointId -> CheckpointId)
-> (Int -> CheckpointId)
-> (CheckpointId -> Int)
-> (CheckpointId -> [CheckpointId])
-> (CheckpointId -> CheckpointId -> [CheckpointId])
-> (CheckpointId -> CheckpointId -> [CheckpointId])
-> (CheckpointId -> CheckpointId -> CheckpointId -> [CheckpointId])
-> Enum CheckpointId
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: CheckpointId -> CheckpointId
succ :: CheckpointId -> CheckpointId
$cpred :: CheckpointId -> CheckpointId
pred :: CheckpointId -> CheckpointId
$ctoEnum :: Int -> CheckpointId
toEnum :: Int -> CheckpointId
$cfromEnum :: CheckpointId -> Int
fromEnum :: CheckpointId -> Int
$cenumFrom :: CheckpointId -> [CheckpointId]
enumFrom :: CheckpointId -> [CheckpointId]
$cenumFromThen :: CheckpointId -> CheckpointId -> [CheckpointId]
enumFromThen :: CheckpointId -> CheckpointId -> [CheckpointId]
$cenumFromTo :: CheckpointId -> CheckpointId -> [CheckpointId]
enumFromTo :: CheckpointId -> CheckpointId -> [CheckpointId]
$cenumFromThenTo :: CheckpointId -> CheckpointId -> CheckpointId -> [CheckpointId]
enumFromThenTo :: CheckpointId -> CheckpointId -> CheckpointId -> [CheckpointId]
Enum, Num CheckpointId
Ord CheckpointId
(Num CheckpointId, Ord CheckpointId) =>
(CheckpointId -> Rational) -> Real CheckpointId
CheckpointId -> Rational
forall a. (Num a, Ord a) => (a -> Rational) -> Real a
$ctoRational :: CheckpointId -> Rational
toRational :: CheckpointId -> Rational
Real, Enum CheckpointId
Real CheckpointId
(Real CheckpointId, Enum CheckpointId) =>
(CheckpointId -> CheckpointId -> CheckpointId)
-> (CheckpointId -> CheckpointId -> CheckpointId)
-> (CheckpointId -> CheckpointId -> CheckpointId)
-> (CheckpointId -> CheckpointId -> CheckpointId)
-> (CheckpointId -> CheckpointId -> (CheckpointId, CheckpointId))
-> (CheckpointId -> CheckpointId -> (CheckpointId, CheckpointId))
-> (CheckpointId -> Integer)
-> Integral CheckpointId
CheckpointId -> Integer
CheckpointId -> CheckpointId -> (CheckpointId, CheckpointId)
CheckpointId -> CheckpointId -> CheckpointId
forall a.
(Real a, Enum a) =>
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> (a, a))
-> (a -> a -> (a, a))
-> (a -> Integer)
-> Integral a
$cquot :: CheckpointId -> CheckpointId -> CheckpointId
quot :: CheckpointId -> CheckpointId -> CheckpointId
$crem :: CheckpointId -> CheckpointId -> CheckpointId
rem :: CheckpointId -> CheckpointId -> CheckpointId
$cdiv :: CheckpointId -> CheckpointId -> CheckpointId
div :: CheckpointId -> CheckpointId -> CheckpointId
$cmod :: CheckpointId -> CheckpointId -> CheckpointId
mod :: CheckpointId -> CheckpointId -> CheckpointId
$cquotRem :: CheckpointId -> CheckpointId -> (CheckpointId, CheckpointId)
quotRem :: CheckpointId -> CheckpointId -> (CheckpointId, CheckpointId)
$cdivMod :: CheckpointId -> CheckpointId -> (CheckpointId, CheckpointId)
divMod :: CheckpointId -> CheckpointId -> (CheckpointId, CheckpointId)
$ctoInteger :: CheckpointId -> Integer
toInteger :: CheckpointId -> Integer
Integral, Integer -> CheckpointId
CheckpointId -> CheckpointId
CheckpointId -> CheckpointId -> CheckpointId
(CheckpointId -> CheckpointId -> CheckpointId)
-> (CheckpointId -> CheckpointId -> CheckpointId)
-> (CheckpointId -> CheckpointId -> CheckpointId)
-> (CheckpointId -> CheckpointId)
-> (CheckpointId -> CheckpointId)
-> (CheckpointId -> CheckpointId)
-> (Integer -> CheckpointId)
-> Num CheckpointId
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: CheckpointId -> CheckpointId -> CheckpointId
+ :: CheckpointId -> CheckpointId -> CheckpointId
$c- :: CheckpointId -> CheckpointId -> CheckpointId
- :: CheckpointId -> CheckpointId -> CheckpointId
$c* :: CheckpointId -> CheckpointId -> CheckpointId
* :: CheckpointId -> CheckpointId -> CheckpointId
$cnegate :: CheckpointId -> CheckpointId
negate :: CheckpointId -> CheckpointId
$cabs :: CheckpointId -> CheckpointId
abs :: CheckpointId -> CheckpointId
$csignum :: CheckpointId -> CheckpointId
signum :: CheckpointId -> CheckpointId
$cfromInteger :: Integer -> CheckpointId
fromInteger :: Integer -> CheckpointId
Num, CheckpointId -> ()
(CheckpointId -> ()) -> NFData CheckpointId
forall a. (a -> ()) -> NFData a
$crnf :: CheckpointId -> ()
rnf :: CheckpointId -> ()
NFData)

instance Show CheckpointId where
  show :: CheckpointId -> String
show (CheckpointId Int
n) = Int -> String
forall a. Show a => a -> String
show Int
n

instance Pretty CheckpointId where
  pretty :: CheckpointId -> Doc
pretty (CheckpointId Int
n) = Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
n

instance HasFresh CheckpointId where
  freshLens :: Lens' TCState CheckpointId
freshLens = (CheckpointId -> f CheckpointId) -> TCState -> f TCState
Lens' TCState CheckpointId
stFreshCheckpointId

freshName :: MonadFresh NameId m => Range -> String -> m Name
freshName :: forall (m :: * -> *).
MonadFresh NameId m =>
Range -> String -> m Name
freshName Range
r String
s = do
  NameId
i <- m NameId
forall i (m :: * -> *). MonadFresh i m => m i
fresh
  Name -> m Name
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> m Name) -> Name -> m Name
forall a b. (a -> b) -> a -> b
$ Range -> NameId -> String -> Name
forall a. MkName a => Range -> NameId -> a -> Name
mkName Range
r NameId
i String
s

freshNoName :: MonadFresh NameId m => Range -> m Name
freshNoName :: forall (m :: * -> *). MonadFresh NameId m => Range -> m Name
freshNoName Range
r =
    do  NameId
i <- m NameId
forall i (m :: * -> *). MonadFresh i m => m i
fresh
        Name -> m Name
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> m Name) -> Name -> m Name
forall a b. (a -> b) -> a -> b
$ NameId -> Name -> Range -> Fixity' -> Bool -> Name
makeName NameId
i (Range -> NameId -> Name
C.NoName Range
forall a. Range' a
noRange NameId
i) Range
r Fixity'
noFixity' Bool
False

freshNoName_ :: MonadFresh NameId m => m Name
freshNoName_ :: forall (m :: * -> *). MonadFresh NameId m => m Name
freshNoName_ = Range -> m Name
forall (m :: * -> *). MonadFresh NameId m => Range -> m Name
freshNoName Range
forall a. Range' a
noRange

freshRecordName :: MonadFresh NameId m => m Name
freshRecordName :: forall (m :: * -> *). MonadFresh NameId m => m Name
freshRecordName = do
  NameId
i <- m NameId
forall i (m :: * -> *). MonadFresh i m => m i
fresh
  Name -> m Name
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> m Name) -> Name -> m Name
forall a b. (a -> b) -> a -> b
$ NameId -> Name -> Range -> Fixity' -> Bool -> Name
makeName NameId
i (Name -> Name
forall a. LensInScope a => a -> a
C.setNotInScope (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ String -> Name
C.simpleName String
"r") Range
forall a. Range' a
noRange Fixity'
noFixity' Bool
True

-- | Create a fresh name from @a@.
class FreshName a where
  freshName_ :: MonadFresh NameId m => a -> m Name

instance FreshName (Range, String) where
  freshName_ :: forall (m :: * -> *).
MonadFresh NameId m =>
(Range, String) -> m Name
freshName_ = (Range -> String -> m Name) -> (Range, String) -> m Name
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Range -> String -> m Name
forall (m :: * -> *).
MonadFresh NameId m =>
Range -> String -> m Name
freshName

instance FreshName String where
  freshName_ :: forall (m :: * -> *). MonadFresh NameId m => String -> m Name
freshName_ = Range -> String -> m Name
forall (m :: * -> *).
MonadFresh NameId m =>
Range -> String -> m Name
freshName Range
forall a. Range' a
noRange

instance FreshName Range where
  freshName_ :: forall (m :: * -> *). MonadFresh NameId m => Range -> m Name
freshName_ = Range -> m Name
forall (m :: * -> *). MonadFresh NameId m => Range -> m Name
freshNoName

instance FreshName () where
  freshName_ :: forall (m :: * -> *). MonadFresh NameId m => () -> m Name
freshName_ () = m Name
forall (m :: * -> *). MonadFresh NameId m => m Name
freshNoName_

---------------------------------------------------------------------------
-- ** Managing file names
---------------------------------------------------------------------------

-- | Maps top-level module names to the corresponding source file
-- names.

type ModuleToSource = Map TopLevelModuleName AbsolutePath

---------------------------------------------------------------------------
-- ** Associating concrete names to an abstract name
---------------------------------------------------------------------------

-- | A monad that has read and write access to the stConcreteNames
--   part of the TCState. Basically, this is a synonym for `MonadState
--   ConcreteNames m` (which cannot be used directly because of the
--   limitations of Haskell's typeclass system).
class Monad m => MonadStConcreteNames m where
  runStConcreteNames :: StateT ConcreteNames m a -> m a

  useConcreteNames :: m ConcreteNames
  useConcreteNames = StateT ConcreteNames m ConcreteNames -> m ConcreteNames
forall a. StateT ConcreteNames m a -> m a
forall (m :: * -> *) a.
MonadStConcreteNames m =>
StateT ConcreteNames m a -> m a
runStConcreteNames StateT ConcreteNames m ConcreteNames
forall s (m :: * -> *). MonadState s m => m s
get

  modifyConcreteNames :: (ConcreteNames -> ConcreteNames) -> m ()
  modifyConcreteNames = StateT ConcreteNames m () -> m ()
forall a. StateT ConcreteNames m a -> m a
forall (m :: * -> *) a.
MonadStConcreteNames m =>
StateT ConcreteNames m a -> m a
runStConcreteNames (StateT ConcreteNames m () -> m ())
-> ((ConcreteNames -> ConcreteNames) -> StateT ConcreteNames m ())
-> (ConcreteNames -> ConcreteNames)
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ConcreteNames -> ConcreteNames) -> StateT ConcreteNames m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify

instance MonadStConcreteNames TCM where
  runStConcreteNames :: forall a. StateT ConcreteNames (TCMT IO) a -> TCM a
runStConcreteNames StateT ConcreteNames (TCMT IO) a
m = Lens' TCState ConcreteNames
-> (ConcreteNames -> TCMT IO (a, ConcreteNames)) -> TCMT IO a
forall (m :: * -> *) a r.
MonadTCState m =>
Lens' TCState a -> (a -> m (r, a)) -> m r
stateTCLensM (ConcreteNames -> f ConcreteNames) -> TCState -> f TCState
Lens' TCState ConcreteNames
stConcreteNames ((ConcreteNames -> TCMT IO (a, ConcreteNames)) -> TCMT IO a)
-> (ConcreteNames -> TCMT IO (a, ConcreteNames)) -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ StateT ConcreteNames (TCMT IO) a
-> ConcreteNames -> TCMT IO (a, ConcreteNames)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT ConcreteNames (TCMT IO) a
m

instance MonadStConcreteNames m => MonadStConcreteNames (IdentityT m) where
  runStConcreteNames :: forall a. StateT ConcreteNames (IdentityT m) a -> IdentityT m a
runStConcreteNames StateT ConcreteNames (IdentityT m) a
m = m a -> IdentityT m a
forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT (m a -> IdentityT m a) -> m a -> IdentityT m a
forall a b. (a -> b) -> a -> b
$ StateT ConcreteNames m a -> m a
forall a. StateT ConcreteNames m a -> m a
forall (m :: * -> *) a.
MonadStConcreteNames m =>
StateT ConcreteNames m a -> m a
runStConcreteNames (StateT ConcreteNames m a -> m a)
-> StateT ConcreteNames m a -> m a
forall a b. (a -> b) -> a -> b
$ (ConcreteNames -> m (a, ConcreteNames)) -> StateT ConcreteNames m a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((ConcreteNames -> m (a, ConcreteNames))
 -> StateT ConcreteNames m a)
-> (ConcreteNames -> m (a, ConcreteNames))
-> StateT ConcreteNames m a
forall a b. (a -> b) -> a -> b
$ IdentityT m (a, ConcreteNames) -> m (a, ConcreteNames)
forall {k} (f :: k -> *) (a :: k). IdentityT f a -> f a
runIdentityT (IdentityT m (a, ConcreteNames) -> m (a, ConcreteNames))
-> (ConcreteNames -> IdentityT m (a, ConcreteNames))
-> ConcreteNames
-> m (a, ConcreteNames)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT ConcreteNames (IdentityT m) a
-> ConcreteNames -> IdentityT m (a, ConcreteNames)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT ConcreteNames (IdentityT m) a
m

instance MonadStConcreteNames m => MonadStConcreteNames (ReaderT r m) where
  runStConcreteNames :: forall a. StateT ConcreteNames (ReaderT r m) a -> ReaderT r m a
runStConcreteNames StateT ConcreteNames (ReaderT r m) a
m = (r -> m a) -> ReaderT r m a
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((r -> m a) -> ReaderT r m a) -> (r -> m a) -> ReaderT r m a
forall a b. (a -> b) -> a -> b
$ StateT ConcreteNames m a -> m a
forall a. StateT ConcreteNames m a -> m a
forall (m :: * -> *) a.
MonadStConcreteNames m =>
StateT ConcreteNames m a -> m a
runStConcreteNames (StateT ConcreteNames m a -> m a)
-> (r -> StateT ConcreteNames m a) -> r -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ConcreteNames -> m (a, ConcreteNames)) -> StateT ConcreteNames m a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((ConcreteNames -> m (a, ConcreteNames))
 -> StateT ConcreteNames m a)
-> (r -> ConcreteNames -> m (a, ConcreteNames))
-> r
-> StateT ConcreteNames m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ConcreteNames -> r -> m (a, ConcreteNames))
-> r -> ConcreteNames -> m (a, ConcreteNames)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (ReaderT r m (a, ConcreteNames) -> r -> m (a, ConcreteNames)
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (ReaderT r m (a, ConcreteNames) -> r -> m (a, ConcreteNames))
-> (ConcreteNames -> ReaderT r m (a, ConcreteNames))
-> ConcreteNames
-> r
-> m (a, ConcreteNames)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT ConcreteNames (ReaderT r m) a
-> ConcreteNames -> ReaderT r m (a, ConcreteNames)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT ConcreteNames (ReaderT r m) a
m)

instance MonadStConcreteNames m => MonadStConcreteNames (StateT s m) where
  runStConcreteNames :: forall a. StateT ConcreteNames (StateT s m) a -> StateT s m a
runStConcreteNames StateT ConcreteNames (StateT s m) a
m = (s -> m (a, s)) -> StateT s m a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((s -> m (a, s)) -> StateT s m a)
-> (s -> m (a, s)) -> StateT s m a
forall a b. (a -> b) -> a -> b
$ \s
s -> StateT ConcreteNames m (a, s) -> m (a, s)
forall a. StateT ConcreteNames m a -> m a
forall (m :: * -> *) a.
MonadStConcreteNames m =>
StateT ConcreteNames m a -> m a
runStConcreteNames (StateT ConcreteNames m (a, s) -> m (a, s))
-> StateT ConcreteNames m (a, s) -> m (a, s)
forall a b. (a -> b) -> a -> b
$ (ConcreteNames -> m ((a, s), ConcreteNames))
-> StateT ConcreteNames m (a, s)
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((ConcreteNames -> m ((a, s), ConcreteNames))
 -> StateT ConcreteNames m (a, s))
-> (ConcreteNames -> m ((a, s), ConcreteNames))
-> StateT ConcreteNames m (a, s)
forall a b. (a -> b) -> a -> b
$ \ConcreteNames
ns -> do
    ((a
x,ConcreteNames
ns'),s
s') <- StateT s m (a, ConcreteNames) -> s -> m ((a, ConcreteNames), s)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (StateT ConcreteNames (StateT s m) a
-> ConcreteNames -> StateT s m (a, ConcreteNames)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT ConcreteNames (StateT s m) a
m ConcreteNames
ns) s
s
    ((a, s), ConcreteNames) -> m ((a, s), ConcreteNames)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((a
x,s
s'),ConcreteNames
ns')

---------------------------------------------------------------------------
-- ** Interface
---------------------------------------------------------------------------


-- | Distinguishes between type-checked and scope-checked interfaces
--   when stored in the map of `VisitedModules`.
data ModuleCheckMode
  = ModuleScopeChecked
  | ModuleTypeChecked
  deriving (ModuleCheckMode -> ModuleCheckMode -> Bool
(ModuleCheckMode -> ModuleCheckMode -> Bool)
-> (ModuleCheckMode -> ModuleCheckMode -> Bool)
-> Eq ModuleCheckMode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ModuleCheckMode -> ModuleCheckMode -> Bool
== :: ModuleCheckMode -> ModuleCheckMode -> Bool
$c/= :: ModuleCheckMode -> ModuleCheckMode -> Bool
/= :: ModuleCheckMode -> ModuleCheckMode -> Bool
Eq, Eq ModuleCheckMode
Eq ModuleCheckMode =>
(ModuleCheckMode -> ModuleCheckMode -> Ordering)
-> (ModuleCheckMode -> ModuleCheckMode -> Bool)
-> (ModuleCheckMode -> ModuleCheckMode -> Bool)
-> (ModuleCheckMode -> ModuleCheckMode -> Bool)
-> (ModuleCheckMode -> ModuleCheckMode -> Bool)
-> (ModuleCheckMode -> ModuleCheckMode -> ModuleCheckMode)
-> (ModuleCheckMode -> ModuleCheckMode -> ModuleCheckMode)
-> Ord ModuleCheckMode
ModuleCheckMode -> ModuleCheckMode -> Bool
ModuleCheckMode -> ModuleCheckMode -> Ordering
ModuleCheckMode -> ModuleCheckMode -> ModuleCheckMode
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ModuleCheckMode -> ModuleCheckMode -> Ordering
compare :: ModuleCheckMode -> ModuleCheckMode -> Ordering
$c< :: ModuleCheckMode -> ModuleCheckMode -> Bool
< :: ModuleCheckMode -> ModuleCheckMode -> Bool
$c<= :: ModuleCheckMode -> ModuleCheckMode -> Bool
<= :: ModuleCheckMode -> ModuleCheckMode -> Bool
$c> :: ModuleCheckMode -> ModuleCheckMode -> Bool
> :: ModuleCheckMode -> ModuleCheckMode -> Bool
$c>= :: ModuleCheckMode -> ModuleCheckMode -> Bool
>= :: ModuleCheckMode -> ModuleCheckMode -> Bool
$cmax :: ModuleCheckMode -> ModuleCheckMode -> ModuleCheckMode
max :: ModuleCheckMode -> ModuleCheckMode -> ModuleCheckMode
$cmin :: ModuleCheckMode -> ModuleCheckMode -> ModuleCheckMode
min :: ModuleCheckMode -> ModuleCheckMode -> ModuleCheckMode
Ord, ModuleCheckMode
ModuleCheckMode -> ModuleCheckMode -> Bounded ModuleCheckMode
forall a. a -> a -> Bounded a
$cminBound :: ModuleCheckMode
minBound :: ModuleCheckMode
$cmaxBound :: ModuleCheckMode
maxBound :: ModuleCheckMode
Bounded, Int -> ModuleCheckMode
ModuleCheckMode -> Int
ModuleCheckMode -> [ModuleCheckMode]
ModuleCheckMode -> ModuleCheckMode
ModuleCheckMode -> ModuleCheckMode -> [ModuleCheckMode]
ModuleCheckMode
-> ModuleCheckMode -> ModuleCheckMode -> [ModuleCheckMode]
(ModuleCheckMode -> ModuleCheckMode)
-> (ModuleCheckMode -> ModuleCheckMode)
-> (Int -> ModuleCheckMode)
-> (ModuleCheckMode -> Int)
-> (ModuleCheckMode -> [ModuleCheckMode])
-> (ModuleCheckMode -> ModuleCheckMode -> [ModuleCheckMode])
-> (ModuleCheckMode -> ModuleCheckMode -> [ModuleCheckMode])
-> (ModuleCheckMode
    -> ModuleCheckMode -> ModuleCheckMode -> [ModuleCheckMode])
-> Enum ModuleCheckMode
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: ModuleCheckMode -> ModuleCheckMode
succ :: ModuleCheckMode -> ModuleCheckMode
$cpred :: ModuleCheckMode -> ModuleCheckMode
pred :: ModuleCheckMode -> ModuleCheckMode
$ctoEnum :: Int -> ModuleCheckMode
toEnum :: Int -> ModuleCheckMode
$cfromEnum :: ModuleCheckMode -> Int
fromEnum :: ModuleCheckMode -> Int
$cenumFrom :: ModuleCheckMode -> [ModuleCheckMode]
enumFrom :: ModuleCheckMode -> [ModuleCheckMode]
$cenumFromThen :: ModuleCheckMode -> ModuleCheckMode -> [ModuleCheckMode]
enumFromThen :: ModuleCheckMode -> ModuleCheckMode -> [ModuleCheckMode]
$cenumFromTo :: ModuleCheckMode -> ModuleCheckMode -> [ModuleCheckMode]
enumFromTo :: ModuleCheckMode -> ModuleCheckMode -> [ModuleCheckMode]
$cenumFromThenTo :: ModuleCheckMode
-> ModuleCheckMode -> ModuleCheckMode -> [ModuleCheckMode]
enumFromThenTo :: ModuleCheckMode
-> ModuleCheckMode -> ModuleCheckMode -> [ModuleCheckMode]
Enum, Int -> ModuleCheckMode -> ShowS
[ModuleCheckMode] -> ShowS
ModuleCheckMode -> String
(Int -> ModuleCheckMode -> ShowS)
-> (ModuleCheckMode -> String)
-> ([ModuleCheckMode] -> ShowS)
-> Show ModuleCheckMode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ModuleCheckMode -> ShowS
showsPrec :: Int -> ModuleCheckMode -> ShowS
$cshow :: ModuleCheckMode -> String
show :: ModuleCheckMode -> String
$cshowList :: [ModuleCheckMode] -> ShowS
showList :: [ModuleCheckMode] -> ShowS
Show, (forall x. ModuleCheckMode -> Rep ModuleCheckMode x)
-> (forall x. Rep ModuleCheckMode x -> ModuleCheckMode)
-> Generic ModuleCheckMode
forall x. Rep ModuleCheckMode x -> ModuleCheckMode
forall x. ModuleCheckMode -> Rep ModuleCheckMode x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ModuleCheckMode -> Rep ModuleCheckMode x
from :: forall x. ModuleCheckMode -> Rep ModuleCheckMode x
$cto :: forall x. Rep ModuleCheckMode x -> ModuleCheckMode
to :: forall x. Rep ModuleCheckMode x -> ModuleCheckMode
Generic)


data ModuleInfo = ModuleInfo
  { ModuleInfo -> Interface
miInterface  :: Interface
  , ModuleInfo -> [TCWarning]
miWarnings   :: [TCWarning]
    -- ^ Warnings were encountered when the module was type checked.
    --   These might include warnings not stored in the interface itself,
    --   specifically unsolved interaction metas.
    --   See "Agda.Interaction.Imports"
  , ModuleInfo -> Bool
miPrimitive  :: Bool
    -- ^ 'True' if the module is a primitive module, which should always
    -- be importable.
  , ModuleInfo -> ModuleCheckMode
miMode       :: ModuleCheckMode
    -- ^ The `ModuleCheckMode` used to create the `Interface`
  }
  deriving (forall x. ModuleInfo -> Rep ModuleInfo x)
-> (forall x. Rep ModuleInfo x -> ModuleInfo) -> Generic ModuleInfo
forall x. Rep ModuleInfo x -> ModuleInfo
forall x. ModuleInfo -> Rep ModuleInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ModuleInfo -> Rep ModuleInfo x
from :: forall x. ModuleInfo -> Rep ModuleInfo x
$cto :: forall x. Rep ModuleInfo x -> ModuleInfo
to :: forall x. Rep ModuleInfo x -> ModuleInfo
Generic

type VisitedModules = Map TopLevelModuleName ModuleInfo
type DecodedModules = Map TopLevelModuleName ModuleInfo

data ForeignCode = ForeignCode Range String
  deriving (Int -> ForeignCode -> ShowS
[ForeignCode] -> ShowS
ForeignCode -> String
(Int -> ForeignCode -> ShowS)
-> (ForeignCode -> String)
-> ([ForeignCode] -> ShowS)
-> Show ForeignCode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ForeignCode -> ShowS
showsPrec :: Int -> ForeignCode -> ShowS
$cshow :: ForeignCode -> String
show :: ForeignCode -> String
$cshowList :: [ForeignCode] -> ShowS
showList :: [ForeignCode] -> ShowS
Show, (forall x. ForeignCode -> Rep ForeignCode x)
-> (forall x. Rep ForeignCode x -> ForeignCode)
-> Generic ForeignCode
forall x. Rep ForeignCode x -> ForeignCode
forall x. ForeignCode -> Rep ForeignCode x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ForeignCode -> Rep ForeignCode x
from :: forall x. ForeignCode -> Rep ForeignCode x
$cto :: forall x. Rep ForeignCode x -> ForeignCode
to :: forall x. Rep ForeignCode x -> ForeignCode
Generic)

-- | Foreign code fragments are stored in reversed order to support efficient appending:
--   head points to the latest pragma in module.
newtype ForeignCodeStack = ForeignCodeStack
  { ForeignCodeStack -> [ForeignCode]
getForeignCodeStack :: [ForeignCode]
  } deriving (Int -> ForeignCodeStack -> ShowS
[ForeignCodeStack] -> ShowS
ForeignCodeStack -> String
(Int -> ForeignCodeStack -> ShowS)
-> (ForeignCodeStack -> String)
-> ([ForeignCodeStack] -> ShowS)
-> Show ForeignCodeStack
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ForeignCodeStack -> ShowS
showsPrec :: Int -> ForeignCodeStack -> ShowS
$cshow :: ForeignCodeStack -> String
show :: ForeignCodeStack -> String
$cshowList :: [ForeignCodeStack] -> ShowS
showList :: [ForeignCodeStack] -> ShowS
Show, (forall x. ForeignCodeStack -> Rep ForeignCodeStack x)
-> (forall x. Rep ForeignCodeStack x -> ForeignCodeStack)
-> Generic ForeignCodeStack
forall x. Rep ForeignCodeStack x -> ForeignCodeStack
forall x. ForeignCodeStack -> Rep ForeignCodeStack x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ForeignCodeStack -> Rep ForeignCodeStack x
from :: forall x. ForeignCodeStack -> Rep ForeignCodeStack x
$cto :: forall x. Rep ForeignCodeStack x -> ForeignCodeStack
to :: forall x. Rep ForeignCodeStack x -> ForeignCodeStack
Generic, ForeignCodeStack -> ()
(ForeignCodeStack -> ()) -> NFData ForeignCodeStack
forall a. (a -> ()) -> NFData a
$crnf :: ForeignCodeStack -> ()
rnf :: ForeignCodeStack -> ()
NFData)

data Interface = Interface
  { Interface -> Word64
iSourceHash      :: !Hash
    -- ^ Hash of the source code.
  , Interface -> Text
iSource          :: TL.Text
    -- ^ The source code. The source code is stored so that the HTML
    -- and LaTeX backends can generate their output without having to
    -- re-read the (possibly out of date) source code.
  , Interface -> FileType
iFileType        :: FileType
    -- ^ Source file type, determined from the file extension
  , Interface -> [(TopLevelModuleName, Word64)]
iImportedModules :: [(TopLevelModuleName, Hash)]
    -- ^ Imported modules and their hashes.
  , Interface -> ModuleName
iModuleName      :: ModuleName
    -- ^ Module name of this interface.
  , Interface -> TopLevelModuleName
iTopLevelModuleName :: TopLevelModuleName
    -- ^ The module's top-level module name.
  , Interface -> Map ModuleName Scope
iScope           :: Map ModuleName Scope
    -- ^ Scope defined by this module.
    --
    --   Andreas, AIM XX: Too avoid duplicate serialization, this field is
    --   not serialized, so if you deserialize an interface, @iScope@
    --   will be empty.
    --   But 'constructIScope' constructs 'iScope' from 'iInsideScope'.
  , Interface -> ScopeInfo
iInsideScope     :: ScopeInfo
    -- ^ Scope after we loaded this interface.
    --   Used in 'Agda.Interaction.BasicOps.AtTopLevel'
    --   and     'Agda.Interaction.CommandLine.interactionLoop'.
  , Interface -> Signature
iSignature       :: Signature
  , Interface -> RemoteMetaStore
iMetaBindings    :: RemoteMetaStore
    -- ^ Instantiations for meta-variables that come from this module.
  , Interface -> DisplayForms
iDisplayForms    :: DisplayForms
    -- ^ Display forms added for imported identifiers.
  , Interface -> Map QName Text
iUserWarnings    :: Map A.QName Text
    -- ^ User warnings for imported identifiers
  , Interface -> Maybe Text
iImportWarning   :: Maybe Text
    -- ^ Whether this module should raise a warning when imported
  , Interface -> BuiltinThings (PrimitiveId, QName)
iBuiltin         :: BuiltinThings (PrimitiveId, QName)
  , Interface -> Map String ForeignCodeStack
iForeignCode     :: Map BackendName ForeignCodeStack
  , Interface -> HighlightingInfo
iHighlighting    :: HighlightingInfo
  , Interface -> [OptionsPragma]
iDefaultPragmaOptions :: [OptionsPragma]
    -- ^ Pragma options set in library files.
  , Interface -> [OptionsPragma]
iFilePragmaOptions    :: [OptionsPragma]
    -- ^ Pragma options set in the file.
  , Interface -> PragmaOptions
iOptionsUsed     :: PragmaOptions
    -- ^ Options/features used when checking the file (can be different
    --   from options set directly in the file).
  , Interface -> PatternSynDefns
iPatternSyns     :: A.PatternSynDefns
  , Interface -> [TCWarning]
iWarnings        :: [TCWarning]
  , Interface -> Set QName
iPartialDefs     :: Set QName
  , Interface -> Map OpaqueId OpaqueBlock
iOpaqueBlocks    :: Map OpaqueId OpaqueBlock
  , Interface -> Map QName OpaqueId
iOpaqueNames     :: Map QName OpaqueId
  }
  deriving (Int -> Interface -> ShowS
[Interface] -> ShowS
Interface -> String
(Int -> Interface -> ShowS)
-> (Interface -> String)
-> ([Interface] -> ShowS)
-> Show Interface
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Interface -> ShowS
showsPrec :: Int -> Interface -> ShowS
$cshow :: Interface -> String
show :: Interface -> String
$cshowList :: [Interface] -> ShowS
showList :: [Interface] -> ShowS
Show, (forall x. Interface -> Rep Interface x)
-> (forall x. Rep Interface x -> Interface) -> Generic Interface
forall x. Rep Interface x -> Interface
forall x. Interface -> Rep Interface x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Interface -> Rep Interface x
from :: forall x. Interface -> Rep Interface x
$cto :: forall x. Rep Interface x -> Interface
to :: forall x. Rep Interface x -> Interface
Generic)

instance Pretty Interface where
  pretty :: Interface -> Doc
pretty (Interface
            Word64
sourceH Text
source FileType
fileT [(TopLevelModuleName, Word64)]
importedM ModuleName
moduleN TopLevelModuleName
topModN Map ModuleName Scope
scope ScopeInfo
insideS
            Signature
signature RemoteMetaStore
metas DisplayForms
display Map QName Text
userwarn Maybe Text
importwarn BuiltinThings (PrimitiveId, QName)
builtin
            Map String ForeignCodeStack
foreignCode HighlightingInfo
highlighting [OptionsPragma]
libPragmaO [OptionsPragma]
filePragmaO PragmaOptions
oUsed
            PatternSynDefns
patternS [TCWarning]
warnings Set QName
partialdefs Map OpaqueId OpaqueBlock
oblocks Map QName OpaqueId
onames) =

    Doc -> Int -> Doc -> Doc
forall a. Doc a -> Int -> Doc a -> Doc a
hang Doc
"Interface" Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
      [ Doc
"source hash:"         Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc) -> (Word64 -> String) -> Word64 -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> String
forall a. Show a => a -> String
show) Word64
sourceH
      , Doc
"source:"              Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
$$  Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (String -> Doc
forall a. String -> Doc a
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Text -> String
TL.unpack Text
source)
      , Doc
"file type:"           Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc) -> (FileType -> String) -> FileType -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FileType -> String
forall a. Show a => a -> String
show) FileType
fileT
      , Doc
"imported modules:"    Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc)
-> ([(TopLevelModuleName, Word64)] -> String)
-> [(TopLevelModuleName, Word64)]
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(TopLevelModuleName, Word64)] -> String
forall a. Show a => a -> String
show) [(TopLevelModuleName, Word64)]
importedM
      , Doc
"module name:"         Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> ModuleName -> Doc
forall a. Pretty a => a -> Doc
pretty ModuleName
moduleN
      , Doc
"top-level module name:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> TopLevelModuleName -> Doc
forall a. Pretty a => a -> Doc
pretty TopLevelModuleName
topModN
      , Doc
"scope:"               Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc)
-> (Map ModuleName Scope -> String) -> Map ModuleName Scope -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map ModuleName Scope -> String
forall a. Show a => a -> String
show) Map ModuleName Scope
scope
      , Doc
"inside scope:"        Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc) -> (ScopeInfo -> String) -> ScopeInfo -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeInfo -> String
forall a. Show a => a -> String
show) ScopeInfo
insideS
      , Doc
"signature:"           Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc) -> (Signature -> String) -> Signature -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signature -> String
forall a. Show a => a -> String
show) Signature
signature
      , Doc
"meta-variables:"      Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc)
-> (RemoteMetaStore -> String) -> RemoteMetaStore -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RemoteMetaStore -> String
forall a. Show a => a -> String
show) RemoteMetaStore
metas
      , Doc
"display:"             Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc) -> (DisplayForms -> String) -> DisplayForms -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DisplayForms -> String
forall a. Show a => a -> String
show) DisplayForms
display
      , Doc
"user warnings:"       Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc)
-> (Map QName Text -> String) -> Map QName Text -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map QName Text -> String
forall a. Show a => a -> String
show) Map QName Text
userwarn
      , Doc
"import warning:"      Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc) -> (Maybe Text -> String) -> Maybe Text -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Text -> String
forall a. Show a => a -> String
show) Maybe Text
importwarn
      , Doc
"builtin:"             Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc)
-> (BuiltinThings (PrimitiveId, QName) -> String)
-> BuiltinThings (PrimitiveId, QName)
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinThings (PrimitiveId, QName) -> String
forall a. Show a => a -> String
show) BuiltinThings (PrimitiveId, QName)
builtin
      , Doc
"Foreign code:"        Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc)
-> (Map String ForeignCodeStack -> String)
-> Map String ForeignCodeStack
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map String ForeignCodeStack -> String
forall a. Show a => a -> String
show) Map String ForeignCodeStack
foreignCode
      , Doc
"highlighting:"        Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc)
-> (HighlightingInfo -> String) -> HighlightingInfo -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HighlightingInfo -> String
forall a. Show a => a -> String
show) HighlightingInfo
highlighting
      , Doc
"library pragma options:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc)
-> ([OptionsPragma] -> String) -> [OptionsPragma] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [OptionsPragma] -> String
forall a. Show a => a -> String
show) [OptionsPragma]
libPragmaO
      , Doc
"file pragma options:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc)
-> ([OptionsPragma] -> String) -> [OptionsPragma] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [OptionsPragma] -> String
forall a. Show a => a -> String
show) [OptionsPragma]
filePragmaO
      , Doc
"options used:"        Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc)
-> (PragmaOptions -> String) -> PragmaOptions -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> String
forall a. Show a => a -> String
show) PragmaOptions
oUsed
      , Doc
"pattern syns:"        Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc)
-> (PatternSynDefns -> String) -> PatternSynDefns -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatternSynDefns -> String
forall a. Show a => a -> String
show) PatternSynDefns
patternS
      , Doc
"warnings:"            Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc) -> ([TCWarning] -> String) -> [TCWarning] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TCWarning] -> String
forall a. Show a => a -> String
show) [TCWarning]
warnings
      , Doc
"partial definitions:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (String -> Doc
forall a. Pretty a => a -> Doc
pretty (String -> Doc) -> (Set QName -> String) -> Set QName -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set QName -> String
forall a. Show a => a -> String
show) Set QName
partialdefs
      , Doc
"opaque blocks:"       Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Map OpaqueId OpaqueBlock -> Doc
forall a. Pretty a => a -> Doc
pretty Map OpaqueId OpaqueBlock
oblocks
      , Doc
"opaque names"         Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Map QName OpaqueId -> Doc
forall a. Pretty a => a -> Doc
pretty Map QName OpaqueId
onames
      ]

-- | Combines the source hash and the (full) hashes of the imported modules.
iFullHash :: Interface -> Hash
iFullHash :: Interface -> Word64
iFullHash Interface
i = [Word64] -> Word64
combineHashes ([Word64] -> Word64) -> [Word64] -> Word64
forall a b. (a -> b) -> a -> b
$ Interface -> Word64
iSourceHash Interface
i Word64 -> [Word64] -> [Word64]
forall a. a -> [a] -> [a]
: ((TopLevelModuleName, Word64) -> Word64)
-> [(TopLevelModuleName, Word64)] -> [Word64]
forall a b. (a -> b) -> [a] -> [b]
List.map (TopLevelModuleName, Word64) -> Word64
forall a b. (a, b) -> b
snd (Interface -> [(TopLevelModuleName, Word64)]
iImportedModules Interface
i)

-- | A lens for the 'iSignature' field of the 'Interface' type.

intSignature :: Lens' Interface Signature
intSignature :: Lens' Interface Signature
intSignature Signature -> f Signature
f Interface
i = Signature -> f Signature
f (Interface -> Signature
iSignature Interface
i) f Signature -> (Signature -> Interface) -> f Interface
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Signature
s -> Interface
i { iSignature = s }

---------------------------------------------------------------------------
-- ** Closure
---------------------------------------------------------------------------

data Closure a = Closure
  { forall a. Closure a -> Signature
clSignature        :: Signature
  , forall a. Closure a -> TCEnv
clEnv              :: TCEnv
  , forall a. Closure a -> ScopeInfo
clScope            :: ScopeInfo
  , forall a. Closure a -> Map ModuleName CheckpointId
clModuleCheckpoints :: Map ModuleName CheckpointId
  , forall a. Closure a -> a
clValue            :: a
  }
    deriving ((forall a b. (a -> b) -> Closure a -> Closure b)
-> (forall a b. a -> Closure b -> Closure a) -> Functor Closure
forall a b. a -> Closure b -> Closure a
forall a b. (a -> b) -> Closure a -> Closure b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Closure a -> Closure b
fmap :: forall a b. (a -> b) -> Closure a -> Closure b
$c<$ :: forall a b. a -> Closure b -> Closure a
<$ :: forall a b. a -> Closure b -> Closure a
Functor, (forall m. Monoid m => Closure m -> m)
-> (forall m a. Monoid m => (a -> m) -> Closure a -> m)
-> (forall m a. Monoid m => (a -> m) -> Closure a -> m)
-> (forall a b. (a -> b -> b) -> b -> Closure a -> b)
-> (forall a b. (a -> b -> b) -> b -> Closure a -> b)
-> (forall b a. (b -> a -> b) -> b -> Closure a -> b)
-> (forall b a. (b -> a -> b) -> b -> Closure a -> b)
-> (forall a. (a -> a -> a) -> Closure a -> a)
-> (forall a. (a -> a -> a) -> Closure a -> a)
-> (forall a. Closure a -> [a])
-> (forall a. Closure a -> Bool)
-> (forall a. Closure a -> Int)
-> (forall a. Eq a => a -> Closure a -> Bool)
-> (forall a. Ord a => Closure a -> a)
-> (forall a. Ord a => Closure a -> a)
-> (forall a. Num a => Closure a -> a)
-> (forall a. Num a => Closure a -> a)
-> Foldable Closure
forall a. Eq a => a -> Closure a -> Bool
forall a. Num a => Closure a -> a
forall a. Ord a => Closure a -> a
forall m. Monoid m => Closure m -> m
forall a. Closure a -> Bool
forall a. Closure a -> Int
forall a. Closure a -> [a]
forall a. (a -> a -> a) -> Closure a -> a
forall m a. Monoid m => (a -> m) -> Closure a -> m
forall b a. (b -> a -> b) -> b -> Closure a -> b
forall a b. (a -> b -> b) -> b -> Closure a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Closure m -> m
fold :: forall m. Monoid m => Closure m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Closure a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Closure a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Closure a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Closure a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Closure a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Closure a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Closure a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Closure a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Closure a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Closure a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Closure a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Closure a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Closure a -> a
foldr1 :: forall a. (a -> a -> a) -> Closure a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Closure a -> a
foldl1 :: forall a. (a -> a -> a) -> Closure a -> a
$ctoList :: forall a. Closure a -> [a]
toList :: forall a. Closure a -> [a]
$cnull :: forall a. Closure a -> Bool
null :: forall a. Closure a -> Bool
$clength :: forall a. Closure a -> Int
length :: forall a. Closure a -> Int
$celem :: forall a. Eq a => a -> Closure a -> Bool
elem :: forall a. Eq a => a -> Closure a -> Bool
$cmaximum :: forall a. Ord a => Closure a -> a
maximum :: forall a. Ord a => Closure a -> a
$cminimum :: forall a. Ord a => Closure a -> a
minimum :: forall a. Ord a => Closure a -> a
$csum :: forall a. Num a => Closure a -> a
sum :: forall a. Num a => Closure a -> a
$cproduct :: forall a. Num a => Closure a -> a
product :: forall a. Num a => Closure a -> a
Foldable, (forall x. Closure a -> Rep (Closure a) x)
-> (forall x. Rep (Closure a) x -> Closure a)
-> Generic (Closure a)
forall x. Rep (Closure a) x -> Closure a
forall x. Closure a -> Rep (Closure a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Closure a) x -> Closure a
forall a x. Closure a -> Rep (Closure a) x
$cfrom :: forall a x. Closure a -> Rep (Closure a) x
from :: forall x. Closure a -> Rep (Closure a) x
$cto :: forall a x. Rep (Closure a) x -> Closure a
to :: forall x. Rep (Closure a) x -> Closure a
Generic)

instance Show a => Show (Closure a) where
  show :: Closure a -> String
show Closure a
cl = String
"Closure { clValue = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show (Closure a -> a
forall a. Closure a -> a
clValue Closure a
cl) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" }"

instance HasRange a => HasRange (Closure a) where
  getRange :: Closure a -> Range
getRange = a -> Range
forall a. HasRange a => a -> Range
getRange (a -> Range) -> (Closure a -> a) -> Closure a -> Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure a -> a
forall a. Closure a -> a
clValue

class LensClosure b a | b -> a where
  lensClosure :: Lens' b (Closure a)

instance LensClosure (Closure a) a where
  lensClosure :: Lens' (Closure a) (Closure a)
lensClosure = (Closure a -> f (Closure a)) -> Closure a -> f (Closure a)
forall a. a -> a
id

instance LensTCEnv (Closure a) where
  lensTCEnv :: Lens' (Closure a) TCEnv
lensTCEnv TCEnv -> f TCEnv
f Closure a
cl = (TCEnv -> f TCEnv
f (TCEnv -> f TCEnv) -> TCEnv -> f TCEnv
forall a b. (a -> b) -> a -> b
$! Closure a -> TCEnv
forall a. Closure a -> TCEnv
clEnv Closure a
cl) f TCEnv -> (TCEnv -> Closure a) -> f (Closure a)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ TCEnv
env -> Closure a
cl { clEnv = env }

{-# SPECIALIZE buildClosure :: a -> TCM (Closure a)  #-}
buildClosure :: (MonadTCEnv m, ReadTCState m) => a -> m (Closure a)
buildClosure :: forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure a
x = do
    TCEnv
env   <- m TCEnv
forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC
    Signature
sig   <- Lens' TCState Signature -> m Signature
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Signature -> f Signature) -> TCState -> f TCState
Lens' TCState Signature
stSignature
    ScopeInfo
scope <- Lens' TCState ScopeInfo -> m ScopeInfo
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (ScopeInfo -> f ScopeInfo) -> TCState -> f TCState
Lens' TCState ScopeInfo
stScope
    Map ModuleName CheckpointId
cps   <- Lens' TCState (Map ModuleName CheckpointId)
-> m (Map ModuleName CheckpointId)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (Map ModuleName CheckpointId -> f (Map ModuleName CheckpointId))
-> TCState -> f TCState
Lens' TCState (Map ModuleName CheckpointId)
stModuleCheckpoints
    Closure a -> m (Closure a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Closure a -> m (Closure a)) -> Closure a -> m (Closure a)
forall a b. (a -> b) -> a -> b
$ Signature
-> TCEnv
-> ScopeInfo
-> Map ModuleName CheckpointId
-> a
-> Closure a
forall a.
Signature
-> TCEnv
-> ScopeInfo
-> Map ModuleName CheckpointId
-> a
-> Closure a
Closure Signature
sig TCEnv
env ScopeInfo
scope Map ModuleName CheckpointId
cps a
x

---------------------------------------------------------------------------
-- ** Constraints
---------------------------------------------------------------------------

type Constraints = [ProblemConstraint]

data ProblemConstraint = PConstr
  { ProblemConstraint -> Set ProblemId
constraintProblems  :: Set ProblemId
  , ProblemConstraint -> Blocker
constraintUnblocker :: Blocker
  , ProblemConstraint -> Closure Constraint
theConstraint       :: Closure Constraint
  }
  deriving (Int -> ProblemConstraint -> ShowS
Constraints -> ShowS
ProblemConstraint -> String
(Int -> ProblemConstraint -> ShowS)
-> (ProblemConstraint -> String)
-> (Constraints -> ShowS)
-> Show ProblemConstraint
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ProblemConstraint -> ShowS
showsPrec :: Int -> ProblemConstraint -> ShowS
$cshow :: ProblemConstraint -> String
show :: ProblemConstraint -> String
$cshowList :: Constraints -> ShowS
showList :: Constraints -> ShowS
Show, (forall x. ProblemConstraint -> Rep ProblemConstraint x)
-> (forall x. Rep ProblemConstraint x -> ProblemConstraint)
-> Generic ProblemConstraint
forall x. Rep ProblemConstraint x -> ProblemConstraint
forall x. ProblemConstraint -> Rep ProblemConstraint x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ProblemConstraint -> Rep ProblemConstraint x
from :: forall x. ProblemConstraint -> Rep ProblemConstraint x
$cto :: forall x. Rep ProblemConstraint x -> ProblemConstraint
to :: forall x. Rep ProblemConstraint x -> ProblemConstraint
Generic)

instance HasRange ProblemConstraint where
  getRange :: ProblemConstraint -> Range
getRange = Closure Constraint -> Range
forall a. HasRange a => a -> Range
getRange (Closure Constraint -> Range)
-> (ProblemConstraint -> Closure Constraint)
-> ProblemConstraint
-> Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Closure Constraint
theConstraint

-- | Why are we performing a modality check?
data WhyCheckModality
  = ConstructorType
  -- ^ Because --without-K is enabled, so the types of data constructors
  -- must be usable at the context's modality.
  | IndexedClause
  -- ^ Because --without-K is enabled, so the result type of clauses
  -- must be usable at the context's modality.
  | IndexedClauseArg Name Name
  -- ^ Because --without-K is enabled, so any argument (second name)
  -- which mentions a dotted argument (first name) must have a type
  -- which is usable at the context's modality.
  | GeneratedClause
  -- ^ Because we double-check the --cubical-compatible clauses. This is
  -- an internal error!
  deriving (Int -> WhyCheckModality -> ShowS
[WhyCheckModality] -> ShowS
WhyCheckModality -> String
(Int -> WhyCheckModality -> ShowS)
-> (WhyCheckModality -> String)
-> ([WhyCheckModality] -> ShowS)
-> Show WhyCheckModality
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> WhyCheckModality -> ShowS
showsPrec :: Int -> WhyCheckModality -> ShowS
$cshow :: WhyCheckModality -> String
show :: WhyCheckModality -> String
$cshowList :: [WhyCheckModality] -> ShowS
showList :: [WhyCheckModality] -> ShowS
Show, (forall x. WhyCheckModality -> Rep WhyCheckModality x)
-> (forall x. Rep WhyCheckModality x -> WhyCheckModality)
-> Generic WhyCheckModality
forall x. Rep WhyCheckModality x -> WhyCheckModality
forall x. WhyCheckModality -> Rep WhyCheckModality x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. WhyCheckModality -> Rep WhyCheckModality x
from :: forall x. WhyCheckModality -> Rep WhyCheckModality x
$cto :: forall x. Rep WhyCheckModality x -> WhyCheckModality
to :: forall x. Rep WhyCheckModality x -> WhyCheckModality
Generic)

data Constraint
  = ValueCmp Comparison CompareAs Term Term
  | ValueCmpOnFace Comparison Term Type Term Term
  | ElimCmp [Polarity] [IsForced] Type Term [Elim] [Elim]
  | SortCmp Comparison Sort Sort
  | LevelCmp Comparison Level Level
--  | ShortCut MetaId Term Type
--    -- ^ A delayed instantiation.  Replaces @ValueCmp@ in 'postponeTypeCheckingProblem'.
  | HasBiggerSort Sort
  | HasPTSRule (Dom Type) (Abs Sort)
  | CheckDataSort QName Sort
    -- ^ Check that the sort 'Sort' of data type 'QName' admits data/record types.
    -- E.g., sorts @IUniv@, @SizeUniv@ etc. do not admit such constructions.
    -- See 'Agda.TypeChecking.Rules.Data.checkDataSort'.
  | CheckMetaInst MetaId
  | CheckType Type
  | UnBlock MetaId
    -- ^ Meta created for a term blocked by a postponed type checking problem or unsolved
    --   constraints. The 'MetaInstantiation' for the meta (when unsolved) is either 'BlockedConst'
    --   or 'PostponedTypeCheckingProblem'.
  | IsEmpty Range Type
    -- ^ The range is the one of the absurd pattern.
  | CheckSizeLtSat Term
    -- ^ Check that the 'Term' is either not a SIZELT or a non-empty SIZELT.
  | FindInstance MetaId (Maybe [Candidate])
    -- ^ the first argument is the instance argument and the second one is the list of candidates
    --   (or Nothing if we haven’t determined the list of candidates yet)
  | ResolveInstanceHead QName
    -- ^ Resolve the head symbol of the type that the given instance targets
  | CheckFunDef A.DefInfo QName [A.Clause] TCErr
    -- ^ Last argument is the error causing us to postpone.
  | UnquoteTactic Term Term Type   -- ^ First argument is computation and the others are hole and goal type
  | CheckLockedVars Term Type (Arg Term) Type     -- ^ @CheckLockedVars t ty lk lk_ty@ with @t : ty@, @lk : lk_ty@ and @t lk@ well-typed.
  | UsableAtModality WhyCheckModality (Maybe Sort) Modality Term
    -- ^ Is the term usable at the given modality?
    -- This check should run if the @Sort@ is @Nothing@ or @isFibrant@.
  deriving (Int -> Constraint -> ShowS
[Constraint] -> ShowS
Constraint -> String
(Int -> Constraint -> ShowS)
-> (Constraint -> String)
-> ([Constraint] -> ShowS)
-> Show Constraint
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Constraint -> ShowS
showsPrec :: Int -> Constraint -> ShowS
$cshow :: Constraint -> String
show :: Constraint -> String
$cshowList :: [Constraint] -> ShowS
showList :: [Constraint] -> ShowS
Show, (forall x. Constraint -> Rep Constraint x)
-> (forall x. Rep Constraint x -> Constraint) -> Generic Constraint
forall x. Rep Constraint x -> Constraint
forall x. Constraint -> Rep Constraint x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Constraint -> Rep Constraint x
from :: forall x. Constraint -> Rep Constraint x
$cto :: forall x. Rep Constraint x -> Constraint
to :: forall x. Rep Constraint x -> Constraint
Generic)

instance HasRange Constraint where
  getRange :: Constraint -> Range
getRange (IsEmpty Range
r Type
t) = Range
r
  getRange Constraint
_ = Range
forall a. Range' a
noRange
{- no Range instances for Term, Type, Elm, Tele, Sort, Level, MetaId
  getRange (ValueCmp cmp a u v) = getRange (a,u,v)
  getRange (ElimCmp pol a v es es') = getRange (a,v,es,es')
  getRange (TelCmp a b cmp tel tel') = getRange (a,b,tel,tel')
  getRange (SortCmp cmp s s') = getRange (s,s')
  getRange (LevelCmp cmp l l') = getRange (l,l')
  getRange (UnBlock x) = getRange x
  getRange (FindInstance x cands) = getRange x
-}

instance Free Constraint where
  freeVars' :: forall a c. IsVarSet a c => Constraint -> FreeM a c
freeVars' Constraint
c =
    case Constraint
c of
      ValueCmp Comparison
_ CompareAs
t Term
u Term
v      -> (CompareAs, (Term, Term)) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => (CompareAs, (Term, Term)) -> FreeM a c
freeVars' (CompareAs
t, (Term
u, Term
v))
      ValueCmpOnFace Comparison
_ Term
p Type
t Term
u Term
v -> (Term, (Type, (Term, Term))) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c.
IsVarSet a c =>
(Term, (Type, (Term, Term))) -> FreeM a c
freeVars' (Term
p, (Type
t, (Term
u, Term
v)))
      ElimCmp [Polarity]
_ [IsForced]
_ Type
t Term
u [Elim]
es [Elim]
es'  -> ((Type, Term), ([Elim], [Elim])) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c.
IsVarSet a c =>
((Type, Term), ([Elim], [Elim])) -> FreeM a c
freeVars' ((Type
t, Term
u), ([Elim]
es, [Elim]
es'))
      SortCmp Comparison
_ Sort
s Sort
s'        -> (Sort, Sort) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => (Sort, Sort) -> FreeM a c
freeVars' (Sort
s, Sort
s')
      LevelCmp Comparison
_ Level
l Level
l'       -> (Level, Level) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => (Level, Level) -> FreeM a c
freeVars' (Level
l, Level
l')
      UnBlock MetaId
_             -> FreeM a c
forall a. Monoid a => a
mempty
      IsEmpty Range
_ Type
t           -> Type -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Type -> FreeM a c
freeVars' Type
t
      CheckSizeLtSat Term
u      -> Term -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Term -> FreeM a c
freeVars' Term
u
      FindInstance MetaId
_ Maybe [Candidate]
cs     -> Maybe [Candidate] -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Maybe [Candidate] -> FreeM a c
freeVars' Maybe [Candidate]
cs
      ResolveInstanceHead QName
q -> FreeM a c
forall a. Monoid a => a
mempty
      CheckFunDef{}         -> FreeM a c
forall a. Monoid a => a
mempty
      HasBiggerSort Sort
s       -> Sort -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Sort -> FreeM a c
freeVars' Sort
s
      HasPTSRule Dom Type
a Abs Sort
s        -> (Dom Type, Abs Sort) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => (Dom Type, Abs Sort) -> FreeM a c
freeVars' (Dom Type
a , Abs Sort
s)
      CheckLockedVars Term
a Type
b Arg Term
c Type
d -> ((Term, Type), (Arg Term, Type)) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c.
IsVarSet a c =>
((Term, Type), (Arg Term, Type)) -> FreeM a c
freeVars' ((Term
a,Type
b),(Arg Term
c,Type
d))
      UnquoteTactic Term
t Term
h Type
g   -> (Term, (Term, Type)) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => (Term, (Term, Type)) -> FreeM a c
freeVars' (Term
t, (Term
h, Type
g))
      CheckDataSort QName
_ Sort
s     -> Sort -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Sort -> FreeM a c
freeVars' Sort
s
      CheckMetaInst MetaId
m       -> FreeM a c
forall a. Monoid a => a
mempty
      CheckType Type
t           -> Type -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Type -> FreeM a c
freeVars' Type
t
      UsableAtModality WhyCheckModality
_ Maybe Sort
ms Modality
mod Term
t -> (Maybe Sort, Term) -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => (Maybe Sort, Term) -> FreeM a c
freeVars' (Maybe Sort
ms, Term
t)

instance TermLike Constraint where
  foldTerm :: forall m. Monoid m => (Term -> m) -> Constraint -> m
foldTerm Term -> m
f = \case
      ValueCmp Comparison
_ CompareAs
t Term
u Term
v       -> (Term -> m) -> (CompareAs, Term, Term) -> m
forall m. Monoid m => (Term -> m) -> (CompareAs, Term, Term) -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f (CompareAs
t, Term
u, Term
v)
      ValueCmpOnFace Comparison
_ Term
p Type
t Term
u Term
v -> (Term -> m) -> (Term, Type, Term, Term) -> m
forall m. Monoid m => (Term -> m) -> (Term, Type, Term, Term) -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f (Term
p, Type
t, Term
u, Term
v)
      ElimCmp [Polarity]
_ [IsForced]
_ Type
t Term
u [Elim]
es [Elim]
es' -> (Term -> m) -> (Type, Term, [Elim], [Elim]) -> m
forall m.
Monoid m =>
(Term -> m) -> (Type, Term, [Elim], [Elim]) -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f (Type
t, Term
u, [Elim]
es, [Elim]
es')
      LevelCmp Comparison
_ Level
l Level
l'        -> (Term -> m) -> (Term, Term) -> m
forall m. Monoid m => (Term -> m) -> (Term, Term) -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f (Level -> Term
Level Level
l, Level -> Term
Level Level
l')  -- Note wrapping as term, to ensure f gets to act on l and l'
      IsEmpty Range
_ Type
t            -> (Term -> m) -> Type -> m
forall m. Monoid m => (Term -> m) -> Type -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Type
t
      CheckSizeLtSat Term
u       -> (Term -> m) -> Term -> m
forall m. Monoid m => (Term -> m) -> Term -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Term
u
      UnquoteTactic Term
t Term
h Type
g    -> (Term -> m) -> (Term, Term, Type) -> m
forall m. Monoid m => (Term -> m) -> (Term, Term, Type) -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f (Term
t, Term
h, Type
g)
      SortCmp Comparison
_ Sort
s1 Sort
s2        -> (Term -> m) -> (Term, Term) -> m
forall m. Monoid m => (Term -> m) -> (Term, Term) -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f (Sort -> Term
Sort Sort
s1, Sort -> Term
Sort Sort
s2)   -- Same as LevelCmp case
      UnBlock MetaId
_              -> m
forall a. Monoid a => a
mempty
      CheckLockedVars Term
a Type
b Arg Term
c Type
d -> (Term -> m) -> (Term, Type, Arg Term, Type) -> m
forall m.
Monoid m =>
(Term -> m) -> (Term, Type, Arg Term, Type) -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f (Term
a, Type
b, Arg Term
c, Type
d)
      FindInstance MetaId
_ Maybe [Candidate]
_       -> m
forall a. Monoid a => a
mempty
      ResolveInstanceHead QName
q  -> m
forall a. Monoid a => a
mempty
      CheckFunDef{}          -> m
forall a. Monoid a => a
mempty
      HasBiggerSort Sort
s        -> (Term -> m) -> Sort -> m
forall m. Monoid m => (Term -> m) -> Sort -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Sort
s
      HasPTSRule Dom Type
a Abs Sort
s         -> (Term -> m) -> (Dom Type, Abs Term) -> m
forall m. Monoid m => (Term -> m) -> (Dom Type, Abs Term) -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f (Dom Type
a, Sort -> Term
Sort (Sort -> Term) -> Abs Sort -> Abs Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Sort
s)
      CheckDataSort QName
_ Sort
s      -> (Term -> m) -> Sort -> m
forall m. Monoid m => (Term -> m) -> Sort -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Sort
s
      CheckMetaInst MetaId
m        -> m
forall a. Monoid a => a
mempty
      CheckType Type
t            -> (Term -> m) -> Type -> m
forall m. Monoid m => (Term -> m) -> Type -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Type
t
      UsableAtModality WhyCheckModality
_ Maybe Sort
ms Modality
m Term
t   -> (Term -> m) -> (Maybe Term, Term) -> m
forall m. Monoid m => (Term -> m) -> (Maybe Term, Term) -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f (Sort -> Term
Sort (Sort -> Term) -> Maybe Sort -> Maybe Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Sort
ms, Term
t)

  traverseTermM :: forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> Constraint -> m Constraint
traverseTermM Term -> m Term
f Constraint
c = m Constraint
forall a. HasCallStack => a
__IMPOSSIBLE__ -- Not yet implemented

instance AllMetas Constraint

data Comparison = CmpEq | CmpLeq
  deriving (Comparison -> Comparison -> Bool
(Comparison -> Comparison -> Bool)
-> (Comparison -> Comparison -> Bool) -> Eq Comparison
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Comparison -> Comparison -> Bool
== :: Comparison -> Comparison -> Bool
$c/= :: Comparison -> Comparison -> Bool
/= :: Comparison -> Comparison -> Bool
Eq, Int -> Comparison -> ShowS
[Comparison] -> ShowS
Comparison -> String
(Int -> Comparison -> ShowS)
-> (Comparison -> String)
-> ([Comparison] -> ShowS)
-> Show Comparison
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Comparison -> ShowS
showsPrec :: Int -> Comparison -> ShowS
$cshow :: Comparison -> String
show :: Comparison -> String
$cshowList :: [Comparison] -> ShowS
showList :: [Comparison] -> ShowS
Show, (forall x. Comparison -> Rep Comparison x)
-> (forall x. Rep Comparison x -> Comparison) -> Generic Comparison
forall x. Rep Comparison x -> Comparison
forall x. Comparison -> Rep Comparison x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Comparison -> Rep Comparison x
from :: forall x. Comparison -> Rep Comparison x
$cto :: forall x. Rep Comparison x -> Comparison
to :: forall x. Rep Comparison x -> Comparison
Generic)

instance Pretty Comparison where
  pretty :: Comparison -> Doc
pretty Comparison
CmpEq  = Doc
"="
  pretty Comparison
CmpLeq = Doc
"=<"

-- | An extension of 'Comparison' to @>=@.
data CompareDirection = DirEq | DirLeq | DirGeq
  deriving (CompareDirection -> CompareDirection -> Bool
(CompareDirection -> CompareDirection -> Bool)
-> (CompareDirection -> CompareDirection -> Bool)
-> Eq CompareDirection
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CompareDirection -> CompareDirection -> Bool
== :: CompareDirection -> CompareDirection -> Bool
$c/= :: CompareDirection -> CompareDirection -> Bool
/= :: CompareDirection -> CompareDirection -> Bool
Eq, Int -> CompareDirection -> ShowS
[CompareDirection] -> ShowS
CompareDirection -> String
(Int -> CompareDirection -> ShowS)
-> (CompareDirection -> String)
-> ([CompareDirection] -> ShowS)
-> Show CompareDirection
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CompareDirection -> ShowS
showsPrec :: Int -> CompareDirection -> ShowS
$cshow :: CompareDirection -> String
show :: CompareDirection -> String
$cshowList :: [CompareDirection] -> ShowS
showList :: [CompareDirection] -> ShowS
Show)

instance Pretty CompareDirection where
  pretty :: CompareDirection -> Doc
pretty = String -> Doc
forall a. String -> Doc a
text (String -> Doc)
-> (CompareDirection -> String) -> CompareDirection -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
    CompareDirection
DirEq  -> String
"="
    CompareDirection
DirLeq -> String
"=<"
    CompareDirection
DirGeq -> String
">="

-- | Embed 'Comparison' into 'CompareDirection'.
fromCmp :: Comparison -> CompareDirection
fromCmp :: Comparison -> CompareDirection
fromCmp Comparison
CmpEq  = CompareDirection
DirEq
fromCmp Comparison
CmpLeq = CompareDirection
DirLeq

-- | Flip the direction of comparison.
flipCmp :: CompareDirection -> CompareDirection
flipCmp :: CompareDirection -> CompareDirection
flipCmp CompareDirection
DirEq  = CompareDirection
DirEq
flipCmp CompareDirection
DirLeq = CompareDirection
DirGeq
flipCmp CompareDirection
DirGeq = CompareDirection
DirLeq

-- | Turn a 'Comparison' function into a 'CompareDirection' function.
--
--   Property: @dirToCmp f (fromCmp cmp) = f cmp@
dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c
dirToCmp :: forall a c.
(Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c
dirToCmp Comparison -> a -> a -> c
cont CompareDirection
DirEq  = Comparison -> a -> a -> c
cont Comparison
CmpEq
dirToCmp Comparison -> a -> a -> c
cont CompareDirection
DirLeq = Comparison -> a -> a -> c
cont Comparison
CmpLeq
dirToCmp Comparison -> a -> a -> c
cont CompareDirection
DirGeq = (a -> a -> c) -> a -> a -> c
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((a -> a -> c) -> a -> a -> c) -> (a -> a -> c) -> a -> a -> c
forall a b. (a -> b) -> a -> b
$ Comparison -> a -> a -> c
cont Comparison
CmpLeq

-- | We can either compare two terms at a given type, or compare two
--   types without knowing (or caring about) their sorts.
data CompareAs
  = AsTermsOf Type -- ^ @Type@ should not be @Size@.
                   --   But currently, we do not rely on this invariant.
  | AsSizes        -- ^ Replaces @AsTermsOf Size@.
  | AsTypes
  deriving (Int -> CompareAs -> ShowS
[CompareAs] -> ShowS
CompareAs -> String
(Int -> CompareAs -> ShowS)
-> (CompareAs -> String)
-> ([CompareAs] -> ShowS)
-> Show CompareAs
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CompareAs -> ShowS
showsPrec :: Int -> CompareAs -> ShowS
$cshow :: CompareAs -> String
show :: CompareAs -> String
$cshowList :: [CompareAs] -> ShowS
showList :: [CompareAs] -> ShowS
Show, (forall x. CompareAs -> Rep CompareAs x)
-> (forall x. Rep CompareAs x -> CompareAs) -> Generic CompareAs
forall x. Rep CompareAs x -> CompareAs
forall x. CompareAs -> Rep CompareAs x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CompareAs -> Rep CompareAs x
from :: forall x. CompareAs -> Rep CompareAs x
$cto :: forall x. Rep CompareAs x -> CompareAs
to :: forall x. Rep CompareAs x -> CompareAs
Generic)

instance Free CompareAs where
  freeVars' :: forall a c. IsVarSet a c => CompareAs -> FreeM a c
freeVars' (AsTermsOf Type
a) = Type -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
forall a c. IsVarSet a c => Type -> FreeM a c
freeVars' Type
a
  freeVars' CompareAs
AsSizes       = FreeM a c
forall a. Monoid a => a
mempty
  freeVars' CompareAs
AsTypes       = FreeM a c
forall a. Monoid a => a
mempty

instance TermLike CompareAs where
  foldTerm :: forall m. Monoid m => (Term -> m) -> CompareAs -> m
foldTerm Term -> m
f (AsTermsOf Type
a) = (Term -> m) -> Type -> m
forall m. Monoid m => (Term -> m) -> Type -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Type
a
  foldTerm Term -> m
f CompareAs
AsSizes       = m
forall a. Monoid a => a
mempty
  foldTerm Term -> m
f CompareAs
AsTypes       = m
forall a. Monoid a => a
mempty

  traverseTermM :: forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> CompareAs -> m CompareAs
traverseTermM Term -> m Term
f = \case
    AsTermsOf Type
a -> Type -> CompareAs
AsTermsOf (Type -> CompareAs) -> m Type -> m CompareAs
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> m Term) -> Type -> m Type
forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
forall (m :: * -> *). Monad m => (Term -> m Term) -> Type -> m Type
traverseTermM Term -> m Term
f Type
a
    CompareAs
AsSizes     -> CompareAs -> m CompareAs
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return CompareAs
AsSizes
    CompareAs
AsTypes     -> CompareAs -> m CompareAs
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return CompareAs
AsTypes

instance AllMetas CompareAs

instance Pretty CompareAs where
  pretty :: CompareAs -> Doc
pretty (AsTermsOf Type
a) = Doc
":" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Type -> Doc
forall a. Pretty a => a -> Doc
pretty Type
a
  pretty CompareAs
AsSizes       = Doc
":" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> String -> Doc
forall a. String -> Doc a
text String
"Size"
  pretty CompareAs
AsTypes       = Doc
forall a. Null a => a
empty

---------------------------------------------------------------------------
-- * Open things
---------------------------------------------------------------------------

-- | A thing tagged with the context it came from. Also keeps the substitution from previous
--   checkpoints. This lets us handle the case when an open thing was created in a context that we
--   have since exited. Remember which module it's from to make sure we don't get confused by
--   checkpoints from other files.
data Open a = OpenThing { forall a. Open a -> CheckpointId
openThingCheckpoint    :: CheckpointId
                        , forall a. Open a -> Map CheckpointId Substitution
openThingCheckpointMap :: Map CheckpointId Substitution
                        , forall a. Open a -> ModuleNameHash
openThingModule        :: ModuleNameHash
                        , forall a. Open a -> a
openThing              :: a }
    deriving (Int -> Open a -> ShowS
[Open a] -> ShowS
Open a -> String
(Int -> Open a -> ShowS)
-> (Open a -> String) -> ([Open a] -> ShowS) -> Show (Open a)
forall a. Show a => Int -> Open a -> ShowS
forall a. Show a => [Open a] -> ShowS
forall a. Show a => Open a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Open a -> ShowS
showsPrec :: Int -> Open a -> ShowS
$cshow :: forall a. Show a => Open a -> String
show :: Open a -> String
$cshowList :: forall a. Show a => [Open a] -> ShowS
showList :: [Open a] -> ShowS
Show, (forall a b. (a -> b) -> Open a -> Open b)
-> (forall a b. a -> Open b -> Open a) -> Functor Open
forall a b. a -> Open b -> Open a
forall a b. (a -> b) -> Open a -> Open b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Open a -> Open b
fmap :: forall a b. (a -> b) -> Open a -> Open b
$c<$ :: forall a b. a -> Open b -> Open a
<$ :: forall a b. a -> Open b -> Open a
Functor, (forall m. Monoid m => Open m -> m)
-> (forall m a. Monoid m => (a -> m) -> Open a -> m)
-> (forall m a. Monoid m => (a -> m) -> Open a -> m)
-> (forall a b. (a -> b -> b) -> b -> Open a -> b)
-> (forall a b. (a -> b -> b) -> b -> Open a -> b)
-> (forall b a. (b -> a -> b) -> b -> Open a -> b)
-> (forall b a. (b -> a -> b) -> b -> Open a -> b)
-> (forall a. (a -> a -> a) -> Open a -> a)
-> (forall a. (a -> a -> a) -> Open a -> a)
-> (forall a. Open a -> [a])
-> (forall a. Open a -> Bool)
-> (forall a. Open a -> Int)
-> (forall a. Eq a => a -> Open a -> Bool)
-> (forall a. Ord a => Open a -> a)
-> (forall a. Ord a => Open a -> a)
-> (forall a. Num a => Open a -> a)
-> (forall a. Num a => Open a -> a)
-> Foldable Open
forall a. Eq a => a -> Open a -> Bool
forall a. Num a => Open a -> a
forall a. Ord a => Open a -> a
forall m. Monoid m => Open m -> m
forall a. Open a -> Bool
forall a. Open a -> Int
forall a. Open a -> [a]
forall a. (a -> a -> a) -> Open a -> a
forall m a. Monoid m => (a -> m) -> Open a -> m
forall b a. (b -> a -> b) -> b -> Open a -> b
forall a b. (a -> b -> b) -> b -> Open a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Open m -> m
fold :: forall m. Monoid m => Open m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Open a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Open a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Open a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Open a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Open a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Open a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Open a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Open a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Open a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Open a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Open a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Open a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Open a -> a
foldr1 :: forall a. (a -> a -> a) -> Open a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Open a -> a
foldl1 :: forall a. (a -> a -> a) -> Open a -> a
$ctoList :: forall a. Open a -> [a]
toList :: forall a. Open a -> [a]
$cnull :: forall a. Open a -> Bool
null :: forall a. Open a -> Bool
$clength :: forall a. Open a -> Int
length :: forall a. Open a -> Int
$celem :: forall a. Eq a => a -> Open a -> Bool
elem :: forall a. Eq a => a -> Open a -> Bool
$cmaximum :: forall a. Ord a => Open a -> a
maximum :: forall a. Ord a => Open a -> a
$cminimum :: forall a. Ord a => Open a -> a
minimum :: forall a. Ord a => Open a -> a
$csum :: forall a. Num a => Open a -> a
sum :: forall a. Num a => Open a -> a
$cproduct :: forall a. Num a => Open a -> a
product :: forall a. Num a => Open a -> a
Foldable, Functor Open
Foldable Open
(Functor Open, Foldable Open) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Open a -> f (Open b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Open (f a) -> f (Open a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Open a -> m (Open b))
-> (forall (m :: * -> *) a. Monad m => Open (m a) -> m (Open a))
-> Traversable Open
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Open (m a) -> m (Open a)
forall (f :: * -> *) a. Applicative f => Open (f a) -> f (Open a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Open a -> m (Open b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Open a -> f (Open b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Open a -> f (Open b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Open a -> f (Open b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Open (f a) -> f (Open a)
sequenceA :: forall (f :: * -> *) a. Applicative f => Open (f a) -> f (Open a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Open a -> m (Open b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Open a -> m (Open b)
$csequence :: forall (m :: * -> *) a. Monad m => Open (m a) -> m (Open a)
sequence :: forall (m :: * -> *) a. Monad m => Open (m a) -> m (Open a)
Traversable, (forall x. Open a -> Rep (Open a) x)
-> (forall x. Rep (Open a) x -> Open a) -> Generic (Open a)
forall x. Rep (Open a) x -> Open a
forall x. Open a -> Rep (Open a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Open a) x -> Open a
forall a x. Open a -> Rep (Open a) x
$cfrom :: forall a x. Open a -> Rep (Open a) x
from :: forall x. Open a -> Rep (Open a) x
$cto :: forall a x. Rep (Open a) x -> Open a
to :: forall x. Rep (Open a) x -> Open a
Generic)

instance Decoration Open where
  traverseF :: forall (m :: * -> *) a b.
Functor m =>
(a -> m b) -> Open a -> m (Open b)
traverseF a -> m b
f (OpenThing CheckpointId
cp Map CheckpointId Substitution
env ModuleNameHash
m a
x) = CheckpointId
-> Map CheckpointId Substitution -> ModuleNameHash -> b -> Open b
forall a.
CheckpointId
-> Map CheckpointId Substitution -> ModuleNameHash -> a -> Open a
OpenThing CheckpointId
cp Map CheckpointId Substitution
env ModuleNameHash
m (b -> Open b) -> m b -> m (Open b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
f a
x

instance Pretty a => Pretty (Open a) where
  prettyPrec :: Int -> Open a -> Doc
prettyPrec Int
p (OpenThing CheckpointId
cp Map CheckpointId Substitution
env ModuleNameHash
_ a
x) = Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
    Doc
"OpenThing" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> CheckpointId -> Doc
forall a. Pretty a => a -> Doc
pretty CheckpointId
cp Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> [(CheckpointId, Substitution)] -> Doc
forall a. Pretty a => a -> Doc
pretty (Map CheckpointId Substitution -> [(CheckpointId, Substitution)]
forall k a. Map k a -> [(k, a)]
Map.toList Map CheckpointId Substitution
env) Doc -> Doc -> Doc
<?> Int -> a -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 a
x

---------------------------------------------------------------------------
-- * Judgements
--
-- Used exclusively for typing of meta variables.
---------------------------------------------------------------------------

-- | Parametrized since it is used without MetaId when creating a new meta.
data Judgement a
  = HasType
    { forall a. Judgement a -> a
jMetaId     :: a
    , forall a. Judgement a -> Comparison
jComparison :: Comparison -- ^ are we checking (@CmpLeq@) or inferring (@CmpEq@) the type?
    , forall a. Judgement a -> Type
jMetaType   :: Type
    }
  | IsSort
    { jMetaId   :: a
    , jMetaType :: Type -- Andreas, 2011-04-26: type needed for higher-order sort metas
    }
  deriving (Int -> Judgement a -> ShowS
[Judgement a] -> ShowS
Judgement a -> String
(Int -> Judgement a -> ShowS)
-> (Judgement a -> String)
-> ([Judgement a] -> ShowS)
-> Show (Judgement a)
forall a. Show a => Int -> Judgement a -> ShowS
forall a. Show a => [Judgement a] -> ShowS
forall a. Show a => Judgement a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Judgement a -> ShowS
showsPrec :: Int -> Judgement a -> ShowS
$cshow :: forall a. Show a => Judgement a -> String
show :: Judgement a -> String
$cshowList :: forall a. Show a => [Judgement a] -> ShowS
showList :: [Judgement a] -> ShowS
Show, (forall x. Judgement a -> Rep (Judgement a) x)
-> (forall x. Rep (Judgement a) x -> Judgement a)
-> Generic (Judgement a)
forall x. Rep (Judgement a) x -> Judgement a
forall x. Judgement a -> Rep (Judgement a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Judgement a) x -> Judgement a
forall a x. Judgement a -> Rep (Judgement a) x
$cfrom :: forall a x. Judgement a -> Rep (Judgement a) x
from :: forall x. Judgement a -> Rep (Judgement a) x
$cto :: forall a x. Rep (Judgement a) x -> Judgement a
to :: forall x. Rep (Judgement a) x -> Judgement a
Generic)

instance Pretty a => Pretty (Judgement a) where
    pretty :: Judgement a -> Doc
pretty (HasType a
a Comparison
cmp Type
t) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a, Doc
":"    , Type -> Doc
forall a. Pretty a => a -> Doc
pretty Type
t ]
    pretty (IsSort  a
a Type
t)     = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a, Doc
":sort", Type -> Doc
forall a. Pretty a => a -> Doc
pretty Type
t ]

-----------------------------------------------------------------------------
-- ** Generalizable variables
-----------------------------------------------------------------------------

data DoGeneralize
  = YesGeneralizeVar  -- ^ Generalize because it is a generalizable variable.
  | YesGeneralizeMeta -- ^ Generalize because it is a metavariable and
                      --   we're currently checking the type of a generalizable variable
                      --   (this should get the default modality).
  | NoGeneralize      -- ^ Don't generalize.
  deriving (DoGeneralize -> DoGeneralize -> Bool
(DoGeneralize -> DoGeneralize -> Bool)
-> (DoGeneralize -> DoGeneralize -> Bool) -> Eq DoGeneralize
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DoGeneralize -> DoGeneralize -> Bool
== :: DoGeneralize -> DoGeneralize -> Bool
$c/= :: DoGeneralize -> DoGeneralize -> Bool
/= :: DoGeneralize -> DoGeneralize -> Bool
Eq, Eq DoGeneralize
Eq DoGeneralize =>
(DoGeneralize -> DoGeneralize -> Ordering)
-> (DoGeneralize -> DoGeneralize -> Bool)
-> (DoGeneralize -> DoGeneralize -> Bool)
-> (DoGeneralize -> DoGeneralize -> Bool)
-> (DoGeneralize -> DoGeneralize -> Bool)
-> (DoGeneralize -> DoGeneralize -> DoGeneralize)
-> (DoGeneralize -> DoGeneralize -> DoGeneralize)
-> Ord DoGeneralize
DoGeneralize -> DoGeneralize -> Bool
DoGeneralize -> DoGeneralize -> Ordering
DoGeneralize -> DoGeneralize -> DoGeneralize
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: DoGeneralize -> DoGeneralize -> Ordering
compare :: DoGeneralize -> DoGeneralize -> Ordering
$c< :: DoGeneralize -> DoGeneralize -> Bool
< :: DoGeneralize -> DoGeneralize -> Bool
$c<= :: DoGeneralize -> DoGeneralize -> Bool
<= :: DoGeneralize -> DoGeneralize -> Bool
$c> :: DoGeneralize -> DoGeneralize -> Bool
> :: DoGeneralize -> DoGeneralize -> Bool
$c>= :: DoGeneralize -> DoGeneralize -> Bool
>= :: DoGeneralize -> DoGeneralize -> Bool
$cmax :: DoGeneralize -> DoGeneralize -> DoGeneralize
max :: DoGeneralize -> DoGeneralize -> DoGeneralize
$cmin :: DoGeneralize -> DoGeneralize -> DoGeneralize
min :: DoGeneralize -> DoGeneralize -> DoGeneralize
Ord, Int -> DoGeneralize -> ShowS
[DoGeneralize] -> ShowS
DoGeneralize -> String
(Int -> DoGeneralize -> ShowS)
-> (DoGeneralize -> String)
-> ([DoGeneralize] -> ShowS)
-> Show DoGeneralize
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DoGeneralize -> ShowS
showsPrec :: Int -> DoGeneralize -> ShowS
$cshow :: DoGeneralize -> String
show :: DoGeneralize -> String
$cshowList :: [DoGeneralize] -> ShowS
showList :: [DoGeneralize] -> ShowS
Show, (forall x. DoGeneralize -> Rep DoGeneralize x)
-> (forall x. Rep DoGeneralize x -> DoGeneralize)
-> Generic DoGeneralize
forall x. Rep DoGeneralize x -> DoGeneralize
forall x. DoGeneralize -> Rep DoGeneralize x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DoGeneralize -> Rep DoGeneralize x
from :: forall x. DoGeneralize -> Rep DoGeneralize x
$cto :: forall x. Rep DoGeneralize x -> DoGeneralize
to :: forall x. Rep DoGeneralize x -> DoGeneralize
Generic)

-- | The value of a generalizable variable. This is created to be a
--   generalizable meta before checking the type to be generalized.
data GeneralizedValue = GeneralizedValue
  { GeneralizedValue -> CheckpointId
genvalCheckpoint :: CheckpointId
  , GeneralizedValue -> Term
genvalTerm       :: Term
  , GeneralizedValue -> Type
genvalType       :: Type
  } deriving (Int -> GeneralizedValue -> ShowS
[GeneralizedValue] -> ShowS
GeneralizedValue -> String
(Int -> GeneralizedValue -> ShowS)
-> (GeneralizedValue -> String)
-> ([GeneralizedValue] -> ShowS)
-> Show GeneralizedValue
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GeneralizedValue -> ShowS
showsPrec :: Int -> GeneralizedValue -> ShowS
$cshow :: GeneralizedValue -> String
show :: GeneralizedValue -> String
$cshowList :: [GeneralizedValue] -> ShowS
showList :: [GeneralizedValue] -> ShowS
Show, (forall x. GeneralizedValue -> Rep GeneralizedValue x)
-> (forall x. Rep GeneralizedValue x -> GeneralizedValue)
-> Generic GeneralizedValue
forall x. Rep GeneralizedValue x -> GeneralizedValue
forall x. GeneralizedValue -> Rep GeneralizedValue x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. GeneralizedValue -> Rep GeneralizedValue x
from :: forall x. GeneralizedValue -> Rep GeneralizedValue x
$cto :: forall x. Rep GeneralizedValue x -> GeneralizedValue
to :: forall x. Rep GeneralizedValue x -> GeneralizedValue
Generic)

---------------------------------------------------------------------------
-- ** Meta variables
---------------------------------------------------------------------------

-- | Information about local meta-variables.

data MetaVariable =
        MetaVar { MetaVariable -> MetaInfo
mvInfo          :: MetaInfo
                , MetaVariable -> MetaPriority
mvPriority      :: MetaPriority -- ^ some metavariables are more eager to be instantiated
                , MetaVariable -> Permutation
mvPermutation   :: Permutation
                  -- ^ a metavariable doesn't have to depend on all variables
                  --   in the context, this "permutation" will throw away the
                  --   ones it does not depend on
                , MetaVariable -> Judgement MetaId
mvJudgement     :: Judgement MetaId
                , MetaVariable -> MetaInstantiation
mvInstantiation :: MetaInstantiation
                , MetaVariable -> Set Listener
mvListeners     :: Set Listener -- ^ meta variables scheduled for eta-expansion but blocked by this one
                , MetaVariable -> Frozen
mvFrozen        :: Frozen -- ^ are we past the point where we can instantiate this meta variable?
                , MetaVariable -> Maybe MetaId
mvTwin          :: Maybe MetaId
                  -- ^ @Just m@ means that this meta-variable will be
                  -- equated to @m@ when the latter is unblocked. See
                  -- 'Agda.TypeChecking.MetaVars.blockTermOnProblem'.
                }
  deriving (forall x. MetaVariable -> Rep MetaVariable x)
-> (forall x. Rep MetaVariable x -> MetaVariable)
-> Generic MetaVariable
forall x. Rep MetaVariable x -> MetaVariable
forall x. MetaVariable -> Rep MetaVariable x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MetaVariable -> Rep MetaVariable x
from :: forall x. MetaVariable -> Rep MetaVariable x
$cto :: forall x. Rep MetaVariable x -> MetaVariable
to :: forall x. Rep MetaVariable x -> MetaVariable
Generic

data Listener = EtaExpand MetaId
              | CheckConstraint Nat ProblemConstraint
  deriving (forall x. Listener -> Rep Listener x)
-> (forall x. Rep Listener x -> Listener) -> Generic Listener
forall x. Rep Listener x -> Listener
forall x. Listener -> Rep Listener x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Listener -> Rep Listener x
from :: forall x. Listener -> Rep Listener x
$cto :: forall x. Rep Listener x -> Listener
to :: forall x. Rep Listener x -> Listener
Generic

instance Eq Listener where
  EtaExpand       MetaId
x   == :: Listener -> Listener -> Bool
== EtaExpand       MetaId
y   = MetaId
x MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
y
  CheckConstraint Int
x ProblemConstraint
_ == CheckConstraint Int
y ProblemConstraint
_ = Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
y
  Listener
_ == Listener
_ = Bool
False

instance Ord Listener where
  EtaExpand       MetaId
x   compare :: Listener -> Listener -> Ordering
`compare` EtaExpand       MetaId
y   = MetaId
x MetaId -> MetaId -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` MetaId
y
  CheckConstraint Int
x ProblemConstraint
_ `compare` CheckConstraint Int
y ProblemConstraint
_ = Int
x Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Int
y
  EtaExpand{} `compare` CheckConstraint{} = Ordering
LT
  CheckConstraint{} `compare` EtaExpand{} = Ordering
GT

-- | Frozen meta variable cannot be instantiated by unification.
--   This serves to prevent the completion of a definition by its use
--   outside of the current block.
--   (See issues 118, 288, 399).
data Frozen
  = Frozen        -- ^ Do not instantiate.
  | Instantiable
    deriving (Frozen -> Frozen -> Bool
(Frozen -> Frozen -> Bool)
-> (Frozen -> Frozen -> Bool) -> Eq Frozen
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Frozen -> Frozen -> Bool
== :: Frozen -> Frozen -> Bool
$c/= :: Frozen -> Frozen -> Bool
/= :: Frozen -> Frozen -> Bool
Eq, Int -> Frozen -> ShowS
[Frozen] -> ShowS
Frozen -> String
(Int -> Frozen -> ShowS)
-> (Frozen -> String) -> ([Frozen] -> ShowS) -> Show Frozen
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Frozen -> ShowS
showsPrec :: Int -> Frozen -> ShowS
$cshow :: Frozen -> String
show :: Frozen -> String
$cshowList :: [Frozen] -> ShowS
showList :: [Frozen] -> ShowS
Show, (forall x. Frozen -> Rep Frozen x)
-> (forall x. Rep Frozen x -> Frozen) -> Generic Frozen
forall x. Rep Frozen x -> Frozen
forall x. Frozen -> Rep Frozen x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Frozen -> Rep Frozen x
from :: forall x. Frozen -> Rep Frozen x
$cto :: forall x. Rep Frozen x -> Frozen
to :: forall x. Rep Frozen x -> Frozen
Generic)

-- | Solution status of meta.
data MetaInstantiation
  = InstV Instantiation -- ^ Solved by 'Instantiation'.
  | OpenMeta MetaKind   -- ^ Unsolved (open to solutions).
  | BlockedConst Term   -- ^ Solved, but solution blocked by unsolved constraints.
  | PostponedTypeCheckingProblem (Closure TypeCheckingProblem)
      -- ^ Meta stands for value of the expression that is still to be type checked.
  deriving (forall x. MetaInstantiation -> Rep MetaInstantiation x)
-> (forall x. Rep MetaInstantiation x -> MetaInstantiation)
-> Generic MetaInstantiation
forall x. Rep MetaInstantiation x -> MetaInstantiation
forall x. MetaInstantiation -> Rep MetaInstantiation x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MetaInstantiation -> Rep MetaInstantiation x
from :: forall x. MetaInstantiation -> Rep MetaInstantiation x
$cto :: forall x. Rep MetaInstantiation x -> MetaInstantiation
to :: forall x. Rep MetaInstantiation x -> MetaInstantiation
Generic

-- | Meta-variable instantiations.

data Instantiation = Instantiation
  { Instantiation -> [Arg String]
instTel :: [Arg String]
    -- ^ The solution is abstracted over these free variables.
  , Instantiation -> Term
instBody :: Term
    -- ^ The body of the solution.
  }
  deriving (Int -> Instantiation -> ShowS
[Instantiation] -> ShowS
Instantiation -> String
(Int -> Instantiation -> ShowS)
-> (Instantiation -> String)
-> ([Instantiation] -> ShowS)
-> Show Instantiation
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Instantiation -> ShowS
showsPrec :: Int -> Instantiation -> ShowS
$cshow :: Instantiation -> String
show :: Instantiation -> String
$cshowList :: [Instantiation] -> ShowS
showList :: [Instantiation] -> ShowS
Show, (forall x. Instantiation -> Rep Instantiation x)
-> (forall x. Rep Instantiation x -> Instantiation)
-> Generic Instantiation
forall x. Rep Instantiation x -> Instantiation
forall x. Instantiation -> Rep Instantiation x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Instantiation -> Rep Instantiation x
from :: forall x. Instantiation -> Rep Instantiation x
$cto :: forall x. Rep Instantiation x -> Instantiation
to :: forall x. Rep Instantiation x -> Instantiation
Generic)

-- | Information about remote meta-variables.
--
-- Remote meta-variables are meta-variables originating in other
-- modules. These meta-variables are always instantiated. We do not
-- retain all the information about a local meta-variable when
-- creating an interface:
--
-- * The 'mvPriority' field is not needed, because the meta-variable
--   cannot be instantiated.
-- * The 'mvFrozen' field is not needed, because there is no point in
--   freezing instantiated meta-variables.
-- * The 'mvListeners' field is not needed, because no meta-variable
--   should be listening to this one.
-- * The 'mvTwin' field is not needed, because the meta-variable has
--   already been instantiated.
-- * The 'mvPermutation' is currently removed, but could be retained
--   if it turns out to be useful for something.
-- * The only part of the 'mvInfo' field that is kept is the
--   'miModality' field. The 'miMetaOccursCheck' and 'miGeneralizable'
--   fields are omitted, because the meta-variable has already been
--   instantiated. The 'Range' that is part of the 'miClosRange' field
--   and the 'miNameSuggestion' field are omitted because instantiated
--   meta-variables are typically not presented to users. Finally the
--   'Closure' part of the 'miClosRange' field is omitted because it
--   can be large (at least if we ignore potential sharing).

data RemoteMetaVariable = RemoteMetaVariable
  { RemoteMetaVariable -> Instantiation
rmvInstantiation :: Instantiation
  , RemoteMetaVariable -> Modality
rmvModality      :: Modality
  , RemoteMetaVariable -> Judgement MetaId
rmvJudgement     :: Judgement MetaId
  }
  deriving (Int -> RemoteMetaVariable -> ShowS
[RemoteMetaVariable] -> ShowS
RemoteMetaVariable -> String
(Int -> RemoteMetaVariable -> ShowS)
-> (RemoteMetaVariable -> String)
-> ([RemoteMetaVariable] -> ShowS)
-> Show RemoteMetaVariable
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RemoteMetaVariable -> ShowS
showsPrec :: Int -> RemoteMetaVariable -> ShowS
$cshow :: RemoteMetaVariable -> String
show :: RemoteMetaVariable -> String
$cshowList :: [RemoteMetaVariable] -> ShowS
showList :: [RemoteMetaVariable] -> ShowS
Show, (forall x. RemoteMetaVariable -> Rep RemoteMetaVariable x)
-> (forall x. Rep RemoteMetaVariable x -> RemoteMetaVariable)
-> Generic RemoteMetaVariable
forall x. Rep RemoteMetaVariable x -> RemoteMetaVariable
forall x. RemoteMetaVariable -> Rep RemoteMetaVariable x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. RemoteMetaVariable -> Rep RemoteMetaVariable x
from :: forall x. RemoteMetaVariable -> Rep RemoteMetaVariable x
$cto :: forall x. Rep RemoteMetaVariable x -> RemoteMetaVariable
to :: forall x. Rep RemoteMetaVariable x -> RemoteMetaVariable
Generic)

-- | Solving a 'CheckArgs' constraint may or may not check the target type. If
--   it did, it returns a handle to any unsolved constraints.
data CheckedTarget = CheckedTarget (Maybe ProblemId)
                   | NotCheckedTarget

data PrincipalArgTypeMetas = PrincipalArgTypeMetas
  { PrincipalArgTypeMetas -> Args
patmMetas     :: Args -- ^ metas created for hidden and instance arguments
                          --   in the principal argument's type
  , PrincipalArgTypeMetas -> Type
patmRemainder :: Type -- ^ principal argument's type, stripped of hidden and
                          --   instance arguments
  }
  deriving (forall x. PrincipalArgTypeMetas -> Rep PrincipalArgTypeMetas x)
-> (forall x. Rep PrincipalArgTypeMetas x -> PrincipalArgTypeMetas)
-> Generic PrincipalArgTypeMetas
forall x. Rep PrincipalArgTypeMetas x -> PrincipalArgTypeMetas
forall x. PrincipalArgTypeMetas -> Rep PrincipalArgTypeMetas x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PrincipalArgTypeMetas -> Rep PrincipalArgTypeMetas x
from :: forall x. PrincipalArgTypeMetas -> Rep PrincipalArgTypeMetas x
$cto :: forall x. Rep PrincipalArgTypeMetas x -> PrincipalArgTypeMetas
to :: forall x. Rep PrincipalArgTypeMetas x -> PrincipalArgTypeMetas
Generic

data TypeCheckingProblem
  = CheckExpr Comparison A.Expr Type
  | CheckArgs Comparison ExpandHidden Range [NamedArg A.Expr] Type Type (ArgsCheckState CheckedTarget -> TCM Term)
  | CheckProjAppToKnownPrincipalArg Comparison A.Expr ProjOrigin (List1 QName) A.Args Type Int Term Type PrincipalArgTypeMetas
  | CheckLambda Comparison (Arg (List1 (WithHiding Name), Maybe Type)) A.Expr Type
    -- ^ @(λ (xs : t₀) → e) : t@
    --   This is not an instance of 'CheckExpr' as the domain type
    --   has already been checked.
    --   For example, when checking
    --     @(λ (x y : Fin _) → e) : (x : Fin n) → ?@
    --   we want to postpone @(λ (y : Fin n) → e) : ?@ where @Fin n@
    --   is a 'Type' rather than an 'A.Expr'.
  | DoQuoteTerm Comparison Term Type -- ^ Quote the given term and check type against `Term`
  deriving (forall x. TypeCheckingProblem -> Rep TypeCheckingProblem x)
-> (forall x. Rep TypeCheckingProblem x -> TypeCheckingProblem)
-> Generic TypeCheckingProblem
forall x. Rep TypeCheckingProblem x -> TypeCheckingProblem
forall x. TypeCheckingProblem -> Rep TypeCheckingProblem x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. TypeCheckingProblem -> Rep TypeCheckingProblem x
from :: forall x. TypeCheckingProblem -> Rep TypeCheckingProblem x
$cto :: forall x. Rep TypeCheckingProblem x -> TypeCheckingProblem
to :: forall x. Rep TypeCheckingProblem x -> TypeCheckingProblem
Generic

instance Pretty MetaInstantiation where
  pretty :: MetaInstantiation -> Doc
pretty = \case
    OpenMeta MetaKind
UnificationMeta                 -> Doc
"Open"
    OpenMeta MetaKind
InstanceMeta                    -> Doc
"OpenInstance"
    PostponedTypeCheckingProblem{}           -> Doc
"PostponedTypeCheckingProblem (...)"
    BlockedConst Term
t                           -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ Doc
"BlockedConst", Doc -> Doc
parens (Term -> Doc
forall a. Pretty a => a -> Doc
pretty Term
t) ]
    InstV Instantiation{ [Arg String]
instTel :: Instantiation -> [Arg String]
instTel :: [Arg String]
instTel, Term
instBody :: Instantiation -> Term
instBody :: Term
instBody } -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ Doc
"InstV", [Arg String] -> Doc
forall a. Pretty a => a -> Doc
pretty [Arg String]
instTel, Doc -> Doc
parens (Term -> Doc
forall a. Pretty a => a -> Doc
pretty Term
instBody) ]

-- | Meta variable priority:
--   When we have an equation between meta-variables, which one
--   should be instantiated?
--
--   Higher value means higher priority to be instantiated.
newtype MetaPriority = MetaPriority Int
    deriving (MetaPriority -> MetaPriority -> Bool
(MetaPriority -> MetaPriority -> Bool)
-> (MetaPriority -> MetaPriority -> Bool) -> Eq MetaPriority
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MetaPriority -> MetaPriority -> Bool
== :: MetaPriority -> MetaPriority -> Bool
$c/= :: MetaPriority -> MetaPriority -> Bool
/= :: MetaPriority -> MetaPriority -> Bool
Eq, Eq MetaPriority
Eq MetaPriority =>
(MetaPriority -> MetaPriority -> Ordering)
-> (MetaPriority -> MetaPriority -> Bool)
-> (MetaPriority -> MetaPriority -> Bool)
-> (MetaPriority -> MetaPriority -> Bool)
-> (MetaPriority -> MetaPriority -> Bool)
-> (MetaPriority -> MetaPriority -> MetaPriority)
-> (MetaPriority -> MetaPriority -> MetaPriority)
-> Ord MetaPriority
MetaPriority -> MetaPriority -> Bool
MetaPriority -> MetaPriority -> Ordering
MetaPriority -> MetaPriority -> MetaPriority
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: MetaPriority -> MetaPriority -> Ordering
compare :: MetaPriority -> MetaPriority -> Ordering
$c< :: MetaPriority -> MetaPriority -> Bool
< :: MetaPriority -> MetaPriority -> Bool
$c<= :: MetaPriority -> MetaPriority -> Bool
<= :: MetaPriority -> MetaPriority -> Bool
$c> :: MetaPriority -> MetaPriority -> Bool
> :: MetaPriority -> MetaPriority -> Bool
$c>= :: MetaPriority -> MetaPriority -> Bool
>= :: MetaPriority -> MetaPriority -> Bool
$cmax :: MetaPriority -> MetaPriority -> MetaPriority
max :: MetaPriority -> MetaPriority -> MetaPriority
$cmin :: MetaPriority -> MetaPriority -> MetaPriority
min :: MetaPriority -> MetaPriority -> MetaPriority
Ord, Int -> MetaPriority -> ShowS
[MetaPriority] -> ShowS
MetaPriority -> String
(Int -> MetaPriority -> ShowS)
-> (MetaPriority -> String)
-> ([MetaPriority] -> ShowS)
-> Show MetaPriority
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MetaPriority -> ShowS
showsPrec :: Int -> MetaPriority -> ShowS
$cshow :: MetaPriority -> String
show :: MetaPriority -> String
$cshowList :: [MetaPriority] -> ShowS
showList :: [MetaPriority] -> ShowS
Show, MetaPriority -> ()
(MetaPriority -> ()) -> NFData MetaPriority
forall a. (a -> ()) -> NFData a
$crnf :: MetaPriority -> ()
rnf :: MetaPriority -> ()
NFData)

data RunMetaOccursCheck
  = RunMetaOccursCheck
  | DontRunMetaOccursCheck
  deriving (RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
(RunMetaOccursCheck -> RunMetaOccursCheck -> Bool)
-> (RunMetaOccursCheck -> RunMetaOccursCheck -> Bool)
-> Eq RunMetaOccursCheck
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
== :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
$c/= :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
/= :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
Eq, Eq RunMetaOccursCheck
Eq RunMetaOccursCheck =>
(RunMetaOccursCheck -> RunMetaOccursCheck -> Ordering)
-> (RunMetaOccursCheck -> RunMetaOccursCheck -> Bool)
-> (RunMetaOccursCheck -> RunMetaOccursCheck -> Bool)
-> (RunMetaOccursCheck -> RunMetaOccursCheck -> Bool)
-> (RunMetaOccursCheck -> RunMetaOccursCheck -> Bool)
-> (RunMetaOccursCheck -> RunMetaOccursCheck -> RunMetaOccursCheck)
-> (RunMetaOccursCheck -> RunMetaOccursCheck -> RunMetaOccursCheck)
-> Ord RunMetaOccursCheck
RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
RunMetaOccursCheck -> RunMetaOccursCheck -> Ordering
RunMetaOccursCheck -> RunMetaOccursCheck -> RunMetaOccursCheck
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: RunMetaOccursCheck -> RunMetaOccursCheck -> Ordering
compare :: RunMetaOccursCheck -> RunMetaOccursCheck -> Ordering
$c< :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
< :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
$c<= :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
<= :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
$c> :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
> :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
$c>= :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
>= :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool
$cmax :: RunMetaOccursCheck -> RunMetaOccursCheck -> RunMetaOccursCheck
max :: RunMetaOccursCheck -> RunMetaOccursCheck -> RunMetaOccursCheck
$cmin :: RunMetaOccursCheck -> RunMetaOccursCheck -> RunMetaOccursCheck
min :: RunMetaOccursCheck -> RunMetaOccursCheck -> RunMetaOccursCheck
Ord, Int -> RunMetaOccursCheck -> ShowS
[RunMetaOccursCheck] -> ShowS
RunMetaOccursCheck -> String
(Int -> RunMetaOccursCheck -> ShowS)
-> (RunMetaOccursCheck -> String)
-> ([RunMetaOccursCheck] -> ShowS)
-> Show RunMetaOccursCheck
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RunMetaOccursCheck -> ShowS
showsPrec :: Int -> RunMetaOccursCheck -> ShowS
$cshow :: RunMetaOccursCheck -> String
show :: RunMetaOccursCheck -> String
$cshowList :: [RunMetaOccursCheck] -> ShowS
showList :: [RunMetaOccursCheck] -> ShowS
Show, (forall x. RunMetaOccursCheck -> Rep RunMetaOccursCheck x)
-> (forall x. Rep RunMetaOccursCheck x -> RunMetaOccursCheck)
-> Generic RunMetaOccursCheck
forall x. Rep RunMetaOccursCheck x -> RunMetaOccursCheck
forall x. RunMetaOccursCheck -> Rep RunMetaOccursCheck x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. RunMetaOccursCheck -> Rep RunMetaOccursCheck x
from :: forall x. RunMetaOccursCheck -> Rep RunMetaOccursCheck x
$cto :: forall x. Rep RunMetaOccursCheck x -> RunMetaOccursCheck
to :: forall x. Rep RunMetaOccursCheck x -> RunMetaOccursCheck
Generic)

-- | @MetaInfo@ is cloned from one meta to the next during pruning.
data MetaInfo = MetaInfo
  { MetaInfo -> Closure Range
miClosRange       :: Closure Range -- TODO: Not so nice. But we want both to have the environment of the meta (Closure) and its range.
  , MetaInfo -> Modality
miModality        :: Modality           -- ^ Instantiable with irrelevant/erased solution?
  , MetaInfo -> RunMetaOccursCheck
miMetaOccursCheck :: RunMetaOccursCheck -- ^ Run the extended occurs check that goes in definitions?
  , MetaInfo -> String
miNameSuggestion  :: MetaNameSuggestion
    -- ^ Used for printing.
    --   @Just x@ if meta-variable comes from omitted argument with name @x@.
  , MetaInfo -> Arg DoGeneralize
miGeneralizable   :: Arg DoGeneralize
    -- ^ Should this meta be generalized if unsolved? If so, at what ArgInfo?
  }
  deriving (forall x. MetaInfo -> Rep MetaInfo x)
-> (forall x. Rep MetaInfo x -> MetaInfo) -> Generic MetaInfo
forall x. Rep MetaInfo x -> MetaInfo
forall x. MetaInfo -> Rep MetaInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MetaInfo -> Rep MetaInfo x
from :: forall x. MetaInfo -> Rep MetaInfo x
$cto :: forall x. Rep MetaInfo x -> MetaInfo
to :: forall x. Rep MetaInfo x -> MetaInfo
Generic

instance LensModality MetaInfo where
  getModality :: MetaInfo -> Modality
getModality = MetaInfo -> Modality
miModality
  setModality :: Modality -> MetaInfo -> MetaInfo
setModality Modality
mod MetaInfo
mi = MetaInfo
mi { miModality = mod }
  mapModality :: (Modality -> Modality) -> MetaInfo -> MetaInfo
mapModality Modality -> Modality
f MetaInfo
mi = MetaInfo
mi { miModality = f $ miModality mi }

instance LensQuantity MetaInfo where
  getQuantity :: MetaInfo -> Quantity
getQuantity   = Modality -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity (Modality -> Quantity)
-> (MetaInfo -> Modality) -> MetaInfo -> Quantity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaInfo -> Modality
forall a. LensModality a => a -> Modality
getModality
  mapQuantity :: (Quantity -> Quantity) -> MetaInfo -> MetaInfo
mapQuantity Quantity -> Quantity
f = (Modality -> Modality) -> MetaInfo -> MetaInfo
forall a. LensModality a => (Modality -> Modality) -> a -> a
mapModality ((Quantity -> Quantity) -> Modality -> Modality
forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
mapQuantity Quantity -> Quantity
f)

instance LensRelevance MetaInfo where
  mapRelevance :: (Relevance -> Relevance) -> MetaInfo -> MetaInfo
mapRelevance Relevance -> Relevance
f = (Modality -> Modality) -> MetaInfo -> MetaInfo
forall a. LensModality a => (Modality -> Modality) -> a -> a
mapModality ((Relevance -> Relevance) -> Modality -> Modality
forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
mapRelevance Relevance -> Relevance
f)

-- | For printing, we couple a meta with its name suggestion.
data NamedMeta = NamedMeta
  { NamedMeta -> String
nmSuggestion :: MetaNameSuggestion
  , NamedMeta -> MetaId
nmid         :: MetaId
  }

-- | Append an 'ArgName' to a 'MetaNameSuggestion', for computing the
-- name suggestions of eta-expansion metas. If the 'MetaNameSuggestion'
-- is empty or an underscore, the field name is taken as the suggestion.
suffixNameSuggestion :: MetaNameSuggestion -> ArgName -> MetaNameSuggestion
suffixNameSuggestion :: String -> ShowS
suffixNameSuggestion String
"_"    String
field = String
field
suffixNameSuggestion String
""     String
field = String
field
suffixNameSuggestion String
record String
field = String
record String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"." String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
field

instance Pretty NamedMeta where
  pretty :: NamedMeta -> Doc
pretty (NamedMeta String
"" MetaId
x) = MetaId -> Doc
forall a. Pretty a => a -> Doc
pretty MetaId
x
  pretty (NamedMeta String
"_" MetaId
x) = MetaId -> Doc
forall a. Pretty a => a -> Doc
pretty MetaId
x
  pretty (NamedMeta String
s  MetaId
x) = String -> Doc
forall a. String -> Doc a
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
"_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ MetaId -> String
forall a. Pretty a => a -> String
prettyShow MetaId
x

-- | Used for meta-variables from the current module.

type LocalMetaStore = Map MetaId MetaVariable

{-# SPECIALIZE Map.insert :: MetaId -> v -> Map MetaId v -> Map MetaId v #-}
{-# SPECIALIZE Map.lookup :: MetaId -> Map MetaId v -> Maybe v #-}

-- | Used for meta-variables from other modules (and in 'Interface's).

type RemoteMetaStore = HashMap MetaId RemoteMetaVariable

instance HasRange MetaInfo where
  getRange :: MetaInfo -> Range
getRange = Closure Range -> Range
forall a. Closure a -> a
clValue (Closure Range -> Range)
-> (MetaInfo -> Closure Range) -> MetaInfo -> Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaInfo -> Closure Range
miClosRange

instance HasRange MetaVariable where
    getRange :: MetaVariable -> Range
getRange MetaVariable
m = Closure Range -> Range
forall a. HasRange a => a -> Range
getRange (Closure Range -> Range) -> Closure Range -> Range
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Closure Range
getMetaInfo MetaVariable
m

instance SetRange MetaInfo where
  setRange :: Range -> MetaInfo -> MetaInfo
setRange Range
r MetaInfo
m = MetaInfo
m { miClosRange = (miClosRange m) { clValue = r }}

instance SetRange MetaVariable where
  setRange :: Range -> MetaVariable -> MetaVariable
setRange Range
r MetaVariable
m = MetaVariable
m { mvInfo = setRange r (mvInfo m) }

instance LensModality MetaVariable where
  getModality :: MetaVariable -> Modality
getModality = MetaInfo -> Modality
forall a. LensModality a => a -> Modality
getModality (MetaInfo -> Modality)
-> (MetaVariable -> MetaInfo) -> MetaVariable -> Modality
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> MetaInfo
mvInfo
  setModality :: Modality -> MetaVariable -> MetaVariable
setModality Modality
mod MetaVariable
mv = MetaVariable
mv { mvInfo = setModality mod $ mvInfo mv }
  mapModality :: (Modality -> Modality) -> MetaVariable -> MetaVariable
mapModality Modality -> Modality
f MetaVariable
mv = MetaVariable
mv { mvInfo = mapModality f $ mvInfo mv }

instance LensRelevance MetaVariable where
  setRelevance :: Relevance -> MetaVariable -> MetaVariable
setRelevance Relevance
mod MetaVariable
mv = MetaVariable
mv { mvInfo = setRelevance mod $ mvInfo mv }

instance LensQuantity MetaVariable where
  getQuantity :: MetaVariable -> Quantity
getQuantity   = Modality -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity (Modality -> Quantity)
-> (MetaVariable -> Modality) -> MetaVariable -> Quantity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> Modality
forall a. LensModality a => a -> Modality
getModality
  mapQuantity :: (Quantity -> Quantity) -> MetaVariable -> MetaVariable
mapQuantity Quantity -> Quantity
f = (Modality -> Modality) -> MetaVariable -> MetaVariable
forall a. LensModality a => (Modality -> Modality) -> a -> a
mapModality ((Quantity -> Quantity) -> Modality -> Modality
forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
mapQuantity Quantity -> Quantity
f)

instance LensModality RemoteMetaVariable where
  getModality :: RemoteMetaVariable -> Modality
getModality      = RemoteMetaVariable -> Modality
rmvModality
  mapModality :: (Modality -> Modality) -> RemoteMetaVariable -> RemoteMetaVariable
mapModality Modality -> Modality
f RemoteMetaVariable
mv = RemoteMetaVariable
mv { rmvModality = f $ rmvModality mv }

instance LensRelevance RemoteMetaVariable where
  mapRelevance :: (Relevance -> Relevance)
-> RemoteMetaVariable -> RemoteMetaVariable
mapRelevance Relevance -> Relevance
f = (Modality -> Modality) -> RemoteMetaVariable -> RemoteMetaVariable
forall a. LensModality a => (Modality -> Modality) -> a -> a
mapModality ((Relevance -> Relevance) -> Modality -> Modality
forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
mapRelevance Relevance -> Relevance
f)

instance LensQuantity RemoteMetaVariable where
  mapQuantity :: (Quantity -> Quantity) -> RemoteMetaVariable -> RemoteMetaVariable
mapQuantity Quantity -> Quantity
f = (Modality -> Modality) -> RemoteMetaVariable -> RemoteMetaVariable
forall a. LensModality a => (Modality -> Modality) -> a -> a
mapModality ((Quantity -> Quantity) -> Modality -> Modality
forall a. LensQuantity a => (Quantity -> Quantity) -> a -> a
mapQuantity Quantity -> Quantity
f)

normalMetaPriority :: MetaPriority
normalMetaPriority :: MetaPriority
normalMetaPriority = Int -> MetaPriority
MetaPriority Int
0

lowMetaPriority :: MetaPriority
lowMetaPriority :: MetaPriority
lowMetaPriority = Int -> MetaPriority
MetaPriority (-Int
10)

highMetaPriority :: MetaPriority
highMetaPriority :: MetaPriority
highMetaPriority = Int -> MetaPriority
MetaPriority Int
10

getMetaInfo :: MetaVariable -> Closure Range
getMetaInfo :: MetaVariable -> Closure Range
getMetaInfo = MetaInfo -> Closure Range
miClosRange (MetaInfo -> Closure Range)
-> (MetaVariable -> MetaInfo) -> MetaVariable -> Closure Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> MetaInfo
mvInfo

getMetaScope :: MetaVariable -> ScopeInfo
getMetaScope :: MetaVariable -> ScopeInfo
getMetaScope MetaVariable
m = Closure Range -> ScopeInfo
forall a. Closure a -> ScopeInfo
clScope (Closure Range -> ScopeInfo) -> Closure Range -> ScopeInfo
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Closure Range
getMetaInfo MetaVariable
m

getMetaEnv :: MetaVariable -> TCEnv
getMetaEnv :: MetaVariable -> TCEnv
getMetaEnv MetaVariable
m = Closure Range -> TCEnv
forall a. Closure a -> TCEnv
clEnv (Closure Range -> TCEnv) -> Closure Range -> TCEnv
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Closure Range
getMetaInfo MetaVariable
m

getMetaSig :: MetaVariable -> Signature
getMetaSig :: MetaVariable -> Signature
getMetaSig MetaVariable
m = Closure Range -> Signature
forall a. Closure a -> Signature
clSignature (Closure Range -> Signature) -> Closure Range -> Signature
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Closure Range
getMetaInfo MetaVariable
m

-- Lenses

metaFrozen :: Lens' MetaVariable Frozen
metaFrozen :: Lens' MetaVariable Frozen
metaFrozen Frozen -> f Frozen
f MetaVariable
mv = Frozen -> f Frozen
f (MetaVariable -> Frozen
mvFrozen MetaVariable
mv) f Frozen -> (Frozen -> MetaVariable) -> f MetaVariable
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Frozen
x -> MetaVariable
mv { mvFrozen = x }

_mvInfo :: Lens' MetaVariable MetaInfo