-- | Data structures for the type checker.
--
-- Part of "Agda.TypeChecking.Monad.Base", extracted to avoid import cycles.

module Agda.TypeChecking.Monad.Base.Types
  ( module Agda.TypeChecking.Monad.Base.Types
  , module X
  )
where

import Prelude hiding (null)

import Control.DeepSeq                ( NFData )
import Data.EnumMap                   ( EnumMap )
import Data.Functor                   ( (<&>) )
import Data.Map                       ( Map )
import GHC.Generics                   ( Generic )

import Agda.Syntax.Info               ( MetaNameSuggestion )
import Agda.Syntax.Internal
import Agda.Syntax.TopLevelModuleName as X ( TopLevelModuleName )

import Agda.Utils.FileId              as X ( FileId, FileDictBuilder )
import Agda.Utils.FileName            as X ( AbsolutePath )
import Agda.Utils.Lens                ( Lens', (&&&), iso )
import Agda.Utils.Null                ( Null(..) )

import Agda.Syntax.Internal           ( Dom, Name, Type )
import Agda.Syntax.Common
  ( LensArgInfo(..), LensCohesion, LensHiding, LensModality, LensOrigin, LensQuantity, LensRelevance, LensModalPolarity )

---------------------------------------------------------------------------
-- * Context
---------------------------------------------------------------------------

-- | The @Context@ is a stack of 'ContextEntry's.
type Context = [ContextEntry]

data ContextEntry
  = CtxVar
    { ContextEntry -> Name
ceName :: Name
    , ContextEntry -> Dom Type
ceType :: Dom Type
    }
  -- N.B. 2024-11-29 there might be CtxLet in the future.
  deriving (Int -> ContextEntry -> ShowS
[ContextEntry] -> ShowS
ContextEntry -> String
(Int -> ContextEntry -> ShowS)
-> (ContextEntry -> String)
-> ([ContextEntry] -> ShowS)
-> Show ContextEntry
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ContextEntry -> ShowS
showsPrec :: Int -> ContextEntry -> ShowS
$cshow :: ContextEntry -> String
show :: ContextEntry -> String
$cshowList :: [ContextEntry] -> ShowS
showList :: [ContextEntry] -> ShowS
Show, (forall x. ContextEntry -> Rep ContextEntry x)
-> (forall x. Rep ContextEntry x -> ContextEntry)
-> Generic ContextEntry
forall x. Rep ContextEntry x -> ContextEntry
forall x. ContextEntry -> Rep ContextEntry x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ContextEntry -> Rep ContextEntry x
from :: forall x. ContextEntry -> Rep ContextEntry x
$cto :: forall x. Rep ContextEntry x -> ContextEntry
to :: forall x. Rep ContextEntry x -> ContextEntry
Generic)

instance LensArgInfo ContextEntry where
  getArgInfo :: ContextEntry -> ArgInfo
getArgInfo (CtxVar Name
_ Dom Type
a) = Dom Type -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Dom Type
a
  mapArgInfo :: (ArgInfo -> ArgInfo) -> ContextEntry -> ContextEntry
mapArgInfo ArgInfo -> ArgInfo
f (CtxVar Name
x Dom Type
a) = Name -> Dom Type -> ContextEntry
CtxVar Name
x (Dom Type -> ContextEntry) -> Dom Type -> ContextEntry
forall a b. (a -> b) -> a -> b
$ (ArgInfo -> ArgInfo) -> Dom Type -> Dom Type
forall a. LensArgInfo a => (ArgInfo -> ArgInfo) -> a -> a
mapArgInfo ArgInfo -> ArgInfo
f Dom Type
a

instance LensModality  ContextEntry
instance LensRelevance ContextEntry
instance LensCohesion  ContextEntry
instance LensOrigin    ContextEntry
instance LensQuantity  ContextEntry
instance LensHiding    ContextEntry
instance LensModalPolarity ContextEntry

---------------------------------------------------------------------------
-- * Conversion
---------------------------------------------------------------------------

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)

