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

module Agda.TypeChecking.Monad.Base.Types where

import Data.Map                       ( Map )
import GHC.Generics                   ( Generic )

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

import Agda.Utils.FileName            ( AbsolutePath )

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

-- | The @Context@ is a stack of 'ContextEntry's.
type Context      = [ContextEntry]
type ContextEntry = Dom (Name, Type)

---------------------------------------------------------------------------
-- * 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
---------------------------------------------------------------------------

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

type ModuleToSource = Map TopLevelModuleName AbsolutePath

---------------------------------------------------------------------------
-- * 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...