-- | 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.Common
  ( LensArgInfo(..), LensCohesion, LensHiding, LensModality, LensOrigin, LensQuantity, LensRelevance, LensModalPolarity, Nat )

import Agda.Syntax.Info               ( MetaNameSuggestion )
import Agda.Syntax.Internal           ( Dom, MetaId, Name, Type )
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.Utils.Size                ( Sized )
import Agda.Utils.List                ( (!!!) )
import Agda.Utils.Tuple               ( second )


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

-- | The @Context@ is a stack of 'ContextEntry's.
--   Unlike telescopes, later context entries are bound in earlier ones.
newtype Context' a = Context
  { forall a. Context' a -> [a]
cxEntries :: [a]
  }
  deriving (Int -> Context' a -> ShowS
[Context' a] -> ShowS
Context' a -> String
(Int -> Context' a -> ShowS)
-> (Context' a -> String)
-> ([Context' a] -> ShowS)
-> Show (Context' a)
forall a. Show a => Int -> Context' a -> ShowS
forall a. Show a => [Context' a] -> ShowS
forall a. Show a => Context' a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Context' a -> ShowS
showsPrec :: Int -> Context' a -> ShowS
$cshow :: forall a. Show a => Context' a -> String
show :: Context' a -> String
$cshowList :: forall a. Show a => [Context' a] -> ShowS
showList :: [Context' a] -> ShowS
Show, (forall x. Context' a -> Rep (Context' a) x)
-> (forall x. Rep (Context' a) x -> Context' a)
-> Generic (Context' a)
forall x. Rep (Context' a) x -> Context' a
forall x. Context' a -> Rep (Context' a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Context' a) x -> Context' a
forall a x. Context' a -> Rep (Context' a) x
$cfrom :: forall a x. Context' a -> Rep (Context' a) x
from :: forall x. Context' a -> Rep (Context' a) x
$cto :: forall a x. Rep (Context' a) x -> Context' a
to :: forall x. Rep (Context' a) x -> Context' a
Generic, Context' a -> Int
Context' a -> Peano
(Context' a -> Int) -> (Context' a -> Peano) -> Sized (Context' a)
forall a. Context' a -> Int
forall a. Context' a -> Peano
forall a. (a -> Int) -> (a -> Peano) -> Sized a
$csize :: forall a. Context' a -> Int
size :: Context' a -> Int
$cnatSize :: forall a. Context' a -> Peano
natSize :: Context' a -> Peano
Sized, (forall a b. (a -> b) -> Context' a -> Context' b)
-> (forall a b. a -> Context' b -> Context' a) -> Functor Context'
forall a b. a -> Context' b -> Context' a
forall a b. (a -> b) -> Context' a -> Context' 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) -> Context' a -> Context' b
fmap :: forall a b. (a -> b) -> Context' a -> Context' b
$c<$ :: forall a b. a -> Context' b -> Context' a
<$ :: forall a b. a -> Context' b -> Context' a
Functor, (forall m. Monoid m => Context' m -> m)
-> (forall m a. Monoid m => (a -> m) -> Context' a -> m)
-> (forall m a. Monoid m => (a -> m) -> Context' a -> m)
-> (forall a b. (a -> b -> b) -> b -> Context' a -> b)
-> (forall a b. (a -> b -> b) -> b -> Context' a -> b)
-> (forall b a. (b -> a -> b) -> b -> Context' a -> b)
-> (forall b a. (b -> a -> b) -> b -> Context' a -> b)
-> (forall a. (a -> a -> a) -> Context' a -> a)
-> (forall a. (a -> a -> a) -> Context' a -> a)
-> (forall a. Context' a -> [a])
-> (forall a. Context' a -> Bool)
-> (forall a. Context' a -> Int)
-> (forall a. Eq a => a -> Context' a -> Bool)
-> (forall a. Ord a => Context' a -> a)
-> (forall a. Ord a => Context' a -> a)
-> (forall a. Num a => Context' a -> a)
-> (forall a. Num a => Context' a -> a)
-> Foldable Context'
forall a. Eq a => a -> Context' a -> Bool
forall a. Num a => Context' a -> a
forall a. Ord a => Context' a -> a
forall m. Monoid m => Context' m -> m
forall a. Context' a -> Bool
forall a. Context' a -> Int
forall a. Context' a -> [a]
forall a. (a -> a -> a) -> Context' a -> a
forall m a. Monoid m => (a -> m) -> Context' a -> m
forall b a. (b -> a -> b) -> b -> Context' a -> b
forall a b. (a -> b -> b) -> b -> Context' 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 => Context' m -> m
fold :: forall m. Monoid m => Context' m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Context' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Context' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Context' a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Context' a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Context' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Context' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Context' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Context' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Context' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Context' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Context' a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Context' a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Context' a -> a
foldr1 :: forall a. (a -> a -> a) -> Context' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Context' a -> a
foldl1 :: forall a. (a -> a -> a) -> Context' a -> a
$ctoList :: forall a. Context' a -> [a]
toList :: forall a. Context' a -> [a]
$cnull :: forall a. Context' a -> Bool
null :: forall a. Context' a -> Bool
$clength :: forall a. Context' a -> Int
length :: forall a. Context' a -> Int
$celem :: forall a. Eq a => a -> Context' a -> Bool
elem :: forall a. Eq a => a -> Context' a -> Bool
$cmaximum :: forall a. Ord a => Context' a -> a
maximum :: forall a. Ord a => Context' a -> a
$cminimum :: forall a. Ord a => Context' a -> a
minimum :: forall a. Ord a => Context' a -> a
$csum :: forall a. Num a => Context' a -> a
sum :: forall a. Num a => Context' a -> a
$cproduct :: forall a. Num a => Context' a -> a
product :: forall a. Num a => Context' a -> a
Foldable, Context' a
Context' a -> Bool
Context' a -> (Context' a -> Bool) -> Null (Context' a)
forall a. Context' a
forall a. a -> (a -> Bool) -> Null a
forall a. Context' a -> Bool
$cempty :: forall a. Context' a
empty :: Context' a
$cnull :: forall a. Context' a -> Bool
null :: Context' a -> Bool
Null, Functor Context'
Foldable Context'
(Functor Context', Foldable Context') =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Context' a -> f (Context' b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Context' (f a) -> f (Context' a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Context' a -> m (Context' b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Context' (m a) -> m (Context' a))
-> Traversable Context'
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 => Context' (m a) -> m (Context' a)
forall (f :: * -> *) a.
Applicative f =>
Context' (f a) -> f (Context' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Context' a -> m (Context' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Context' a -> f (Context' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Context' a -> f (Context' b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Context' a -> f (Context' b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Context' (f a) -> f (Context' a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Context' (f a) -> f (Context' a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Context' a -> m (Context' b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Context' a -> m (Context' b)
$csequence :: forall (m :: * -> *) a. Monad m => Context' (m a) -> m (Context' a)
sequence :: forall (m :: * -> *) a. Monad m => Context' (m a) -> m (Context' a)
Traversable)

type Context = Context' ContextEntry

pattern CxEmpty     :: Context
pattern CxExtendVar :: Name -> Dom Type -> Context -> Context
pattern CxExtend    :: ContextEntry -> Context -> Context

pattern $mCxEmpty :: forall {r}. Context -> ((# #) -> r) -> ((# #) -> r) -> r
$bCxEmpty :: Context
CxEmpty = Context []
pattern $mCxExtend :: forall {r}.
Context -> (ContextEntry -> Context -> r) -> ((# #) -> r) -> r
$bCxExtend :: ContextEntry -> Context -> Context
CxExtend x g <- Context (x : (Context -> g)) where
  CxExtend ContextEntry
x (Context [ContextEntry]
g) = [ContextEntry] -> Context
forall a. [a] -> Context' a
Context (ContextEntry
x ContextEntry -> [ContextEntry] -> [ContextEntry]
forall a. a -> [a] -> [a]
: [ContextEntry]
g)
pattern $mCxExtendVar :: forall {r}.
Context -> (Name -> Dom Type -> Context -> r) -> ((# #) -> r) -> r
$bCxExtendVar :: Name -> Dom Type -> Context -> Context
CxExtendVar x a g = CxExtend (CtxVar x a) g

{-# COMPLETE CxEmpty, CxExtend #-}
{-# COMPLETE CxEmpty, CxExtendVar #-}

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)

-- | Does not raise the retrieved entry!
cxLookup :: Nat -> Context -> Maybe ContextEntry
cxLookup :: Int -> Context -> Maybe ContextEntry
cxLookup Int
i (Context [ContextEntry]
es) = [ContextEntry]
es [ContextEntry] -> Int -> Maybe ContextEntry
forall a. [a] -> Int -> Maybe a
!!! Int
i

cxDrop :: Nat -> Context -> Context
cxDrop :: Int -> Context -> Context
cxDrop Int
n (Context [ContextEntry]
es) = [ContextEntry] -> Context
forall a. [a] -> Context' a
Context ([ContextEntry] -> Context) -> [ContextEntry] -> Context
forall a b. (a -> b) -> a -> b
$ Int -> [ContextEntry] -> [ContextEntry]
forall a. Int -> [a] -> [a]
drop Int
n [ContextEntry]
es

-- | The returned list of context entries follows the context ordering
--   convention (earlier entries depend on later ones)
cxTake :: Nat -> Context -> [ContextEntry]
cxTake :: Int -> Context -> [ContextEntry]
cxTake Int
n (Context [ContextEntry]
es) = Int -> [ContextEntry] -> [ContextEntry]
forall a. Int -> [a] -> [a]
take Int
n [ContextEntry]
es

-- | Assumes the list of entries to be prepended follows the context ordering
--   convention (earlier entries depend on later ones)
cxPrepend :: [ContextEntry] -> Context -> Context
cxPrepend :: [ContextEntry] -> Context -> Context
cxPrepend [ContextEntry]
es' (Context [ContextEntry]
es) = [ContextEntry] -> Context
forall a. [a] -> Context' a
Context ([ContextEntry] -> Context) -> [ContextEntry] -> Context
forall a b. (a -> b) -> a -> b
$ [ContextEntry]
es' [ContextEntry] -> [ContextEntry] -> [ContextEntry]
forall a. [a] -> [a] -> [a]
++ [ContextEntry]
es

-- | The returned prefix follows the context ordering convention (earlier
--   entries depend on later ones)
cxSplitAt :: Nat -> Context -> ([ContextEntry], Context)
cxSplitAt :: Int -> Context -> ([ContextEntry], Context)
cxSplitAt Int
n (Context [ContextEntry]
es) = ([ContextEntry] -> Context)
-> ([ContextEntry], [ContextEntry]) -> ([ContextEntry], Context)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second [ContextEntry] -> Context
forall a. [a] -> Context' a
Context (([ContextEntry], [ContextEntry]) -> ([ContextEntry], Context))
-> ([ContextEntry], [ContextEntry]) -> ([ContextEntry], Context)
forall a b. (a -> b) -> a -> b
$ Int -> [ContextEntry] -> ([ContextEntry], [ContextEntry])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [ContextEntry]
es

cxWithIndex :: (Nat -> ContextEntry -> a) -> Context -> [a]
cxWithIndex :: forall a. (Int -> ContextEntry -> a) -> Context -> [a]
cxWithIndex Int -> ContextEntry -> a
f (Context [ContextEntry]
es) = (Int -> ContextEntry -> a) -> [Int] -> [ContextEntry] -> [a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> ContextEntry -> a
f [Int
0..] [ContextEntry]
es

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)

data TopLevelModuleNameWithSourceFile = TopLevelModuleNameWithSourceFile
  { TopLevelModuleNameWithSourceFile -> TopLevelModuleName
fileModuleName       :: TopLevelModuleName
  , TopLevelModuleNameWithSourceFile -> SourceFile
fileModuleSourceFile :: SourceFile
  }
  deriving (Int -> TopLevelModuleNameWithSourceFile -> ShowS
[TopLevelModuleNameWithSourceFile] -> ShowS
TopLevelModuleNameWithSourceFile -> String
(Int -> TopLevelModuleNameWithSourceFile -> ShowS)
-> (TopLevelModuleNameWithSourceFile -> String)
-> ([TopLevelModuleNameWithSourceFile] -> ShowS)
-> Show TopLevelModuleNameWithSourceFile
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TopLevelModuleNameWithSourceFile -> ShowS
showsPrec :: Int -> TopLevelModuleNameWithSourceFile -> ShowS
$cshow :: TopLevelModuleNameWithSourceFile -> String
show :: TopLevelModuleNameWithSourceFile -> String
$cshowList :: [TopLevelModuleNameWithSourceFile] -> ShowS
showList :: [TopLevelModuleNameWithSourceFile] -> ShowS
Show, (forall x.
 TopLevelModuleNameWithSourceFile
 -> Rep TopLevelModuleNameWithSourceFile x)
-> (forall x.
    Rep TopLevelModuleNameWithSourceFile x
    -> TopLevelModuleNameWithSourceFile)
-> Generic TopLevelModuleNameWithSourceFile
forall x.
Rep TopLevelModuleNameWithSourceFile x
-> TopLevelModuleNameWithSourceFile
forall x.
TopLevelModuleNameWithSourceFile
-> Rep TopLevelModuleNameWithSourceFile x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x.
TopLevelModuleNameWithSourceFile
-> Rep TopLevelModuleNameWithSourceFile x
from :: forall x.
TopLevelModuleNameWithSourceFile
-> Rep TopLevelModuleNameWithSourceFile x
$cto :: forall x.
Rep TopLevelModuleNameWithSourceFile x
-> TopLevelModuleNameWithSourceFile
to :: forall x.
Rep TopLevelModuleNameWithSourceFile x
-> TopLevelModuleNameWithSourceFile
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 Context
instance NFData ContextEntry
instance NFData FileDictWithBuiltins
instance NFData SourceFile
instance NFData IsBuiltinModule
instance NFData TopLevelModuleNameWithSourceFile