-- | Polarity for equality and subtype checking.
data Polarity
  = Covariant      -- ^ monotone
  | Contravariant  -- ^ antitone
  | Invariant      -- ^ no information (mixed variance)
  | Nonvariant     -- ^ constant
  deriving (Int -> Polarity -> ShowS
[Polarity] -> ShowS
Polarity -> String
(Int -> Polarity -> ShowS)
-> (Polarity -> String) -> ([Polarity] -> ShowS) -> Show Polarity
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Polarity -> ShowS
showsPrec :: Int -> Polarity -> ShowS
$cshow :: Polarity -> String
show :: Polarity -> String
$cshowList :: [Polarity] -> ShowS
showList :: [Polarity] -> ShowS
Show, Polarity -> Polarity -> Bool
(Polarity -> Polarity -> Bool)
-> (Polarity -> Polarity -> Bool) -> Eq Polarity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Polarity -> Polarity -> Bool
== :: Polarity -> Polarity -> Bool
$c/= :: Polarity -> Polarity -> Bool
/= :: Polarity -> Polarity -> Bool
Eq, (forall x. Polarity -> Rep Polarity x)
-> (forall x. Rep Polarity x -> Polarity) -> Generic Polarity
forall x. Rep Polarity x -> Polarity
forall x. Polarity -> Rep Polarity x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Polarity -> Rep Polarity x
from :: forall x. Polarity -> Rep Polarity x
$cto :: forall x. Rep Polarity x -> Polarity
to :: forall x. Rep Polarity x -> Polarity
Generic)

---------------------------------------------------------------------------
-- * Cubical
---------------------------------------------------------------------------

-- | Datatype representing a single boundary condition:
--   x_0 = u_0, ... ,x_n = u_n ⊢ t = ?n es
data IPFace' t = IPFace'
  { forall t. IPFace' t -> [(t, t)]
faceEqns :: [(t, t)]
  , forall t. IPFace' t -> t
faceRHS  :: t
  }

---------------------------------------------------------------------------
-- * Highlighting
---------------------------------------------------------------------------

-- | How much highlighting should be sent to the user interface?

