Agda-2.8.0: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Monad.Base.Types

Description

Data structures for the type checker.

Part of Agda.TypeChecking.Monad.Base, extracted to avoid import cycles.

Synopsis

Documentation

data Comparison Source #

Constructors

CmpEq 
CmpLeq 

Instances

Instances details
Pretty Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Comparison -> Doc Source #

prettyPrec :: Int -> Comparison -> Doc Source #

prettyList :: [Comparison] -> Doc Source #

PrettyTCM Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Comparison -> m Doc Source #

EmbPrj Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Comparison -> S Word32 Source #

icod_ :: Comparison -> S Word32 Source #

value :: Word32 -> R Comparison Source #

Generic Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Associated Types

type Rep Comparison 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep Comparison = D1 ('MetaData "Comparison" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'False) (C1 ('MetaCons "CmpEq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CmpLeq" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: Comparison -> Rep Comparison x #

to :: Rep Comparison x -> Comparison #

Show Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

showsPrec :: Int -> Comparison -> ShowS #

show :: Comparison -> String #

showList :: [Comparison] -> ShowS #

NFData Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

rnf :: Comparison -> () #

Eq Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

(==) :: Comparison -> Comparison -> Bool #

(/=) :: Comparison -> Comparison -> Bool #

type Rep Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep Comparison = D1 ('MetaData "Comparison" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'False) (C1 ('MetaCons "CmpEq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CmpLeq" 'PrefixI 'False) (U1 :: Type -> Type))

data Polarity Source #

Polarity for equality and subtype checking.

Constructors

Covariant

monotone

Contravariant

antitone

Invariant

no information (mixed variance)

Nonvariant

constant

Instances

Instances details
Pretty Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Polarity -> Doc Source #

prettyPrec :: Int -> Polarity -> Doc Source #

prettyList :: [Polarity] -> Doc Source #

KillRange Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

killRange :: KillRangeT Polarity Source #

PrettyTCM Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Polarity -> m Doc Source #

EmbPrj Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Polarity -> S Word32 Source #

icod_ :: Polarity -> S Word32 Source #

value :: Word32 -> R Polarity Source #

Generic Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Associated Types

type Rep Polarity 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep Polarity = D1 ('MetaData "Polarity" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'False) ((C1 ('MetaCons "Covariant" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Contravariant" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Invariant" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Nonvariant" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: Polarity -> Rep Polarity x #

to :: Rep Polarity x -> Polarity #

Show Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

showsPrec :: Int -> Polarity -> ShowS #

show :: Polarity -> String #

showList :: [Polarity] -> ShowS #

NFData Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

rnf :: Polarity -> () #

Eq Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

(==) :: Polarity -> Polarity -> Bool #

(/=) :: Polarity -> Polarity -> Bool #

Abstract [Polarity] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> [Polarity] -> [Polarity] Source #

Apply [Polarity] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

apply :: [Polarity] -> Args -> [Polarity] Source #

applyE :: [Polarity] -> Elims -> [Polarity] Source #

type Rep Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep Polarity = D1 ('MetaData "Polarity" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'False) ((C1 ('MetaCons "Covariant" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Contravariant" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Invariant" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Nonvariant" 'PrefixI 'False) (U1 :: Type -> Type)))

data HighlightingLevel Source #

How much highlighting should be sent to the user interface?

Constructors

None 
NonInteractive 
Interactive

This includes both non-interactive highlighting and interactive highlighting of the expression that is currently being type-checked.

Instances

Instances details
Generic HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Associated Types

type Rep HighlightingLevel 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep HighlightingLevel = D1 ('MetaData "HighlightingLevel" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'False) (C1 ('MetaCons "None" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NonInteractive" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Interactive" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: HighlightingLevel -> Rep HighlightingLevel x #

to :: Rep HighlightingLevel x -> HighlightingLevel #

Read HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

readsPrec :: Int -> ReadS HighlightingLevel #

readList :: ReadS [HighlightingLevel] #

readPrec :: ReadPrec HighlightingLevel #

readListPrec :: ReadPrec [HighlightingLevel] #

Show HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

showsPrec :: Int -> HighlightingLevel -> ShowS #

show :: HighlightingLevel -> String #

showList :: [HighlightingLevel] -> ShowS #

NFData HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

rnf :: HighlightingLevel -> () #

Eq HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

(==) :: HighlightingLevel -> HighlightingLevel -> Bool #

(/=) :: HighlightingLevel -> HighlightingLevel -> Bool #

Ord HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

compare :: HighlightingLevel -> HighlightingLevel -> Ordering #

(<) :: HighlightingLevel -> HighlightingLevel -> Bool #

(<=) :: HighlightingLevel -> HighlightingLevel -> Bool #

(>) :: HighlightingLevel -> HighlightingLevel -> Bool #

(>=) :: HighlightingLevel -> HighlightingLevel -> Bool #

max :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel #

min :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel #

type Rep HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep HighlightingLevel = D1 ('MetaData "HighlightingLevel" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'False) (C1 ('MetaCons "None" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NonInteractive" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Interactive" 'PrefixI 'False) (U1 :: Type -> Type)))

data HighlightingMethod Source #

How should highlighting be sent to the user interface?

Constructors

Direct

Via stdout.

Indirect

Both via files and via stdout.

Instances

Instances details
Generic HighlightingMethod Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Associated Types

type Rep HighlightingMethod 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep HighlightingMethod = D1 ('MetaData "HighlightingMethod" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'False) (C1 ('MetaCons "Direct" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Indirect" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: HighlightingMethod -> Rep HighlightingMethod x #

to :: Rep HighlightingMethod x -> HighlightingMethod #

Read HighlightingMethod Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

readsPrec :: Int -> ReadS HighlightingMethod #

readList :: ReadS [HighlightingMethod] #

readPrec :: ReadPrec HighlightingMethod #

readListPrec :: ReadPrec [HighlightingMethod] #

Show HighlightingMethod Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

showsPrec :: Int -> HighlightingMethod -> ShowS #

show :: HighlightingMethod -> String #

showList :: [HighlightingMethod] -> ShowS #

NFData HighlightingMethod Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

rnf :: HighlightingMethod -> () #

Eq HighlightingMethod Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

(==) :: HighlightingMethod -> HighlightingMethod -> Bool #

(/=) :: HighlightingMethod -> HighlightingMethod -> Bool #

type Rep HighlightingMethod Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep HighlightingMethod = D1 ('MetaData "HighlightingMethod" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'False) (C1 ('MetaCons "Direct" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Indirect" 'PrefixI 'False) (U1 :: Type -> Type))

data NamedMeta Source #

For printing, we couple a meta with its name suggestion.

Constructors

NamedMeta 

Fields

Instances

Instances details
EncodeTCM NamedMeta Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: NamedMeta -> TCM Value Source #

Pretty NamedMeta Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: NamedMeta -> Doc Source #

prettyPrec :: Int -> NamedMeta -> Doc Source #

prettyList :: [NamedMeta] -> Doc Source #

ToConcrete NamedMeta Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs NamedMeta 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs NamedMeta = Expr

Methods

toConcrete :: MonadToConcrete m => NamedMeta -> m (ConOfAbs NamedMeta) Source #

bindToConcrete :: MonadToConcrete m => NamedMeta -> (ConOfAbs NamedMeta -> m b) -> m b Source #

PrettyTCM NamedMeta Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => NamedMeta -> m Doc Source #

type ConOfAbs NamedMeta Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

type ConOfAbs NamedMeta = Expr

newtype SourceFile Source #

SourceFiles must exist and be registered in our file dictionary.

Constructors

SourceFile 

Fields

Instances

Instances details
Generic SourceFile Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Associated Types

type Rep SourceFile 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep SourceFile = D1 ('MetaData "SourceFile" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'True) (C1 ('MetaCons "SourceFile" 'PrefixI 'True) (S1 ('MetaSel ('Just "srcFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileId)))

Methods

from :: SourceFile -> Rep SourceFile x #

to :: Rep SourceFile x -> SourceFile #

Show SourceFile Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

showsPrec :: Int -> SourceFile -> ShowS #

show :: SourceFile -> String #

showList :: [SourceFile] -> ShowS #

NFData SourceFile Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

rnf :: SourceFile -> () #

Eq SourceFile Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

(==) :: SourceFile -> SourceFile -> Bool #

(/=) :: SourceFile -> SourceFile -> Bool #

Ord SourceFile Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

compare :: SourceFile -> SourceFile -> Ordering #

(<) :: SourceFile -> SourceFile -> Bool #

(<=) :: SourceFile -> SourceFile -> Bool #

(>) :: SourceFile -> SourceFile -> Bool #

(>=) :: SourceFile -> SourceFile -> Bool #

max :: SourceFile -> SourceFile -> SourceFile #

min :: SourceFile -> SourceFile -> SourceFile #

type Rep SourceFile Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep SourceFile = D1 ('MetaData "SourceFile" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'True) (C1 ('MetaCons "SourceFile" 'PrefixI 'True) (S1 ('MetaSel ('Just "srcFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileId)))

data ModuleToSource Source #

Constructors

ModuleToSource 

Fields

Instances

Instances details
Pretty ModuleToSource Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: ModuleToSource -> Doc Source #

prettyPrec :: Int -> ModuleToSource -> Doc Source #

prettyList :: [ModuleToSource] -> Doc Source #

data IPFace' t Source #

Datatype representing a single boundary condition: x_0 = u_0, ... ,x_n = u_n ⊢ t = ?n es

Constructors

IPFace' 

Fields

Instances

Instances details
Pretty c => Pretty (IPFace' c) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

Methods

pretty :: IPFace' c -> Doc Source #

prettyPrec :: Int -> IPFace' c -> Doc Source #

prettyList :: [IPFace' c] -> Doc Source #

data IsBuiltinModule Source #

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

Constructors

IsPrimitiveModule

Very magical module, e.g. Agda.Primitive.

IsBuiltinModuleWithSafePostulates

Safe module, e.g. Agda.Builtin.Equality.

IsBuiltinModule

Any builtin module.

Instances

Instances details
Generic IsBuiltinModule Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Associated Types

type Rep IsBuiltinModule 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep IsBuiltinModule = D1 ('MetaData "IsBuiltinModule" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'False) (C1 ('MetaCons "IsPrimitiveModule" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "IsBuiltinModuleWithSafePostulates" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsBuiltinModule" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: IsBuiltinModule -> Rep IsBuiltinModule x #

to :: Rep IsBuiltinModule x -> IsBuiltinModule #

Show IsBuiltinModule Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

showsPrec :: Int -> IsBuiltinModule -> ShowS #

show :: IsBuiltinModule -> String #

showList :: [IsBuiltinModule] -> ShowS #

NFData IsBuiltinModule Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

rnf :: IsBuiltinModule -> () #

Eq IsBuiltinModule Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

(==) :: IsBuiltinModule -> IsBuiltinModule -> Bool #

(/=) :: IsBuiltinModule -> IsBuiltinModule -> Bool #

Ord IsBuiltinModule Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

compare :: IsBuiltinModule -> IsBuiltinModule -> Ordering #

(<) :: IsBuiltinModule -> IsBuiltinModule -> Bool #

(<=) :: IsBuiltinModule -> IsBuiltinModule -> Bool #

(>) :: IsBuiltinModule -> IsBuiltinModule -> Bool #

(>=) :: IsBuiltinModule -> IsBuiltinModule -> Bool #

max :: IsBuiltinModule -> IsBuiltinModule -> IsBuiltinModule #

min :: IsBuiltinModule -> IsBuiltinModule -> IsBuiltinModule #

type Rep IsBuiltinModule Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep IsBuiltinModule = D1 ('MetaData "IsBuiltinModule" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'False) (C1 ('MetaCons "IsPrimitiveModule" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "IsBuiltinModuleWithSafePostulates" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsBuiltinModule" 'PrefixI 'False) (U1 :: Type -> Type)))

type Context = [ContextEntry] Source #

The Context is a stack of ContextEntrys.

data ContextEntry Source #

Constructors

CtxVar 

Fields

Instances

Instances details
LensArgInfo ContextEntry Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

getArgInfo :: ContextEntry -> ArgInfo Source #

setArgInfo :: ArgInfo -> ContextEntry -> ContextEntry Source #

mapArgInfo :: (ArgInfo -> ArgInfo) -> ContextEntry -> ContextEntry Source #

LensCohesion ContextEntry Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

getCohesion :: ContextEntry -> Cohesion Source #

setCohesion :: Cohesion -> ContextEntry -> ContextEntry Source #

mapCohesion :: (Cohesion -> Cohesion) -> ContextEntry -> ContextEntry Source #

LensHiding ContextEntry Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

getHiding :: ContextEntry -> Hiding Source #

setHiding :: Hiding -> ContextEntry -> ContextEntry Source #

mapHiding :: (Hiding -> Hiding) -> ContextEntry -> ContextEntry Source #

LensModalPolarity ContextEntry Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

getModalPolarity :: ContextEntry -> PolarityModality Source #

setModalPolarity :: PolarityModality -> ContextEntry -> ContextEntry Source #

mapModalPolarity :: (PolarityModality -> PolarityModality) -> ContextEntry -> ContextEntry Source #

LensModality ContextEntry Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

getModality :: ContextEntry -> Modality Source #

setModality :: Modality -> ContextEntry -> ContextEntry Source #

mapModality :: (Modality -> Modality) -> ContextEntry -> ContextEntry Source #

LensOrigin ContextEntry Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

getOrigin :: ContextEntry -> Origin Source #

setOrigin :: Origin -> ContextEntry -> ContextEntry Source #

mapOrigin :: (Origin -> Origin) -> ContextEntry -> ContextEntry Source #

LensQuantity ContextEntry Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

getQuantity :: ContextEntry -> Quantity Source #

setQuantity :: Quantity -> ContextEntry -> ContextEntry Source #

mapQuantity :: (Quantity -> Quantity) -> ContextEntry -> ContextEntry Source #

LensRelevance ContextEntry Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

getRelevance :: ContextEntry -> Relevance Source #

setRelevance :: Relevance -> ContextEntry -> ContextEntry Source #

mapRelevance :: (Relevance -> Relevance) -> ContextEntry -> ContextEntry Source #

Reify ContextEntry Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo ContextEntry 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo ContextEntry = TypedBinding

Methods

reify :: MonadReify m => ContextEntry -> m (ReifiesTo ContextEntry) Source #

reifyWhen :: MonadReify m => Bool -> ContextEntry -> m (ReifiesTo ContextEntry) Source #

AddContext ContextEntry Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ContextEntry -> m a -> m a Source #

contextSize :: ContextEntry -> Nat Source #

PrettyTCM ContextEntry Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => ContextEntry -> m Doc Source #

InstantiateFull ContextEntry Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: ContextEntry -> ReduceM ContextEntry Source #

Subst ContextEntry Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg ContextEntry 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg ContextEntry = Term

Methods

applySubst :: Substitution' (SubstArg ContextEntry) -> ContextEntry -> ContextEntry Source #

Generic ContextEntry Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Associated Types

type Rep ContextEntry 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep ContextEntry = D1 ('MetaData "ContextEntry" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'False) (C1 ('MetaCons "CtxVar" 'PrefixI 'True) (S1 ('MetaSel ('Just "ceName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Just "ceType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Dom Type))))

Methods

from :: ContextEntry -> Rep ContextEntry x #

to :: Rep ContextEntry x -> ContextEntry #

Show ContextEntry Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

showsPrec :: Int -> ContextEntry -> ShowS #

show :: ContextEntry -> String #

showList :: [ContextEntry] -> ShowS #

NFData ContextEntry Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

rnf :: ContextEntry -> () #

type ReifiesTo ContextEntry Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type ReifiesTo ContextEntry = TypedBinding
type SubstArg ContextEntry Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg ContextEntry = Term
type Rep ContextEntry Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep ContextEntry = D1 ('MetaData "ContextEntry" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'False) (C1 ('MetaCons "CtxVar" 'PrefixI 'True) (S1 ('MetaSel ('Just "ceName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Just "ceType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Dom Type))))

type BuiltinModuleIds = EnumMap FileId IsBuiltinModule Source #

Collection of FileIds of primitive modules.

data FileDictWithBuiltins Source #

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

Constructors

FileDictWithBuiltins 

Fields

Instances

Instances details
GetFileId FileDictWithBuiltins Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getFileId :: FileDictWithBuiltins -> File -> FileId Source #

GetIdFile FileDictWithBuiltins Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getIdFile :: FileDictWithBuiltins -> FileId -> File Source #

Generic FileDictWithBuiltins Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Associated Types

type Rep FileDictWithBuiltins 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep FileDictWithBuiltins = D1 ('MetaData "FileDictWithBuiltins" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'False) (C1 ('MetaCons "FileDictWithBuiltins" 'PrefixI 'True) (S1 ('MetaSel ('Just "fileDictBuilder") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 FileDictBuilder) :*: (S1 ('MetaSel ('Just "builtinModuleIds") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 BuiltinModuleIds) :*: S1 ('MetaSel ('Just "primitiveLibDir") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 PrimitiveLibDir))))

Methods

from :: FileDictWithBuiltins -> Rep FileDictWithBuiltins x #

to :: Rep FileDictWithBuiltins x -> FileDictWithBuiltins #

NFData FileDictWithBuiltins Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

Methods

rnf :: FileDictWithBuiltins -> () #

type Rep FileDictWithBuiltins Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base.Types

type Rep FileDictWithBuiltins = D1 ('MetaData "FileDictWithBuiltins" "Agda.TypeChecking.Monad.Base.Types" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'False) (C1 ('MetaCons "FileDictWithBuiltins" 'PrefixI 'True) (S1 ('MetaSel ('Just "fileDictBuilder") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 FileDictBuilder) :*: (S1 ('MetaSel ('Just "builtinModuleIds") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 BuiltinModuleIds) :*: S1 ('MetaSel ('Just "primitiveLibDir") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 PrimitiveLibDir))))

type PrimitiveLibDir = AbsolutePath Source #

type ModuleToSourceId = Map TopLevelModuleName SourceFile Source #

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

lensFileDictFileDictBuilder :: Lens' FileDictWithBuiltins FileDictBuilder Source #

lensFileDictBuiltinModuleIds :: Lens' FileDictWithBuiltins BuiltinModuleIds Source #

lensFileDictPrimitiveLibDir :: Lens' FileDictWithBuiltins PrimitiveLibDir Source #

lensPairModuleToSource :: Lens' (FileDictWithBuiltins, ModuleToSourceId) ModuleToSource Source #

type TopLevelModuleName = TopLevelModuleName' Range Source #

Top-level module names (with constant-time comparisons).

data AbsolutePath Source #

Paths which are known to be absolute.

Note that the Eq and Ord instances do not check if different paths point to the same files or directories.

Instances

Instances details
Pretty AbsolutePath Source # 
Instance details

Defined in Agda.Syntax.Common.Pretty

Methods

pretty :: AbsolutePath -> Doc Source #

prettyPrec :: Int -> AbsolutePath -> Doc Source #

prettyList :: [AbsolutePath] -> Doc Source #

GetFileId FileToId Source # 
Instance details

Defined in Agda.Utils.FileId

Methods

getFileId :: FileToId -> File -> FileId Source #

GetIdFile IdToFile Source # 
Instance details

Defined in Agda.Utils.FileId

Methods

getIdFile :: IdToFile -> FileId -> File Source #

ToJSON AbsolutePath Source # 
Instance details

Defined in Agda.Interaction.JSON

Methods

toJSON :: AbsolutePath -> Value #

toEncoding :: AbsolutePath -> Encoding #

toJSONList :: [AbsolutePath] -> Value #

toEncodingList :: [AbsolutePath] -> Encoding #

omitField :: AbsolutePath -> Bool #

Read AbsolutePath Source # 
Instance details

Defined in Agda.Interaction.Base

Methods

readsPrec :: Int -> ReadS AbsolutePath #

readList :: ReadS [AbsolutePath] #

readPrec :: ReadPrec AbsolutePath #

readListPrec :: ReadPrec [AbsolutePath] #

Show AbsolutePath Source # 
Instance details

Defined in Agda.Utils.FileName

Methods

showsPrec :: Int -> AbsolutePath -> ShowS #

show :: AbsolutePath -> String #

showList :: [AbsolutePath] -> ShowS #

NFData AbsolutePath Source # 
Instance details

Defined in Agda.Utils.FileName

Methods

rnf :: AbsolutePath -> () #

Eq AbsolutePath Source # 
Instance details

Defined in Agda.Utils.FileName

Methods

(==) :: AbsolutePath -> AbsolutePath -> Bool #

(/=) :: AbsolutePath -> AbsolutePath -> Bool #

Ord AbsolutePath Source # 
Instance details

Defined in Agda.Utils.FileName

Methods

compare :: AbsolutePath -> AbsolutePath -> Ordering #

(<) :: AbsolutePath -> AbsolutePath -> Bool #

(<=) :: AbsolutePath -> AbsolutePath -> Bool #

(>) :: AbsolutePath -> AbsolutePath -> Bool #

(>=) :: AbsolutePath -> AbsolutePath -> Bool #

max :: AbsolutePath -> AbsolutePath -> AbsolutePath #

min :: AbsolutePath -> AbsolutePath -> AbsolutePath #

Hashable AbsolutePath Source # 
Instance details

Defined in Agda.Utils.FileName

Methods

hashWithSalt :: Int -> AbsolutePath -> Int #

hash :: AbsolutePath -> Int #

data FileId Source #

Unique identifier of a file.

Instances

Instances details
GetFileId FileToId Source # 
Instance details

Defined in Agda.Utils.FileId

Methods

getFileId :: FileToId -> File -> FileId Source #

GetIdFile IdToFile Source # 
Instance details

Defined in Agda.Utils.FileId

Methods

getIdFile :: IdToFile -> FileId -> File Source #

Enum FileId Source # 
Instance details

Defined in Agda.Utils.FileId

Methods

succ :: FileId -> FileId #

pred :: FileId -> FileId #

toEnum :: Int -> FileId #

fromEnum :: FileId -> Int #

enumFrom :: FileId -> [FileId] #

enumFromThen :: FileId -> FileId -> [FileId] #

enumFromTo :: FileId -> FileId -> [FileId] #

enumFromThenTo :: FileId -> FileId -> FileId -> [FileId] #

Generic FileId Source # 
Instance details

Defined in Agda.Utils.FileId

Associated Types

type Rep FileId 
Instance details

Defined in Agda.Utils.FileId

type Rep FileId = D1 ('MetaData "FileId" "Agda.Utils.FileId" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'True) (C1 ('MetaCons "FileId" 'PrefixI 'True) (S1 ('MetaSel ('Just "theFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word32)))

Methods

from :: FileId -> Rep FileId x #

to :: Rep FileId x -> FileId #

Num FileId Source # 
Instance details

Defined in Agda.Utils.FileId

Methods

(+) :: FileId -> FileId -> FileId #

(-) :: FileId -> FileId -> FileId #

(*) :: FileId -> FileId -> FileId #

negate :: FileId -> FileId #

abs :: FileId -> FileId #

signum :: FileId -> FileId #

fromInteger :: Integer -> FileId #

Show FileId Source # 
Instance details

Defined in Agda.Utils.FileId

Methods

showsPrec :: Int -> FileId -> ShowS #

show :: FileId -> String #

showList :: [FileId] -> ShowS #

NFData FileId Source # 
Instance details

Defined in Agda.Utils.FileId

Methods

rnf :: FileId -> () #

Eq FileId Source # 
Instance details

Defined in Agda.Utils.FileId

Methods

(==) :: FileId -> FileId -> Bool #

(/=) :: FileId -> FileId -> Bool #

Ord FileId Source # 
Instance details

Defined in Agda.Utils.FileId

Methods

compare :: FileId -> FileId -> Ordering #

(<) :: FileId -> FileId -> Bool #

(<=) :: FileId -> FileId -> Bool #

(>) :: FileId -> FileId -> Bool #

(>=) :: FileId -> FileId -> Bool #

max :: FileId -> FileId -> FileId #

min :: FileId -> FileId -> FileId #

type Rep FileId Source # 
Instance details

Defined in Agda.Utils.FileId

type Rep FileId = D1 ('MetaData "FileId" "Agda.Utils.FileId" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'True) (C1 ('MetaCons "FileId" 'PrefixI 'True) (S1 ('MetaSel ('Just "theFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word32)))

data FileDictBuilder Source #

Instances

Instances details
GetFileId FileDictBuilder Source # 
Instance details

Defined in Agda.Utils.FileId

Methods

getFileId :: FileDictBuilder -> File -> FileId Source #

GetIdFile FileDictBuilder Source # 
Instance details

Defined in Agda.Utils.FileId

Methods

getIdFile :: FileDictBuilder -> FileId -> File Source #

Null FileDictBuilder Source # 
Instance details

Defined in Agda.Utils.FileId

Methods

empty :: FileDictBuilder Source #

null :: FileDictBuilder -> Bool Source #

Generic FileDictBuilder Source # 
Instance details

Defined in Agda.Utils.FileId

Associated Types

type Rep FileDictBuilder 
Instance details

Defined in Agda.Utils.FileId

type Rep FileDictBuilder = D1 ('MetaData "FileDictBuilder" "Agda.Utils.FileId" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'False) (C1 ('MetaCons "FileDictBuilder" 'PrefixI 'True) (S1 ('MetaSel ('Just "nextFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileId) :*: S1 ('MetaSel ('Just "fileDict") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileDict)))

Methods

from :: FileDictBuilder -> Rep FileDictBuilder x #

to :: Rep FileDictBuilder x -> FileDictBuilder #

NFData FileDictBuilder Source # 
Instance details

Defined in Agda.Utils.FileId

Methods

rnf :: FileDictBuilder -> () #

type Rep FileDictBuilder Source # 
Instance details

Defined in Agda.Utils.FileId

type Rep FileDictBuilder = D1 ('MetaData "FileDictBuilder" "Agda.Utils.FileId" "Agda-2.8.0-FNNdyyq6AygGlTrvnmZq2W" 'False) (C1 ('MetaCons "FileDictBuilder" 'PrefixI 'True) (S1 ('MetaSel ('Just "nextFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileId) :*: S1 ('MetaSel ('Just "fileDict") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileDict)))