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

Agda.Compiler.Backend

Description

Interface for compiler backend writers.

Synopsis

Documentation

data Backend where Source #

Constructors

Backend :: Backend' opts env menv mod def -> Backend 

data Backend' opts env menv mod def Source #

Constructors

Backend' 

Fields

  • backendName :: String
     
  • backendVersion :: Maybe String

    Optional version information to be printed with --version.

  • options :: opts

    Default options

  • commandLineFlags :: [OptDescr (Flag opts)]

    Backend-specific command-line flags. Should at minimum contain a flag to enable the backend.

  • isEnabled :: opts -> Bool

    Unless the backend has been enabled, runAgda will fall back to vanilla Agda behaviour.

  • preCompile :: opts -> TCM env

    Called after type checking completes, but before compilation starts.

  • postCompile :: env -> IsMain -> Map ModuleName mod -> TCM ()

    Called after module compilation has completed. The IsMain argument is NotMain if the --no-main flag is present.

  • preModule :: env -> IsMain -> ModuleName -> FilePath -> TCM (Recompile menv mod)

    Called before compilation of each module. Gets the path to the .agdai file to allow up-to-date checking of previously written compilation results. Should return Skip m if compilation is not required.

  • postModule :: env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod

    Called after all definitions of a module have been compiled.

  • compileDef :: env -> menv -> IsMain -> Definition -> TCM def

    Compile a single definition.

  • scopeCheckingSuffices :: Bool

    True if the backend works if --only-scope-checking is used.

  • mayEraseType :: QName -> TCM Bool

    The treeless compiler may ask the Backend if elements of the given type maybe possibly erased. The answer should be False if the compilation of the type is used by a third party, e.g. in a FFI binding.

data Recompile menv mod Source #

Constructors

Recompile menv 
Skip mod 

data IsMain Source #

Constructors

IsMain 
NotMain 

Instances

Instances details
Eq IsMain Source # 
Instance details

Defined in Agda.Compiler.Common

Methods

(==) :: IsMain -> IsMain -> Bool

(/=) :: IsMain -> IsMain -> Bool

Show IsMain Source # 
Instance details

Defined in Agda.Compiler.Common

Methods

showsPrec :: Int -> IsMain -> ShowS

show :: IsMain -> String

showList :: [IsMain] -> ShowS

Semigroup IsMain Source #

Conjunctive semigroup (NotMain is absorbing).

Instance details

Defined in Agda.Compiler.Common

Methods

(<>) :: IsMain -> IsMain -> IsMain #

sconcat :: NonEmpty IsMain -> IsMain

stimes :: Integral b => b -> IsMain -> IsMain

Monoid IsMain Source # 
Instance details

Defined in Agda.Compiler.Common

type Flag opts = opts -> OptM opts Source #

f :: Flag opts is an action on the option record that results from parsing an option. f opts produces either an error message or an updated options record

toTreeless :: EvaluationStrategy -> QName -> TCM (Maybe TTerm) Source #

Converts compiled clauses to treeless syntax.

Note: Do not use any of the concrete names in the returned term for identification purposes! If you wish to do so, first apply the Agda.Compiler.Treeless.NormalizeNames transformation.

builtinNat :: String Source #

builtinSuc :: String Source #

builtinZero :: String Source #

builtinChar :: String Source #

builtinUnit :: String Source #

builtinBool :: String Source #

builtinTrue :: String Source #

builtinList :: String Source #

builtinNil :: String Source #

builtinCons :: String Source #

builtinIO :: String Source #

builtinId :: String Source #

builtinPath :: String Source #

builtinIMin :: String Source #

builtinIMax :: String Source #

builtinINeg :: String Source #

builtinIOne :: String Source #

builtinGlue :: String Source #

builtinComp :: String Source #

builtinPOr :: String Source #

builtinSub :: String Source #

builtinSize :: String Source #

builtinInf :: String Source #

builtinFlat :: String Source #

builtinRefl :: String Source #

builtinArg :: String Source #

builtinAbs :: String Source #

builtinsNoDef :: [String] Source #

Builtins that come without a definition in Agda syntax. These are giving names to Agda internal concepts which cannot be assigned an Agda type.

An example would be a user-defined name for Set.

{--}

The type of Type would be Type : Level → Setω which is not valid Agda.

sizeBuiltins :: [String] Source #

data Polarity Source #

Polarity for equality and subtype checking.

Constructors

Covariant

monotone

Contravariant

antitone

Invariant

no information (mixed variance)

Nonvariant

constant

Instances

Instances details
Eq Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

Data Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Polarity -> c Polarity

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Polarity

toConstr :: Polarity -> Constr

dataTypeOf :: Polarity -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Polarity)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Polarity)

gmapT :: (forall b. Data b => b -> b) -> Polarity -> Polarity

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Polarity -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Polarity -> r

gmapQ :: (forall d. Data d => d -> u) -> Polarity -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Polarity -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Polarity -> m Polarity

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Polarity -> m Polarity

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Polarity -> m Polarity

Show Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Polarity -> ShowS

show :: Polarity -> String

showList :: [Polarity] -> ShowS

Pretty Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Polarity -> S Int32 Source #

icod_ :: Polarity -> S Int32 Source #

value :: Int32 -> R Polarity Source #

PrettyTCM Polarity Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Abstract [Polarity] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply [Polarity] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

newtype ProblemId Source #

Constructors

ProblemId Nat 

Instances

Instances details
Enum ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Eq ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: ProblemId -> ProblemId -> Bool

(/=) :: ProblemId -> ProblemId -> Bool

Integral ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProblemId -> c ProblemId

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProblemId

toConstr :: ProblemId -> Constr

dataTypeOf :: ProblemId -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProblemId)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProblemId)

gmapT :: (forall b. Data b => b -> b) -> ProblemId -> ProblemId

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProblemId -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProblemId -> r

gmapQ :: (forall d. Data d => d -> u) -> ProblemId -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ProblemId -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId

Num ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Ord ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

compare :: ProblemId -> ProblemId -> Ordering

(<) :: ProblemId -> ProblemId -> Bool

(<=) :: ProblemId -> ProblemId -> Bool

(>) :: ProblemId -> ProblemId -> Bool

(>=) :: ProblemId -> ProblemId -> Bool

max :: ProblemId -> ProblemId -> ProblemId

min :: ProblemId -> ProblemId -> ProblemId

Real ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

toRational :: ProblemId -> Rational

Show ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> ProblemId -> ShowS

show :: ProblemId -> String

showList :: [ProblemId] -> ShowS

ToJSON ProblemId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Pretty ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasFresh ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM ProblemId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

EncodeTCM ProblemId Source # 
Instance details

Defined in Agda.Interaction.JSONTop

Monad m => MonadFresh ProblemId (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

data Comparison Source #

Constructors

CmpEq 
CmpLeq 

Instances

Instances details
Eq Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

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

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

Data Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Comparison -> c Comparison

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Comparison

toConstr :: Comparison -> Constr

dataTypeOf :: Comparison -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Comparison)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Comparison)

gmapT :: (forall b. Data b => b -> b) -> Comparison -> Comparison

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Comparison -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Comparison -> r

gmapQ :: (forall d. Data d => d -> u) -> Comparison -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Comparison -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Comparison -> m Comparison

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Comparison -> m Comparison

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Comparison -> m Comparison

Show Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Comparison -> ShowS

show :: Comparison -> String

showList :: [Comparison] -> ShowS

Pretty Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM Comparison Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

type BackendName = String Source #

type ModuleToSource = Map TopLevelModuleName AbsolutePath Source #

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

type TCM = TCMT IO Source #

Type checking monad.

newtype TCMT m a Source #

The type checking monad transformer. Adds readonly TCEnv and mutable TCState.

Constructors

TCM 

Fields

Instances

Instances details
MonadTrans TCMT Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

lift :: Monad m => m a -> TCMT m a

CatchImpossible TCM Source #

Like catchError, but resets the state completely before running the handler. This means it also loses changes to the stPersistentState.

The intended use is to catch internal errors during debug printing. In debug printing, we are not expecting state changes.

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

catchImpossible :: TCM a -> (Impossible -> TCM a) -> TCM a Source #

catchImpossibleJust :: (Impossible -> Maybe b) -> TCM a -> (b -> TCM a) -> TCM a Source #

handleImpossible :: (Impossible -> TCM a) -> TCM a -> TCM a Source #

handleImpossibleJust :: (Impossible -> Maybe b) -> (b -> TCM a) -> TCM a -> TCM a Source #

MonadFixityError ScopeM Source # 
Instance details

Defined in Agda.Syntax.Scope.Monad

MonadStConcreteNames TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadInteractionPoints TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

MonadAddContext TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> TCM a -> TCM a Source #

addLetBinding' :: Name -> Term -> Dom Type -> TCM a -> TCM a Source #

updateContext :: Substitution -> (Context -> Context) -> TCM a -> TCM a Source #

withFreshName :: Range -> ArgName -> (Name -> TCM a) -> TCM a Source #

MonadDebug TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

MonadStatistics TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Statistics

Methods

modifyCounter :: String -> (Integer -> Integer) -> TCM () Source #

MonadWarning TCM Source # 
Instance details

Defined in Agda.TypeChecking.Warnings

Methods

addWarning :: TCWarning -> TCM () Source #

MonadConstraint TCM Source # 
Instance details

Defined in Agda.TypeChecking.Constraints

MonadMetaSolver TCM Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars

MonadError TCErr TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

throwError :: TCErr -> TCM a #

catchError :: TCM a -> (TCErr -> TCM a) -> TCM a #

MonadError TCErr IM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

throwError :: TCErr -> IM a #

catchError :: IM a -> (TCErr -> IM a) -> IM a #

MonadBench Phase TCM Source #

We store benchmark statistics in an IORef. This enables benchmarking pure computation, see Agda.Benchmarking.

Instance details

Defined in Agda.TypeChecking.Monad.Base

HasFresh i => MonadFresh i TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fresh :: TCM i Source #

Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) Source #