data HighlightingLevel
  = None
  | NonInteractive
  | Interactive
    -- ^ This includes both non-interactive highlighting and
    -- interactive highlighting of the expression that is currently
    -- being type-checked.
    deriving (HighlightingLevel -> HighlightingLevel -> Bool
(HighlightingLevel -> HighlightingLevel -> Bool)
-> (HighlightingLevel -> HighlightingLevel -> Bool)
-> Eq HighlightingLevel
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HighlightingLevel -> HighlightingLevel -> Bool
== :: HighlightingLevel -> HighlightingLevel -> Bool
$c/= :: HighlightingLevel -> HighlightingLevel -> Bool
/= :: HighlightingLevel -> HighlightingLevel -> Bool
Eq, Eq HighlightingLevel
Eq HighlightingLevel =>
(HighlightingLevel -> HighlightingLevel -> Ordering)
-> (HighlightingLevel -> HighlightingLevel -> Bool)
-> (HighlightingLevel -> HighlightingLevel -> Bool)
-> (HighlightingLevel -> HighlightingLevel -> Bool)
-> (HighlightingLevel -> HighlightingLevel -> Bool)
-> (HighlightingLevel -> HighlightingLevel -> HighlightingLevel)
-> (HighlightingLevel -> HighlightingLevel -> HighlightingLevel)
-> Ord HighlightingLevel
HighlightingLevel -> HighlightingLevel -> Bool
HighlightingLevel -> HighlightingLevel -> Ordering
HighlightingLevel -> HighlightingLevel -> HighlightingLevel
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 :: HighlightingLevel -> HighlightingLevel -> Ordering
compare :: HighlightingLevel -> HighlightingLevel -> Ordering
$c< :: HighlightingLevel -> HighlightingLevel -> Bool
< :: HighlightingLevel -> HighlightingLevel -> Bool
$c<= :: HighlightingLevel -> HighlightingLevel -> Bool
<= :: HighlightingLevel -> HighlightingLevel -> Bool
$c> :: HighlightingLevel -> HighlightingLevel -> Bool
> :: HighlightingLevel -> HighlightingLevel -> Bool
$c>= :: HighlightingLevel -> HighlightingLevel -> Bool
>= :: HighlightingLevel -> HighlightingLevel -> Bool
$cmax :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel
max :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel
$cmin :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel
min :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel
Ord, Int -> HighlightingLevel -> ShowS
[HighlightingLevel] -> ShowS
HighlightingLevel -> String
(Int -> HighlightingLevel -> ShowS)
-> (HighlightingLevel -> String)
-> ([HighlightingLevel] -> ShowS)
-> Show HighlightingLevel
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HighlightingLevel -> ShowS
showsPrec :: Int -> HighlightingLevel -> ShowS
$cshow :: HighlightingLevel -> String
show :: HighlightingLevel -> String
$cshowList :: [HighlightingLevel] -> ShowS
showList :: [HighlightingLevel] -> ShowS
Show, ReadPrec [HighlightingLevel]
ReadPrec HighlightingLevel
Int -> ReadS HighlightingLevel
ReadS [HighlightingLevel]
(Int -> ReadS HighlightingLevel)
-> ReadS [HighlightingLevel]
-> ReadPrec HighlightingLevel
-> ReadPrec [HighlightingLevel]
-> Read HighlightingLevel
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS HighlightingLevel
readsPrec :: Int -> ReadS HighlightingLevel
$creadList :: ReadS [HighlightingLevel]
readList :: ReadS [HighlightingLevel]
$creadPrec :: ReadPrec HighlightingLevel
readPrec :: ReadPrec HighlightingLevel
$creadListPrec :: ReadPrec [HighlightingLevel]
readListPrec :: ReadPrec [HighlightingLevel]
Read, (forall x. HighlightingLevel -> Rep HighlightingLevel x)
-> (forall x. Rep HighlightingLevel x -> HighlightingLevel)
-> Generic HighlightingLevel
forall x. Rep HighlightingLevel x -> HighlightingLevel
forall x. HighlightingLevel -> Rep HighlightingLevel x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. HighlightingLevel -> Rep HighlightingLevel x
from :: forall x. HighlightingLevel -> Rep HighlightingLevel x
$cto :: forall x. Rep HighlightingLevel x -> HighlightingLevel
to :: forall x. Rep HighlightingLevel x -> HighlightingLevel
Generic)

-- | How should highlighting be sent to the user interface?

data HighlightingMethod
  = Direct
    -- ^ Via stdout.
  | Indirect
    -- ^ Both via files and via stdout.
    deriving (HighlightingMethod -> HighlightingMethod -> Bool
(HighlightingMethod -> HighlightingMethod -> Bool)
-> (HighlightingMethod -> HighlightingMethod -> Bool)
-> Eq HighlightingMethod
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HighlightingMethod -> HighlightingMethod -> Bool
== :: HighlightingMethod -> HighlightingMethod -> Bool
$c/= :: HighlightingMethod -> HighlightingMethod -> Bool
/= :: HighlightingMethod -> HighlightingMethod -> Bool
Eq, Int -> HighlightingMethod -> ShowS
[HighlightingMethod] -> ShowS
HighlightingMethod -> String
(Int -> HighlightingMethod -> ShowS)
-> (HighlightingMethod -> String)
-> ([HighlightingMethod] -> ShowS)
-> Show HighlightingMethod
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HighlightingMethod -> ShowS
showsPrec :: Int -> HighlightingMethod -> ShowS
$cshow :: HighlightingMethod -> String
show :: HighlightingMethod -> String
$cshowList :: [HighlightingMethod] -> ShowS
showList :: [HighlightingMethod] -> ShowS
Show, ReadPrec [HighlightingMethod]
ReadPrec HighlightingMethod
Int -> ReadS HighlightingMethod
ReadS [HighlightingMethod]
(Int -> ReadS HighlightingMethod)
-> ReadS [HighlightingMethod]
-> ReadPrec HighlightingMethod
-> ReadPrec [HighlightingMethod]
-> Read HighlightingMethod
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS HighlightingMethod
readsPrec :: Int -> ReadS HighlightingMethod
$creadList :: ReadS [HighlightingMethod]
readList :: ReadS [HighlightingMethod]
$creadPrec :: ReadPrec HighlightingMethod
readPrec :: ReadPrec HighlightingMethod
$creadListPrec :: ReadPrec [HighlightingMethod]
readListPrec :: ReadPrec [HighlightingMethod]
Read, (forall x. HighlightingMethod -> Rep HighlightingMethod x)
-> (forall x. Rep HighlightingMethod x -> HighlightingMethod)
-> Generic HighlightingMethod
forall x. Rep HighlightingMethod x -> HighlightingMethod
forall x. HighlightingMethod -> Rep HighlightingMethod x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. HighlightingMethod -> Rep HighlightingMethod x
from :: forall x. HighlightingMethod -> Rep HighlightingMethod x
$cto :: forall x. Rep HighlightingMethod x -> HighlightingMethod
to :: forall x. Rep HighlightingMethod x -> HighlightingMethod
Generic)

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

-- | Discern Agda's primitive modules from other file modules.
--   @IsPrimitiveModule `implies` IsBuiltinModuleWithSafePostulate `implies` isBuiltinModule.