Conversion TOM Type (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Type -> TOM (MExp O) Source #

Conversion TOM Term (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Term -> TOM (MExp O) Source #

Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) Source #

Conversion TOM [Clause] [([Pat O], MExp O)] Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: [Clause] -> TOM [([Pat O], MExp O)] Source #

Conversion TOM (Arg Pattern) (Pat O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Arg Pattern -> TOM (Pat O) Source #

Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Arg a -> TOM (Hiding, b) Source #

MonadIO m => Monad (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(>>=) :: TCMT m a -> (a -> TCMT m b) -> TCMT m b

(>>) :: TCMT m a -> TCMT m b -> TCMT m b

return :: a -> TCMT m a

MonadIO m => Functor (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fmap :: (a -> b) -> TCMT m a -> TCMT m b

(<$) :: a -> TCMT m b -> TCMT m a #

MonadIO m => MonadFail (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fail :: String -> TCMT m a

MonadIO m => Applicative (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pure :: a -> TCMT m a

(<*>) :: TCMT m (a -> b) -> TCMT m a -> TCMT m b #

liftA2 :: (a -> b -> c) -> TCMT m a -> TCMT m b -> TCMT m c

(*>) :: TCMT m a -> TCMT m b -> TCMT m b

(<*) :: TCMT m a -> TCMT m b -> TCMT m a

Semigroup (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Warnings

Methods

(<>) :: TCM Doc -> TCM Doc -> TCM Doc #

sconcat :: NonEmpty (TCM Doc) -> TCM Doc

stimes :: Integral b => b -> TCM Doc -> TCM Doc

MonadIO m => MonadIO (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftIO :: IO a -> TCMT m a

Null (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

empty :: TCM Doc Source #

null :: TCM Doc -> Bool Source #

MonadIO m => MonadTCM (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> TCMT m a Source #

MonadIO m => MonadTCState (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadIO m => MonadTCEnv (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: TCMT m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> TCMT m a -> TCMT m a Source #

MonadIO m => MonadReduce (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> TCMT m a Source #

MonadIO m => HasOptions (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadIO m => ReadTCState (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: TCMT m TCState Source #

locallyTCState :: Lens' a TCState -> (a -> a) -> TCMT m b -> TCMT m b Source #

withTCState :: (TCState -> TCState) -> TCMT m a -> TCMT m a Source #

MonadIO m => HasBuiltins (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: String -> TCMT m (Maybe (Builtin PrimFun)) Source #

TraceS [TCM Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m c -> m c Source #

TraceS (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c Source #

ReportS [TCM Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m () Source #

ReportS (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m () Source #

HasConstInfo (TCMT IO) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Signature

(IsString a, MonadIO m) => IsString (TCMT m a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fromString :: String -> TCMT m a

(MonadIO m, Semigroup a) => Semigroup (TCMT m a) Source #

Strict (non-shortcut) semigroup.

Note that there might be a lazy alternative, e.g., for TCM All we might want and2M as concatenation, to shortcut conjunction in case we already have False.

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(<>) :: TCMT m a -> TCMT m a -> TCMT m a #

sconcat :: NonEmpty (TCMT m a) -> TCMT m a

stimes :: Integral b => b -> TCMT m a -> TCMT m a

(MonadIO m, Semigroup a, Monoid a) => Monoid (TCMT m a) Source #

Strict (non-shortcut) monoid.

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

mempty :: TCMT m a

mappend :: TCMT m a -> TCMT m a -> TCMT m a

mconcat :: [TCMT m a] -> TCMT m a

data TCState Source #

Constructors

TCSt 

Fields

Instances

Instances details
Show TCState Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> TCState -> ShowS

show :: TCState -> String

showList :: [TCState] -> ShowS

LensPersistentVerbosity TCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensIncludePaths TCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensSafeMode TCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensCommandLineOptions TCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensVerbosity TCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensPragmaOptions TCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

data TCEnv Source #

Constructors

TCEnv 

Fields

Instances

Instances details
Data TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TCEnv -> c TCEnv

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TCEnv

toConstr :: TCEnv -> Constr

dataTypeOf :: TCEnv -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TCEnv)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TCEnv)

gmapT :: (forall b. Data b => b -> b) -> TCEnv -> TCEnv

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TCEnv -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TCEnv -> r

gmapQ :: (forall d. Data d => d -> u) -> TCEnv -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> TCEnv -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TCEnv -> m TCEnv

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TCEnv -> m TCEnv

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TCEnv -> m TCEnv

LensIsAbstract TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensRelevance TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensQuantity TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensModality TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensTCEnv TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

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
Eq HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HighlightingLevel -> c HighlightingLevel

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HighlightingLevel

toConstr :: HighlightingLevel -> Constr

dataTypeOf :: HighlightingLevel -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HighlightingLevel)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HighlightingLevel)

gmapT :: (forall b. Data b => b -> b) -> HighlightingLevel -> HighlightingLevel

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HighlightingLevel -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HighlightingLevel -> r

gmapQ :: (forall d. Data d => d -> u) -> HighlightingLevel -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> HighlightingLevel -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> HighlightingLevel -> m HighlightingLevel

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HighlightingLevel -> m HighlightingLevel

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HighlightingLevel -> m HighlightingLevel

Ord HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Read HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show HighlightingLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> HighlightingLevel -> ShowS

show :: HighlightingLevel -> String

showList :: [HighlightingLevel] -> ShowS

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
Eq HighlightingMethod Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data HighlightingMethod Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HighlightingMethod -> c HighlightingMethod

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HighlightingMethod

toConstr :: HighlightingMethod -> Constr

dataTypeOf :: HighlightingMethod -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HighlightingMethod)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HighlightingMethod)

gmapT :: (forall b. Data b => b -> b) -> HighlightingMethod -> HighlightingMethod

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HighlightingMethod -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HighlightingMethod -> r

gmapQ :: (forall d. Data d => d -> u) -> HighlightingMethod -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> HighlightingMethod -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> HighlightingMethod -> m HighlightingMethod

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HighlightingMethod -> m HighlightingMethod

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HighlightingMethod -> m HighlightingMethod

Read HighlightingMethod Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show HighlightingMethod Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> HighlightingMethod -> ShowS

show :: HighlightingMethod -> String

showList :: [HighlightingMethod] -> ShowS

data NamedMeta Source #

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

data TCWarning Source #

Constructors

TCWarning 

Fields

Instances

Instances details
Eq TCWarning Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: TCWarning -> TCWarning -> Bool

(/=) :: TCWarning -> TCWarning -> Bool

Show TCWarning Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> TCWarning -> ShowS

show :: TCWarning -> String

showList :: [TCWarning] -> ShowS

HasRange TCWarning Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj TCWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: TCWarning -> S Int32 Source #

icod_ :: TCWarning -> S Int32 Source #

value :: Int32 -> R TCWarning Source #

PrettyTCM TCWarning Source # 
Instance details

Defined in Agda.TypeChecking.Pretty.Warning

data TCErr Source #

Type-checking errors.

Constructors

TypeError 

Fields

Exception Range Doc 
IOException TCState Range IOException

The first argument is the state in which the error was raised.

PatternErr

The exception which is usually caught. Raised for pattern violations during unification (assignV) but also in other situations where we want to backtrack.

Instances

Instances details
Show TCErr Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> TCErr -> ShowS

show :: TCErr -> String

showList :: [TCErr] -> ShowS

Exception TCErr Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Error TCErr Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

noMsg :: TCErr Source #

strMsg :: String -> TCErr Source #

HasRange TCErr Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: TCErr -> Range Source #

PrettyTCM TCErr Source # 
Instance details

Defined in Agda.TypeChecking.Errors

Methods

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

MonadError TCErr TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

throwError :: TCErr -> TCM a #

catchError :: TCM a -> (TCErr -> TCM a) -> TCM a #

MonadError TCErr IM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

throwError :: TCErr -> IM a #

catchError :: IM a -> (TCErr -> IM a) -> IM a #

MonadError TCErr TerM Source # 
Instance details

Defined in Agda.Termination.Monad

Methods

throwError :: TCErr -> TerM a #

catchError :: TerM a -> (TCErr -> TerM a) -> TerM a #

Monad m => MonadError TCErr (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

data Warning Source #

A non-fatal error is an error which does not prevent us from checking the document further and interacting with the user.

Constructors

NicifierIssue DeclarationWarning 
TerminationIssue [TerminationError] 
UnreachableClauses QName [Range]

`UnreachableClauses f rs` means that the clauses in f whose ranges are rs are unreachable

CoverageIssue QName [(Telescope, [NamedArg DeBruijnPattern])]

`CoverageIssue f pss` means that pss are not covered in f

CoverageNoExactSplit QName [Clause] 
NotStrictlyPositive QName (Seq OccursWhere) 
UnsolvedMetaVariables [Range]

Do not use directly with warning

UnsolvedInteractionMetas [Range]

Do not use directly with warning

UnsolvedConstraints Constraints

Do not use directly with warning

CantGeneralizeOverSorts [MetaId] 
AbsurdPatternRequiresNoRHS [NamedArg DeBruijnPattern] 
OldBuiltin String String

In `OldBuiltin old new`, the BUILTIN old has been replaced by new

EmptyRewritePragma

If the user wrote just {-# REWRITE #-}.

IllformedAsClause String

If the user wrote something other than an unqualified name in the as clause of an import statement. The String gives optionally extra explanation.

ClashesViaRenaming NameOrModule [Name]

If a renaming import directive introduces a name or module name clash in the exported names of a module. (See issue #4154.)

UselessPublic

If the user opens a module public before the module header. (See issue #2377.)

UselessInline QName 
WrongInstanceDeclaration 
InstanceWithExplicitArg QName

An instance was declared with an implicit argument, which means it will never actually be considered by instance search.

InstanceNoOutputTypeName Doc

The type of an instance argument doesn't end in a named or variable type, so it will never be considered by instance search.

InstanceArgWithExplicitArg Doc

As InstanceWithExplicitArg, but for local bindings rather than top-level instances.

InversionDepthReached QName

The --inversion-max-depth was reached. Generic warnings for one-off things

GenericWarning Doc

Harmless generic warning (not an error)

GenericNonFatalError Doc

Generic error which doesn't abort proceedings (not a warning) Safe flag errors

SafeFlagPostulate Name 
SafeFlagPragma [String]

Unsafe OPTIONS.

SafeFlagNonTerminating 
SafeFlagTerminating 
SafeFlagWithoutKFlagPrimEraseEquality 
WithoutKFlagPrimEraseEquality 
SafeFlagNoPositivityCheck 
SafeFlagPolarity 
SafeFlagNoUniverseCheck 
SafeFlagNoCoverageCheck 
SafeFlagInjective 
SafeFlagEta

ETA pragma is unsafe.

ParseWarning ParseWarning 
LibraryWarning LibWarning 
DeprecationWarning String String String

`DeprecationWarning old new version`: old is deprecated, use new instead. This will be an error in Agda version.

UserWarning String

User-defined warning (e.g. to mention that a name is deprecated)

FixityInRenamingModule (NonEmpty Range)

Fixity of modules cannot be changed via renaming (since modules have no fixity).

ModuleDoesntExport QName [ImportedName]

Some imported names are not actually exported by the source module

InfectiveImport String ModuleName

Importing a file using an infective option into one which doesn't

CoInfectiveImport String ModuleName

Importing a file not using a coinfective option from one which does

RewriteNonConfluent Term Term Term Doc

Confluence checker found critical pair and equality checking resulted in a type error

RewriteMaybeNonConfluent Term Term [Doc]

Confluence checker got stuck on computing overlap between two rewrite rules

PragmaCompileErased BackendName QName

COMPILE directive for an erased symbol

NotInScopeW [QName]

Out of scope error we can recover from

Instances

Instances details
Data Warning Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Warning -> c Warning

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Warning

toConstr :: Warning -> Constr

dataTypeOf :: Warning -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Warning)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Warning)

gmapT :: (forall b. Data b => b -> b) -> Warning -> Warning

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Warning -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Warning -> r

gmapQ :: (forall d. Data d => d -> u) -> Warning -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Warning -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Warning -> m Warning

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Warning -> m Warning

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Warning -> m Warning

Show Warning Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Warning -> ShowS

show :: Warning -> String

showList :: [Warning] -> ShowS

EmbPrj Warning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: Warning -> S Int32 Source #

icod_ :: Warning -> S Int32 Source #

value :: Int32 -> R Warning Source #

PrettyTCM Warning Source # 
Instance details

Defined in Agda.TypeChecking.Pretty.Warning

Methods

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

type VerboseLevel = Int Source #

type VerboseKey = String Source #

class (Applicative tcm, MonadIO tcm, MonadTCEnv tcm, MonadTCState tcm, HasOptions tcm) => MonadTCM tcm where Source #

Embedding a TCM computation.

Minimal complete definition

Nothing

Methods

liftTCM :: TCM a -> tcm a Source #

default liftTCM :: (MonadTCM m, MonadTrans t, tcm ~ t m) => TCM a -> tcm a Source #

Instances

Instances details
MonadTCM TerM Source # 
Instance details

Defined in Agda.Termination.Monad

Methods

liftTCM :: TCM a -> TerM a Source #

MonadTCM tcm => MonadTCM (MaybeT tcm) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> MaybeT tcm a Source #

MonadTCM tcm => MonadTCM (ListT tcm) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> ListT tcm a Source #

MonadIO m => MonadTCM (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> TCMT m a Source #

MonadTCM tcm => MonadTCM (ChangeT tcm) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> ChangeT tcm a Source #

MonadTCM m => MonadTCM (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

Methods

liftTCM :: TCM a -> NamesT m a Source #

MonadTCM tcm => MonadTCM (ExceptT err tcm) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> ExceptT err tcm a Source #

MonadTCM tcm => MonadTCM (IdentityT tcm) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> IdentityT tcm a Source #

MonadTCM tcm => MonadTCM (ReaderT r tcm) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> ReaderT r tcm a Source #

MonadTCM tcm => MonadTCM (StateT s tcm) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> StateT s tcm a Source #

(Monoid w, MonadTCM tcm) => MonadTCM (WriterT w tcm) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftTCM :: TCM a -> WriterT w tcm a Source #

type IM = TCMT (InputT IO) Source #

Interaction monad.

class Monad m => MonadTCState m where Source #

MonadTCState made into its own dedicated service class. This allows us to use MonadState for StateT extensions of TCM.

Minimal complete definition

getTC, (putTC | modifyTC)

Methods

getTC :: m TCState Source #

putTC :: TCState -> m () Source #

modifyTC :: (TCState -> TCState) -> m () Source #

Instances

Instances details
MonadTCState TerM Source # 
Instance details

Defined in Agda.Termination.Monad

MonadTCState m => MonadTCState (MaybeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTC :: MaybeT m TCState Source #

putTC :: TCState -> MaybeT m () Source #

modifyTC :: (TCState -> TCState) -> MaybeT m () Source #

MonadTCState m => MonadTCState (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadIO m => MonadTCState (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadTCState m => MonadTCState (ChangeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadTCState m => MonadTCState (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

MonadTCState m => MonadTCState (ExceptT err m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTC :: ExceptT err m TCState Source #

putTC :: TCState -> ExceptT err m () Source #

modifyTC :: (TCState -> TCState) -> ExceptT err m () Source #

MonadTCState m => MonadTCState (IdentityT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTC :: IdentityT m TCState Source #

putTC :: TCState -> IdentityT m () Source #

modifyTC :: (TCState -> TCState) -> IdentityT m () Source #

MonadTCState m => MonadTCState (ReaderT r m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTC :: ReaderT r m TCState Source #

putTC :: TCState -> ReaderT r m () Source #

modifyTC :: (TCState -> TCState) -> ReaderT r m () Source #

MonadTCState m => MonadTCState (StateT s m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTC :: StateT s m TCState Source #

putTC :: TCState -> StateT s m () Source #

modifyTC :: (TCState -> TCState) -> StateT s m () Source #

(Monoid w, MonadTCState m) => MonadTCState (WriterT w m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTC :: WriterT w m TCState Source #

putTC :: TCState -> WriterT w m () Source #

modifyTC :: (TCState -> TCState) -> WriterT w m () Source #

class Monad m => MonadTCEnv m where Source #

MonadTCEnv made into its own dedicated service class. This allows us to use MonadReader for ReaderT extensions of TCM.

Methods

askTC :: m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> m a -> m a Source #

Instances

Instances details
MonadTCEnv ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadTCEnv AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

MonadTCEnv TerM Source # 
Instance details

Defined in Agda.Termination.Monad

Methods

askTC :: TerM TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> TerM a -> TerM a Source #

MonadTCEnv m => MonadTCEnv (MaybeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: MaybeT m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> MaybeT m a -> MaybeT m a Source #

MonadTCEnv m => MonadTCEnv (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: ListT m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> ListT m a -> ListT m a Source #

MonadIO m => MonadTCEnv (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: TCMT m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> TCMT m a -> TCMT m a Source #

MonadTCEnv m => MonadTCEnv (ChangeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: ChangeT m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> ChangeT m a -> ChangeT m a Source #

MonadTCEnv m => MonadTCEnv (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

Methods

askTC :: NamesT m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> NamesT m a -> NamesT m a Source #

MonadTCEnv m => MonadTCEnv (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

MonadTCEnv m => MonadTCEnv (ExceptT err m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: ExceptT err m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> ExceptT err m a -> ExceptT err m a Source #

MonadTCEnv m => MonadTCEnv (IdentityT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: IdentityT m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> IdentityT m a -> IdentityT m a Source #

MonadTCEnv m => MonadTCEnv (ReaderT r m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: ReaderT r m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> ReaderT r m a -> ReaderT r m a Source #

MonadTCEnv m => MonadTCEnv (StateT s m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: StateT s m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> StateT s m a -> StateT s m a Source #

(Monoid w, MonadTCEnv m) => MonadTCEnv (WriterT w m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

askTC :: WriterT w m TCEnv Source #

localTC :: (TCEnv -> TCEnv) -> WriterT w m a -> WriterT w m a Source #

class (Applicative m, MonadTCEnv m, ReadTCState m, HasOptions m) => MonadReduce m where Source #

Methods

liftReduce :: ReduceM a -> m a Source #

Instances

Instances details
MonadReduce ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> ReduceM a Source #

MonadReduce TerM Source # 
Instance details

Defined in Agda.Termination.Monad

Methods

liftReduce :: ReduceM a -> TerM a Source #

MonadReduce m => MonadReduce (MaybeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> MaybeT m a Source #

MonadReduce m => MonadReduce (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> ListT m a Source #

MonadIO m => MonadReduce (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> TCMT m a Source #

MonadReduce m => MonadReduce (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

Methods

liftReduce :: ReduceM a -> NamesT m a Source #

MonadReduce m => MonadReduce (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

MonadReduce m => MonadReduce (ExceptT err m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> ExceptT err m a Source #

MonadReduce m => MonadReduce (ReaderT r m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> ReaderT r m a Source #

MonadReduce m => MonadReduce (StateT w m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> StateT w m a Source #

(Monoid w, MonadReduce m) => MonadReduce (WriterT w m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> WriterT w m a Source #

newtype ReduceM a Source #

Constructors

ReduceM 

Fields

Instances

Instances details
Monad ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(>>=) :: ReduceM a -> (a -> ReduceM b) -> ReduceM b

(>>) :: ReduceM a -> ReduceM b -> ReduceM b

return :: a -> ReduceM a

Functor ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fmap :: (a -> b) -> ReduceM a -> ReduceM b

(<$) :: a -> ReduceM b -> ReduceM a #

MonadFail ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fail :: String -> ReduceM a

Applicative ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pure :: a -> ReduceM a

(<*>) :: ReduceM (a -> b) -> ReduceM a -> ReduceM b #

liftA2 :: (a -> b -> c) -> ReduceM a -> ReduceM b -> ReduceM c

(*>) :: ReduceM a -> ReduceM b -> ReduceM b

(<*) :: ReduceM a -> ReduceM b -> ReduceM a

MonadTCEnv ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadReduce ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

liftReduce :: ReduceM a -> ReduceM a Source #

HasOptions ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

ReadTCState ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadAddContext ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Reduce.Monad

HasBuiltins ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Reduce.Monad

Methods

getBuiltinThing :: String -> ReduceM (Maybe (Builtin PrimFun)) Source #

MonadDebug ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Reduce.Monad

HasConstInfo ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Reduce.Monad

data ReduceEnv Source #

Environment of the reduce monad.

Constructors

ReduceEnv 

Fields

class (Functor m, Applicative m, Monad m) => HasOptions m where Source #

Minimal complete definition

Nothing

Methods

pragmaOptions :: m PragmaOptions Source #

Returns the pragma options which are currently in effect.

default pragmaOptions :: (HasOptions n, MonadTrans t, m ~ t n) => m PragmaOptions Source #

commandLineOptions :: m CommandLineOptions Source #

Returns the command line options which are currently in effect.

default commandLineOptions :: (HasOptions n, MonadTrans t, m ~ t n) => m CommandLineOptions Source #

Instances

Instances details
HasOptions ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasOptions AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

HasOptions TerM Source # 
Instance details

Defined in Agda.Termination.Monad

HasOptions m => HasOptions (MaybeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasOptions m => HasOptions (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadIO m => HasOptions (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasOptions m => HasOptions (ChangeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasOptions m => HasOptions (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

HasOptions m => HasOptions (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

HasOptions m => HasOptions (ExceptT e m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasOptions m => HasOptions (IdentityT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasOptions m => HasOptions (ReaderT r m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasOptions m => HasOptions (StateT s m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

(HasOptions m, Monoid w) => HasOptions (WriterT w m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

data LHSOrPatSyn Source #

Distinguish error message when parsing lhs or pattern synonym, resp.

Constructors

IsLHS 
IsPatSyn 

Instances

Instances details
Eq LHSOrPatSyn Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: LHSOrPatSyn -> LHSOrPatSyn -> Bool

(/=) :: LHSOrPatSyn -> LHSOrPatSyn -> Bool

Show LHSOrPatSyn Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> LHSOrPatSyn -> ShowS

show :: LHSOrPatSyn -> String

showList :: [LHSOrPatSyn] -> ShowS

data TypeError Source #

Constructors

InternalError String 
NotImplemented String 
NotSupported String 
CompilationError String 
PropMustBeSingleton 
DataMustEndInSort Term 
ShouldEndInApplicationOfTheDatatype Type

The target of a constructor isn't an application of its datatype. The Type records what it does target.

ShouldBeAppliedToTheDatatypeParameters Term Term

The target of a constructor isn't its datatype applied to something that isn't the parameters. First term is the correct target and the second term is the actual target.

ShouldBeApplicationOf Type QName

Expected a type to be an application of a particular datatype.

ConstructorPatternInWrongDatatype QName QName

constructor, datatype

CantResolveOverloadedConstructorsTargetingSameDatatype QName [QName]

Datatype, constructors.

DoesNotConstructAnElementOf QName Type

constructor, type

WrongHidingInLHS

The left hand side of a function definition has a hidden argument where a non-hidden was expected.

WrongHidingInLambda Type

Expected a non-hidden function and found a hidden lambda.

WrongHidingInApplication Type

A function is applied to a hidden argument where a non-hidden was expected.

WrongNamedArgument (NamedArg Expr) [NamedName]

A function is applied to a hidden named argument it does not have. The list contains names of possible hidden arguments at this point.

WrongIrrelevanceInLambda

Wrong user-given relevance annotation in lambda.

WrongQuantityInLambda

Wrong user-given quantity annotation in lambda.

WrongCohesionInLambda

Wrong user-given cohesion annotation in lambda.

QuantityMismatch Quantity Quantity

The given quantity does not correspond to the expected quantity.

HidingMismatch Hiding Hiding

The given hiding does not correspond to the expected hiding.

RelevanceMismatch Relevance Relevance

The given relevance does not correspond to the expected relevane.

UninstantiatedDotPattern Expr 
ForcedConstructorNotInstantiated Pattern 
IlltypedPattern Pattern Type 
IllformedProjectionPattern Pattern 
CannotEliminateWithPattern (NamedArg Pattern) Type 
WrongNumberOfConstructorArguments QName Nat Nat 
ShouldBeEmpty Type [DeBruijnPattern] 
ShouldBeASort Type

The given type should have been a sort.

ShouldBePi Type

The given type should have been a pi.

ShouldBePath Type 
ShouldBeRecordType Type 
ShouldBeRecordPattern DeBruijnPattern 
NotAProjectionPattern (NamedArg Pattern) 
NotAProperTerm 
InvalidTypeSort Sort

This sort is not a type expression.

InvalidType Term

This term is not a type expression.

FunctionTypeInSizeUniv Term

This term, a function type constructor, lives in SizeUniv, which is not allowed.

SplitOnIrrelevant (Dom Type) 
SplitOnUnusableCohesion (Dom Type) 
SplitOnNonVariable Term Type 
DefinitionIsIrrelevant QName 
DefinitionIsErased QName 
VariableIsIrrelevant Name 
VariableIsErased Name 
VariableIsOfUnusableCohesion Name Cohesion 
UnequalLevel Comparison Level Level 
UnequalTerms Comparison Term Term CompareAs 
UnequalTypes Comparison Type Type 
UnequalRelevance Comparison Term Term

The two function types have different relevance.

UnequalQuantity Comparison Term Term

The two function types have different relevance.

UnequalCohesion Comparison Term Term

The two function types have different cohesion.

UnequalHiding Term Term

The two function types have different hiding.

UnequalSorts Sort Sort 
UnequalBecauseOfUniverseConflict Comparison Term Term 
NotLeqSort Sort Sort 
MetaCannotDependOn MetaId Nat

The arguments are the meta variable and the parameter that it wants to depend on.

MetaOccursInItself MetaId 
MetaIrrelevantSolution MetaId Term 
MetaErasedSolution MetaId Term 
GenericError String 
GenericDocError Doc 
BuiltinMustBeConstructor String Expr 
NoSuchBuiltinName String 
DuplicateBuiltinBinding String Term Term 
NoBindingForBuiltin String 
NoSuchPrimitiveFunction String 
DuplicatePrimitiveBinding String QName QName 
ShadowedModule Name [ModuleName] 
BuiltinInParameterisedModule String 
IllegalLetInTelescope TypedBinding 
IllegalPatternInTelescope Binder 
NoRHSRequiresAbsurdPattern [NamedArg Pattern] 
TooManyFields QName [Name] [Name]

Record type, fields not supplied by user, non-fields not supplied.

DuplicateFields [Name] 
DuplicateConstructors [Name] 
WithOnFreeVariable Expr Term 
UnexpectedWithPatterns [Pattern] 
WithClausePatternMismatch Pattern (NamedArg DeBruijnPattern) 
FieldOutsideRecord 
ModuleArityMismatch ModuleName Telescope [NamedArg Expr] 
GeneralizeCyclicDependency 
GeneralizeUnsolvedMeta 
SplitError SplitError 
ImpossibleConstructor QName NegativeUnification 
TooManyPolarities QName Int 
LocalVsImportedModuleClash ModuleName 
SolvedButOpenHoles

Some interaction points (holes) have not been filled by user. There are not UnsolvedMetas since unification solved them. This is an error, since interaction points are never filled without user interaction.

CyclicModuleDependency [TopLevelModuleName] 
FileNotFound TopLevelModuleName [AbsolutePath] 
OverlappingProjects AbsolutePath TopLevelModuleName TopLevelModuleName 
AmbiguousTopLevelModuleName TopLevelModuleName [AbsolutePath] 
ModuleNameUnexpected TopLevelModuleName TopLevelModuleName

Found module name, expected module name.

ModuleNameDoesntMatchFileName TopLevelModuleName [AbsolutePath] 
ClashingFileNamesFor ModuleName [AbsolutePath] 
ModuleDefinedInOtherFile TopLevelModuleName AbsolutePath AbsolutePath

Module name, file from which it was loaded, file which the include path says contains the module. Scope errors

BothWithAndRHS 
AbstractConstructorNotInScope QName 
NotInScope [QName] 
NoSuchModule QName 
AmbiguousName QName (NonEmpty QName) 
AmbiguousModule QName (NonEmpty ModuleName) 
ClashingDefinition QName QName 
ClashingModule ModuleName ModuleName 
ClashingImport Name QName 
ClashingModuleImport Name ModuleName 
PatternShadowsConstructor Name QName 
DuplicateImports QName [ImportedName] 
InvalidPattern Pattern 
RepeatedVariablesInPattern [Name] 
GeneralizeNotSupportedHere QName 
MultipleFixityDecls [(Name, [Fixity'])] 
MultiplePolarityPragmas [Name] 
NotAModuleExpr Expr

The expr was used in the right hand side of an implicit module definition, but it wasn't of the form m Delta.

NotAnExpression Expr 
NotAValidLetBinding NiceDeclaration 
NotValidBeforeField NiceDeclaration 
NothingAppliedToHiddenArg Expr 
NothingAppliedToInstanceArg Expr 
BadArgumentsToPatternSynonym AmbiguousQName 
TooFewArgumentsToPatternSynonym AmbiguousQName 
CannotResolveAmbiguousPatternSynonym (NonEmpty (QName, PatternSynDefn)) 
UnusedVariableInPatternSynonym 
NoParseForApplication [Expr] 
AmbiguousParseForApplication [Expr] [Expr] 
NoParseForLHS LHSOrPatSyn Pattern 
AmbiguousParseForLHS LHSOrPatSyn Pattern [Pattern] 
OperatorInformation [NotationSection] TypeError 
InstanceNoCandidate Type [(Term, TCErr)] 
UnquoteFailed UnquoteError 
DeBruijnIndexOutOfScope Nat Telescope [Name] 
NeedOptionCopatterns 
NeedOptionRewriting 
NeedOptionProp 
NonFatalErrors [TCWarning] 
InstanceSearchDepthExhausted Term Type Int 
TriedToCopyConstrainedPrim QName 

Instances

Instances details
Show TypeError Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> TypeError -> ShowS

show :: TypeError -> String

showList :: [TypeError] -> ShowS

PrettyTCM TypeError Source # 
Instance details

Defined in Agda.TypeChecking.Errors

data UnquoteError Source #

Constructors

BadVisibility String (Arg Term) 
ConInsteadOfDef QName String String 
DefInsteadOfCon QName String String 
NonCanonical String Term 
BlockedOnMeta TCState MetaId 
UnquotePanic String 

Instances

Instances details
Show UnquoteError Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> UnquoteError -> ShowS

show :: UnquoteError -> String

showList :: [UnquoteError] -> ShowS

data UnificationFailure Source #

Constructors

UnifyIndicesNotVars Telescope Type Term Term Args

Failed to apply injectivity to constructor of indexed datatype

UnifyRecursiveEq Telescope Type Int Term

Can't solve equation because variable occurs in (type of) lhs

UnifyReflexiveEq Telescope Type Term

Can't solve reflexive equation because --without-K is enabled

UnifyUnusableModality Telescope Type Int Term Modality

Can't solve equation because solution modality is less "usable"

Instances

Instances details
Show UnificationFailure Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> UnificationFailure -> ShowS

show :: UnificationFailure -> String

showList :: [UnificationFailure] -> ShowS

PrettyTCM UnificationFailure Source # 
Instance details

Defined in Agda.TypeChecking.Errors

data SplitError Source #

Error when splitting a pattern variable into possible constructor patterns.

Constructors

NotADatatype (Closure Type)

Neither data type nor record.

IrrelevantDatatype (Closure Type)

Data type, but in irrelevant position.

ErasedDatatype Bool (Closure Type)

Data type, but in erased position. If the boolean is True, then the reason for the error is that the K rule is turned off.

CoinductiveDatatype (Closure Type)

Split on codata not allowed. UNUSED, but keep! -- | NoRecordConstructor Type -- ^ record type, but no constructor

UnificationStuck 

Fields

CosplitCatchall

Copattern split with a catchall

CosplitNoTarget

We do not know the target type of the clause.

CosplitNoRecordType (Closure Type)

Target type is not a record type.

CannotCreateMissingClause QName (Telescope, [NamedArg DeBruijnPattern]) Doc (Closure (Abs Type)) 
GenericSplitError String 

Instances

Instances details
Show SplitError Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> SplitError -> ShowS

show :: SplitError -> String

showList :: [SplitError] -> ShowS

PrettyTCM SplitError Source # 
Instance details

Defined in Agda.TypeChecking.Errors

data TerminationError Source #

Information about a mutual block which did not pass the termination checker.

Constructors

TerminationError 

Fields

Instances

Instances details
Data TerminationError Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TerminationError -> c TerminationError

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TerminationError

toConstr :: TerminationError -> Constr

dataTypeOf :: TerminationError -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TerminationError)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TerminationError)

gmapT :: (forall b. Data b => b -> b) -> TerminationError -> TerminationError

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TerminationError -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TerminationError -> r

gmapQ :: (forall d. Data d => d -> u) -> TerminationError -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> TerminationError -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TerminationError -> m TerminationError

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TerminationError -> m TerminationError

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TerminationError -> m TerminationError

Show TerminationError Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> TerminationError -> ShowS

show :: TerminationError -> String

showList :: [TerminationError] -> ShowS

data CallInfo Source #

Information about a call.

Constructors

CallInfo 

Fields

Instances

Instances details
Data CallInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CallInfo -> c CallInfo

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CallInfo

toConstr :: CallInfo -> Constr

dataTypeOf :: CallInfo -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CallInfo)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CallInfo)

gmapT :: (forall b. Data b => b -> b) -> CallInfo -> CallInfo

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CallInfo -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CallInfo -> r

gmapQ :: (forall d. Data d => d -> u) -> CallInfo -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> CallInfo -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> CallInfo -> m CallInfo

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CallInfo -> m CallInfo

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CallInfo -> m CallInfo

Show CallInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> CallInfo -> ShowS

show :: CallInfo -> String

showList :: [CallInfo] -> ShowS

Pretty CallInfo Source #

We only show the name of the callee.

Instance details

Defined in Agda.TypeChecking.Monad.Base

AllNames CallInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

allNames :: CallInfo -> Seq QName Source #

PrettyTCM CallInfo Source # 
Instance details

Defined in Agda.TypeChecking.Pretty.Call

data Candidate Source #

A candidate solution for an instance meta is a term with its type. It may be the case that the candidate is not fully applied yet or of the wrong type, hence the need for the type.

Instances

Instances details
Eq Candidate 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

(==) :: Candidate -> Candidate -> Bool

(/=) :: Candidate -> Candidate -> Bool

Data Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Candidate -> c Candidate

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Candidate

toConstr :: Candidate -> Constr

dataTypeOf :: Candidate -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Candidate)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Candidate)

gmapT :: (forall b. Data b => b -> b) -> Candidate -> Candidate

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Candidate -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Candidate -> r

gmapQ :: (forall d. Data d => d -> u) -> Candidate -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Candidate -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Candidate -> m Candidate

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Candidate -> m Candidate

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Candidate -> m Candidate

Show Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Candidate -> ShowS

show :: Candidate -> String

showList :: [Candidate] -> ShowS

Free Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

freeVars' :: IsVarSet a c => Candidate -> FreeM a c Source #

InstantiateFull Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Subst Term Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

data ExpandHidden Source #

Constructors

ExpandLast

Add implicit arguments in the end until type is no longer hidden Pi.

DontExpandLast

Do not append implicit arguments.

ReallyDontExpandLast

Makes doExpandLast have no effect. Used to avoid implicit insertion of arguments to metavariables.

Instances

Instances details
Eq ExpandHidden Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: ExpandHidden -> ExpandHidden -> Bool

(/=) :: ExpandHidden -> ExpandHidden -> Bool

Data ExpandHidden Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ExpandHidden -> c ExpandHidden

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ExpandHidden

toConstr :: ExpandHidden -> Constr

dataTypeOf :: ExpandHidden -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ExpandHidden)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExpandHidden)

gmapT :: (forall b. Data b => b -> b) -> ExpandHidden -> ExpandHidden

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ExpandHidden -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ExpandHidden -> r

gmapQ :: (forall d. Data d => d -> u) -> ExpandHidden -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ExpandHidden -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ExpandHidden -> m ExpandHidden

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ExpandHidden -> m ExpandHidden

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ExpandHidden -> m ExpandHidden

data AbstractMode Source #

Constructors

AbstractMode

Abstract things in the current module can be accessed.

ConcreteMode

No abstract things can be accessed.

IgnoreAbstractMode

All abstract things can be accessed.

Instances

Instances details
Eq AbstractMode Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: AbstractMode -> AbstractMode -> Bool

(/=) :: AbstractMode -> AbstractMode -> Bool

Data AbstractMode Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AbstractMode -> c AbstractMode

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AbstractMode

toConstr :: AbstractMode -> Constr

dataTypeOf :: AbstractMode -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AbstractMode)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AbstractMode)

gmapT :: (forall b. Data b => b -> b) -> AbstractMode -> AbstractMode

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AbstractMode -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AbstractMode -> r

gmapQ :: (forall d. Data d => d -> u) -> AbstractMode -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> AbstractMode -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> AbstractMode -> m AbstractMode

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AbstractMode -> m AbstractMode

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AbstractMode -> m AbstractMode

Show AbstractMode Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> AbstractMode -> ShowS

show :: AbstractMode -> String

showList :: [AbstractMode] -> ShowS

type Context = [ContextEntry] Source #

The Context is a stack of ContextEntrys.

data UnquoteFlags Source #

Constructors

UnquoteFlags 

Fields

Instances

Instances details
Data UnquoteFlags Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UnquoteFlags -> c UnquoteFlags

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UnquoteFlags

toConstr :: UnquoteFlags -> Constr

dataTypeOf :: UnquoteFlags -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c UnquoteFlags)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UnquoteFlags)

gmapT :: (forall b. Data b => b -> b) -> UnquoteFlags -> UnquoteFlags

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UnquoteFlags -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UnquoteFlags -> r

gmapQ :: (forall d. Data d => d -> u) -> UnquoteFlags -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> UnquoteFlags -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> UnquoteFlags -> m UnquoteFlags

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UnquoteFlags -> m UnquoteFlags

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UnquoteFlags -> m UnquoteFlags

class LensTCEnv a where Source #

Instances

Instances details
LensTCEnv TCEnv Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensTCEnv (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

data Builtin pf Source #

Constructors

Builtin Term 
Prim pf 

Instances

Instances details
Functor Builtin Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fmap :: (a -> b) -> Builtin a -> Builtin b

(<$) :: a -> Builtin b -> Builtin a #

Foldable Builtin Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fold :: Monoid m => Builtin m -> m

foldMap :: Monoid m => (a -> m) -> Builtin a -> m

foldMap' :: Monoid m => (a -> m) -> Builtin a -> m

foldr :: (a -> b -> b) -> b -> Builtin a -> b

foldr' :: (a -> b -> b) -> b -> Builtin a -> b

foldl :: (b -> a -> b) -> b -> Builtin a -> b

foldl' :: (b -> a -> b) -> b -> Builtin a -> b

foldr1 :: (a -> a -> a) -> Builtin a -> a

foldl1 :: (a -> a -> a) -> Builtin a -> a

toList :: Builtin a -> [a]

null :: Builtin a -> Bool

length :: Builtin a -> Int

elem :: Eq a => a -> Builtin a -> Bool

maximum :: Ord a => Builtin a -> a

minimum :: Ord a => Builtin a -> a

sum :: Num a => Builtin a -> a

product :: Num a => Builtin a -> a

Traversable Builtin Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

traverse :: Applicative f => (a -> f b) -> Builtin a -> f (Builtin b)

sequenceA :: Applicative f => Builtin (f a) -> f (Builtin a)

mapM :: Monad m => (a -> m b) -> Builtin a -> m (Builtin b)

sequence :: Monad m => Builtin (m a) -> m (Builtin a)

Show pf => Show (Builtin pf) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Builtin pf -> ShowS

show :: Builtin pf -> String

showList :: [Builtin pf] -> ShowS

EmbPrj a => EmbPrj (Builtin a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Builtin a -> S Int32 Source #

icod_ :: Builtin a -> S Int32 Source #

value :: Int32 -> R (Builtin a) Source #

InstantiateFull a => InstantiateFull (Builtin a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

type BuiltinThings pf = Map String (Builtin pf) Source #

data BuiltinDescriptor Source #

Constructors

BuiltinData (TCM Type) [String] 
BuiltinDataCons (TCM Type) 
BuiltinPrim String (Term -> TCM ()) 
BuiltinPostulate Relevance (TCM Type) 
BuiltinUnknown (Maybe (TCM Type)) (Term -> Type -> TCM ())

Builtin of any kind. Type can be checked (Just t) or inferred (Nothing). The second argument is the hook for the verification function.

type TempInstanceTable = (InstanceTable, Set QName) Source #

When typechecking something of the following form:

instance x : _ x = y

it's not yet known where to add x, so we add it to a list of unresolved instances and we'll deal with it later.

type InstanceTable = Map QName (Set QName) Source #

The instance table is a Map associating to every name of recorddata typepostulate its list of instances

data Call Source #

Instances

Instances details
Data Call Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Call -> c Call

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Call

toConstr :: Call -> Constr

dataTypeOf :: Call -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Call)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Call)

gmapT :: (forall b. Data b => b -> b) -> Call -> Call

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Call -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Call -> r

gmapQ :: (forall d. Data d => d -> u) -> Call -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Call -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Call -> m Call

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Call -> m Call

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Call -> m Call

Pretty Call Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Call -> Doc Source #

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

prettyList :: [Call] -> Doc Source #

HasRange Call Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: Call -> Range Source #

PrettyTCM Call Source # 
Instance details

Defined in Agda.TypeChecking.Pretty.Call

Methods

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

type Statistics = Map String Integer Source #

newtype MutualId Source #

Constructors

MutId Int32 

Instances

Instances details
Enum MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Eq MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: MutualId -> MutualId -> Bool

(/=) :: MutualId -> MutualId -> Bool

Data MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MutualId -> c MutualId

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MutualId

toConstr :: MutualId -> Constr

dataTypeOf :: MutualId -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MutualId)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MutualId)

gmapT :: (forall b. Data b => b -> b) -> MutualId -> MutualId

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MutualId -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MutualId -> r

gmapQ :: (forall d. Data d => d -> u) -> MutualId -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> MutualId -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> MutualId -> m MutualId

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MutualId -> m MutualId

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MutualId -> m MutualId

Num MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Ord MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

compare :: MutualId -> MutualId -> Ordering

(<) :: MutualId -> MutualId -> Bool

(<=) :: MutualId -> MutualId -> Bool

(>) :: MutualId -> MutualId -> Bool

(>=) :: MutualId -> MutualId -> Bool

max :: MutualId -> MutualId -> MutualId

min :: MutualId -> MutualId -> MutualId

Show MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> MutualId -> ShowS

show :: MutualId -> String

showList :: [MutualId] -> ShowS

KillRange MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasFresh MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj MutualId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: MutualId -> S Int32 Source #

icod_ :: MutualId -> S Int32 Source #

value :: Int32 -> R MutualId Source #

data TermHead Source #

Instances

Instances details
Eq TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: TermHead -> TermHead -> Bool

(/=) :: TermHead -> TermHead -> Bool

Data TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TermHead -> c TermHead

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TermHead

toConstr :: TermHead -> Constr

dataTypeOf :: TermHead -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TermHead)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TermHead)

gmapT :: (forall b. Data b => b -> b) -> TermHead -> TermHead

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TermHead -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TermHead -> r

gmapQ :: (forall d. Data d => d -> u) -> TermHead -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> TermHead -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TermHead -> m TermHead

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TermHead -> m TermHead

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TermHead -> m TermHead

Ord TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

compare :: TermHead -> TermHead -> Ordering

(<) :: TermHead -> TermHead -> Bool

(<=) :: TermHead -> TermHead -> Bool

(>) :: TermHead -> TermHead -> Bool

(>=) :: TermHead -> TermHead -> Bool

max :: TermHead -> TermHead -> TermHead

min :: TermHead -> TermHead -> TermHead

Show TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> TermHead -> ShowS

show :: TermHead -> String

showList :: [TermHead] -> ShowS

Pretty TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj TermHead Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: TermHead -> S Int32 Source #

icod_ :: TermHead -> S Int32 Source #

value :: Int32 -> R TermHead Source #

data FunctionInverse' c Source #

Constructors

NotInjective 
Inverse (InversionMap c) 

Instances

Instances details
Functor FunctionInverse' Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fmap :: (a -> b) -> FunctionInverse' a -> FunctionInverse' b

(<$) :: a -> FunctionInverse' b -> FunctionInverse' a #

Abstract FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

DropArgs FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.DropArgs

InstantiateFull FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Data c => Data (FunctionInverse' c) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c0 (d -> b) -> d -> c0 b) -> (forall g. g -> c0 g) -> FunctionInverse' c -> c0 (FunctionInverse' c)

gunfold :: (forall b r. Data b => c0 (b -> r) -> c0 r) -> (forall r. r -> c0 r) -> Constr -> c0 (FunctionInverse' c)

toConstr :: FunctionInverse' c -> Constr

dataTypeOf :: FunctionInverse' c -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c0 (t d)) -> Maybe (c0 (FunctionInverse' c))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c0 (t d e)) -> Maybe (c0 (FunctionInverse' c))

gmapT :: (forall b. Data b => b -> b) -> FunctionInverse' c -> FunctionInverse' c

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FunctionInverse' c -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FunctionInverse' c -> r

gmapQ :: (forall d. Data d => d -> u) -> FunctionInverse' c -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> FunctionInverse' c -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> FunctionInverse' c -> m (FunctionInverse' c)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FunctionInverse' c -> m (FunctionInverse' c)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FunctionInverse' c -> m (FunctionInverse' c)

Show c => Show (FunctionInverse' c) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> FunctionInverse' c -> ShowS

show :: FunctionInverse' c -> String

showList :: [FunctionInverse' c] -> ShowS

KillRange c => KillRange (FunctionInverse' c) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj a => EmbPrj (FunctionInverse' a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: FunctionInverse' a -> S Int32 Source #

icod_ :: FunctionInverse' a -> S Int32 Source #

value :: Int32 -> R (FunctionInverse' a) Source #

type InversionMap c = Map TermHead [c] Source #

data PrimFun Source #

Instances

Instances details
Abstract PrimFun Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply PrimFun Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

data PrimitiveImpl Source #

Primitives

Constructors

PrimImpl Type PrimFun 

data AllowedReduction Source #

Controlling reduce.

Constructors

ProjectionReductions

(Projection and) projection-like functions may be reduced.

InlineReductions

Functions marked INLINE may be reduced.

CopatternReductions

Copattern definitions may be reduced.

FunctionReductions

Non-recursive functions and primitives may be reduced.

RecursiveReductions

Even recursive functions may be reduced.

LevelReductions

Reduce Level terms.

TypeLevelReductions

Allow allReductions in types, even if not allowed at term level (used by confluence checker)

UnconfirmedReductions

Functions whose termination has not (yet) been confirmed.

NonTerminatingReductions

Functions that have failed termination checking.

Instances

Instances details
Bounded AllowedReduction Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Enum AllowedReduction Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Eq AllowedReduction Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data AllowedReduction Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AllowedReduction -> c AllowedReduction

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AllowedReduction

toConstr :: AllowedReduction -> Constr

dataTypeOf :: AllowedReduction -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AllowedReduction)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AllowedReduction)

gmapT :: (forall b. Data b => b -> b) -> AllowedReduction -> AllowedReduction

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AllowedReduction -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AllowedReduction -> r

gmapQ :: (forall d. Data d => d -> u) -> AllowedReduction -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> AllowedReduction -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> AllowedReduction -> m AllowedReduction

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AllowedReduction -> m AllowedReduction

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AllowedReduction -> m AllowedReduction

Ord AllowedReduction Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show AllowedReduction Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> AllowedReduction -> ShowS

show :: AllowedReduction -> String

showList :: [AllowedReduction] -> ShowS

Ix AllowedReduction Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

data MaybeReduced a Source #

Constructors

MaybeRed 

Instances

Instances details
Functor MaybeReduced Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fmap :: (a -> b) -> MaybeReduced a -> MaybeReduced b

(<$) :: a -> MaybeReduced b -> MaybeReduced a #

IsProjElim e => IsProjElim (MaybeReduced e) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM a => PrettyTCM (MaybeReduced a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

data IsReduced Source #

Three cases: 1. not reduced, 2. reduced, but blocked, 3. reduced, not blocked.

Constructors

NotReduced 
Reduced (Blocked ()) 

data Reduced no yes Source #

Instances

Instances details
Functor (Reduced no) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fmap :: (a -> b) -> Reduced no a -> Reduced no b

(<$) :: a -> Reduced no b -> Reduced no a #

data Simplification Source #

Did we encounter a simplifying reduction? In terms of CIC, that would be a iota-reduction. In terms of Agda, this is a constructor or literal pattern that matched. Just beta-reduction (substitution) or delta-reduction (unfolding of definitions) does not count as simplifying?

Instances

Instances details
Eq Simplification Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data Simplification Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Simplification -> c Simplification

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Simplification

toConstr :: Simplification -> Constr

dataTypeOf :: Simplification -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Simplification)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Simplification)

gmapT :: (forall b. Data b => b -> b) -> Simplification -> Simplification

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Simplification -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Simplification -> r

gmapQ :: (forall d. Data d => d -> u) -> Simplification -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Simplification -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Simplification -> m Simplification

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Simplification -> m Simplification

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Simplification -> m Simplification

Show Simplification Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Simplification -> ShowS

show :: Simplification -> String

showList :: [Simplification] -> ShowS

Semigroup Simplification Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Monoid Simplification Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Null Simplification Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

newtype Fields Source #

Constructors

Fields [(Name, Type)] 

Instances

Instances details
Null Fields Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

empty :: Fields Source #

null :: Fields -> Bool Source #

data Defn Source #

Constructors

Axiom

Postulate

DataOrRecSig

Data or record type signature that doesn't yet have a definition

Fields

GeneralizableVar

Generalizable variable (introduced in generalize block)

AbstractDefn Defn

Returned by getConstInfo if definition is abstract.

Function 

Fields

  • funClauses :: [Clause]
     
  • funCompiled :: Maybe CompiledClauses

    Nothing while function is still type-checked. Just cc after type and coverage checking and translation to case trees.

  • funSplitTree :: Maybe SplitTree

    The split tree constructed by the coverage checker. Needed to re-compile the clauses after forcing translation.

  • funTreeless :: Maybe Compiled

    Intermediate representation for compiler backends.

  • funCovering :: [Clause]

    Covering clauses computed by coverage checking. Erased by (IApply) confluence checking(?)

  • funInv :: FunctionInverse
     
  • funMutual :: Maybe [QName]

    Mutually recursive functions, datas and records. Does include this function. Empty list if not recursive. Nothing if not yet computed (by positivity checker).

  • funAbstr :: IsAbstract
     
  • funDelayed :: Delayed

    Are the clauses of this definition delayed?

  • funProjection :: Maybe Projection

    Is it a record projection? If yes, then return the name of the record type and index of the record argument. Start counting with 1, because 0 means that it is already applied to the record. (Can happen in module instantiation.) This information is used in the termination checker.

  • funFlags :: Set FunctionFlag
     
  • funTerminates :: Maybe Bool

    Has this function been termination checked? Did it pass?

  • funExtLam :: Maybe ExtLamInfo

    Is this function generated from an extended lambda? If yes, then return the number of hidden and non-hidden lambda-lifted arguments

  • funWith :: Maybe QName

    Is this a generated with-function? If yes, then what's the name of the parent function.

Datatype 

Fields

Record 

Fields

  • recPars :: Nat

    Number of parameters.

  • recClause :: Maybe Clause

    Was this record type created by a module application? If yes, the clause is its definition (linking back to the original record type).

  • recConHead :: ConHead

    Constructor name and fields.

  • recNamedCon :: Bool

    Does this record have a constructor?

  • recFields :: [Dom QName]

    The record field names.

  • recTel :: Telescope

    The record field telescope. (Includes record parameters.) Note: TelV recTel _ == telView' recConType. Thus, recTel is redundant.

  • recMutual :: Maybe [QName]

    Mutually recursive functions, datas and records. Does include this record. Empty if not recursive. Nothing if not yet computed (by positivity checker).

  • recEtaEquality' :: EtaEquality

    Eta-expand at this record type? False for unguarded recursive records and coinductive records unless the user specifies otherwise.

  • recInduction :: Maybe Induction

    Inductive or CoInductive? Matters only for recursive records. Nothing means that the user did not specify it, which is an error for recursive records.

  • recAbstr :: IsAbstract
     
  • recComp :: CompKit
     
Constructor 

Fields

  • conPars :: Int

    Number of parameters.

  • conArity :: Int

    Number of arguments (excluding parameters).

  • conSrcCon :: ConHead

    Name of (original) constructor and fields. (This might be in a module instance.)

  • conData :: QName

    Name of datatype or record type.

  • conAbstr :: IsAbstract
     
  • conInd :: Induction

    Inductive or coinductive?

  • conComp :: CompKit

    Cubical composition.

  • conProj :: Maybe [QName]

    Projections. Nothing if not yet computed.

  • conForced :: [IsForced]

    Which arguments are forced (i.e. determined by the type of the constructor)? Either this list is empty (if the forcing analysis isn't run), or its length is conArity.

  • conErased :: Maybe [Bool]

    Which arguments are erased at runtime (computed during compilation to treeless)? True means erased, False means retained. Nothing if no erasure analysis has been performed yet. The length of the list is conArity.

Primitive

Primitive or builtin functions.

Fields

Instances

Instances details
Data Defn Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Defn -> c Defn

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Defn

toConstr :: Defn -> Constr

dataTypeOf :: Defn -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Defn)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Defn)

gmapT :: (forall b. Data b => b -> b) -> Defn -> Defn

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r

gmapQ :: (forall d. Data d => d -> u) -> Defn -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Defn -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Defn -> m Defn

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Defn -> m Defn

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Defn -> m Defn

Show Defn Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Defn -> ShowS

show :: Defn -> String

showList :: [Defn] -> ShowS

Pretty Defn Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

pretty :: Defn -> Doc Source #

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

prettyList :: [Defn] -> Doc Source #

KillRange Defn Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Abstract Defn Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply Defn Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Defn -> Args -> Defn Source #

applyE :: Defn -> Elims -> Defn Source #

EmbPrj Defn Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Defn -> S Int32 Source #

icod_ :: Defn -> S Int32 Source #

value :: Int32 -> R Defn Source #

NamesIn Defn Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Defn -> Set QName Source #

InstantiateFull Defn Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Occurs Defn Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

data CompKit Source #

Constructors

CompKit 

Fields

Instances

Instances details
Eq CompKit Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: CompKit -> CompKit -> Bool

(/=) :: CompKit -> CompKit -> Bool

Data CompKit Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CompKit -> c CompKit

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CompKit

toConstr :: CompKit -> Constr

dataTypeOf :: CompKit -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CompKit)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CompKit)

gmapT :: (forall b. Data b => b -> b) -> CompKit -> CompKit

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CompKit -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CompKit -> r

gmapQ :: (forall d. Data d => d -> u) -> CompKit -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> CompKit -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> CompKit -> m CompKit

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CompKit -> m CompKit

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CompKit -> m CompKit

Ord CompKit Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

compare :: CompKit -> CompKit -> Ordering

(<) :: CompKit -> CompKit -> Bool

(<=) :: CompKit -> CompKit -> Bool

(>) :: CompKit -> CompKit -> Bool

(>=) :: CompKit -> CompKit -> Bool

max :: CompKit -> CompKit -> CompKit

min :: CompKit -> CompKit -> CompKit

Show CompKit Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> CompKit -> ShowS

show :: CompKit -> String

showList :: [CompKit] -> ShowS

KillRange CompKit Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj CompKit Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: CompKit -> S Int32 Source #

icod_ :: CompKit -> S Int32 Source #

value :: Int32 -> R CompKit Source #

NamesIn CompKit Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: CompKit -> Set QName Source #

data FunctionFlag Source #

Constructors

FunStatic

Should calls to this function be normalised at compile-time?

FunInline

Should calls to this function be inlined by the compiler?

FunMacro

Is this function a macro?

Instances

Instances details
Enum FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Eq FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: FunctionFlag -> FunctionFlag -> Bool

(/=) :: FunctionFlag -> FunctionFlag -> Bool

Data FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FunctionFlag -> c FunctionFlag

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FunctionFlag

toConstr :: FunctionFlag -> Constr

dataTypeOf :: FunctionFlag -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FunctionFlag)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunctionFlag)

gmapT :: (forall b. Data b => b -> b) -> FunctionFlag -> FunctionFlag

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FunctionFlag -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FunctionFlag -> r

gmapQ :: (forall d. Data d => d -> u) -> FunctionFlag -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> FunctionFlag -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> FunctionFlag -> m FunctionFlag

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FunctionFlag -> m FunctionFlag

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FunctionFlag -> m FunctionFlag

Ord FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> FunctionFlag -> ShowS

show :: FunctionFlag -> String

showList :: [FunctionFlag] -> ShowS

KillRange FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj FunctionFlag Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: FunctionFlag -> S Int32 Source #

icod_ :: FunctionFlag -> S Int32 Source #

value :: Int32 -> R FunctionFlag Source #

data EtaEquality Source #

Should a record type admit eta-equality?

Constructors

Specified

User specifed 'eta-equality' or 'no-eta-equality'.

Inferred

Positivity checker inferred whether eta is safe.

Instances

Instances details
Eq EtaEquality Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: EtaEquality -> EtaEquality -> Bool

(/=) :: EtaEquality -> EtaEquality -> Bool

Data EtaEquality Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> EtaEquality -> c EtaEquality

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c EtaEquality

toConstr :: EtaEquality -> Constr

dataTypeOf :: EtaEquality -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c EtaEquality)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EtaEquality)

gmapT :: (forall b. Data b => b -> b) -> EtaEquality -> EtaEquality

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> EtaEquality -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> EtaEquality -> r

gmapQ :: (forall d. Data d => d -> u) -> EtaEquality -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> EtaEquality -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> EtaEquality -> m EtaEquality

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> EtaEquality -> m EtaEquality

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> EtaEquality -> m EtaEquality

Show EtaEquality Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> EtaEquality -> ShowS

show :: EtaEquality -> String

showList :: [EtaEquality] -> ShowS

KillRange EtaEquality Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj EtaEquality Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: EtaEquality -> S Int32 Source #

icod_ :: EtaEquality -> S Int32 Source #

value :: Int32 -> R EtaEquality Source #

newtype ProjLams Source #

Abstractions to build projection function (dropping parameters).

Constructors

ProjLams 

Fields

Instances

Instances details
Data ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProjLams -> c ProjLams

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProjLams

toConstr :: ProjLams -> Constr

dataTypeOf :: ProjLams -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProjLams)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProjLams)

gmapT :: (forall b. Data b => b -> b) -> ProjLams -> ProjLams

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProjLams -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProjLams -> r

gmapQ :: (forall d. Data d => d -> u) -> ProjLams -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ProjLams -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProjLams -> m ProjLams

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProjLams -> m ProjLams

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProjLams -> m ProjLams

Show ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> ProjLams -> ShowS

show :: ProjLams -> String

showList :: [ProjLams] -> ShowS

Null ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

empty :: ProjLams Source #

null :: ProjLams -> Bool Source #

KillRange ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Abstract ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

EmbPrj ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ProjLams -> S Int32 Source #

icod_ :: ProjLams -> S Int32 Source #

value :: Int32 -> R ProjLams Source #

data Projection Source #

Additional information for projection Functions.

Constructors

Projection 

Fields

  • projProper :: Maybe QName

    Nothing if only projection-like, Just r if record projection. The r is the name of the record type projected from. This field is updated by module application.

  • projOrig :: QName

    The original projection name (current name could be from module application).

  • projFromType :: Arg QName

    Type projected from. Original record type if projProper = Just{}. Also stores ArgInfo of the principal argument. This field is unchanged by module application.

  • projIndex :: Int

    Index of the record argument. Start counting with 1, because 0 means that it is already applied to the record value. This can happen in module instantiation, but then either the record value is var 0, or funProjection == Nothing.

  • projLams :: ProjLams

    Term t to be be applied to record parameters and record value. The parameters will be dropped. In case of a proper projection, a postfix projection application will be created: t = pars r -> r .p (Invariant: the number of abstractions equals projIndex.) In case of a projection-like function, just the function symbol is returned as Def: t = pars -> f.

Instances

Instances details
Data Projection Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Projection -> c Projection

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Projection

toConstr :: Projection -> Constr

dataTypeOf :: Projection -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Projection)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Projection)

gmapT :: (forall b. Data b => b -> b) -> Projection -> Projection

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Projection -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Projection -> r

gmapQ :: (forall d. Data d => d -> u) -> Projection -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Projection -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Projection -> m Projection

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Projection -> m Projection

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Projection -> m Projection

Show Projection Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Projection -> ShowS

show :: Projection -> String

showList :: [Projection] -> ShowS

KillRange Projection Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Abstract Projection Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply Projection Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

EmbPrj Projection Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Projection -> S Int32 Source #

icod_ :: Projection -> S Int32 Source #

value :: Int32 -> R Projection Source #

data ExtLamInfo Source #

Additional information for extended lambdas.

Constructors

ExtLamInfo 

Fields

  • extLamModule :: ModuleName

    For complicated reasons the scope checker decides the QName of a pattern lambda, and thus its module. We really need to decide the module during type checking though, since if the lambda appears in a refined context the module picked by the scope checker has very much the wrong parameters.

  • extLamSys :: !(Maybe System)
     

Instances

Instances details
Data ExtLamInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ExtLamInfo -> c ExtLamInfo

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ExtLamInfo

toConstr :: ExtLamInfo -> Constr

dataTypeOf :: ExtLamInfo -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ExtLamInfo)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExtLamInfo)

gmapT :: (forall b. Data b => b -> b) -> ExtLamInfo -> ExtLamInfo

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ExtLamInfo -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ExtLamInfo -> r

gmapQ :: (forall d. Data d => d -> u) -> ExtLamInfo -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ExtLamInfo -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ExtLamInfo -> m ExtLamInfo

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ExtLamInfo -> m ExtLamInfo

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ExtLamInfo -> m ExtLamInfo

Show ExtLamInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> ExtLamInfo -> ShowS

show :: ExtLamInfo -> String

showList :: [ExtLamInfo] -> ShowS

KillRange ExtLamInfo Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Apply ExtLamInfo Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

EmbPrj ExtLamInfo Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ExtLamInfo -> S Int32 Source #

icod_ :: ExtLamInfo -> S Int32 Source #

value :: Int32 -> R ExtLamInfo Source #

InstantiateFull ExtLamInfo Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

data System Source #

An alternative representation of partial elements in a telescope: Γ ⊢ λ Δ. [φ₁ u₁, ... , φₙ uₙ] : Δ → PartialP (∨_ᵢ φᵢ) T see cubicaltt paper (however we do not store the type T).

Constructors

System 

Fields

  • systemTel :: Telescope

    the telescope Δ, binding vars for the clauses, Γ ⊢ Δ

  • systemClauses :: [(Face, Term)]

    a system [φ₁ u₁, ... , φₙ uₙ] where Γ, Δ ⊢ φᵢ and Γ, Δ, φᵢ ⊢ uᵢ

Instances

Instances details
Data System Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> System -> c System

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c System

toConstr :: System -> Constr

dataTypeOf :: System -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c System)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c System)

gmapT :: (forall b. Data b => b -> b) -> System -> System

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> System -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> System -> r

gmapQ :: (forall d. Data d => d -> u) -> System -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> System -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> System -> m System

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> System -> m System

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> System -> m System

Show System Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> System -> ShowS

show :: System -> String

showList :: [System] -> ShowS

KillRange System Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Abstract System Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply System Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

EmbPrj System Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: System -> S Int32 Source #

icod_ :: System -> S Int32 Source #

value :: Int32 -> R System Source #

InstantiateFull System Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reify (QNamed System) [Clause] Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => QNamed System -> m [Clause] Source #

reifyWhen :: MonadReify m => Bool -> QNamed System -> m [Clause] Source #

type Face = [(Term, Bool)] Source #

data CompilerPragma Source #

The backends are responsible for parsing their own pragmas.

Constructors

CompilerPragma Range String 

Instances

Instances details
Eq CompilerPragma Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data CompilerPragma Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CompilerPragma -> c CompilerPragma

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CompilerPragma

toConstr :: CompilerPragma -> Constr

dataTypeOf :: CompilerPragma -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CompilerPragma)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CompilerPragma)

gmapT :: (forall b. Data b => b -> b) -> CompilerPragma -> CompilerPragma

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CompilerPragma -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CompilerPragma -> r

gmapQ :: (forall d. Data d => d -> u) -> CompilerPragma -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> CompilerPragma -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> CompilerPragma -> m CompilerPragma

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CompilerPragma -> m CompilerPragma

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CompilerPragma -> m CompilerPragma

Show CompilerPragma Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> CompilerPragma -> ShowS

show :: CompilerPragma -> String

showList :: [CompilerPragma] -> ShowS

KillRange CompiledRepresentation Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasRange CompilerPragma Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj CompilerPragma Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Compilers

Methods

icode :: CompilerPragma -> S Int32 Source #

icod_ :: CompilerPragma -> S Int32 Source #

value :: Int32 -> R CompilerPragma Source #

data IsForced Source #

Information about whether an argument is forced by the type of a function.

Constructors

Forced 
NotForced 

Instances

Instances details
Eq IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: IsForced -> IsForced -> Bool

(/=) :: IsForced -> IsForced -> Bool

Data IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsForced -> c IsForced

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IsForced

toConstr :: IsForced -> Constr

dataTypeOf :: IsForced -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IsForced)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IsForced)

gmapT :: (forall b. Data b => b -> b) -> IsForced -> IsForced

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsForced -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsForced -> r

gmapQ :: (forall d. Data d => d -> u) -> IsForced -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> IsForced -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsForced -> m IsForced

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsForced -> m IsForced

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsForced -> m IsForced

Show IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> IsForced -> ShowS

show :: IsForced -> String

showList :: [IsForced] -> ShowS

KillRange IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: IsForced -> S Int32 Source #

icod_ :: IsForced -> S Int32 Source #

value :: Int32 -> R IsForced Source #

PrettyTCM IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

ChooseFlex IsForced Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

data NumGeneralizableArgs Source #

Constructors

NoGeneralizableArgs 
SomeGeneralizableArgs Int

When lambda-lifting new args are generalizable if SomeGeneralizableArgs, also when the number is zero.

Instances

Instances details
Data NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NumGeneralizableArgs -> c NumGeneralizableArgs

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NumGeneralizableArgs

toConstr :: NumGeneralizableArgs -> Constr

dataTypeOf :: NumGeneralizableArgs -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NumGeneralizableArgs)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NumGeneralizableArgs)

gmapT :: (forall b. Data b => b -> b) -> NumGeneralizableArgs -> NumGeneralizableArgs

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NumGeneralizableArgs -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NumGeneralizableArgs -> r

gmapQ :: (forall d. Data d => d -> u) -> NumGeneralizableArgs -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> NumGeneralizableArgs -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NumGeneralizableArgs -> m NumGeneralizableArgs

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NumGeneralizableArgs -> m NumGeneralizableArgs

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NumGeneralizableArgs -> m NumGeneralizableArgs

Show NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> NumGeneralizableArgs -> ShowS

show :: NumGeneralizableArgs -> String

showList :: [NumGeneralizableArgs] -> ShowS

KillRange NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Abstract NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

EmbPrj NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

data Definition Source #

Constructors

Defn 

Fields

Instances

Instances details
Data Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Definition -> c Definition

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Definition

toConstr :: Definition -> Constr

dataTypeOf :: Definition -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Definition)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Definition)

gmapT :: (forall b. Data b => b -> b) -> Definition -> Definition

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Definition -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Definition -> r

gmapQ :: (forall d. Data d => d -> u) -> Definition -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Definition -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Definition -> m Definition

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Definition -> m Definition

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Definition -> m Definition

Show Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Definition -> ShowS

show :: Definition -> String

showList :: [Definition] -> ShowS

Pretty Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Definitions Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensArgInfo Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensRelevance Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensQuantity Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensModality Definition Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Abstract Definition Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply Definition Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

EmbPrj Definition Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Definition -> S Int32 Source #

icod_ :: Definition -> S Int32 Source #

value :: Int32 -> R Definition Source #

NamesIn Definition Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Definition -> Set QName Source #

InstantiateFull Definition Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

data RewriteRule Source #

Rewrite rules can be added independently from function clauses.

Constructors

RewriteRule 

Fields

Instances

Instances details
Data RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RewriteRule -> c RewriteRule

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RewriteRule

toConstr :: RewriteRule -> Constr

dataTypeOf :: RewriteRule -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RewriteRule)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RewriteRule)

gmapT :: (forall b. Data b => b -> b) -> RewriteRule -> RewriteRule

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RewriteRule -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RewriteRule -> r

gmapQ :: (forall d. Data d => d -> u) -> RewriteRule -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> RewriteRule -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RewriteRule -> m RewriteRule

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RewriteRule -> m RewriteRule

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RewriteRule -> m RewriteRule

Show RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> RewriteRule -> ShowS

show :: RewriteRule -> String

showList :: [RewriteRule] -> ShowS

KillRange RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange RewriteRuleMap Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Abstract RewriteRule Source #

tel ⊢ (Γ ⊢ lhs ↦ rhs : t) becomes tel, Γ ⊢ lhs ↦ rhs : t) we do not need to change lhs, rhs, and t since they live in Γ. See 'Abstract Clause'.

Instance details

Defined in Agda.TypeChecking.Substitute

Apply RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

EmbPrj RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: RewriteRule -> S Int32 Source #

icod_ :: RewriteRule -> S Int32 Source #

value :: Int32 -> R RewriteRule Source #

PrettyTCM RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

InstantiateFull RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

GetMatchables RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Subst NLPat RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

data NLPSort Source #

Constructors

PType NLPat 
PProp NLPat 
PInf 
PSizeUniv 

Instances

Instances details
Data NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NLPSort -> c NLPSort

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NLPSort

toConstr :: NLPSort -> Constr

dataTypeOf :: NLPSort -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NLPSort)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NLPSort)

gmapT :: (forall b. Data b => b -> b) -> NLPSort -> NLPSort

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NLPSort -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NLPSort -> r

gmapQ :: (forall d. Data d => d -> u) -> NLPSort -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> NLPSort -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NLPSort -> m NLPSort

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NLPSort -> m NLPSort

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NLPSort -> m NLPSort

Show NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> NLPSort -> ShowS

show :: NLPSort -> String

showList :: [NLPSort] -> ShowS

KillRange NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Free NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

freeVars' :: IsVarSet a c => NLPSort -> FreeM a c Source #

EmbPrj NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NLPSort -> S Int32 Source #

icod_ :: NLPSort -> S Int32 Source #

value :: Int32 -> R NLPSort Source #

PrettyTCM NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

InstantiateFull NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

GetMatchables NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

NLPatVars NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

nlPatVarsUnder :: Int -> NLPSort -> IntSet Source #

nlPatVars :: NLPSort -> IntSet Source #

Subst NLPat NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

NLPatToTerm NLPSort Sort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

PatternFrom () Sort NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> () -> Sort -> TCM NLPSort Source #

Match () NLPSort Sort Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> () -> NLPSort -> Sort -> NLM () Source #

data NLPType Source #

Constructors

NLPType 

Instances

Instances details
Data NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NLPType -> c NLPType

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NLPType

toConstr :: NLPType -> Constr

dataTypeOf :: NLPType -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NLPType)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NLPType)

gmapT :: (forall b. Data b => b -> b) -> NLPType -> NLPType

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NLPType -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NLPType -> r

gmapQ :: (forall d. Data d => d -> u) -> NLPType -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> NLPType -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NLPType -> m NLPType

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NLPType -> m NLPType

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NLPType -> m NLPType

Show NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> NLPType -> ShowS

show :: NLPType -> String

showList :: [NLPType] -> ShowS

KillRange NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Free NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

freeVars' :: IsVarSet a c => NLPType -> FreeM a c Source #

EmbPrj NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NLPType -> S Int32 Source #

icod_ :: NLPType -> S Int32 Source #

value :: Int32 -> R NLPType Source #

PrettyTCM NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

InstantiateFull NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

GetMatchables NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

NLPatVars NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

nlPatVarsUnder :: Int -> NLPType -> IntSet Source #

nlPatVars :: NLPType -> IntSet Source #

Subst NLPat NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

NLPatToTerm NLPType Type Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

PatternFrom () Type NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> () -> Type -> TCM NLPType Source #

Match () NLPType Type Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> () -> NLPType -> Type -> NLM () Source #

data NLPat Source #

Non-linear (non-constructor) first-order pattern.

Constructors

PVar !Int [Arg Int]

Matches anything (modulo non-linearity) that only contains bound variables that occur in the given arguments.

PDef QName PElims

Matches f es

PLam ArgInfo (Abs NLPat)

Matches λ x → t

PPi (Dom NLPType) (Abs NLPType)

Matches (x : A) → B

PSort NLPSort

Matches a sort of the given shape.

PBoundVar !Int PElims

Matches x es where x is a lambda-bound variable

PTerm Term

Matches the term modulo β (ideally βη).

Instances

Instances details
Data NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NLPat -> c NLPat

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NLPat

toConstr :: NLPat -> Constr

dataTypeOf :: NLPat -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NLPat)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NLPat)

gmapT :: (forall b. Data b => b -> b) -> NLPat -> NLPat

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NLPat -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NLPat -> r

gmapQ :: (forall d. Data d => d -> u) -> NLPat -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> NLPat -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NLPat -> m NLPat

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NLPat -> m NLPat

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NLPat -> m NLPat

Show NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> NLPat -> ShowS

show :: NLPat -> String

showList :: [NLPat] -> ShowS

KillRange NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

DeBruijn NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

deBruijnVar :: Int -> NLPat Source #

debruijnNamedVar :: String -> Int -> NLPat Source #

deBruijnView :: NLPat -> Maybe Int Source #

Free NLPat Source #

Only computes free variables that are not bound (see nlPatVars), i.e., those in a PTerm.

Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

freeVars' :: IsVarSet a c => NLPat -> FreeM a c Source #

EmbPrj NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NLPat -> S Int32 Source #

icod_ :: NLPat -> S Int32 Source #

value :: Int32 -> R NLPat Source #

PrettyTCM NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

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

InstantiateFull NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

GetMatchables NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

NLPatVars NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

nlPatVarsUnder :: Int -> NLPat -> IntSet Source #

nlPatVars :: NLPat -> IntSet Source #

Subst NLPat RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst NLPat NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst NLPat NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst NLPat NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

NLPatToTerm NLPat Level Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

NLPatToTerm NLPat Term Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

PatternFrom () Level NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> () -> Level -> TCM NLPat Source #

PatternFrom Type Term NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> Type -> Term -> TCM NLPat Source #

Match () NLPat Level Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> () -> NLPat -> Level -> NLM () Source #

Match Type NLPat Term Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> Type -> NLPat -> Term -> NLM () Source #

PrettyTCM (Type' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

ToNLPat (Arg DeBruijnPattern) (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

PatternFrom (Type, Term) Elims [Elim' NLPat] Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

patternFrom :: Relevance -> Int -> (Type, Term) -> Elims -> TCM [Elim' NLPat] Source #

Match (Type, Term) [Elim' NLPat] Elims Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> (Type, Term) -> [Elim' NLPat] -> Elims -> NLM () Source #

data DisplayTerm Source #

A structured presentation of a Term for reification into Syntax.

Constructors

DWithApp DisplayTerm [DisplayTerm] Elims

(f vs | ws) es. The first DisplayTerm is the parent function f with its args vs. The list of DisplayTerms are the with expressions ws. The Elims are additional arguments es (possible in case the with-application is of function type) or projections (if it is of record type).

DCon ConHead ConInfo [Arg DisplayTerm]

c vs.

DDef QName [Elim' DisplayTerm]

d vs.

DDot Term

.v.

DTerm Term

v.

Instances

Instances details
Data DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DisplayTerm -> c DisplayTerm

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DisplayTerm

toConstr :: DisplayTerm -> Constr

dataTypeOf :: DisplayTerm -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DisplayTerm)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DisplayTerm)

gmapT :: (forall b. Data b => b -> b) -> DisplayTerm -> DisplayTerm

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DisplayTerm -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DisplayTerm -> r

gmapQ :: (forall d. Data d => d -> u) -> DisplayTerm -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> DisplayTerm -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DisplayTerm -> m DisplayTerm

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DisplayTerm -> m DisplayTerm

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DisplayTerm -> m DisplayTerm

Show DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> DisplayTerm -> ShowS

show :: DisplayTerm -> String

showList :: [DisplayTerm] -> ShowS

Pretty DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Free DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

freeVars' :: IsVarSet a c => DisplayTerm -> FreeM a c Source #

Apply DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

EmbPrj DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DisplayTerm -> S Int32 Source #

icod_ :: DisplayTerm -> S Int32 Source #

value :: Int32 -> R DisplayTerm Source #

PrettyTCM DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

NamesIn DisplayTerm Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: DisplayTerm -> Set QName Source #

InstantiateFull DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

SubstWithOrigin DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.DisplayForm

Subst Term DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Reify DisplayTerm Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

PrettyTCM (Elim' DisplayTerm) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

SubstWithOrigin (Arg DisplayTerm) Source # 
Instance details

Defined in Agda.TypeChecking.DisplayForm

data DisplayForm Source #

A DisplayForm is in essence a rewrite rule q ts --> dt for a defined symbol (could be a constructor as well) q. The right hand side is a DisplayTerm which is used to reify to a more readable Syntax.

The patterns ts are just terms, but var 0 is interpreted as a hole. Each occurrence of var 0 is a new hole (pattern var). For each *occurrence* of var0 the rhs dt has a free variable. These are instantiated when matching a display form against a term q vs succeeds.

Constructors

Display 

Fields

Instances

Instances details
Data DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DisplayForm -> c DisplayForm

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DisplayForm

toConstr :: DisplayForm -> Constr

dataTypeOf :: DisplayForm -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DisplayForm)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DisplayForm)

gmapT :: (forall b. Data b => b -> b) -> DisplayForm -> DisplayForm

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DisplayForm -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DisplayForm -> r

gmapQ :: (forall d. Data d => d -> u) -> DisplayForm -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> DisplayForm -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DisplayForm -> m DisplayForm

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DisplayForm -> m DisplayForm

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DisplayForm -> m DisplayForm

Show DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> DisplayForm -> ShowS

show :: DisplayForm -> String

showList :: [DisplayForm] -> ShowS

KillRange DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Free DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

freeVars' :: IsVarSet a c => DisplayForm -> FreeM a c Source #

EmbPrj DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DisplayForm -> S Int32 Source #

icod_ :: DisplayForm -> S Int32 Source #

value :: Int32 -> R DisplayForm Source #

NamesIn DisplayForm Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: DisplayForm -> Set QName Source #

InstantiateFull DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Subst Term DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

newtype Section Source #

Constructors

Section 

Instances

Instances details
Eq Section 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

(==) :: Section -> Section -> Bool

(/=) :: Section -> Section -> Bool

Data Section Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Section -> c Section

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Section

toConstr :: Section -> Constr

dataTypeOf :: Section -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Section)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Section)

gmapT :: (forall b. Data b => b -> b) -> Section -> Section

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Section -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Section -> r

gmapQ :: (forall d. Data d => d -> u) -> Section -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Section -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Section -> m Section

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Section -> m Section

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Section -> m Section

Show Section Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Section -> ShowS

show :: Section -> String

showList :: [Section] -> ShowS

Pretty Section Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Section Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

KillRange Sections Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj Section Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Section -> S Int32 Source #

icod_ :: Section -> S Int32 Source #

value :: Int32 -> R Section Source #

InstantiateFull Section Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

data Signature Source #

Constructors

Sig 

Fields

Instances

Instances details
Data Signature Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Signature -> c Signature

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Signature

toConstr :: Signature -> Constr

dataTypeOf :: Signature -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Signature)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Signature)

gmapT :: (forall b. Data b => b -> b) -> Signature -> Signature

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Signature -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Signature -> r

gmapQ :: (forall d. Data d => d -> u) -> Signature -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Signature -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Signature -> m Signature

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Signature -> m Signature

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Signature -> m Signature

Show Signature Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Signature -> ShowS

show :: Signature -> String

showList :: [Signature] -> ShowS

KillRange Signature Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj Signature Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Signature -> S Int32 Source #

icod_ :: Signature -> S Int32 Source #

value :: Int32 -> R Signature Source #

InstantiateFull Signature Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

data IPClause Source #

Which clause is an interaction point located in?

Constructors

IPClause 

Fields

IPNoClause

The interaction point is not in the rhs of a clause.

Instances

Instances details
Eq IPClause Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: IPClause -> IPClause -> Bool

(/=) :: IPClause -> IPClause -> Bool

Data IPClause Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IPClause -> c IPClause

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IPClause

toConstr :: IPClause -> Constr

dataTypeOf :: IPClause -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c IPClause)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IPClause)

gmapT :: (forall b. Data b => b -> b) -> IPClause -> IPClause

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IPClause -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IPClause -> r

gmapQ :: (forall d. Data d => d -> u) -> IPClause -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> IPClause -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IPClause -> m IPClause

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IPClause -> m IPClause

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IPClause -> m IPClause

data IPBoundary' t Source #

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

Constructors

IPBoundary 

Fields

Instances

Instances details
Functor IPBoundary' Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fmap :: (a -> b) -> IPBoundary' a -> IPBoundary' b

(<$) :: a -> IPBoundary' b -> IPBoundary' a #

Foldable IPBoundary' Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fold :: Monoid m => IPBoundary' m -> m

foldMap :: Monoid m => (a -> m) -> IPBoundary' a -> m

foldMap' :: Monoid m => (a -> m) -> IPBoundary' a -> m

foldr :: (a -> b -> b) -> b -> IPBoundary' a -> b

foldr' :: (a -> b -> b) -> b -> IPBoundary' a -> b

foldl :: (b -> a -> b) -> b -> IPBoundary' a -> b

foldl' :: (b -> a -> b) -> b -> IPBoundary' a -> b

foldr1 :: (a -> a -> a) -> IPBoundary' a -> a

foldl1 :: (a -> a -> a) -> IPBoundary' a -> a

toList :: IPBoundary' a -> [a]

null :: IPBoundary' a -> Bool

length :: IPBoundary' a -> Int

elem :: Eq a => a -> IPBoundary' a -> Bool

maximum :: Ord a => IPBoundary' a -> a

minimum :: Ord a => IPBoundary' a -> a

sum :: Num a => IPBoundary' a -> a

product :: Num a => IPBoundary' a -> a

Traversable IPBoundary' Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

traverse :: Applicative f => (a -> f b) -> IPBoundary' a -> f (IPBoundary' b)

sequenceA :: Applicative f => IPBoundary' (f a) -> f (IPBoundary' a)

mapM :: Monad m => (a -> m b) -> IPBoundary' a -> m (IPBoundary' b)

sequence :: Monad m => IPBoundary' (m a) -> m (IPBoundary' a)

Data t => Data (IPBoundary' t) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IPBoundary' t -> c (IPBoundary' t)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (IPBoundary' t)

toConstr :: IPBoundary' t -> Constr

dataTypeOf :: IPBoundary' t -> DataType

dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (IPBoundary' t))

dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (IPBoundary' t))

gmapT :: (forall b. Data b => b -> b) -> IPBoundary' t -> IPBoundary' t

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IPBoundary' t -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IPBoundary' t -> r

gmapQ :: (forall d. Data d => d -> u) -> IPBoundary' t -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> IPBoundary' t -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IPBoundary' t -> m (IPBoundary' t)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IPBoundary' t -> m (IPBoundary' t)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IPBoundary' t -> m (IPBoundary' t)

Show t => Show (IPBoundary' t) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> IPBoundary' t -> ShowS

show :: IPBoundary' t -> String

showList :: [IPBoundary' t] -> ShowS

Pretty c => Pretty (IPBoundary' c) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

Normalise t => Normalise (IPBoundary' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify t => Simplify (IPBoundary' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce t => Reduce (IPBoundary' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

ToConcrete a c => ToConcrete (IPBoundary' a) (IPBoundary' c) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

Reify a e => Reify (IPBoundary' a) (IPBoundary' e) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

Methods

reify :: MonadReify m => IPBoundary' a -> m (IPBoundary' e) Source #

reifyWhen :: MonadReify m => Bool -> IPBoundary' a -> m (IPBoundary' e) Source #

data Overapplied Source #

Flag to indicate whether the meta is overapplied in the constraint. A meta is overapplied if it has more arguments than the size of the telescope in its creation environment (as stored in MetaInfo).

Instances

Instances details
Eq Overapplied Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: Overapplied -> Overapplied -> Bool

(/=) :: Overapplied -> Overapplied -> Bool

Data Overapplied Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Overapplied -> c Overapplied

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Overapplied

toConstr :: Overapplied -> Constr

dataTypeOf :: Overapplied -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Overapplied)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Overapplied)

gmapT :: (forall b. Data b => b -> b) -> Overapplied -> Overapplied

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Overapplied -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Overapplied -> r

gmapQ :: (forall d. Data d => d -> u) -> Overapplied -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Overapplied -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Overapplied -> m Overapplied

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Overapplied -> m Overapplied

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Overapplied -> m Overapplied

Show Overapplied Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Overapplied -> ShowS

show :: Overapplied -> String

showList :: [Overapplied] -> ShowS

type InteractionPoints = Map InteractionId InteractionPoint Source #

Data structure managing the interaction points.

We never remove interaction points from this map, only set their ipSolved to True. (Issue #2368)

data InteractionPoint Source #

Interaction points are created by the scope checker who sets the range. The meta variable is created by the type checker and then hooked up to the interaction point.

Constructors

InteractionPoint 

Fields

  • ipRange :: Range

    The position of the interaction point.

  • ipMeta :: Maybe MetaId

    The meta variable, if any, holding the type etc.

  • ipSolved :: Bool

    Has this interaction point already been solved?

  • ipClause :: IPClause

    The clause of the interaction point (if any). Used for case splitting.

Instances

Instances details
Eq InteractionPoint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

type MetaNameSuggestion = String Source #

Name suggestion for meta variable. Empty string means no suggestion.

data MetaInfo Source #

MetaInfo is cloned from one meta to the next during pruning.

Constructors

MetaInfo 

Fields

newtype MetaPriority Source #

Meta variable priority: When we have an equation between meta-variables, which one should be instantiated?

Higher value means higher priority to be instantiated.

Constructors

MetaPriority Int 

Instances

Instances details
Eq MetaPriority Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: MetaPriority -> MetaPriority -> Bool

(/=) :: MetaPriority -> MetaPriority -> Bool

Ord MetaPriority Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show MetaPriority Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> MetaPriority -> ShowS

show :: MetaPriority -> String

showList :: [MetaPriority] -> ShowS

data TypeCheckingProblem Source #

Constructors

CheckExpr Comparison Expr Type 
CheckArgs ExpandHidden Range [NamedArg Expr] Type Type ([Maybe Range] -> Elims -> Type -> CheckedTarget -> TCM Term) 
CheckProjAppToKnownPrincipalArg Comparison Expr ProjOrigin (NonEmpty QName) Args Type Int Term Type 
CheckLambda Comparison (Arg ([WithHiding Name], Maybe Type)) Expr Type

(λ (xs : t₀) → e) : t This is not an instance of CheckExpr as the domain type has already been checked. For example, when checking (λ (x y : Fin _) → e) : (x : Fin n) → ? we want to postpone (λ (y : Fin n) → e) : ? where Fin n is a Type rather than an Expr.

DoQuoteTerm Comparison Term Type

Quote the given term and check type against Term

Instances

Instances details
PrettyTCM TypeCheckingProblem Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

data CheckedTarget Source #

Solving a CheckArgs constraint may or may not check the target type. If it did, it returns a handle to any unsolved constraints.

data MetaInstantiation Source #

Constructors

InstV [Arg String] Term

solved by term (abstracted over some free variables)

Open

unsolved

OpenInstance

open, to be instantiated by instance search

BlockedConst Term

solution blocked by unsolved constraints

PostponedTypeCheckingProblem (Closure TypeCheckingProblem) (TCM Bool) 

Instances

Instances details
Show MetaInstantiation Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> MetaInstantiation -> ShowS

show :: MetaInstantiation -> String

showList :: [MetaInstantiation] -> ShowS

data Frozen Source #

Frozen meta variable cannot be instantiated by unification. This serves to prevent the completion of a definition by its use outside of the current block. (See issues 118, 288, 399).

Constructors

Frozen

Do not instantiate.

Instantiable 

Instances

Instances details
Eq Frozen Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: Frozen -> Frozen -> Bool

(/=) :: Frozen -> Frozen -> Bool

Show Frozen Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Frozen -> ShowS

show :: Frozen -> String

showList :: [Frozen] -> ShowS

data Listener Source #

Instances

Instances details
Eq Listener Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: Listener -> Listener -> Bool

(/=) :: Listener -> Listener -> Bool

Ord Listener Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

compare :: Listener -> Listener -> Ordering

(<) :: Listener -> Listener -> Bool

(<=) :: Listener -> Listener -> Bool

(>) :: Listener -> Listener -> Bool

(>=) :: Listener -> Listener -> Bool

max :: Listener -> Listener -> Listener

min :: Listener -> Listener -> Listener

data MetaVariable Source #

Constructors

MetaVar 

Fields

data GeneralizedValue Source #

The value of a generalizable variable. This is created to be a generalizable meta before checking the type to be generalized.

Instances

Instances details
Data GeneralizedValue Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GeneralizedValue -> c GeneralizedValue

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GeneralizedValue

toConstr :: GeneralizedValue -> Constr

dataTypeOf :: GeneralizedValue -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c GeneralizedValue)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GeneralizedValue)

gmapT :: (forall b. Data b => b -> b) -> GeneralizedValue -> GeneralizedValue

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GeneralizedValue -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GeneralizedValue -> r

gmapQ :: (forall d. Data d => d -> u) -> GeneralizedValue -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> GeneralizedValue -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> GeneralizedValue -> m GeneralizedValue

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GeneralizedValue -> m GeneralizedValue

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GeneralizedValue -> m GeneralizedValue

Show GeneralizedValue Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> GeneralizedValue -> ShowS

show :: GeneralizedValue -> String

showList :: [GeneralizedValue] -> ShowS

data DoGeneralize Source #

Instances

Instances details
Eq DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: DoGeneralize -> DoGeneralize -> Bool

(/=) :: DoGeneralize -> DoGeneralize -> Bool

Data DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DoGeneralize -> c DoGeneralize

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DoGeneralize

toConstr :: DoGeneralize -> Constr

dataTypeOf :: DoGeneralize -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DoGeneralize)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DoGeneralize)

gmapT :: (forall b. Data b => b -> b) -> DoGeneralize -> DoGeneralize

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DoGeneralize -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DoGeneralize -> r

gmapQ :: (forall d. Data d => d -> u) -> DoGeneralize -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> DoGeneralize -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> DoGeneralize -> m DoGeneralize

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DoGeneralize -> m DoGeneralize

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DoGeneralize -> m DoGeneralize

Ord DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> DoGeneralize -> ShowS

show :: DoGeneralize -> String

showList :: [DoGeneralize] -> ShowS

KillRange DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj DoGeneralize Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DoGeneralize -> S Int32 Source #

icod_ :: DoGeneralize -> S Int32 Source #

value :: Int32 -> R DoGeneralize Source #

data Judgement a Source #

Parametrized since it is used without MetaId when creating a new meta.

Constructors

HasType 

Fields

IsSort 

Fields

Instances

Instances details
Show a => Show (Judgement a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Judgement a -> ShowS

show :: Judgement a -> String

showList :: [Judgement a] -> ShowS

PrettyTCM a => PrettyTCM (Judgement a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Judgement a -> m Doc Source #

data Open a Source #

A thing tagged with the context it came from.

Constructors

OpenThing 

Instances

Instances details
Functor Open Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fmap :: (a -> b) -> Open a -> Open b

(<$) :: a -> Open b -> Open a #

Foldable Open Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fold :: Monoid m => Open m -> m

foldMap :: Monoid m => (a -> m) -> Open a -> m

foldMap' :: Monoid m => (a -> m) -> Open a -> m

foldr :: (a -> b -> b) -> b -> Open a -> b

foldr' :: (a -> b -> b) -> b -> Open a -> b

foldl :: (b -> a -> b) -> b -> Open a -> b

foldl' :: (b -> a -> b) -> b -> Open a -> b

foldr1 :: (a -> a -> a) -> Open a -> a

foldl1 :: (a -> a -> a) -> Open a -> a

toList :: Open a -> [a]

null :: Open a -> Bool

length :: Open a -> Int

elem :: Eq a => a -> Open a -> Bool

maximum :: Ord a => Open a -> a

minimum :: Ord a => Open a -> a

sum :: Num a => Open a -> a

product :: Num a => Open a -> a

Traversable Open Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

traverse :: Applicative f => (a -> f b) -> Open a -> f (Open b)

sequenceA :: Applicative f => Open (f a) -> f (Open a)

mapM :: Monad m => (a -> m b) -> Open a -> m (Open b)

sequence :: Monad m => Open (m a) -> m (Open a)

Decoration Open Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

traverseF :: Functor m => (a -> m b) -> Open a -> m (Open b) Source #

distributeF :: Functor m => Open (m a) -> m (Open a) Source #

Data a => Data (Open a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Open a -> c (Open a)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Open a)

toConstr :: Open a -> Constr

dataTypeOf :: Open a -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Open a))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Open a))

gmapT :: (forall b. Data b => b -> b) -> Open a -> Open a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Open a -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Open a -> r

gmapQ :: (forall d. Data d => d -> u) -> Open a -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Open a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Open a -> m (Open a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Open a -> m (Open a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Open a -> m (Open a)

Show a => Show (Open a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Open a -> ShowS

show :: Open a -> String

showList :: [Open a] -> ShowS

KillRange a => KillRange (Open a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj a => EmbPrj (Open a) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Open a -> S Int32 Source #

icod_ :: Open a -> S Int32 Source #

value :: Int32 -> R (Open a) Source #

NamesIn a => NamesIn (Open a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Open a -> Set QName Source #

InstantiateFull t => InstantiateFull (Open t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

data CompareAs Source #

We can either compare two terms at a given type, or compare two types without knowing (or caring about) their sorts.

Constructors

AsTermsOf Type

Type should not be Size. But currently, we do not rely on this invariant.

AsSizes

Replaces AsTermsOf Size.

AsTypes 

Instances

Instances details
Eq CompareAs 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

(==) :: CompareAs -> CompareAs -> Bool

(/=) :: CompareAs -> CompareAs -> Bool

Data CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CompareAs -> c CompareAs

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CompareAs

toConstr :: CompareAs -> Constr

dataTypeOf :: CompareAs -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CompareAs)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CompareAs)

gmapT :: (forall b. Data b => b -> b) -> CompareAs -> CompareAs

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CompareAs -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CompareAs -> r

gmapQ :: (forall d. Data d => d -> u) -> CompareAs -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> CompareAs -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> CompareAs -> m CompareAs

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CompareAs -> m CompareAs

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CompareAs -> m CompareAs

Show CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> CompareAs -> ShowS

show :: CompareAs -> String

showList :: [CompareAs] -> ShowS

Free CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

freeVars' :: IsVarSet a c => CompareAs -> FreeM a c Source #

TermLike CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

traverseTermM :: Monad m => (Term -> m Term) -> CompareAs -> m CompareAs Source #

foldTerm :: Monoid m => (Term -> m) -> CompareAs -> m Source #

PrettyTCM CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

IsSizeType CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

isSizeType :: (HasOptions m, HasBuiltins m) => CompareAs -> m (Maybe BoundedSize) Source #

MentionsMeta CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

InstantiateFull CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

IsMeta CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: HasBuiltins m => CompareAs -> m (Maybe MetaId) Source #

Instantiate CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Subst Term CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

data CompareDirection Source #

An extension of Comparison to >=.

Constructors

DirEq 
DirLeq 
DirGeq 

Instances

Instances details
Eq CompareDirection Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Show CompareDirection Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> CompareDirection -> ShowS

show :: CompareDirection -> String

showList :: [CompareDirection] -> ShowS

Pretty CompareDirection Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

data Constraint Source #

Constructors

ValueCmp Comparison CompareAs Term Term 
ValueCmpOnFace Comparison Term Type Term Term 
ElimCmp [Polarity] [IsForced] Type Term [Elim] [Elim] 
TelCmp Type Type Comparison Telescope Telescope

the two types are for the error message only

SortCmp Comparison Sort Sort 
LevelCmp Comparison Level Level 
HasBiggerSort Sort 
HasPTSRule (Dom Type) (Abs Sort) 
CheckMetaInst MetaId 
UnBlock MetaId 
Guarded Constraint ProblemId 
IsEmpty Range Type

The range is the one of the absurd pattern.

CheckSizeLtSat Term

Check that the Term is either not a SIZELT or a non-empty SIZELT.

FindInstance MetaId (Maybe MetaId) (Maybe [Candidate])

the first argument is the instance argument, the second one is the meta on which the constraint may be blocked on and the third one is the list of candidates (or Nothing if we haven’t determined the list of candidates yet)

CheckFunDef Delayed DefInfo QName [Clause] 
UnquoteTactic (Maybe MetaId) Term Term Type

First argument is computation and the others are hole and goal type

Instances

Instances details
Data Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Constraint -> c Constraint

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Constraint

toConstr :: Constraint -> Constr

dataTypeOf :: Constraint -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Constraint)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constraint)

gmapT :: (forall b. Data b => b -> b) -> Constraint -> Constraint

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Constraint -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Constraint -> r

gmapQ :: (forall d. Data d => d -> u) -> Constraint -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Constraint -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Constraint -> m Constraint

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Constraint -> m Constraint

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Constraint -> m Constraint

Show Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Constraint -> ShowS

show :: Constraint -> String

showList :: [Constraint] -> ShowS

HasRange Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Free Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

freeVars' :: IsVarSet a c => Constraint -> FreeM a c Source #

TermLike Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Constraint -> m Constraint Source #

foldTerm :: Monoid m => (Term -> m) -> Constraint -> m Source #

PrettyTCM Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

MentionsMeta Constraint Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

InstantiateFull Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Subst Term Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Reify Constraint (OutputConstraint Expr Expr) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

data ProblemConstraint Source #

Instances

Instances details
Data ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProblemConstraint -> c ProblemConstraint

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProblemConstraint

toConstr :: ProblemConstraint -> Constr

dataTypeOf :: ProblemConstraint -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProblemConstraint)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProblemConstraint)

gmapT :: (forall b. Data b => b -> b) -> ProblemConstraint -> ProblemConstraint

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProblemConstraint -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProblemConstraint -> r

gmapQ :: (forall d. Data d => d -> u) -> ProblemConstraint -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ProblemConstraint -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProblemConstraint -> m ProblemConstraint

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemConstraint -> m ProblemConstraint

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemConstraint -> m ProblemConstraint

Show ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> ProblemConstraint -> ShowS

show :: ProblemConstraint -> String

showList :: [ProblemConstraint] -> ShowS

HasRange ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

MentionsMeta ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

InstantiateFull ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reify ProblemConstraint (Closure (OutputForm Expr Expr)) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

class LensClosure a b | b -> a where Source #

Methods

lensClosure :: Lens' (Closure a) b Source #

data Closure a Source #

Instances

Instances details
Functor Closure Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fmap :: (a -> b) -> Closure a -> Closure b

(<$) :: a -> Closure b -> Closure a #

Foldable Closure Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fold :: Monoid m => Closure m -> m

foldMap :: Monoid m => (a -> m) -> Closure a -> m

foldMap' :: Monoid m => (a -> m) -> Closure a -> m

foldr :: (a -> b -> b) -> b -> Closure a -> b

foldr' :: (a -> b -> b) -> b -> Closure a -> b

foldl :: (b -> a -> b) -> b -> Closure a -> b

foldl' :: (b -> a -> b) -> b -> Closure a -> b

foldr1 :: (a -> a -> a) -> Closure a -> a

foldl1 :: (a -> a -> a) -> Closure a -> a

toList :: Closure a -> [a]

null :: Closure a -> Bool

length :: Closure a -> Int

elem :: Eq a => a -> Closure a -> Bool

maximum :: Ord a => Closure a -> a

minimum :: Ord a => Closure a -> a

sum :: Num a => Closure a -> a

product :: Num a => Closure a -> a

LensClosure a (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Reify ProblemConstraint (Closure (OutputForm Expr Expr)) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

Data a => Data (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Closure a -> c (Closure a)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Closure a)

toConstr :: Closure a -> Constr

dataTypeOf :: Closure a -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Closure a))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Closure a))

gmapT :: (forall b. Data b => b -> b) -> Closure a -> Closure a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Closure a -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Closure a -> r

gmapQ :: (forall d. Data d => d -> u) -> Closure a -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Closure a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Closure a -> m (Closure a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Closure a -> m (Closure a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Closure a -> m (Closure a)

Show a => Show (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Closure a -> ShowS

show :: Closure a -> String

showList :: [Closure a] -> ShowS

KillRange a => KillRange (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasRange a => HasRange (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getRange :: Closure a -> Range Source #

LensIsAbstract (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

LensTCEnv (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

PrettyTCM a => PrettyTCM (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Closure a -> m Doc Source #

MentionsMeta a => MentionsMeta (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Closure a -> Bool Source #

InstantiateFull a => InstantiateFull (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Normalise a => Normalise (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Simplify a => Simplify (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Reduce a => Reduce (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Instantiate a => Instantiate (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

data Interface Source #

Constructors

Interface 

Fields

Instances

Instances details
Show Interface Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> Interface -> ShowS

show :: Interface -> String

showList :: [Interface] -> ShowS

Pretty Interface Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj Interface Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances

Methods

icode :: Interface -> S Int32 Source #

icod_ :: Interface -> S Int32 Source #

value :: Int32 -> R Interface Source #

InstantiateFull Interface Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

data ForeignCode Source #

Constructors

ForeignCode Range String 

Instances

Instances details
Show ForeignCode Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> ForeignCode -> ShowS

show :: ForeignCode -> String

showList :: [ForeignCode] -> ShowS

EmbPrj ForeignCode Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Compilers

Methods

icode :: ForeignCode -> S Int32 Source #

icod_ :: ForeignCode -> S Int32 Source #

value :: Int32 -> R ForeignCode Source #

data ModuleInfo Source #

Constructors

ModuleInfo 

Fields

  • miInterface :: Interface
     
  • miWarnings :: Bool

    True if warnings were encountered when the module was type checked.

  • miPrimitive :: Bool

    True if the module is a primitive module, which should always be importable.

class Monad m => MonadStConcreteNames m where Source #

A monad that has read and write access to the stConcreteNames part of the TCState. Basically, this is a synonym for `MonadState ConcreteNames m` (which cannot be used directly because of the limitations of Haskell's typeclass system).

Minimal complete definition

runStConcreteNames

Instances

Instances details
MonadStConcreteNames TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

MonadStConcreteNames AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ReadTCState m => MonadStConcreteNames (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

MonadStConcreteNames m => MonadStConcreteNames (ReaderT r m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

runStConcreteNames :: StateT ConcreteNames (ReaderT r m) a -> ReaderT r m a Source #

useConcreteNames :: ReaderT r m ConcreteNames Source #

modifyConcreteNames :: (ConcreteNames -> ConcreteNames) -> ReaderT r m () Source #

MonadStConcreteNames m => MonadStConcreteNames (StateT s m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

runStConcreteNames :: StateT ConcreteNames (StateT s m) a -> StateT s m a Source #

useConcreteNames :: StateT s m ConcreteNames Source #

modifyConcreteNames :: (ConcreteNames -> ConcreteNames) -> StateT s m () Source #

type SourceToModule = Map AbsolutePath TopLevelModuleName Source #

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

class FreshName a where Source #

Create a fresh name from a.

Methods

freshName_ :: MonadFresh NameId m => a -> m Name Source #

Instances

Instances details
FreshName () Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

freshName_ :: MonadFresh NameId m => () -> m Name Source #

FreshName String Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

freshName_ :: MonadFresh NameId m => String -> m Name Source #

FreshName Range Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

FreshName (Range, String) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

freshName_ :: MonadFresh NameId m => (Range, String) -> m Name Source #

newtype CheckpointId Source #

Constructors

CheckpointId Int 

Instances

Instances details
Enum CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Eq CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: CheckpointId -> CheckpointId -> Bool

(/=) :: CheckpointId -> CheckpointId -> Bool

Integral CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Data CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CheckpointId -> c CheckpointId

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CheckpointId

toConstr :: CheckpointId -> Constr

dataTypeOf :: CheckpointId -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CheckpointId)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CheckpointId)

gmapT :: (forall b. Data b => b -> b) -> CheckpointId -> CheckpointId

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CheckpointId -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CheckpointId -> r

gmapQ :: (forall d. Data d => d -> u) -> CheckpointId -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> CheckpointId -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> CheckpointId -> m CheckpointId

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CheckpointId -> m CheckpointId

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CheckpointId -> m CheckpointId

Num CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Ord CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Real CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

toRational :: CheckpointId -> Rational

Show CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> CheckpointId -> ShowS

show :: CheckpointId -> String

showList :: [CheckpointId] -> ShowS

Pretty CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

HasFresh CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

EmbPrj CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: CheckpointId -> S Int32 Source #

icod_ :: CheckpointId -> S Int32 Source #

value :: Int32 -> R CheckpointId Source #

PrettyTCM CheckpointId Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

class Monad m => MonadFresh i m where Source #

Methods

fresh :: m i Source #

Instances

Instances details
HasFresh i => MonadFresh i TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fresh :: TCM i Source #

Monad m => MonadFresh Int (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

fresh :: PureConversionT m Int Source #

Monad m => MonadFresh NameId (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Monad m => MonadFresh ProblemId (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

MonadFresh i m => MonadFresh i (StateT s m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fresh :: StateT s m i Source #

MonadFresh i m => MonadFresh i (ReaderT r m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fresh :: ReaderT r m i Source #

data TypeCheckAction Source #

A complete log for a module will look like this:

type CurrentTypeCheckLog = [(TypeCheckAction, PostScopeState)] Source #

Like CachedTypeCheckLog, but storing the log for an ongoing type checking of a module. Stored in reverse order (last performed action first).

type CachedTypeCheckLog = [(TypeCheckAction, PostScopeState)] Source #

A log of what the type checker does and states after the action is completed. The cached version is stored first executed action first.

data PersistentTCState Source #

A part of the state which is not reverted when an error is thrown or the state is reset.

Constructors

PersistentTCSt 

Fields

Instances

Instances details
LensPersistentVerbosity PersistentTCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensIncludePaths PersistentTCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensSafeMode PersistentTCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

LensCommandLineOptions PersistentTCState Source # 
Instance details

Defined in Agda.Interaction.Options.Lenses

data MutualBlock Source #

A mutual block of names in the signature.

Constructors

MutualBlock 

Fields

Instances

Instances details
Eq MutualBlock Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

(==) :: MutualBlock -> MutualBlock -> Bool

(/=) :: MutualBlock -> MutualBlock -> Bool

Show MutualBlock Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

showsPrec :: Int -> MutualBlock -> ShowS

show :: MutualBlock -> String

showList :: [MutualBlock] -> ShowS

Null MutualBlock Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

data PostScopeState Source #

Constructors

PostScopeState 

Fields

data PreScopeState Source #

Constructors

PreScopeState 

Fields

class Monad m => ReadTCState m where Source #

Minimal complete definition

getTCState, locallyTCState

Methods

getTCState :: m TCState Source #

locallyTCState :: Lens' a TCState -> (a -> a) -> m b -> m b Source #

withTCState :: (TCState -> TCState) -> m a -> m a Source #

Instances

Instances details
ReadTCState ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

ReadTCState AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ReadTCState TerM Source # 
Instance details

Defined in Agda.Termination.Monad

ReadTCState m => ReadTCState (MaybeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: MaybeT m TCState Source #

locallyTCState :: Lens' a TCState -> (a -> a) -> MaybeT m b -> MaybeT m b Source #

withTCState :: (TCState -> TCState) -> MaybeT m a -> MaybeT m a Source #

ReadTCState m => ReadTCState (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: ListT m TCState Source #

locallyTCState :: Lens' a TCState -> (a -> a) -> ListT m b -> ListT m b Source #

withTCState :: (TCState -> TCState) -> ListT m a -> ListT m a Source #

MonadIO m => ReadTCState (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: TCMT m TCState Source #

locallyTCState :: Lens' a TCState -> (a -> a) -> TCMT m b -> TCMT m b Source #

withTCState :: (TCState -> TCState) -> TCMT m a -> TCMT m a Source #

ReadTCState m => ReadTCState (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

Methods

getTCState :: NamesT m TCState Source #

locallyTCState :: Lens' a TCState -> (a -> a) -> NamesT m b -> NamesT m b Source #

withTCState :: (TCState -> TCState) -> NamesT m a -> NamesT m a Source #

ReadTCState m => ReadTCState (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

ReadTCState m => ReadTCState (ExceptT err m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: ExceptT err m TCState Source #

locallyTCState :: Lens' a TCState -> (a -> a) -> ExceptT err m b -> ExceptT err m b Source #

withTCState :: (TCState -> TCState) -> ExceptT err m a -> ExceptT err m a Source #

ReadTCState m => ReadTCState (ReaderT r m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: ReaderT r m TCState Source #

locallyTCState :: Lens' a TCState -> (a -> a) -> ReaderT r m b -> ReaderT r m b Source #

withTCState :: (TCState -> TCState) -> ReaderT r m a -> ReaderT r m a Source #

ReadTCState m => ReadTCState (StateT s m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: StateT s m TCState Source #

locallyTCState :: Lens' a TCState -> (a -> a) -> StateT s m b -> StateT s m b Source #

withTCState :: (TCState -> TCState) -> StateT s m a -> StateT s m a Source #

(Monoid w, ReadTCState m) => ReadTCState (WriterT w m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getTCState :: WriterT w m TCState Source #

locallyTCState :: Lens' a TCState -> (a -> a) -> WriterT w m b -> WriterT w m b Source #

withTCState :: (TCState -> TCState) -> WriterT w m a -> WriterT w m a Source #

initPersistentState :: PersistentTCState Source #

Empty persistent state.

initPreScopeState :: PreScopeState Source #

Empty state of type checker.

getUserWarnings :: ReadTCState m => m (Map QName String) Source #

freshName :: MonadFresh NameId m => Range -> String -> m Name Source #

sourceToModule :: TCM SourceToModule Source #

Creates a SourceToModule map based on stModuleToSource.

O(n log n).

For a single reverse lookup in stModuleToSource, rather use lookupModuleFromSourse.

iFullHash :: Interface -> Hash Source #

Combines the source hash and the (full) hashes of the imported modules.

flipCmp :: CompareDirection -> CompareDirection Source #

Flip the direction of comparison.

dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c Source #

Turn a Comparison function into a CompareDirection function.

Property: dirToCmp f (fromCmp cmp) = f cmp

defaultDisplayForm :: QName -> [LocalDisplayForm] Source #

By default, we have no display form.

defaultDefn :: ArgInfo -> QName -> Type -> Defn -> Definition Source #

Create a definition with sensible defaults.

projDropPars :: Projection -> ProjOrigin -> Term Source #

Building the projection function (which drops the parameters).

projArgInfo :: Projection -> ArgInfo Source #

The info of the principal (record) argument.

setEtaEquality :: EtaEquality -> HasEta -> EtaEquality Source #

Make sure we do not overwrite a user specification.

recRecursive :: Defn -> Bool Source #

Is the record type recursive?

emptyFunction :: Defn Source #

A template for creating Function definitions, with sensible defaults.

isMacro :: Defn -> Bool Source #

isEmptyFunction :: Defn -> Bool Source #

Checking whether we are dealing with a function yet to be defined.

redBind :: ReduceM (Reduced a a') -> (a -> b) -> (a' -> ReduceM (Reduced b b')) -> ReduceM (Reduced b b') Source #

Conceptually: redBind m f k = either (return . Left . f) k =<< m

allReductions :: AllowedReductions Source #

Not quite all reductions (skip non-terminating reductions)

defDelayed :: Definition -> Delayed Source #

Are the clauses of this definition delayed?

defNonterminating :: Definition -> Bool Source #

Has the definition failed the termination checker?

defTerminationUnconfirmed :: Definition -> Bool Source #

Has the definition not termination checked or did the check fail?

ifTopLevelAndHighlightingLevelIsOr :: MonadTCM tcm => HighlightingLevel -> Bool -> tcm () -> tcm () Source #

ifTopLevelAndHighlightingLevelIs l b m runs m when we're type-checking the top-level module and either the highlighting level is at least l or b is True.

ifTopLevelAndHighlightingLevelIs :: MonadTCM tcm => HighlightingLevel -> tcm () -> tcm () Source #

ifTopLevelAndHighlightingLevelIs l m runs m when we're type-checking the top-level module and the highlighting level is at least l.

getIncludeDirs :: HasOptions m => m [AbsolutePath] Source #

Gets the include directories.

Precondition: optAbsoluteIncludePaths must be nonempty (i.e. setCommandLineOptions must have run).

fmapReduce :: (a -> b) -> ReduceM a -> ReduceM b Source #

apReduce :: ReduceM (a -> b) -> ReduceM a -> ReduceM b Source #

bindReduce :: ReduceM a -> (a -> ReduceM b) -> ReduceM b Source #

runReduceF :: (a -> ReduceM b) -> TCM (a -> b) Source #

asksTC :: MonadTCEnv m => (TCEnv -> a) -> m a Source #

viewTC :: MonadTCEnv m => Lens' a TCEnv -> m a Source #

locallyTC :: MonadTCEnv m => Lens' a TCEnv -> (a -> a) -> m b -> m b Source #

Modify the lens-indicated part of the TCEnv in a subcomputation.

getsTC :: ReadTCState m => (TCState -> a) -> m a Source #

modifyTC' :: MonadTCState m => (TCState -> TCState) -> m () Source #

A variant of modifyTC in which the computation is strict in the new state.

setTCLens :: MonadTCState m => Lens' a TCState -> a -> m () infix 4 Source #

Overwrite the part of the TCState focused on by the lens.

modifyTCLens :: MonadTCState m => Lens' a TCState -> (a -> a) -> m () Source #

Modify the part of the TCState focused on by the lens.

modifyTCLensM :: MonadTCState m => Lens' a TCState -> (a -> m a) -> m () Source #

Modify a part of the state monadically.

stateTCLens :: MonadTCState m => Lens' a TCState -> (a -> (r, a)) -> m r Source #

Modify the part of the TCState focused on by the lens, and return some result.

stateTCLensM :: MonadTCState m => Lens' a TCState -> (a -> m (r, a)) -> m r Source #

Modify a part of the state monadically, and return some result.

mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n a Source #

pureTCM :: MonadIO m => (TCState -> TCEnv -> a) -> TCMT m a Source #

returnTCMT :: MonadIO m => a -> TCMT m a Source #

bindTCMT :: MonadIO m => TCMT m a -> (a -> TCMT m b) -> TCMT m b Source #

thenTCMT :: MonadIO m => TCMT m a -> TCMT m b -> TCMT m b Source #

fmapTCMT :: MonadIO m => (a -> b) -> TCMT m a -> TCMT m b Source #

apTCMT :: MonadIO m => TCMT m (a -> b) -> TCMT m a -> TCMT m b Source #

runIM :: IM a -> TCM a Source #

catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a Source #

Preserve the state of the failing computation.

finally_ :: TCM a -> TCM b -> TCM a Source #

Execute a finalizer even when an exception is thrown. Does not catch any errors. In case both the regular computation and the finalizer throw an exception, the one of the finalizer is propagated.

internalError :: MonadTCM tcm => String -> tcm a Source #

runTCM :: MonadIO m => TCEnv -> TCState -> TCMT m a -> m (a, TCState) Source #

Running the type checking monad (most general form).

runTCMTop :: TCM a -> IO (Either TCErr a) Source #

Running the type checking monad on toplevel (with initial state).

runTCMTop' :: MonadIO m => TCMT m a -> m a Source #

runSafeTCM :: TCM a -> TCState -> IO (a, TCState) Source #

runSafeTCM runs a safe TCM action (a TCM action which cannot fail) in the initial environment.

forkTCM :: TCM a -> TCM () Source #

Runs the given computation in a separate thread, with a copy of the current state and environment.

Note that Agda sometimes uses actual, mutable state. If the computation given to forkTCM tries to modify this state, then bad things can happen, because accesses are not mutually exclusive. The forkTCM function has been added mainly to allow the thread to read (a snapshot of) the current state in a convenient way.

Note also that exceptions which are raised in the thread are not propagated to the parent, so the thread should not do anything important.

patternInTeleName :: String Source #

Base name for patterns in telescopes

extendedLambdaName :: String Source #

Base name for extended lambda patterns

isExtendedLambdaName :: QName -> Bool Source #

Check whether we have an definition from an extended lambda.

absurdLambdaName :: String Source #

Name of absurdLambda definitions.

isAbsurdLambdaName :: QName -> Bool Source #

Check whether we have an definition from an absurd lambda.

generalizedFieldName :: String Source #

Base name for generalized variable projections

getGeneralizedFieldName :: QName -> Maybe String Source #

Check whether we have a generalized variable field

checkForImportCycle :: TCM () Source #

Assumes that the first module in the import path is the module we are worried about.

currentModule :: MonadTCEnv m => m ModuleName Source #

Get the name of the current module, if any.

withCurrentModule :: MonadTCEnv m => ModuleName -> m a -> m a Source #

Set the name of the current module.

getCurrentPath :: MonadTCEnv m => m AbsolutePath Source #

Get the path of the currently checked file

getAnonymousVariables :: MonadTCEnv m => ModuleName -> m Nat Source #

Get the number of variables bound by anonymous modules.

withAnonymousModule :: ModuleName -> Nat -> TCM a -> TCM a Source #

Add variables bound by an anonymous module.

withEnv :: MonadTCEnv m => TCEnv -> m a -> m a Source #

Set the current environment to the given

getEnv :: TCM TCEnv Source #

Get the current environment

withIncreasedModuleNestingLevel :: TCM a -> TCM a Source #

Increases the module nesting level by one in the given computation.

withHighlightingLevel :: HighlightingLevel -> TCM a -> TCM a Source #

Set highlighting level

doExpandLast :: TCM a -> TCM a Source #

Restore setting for ExpandLast to default.

performedSimplification :: MonadTCEnv m => m a -> m a Source #

If the reduced did a proper match (constructor or literal pattern), then record this as simplification step.

onlyReduceProjections :: MonadTCEnv m => m a -> m a Source #

Reduce Def f vs only if f is a projection.

allowAllReductions :: MonadTCEnv m => m a -> m a Source #

Allow all reductions except for non-terminating functions (default).

allowNonTerminatingReductions :: MonadTCEnv m => m a -> m a Source #

Allow all reductions including non-terminating functions.

onlyReduceTypes :: MonadTCEnv m => m a -> m a Source #

Allow all reductions when reducing types

typeLevelReductions :: MonadTCEnv m => m a -> m a Source #

Update allowed reductions when working on types

callByName :: TCM a -> TCM a Source #

Don't use call-by-need evaluation for the given computation.

class MonadTCEnv m => MonadAddContext m where Source #

Methods

addCtx :: Name -> Dom Type -> m a -> m a Source #

addCtx x arg cont add a variable to the context.

Chooses an unused Name.

Warning: Does not update module parameter substitution!

addLetBinding' :: Name -> Term -> Dom Type -> m a -> m a Source #

Add a let bound variable to the context

updateContext :: Substitution -> (Context -> Context) -> m a -> m a Source #

Update the context. Requires a substitution that transports things living in the old context to the new.

withFreshName :: Range -> ArgName -> (Name -> m a) -> m a Source #

Instances

Instances details
MonadAddContext TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> TCM a -> TCM a Source #

addLetBinding' :: Name -> Term -> Dom Type -> TCM a -> TCM a Source #

updateContext :: Substitution -> (Context -> Context) -> TCM a -> TCM a Source #

withFreshName :: Range -> ArgName -> (Name -> TCM a) -> TCM a Source #

MonadAddContext ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Reduce.Monad

MonadAddContext TerM Source # 
Instance details

Defined in Agda.Termination.Monad

MonadAddContext m => MonadAddContext (MaybeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> MaybeT m a -> MaybeT m a Source #

addLetBinding' :: Name -> Term -> Dom Type -> MaybeT m a -> MaybeT m a Source #

updateContext :: Substitution -> (Context -> Context) -> MaybeT m a -> MaybeT m a Source #

withFreshName :: Range -> ArgName -> (Name -> MaybeT m a) -> MaybeT m a Source #

MonadAddContext m => MonadAddContext (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> ListT m a -> ListT m a Source #

addLetBinding' :: Name -> Term -> Dom Type -> ListT m a -> ListT m a Source #

updateContext :: Substitution -> (Context -> Context) -> ListT m a -> ListT m a Source #

withFreshName :: Range -> ArgName -> (Name -> ListT m a) -> ListT m a Source #

MonadAddContext m => MonadAddContext (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

Methods

addCtx :: Name -> Dom Type -> NamesT m a -> NamesT m a Source #

addLetBinding' :: Name -> Term -> Dom Type -> NamesT m a -> NamesT m a Source #

updateContext :: Substitution -> (Context -> Context) -> NamesT m a -> NamesT m a Source #

withFreshName :: Range -> ArgName -> (Name -> NamesT m a) -> NamesT m a Source #

MonadAddContext m => MonadAddContext (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

MonadAddContext m => MonadAddContext (ExceptT e m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> ExceptT e m a -> ExceptT e m a Source #

addLetBinding' :: Name -> Term -> Dom Type -> ExceptT e m a -> ExceptT e m a Source #

updateContext :: Substitution -> (Context -> Context) -> ExceptT e m a -> ExceptT e m a Source #

withFreshName :: Range -> ArgName -> (Name -> ExceptT e m a) -> ExceptT e m a Source #

MonadAddContext m => MonadAddContext (ReaderT r m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> ReaderT r m a -> ReaderT r m a Source #

addLetBinding' :: Name -> Term -> Dom Type -> ReaderT r m a -> ReaderT r m a Source #

updateContext :: Substitution -> (Context -> Context) -> ReaderT r m a -> ReaderT r m a Source #

withFreshName :: Range -> ArgName -> (Name -> ReaderT r m a) -> ReaderT r m a Source #

MonadAddContext m => MonadAddContext (StateT r m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> StateT r m a -> StateT r m a Source #

addLetBinding' :: Name -> Term -> Dom Type -> StateT r m a -> StateT r m a Source #

updateContext :: Substitution -> (Context -> Context) -> StateT r m a -> StateT r m a Source #

withFreshName :: Range -> ArgName -> (Name -> StateT r m a) -> StateT r m a Source #

(Monoid w, MonadAddContext m) => MonadAddContext (WriterT w m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> WriterT w m a -> WriterT w m a Source #

addLetBinding' :: Name -> Term -> Dom Type -> WriterT w m a -> WriterT w m a Source #

updateContext :: Substitution -> (Context -> Context) -> WriterT w m a -> WriterT w m a Source #

withFreshName :: Range -> ArgName -> (Name -> WriterT w m a) -> WriterT w m a Source #

checkpointSubstitution :: MonadTCEnv tcm => CheckpointId -> tcm Substitution Source #

Get the substitution from the context at a given checkpoint to the current context.

class (Functor m, Applicative m, MonadFail m) => HasBuiltins m where Source #

Methods

getBuiltinThing :: String -> m (Maybe (Builtin PrimFun)) Source #

Instances

Instances details
HasBuiltins ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Reduce.Monad

Methods

getBuiltinThing :: String -> ReduceM (Maybe (Builtin PrimFun)) Source #

HasBuiltins TerM Source # 
Instance details

Defined in Agda.Termination.Monad

Methods

getBuiltinThing :: String -> TerM (Maybe (Builtin PrimFun)) Source #

HasBuiltins m => HasBuiltins (MaybeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: String -> MaybeT m (Maybe (Builtin PrimFun)) Source #

HasBuiltins m => HasBuiltins (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: String -> ListT m (Maybe (Builtin PrimFun)) Source #

MonadIO m => HasBuiltins (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: String -> TCMT m (Maybe (Builtin PrimFun)) Source #

HasBuiltins m => HasBuiltins (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

Methods

getBuiltinThing :: String -> NamesT m (Maybe (Builtin PrimFun)) Source #

HasBuiltins m => HasBuiltins (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

getBuiltinThing :: String -> PureConversionT m (Maybe (Builtin PrimFun)) Source #

HasBuiltins m => HasBuiltins (ExceptT e m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: String -> ExceptT e m (Maybe (Builtin PrimFun)) Source #

HasBuiltins m => HasBuiltins (ReaderT e m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: String -> ReaderT e m (Maybe (Builtin PrimFun)) Source #

HasBuiltins m => HasBuiltins (StateT s m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: String -> StateT s m (Maybe (Builtin PrimFun)) Source #

(HasBuiltins m, Monoid w) => HasBuiltins (WriterT w m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: String -> WriterT w m (Maybe (Builtin PrimFun)) Source #

class TraceS a where Source #

Debug print some lines if the verbosity level for the given VerboseKey is at least VerboseLevel.

Note: In the presence of OverloadedStrings, just @ traceS key level "Literate string" gives an Ambiguous type variable error in GHC@. Use the legacy functions traceSLn and traceSDoc instead then.

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> a -> m c -> m c Source #

Instances

Instances details
TraceS String Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m c -> m c Source #

TraceS Doc Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> Doc -> m c -> m c Source #

TraceS [String] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [String] -> m c -> m c Source #

TraceS [Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [Doc] -> m c -> m c Source #

TraceS [TCM Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m c -> m c Source #

TraceS (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c Source #

class ReportS a where Source #

Debug print some lines if the verbosity level for the given VerboseKey is at least VerboseLevel.

Note: In the presence of OverloadedStrings, just @ reportS key level "Literate string" gives an Ambiguous type variable error in GHC@. Use the legacy functions reportSLn and reportSDoc instead then.

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> a -> m () Source #

Instances

Instances details
ReportS String Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m () Source #

ReportS Doc Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> Doc -> m () Source #

ReportS [String] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [String] -> m () Source #

ReportS [Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [Doc] -> m () Source #

ReportS [TCM Doc] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m () Source #

ReportS (TCM Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m () Source #

class (Functor m, Applicative m, Monad m) => MonadDebug m where Source #

Minimal complete definition

formatDebugMessage, verboseBracket

Methods

displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> m () Source #

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> m a -> m a Source #

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> m String Source #

getVerbosity :: m Verbosity Source #

isDebugPrinting :: m Bool Source #

default isDebugPrinting :: MonadTCEnv m => m Bool Source #

nowDebugPrinting :: m a -> m a Source #

default nowDebugPrinting :: MonadTCEnv m => m a -> m a Source #

verboseBracket :: VerboseKey -> VerboseLevel -> String -> m a -> m a Source #

Print brackets around debug messages issued by a computation.

Instances

Instances details
MonadDebug TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

MonadDebug ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Reduce.Monad

MonadDebug AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

MonadDebug TerM Source # 
Instance details

Defined in Agda.Termination.Monad

MonadDebug m => MonadDebug (MaybeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> MaybeT m () Source #

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> MaybeT m a -> MaybeT m a Source #

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> MaybeT m String Source #

getVerbosity :: MaybeT m Verbosity Source #

isDebugPrinting :: MaybeT m Bool Source #

nowDebugPrinting :: MaybeT m a -> MaybeT m a Source #

verboseBracket :: VerboseKey -> VerboseLevel -> String -> MaybeT m a -> MaybeT m a Source #

MonadDebug m => MonadDebug (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

MonadDebug m => MonadDebug (ChangeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

MonadDebug m => MonadDebug (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

MonadDebug m => MonadDebug (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

MonadDebug m => MonadDebug (ExceptT e m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

MonadDebug m => MonadDebug (IdentityT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> IdentityT m () Source #

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> IdentityT m a -> IdentityT m a Source #

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> IdentityT m String Source #

getVerbosity :: IdentityT m Verbosity Source #

isDebugPrinting :: IdentityT m Bool Source #

nowDebugPrinting :: IdentityT m a -> IdentityT m a Source #

verboseBracket :: VerboseKey -> VerboseLevel -> String -> IdentityT m a -> IdentityT m a Source #

MonadDebug m => MonadDebug (ReaderT r m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> ReaderT r m () Source #

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> ReaderT r m a -> ReaderT r m a Source #

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> ReaderT r m String Source #

getVerbosity :: ReaderT r m Verbosity Source #

isDebugPrinting :: ReaderT r m Bool Source #

nowDebugPrinting :: ReaderT r m a -> ReaderT r m a Source #

verboseBracket :: VerboseKey -> VerboseLevel -> String -> ReaderT r m a -> ReaderT r m a Source #

MonadDebug m => MonadDebug (StateT s m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> StateT s m () Source #

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> StateT s m a -> StateT s m a Source #

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> StateT s m String Source #

getVerbosity :: StateT s m Verbosity Source #

isDebugPrinting :: StateT s m Bool Source #

nowDebugPrinting :: StateT s m a -> StateT s m a Source #

verboseBracket :: VerboseKey -> VerboseLevel -> String -> StateT s m a -> StateT s m a Source #

(MonadDebug m, Monoid w) => MonadDebug (WriterT w m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> WriterT w m () Source #

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> WriterT w m a -> WriterT w m a Source #

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> WriterT w m String Source #

getVerbosity :: WriterT w m Verbosity Source #

isDebugPrinting :: WriterT w m Bool Source #

nowDebugPrinting :: WriterT w m a -> WriterT w m a Source #

verboseBracket :: VerboseKey -> VerboseLevel -> String -> WriterT w m a -> WriterT w m a Source #

catchAndPrintImpossible :: (CatchImpossible m, Monad m) => VerboseKey -> VerboseLevel -> m String -> m String Source #

During printing, catch internal errors of kind Impossible and print them.

reportSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m () Source #

Conditionally println debug string.

__IMPOSSIBLE_VERBOSE__ :: (HasCallStack, MonadDebug m) => String -> m a Source #

reportSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m () Source #

Conditionally render debug Doc and print it.

reportResult :: MonadDebug m => VerboseKey -> VerboseLevel -> (a -> TCM Doc) -> m a -> m a Source #

Debug print the result of a computation.

unlessDebugPrinting :: MonadDebug m => m () -> m () Source #

traceSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m a -> m a Source #

traceSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m a -> m a Source #

Conditionally render debug Doc, print it, and then continue.

hasVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m Bool Source #

Check whether a certain verbosity level is activated.

Precondition: The level must be non-negative.

hasExactVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m Bool Source #

Check whether a certain verbosity level is activated (exact match).

whenExactVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m () -> m () Source #

Run a computation if a certain verbosity level is activated (exact match).

__CRASH_WHEN__ :: (HasCallStack, MonadTCM m, MonadDebug m) => VerboseKey -> VerboseLevel -> m () Source #

verboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> m () -> m () Source #

Run a computation if a certain verbosity level is activated.

Precondition: The level must be non-negative.

applyWhenVerboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a Source #

Apply a function if a certain verbosity level is activated.

Precondition: The level must be non-negative.

class ReadTCState m => MonadStatistics m where Source #

Minimal complete definition

Nothing

Methods

modifyCounter :: String -> (Integer -> Integer) -> m () Source #

default modifyCounter :: (MonadStatistics n, MonadTrans t, t n ~ m) => String -> (Integer -> Integer) -> m () Source #

Instances

Instances details
MonadStatistics TCM Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Statistics

Methods

modifyCounter :: String -> (Integer -> Integer) -> TCM () Source #

MonadStatistics TerM Source # 
Instance details

Defined in Agda.Termination.Monad

Methods

modifyCounter :: String -> (Integer -> Integer) -> TerM () Source #

MonadStatistics m => MonadStatistics (MaybeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Statistics

Methods

modifyCounter :: String -> (Integer -> Integer) -> MaybeT m () Source #

ReadTCState m => MonadStatistics (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

modifyCounter :: String -> (Integer -> Integer) -> PureConversionT m () Source #

MonadStatistics m => MonadStatistics (ExceptT e m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Statistics

Methods

modifyCounter :: String -> (Integer -> Integer) -> ExceptT e m () Source #

MonadStatistics m => MonadStatistics (ReaderT r m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Statistics

Methods

modifyCounter :: String -> (Integer -> Integer) -> ReaderT r m () Source #

MonadStatistics m => MonadStatistics (StateT s m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Statistics

Methods

modifyCounter :: String -> (Integer -> Integer) -> StateT s m () Source #

(MonadStatistics m, Monoid w) => MonadStatistics (WriterT w m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Statistics

Methods

modifyCounter :: String -> (Integer -> Integer) -> WriterT w m () Source #

getStatistics :: ReadTCState m => m Statistics Source #

Get the statistics.

modifyStatistics :: (Statistics -> Statistics) -> TCM () Source #

Modify the statistics via given function.

tick :: MonadStatistics m => String -> m () Source #

Increase specified counter by 1.

tickN :: MonadStatistics m => String -> Integer -> m () Source #

Increase specified counter by n.

tickMax :: MonadStatistics m => String -> Integer -> m () Source #

Set the specified counter to the maximum of its current value and n.

printStatistics :: (MonadDebug m, MonadTCEnv m, HasOptions m) => Int -> Maybe TopLevelModuleName -> Statistics -> m () Source #

Print the given statistics if verbosity "profile.ticks" is given.

class (Functor m, Applicative m, MonadFail m, HasOptions m, MonadDebug m, MonadTCEnv m) => HasConstInfo m where Source #

Minimal complete definition

Nothing

Methods

getConstInfo :: QName -> m Definition Source #

Lookup the definition of a name. The result is a closed thing, all free variables have been abstracted over.

getConstInfo' :: QName -> m (Either SigError Definition) Source #

Version that reports exceptions:

default getConstInfo' :: (HasConstInfo n, MonadTrans t, m ~ t n) => QName -> m (Either SigError Definition) Source #

getRewriteRulesFor :: QName -> m RewriteRules Source #

Lookup the rewrite rules with the given head symbol.

default getRewriteRulesFor :: (HasConstInfo n, MonadTrans t, m ~ t n) => QName -> m RewriteRules Source #

Instances

Instances details
HasConstInfo ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Reduce.Monad

HasConstInfo TerM Source # 
Instance details

Defined in Agda.Termination.Monad

HasConstInfo m => HasConstInfo (MaybeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Signature

HasConstInfo m => HasConstInfo (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Signature

HasConstInfo (TCMT IO) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Signature

HasConstInfo m => HasConstInfo (ChangeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Signature

HasConstInfo m => HasConstInfo (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

HasConstInfo m => HasConstInfo (ExceptT err m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Signature

HasConstInfo m => HasConstInfo (IdentityT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Signature

Methods

getConstInfo :: QName -> IdentityT m Definition Source #

getConstInfo' :: QName -> IdentityT m (Either SigError Definition) Source #

getRewriteRulesFor :: QName -> IdentityT m RewriteRules Source #

HasConstInfo m => HasConstInfo (ReaderT r m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Signature

Methods

getConstInfo :: QName -> ReaderT r m Definition Source #

getConstInfo' :: QName -> ReaderT r m (Either SigError Definition) Source #

getRewriteRulesFor :: QName -> ReaderT r m RewriteRules Source #

HasConstInfo m => HasConstInfo (StateT s m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Signature

Methods

getConstInfo :: QName -> StateT s m Definition Source #

getConstInfo' :: QName -> StateT s m (Either SigError Definition) Source #

getRewriteRulesFor :: QName -> StateT s m RewriteRules Source #

(Monoid w, HasConstInfo m) => HasConstInfo (WriterT w m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Signature

Methods

getConstInfo :: QName -> WriterT w m Definition Source #

getConstInfo' :: QName -> WriterT w m (Either SigError Definition) Source #

getRewriteRulesFor :: QName -> WriterT w m RewriteRules Source #

data SigError Source #

Signature lookup errors.

Constructors

SigUnknown String

The name is not in the signature; default error message.

SigAbstract

The name is not available, since it is abstract.

lookupSection :: (Functor m, ReadTCState m) => ModuleName -> m Telescope Source #

Lookup a section telescope.

If it doesn't exist, like in hierarchical top-level modules, the section telescope is empty.

inFreshModuleIfFreeParams :: TCM a -> TCM a Source #

Unless all variables in the context are module parameters, create a fresh module to capture the non-module parameters. Used when unquoting to make sure generated definitions work properly.

cachingStarts :: (MonadTCState m, ReadTCState m) => m () Source #

To be called before any write or restore calls.

writeToCurrentLog :: (MonadDebug m, MonadTCState m, ReadTCState m) => TypeCheckAction -> m () Source #

Writes a TypeCheckAction to the current log, using the current PostScopeState

localCache :: (MonadTCState m, ReadTCState m) => m a -> m a Source #

Runs the action and restores the current cache at the end of it.

withoutCache :: (MonadTCState m, ReadTCState m) => m a -> m a Source #

Runs the action without cache and restores the current cache at the end of it.

readFromCachedLog :: (MonadDebug m, MonadTCState m, ReadTCState m) => m (Maybe (TypeCheckAction, PostScopeState)) Source #

Reads the next entry in the cached type check log, if present.

cleanCachedLog :: (MonadDebug m, MonadTCState m) => m () Source #

Empties the "to read" CachedState. To be used when it gets invalid.

activateLoadedFileCache :: (HasOptions m, MonadDebug m, MonadTCState m) => m () Source #

Makes sure that the stLoadedFileCache is Just, with a clean current log. Crashes is stLoadedFileCache is already active with a dirty log. Should be called when we start typechecking the current file.

cacheCurrentLog :: (MonadDebug m, MonadTCState m) => m () Source #

Caches the current type check log. Discardes the old cache. Does nothing if caching is inactive.

resetState :: TCM () Source #

Resets the non-persistent part of the type checking state.

resetAllState :: TCM () Source #

Resets all of the type checking state.

Keep only Benchmark and backend information.

localTCState :: TCM a -> TCM a Source #

Restore TCState after performing subcomputation.

In contrast to localState, the Benchmark info from the subcomputation is saved.

localTCStateSaving :: TCM a -> TCM (a, TCState) Source #

Same as localTCState but also returns the state in which we were just before reverting it.

localTCStateSavingWarnings :: TCM a -> TCM a Source #

Same as localTCState but keep all warnings.

speculateTCState :: TCM (a, SpeculateResult) -> TCM a Source #

Allow rolling back the state changes of a TCM computation.

freshTCM :: TCM a -> TCM (Either TCErr a) Source #

A fresh TCM instance.

The computation is run in a fresh state, with the exception that the persistent state is preserved. If the computation changes the state, then these changes are ignored, except for changes to the persistent state. (Changes to the persistent state are also ignored if errors other than type errors or IO exceptions are encountered.)

getScope :: ReadTCState m => m ScopeInfo Source #

Get the current scope.

setScope :: ScopeInfo -> TCM () Source #

Set the current scope.

modifyScope_ :: MonadTCState m => (ScopeInfo -> ScopeInfo) -> m () Source #

Modify the current scope without updating the inverse maps.

modifyScope :: MonadTCState m => (ScopeInfo -> ScopeInfo) -> m () Source #

Modify the current scope.

useScope :: ReadTCState m => Lens' a ScopeInfo -> m a Source #

Get a part of the current scope.

locallyScope :: ReadTCState m => Lens' a ScopeInfo -> (a -> a) -> m b -> m b Source #

Run a computation in a modified scope.

withScope :: ReadTCState m => ScopeInfo -> m a -> m (a, ScopeInfo) Source #

Run a computation in a local scope.

withScope_ :: ReadTCState m => ScopeInfo -> m a -> m a Source #

Same as withScope, but discard the scope from the computation.

localScope :: TCM a -> TCM a Source #

Discard any changes to the scope by a computation.

notInScopeError :: QName -> TCM a Source #

Scope error.

printScope :: String -> Int -> String -> TCM () Source #

Debug print the scope.

modifyGlobalDefinition :: QName -> (Definition -> Definition) -> TCM () Source #

Update a possibly imported definition. Warning: changes made to imported definitions (during type checking) will not persist outside the current module. This function is currently used to update the compiled representation of a function during compilation.

withSignature :: Signature -> TCM a -> TCM a Source #

Run some computation in a different signature, restore original signature.

setTopLevelModule :: QName -> TCM () Source #

Set the top-level module. This affects the global module id of freshly generated names.

withTopLevelModule :: QName -> TCM a -> TCM a Source #

Use a different top-level module for a computation. Used when generating names for imported modules.

getAllPatternSyns :: ReadTCState m => m PatternSynDefns Source #

Get both local and imported pattern synonyms

modifyBenchmark :: (Benchmark -> Benchmark) -> TCM () Source #

Lens modify for Benchmark.

addImportedInstances :: Signature -> TCM () Source #

Look through the signature and reconstruct the instance table.

clearAnonInstanceDefs :: TCM () Source #

Remove all instances whose type is still unresolved.

addUnknownInstance :: QName -> TCM () Source #

Add an instance whose type is still unresolved.

addNamedInstance Source #

Arguments

:: QName

Name of the instance.

-> QName

Name of the class.

-> TCM () 

Add instance to some `class'.

traceCallM :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => tcm Call -> tcm a -> tcm a Source #

traceCallCPS :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => Call -> ((a -> tcm b) -> tcm b) -> (a -> tcm b) -> tcm b Source #

Reset envCall to previous value in the continuation.

Caveat: if the last traceCall did not set an interestingCall, for example, only set the Range with SetRange, we will revert to the last interesting call.

traceCall :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => Call -> tcm a -> tcm a Source #

Record a function call in the trace.

traceClosureCall :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => Closure Call -> tcm a -> tcm a Source #

setCurrentRange :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) => x -> tcm a -> tcm a Source #

Sets the current range (for error messages etc.) to the range of the given object, if it has a range (i.e., its range is not noRange).

highlightAsTypeChecked Source #

Arguments

:: (MonadTCM tcm, ReadTCState tcm) 
=> Range
rPre
-> Range
r
-> tcm a 
-> tcm a 

highlightAsTypeChecked rPre r m runs m and returns its result. Additionally, some code may be highlighted:

  • If r is non-empty and not a sub-range of rPre (after continuousPerLine has been applied to both): r is highlighted as being type-checked while m is running (this highlighting is removed if m completes successfully).
  • Otherwise: Highlighting is removed for rPre - r before m runs, and if m completes successfully, then rPre - r is highlighted as being type-checked.

printHighlightingInfo :: (MonadTCM tcm, ReadTCState tcm) => RemoveTokenBasedHighlighting -> HighlightingInfo -> tcm () Source #

Lispify and print the given highlighting information.

inMutualBlock :: (MutualId -> TCM a) -> TCM a Source #

Pass the current mutual block id or create a new mutual block if we are not already inside on.

setMutualBlockInfo :: MutualId -> MutualInfo -> TCM () Source #

Set the mutual block info for a block, possibly overwriting the existing one.

insertMutualBlockInfo :: MutualId -> MutualInfo -> TCM () Source #

Set the mutual block info for a block if non-existing.

setMutualBlock :: MutualId -> QName -> TCM () Source #

Set the mutual block for a definition.

currentOrFreshMutualBlock :: TCM MutualId Source #

Get the current mutual block, if any, otherwise a fresh mutual block is returned.

mutualBlockOf :: QName -> TCM MutualId Source #

Reverse lookup of a mutual block id for a names.

enterClosure :: (MonadTCEnv m, ReadTCState m, LensClosure a c) => c -> (a -> m b) -> m b Source #

withClosure :: (MonadTCEnv m, ReadTCState m) => Closure a -> (a -> m b) -> m (Closure b) Source #

mapClosure :: (MonadTCEnv m, ReadTCState m) => (a -> m b) -> Closure a -> m (Closure b) Source #

class (MonadTCEnv m, ReadTCState m, MonadError TCErr m, HasOptions m, MonadDebug m) => MonadConstraint m where Source #

Monad service class containing methods for adding and solving constraints

Methods

addConstraint :: Constraint -> m () Source #

Unconditionally add the constraint.

addAwakeConstraint :: Constraint -> m () Source #

Add constraint as awake constraint.

catchPatternErr :: m a -> m a -> m a Source #

`catchPatternErr handle m` runs m, handling pattern violations with handle (doesn't roll back the state)

solveConstraint :: Constraint -> m () Source #

solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> m () Source #

Solve awake constraints matching the predicate. If the second argument is True solve constraints even if already isSolvingConstraints.

wakeConstraints :: (ProblemConstraint -> m Bool) -> m () Source #

stealConstraints :: ProblemId -> m () Source #

modifyAwakeConstraints :: (Constraints -> Constraints) -> m () Source #

modifySleepingConstraints :: (Constraints -> Constraints) -> m () Source #

Instances

Instances details
MonadConstraint TCM Source # 
Instance details

Defined in Agda.TypeChecking.Constraints

(MonadTCEnv m, ReadTCState m, HasOptions m, MonadDebug m) => MonadConstraint (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

data ConstraintStatus Source #

Instances

Instances details
Eq ConstraintStatus Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Constraints

Show ConstraintStatus Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Constraints

Methods

showsPrec :: Int -> ConstraintStatus -> ShowS

show :: ConstraintStatus -> String

showList :: [ConstraintStatus] -> ShowS

getAwakeConstraints :: ReadTCState m => m Constraints Source #

Get the awake constraints

takeConstraints :: MonadConstraint m => (ProblemConstraint -> Bool) -> m Constraints Source #

Takes out all constraints matching given filter. Danger! The taken constraints need to be solved or put back at some point.

holdConstraints :: (ConstraintStatus -> ProblemConstraint -> Bool) -> TCM a -> TCM a Source #

Suspend constraints matching the predicate during the execution of the second argument. Caution: held sleeping constraints will not be woken up by events that would normally trigger a wakeup call.

addConstraint' :: Constraint -> TCM () Source #

Add new a constraint

nowSolvingConstraints :: MonadTCEnv m => m a -> m a Source #

Start solving constraints

catchConstraint :: MonadConstraint m => Constraint -> m () -> m () Source #

Add constraint if the action raises a pattern violation

setPragmaOptions :: PragmaOptions -> TCM () Source #

Sets the pragma options.

setCommandLineOptions :: CommandLineOptions -> TCM () Source #

Sets the command line options (both persistent and pragma options are updated).

Relative include directories are made absolute with respect to the current working directory. If the include directories have changed (thus, they are Left now, and were previously Right something), then the state is reset (completely, see setIncludeDirs) .

An empty list of relative include directories (Left []) is interpreted as ["."].

setCommandLineOptions' Source #

Arguments

:: AbsolutePath

The base directory of relative paths.

-> CommandLineOptions 
-> TCM () 

setLibraryPaths Source #

Arguments

:: AbsolutePath

The base directory of relative paths.

-> CommandLineOptions 
-> TCM CommandLineOptions 

addDefaultLibraries Source #

Arguments

:: AbsolutePath

The base directory of relative paths.

-> CommandLineOptions 
-> TCM CommandLineOptions 

enableDisplayForms :: MonadTCEnv m => m a -> m a Source #

Disable display forms.

disableDisplayForms :: MonadTCEnv m => m a -> m a Source #

Disable display forms.

displayFormsEnabled :: MonadTCEnv m => m Bool Source #

Check if display forms are enabled.

setIncludeDirs Source #

Arguments

:: [FilePath]

New include directories.

-> AbsolutePath

The base directory of relative paths.

-> TCM () 

Makes the given directories absolute and stores them as include directories.

If the include directories change, then the state is reset (completely, except for the include directories and stInteractionOutputCallback).

An empty list is interpreted as ["."].

setInputFile :: FilePath -> TCM () Source #

withShowAllArguments :: ReadTCState m => m a -> m a Source #

Switch on printing of implicit and irrelevant arguments. E.g. for reification in with-function generation.

Restores all PragmaOptions after completion. Thus, do not attempt to make persistent PragmaOptions changes in a withShowAllArguments bracket.

withShowAllArguments' :: ReadTCState m => Bool -> m a -> m a Source #

withPragmaOptions :: ReadTCState m => (PragmaOptions -> PragmaOptions) -> m a -> m a Source #

Change PragmaOptions for a computation and restore afterwards.

typeInType :: HasOptions m => m Bool Source #

etaEnabled :: HasOptions m => m Bool Source #

makeOpen :: MonadTCEnv m => a -> m (Open a) Source #

Create an open term in the current context.

getOpen :: (Subst Term a, MonadTCEnv m) => Open a -> m a Source #

Extract the value from an open term. The checkpoint at which it was created must be in scope.

tryGetOpen :: (Subst Term a, MonadTCEnv m) => Open a -> m (Maybe a) Source #

Extract the value from an open term. Returns Nothing if the checkpoint at which it was created is not in scope.

isClosed :: Open a -> Bool Source #

An Open is closed if it has checkpoint 0.

newtype KeepNames a Source #

Wrapper to tell addContext not to mark names as NotInScope. Used when adding a user-provided, but already type checked, telescope to the context.

Constructors

KeepNames a 

Instances

Instances details
AddContext (KeepNames Telescope) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

AddContext (KeepNames String, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => (KeepNames String, Dom Type) -> m a -> m a Source #

contextSize :: (KeepNames String, Dom Type) -> Nat Source #

class AddContext b where Source #

Various specializations of addCtx.

Methods

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

contextSize :: b -> Nat Source #

Instances

Instances details
AddContext String Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: String -> Nat Source #

AddContext Name Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

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

contextSize :: Name -> Nat Source #

AddContext Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

AddContext a => AddContext [a] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => [a] -> m a0 -> m a0 Source #

contextSize :: [a] -> Nat Source #

AddContext (Dom (String, Type)) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => Dom (String, Type) -> m a -> m a Source #

contextSize :: Dom (String, Type) -> Nat Source #

AddContext (Dom (Name, Type)) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => Dom (Name, Type) -> m a -> m a Source #

contextSize :: Dom (Name, Type) -> Nat Source #

AddContext (Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => Dom Type -> m a -> m a Source #

contextSize :: Dom Type -> Nat Source #

AddContext (KeepNames Telescope) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

AddContext ([NamedArg Name], Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source #

contextSize :: ([NamedArg Name], Type) -> Nat Source #

AddContext ([Arg Name], Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ([Arg Name], Type) -> m a -> m a Source #

contextSize :: ([Arg Name], Type) -> Nat Source #

AddContext ([WithHiding Name], Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

AddContext ([Name], Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => ([Name], Dom Type) -> m a -> m a Source #

contextSize :: ([Name], Dom Type) -> Nat Source #

AddContext (String, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => (String, Dom Type) -> m a -> m a Source #

contextSize :: (String, Dom Type) -> Nat Source #

AddContext (Name, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => (Name, Dom Type) -> m a -> m a Source #

contextSize :: (Name, Dom Type) -> Nat Source #

AddContext (KeepNames String, Dom Type) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addContext :: MonadAddContext m => (KeepNames String, Dom Type) -> m a -> m a Source #

contextSize :: (KeepNames String, Dom Type) -> Nat Source #

unsafeModifyContext :: MonadTCEnv tcm => (Context -> Context) -> tcm a -> tcm a Source #

Modify a Context in a computation. Warning: does not update the checkpoints. Use updateContext instead.

modifyContextInfo :: MonadTCEnv tcm => (forall e. Dom e -> Dom e) -> tcm a -> tcm a Source #

Modify the Dom part of context entries.

inTopContext :: (MonadTCEnv tcm, ReadTCState tcm) => tcm a -> tcm a Source #

Change to top (=empty) context. Resets the checkpoints.

unsafeInTopContext :: (MonadTCEnv m, ReadTCState m) => m a -> m a Source #

Change to top (=empty) context, but don't update the checkpoints. Totally not safe!

unsafeEscapeContext :: MonadTCM tcm => Int -> tcm a -> tcm a Source #

Delete the last n bindings from the context.

Doesn't update checkpoints! Use escapeContext or `updateContext rho (drop n)` instead, for an appropriate substitution rho.

escapeContext :: MonadAddContext m => Empty -> Int -> m a -> m a Source #

Delete the last n bindings from the context. Any occurrences of these variables are replaced with the given err.

checkpoint :: (MonadDebug tcm, MonadTCM tcm, MonadFresh CheckpointId tcm, ReadTCState tcm) => Substitution -> tcm a -> tcm a Source #

Add a new checkpoint. Do not use directly!

checkpointSubstitution' :: MonadTCEnv tcm => CheckpointId -> tcm (Maybe Substitution) Source #

Get the substitution from the context at a given checkpoint to the current context.

getModuleParameterSub :: (MonadTCEnv m, ReadTCState m) => ModuleName -> m (Maybe Substitution) Source #

Get substitution Γ ⊢ ρ : Γm where Γ is the current context and Γm is the module parameter telescope of module m.

Returns Nothing in case the we don't have a checkpoint for m.

defaultAddCtx :: MonadAddContext m => Name -> Dom Type -> m a -> m a Source #

Default implementation of addCtx in terms of updateContext

withFreshName_ :: MonadAddContext m => ArgName -> (Name -> m a) -> m a Source #

withShadowingNameTCM :: Name -> TCM b -> TCM b Source #

Run the given TCM action, and register the given variable as being shadowed by all the names with the same root that are added to the context during this TCM action.

underAbstraction :: (Subst t a, MonadAddContext m) => Dom Type -> Abs a -> (a -> m b) -> m b Source #

Go under an abstraction. Do not extend context in case of NoAbs.

underAbstraction' :: (Subst t a, MonadAddContext m, AddContext (name, Dom Type)) => (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b Source #

underAbstractionAbs :: (Subst t a, MonadAddContext m) => Dom Type -> Abs a -> (a -> m b) -> m b Source #

Go under an abstraction, treating NoAbs as Abs.

underAbstractionAbs' :: (Subst t a, MonadAddContext m, AddContext (name, Dom Type)) => (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b Source #

underAbstraction_ :: (Subst t a, MonadAddContext m) => Abs a -> (a -> m b) -> m b Source #

Go under an abstract without worrying about the type to add to the context.

mapAbstraction :: (Subst t a, Subst t' b, Free b, MonadAddContext m) => Dom Type -> (a -> m b) -> Abs a -> m (Abs b) Source #

Map a monadic function on the thing under the abstraction, adding the abstracted variable to the context.

defaultAddLetBinding' :: MonadTCEnv m => Name -> Term -> Dom Type -> m a -> m a Source #

Add a let bound variable

addLetBinding :: MonadAddContext m => ArgInfo -> Name -> Term -> Type -> m a -> m a Source #

Add a let bound variable

getContext :: MonadTCEnv m => m [Dom (Name, Type)] Source #

Get the current context.

getContextSize :: (Applicative m, MonadTCEnv m) => m Nat Source #

Get the size of the current context.

getContextArgs :: (Applicative m, MonadTCEnv m) => m Args Source #

Generate [var (n - 1), ..., var 0] for all declarations in the context.

getContextTerms :: (Applicative m, MonadTCEnv m) => m [Term] Source #

Generate [var (n - 1), ..., var 0] for all declarations in the context.

getContextTelescope :: (Applicative m, MonadTCEnv m) => m Telescope Source #

Get the current context as a Telescope.

getContextNames :: (Applicative m, MonadTCEnv m) => m [Name] Source #

Get the names of all declarations in the context.

lookupBV' :: MonadTCEnv m => Nat -> m (Maybe (Dom (Name, Type))) Source #

get type of bound variable (i.e. deBruijn index)

lookupBV :: (MonadFail m, MonadTCEnv m) => Nat -> m (Dom (Name, Type)) Source #

domOfBV :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m (Dom Type) Source #

typeOfBV :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m Type Source #

nameOfBV' :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m (Maybe Name) Source #

nameOfBV :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m Name Source #

getVarInfo :: (MonadFail m, MonadTCEnv m) => Name -> m (Term, Dom Type) Source #

Get the term corresponding to a named variable. If it is a lambda bound variable the deBruijn index is returned and if it is a let bound variable its definition is returned.

data CoinductionKit Source #

The coinductive primitives.

bindBuiltinName :: String -> Term -> TCM () Source #

bindPrimitive :: String -> PrimFun -> TCM () Source #

getBuiltin' :: HasBuiltins m => String -> m (Maybe Term) Source #

getPrimitive' :: HasBuiltins m => String -> m (Maybe PrimFun) Source #

getPrimitiveTerm' :: HasBuiltins m => String -> m (Maybe Term) Source #

getTerm' :: HasBuiltins m => String -> m (Maybe Term) Source #

getName' :: HasBuiltins m => String -> m (Maybe QName) Source #

getTerm :: HasBuiltins m => String -> String -> m Term Source #

getTerm use name looks up name as a primitive or builtin, and throws an error otherwise. The use argument describes how the name is used for the sake of the error message.

constructorForm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => Term -> m Term Source #

Rewrite a literal to constructor form if possible.

constructorForm' :: Applicative m => m Term -> m Term -> Term -> m Term Source #

getBuiltinName' :: HasBuiltins m => String -> m (Maybe QName) Source #

getPrimitiveName' :: HasBuiltins m => String -> m (Maybe QName) Source #

isPrimitive :: HasBuiltins m => String -> QName -> m Bool Source #

pathView :: HasBuiltins m => Type -> m PathView Source #

Check whether the type is actually an path (lhs ≡ rhs) and extract lhs, rhs, and their type.

Precondition: type is reduced.

idViewAsPath :: HasBuiltins m => Type -> m PathView Source #

Non dependent Path

pathUnview :: PathView -> Type Source #

Revert the PathView.

Postcondition: type is reduced.

primEqualityName :: TCM QName Source #

Get the name of the equality type.

equalityView :: Type -> TCM EqualityView Source #

Check whether the type is actually an equality (lhs ≡ rhs) and extract lhs, rhs, and their type.

Precondition: type is reduced.

equalityUnview :: EqualityView -> Type Source #

Revert the EqualityView.

Postcondition: type is reduced.

constrainedPrims :: [String] Source #

Primitives with typechecking constrants.

getNameOfConstrained :: HasBuiltins m => String -> m (Maybe QName) Source #

data SizeViewComparable a Source #

Instances

Instances details
Functor SizeViewComparable Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

data DeepSizeView Source #

A deep view on sizes.

Instances

Instances details
Show DeepSizeView Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

showsPrec :: Int -> DeepSizeView -> ShowS

show :: DeepSizeView -> String

showList :: [DeepSizeView] -> ShowS

Pretty DeepSizeView Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

data SizeView Source #

A useful view on sizes.

class IsSizeType a where Source #

Check if a type is the primSize type. The argument should be reduced.

Methods

isSizeType :: (HasOptions m, HasBuiltins m) => a -> m (Maybe BoundedSize) Source #

Instances

Instances details
IsSizeType Term Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

isSizeType :: (HasOptions m, HasBuiltins m) => Term -> m (Maybe BoundedSize) Source #

IsSizeType CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

isSizeType :: (HasOptions m, HasBuiltins m) => CompareAs -> m (Maybe BoundedSize) Source #

IsSizeType a => IsSizeType (Type' a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

isSizeType :: (HasOptions m, HasBuiltins m) => Type' a -> m (Maybe BoundedSize) Source #

IsSizeType a => IsSizeType (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

isSizeType :: (HasOptions m, HasBuiltins m) => Dom a -> m (Maybe BoundedSize) Source #

IsSizeType a => IsSizeType (b, a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

isSizeType :: (HasOptions m, HasBuiltins m) => (b, a) -> m (Maybe BoundedSize) Source #

data BoundedSize Source #

Result of querying whether size variable i is bounded by another size.

Constructors

BoundedLt Term

yes i : Size< t

BoundedNo 

Instances

Instances details
Eq BoundedSize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

(==) :: BoundedSize -> BoundedSize -> Bool

(/=) :: BoundedSize -> BoundedSize -> Bool

Show BoundedSize Source # 
Instance details

Defined in Agda.TypeChecking.Monad.SizedTypes

Methods

showsPrec :: Int -> BoundedSize -> ShowS

show :: BoundedSize -> String

showList :: [BoundedSize] -> ShowS

getBuiltinDefName :: HasBuiltins m => String -> m (Maybe QName) Source #

getBuiltinSize :: HasBuiltins m => m (Maybe QName, Maybe QName) Source #

haveSizedTypes :: TCM Bool Source #

Test whether OPTIONS --sized-types and whether the size built-ins are defined.

haveSizeLt :: TCM Bool Source #

Test whether the SIZELT builtin is defined.

builtinSizeHook :: String -> QName -> Type -> TCM () Source #

Add polarity info to a SIZE builtin.

sizeSort :: Sort Source #

The sort of built-in types SIZE and SIZELT.

sizeUniv :: Type Source #

The type of built-in types SIZE and SIZELT.

sizeType_ :: QName -> Type Source #

The built-in type SIZE with user-given name.

sizeType :: (HasBuiltins m, MonadTCEnv m, ReadTCState m) => m Type Source #

The built-in type SIZE.

sizeSucName :: (HasBuiltins m, HasOptions m) => m (Maybe QName) Source #

The name of SIZESUC.

sizeMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => NonEmpty Term -> m Term Source #

Transform list of terms into a term build from binary maximum.

sizeView :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => Term -> m SizeView Source #

Expects argument to be reduced.

sizeViewComparable :: DeepSizeView -> DeepSizeView -> SizeViewComparable () Source #

sizeViewComparable v w checks whether v >= w (then Left) or v <= w (then Right). If uncomparable, it returns NotComparable.

sizeViewPred :: Nat -> DeepSizeView -> DeepSizeView Source #

sizeViewPred k v decrements v by k (must be possible!).

sizeViewOffset :: DeepSizeView -> Maybe Offset Source #

sizeViewOffset v returns the number of successors or Nothing when infty.

removeSucs :: (DeepSizeView, DeepSizeView) -> (DeepSizeView, DeepSizeView) Source #

Remove successors common to both sides.

unSizeView :: SizeView -> TCM Term Source #

Turn a size view into a term.

maxViewCons :: DeepSizeView -> SizeMaxView -> SizeMaxView Source #

maxViewCons v ws = max v ws. It only adds v to ws if it is not subsumed by an element of ws.

sizeViewComparableWithMax :: DeepSizeView -> SizeMaxView -> SizeViewComparable SizeMaxView' Source #

sizeViewComparableWithMax v ws tries to find w in ws that compares with v and singles this out. Precondition: v /= DSizeInv.

addConstant :: QName -> Definition -> TCM () Source #

Add a constant to the signature. Lifts the definition to top level.

setTerminates :: QName -> Bool -> TCM () Source #

Set termination info of a defined function symbol.

setCompiledClauses :: QName -> CompiledClauses -> TCM () Source #

Set CompiledClauses of a defined function symbol.

setSplitTree :: QName -> SplitTree -> TCM () Source #

Set SplitTree of a defined function symbol.

modifyFunClauses :: QName -> ([Clause] -> [Clause]) -> TCM () Source #

Modify the clauses of a function.

addClauses :: QName -> [Clause] -> TCM () Source #

Lifts clauses to the top-level and adds them to definition. Also adjusts the funCopatternLHS field if necessary.

addPragma :: BackendName -> QName -> String -> TCM () Source #

Add a compiler pragma `{-# COMPILE backend name text #-}`

markInline :: Bool -> QName -> TCM () Source #

addSection :: ModuleName -> TCM () Source #

Add a section to the signature.

The current context will be stored as the cumulative module parameters for this section.

setModuleCheckpoint :: ModuleName -> TCM () Source #

Sets the checkpoint for the given module to the current checkpoint.

getSection :: (Functor m, ReadTCState m) => ModuleName -> m (Maybe Section) Source #

Get a section.

Why Maybe? The reason is that we look up all prefixes of a module to compute number of parameters, and for hierarchical top-level modules, A.B.C say, A and A.B do not exist.

applySection Source #

Arguments

:: ModuleName

Name of new module defined by the module macro.

-> Telescope

Parameters of new module.

-> ModuleName

Name of old module applied to arguments.

-> Args

Arguments of module application.

-> ScopeCopyInfo

Imported names and modules

-> TCM () 

Module application (followed by module parameter abstraction).

addDisplayForm :: QName -> DisplayForm -> TCM () Source #

Add a display form to a definition (could be in this or imported signature).

isLocal :: ReadTCState m => QName -> m Bool Source #

chaseDisplayForms :: QName -> TCM (Set QName) Source #

Find all names used (recursively) by display forms of a given name.

hasLoopingDisplayForm :: QName -> TCM Bool Source #

Check if a display form is looping.

sameDef :: HasConstInfo m => QName -> QName -> m (Maybe QName) Source #

whatInduction :: MonadTCM tcm => QName -> tcm Induction Source #

Can be called on either a (co)datatype, a record type or a (co)constructor.

singleConstructorType :: QName -> TCM Bool Source #

Does the given constructor come from a single-constructor type?

Precondition: The name has to refer to a constructor.

sigError :: (String -> a) -> a -> SigError -> a Source #

Standard eliminator for SigError.

getOriginalProjection :: HasConstInfo m => QName -> m QName Source #

Get the original name of the projection (the current one could be from a module application).

getPolarity :: HasConstInfo m => QName -> m [Polarity] Source #

Look up the polarity of a definition.

getPolarity' :: HasConstInfo m => Comparison -> QName -> m [Polarity] Source #

Look up polarity of a definition and compose with polarity represented by Comparison.

setPolarity :: QName -> [Polarity] -> TCM () Source #

Set the polarity of a definition.

getForcedArgs :: HasConstInfo m => QName -> m [IsForced] Source #

Look up the forced arguments of a definition.

getArgOccurrence :: QName -> Nat -> TCM Occurrence Source #

Get argument occurrence info for argument i of definition d (never fails).

setArgOccurrences :: QName -> [Occurrence] -> TCM () Source #

Sets the defArgOccurrences for the given identifier (which should already exist in the signature).

setCompiledArgUse :: QName -> [Bool] -> TCM () Source #

getErasedConArgs :: QName -> TCM [Bool] Source #

Returns a list of length conArity. If no erasure analysis has been performed yet, this will be a list of Falses.

setErasedConArgs :: QName -> [Bool] -> TCM () Source #

addDataCons :: QName -> [QName] -> TCM () Source #

add data constructors to a datatype

getMutual :: QName -> TCM (Maybe [QName]) Source #

Get the mutually recursive identifiers of a symbol from the signature.

getMutual_ :: Defn -> Maybe [QName] Source #

Get the mutually recursive identifiers from a Definition.

setMutual :: QName -> [QName] -> TCM () Source #

Set the mutually recursive identifiers.

mutuallyRecursive :: QName -> QName -> TCM Bool Source #

Check whether two definitions are mutually recursive.

definitelyNonRecursive_ :: Defn -> Bool Source #

A functiondatarecord definition is nonRecursive if it is not even mutually recursive with itself.

getCurrentModuleFreeVars :: TCM Nat Source #

Get the number of parameters to the current module.

getDefFreeVars :: (Functor m, Applicative m, ReadTCState m, MonadTCEnv m) => QName -> m Nat Source #

Compute the number of free variables of a defined name. This is the sum of number of parameters shared with the current module and the number of anonymous variables (if the name comes from a let-bound module).

getModuleFreeVars :: (Functor m, Applicative m, MonadTCEnv m, ReadTCState m) => ModuleName -> m Nat Source #

moduleParamsToApply :: (Functor m, Applicative m, HasOptions m, MonadTCEnv m, ReadTCState m, MonadDebug m) => ModuleName -> m Args Source #

Compute the context variables to apply a definition to.

We have to insert the module telescope of the common prefix of the current module and the module where the definition comes from. (Properly raised to the current context.)

Example: module M₁ Γ where module M₁ Δ where f = ... module M₃ Θ where ... M₁.M₂.f [insert Γ raised by Θ]

instantiateDef :: (Functor m, HasConstInfo m, HasOptions m, ReadTCState m, MonadTCEnv m, MonadDebug m) => Definition -> m Definition Source #

Instantiate a closed definition with the correct part of the current context.

makeAbstract :: Definition -> Maybe Definition Source #

Give the abstract view of a definition.

inAbstractMode :: MonadTCEnv m => m a -> m a Source #

Enter abstract mode. Abstract definition in the current module are transparent.

inConcreteMode :: MonadTCEnv m => m a -> m a Source #

Not in abstract mode. All abstract definitions are opaque.

ignoreAbstractMode :: MonadTCEnv m => m a -> m a Source #

Ignore abstract mode. All abstract definitions are transparent.

inConcreteOrAbstractMode :: (MonadTCEnv m, HasConstInfo m) => QName -> (Definition -> m a) -> m a Source #

Enter concrete or abstract mode depending on whether the given identifier is concrete or abstract.

treatAbstractly :: MonadTCEnv m => QName -> m Bool Source #

Check whether a name might have to be treated abstractly (either if we're inAbstractMode or it's not a local name). Returns true for things not declared abstract as well, but for those makeAbstract will have no effect.

treatAbstractly' :: QName -> TCEnv -> Bool Source #

Andreas, 2015-07-01: If the current module is a weak suffix of the identifier module, we can see through its abstract definition if we are abstract. (Then treatAbstractly' returns False).

If I am not mistaken, then we cannot see definitions in the where block of an abstract function from the perspective of the function, because then the current module is a strict prefix of the module of the local identifier. This problem is fixed by removing trailing anonymous module name parts (underscores) from both names.

typeOfConst :: (HasConstInfo m, ReadTCState m) => QName -> m Type Source #

Get type of a constant, instantiated to the current context.

relOfConst :: HasConstInfo m => QName -> m Relevance Source #

Get relevance of a constant.

modalityOfConst :: HasConstInfo m => QName -> m Modality Source #

Get modality of a constant.

droppedPars :: Definition -> Int Source #

The number of dropped parameters for a definition. 0 except for projection(-like) functions and constructors.

isProjection :: HasConstInfo m => QName -> m (Maybe Projection) Source #

Is it the name of a record projection?

isStaticFun :: Defn -> Bool Source #

Is it a function marked STATIC?

isInlineFun :: Defn -> Bool Source #

Is it a function marked INLINE?

isProperProjection :: Defn -> Bool Source #

Returns True if we are dealing with a proper projection, i.e., not a projection-like function nor a record field value (projection applied to argument).

projectionArgs :: Defn -> Int Source #

Number of dropped initial arguments of a projection(-like) function.

usesCopatterns :: HasConstInfo m => QName -> m Bool Source #

Check whether a definition uses copatterns.

applyDef :: HasConstInfo m => ProjOrigin -> QName -> Arg Term -> m Term Source #

Apply a function f to its first argument, producing the proper postfix projection if f is a projection.

class UnFreezeMeta a where Source #

Unfreeze meta and its type if this is a meta again. Does not unfreeze deep occurrences of metas.

Methods

unfreezeMeta :: MonadMetaSolver m => a -> m () Source #

Instances

Instances details
UnFreezeMeta MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => MetaId -> m () Source #

UnFreezeMeta LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

UnFreezeMeta PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

UnFreezeMeta Level Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => Level -> m () Source #

UnFreezeMeta Sort Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => Sort -> m () Source #

UnFreezeMeta Type Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => Type -> m () Source #

UnFreezeMeta Term Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => Term -> m () Source #

UnFreezeMeta a => UnFreezeMeta [a] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => [a] -> m () Source #

UnFreezeMeta a => UnFreezeMeta (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => Abs a -> m () Source #

class IsInstantiatedMeta a where Source #

Check whether all metas are instantiated. Precondition: argument is a meta (in some form) or a list of metas.

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => a -> m Bool Source #

Instances

Instances details
IsInstantiatedMeta MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => MetaId -> m Bool Source #

IsInstantiatedMeta LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => LevelAtom -> m Bool Source #

IsInstantiatedMeta PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => PlusLevel -> m Bool Source #

IsInstantiatedMeta Level Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Level -> m Bool Source #

IsInstantiatedMeta Term Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Term -> m Bool Source #

IsInstantiatedMeta a => IsInstantiatedMeta [a] Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => [a] -> m Bool Source #

IsInstantiatedMeta a => IsInstantiatedMeta (Maybe a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Maybe a -> m Bool Source #

IsInstantiatedMeta a => IsInstantiatedMeta (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Arg a -> m Bool Source #

IsInstantiatedMeta a => IsInstantiatedMeta (Abs a) Source #

Does not worry about raising.

Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

isInstantiatedMeta :: (MonadFail m, ReadTCState m) => Abs a -> m Bool Source #

class (MonadConstraint m, MonadReduce m, MonadAddContext m, MonadTCEnv m, ReadTCState m, HasBuiltins m, HasConstInfo m, MonadDebug m) => MonadMetaSolver m where Source #

Monad service class for creating, solving and eta-expanding of metavariables.

Methods

newMeta' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> m MetaId Source #

Generate a new meta variable with some instantiation given. For instance, the instantiation could be a PostponedTypeCheckingProblem.

assignV :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> m () Source #

Assign to an open metavar which may not be frozen. First check that metavar args are in pattern fragment. Then do extended occurs check on given thing.

Assignment is aborted by throwing a PatternErr via a call to patternViolation. This error is caught by catchConstraint during equality checking (compareAtom) and leads to restoration of the original constraints.

assignTerm' :: MonadMetaSolver m => MetaId -> [Arg ArgName] -> Term -> m () Source #

Directly instantiate the metavariable. Skip pattern check, occurs check and frozen check. Used for eta expanding frozen metas.

etaExpandMeta :: [MetaKind] -> MetaId -> m () Source #

Eta expand a metavariable, if it is of the specified kind. Don't do anything if the metavariable is a blocked term.

updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> m () Source #

Update the status of the metavariable

speculateMetas :: m () -> m KeepMetas -> m () Source #

'speculateMetas fallback m' speculatively runs m, but if the result is RollBackMetas any changes to metavariables are rolled back and fallback is run instead.

data MetaKind Source #

Various kinds of metavariables.

Constructors

Records

Meta variables of record type.

SingletonRecords

Meta variables of "hereditarily singleton" record type.

Levels

Meta variables of level type, if type-in-type is activated.

Instances

Instances details
Bounded MetaKind Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Enum MetaKind Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Eq MetaKind Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

(==) :: MetaKind -> MetaKind -> Bool

(/=) :: MetaKind -> MetaKind -> Bool

Show MetaKind Source # 
Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

showsPrec :: Int -> MetaKind -> ShowS

show :: MetaKind -> String

showList :: [MetaKind] -> ShowS

allMetaKinds :: [MetaKind] Source #

All possible metavariable kinds.

dontAssignMetas :: (MonadTCEnv m, HasOptions m, MonadDebug m) => m a -> m a Source #

Switch off assignment of metas.

getMetaStore :: ReadTCState m => m MetaStore Source #

Get the meta store.

metasCreatedBy :: ReadTCState m => m a -> m (a, IntSet) Source #

Run a computation and record which new metas it created.

lookupMeta' :: ReadTCState m => MetaId -> m (Maybe MetaVariable) Source #

Lookup a meta variable.

lookupMeta :: (MonadFail m, ReadTCState m) => MetaId -> m MetaVariable Source #

metaType :: (MonadFail m, ReadTCState m) => MetaId -> m Type Source #

Type of a term or sort meta.

updateMetaVarTCM :: MetaId -> (MetaVariable -> MetaVariable) -> TCM () Source #

Update the information associated with a meta variable.

insertMetaVar :: MetaId -> MetaVariable -> TCM () Source #

Insert a new meta variable with associated information into the meta store.

isSortMeta :: (MonadFail m, ReadTCState m) => MetaId -> m Bool Source #

getMetaType :: (MonadFail m, ReadTCState m) => MetaId -> m Type Source #

getMetaContextArgs :: MonadTCEnv m => MetaVariable -> m Args Source #

Compute the context variables that a meta should be applied to, accounting for pruning.

getMetaTypeInContext :: (MonadFail m, MonadTCEnv m, ReadTCState m, MonadReduce m) => MetaId -> m Type Source #

Given a meta, return the type applied to the current context.

isGeneralizableMeta :: (ReadTCState m, MonadFail m) => MetaId -> m DoGeneralize Source #

Is it a meta that might be generalized?

isInstantiatedMeta' :: (MonadFail m, ReadTCState m) => MetaId -> m (Maybe Term) Source #

constraintMetas :: Constraint -> TCM (Set MetaId) Source #

Returns all metavariables in a constraint. Slightly complicated by the fact that blocked terms are represented by two meta variables. To find the second one we need to look up the meta listeners for the one in the UnBlock constraint.

createMetaInfo :: (MonadTCEnv m, ReadTCState m) => m MetaInfo Source #

Create MetaInfo in the current environment.

registerInteractionPoint :: forall m. MonadInteractionPoints m => Bool -> Range -> Maybe Nat -> m InteractionId Source #

Register an interaction point during scope checking. If there is no interaction id yet, create one.

findInteractionPoint_ :: Range -> InteractionPoints -> Maybe InteractionId Source #

Find an interaction point by Range by searching the whole map.

O(n): linear in the number of registered interaction points.

connectInteractionPoint :: MonadInteractionPoints m => InteractionId -> MetaId -> m () Source #

Hook up meta variable to interaction point.

removeInteractionPoint :: MonadInteractionPoints m => InteractionId -> m () Source #

Mark an interaction point as solved.

getInteractionPoints :: ReadTCState m => m [InteractionId] Source #

Get a list of interaction ids.

getInteractionMetas :: ReadTCState m => m [MetaId] Source #

Get all metas that correspond to unsolved interaction ids.

getInteractionIdsAndMetas :: ReadTCState m => m [(InteractionId, MetaId)] Source #

Get all metas that correspond to unsolved interaction ids.

isInteractionMeta :: ReadTCState m => MetaId -> m (Maybe InteractionId) Source #

Does the meta variable correspond to an interaction point?

Time: O(n) where n is the number of interaction metas.

lookupInteractionPoint :: (MonadFail m, ReadTCState m, MonadError TCErr m) => InteractionId -> m InteractionPoint Source #

Get the information associated to an interaction point.

lookupInteractionId :: (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) => InteractionId -> m MetaId Source #

Get MetaId for an interaction point. Precondition: interaction point is connected.

lookupInteractionMeta :: ReadTCState m => InteractionId -> m (Maybe MetaId) Source #

Check whether an interaction id is already associated with a meta variable.

newMeta :: MonadMetaSolver m => Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> m MetaId Source #

Generate new meta variable.

newMetaTCM' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> TCM MetaId Source #

Generate a new meta variable with some instantiation given. For instance, the instantiation could be a PostponedTypeCheckingProblem.

getInteractionRange :: (MonadInteractionPoints m, MonadFail m, MonadError TCErr m) => InteractionId -> m Range Source #

Get the Range for an interaction point.

getMetaRange :: (MonadFail m, ReadTCState m) => MetaId -> m Range Source #

Get the Range for a meta variable.

listenToMeta :: MonadMetaSolver m => Listener -> MetaId -> m () Source #

listenToMeta l m: register l as a listener to m. This is done when the type of l is blocked by m.

unlistenToMeta :: MonadMetaSolver m => Listener -> MetaId -> m () Source #

Unregister a listener.

getMetaListeners :: (MonadFail m, ReadTCState m) => MetaId -> m [Listener] Source #

Get the listeners to a meta.

withFreezeMetas :: TCM a -> TCM a Source #

Freeze all so far unfrozen metas for the duration of the given computation.

freezeMetas :: TCM [MetaId] Source #

Freeze all meta variables and return the list of metas that got frozen.

freezeMetas' :: (MetaId -> Bool) -> TCM [MetaId] Source #

Freeze some meta variables and return the list of metas that got frozen.

unfreezeMetas :: TCM () Source #

Thaw all meta variables.

unfreezeMetas' :: (MetaId -> Bool) -> TCM () Source #

Thaw some metas, as indicated by the passed condition.

isFrozen :: (MonadFail m, ReadTCState m) => MetaId -> m Bool Source #

activeBackendMayEraseType :: QName -> TCM Bool Source #

Ask the active backend whether a type may be erased. See issue #3732.

backendInteraction :: [Backend] -> (TCM (Maybe Interface) -> TCM ()) -> TCM (Maybe Interface) -> TCM () Source #

callBackend :: String -> IsMain -> Interface -> TCM () Source #

Call the compilerMain function of the given backend.

lookupBackend :: BackendName -> TCM (Maybe Backend) Source #

Look for a backend of the given name.

activeBackend :: TCM (Maybe Backend) Source #

Get the currently active backend (if any).