--   Keep constructors in this order!
data IsBuiltinModule
  = IsPrimitiveModule
      -- ^ Very magical module, e.g. @Agda.Primitive@.
  | IsBuiltinModuleWithSafePostulates
      -- ^ Safe module, e.g. @Agda.Builtin.Equality@.
  | IsBuiltinModule
      -- ^ Any builtin module.
  deriving (IsBuiltinModule -> IsBuiltinModule -> Bool
(IsBuiltinModule -> IsBuiltinModule -> Bool)
-> (IsBuiltinModule -> IsBuiltinModule -> Bool)
-> Eq IsBuiltinModule
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: IsBuiltinModule -> IsBuiltinModule -> Bool
== :: IsBuiltinModule -> IsBuiltinModule -> Bool
$c/= :: IsBuiltinModule -> IsBuiltinModule -> Bool
/= :: IsBuiltinModule -> IsBuiltinModule -> Bool
Eq, Eq IsBuiltinModule
Eq IsBuiltinModule =>
(IsBuiltinModule -> IsBuiltinModule -> Ordering)
-> (IsBuiltinModule -> IsBuiltinModule -> Bool)
-> (IsBuiltinModule -> IsBuiltinModule -> Bool)
-> (IsBuiltinModule -> IsBuiltinModule -> Bool)
-> (IsBuiltinModule -> IsBuiltinModule -> Bool)
-> (IsBuiltinModule -> IsBuiltinModule -> IsBuiltinModule)
-> (IsBuiltinModule -> IsBuiltinModule -> IsBuiltinModule)
-> Ord IsBuiltinModule
IsBuiltinModule -> IsBuiltinModule -> Bool
IsBuiltinModule -> IsBuiltinModule -> Ordering
IsBuiltinModule -> IsBuiltinModule -> IsBuiltinModule
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 :: IsBuiltinModule -> IsBuiltinModule -> Ordering
compare :: IsBuiltinModule -> IsBuiltinModule -> Ordering
$c< :: IsBuiltinModule -> IsBuiltinModule -> Bool
< :: IsBuiltinModule -> IsBuiltinModule -> Bool
$c<= :: IsBuiltinModule -> IsBuiltinModule -> Bool
<= :: IsBuiltinModule -> IsBuiltinModule -> Bool
$c> :: IsBuiltinModule -> IsBuiltinModule -> Bool
> :: IsBuiltinModule -> IsBuiltinModule -> Bool
$c>= :: IsBuiltinModule -> IsBuiltinModule -> Bool
>= :: IsBuiltinModule -> IsBuiltinModule -> Bool
$cmax :: IsBuiltinModule -> IsBuiltinModule -> IsBuiltinModule
max :: IsBuiltinModule -> IsBuiltinModule -> IsBuiltinModule
$cmin :: IsBuiltinModule -> IsBuiltinModule -> IsBuiltinModule
min :: IsBuiltinModule -> IsBuiltinModule -> IsBuiltinModule
Ord, Int -> IsBuiltinModule -> ShowS
[IsBuiltinModule] -> ShowS
IsBuiltinModule -> String
(Int -> IsBuiltinModule -> ShowS)
-> (IsBuiltinModule -> String)
-> ([IsBuiltinModule] -> ShowS)
-> Show IsBuiltinModule
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IsBuiltinModule -> ShowS
showsPrec :: Int -> IsBuiltinModule -> ShowS
$cshow :: IsBuiltinModule -> String
show :: IsBuiltinModule -> String
$cshowList :: [IsBuiltinModule] -> ShowS
showList :: [IsBuiltinModule] -> ShowS
Show, (forall x. IsBuiltinModule -> Rep IsBuiltinModule x)
-> (forall x. Rep IsBuiltinModule x -> IsBuiltinModule)
-> Generic IsBuiltinModule
forall x. Rep IsBuiltinModule x -> IsBuiltinModule
forall x. IsBuiltinModule -> Rep IsBuiltinModule x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. IsBuiltinModule -> Rep IsBuiltinModule x
from :: forall x. IsBuiltinModule -> Rep IsBuiltinModule x
$cto :: forall x. Rep IsBuiltinModule x -> IsBuiltinModule
to :: forall x. Rep IsBuiltinModule x -> IsBuiltinModule
Generic)

-- | Collection of 'FileId's of primitive modules.

type BuiltinModuleIds = EnumMap FileId IsBuiltinModule

-- | Translation between 'AbsolutePath' and 'FileId' that also knows about Agda's builtin modules.

data FileDictWithBuiltins = FileDictWithBuiltins
  { FileDictWithBuiltins -> FileDictBuilder
fileDictBuilder  :: !FileDictBuilder
      -- ^ (Building a) translation between 'AbsolutePath' and 'FileId'.
  , FileDictWithBuiltins -> BuiltinModuleIds
builtinModuleIds :: !BuiltinModuleIds
      -- ^ For the known 'FileId's, remember whether they refer to Agda's builtin modules.
  , FileDictWithBuiltins -> PrimitiveLibDir
primitiveLibDir  :: !PrimitiveLibDir
      -- ^ The absolute path to the directory with the builtin modules.
      --   Needs to be set upon initialization.
  }
  deriving (forall x. FileDictWithBuiltins -> Rep FileDictWithBuiltins x)
-> (forall x. Rep FileDictWithBuiltins x -> FileDictWithBuiltins)
-> Generic FileDictWithBuiltins
forall x. Rep FileDictWithBuiltins x -> FileDictWithBuiltins
forall x. FileDictWithBuiltins -> Rep FileDictWithBuiltins x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. FileDictWithBuiltins -> Rep FileDictWithBuiltins x
from :: forall x. FileDictWithBuiltins -> Rep FileDictWithBuiltins x
$cto :: forall x. Rep FileDictWithBuiltins x -> FileDictWithBuiltins
to :: forall x. Rep FileDictWithBuiltins x -> FileDictWithBuiltins
Generic

type PrimitiveLibDir = AbsolutePath

-- | 'SourceFile's must exist and be registered in our file dictionary.

newtype SourceFile = SourceFile { SourceFile -> FileId
srcFileId :: FileId }
  deriving (SourceFile -> SourceFile -> Bool
(SourceFile -> SourceFile -> Bool)
-> (SourceFile -> SourceFile -> Bool) -> Eq SourceFile
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SourceFile -> SourceFile -> Bool
== :: SourceFile -> SourceFile -> Bool
$c/= :: SourceFile -> SourceFile -> Bool
/= :: SourceFile -> SourceFile -> Bool
Eq, Eq SourceFile
Eq SourceFile =>
(SourceFile -> SourceFile -> Ordering)
-> (SourceFile -> SourceFile -> Bool)
-> (SourceFile -> SourceFile -> Bool)
-> (SourceFile -> SourceFile -> Bool)
-> (SourceFile -> SourceFile -> Bool)
-> (SourceFile -> SourceFile -> SourceFile)
-> (SourceFile -> SourceFile -> SourceFile)
-> Ord SourceFile
SourceFile -> SourceFile -> Bool
SourceFile -> SourceFile -> Ordering
SourceFile -> SourceFile -> SourceFile
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 :: SourceFile -> SourceFile -> Ordering
compare :: SourceFile -> SourceFile -> Ordering
$c< :: SourceFile -> SourceFile -> Bool
< :: SourceFile -> SourceFile -> Bool
$c<= :: SourceFile -> SourceFile -> Bool
<= :: SourceFile -> SourceFile -> Bool
$c> :: SourceFile -> SourceFile -> Bool
> :: SourceFile -> SourceFile -> Bool
$c>= :: SourceFile -> SourceFile -> Bool
>= :: SourceFile -> SourceFile -> Bool
$cmax :: SourceFile -> SourceFile -> SourceFile
max :: SourceFile -> SourceFile -> SourceFile
$cmin :: SourceFile -> SourceFile -> SourceFile
min :: SourceFile -> SourceFile -> SourceFile
Ord, Int -> SourceFile -> ShowS
[SourceFile] -> ShowS
SourceFile -> String
(Int -> SourceFile -> ShowS)
-> (SourceFile -> String)
-> ([SourceFile] -> ShowS)
-> Show SourceFile
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SourceFile -> ShowS
showsPrec :: Int -> SourceFile -> ShowS
$cshow :: SourceFile -> String
show :: SourceFile -> String
$cshowList :: [SourceFile] -> ShowS
showList :: [SourceFile] -> ShowS
Show, (forall x. SourceFile -> Rep SourceFile x)
-> (forall x. Rep SourceFile x -> SourceFile) -> Generic SourceFile
forall x. Rep SourceFile x -> SourceFile
forall x. SourceFile -> Rep SourceFile x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SourceFile -> Rep SourceFile x
from :: forall x. SourceFile -> Rep SourceFile x
$cto :: forall x. Rep SourceFile x -> SourceFile
to :: forall x. Rep SourceFile x -> SourceFile
Generic)

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

type ModuleToSourceId = Map TopLevelModuleName SourceFile

data ModuleToSource = ModuleToSource
  { ModuleToSource -> FileDictWithBuiltins
fileDict         :: !FileDictWithBuiltins
  , ModuleToSource -> ModuleToSourceId
moduleToSourceId :: !ModuleToSourceId
  }

-- ** Lenses

lensFileDictFileDictBuilder :: Lens' FileDictWithBuiltins FileDictBuilder
lensFileDictFileDictBuilder :: Lens' FileDictWithBuiltins FileDictBuilder
lensFileDictFileDictBuilder FileDictBuilder -> f FileDictBuilder
f FileDictWithBuiltins
s = FileDictBuilder -> f FileDictBuilder
f (FileDictWithBuiltins -> FileDictBuilder
fileDictBuilder FileDictWithBuiltins
s) f FileDictBuilder
-> (FileDictBuilder -> FileDictWithBuiltins)
-> f FileDictWithBuiltins
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ FileDictBuilder
x -> FileDictWithBuiltins
s { fileDictBuilder = x }

lensFileDictBuiltinModuleIds :: Lens' FileDictWithBuiltins BuiltinModuleIds
lensFileDictBuiltinModuleIds :: Lens' FileDictWithBuiltins BuiltinModuleIds
lensFileDictBuiltinModuleIds BuiltinModuleIds -> f BuiltinModuleIds
f FileDictWithBuiltins
s = BuiltinModuleIds -> f BuiltinModuleIds
f (FileDictWithBuiltins -> BuiltinModuleIds
builtinModuleIds FileDictWithBuiltins
s) f BuiltinModuleIds
-> (BuiltinModuleIds -> FileDictWithBuiltins)
-> f FileDictWithBuiltins
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ BuiltinModuleIds
x -> FileDictWithBuiltins
s { builtinModuleIds = x }

lensFileDictPrimitiveLibDir :: Lens' FileDictWithBuiltins PrimitiveLibDir
lensFileDictPrimitiveLibDir :: Lens' FileDictWithBuiltins PrimitiveLibDir
lensFileDictPrimitiveLibDir PrimitiveLibDir -> f PrimitiveLibDir
f FileDictWithBuiltins
s = PrimitiveLibDir -> f PrimitiveLibDir
f (FileDictWithBuiltins -> PrimitiveLibDir
primitiveLibDir FileDictWithBuiltins
s) f PrimitiveLibDir
-> (PrimitiveLibDir -> FileDictWithBuiltins)
-> f FileDictWithBuiltins
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ PrimitiveLibDir
x -> FileDictWithBuiltins
s { primitiveLibDir = x }

lensPairModuleToSource :: Lens' (FileDictWithBuiltins, ModuleToSourceId) ModuleToSource
lensPairModuleToSource :: Lens' (FileDictWithBuiltins, ModuleToSourceId) ModuleToSource
lensPairModuleToSource = ((FileDictWithBuiltins, ModuleToSourceId) -> ModuleToSource)
-> (ModuleToSource -> (FileDictWithBuiltins, ModuleToSourceId))
-> Lens' (FileDictWithBuiltins, ModuleToSourceId) ModuleToSource
forall o i. (o -> i) -> (i -> o) -> Lens' o i
iso ((FileDictWithBuiltins -> ModuleToSourceId -> ModuleToSource)
-> (FileDictWithBuiltins, ModuleToSourceId) -> ModuleToSource
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry FileDictWithBuiltins -> ModuleToSourceId -> ModuleToSource
ModuleToSource) (ModuleToSource -> FileDictWithBuiltins
fileDict (ModuleToSource -> FileDictWithBuiltins)
-> (ModuleToSource -> ModuleToSourceId)
-> ModuleToSource
-> (FileDictWithBuiltins, ModuleToSourceId)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& ModuleToSource -> ModuleToSourceId
moduleToSourceId)

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

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



-- Feel free to move more types from Agda.TypeChecking.Monad.Base here when needed...

-- Null instances

-- Andreas, 2024-11-10: Let's not have these instances because there is no default primLibDir:
--
-- instance Null FileDictWithBuiltins where
--   empty = FileDictWithBuiltins empty empty __IMPOSSIBLE__
--   null (FileDictWithBuiltins a b _primLibDir) = null a && null b
--
-- instance Null ModuleToSource where
--   empty = ModuleToSource empty empty
--   null (ModuleToSource dict m2s) = null dict && null m2s

-- NFData instances

instance NFData ContextEntry
instance NFData FileDictWithBuiltins
instance NFData SourceFile
instance NFData IsBuiltinModule