Agda.TypeChecking.Monad.Base

Type checking state

data TCState

Constructors

TCSt

Fields

• stPreScopeState :: !PreScopeState

  The state which is frozen after scope checking.

• stPostScopeState :: !PostScopeState

  The state which is modified after scope checking.

• stPersistentState :: !PersistentTCState

  State which is forever, like a diamond.

Instances

Show TCState

Methods

showsPrec :: Int -> TCState -> ShowS

show :: TCState -> String

showList :: [TCState] -> ShowS

LensPersistentVerbosity TCState

Methods

getPersistentVerbosity :: TCState -> PersistentVerbosity

setPersistentVerbosity :: PersistentVerbosity -> TCState -> TCState

mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> TCState -> TCState

LensIncludePaths TCState

Methods

getIncludePaths :: TCState -> [FilePath]

setIncludePaths :: [FilePath] -> TCState -> TCState

mapIncludePaths :: ([FilePath] -> [FilePath]) -> TCState -> TCState

getAbsoluteIncludePaths :: TCState -> [AbsolutePath]

setAbsoluteIncludePaths :: [AbsolutePath] -> TCState -> TCState

mapAbsoluteIncludePaths :: ([AbsolutePath] -> [AbsolutePath]) -> TCState -> TCState

LensSafeMode TCState

Methods

getSafeMode :: TCState -> SafeMode

setSafeMode :: SafeMode -> TCState -> TCState

mapSafeMode :: (SafeMode -> SafeMode) -> TCState -> TCState

LensCommandLineOptions TCState

Methods

getCommandLineOptions :: TCState -> CommandLineOptions

setCommandLineOptions :: CommandLineOptions -> TCState -> TCState

mapCommandLineOptions :: (CommandLineOptions -> CommandLineOptions) -> TCState -> TCState

LensVerbosity TCState

Methods

getVerbosity :: TCState -> Verbosity

setVerbosity :: Verbosity -> TCState -> TCState

mapVerbosity :: (Verbosity -> Verbosity) -> TCState -> TCState

LensPragmaOptions TCState

Methods

getPragmaOptions :: TCState -> PragmaOptions

setPragmaOptions :: PragmaOptions -> TCState -> TCState

mapPragmaOptions :: (PragmaOptions -> PragmaOptions) -> TCState -> TCState

MonadState TCState TerM

Methods

get :: TerM TCState

put :: TCState -> TerM ()

state :: (TCState -> (a, TCState)) -> TerM a

MonadIO m => MonadState TCState (TCMT m)

Methods

get :: TCMT m TCState

put :: TCState -> TCMT m ()

state :: (TCState -> (a, TCState)) -> TCMT m a

class Monad m => ReadTCState m where

Minimal complete definition

getTCState

Methods

getTCState :: m TCState

Instances

ReadTCState ReduceM

Methods

getTCState :: ReduceM TCState

MonadIO m => ReadTCState (TCMT m)

Methods

getTCState :: TCMT m TCState

data PreScopeState

Constructors

PreScopeState

Fields

• stPreTokens :: !CompressedFile

  Highlighting info for tokens (but not those tokens for which highlighting exists in stSyntaxInfo).

• stPreImports :: !Signature

  Imported declared identifiers. Those most not be serialized!

• stPreImportedModules :: !(Set ModuleName)
• stPreModuleToSource :: !ModuleToSource
• stPreVisitedModules :: !VisitedModules
• stPreScope :: !ScopeInfo
• stPrePatternSyns :: !PatternSynDefns

  Pattern synonyms of the current file. Serialized.

• stPrePatternSynImports :: !PatternSynDefns

  Imported pattern synonyms. Must not be serialized!

• stPrePragmaOptions :: !PragmaOptions

  Options applying to the current file. OPTIONS pragmas only affect this field.

• stPreImportedBuiltins :: !(BuiltinThings PrimFun)
• stPreImportedDisplayForms :: !DisplayForms

  Display forms added by someone else to imported identifiers

• stPreImportedInstanceDefs :: !InstanceTable
• stPreForeignCode :: !(Map BackendName [ForeignCode])

  {--} code that should be included in the compiled output. Does not include code for imported modules.

• stPreFreshInteractionId :: !InteractionId

type DisambiguatedNames = IntMap QName

data PostScopeState

Constructors

PostScopeState

Fields

• stPostSyntaxInfo :: !CompressedFile

  Highlighting info.

• stPostDisambiguatedNames :: !DisambiguatedNames

  Disambiguation carried out by the type checker. Maps position of first name character to disambiguated QName for each AmbiguousQName already passed by the type checker.

• stPostMetaStore :: !MetaStore
• stPostInteractionPoints :: !InteractionPoints
• stPostAwakeConstraints :: !Constraints
• stPostSleepingConstraints :: !Constraints
• stPostDirty :: !Bool

  Dirty when a constraint is added, used to prevent pointer update. Currently unused.

• stPostOccursCheckDefs :: !(Set QName)

  Definitions to be considered during occurs check. Initialized to the current mutual block before the check. During occurs check, we remove definitions from this set as soon we have checked them.

• stPostSignature :: !Signature

  Declared identifiers of the current file. These will be serialized after successful type checking.

• stPostModuleParameters :: !ModuleParamDict

  TODO: can these be moved into the TCEnv?

• stPostImportsDisplayForms :: !DisplayForms

  Display forms we add for imported identifiers

• stPostCurrentModule :: !(Maybe ModuleName)

  The current module is available after it has been type checked.

• stPostInstanceDefs :: !TempInstanceTable
• stPostStatistics :: !Statistics

  Counters to collect various statistics about meta variables etc. Only for current file.

• stPostTCWarnings :: ![TCWarning]
• stPostMutualBlocks :: !(Map MutualId MutualBlock)
• stPostLocalBuiltins :: !(BuiltinThings PrimFun)
• stPostFreshMetaId :: !MetaId
• stPostFreshMutualId :: !MutualId
• stPostFreshCtxId :: !CtxId
• stPostFreshProblemId :: !ProblemId
• stPostFreshInt :: !Int
• stPostFreshNameId :: !NameId

data MutualBlock

A mutual block of names in the signature.

Constructors

MutualBlock

Fields

• mutualInfo :: MutualInfo

  The original info of the mutual block.

• mutualNames :: Set QName

Instances

Eq MutualBlock

Methods

(==) :: MutualBlock -> MutualBlock -> Bool

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

Show MutualBlock

Methods

showsPrec :: Int -> MutualBlock -> ShowS

show :: MutualBlock -> String

showList :: [MutualBlock] -> ShowS

Null MutualBlock

Methods

empty :: MutualBlock

null :: MutualBlock -> Bool

data PersistentTCState

A part of the state which is not reverted when an error is thrown or the state is reset.

Constructors

PersistentTCSt

Fields

• stDecodedModules :: DecodedModules
• stPersistentOptions :: CommandLineOptions
• stInteractionOutputCallback :: InteractionOutputCallback

  Callback function to call when there is a response to give to the interactive frontend. See the documentation of InteractionOutputCallback.

• stBenchmark :: !Benchmark

  Structure to track how much CPU time was spent on which Agda phase. Needs to be a strict field to avoid space leaks!

• stAccumStatistics :: !Statistics

  Should be strict field.

• stLoadedFileCache :: !(Maybe LoadedFileCache)

  Cached typechecking state from the last loaded file. Should be Nothing when checking imports.

• stPersistBackends :: [Backend]

  Current backends with their options

Instances

LensPersistentVerbosity PersistentTCState

Methods

getPersistentVerbosity :: PersistentTCState -> PersistentVerbosity

setPersistentVerbosity :: PersistentVerbosity -> PersistentTCState -> PersistentTCState

mapPersistentVerbosity :: (PersistentVerbosity -> PersistentVerbosity) -> PersistentTCState -> PersistentTCState

LensIncludePaths PersistentTCState

Methods

getIncludePaths :: PersistentTCState -> [FilePath]

setIncludePaths :: [FilePath] -> PersistentTCState -> PersistentTCState

mapIncludePaths :: ([FilePath] -> [FilePath]) -> PersistentTCState -> PersistentTCState

getAbsoluteIncludePaths :: PersistentTCState -> [AbsolutePath]

setAbsoluteIncludePaths :: [AbsolutePath] -> PersistentTCState -> PersistentTCState

mapAbsoluteIncludePaths :: ([AbsolutePath] -> [AbsolutePath]) -> PersistentTCState -> PersistentTCState

LensSafeMode PersistentTCState

Methods

getSafeMode :: PersistentTCState -> SafeMode

setSafeMode :: SafeMode -> PersistentTCState -> PersistentTCState

mapSafeMode :: (SafeMode -> SafeMode) -> PersistentTCState -> PersistentTCState

LensCommandLineOptions PersistentTCState

Methods

getCommandLineOptions :: PersistentTCState -> CommandLineOptions

setCommandLineOptions :: CommandLineOptions -> PersistentTCState -> PersistentTCState

mapCommandLineOptions :: (CommandLineOptions -> CommandLineOptions) -> PersistentTCState -> PersistentTCState

data LoadedFileCache

Constructors

LoadedFileCache

Fields

• lfcCached :: !CachedTypeCheckLog
• lfcCurrent :: !CurrentTypeCheckLog

type CachedTypeCheckLog = [(TypeCheckAction, PostScopeState)]

A log of what the type checker does and states after the action is completed. The cached version is stored first executed action first.

type CurrentTypeCheckLog = [(TypeCheckAction, PostScopeState)]

Like CachedTypeCheckLog, but storing the log for an ongoing type checking of a module. Stored in reverse order (last performed action first).

data TypeCheckAction

A complete log for a module will look like this:

• Pragmas
• EnterSection, entering the main module.
• 'Decl'/'EnterSection'/'LeaveSection', for declarations and nested modules
• LeaveSection, leaving the main module.

Constructors

EnterSection !ModuleInfo !ModuleName ![TypedBindings]

LeaveSection !ModuleName

Decl !Declaration

Never a Section or ScopeDecl

Pragmas !PragmaOptions

initPersistentState :: PersistentTCState

Empty persistent state.

initPreScopeState :: PreScopeState

Empty state of type checker.

initPostScopeState :: PostScopeState

initState :: TCState

st-prefixed lenses

stTokens :: Lens' CompressedFile TCState

stImports :: Lens' Signature TCState

stImportedModules :: Lens' (Set ModuleName) TCState

stModuleToSource :: Lens' ModuleToSource TCState

stVisitedModules :: Lens' VisitedModules TCState

stScope :: Lens' ScopeInfo TCState

stPatternSyns :: Lens' PatternSynDefns TCState

stPatternSynImports :: Lens' PatternSynDefns TCState

stPragmaOptions :: Lens' PragmaOptions TCState

stImportedBuiltins :: Lens' (BuiltinThings PrimFun) TCState

stForeignCode :: Lens' (Map BackendName [ForeignCode]) TCState

stFreshInteractionId :: Lens' InteractionId TCState

stBackends :: Lens' [Backend] TCState

stFreshNameId :: Lens' NameId TCState

stSyntaxInfo :: Lens' CompressedFile TCState

stDisambiguatedNames :: Lens' DisambiguatedNames TCState

stMetaStore :: Lens' MetaStore TCState

stInteractionPoints :: Lens' InteractionPoints TCState

stAwakeConstraints :: Lens' Constraints TCState

stSleepingConstraints :: Lens' Constraints TCState

stDirty :: Lens' Bool TCState

stOccursCheckDefs :: Lens' (Set QName) TCState

stSignature :: Lens' Signature TCState

stModuleParameters :: Lens' ModuleParamDict TCState

stImportsDisplayForms :: Lens' DisplayForms TCState

stImportedDisplayForms :: Lens' DisplayForms TCState

stCurrentModule :: Lens' (Maybe ModuleName) TCState

stImportedInstanceDefs :: Lens' InstanceTable TCState

stInstanceDefs :: Lens' TempInstanceTable TCState

stStatistics :: Lens' Statistics TCState

stTCWarnings :: Lens' [TCWarning] TCState

stMutualBlocks :: Lens' (Map MutualId MutualBlock) TCState

stLocalBuiltins :: Lens' (BuiltinThings PrimFun) TCState

stFreshMetaId :: Lens' MetaId TCState

stFreshMutualId :: Lens' MutualId TCState

stFreshCtxId :: Lens' CtxId TCState

stFreshProblemId :: Lens' ProblemId TCState

stFreshInt :: Lens' Int TCState

stBuiltinThings :: TCState -> BuiltinThings PrimFun

Fresh things

class Enum i => HasFresh i where

Minimal complete definition

freshLens

Methods

freshLens :: Lens' i TCState

nextFresh' :: i -> i

Instances

HasFresh Int

Methods

freshLens :: Lens' Int TCState

nextFresh' :: Int -> Int

HasFresh InteractionId

Methods

freshLens :: Lens' InteractionId TCState

nextFresh' :: InteractionId -> InteractionId

HasFresh MetaId

Methods

freshLens :: Lens' MetaId TCState

nextFresh' :: MetaId -> MetaId

HasFresh NameId

Methods

freshLens :: Lens' NameId TCState

nextFresh' :: NameId -> NameId

HasFresh CtxId

Methods

freshLens :: Lens' CtxId TCState

nextFresh' :: CtxId -> CtxId

HasFresh MutualId

Methods

freshLens :: Lens' MutualId TCState

nextFresh' :: MutualId -> MutualId

HasFresh ProblemId

Methods

freshLens :: Lens' ProblemId TCState

nextFresh' :: ProblemId -> ProblemId

nextFresh :: HasFresh i => TCState -> (i, TCState)

fresh :: (HasFresh i, MonadState TCState m) => m i

newtype ProblemId

Constructors

ProblemId Nat

Instances

Enum ProblemId

Methods

succ :: ProblemId -> ProblemId

pred :: ProblemId -> ProblemId

toEnum :: Int -> ProblemId

fromEnum :: ProblemId -> Int

enumFrom :: ProblemId -> [ProblemId]

enumFromThen :: ProblemId -> ProblemId -> [ProblemId]

enumFromTo :: ProblemId -> ProblemId -> [ProblemId]

enumFromThenTo :: ProblemId -> ProblemId -> ProblemId -> [ProblemId]

Eq ProblemId

Methods

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

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

Integral ProblemId

Methods

quot :: ProblemId -> ProblemId -> ProblemId

rem :: ProblemId -> ProblemId -> ProblemId

div :: ProblemId -> ProblemId -> ProblemId

mod :: ProblemId -> ProblemId -> ProblemId

quotRem :: ProblemId -> ProblemId -> (ProblemId, ProblemId)

divMod :: ProblemId -> ProblemId -> (ProblemId, ProblemId)

toInteger :: ProblemId -> Integer

Data ProblemId

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 :: (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

Methods

(+) :: ProblemId -> ProblemId -> ProblemId

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

(*) :: ProblemId -> ProblemId -> ProblemId

negate :: ProblemId -> ProblemId

abs :: ProblemId -> ProblemId

signum :: ProblemId -> ProblemId

fromInteger :: Integer -> ProblemId

Ord ProblemId

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

Methods

toRational :: ProblemId -> Rational

Show ProblemId

Methods

showsPrec :: Int -> ProblemId -> ShowS

show :: ProblemId -> String

showList :: [ProblemId] -> ShowS

Pretty ProblemId

Methods

pretty :: ProblemId -> Doc

prettyPrec :: Int -> ProblemId -> Doc

prettyList :: [ProblemId] -> Doc

HasFresh ProblemId

Methods

freshLens :: Lens' ProblemId TCState

nextFresh' :: ProblemId -> ProblemId

PrettyTCM ProblemId

Methods

prettyTCM :: ProblemId -> TCM Doc

freshName :: MonadState TCState m => Range -> String -> m Name

freshNoName :: MonadState TCState m => Range -> m Name

freshNoName_ :: MonadState TCState m => m Name

class FreshName a where

Create a fresh name from a.

Minimal complete definition

freshName_

Methods

freshName_ :: MonadState TCState m => a -> m Name

Instances

FreshName ()

Methods

freshName_ :: MonadState TCState m => () -> m Name

FreshName String

Methods

freshName_ :: MonadState TCState m => String -> m Name

FreshName Range

Methods

freshName_ :: MonadState TCState m => Range -> m Name

FreshName (Range, String)

Methods

freshName_ :: MonadState TCState m => (Range, String) -> m Name

Managing file names

type ModuleToSource = Map TopLevelModuleName AbsolutePath

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

type SourceToModule = Map AbsolutePath TopLevelModuleName

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

sourceToModule :: TCM SourceToModule

Creates a SourceToModule map based on stModuleToSource.

O(n log n).

For a single reverse lookup in stModuleToSource, rather use lookupModuleFromSourse.

lookupModuleFromSource :: AbsolutePath -> TCM (Maybe TopLevelModuleName)

Lookup an AbsolutePath in sourceToModule.

O(n).

Interface

data ModuleInfo

Constructors

ModuleInfo

Fields

• miInterface :: Interface
• miWarnings :: Bool

  True if warnings were encountered when the module was type checked.

type VisitedModules = Map TopLevelModuleName ModuleInfo

type DecodedModules = Map TopLevelModuleName Interface

data ForeignCode

Constructors

ForeignCode Range String

Instances

Show ForeignCode

Methods

showsPrec :: Int -> ForeignCode -> ShowS

show :: ForeignCode -> String

showList :: [ForeignCode] -> ShowS

data Interface

Constructors

Interface

Fields

• iSourceHash :: Hash

  Hash of the source code.

• iImportedModules :: [(ModuleName, Hash)]

  Imported modules and their hashes.

• iModuleName :: ModuleName

  Module name of this interface.

• iScope :: Map ModuleName Scope

  Scope defined by this module.

  Andreas, AIM XX: Too avoid duplicate serialization, this field is not serialized, so if you deserialize an interface, iScope will be empty. But constructIScope constructs iScope from iInsideScope.

• iInsideScope :: ScopeInfo

  Scope after we loaded this interface. Used in AtTopLevel and interactionLoop.

• iSignature :: Signature
• iDisplayForms :: DisplayForms

  Display forms added for imported identifiers.

• iBuiltin :: BuiltinThings (String, QName)
• iForeignCode :: Map BackendName [ForeignCode]
• iHighlighting :: HighlightingInfo
• iPragmaOptions :: [OptionsPragma]

  Pragma options set in the file.

• iPatternSyns :: PatternSynDefns
• iWarnings :: [TCWarning]

Instances

Show Interface

Methods

showsPrec :: Int -> Interface -> ShowS

show :: Interface -> String

showList :: [Interface] -> ShowS

Pretty Interface

Methods

pretty :: Interface -> Doc

prettyPrec :: Int -> Interface -> Doc

prettyList :: [Interface] -> Doc

InstantiateFull Interface

Methods

instantiateFull' :: Interface -> ReduceM Interface

iFullHash :: Interface -> Hash

Combines the source hash and the (full) hashes of the imported modules.

Closure

data Closure a

Constructors

Closure

Fields

• clSignature :: Signature
• clEnv :: TCEnv
• clScope :: ScopeInfo
• clModuleParameters :: ModuleParamDict

  Since module parameters are currently stored in TCState not in TCEnv, we save them here. The map contains for each ModuleName M with module telescope Γ_M a substitution Γ ⊢ ρ_M : Γ_M from the current context Γ = envContext (clEnv).

• clValue :: a

Instances

Functor Closure

Methods

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

(<$) :: a -> Closure b -> Closure a

Foldable Closure

Methods

fold :: Monoid m => Closure m -> 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

Data a => Data (Closure a)

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 :: (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)

Methods

showsPrec :: Int -> Closure a -> ShowS

show :: Closure a -> String

showList :: [Closure a] -> ShowS

HasRange a => HasRange (Closure a)

Methods

getRange :: Closure a -> Range

PrettyTCM a => PrettyTCM (Closure a)

Methods

prettyTCM :: Closure a -> TCM Doc

MentionsMeta a => MentionsMeta (Closure a)

Methods

mentionsMeta :: MetaId -> Closure a -> Bool

InstantiateFull a => InstantiateFull (Closure a)

Methods

instantiateFull' :: Closure a -> ReduceM (Closure a)

Normalise a => Normalise (Closure a)

Methods

normalise' :: Closure a -> ReduceM (Closure a)

Simplify a => Simplify (Closure a)

Methods

simplify' :: Closure a -> ReduceM (Closure a)

Reduce a => Reduce (Closure a)

Methods

reduce' :: Closure a -> ReduceM (Closure a)

reduceB' :: Closure a -> ReduceM (Blocked (Closure a))

Instantiate a => Instantiate (Closure a)

Methods

instantiate' :: Closure a -> ReduceM (Closure a)

buildClosure :: a -> TCM (Closure a)

Constraints

type Constraints = [ProblemConstraint]

data ProblemConstraint

Constructors

PConstr

Fields

• constraintProblems :: Set ProblemId
• theConstraint :: Closure Constraint

Instances

Data ProblemConstraint

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 :: (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

Methods

showsPrec :: Int -> ProblemConstraint -> ShowS

show :: ProblemConstraint -> String

showList :: [ProblemConstraint] -> ShowS

HasRange ProblemConstraint

Methods

getRange :: ProblemConstraint -> Range

PrettyTCM ProblemConstraint

Methods

prettyTCM :: ProblemConstraint -> TCM Doc

MentionsMeta ProblemConstraint

Methods

mentionsMeta :: MetaId -> ProblemConstraint -> Bool

InstantiateFull ProblemConstraint

Methods

instantiateFull' :: ProblemConstraint -> ReduceM ProblemConstraint

Normalise ProblemConstraint

Methods

normalise' :: ProblemConstraint -> ReduceM ProblemConstraint

Simplify ProblemConstraint

Methods

simplify' :: ProblemConstraint -> ReduceM ProblemConstraint

data Constraint

Constructors

ValueCmp Comparison Type Term Term

ElimCmp [Polarity] Type Term [Elim] [Elim]

TypeCmp Comparison Type Type

TelCmp Type Type Comparison Telescope Telescope

the two types are for the error message only

SortCmp Comparison Sort Sort

LevelCmp Comparison Level Level

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.

FindInScope 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)

Instances

Data Constraint

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 :: (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

Methods

showsPrec :: Int -> Constraint -> ShowS

show :: Constraint -> String

showList :: [Constraint] -> ShowS

HasRange Constraint

Methods

getRange :: Constraint -> Range

Free Constraint

Methods

freeVars' :: IsVarSet c => Constraint -> FreeM c

TermLike Constraint

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Constraint -> m Constraint

foldTerm :: Monoid m => (Term -> m) -> Constraint -> m

PrettyTCM Constraint

Methods

prettyTCM :: Constraint -> TCM Doc

MentionsMeta Constraint

Methods

mentionsMeta :: MetaId -> Constraint -> Bool

InstantiateFull Constraint

Methods

instantiateFull' :: Constraint -> ReduceM Constraint

Normalise Constraint

Methods

normalise' :: Constraint -> ReduceM Constraint

Simplify Constraint

Methods

simplify' :: Constraint -> ReduceM Constraint

Reduce Constraint

Methods

reduce' :: Constraint -> ReduceM Constraint

reduceB' :: Constraint -> ReduceM (Blocked Constraint)

Instantiate Constraint

Methods

instantiate' :: Constraint -> ReduceM Constraint

data Comparison

Constructors

CmpEq

CmpLeq

Instances

Eq Comparison

Methods

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

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

Data Comparison

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 :: (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

Methods

showsPrec :: Int -> Comparison -> ShowS

show :: Comparison -> String

showList :: [Comparison] -> ShowS

Pretty Comparison

Methods

pretty :: Comparison -> Doc

prettyPrec :: Int -> Comparison -> Doc

prettyList :: [Comparison] -> Doc

PrettyTCM Comparison

Methods

prettyTCM :: Comparison -> TCM Doc

data CompareDirection

An extension of Comparison to >=.

Constructors

DirEq

DirLeq

DirGeq

Instances

Eq CompareDirection

Methods

(==) :: CompareDirection -> CompareDirection -> Bool

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

Show CompareDirection

Methods

showsPrec :: Int -> CompareDirection -> ShowS

show :: CompareDirection -> String

showList :: [CompareDirection] -> ShowS

Pretty CompareDirection

Methods

pretty :: CompareDirection -> Doc

prettyPrec :: Int -> CompareDirection -> Doc

prettyList :: [CompareDirection] -> Doc

fromCmp :: Comparison -> CompareDirection

Embed Comparison into CompareDirection.

flipCmp :: CompareDirection -> CompareDirection

Flip the direction of comparison.

dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c

Turn a Comparison function into a CompareDirection function.

Property: dirToCmp f (fromCmp cmp) = f cmp

Open things

data Open a

A thing tagged with the context it came from.

Constructors

OpenThing

Fields

• openThingCtxIds :: [CtxId]
• openThing :: a

Instances

Functor Open

Methods

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

(<$) :: a -> Open b -> Open a

Foldable Open

Methods

fold :: Monoid m => Open m -> 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

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

Methods

traverseF :: Functor m => (a -> m b) -> Open a -> m (Open b)

distributeF :: Functor m => Open (m a) -> m (Open a)

Data a => Data (Open a)

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 :: (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)

Methods

showsPrec :: Int -> Open a -> ShowS

show :: Open a -> String

showList :: [Open a] -> ShowS

KillRange a => KillRange (Open a)

Methods

killRange :: KillRangeT (Open a)

NamesIn a => NamesIn (Open a)

Methods

namesIn :: Open a -> Set QName

InstantiateFull a => InstantiateFull (Open a)

Methods

instantiateFull' :: Open a -> ReduceM (Open a)

data Local a

Constructors

Local ModuleName a

Local to a given module, the value should have module parameters as free variables.

Global a

Global value, should be closed.

Instances

Functor Local

Methods

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

(<$) :: a -> Local b -> Local a

Foldable Local

Methods

fold :: Monoid m => Local m -> m

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

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

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

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

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

foldr1 :: (a -> a -> a) -> Local a -> a

foldl1 :: (a -> a -> a) -> Local a -> a

toList :: Local a -> [a]

null :: Local a -> Bool

length :: Local a -> Int

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

maximum :: Ord a => Local a -> a

minimum :: Ord a => Local a -> a

sum :: Num a => Local a -> a

product :: Num a => Local a -> a

Traversable Local

Methods

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

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

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

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

Decoration Local

Methods

traverseF :: Functor m => (a -> m b) -> Local a -> m (Local b)

distributeF :: Functor m => Local (m a) -> m (Local a)

Data a => Data (Local a)

Methods

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

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

toConstr :: Local a -> Constr

dataTypeOf :: Local a -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (Local a))

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

gmapT :: (forall b. Data b => b -> b) -> Local a -> Local a

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

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

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

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

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

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

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

Show a => Show (Local a)

Methods

showsPrec :: Int -> Local a -> ShowS

show :: Local a -> String

showList :: [Local a] -> ShowS

KillRange a => KillRange (Local a)

Methods

killRange :: KillRangeT (Local a)

NamesIn a => NamesIn (Local a)

Methods

namesIn :: Local a -> Set QName

InstantiateFull a => InstantiateFull (Local a)

Methods

instantiateFull' :: Local a -> ReduceM (Local a)

isGlobal :: Local a -> Bool

Judgements

data Judgement a

Parametrized since it is used without MetaId when creating a new meta.

Constructors

HasType

Fields

• jMetaId :: a
• jMetaType :: Type

IsSort

Fields

• jMetaId :: a
• jMetaType :: Type

Instances

Show a => Show (Judgement a)

Methods

showsPrec :: Int -> Judgement a -> ShowS

show :: Judgement a -> String

showList :: [Judgement a] -> ShowS

PrettyTCM a => PrettyTCM (Judgement a)

Methods

prettyTCM :: Judgement a -> TCM Doc

Meta variables

data MetaVariable

Constructors

MetaVar

Fields

• mvInfo :: MetaInfo
• mvPriority :: MetaPriority

  some metavariables are more eager to be instantiated

• mvPermutation :: Permutation

  a metavariable doesn't have to depend on all variables in the context, this "permutation" will throw away the ones it does not depend on

• mvJudgement :: Judgement MetaId
• mvInstantiation :: MetaInstantiation
• mvListeners :: Set Listener

  meta variables scheduled for eta-expansion but blocked by this one

• mvFrozen :: Frozen

  are we past the point where we can instantiate this meta variable?

Instances

SetRange MetaVariable

Methods

setRange :: Range -> MetaVariable -> MetaVariable

HasRange MetaVariable

Methods

getRange :: MetaVariable -> Range

data Listener

Constructors

EtaExpand MetaId

CheckConstraint Nat ProblemConstraint

Instances

Eq Listener

Methods

(==) :: Listener -> Listener -> Bool

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

Ord Listener

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 Frozen

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

Eq Frozen

Methods

(==) :: Frozen -> Frozen -> Bool

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

Show Frozen

Methods

showsPrec :: Int -> Frozen -> ShowS

show :: Frozen -> String

showList :: [Frozen] -> ShowS

data MetaInstantiation

Constructors

InstV [Arg String] Term

solved by term (abstracted over some free variables)

Open

unsolved

OpenIFS

open, to be instantiated as "implicit from scope"

BlockedConst Term

solution blocked by unsolved constraints

PostponedTypeCheckingProblem (Closure TypeCheckingProblem) (TCM Bool)

Instances

Show MetaInstantiation

Methods

showsPrec :: Int -> MetaInstantiation -> ShowS

show :: MetaInstantiation -> String

showList :: [MetaInstantiation] -> ShowS

data TypeCheckingProblem

Constructors

CheckExpr Expr Type

CheckArgs ExpandHidden Range [NamedArg Expr] Type Type (Args -> Type -> TCM Term)

CheckLambda (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.

UnquoteTactic Term Term Type

First argument is computation and the others are hole and goal type

Instances

PrettyTCM TypeCheckingProblem

Methods

prettyTCM :: TypeCheckingProblem -> TCM Doc

newtype MetaPriority

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

Eq MetaPriority

Methods

(==) :: MetaPriority -> MetaPriority -> Bool

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

Ord MetaPriority

Methods

compare :: MetaPriority -> MetaPriority -> Ordering

(<) :: MetaPriority -> MetaPriority -> Bool

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

(>) :: MetaPriority -> MetaPriority -> Bool

(>=) :: MetaPriority -> MetaPriority -> Bool

max :: MetaPriority -> MetaPriority -> MetaPriority

min :: MetaPriority -> MetaPriority -> MetaPriority

Show MetaPriority

Methods

showsPrec :: Int -> MetaPriority -> ShowS

show :: MetaPriority -> String

showList :: [MetaPriority] -> ShowS

data RunMetaOccursCheck

Constructors

RunMetaOccursCheck

DontRunMetaOccursCheck

Instances

Eq RunMetaOccursCheck

Methods

(==) :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool

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

Ord RunMetaOccursCheck

Methods

compare :: RunMetaOccursCheck -> RunMetaOccursCheck -> Ordering

(<) :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool

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

(>) :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool

(>=) :: RunMetaOccursCheck -> RunMetaOccursCheck -> Bool

max :: RunMetaOccursCheck -> RunMetaOccursCheck -> RunMetaOccursCheck

min :: RunMetaOccursCheck -> RunMetaOccursCheck -> RunMetaOccursCheck

Show RunMetaOccursCheck

Methods

showsPrec :: Int -> RunMetaOccursCheck -> ShowS

show :: RunMetaOccursCheck -> String

showList :: [RunMetaOccursCheck] -> ShowS

data MetaInfo

MetaInfo is cloned from one meta to the next during pruning.

Constructors

MetaInfo

Fields

• miClosRange :: Closure Range
• miMetaOccursCheck :: RunMetaOccursCheck

  Run the extended occurs check that goes in definitions?

• miNameSuggestion :: MetaNameSuggestion

  Used for printing. Just x if meta-variable comes from omitted argument with name x.

Instances

SetRange MetaInfo

Methods

setRange :: Range -> MetaInfo -> MetaInfo

HasRange MetaInfo

Methods

getRange :: MetaInfo -> Range

type MetaNameSuggestion = String

Name suggestion for meta variable. Empty string means no suggestion.

data NamedMeta

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

Constructors

NamedMeta

Fields

• nmSuggestion :: MetaNameSuggestion
• nmid :: MetaId

Instances

Pretty NamedMeta

Methods

pretty :: NamedMeta -> Doc

prettyPrec :: Int -> NamedMeta -> Doc

prettyList :: [NamedMeta] -> Doc

ToConcrete NamedMeta Expr

Methods

toConcrete :: NamedMeta -> AbsToCon Expr

bindToConcrete :: NamedMeta -> (Expr -> AbsToCon b) -> AbsToCon b

type MetaStore = Map MetaId MetaVariable

normalMetaPriority :: MetaPriority

lowMetaPriority :: MetaPriority

highMetaPriority :: MetaPriority

getMetaInfo :: MetaVariable -> Closure Range

getMetaScope :: MetaVariable -> ScopeInfo

getMetaEnv :: MetaVariable -> TCEnv

getMetaSig :: MetaVariable -> Signature

getMetaRelevance :: MetaVariable -> Relevance

Interaction meta variables

data InteractionPoint

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

Eq InteractionPoint

Methods

(==) :: InteractionPoint -> InteractionPoint -> Bool

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

type InteractionPoints = Map InteractionId InteractionPoint

Data structure managing the interaction points.

We never remove interaction points from this map, only set their ipSolved to True. (Issue #2368)

data IPClause

Which clause is an interaction point located in?

Constructors

IPClause

Fields

• ipcQName :: QName

  The name of the function.

• ipcClauseNo :: Int

  The number of the clause of this function.

• ipcClause :: RHS

  The original AST clause rhs.

IPNoClause

The interaction point is not in the rhs of a clause.

Instances

Eq IPClause

Methods

(==) :: IPClause -> IPClause -> Bool

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

Data IPClause

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 :: (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

Signature

data Signature

Constructors

Sig

Fields

• _sigSections :: Sections
• _sigDefinitions :: Definitions
• _sigRewriteRules :: RewriteRuleMap

  The rewrite rules defined in this file.

Instances

Data Signature

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 :: (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

Methods

showsPrec :: Int -> Signature -> ShowS

show :: Signature -> String

showList :: [Signature] -> ShowS

KillRange Signature

Methods

killRange :: KillRangeT Signature

InstantiateFull Signature

Methods

instantiateFull' :: Signature -> ReduceM Signature

sigSections :: Lens' Sections Signature

sigDefinitions :: Lens' Definitions Signature

sigRewriteRules :: Lens' RewriteRuleMap Signature

type Sections = Map ModuleName Section

type Definitions = HashMap QName Definition

type RewriteRuleMap = HashMap QName RewriteRules

type DisplayForms = HashMap QName [LocalDisplayForm]

newtype Section

Constructors

Section

Fields

• _secTelescope :: Telescope

Instances

Data Section

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 :: (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

Methods

showsPrec :: Int -> Section -> ShowS

show :: Section -> String

showList :: [Section] -> ShowS

Pretty Section

Methods

pretty :: Section -> Doc

prettyPrec :: Int -> Section -> Doc

prettyList :: [Section] -> Doc

KillRange Section

Methods

killRange :: KillRangeT Section

KillRange Sections

Methods

killRange :: KillRangeT Sections

InstantiateFull Section

Methods

instantiateFull' :: Section -> ReduceM Section

secTelescope :: Lens' Telescope Section

emptySignature :: Signature

data DisplayForm

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

• dfFreeVars :: Nat

  Number n of free variables in dfRHS.

• dfPats :: Elims

  Left hand side patterns, where var 0 stands for a pattern variable. There should be n occurrences of var0 in dfPats. The ArgInfo is ignored in these patterns.

• dfRHS :: DisplayTerm

  Right hand side, with n free variables.

Instances

Data DisplayForm

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 :: (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

Methods

showsPrec :: Int -> DisplayForm -> ShowS

show :: DisplayForm -> String

showList :: [DisplayForm] -> ShowS

KillRange DisplayForm

Methods

killRange :: KillRangeT DisplayForm

Free DisplayForm

Methods

freeVars' :: IsVarSet c => DisplayForm -> FreeM c

NamesIn DisplayForm

Methods

namesIn :: DisplayForm -> Set QName

InstantiateFull DisplayForm

Methods

instantiateFull' :: DisplayForm -> ReduceM DisplayForm

Normalise DisplayForm

Methods

normalise' :: DisplayForm -> ReduceM DisplayForm

Simplify DisplayForm

Methods

simplify' :: DisplayForm -> ReduceM DisplayForm

type LocalDisplayForm = Local DisplayForm

data DisplayTerm

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

Data DisplayTerm

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 :: (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

Methods

showsPrec :: Int -> DisplayTerm -> ShowS

show :: DisplayTerm -> String

showList :: [DisplayTerm] -> ShowS

Pretty DisplayTerm

Methods

pretty :: DisplayTerm -> Doc

prettyPrec :: Int -> DisplayTerm -> Doc

prettyList :: [DisplayTerm] -> Doc

KillRange DisplayTerm

Methods

killRange :: KillRangeT DisplayTerm

Free DisplayTerm

Methods

freeVars' :: IsVarSet c => DisplayTerm -> FreeM c

PrettyTCM DisplayTerm

Methods

prettyTCM :: DisplayTerm -> TCM Doc

NamesIn DisplayTerm

Methods

namesIn :: DisplayTerm -> Set QName

InstantiateFull DisplayTerm

Methods

instantiateFull' :: DisplayTerm -> ReduceM DisplayTerm

SubstWithOrigin DisplayTerm

Methods

substWithOrigin :: Substitution -> [WithOrigin Term] -> DisplayTerm -> DisplayTerm

Reify DisplayTerm Expr

Methods

reify :: DisplayTerm -> TCM Expr

reifyWhen :: Bool -> DisplayTerm -> TCM Expr

PrettyTCM (Elim' DisplayTerm)

Methods

prettyTCM :: Elim' DisplayTerm -> TCM Doc

SubstWithOrigin (Arg DisplayTerm)

Methods

substWithOrigin :: Substitution -> [WithOrigin Term] -> Arg DisplayTerm -> Arg DisplayTerm

defaultDisplayForm :: QName -> [LocalDisplayForm]

By default, we have no display form.

defRelevance :: Definition -> Relevance

data NLPat

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.

PWild

Matches anything (e.g. irrelevant terms).

PDef QName PElims

Matches f es

PLam ArgInfo (Abs NLPat)

Matches λ x → t

PPi (Dom NLPType) (Abs NLPType)

Matches (x : A) → B

PBoundVar !Int PElims

Matches x es where x is a lambda-bound variable

PTerm Term

Matches the term modulo β (ideally βη).

Instances

Data NLPat

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 :: (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

Methods

showsPrec :: Int -> NLPat -> ShowS

show :: NLPat -> String

showList :: [NLPat] -> ShowS

KillRange NLPat

Methods

killRange :: KillRangeT NLPat

PrettyTCM NLPat

Methods

prettyTCM :: NLPat -> TCM Doc

InstantiateFull NLPat

Methods

instantiateFull' :: NLPat -> ReduceM NLPat

GetMatchables NLPat

Methods

getMatchables :: NLPat -> [QName]

NLPatVars NLPat

Methods

nlPatVarsUnder :: Int -> NLPat -> IntSet

nlPatVars :: NLPat -> IntSet

Match NLPat Level

Methods

match :: Relevance -> Telescope -> Telescope -> NLPat -> Level -> NLM ()

Match NLPat Sort

Methods

match :: Relevance -> Telescope -> Telescope -> NLPat -> Sort -> NLM ()

Match NLPat Term

Methods

match :: Relevance -> Telescope -> Telescope -> NLPat -> Term -> NLM ()

PatternFrom Sort NLPat

Methods

patternFrom :: Relevance -> Int -> Sort -> TCM NLPat

PatternFrom Term NLPat

Methods

patternFrom :: Relevance -> Int -> Term -> TCM NLPat

PrettyTCM (Type' NLPat)

Methods

prettyTCM :: Type' NLPat -> TCM Doc

PrettyTCM (Elim' NLPat)

Methods

prettyTCM :: Elim' NLPat -> TCM Doc

PatternFrom a NLPat => PatternFrom (Elim' a) (Elim' NLPat)

Methods

patternFrom :: Relevance -> Int -> Elim' a -> TCM (Elim' NLPat)

type PElims = [Elim' NLPat]

data NLPType

Constructors

NLPType

Fields

• nlpTypeLevel :: NLPat
• nlpTypeUnEl :: NLPat

Instances

Data NLPType

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 :: (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

Methods

showsPrec :: Int -> NLPType -> ShowS

show :: NLPType -> String

showList :: [NLPType] -> ShowS

KillRange NLPType

Methods

killRange :: KillRangeT NLPType

PrettyTCM NLPType

Methods

prettyTCM :: NLPType -> TCM Doc

InstantiateFull NLPType

Methods

instantiateFull' :: NLPType -> ReduceM NLPType

NLPatVars NLPType

Methods

nlPatVarsUnder :: Int -> NLPType -> IntSet

nlPatVars :: NLPType -> IntSet

Match NLPType Type

Methods

match :: Relevance -> Telescope -> Telescope -> NLPType -> Type -> NLM ()

PatternFrom Type NLPType

Methods

patternFrom :: Relevance -> Int -> Type -> TCM NLPType

type RewriteRules = [RewriteRule]

data RewriteRule

Rewrite rules can be added independently from function clauses.

Constructors

RewriteRule

Fields

• rewName :: QName

  Name of rewrite rule q : Γ → f ps ≡ rhs where ≡ is the rewrite relation.

• rewContext :: Telescope

  Γ.

• rewHead :: QName

  f.

• rewPats :: PElims

  Γ ⊢ f ps : t.

• rewRHS :: Term

  Γ ⊢ rhs : t.

• rewType :: Type

  Γ ⊢ t.

Instances

Data RewriteRule

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 :: (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

Methods

showsPrec :: Int -> RewriteRule -> ShowS

show :: RewriteRule -> String

showList :: [RewriteRule] -> ShowS

KillRange RewriteRule

Methods

killRange :: KillRangeT RewriteRule

KillRange RewriteRuleMap

Methods

killRange :: KillRangeT RewriteRuleMap

PrettyTCM RewriteRule

Methods

prettyTCM :: RewriteRule -> TCM Doc

InstantiateFull RewriteRule

Methods

instantiateFull' :: RewriteRule -> ReduceM RewriteRule

GetMatchables RewriteRule

Methods

getMatchables :: RewriteRule -> [QName]

data Definition

Constructors

Defn

Fields

• defArgInfo :: ArgInfo

  Hiding should not be used.

• defName :: QName
• defType :: Type

  Type of the lifted definition.

• defPolarity :: [Polarity]

  Variance information on arguments of the definition. Does not include info for dropped parameters to projection(-like) functions and constructors.

• defArgOccurrences :: [Occurrence]

  Positivity information on arguments of the definition. Does not include info for dropped parameters to projection(-like) functions and constructors.

• defDisplay :: [LocalDisplayForm]
• defMutual :: MutualId
• defCompiledRep :: CompiledRepresentation
• defInstance :: Maybe QName

  Just q when this definition is an instance of class q

• defCopy :: Bool

  Has this function been created by a module instantiation?

• defMatchable :: Bool

  Is the def matched against in a rewrite rule?

• defInjective :: Bool

  Should the def be treated as injective by the pattern matching unifier?

• theDef :: Defn

Instances

Data Definition

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 :: (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

Methods

showsPrec :: Int -> Definition -> ShowS

show :: Definition -> String

showList :: [Definition] -> ShowS

Pretty Definition

Methods

pretty :: Definition -> Doc

prettyPrec :: Int -> Definition -> Doc

prettyList :: [Definition] -> Doc

KillRange Definition

Methods

killRange :: KillRangeT Definition

KillRange Definitions

Methods

killRange :: KillRangeT Definitions

NamesIn Definition

Methods

namesIn :: Definition -> Set QName

InstantiateFull Definition

Methods

instantiateFull' :: Definition -> ReduceM Definition

theDefLens :: Lens' Defn Definition

defaultDefn :: ArgInfo -> QName -> Type -> Defn -> Definition

Create a definition with sensible defaults.

data Polarity

Polarity for equality and subtype checking.

Constructors

Covariant

monotone

Contravariant

antitone

Invariant

no information (mixed variance)

Nonvariant

constant

Instances

Eq Polarity

Methods

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

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

Data Polarity

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 :: (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

Methods

showsPrec :: Int -> Polarity -> ShowS

show :: Polarity -> String

showList :: [Polarity] -> ShowS

Pretty Polarity

Methods

pretty :: Polarity -> Doc

prettyPrec :: Int -> Polarity -> Doc

prettyList :: [Polarity] -> Doc

KillRange Polarity

Methods

killRange :: KillRangeT Polarity

PrettyTCM Polarity

Methods

prettyTCM :: Polarity -> TCM Doc

data CompilerPragma

The backends are responsible for parsing their own pragmas.

Constructors

CompilerPragma Range String

Instances

Eq CompilerPragma

Methods

(==) :: CompilerPragma -> CompilerPragma -> Bool

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

Data CompilerPragma

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 :: (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

Methods

showsPrec :: Int -> CompilerPragma -> ShowS

show :: CompilerPragma -> String

showList :: [CompilerPragma] -> ShowS

KillRange CompiledRepresentation

Methods

killRange :: KillRangeT CompiledRepresentation

HasRange CompilerPragma

Methods

getRange :: CompilerPragma -> Range

type BackendName = String

jsBackendName :: BackendName

ghcBackendName :: BackendName

uhcBackendName :: BackendName

type CompiledRepresentation = Map BackendName [CompilerPragma]

noCompiledRep :: CompiledRepresentation

data ExtLamInfo

Additional information for extended lambdas.

Constructors

ExtLamInfo

Fields

• extLamNumHidden :: Int
• extLamNumNonHid :: Int

Instances

Eq ExtLamInfo

Methods

(==) :: ExtLamInfo -> ExtLamInfo -> Bool

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

Data ExtLamInfo

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 :: (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

Ord ExtLamInfo

Methods

compare :: ExtLamInfo -> ExtLamInfo -> Ordering

(<) :: ExtLamInfo -> ExtLamInfo -> Bool

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

(>) :: ExtLamInfo -> ExtLamInfo -> Bool

(>=) :: ExtLamInfo -> ExtLamInfo -> Bool

max :: ExtLamInfo -> ExtLamInfo -> ExtLamInfo

min :: ExtLamInfo -> ExtLamInfo -> ExtLamInfo

Show ExtLamInfo

Methods

showsPrec :: Int -> ExtLamInfo -> ShowS

show :: ExtLamInfo -> String

showList :: [ExtLamInfo] -> ShowS

KillRange ExtLamInfo

Methods

killRange :: KillRangeT ExtLamInfo

data Projection

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

Data Projection

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 :: (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

Methods

showsPrec :: Int -> Projection -> ShowS

show :: Projection -> String

showList :: [Projection] -> ShowS

KillRange Projection

Methods

killRange :: KillRangeT Projection

newtype ProjLams

Abstractions to build projection function (dropping parameters).

Constructors

ProjLams

Fields

• getProjLams :: [Arg ArgName]

Instances

Data ProjLams

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 :: (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

Methods

showsPrec :: Int -> ProjLams -> ShowS

show :: ProjLams -> String

showList :: [ProjLams] -> ShowS

Null ProjLams

Methods

empty :: ProjLams

null :: ProjLams -> Bool

KillRange ProjLams

Methods

killRange :: KillRangeT ProjLams

projDropPars :: Projection -> ProjOrigin -> Term

Building the projection function (which drops the parameters).

projArgInfo :: Projection -> ArgInfo

The info of the principal (record) argument.

data EtaEquality

Should a record type admit eta-equality?

Constructors

Specified !Bool

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

Inferred !Bool

Positivity checker inferred whether eta is safe.

Instances

Eq EtaEquality

Methods

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

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

Data EtaEquality

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 :: (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

Methods

showsPrec :: Int -> EtaEquality -> ShowS

show :: EtaEquality -> String

showList :: [EtaEquality] -> ShowS

KillRange EtaEquality

Methods

killRange :: KillRangeT EtaEquality

etaEqualityToBool :: EtaEquality -> Bool

setEtaEquality :: EtaEquality -> Bool -> EtaEquality

Make sure we do not overwrite a user specification.

data FunctionFlag

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

Enum FunctionFlag

Methods

succ :: FunctionFlag -> FunctionFlag

pred :: FunctionFlag -> FunctionFlag

toEnum :: Int -> FunctionFlag

fromEnum :: FunctionFlag -> Int

enumFrom :: FunctionFlag -> [FunctionFlag]

enumFromThen :: FunctionFlag -> FunctionFlag -> [FunctionFlag]

enumFromTo :: FunctionFlag -> FunctionFlag -> [FunctionFlag]

enumFromThenTo :: FunctionFlag -> FunctionFlag -> FunctionFlag -> [FunctionFlag]

Eq FunctionFlag

Methods

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

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

Data FunctionFlag

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 :: (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

Methods

compare :: FunctionFlag -> FunctionFlag -> Ordering

(<) :: FunctionFlag -> FunctionFlag -> Bool

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

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

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

max :: FunctionFlag -> FunctionFlag -> FunctionFlag

min :: FunctionFlag -> FunctionFlag -> FunctionFlag

Show FunctionFlag

Methods

showsPrec :: Int -> FunctionFlag -> ShowS

show :: FunctionFlag -> String

showList :: [FunctionFlag] -> ShowS

KillRange FunctionFlag

Methods

killRange :: KillRangeT FunctionFlag

data Defn

Constructors

Axiom

Postulate.

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.

• funTreeless :: Maybe Compiled

  Intermediate representation for compiler backends.

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

• funCopatternLHS :: Bool

  Is this a function defined by copatterns?

Datatype

Fields

• dataPars :: Nat

  Number of parameters.

• dataSmallPars :: Permutation

  Parameters that are maybe small.

• dataNonLinPars :: Drop Permutation

  Parameters that appear in indices.

• dataIxs :: Nat

  Number of indices.

• dataInduction :: Induction

  data or codata (legacy).

• dataClause :: Maybe Clause

  This might be in an instantiated module.

• dataCons :: [QName]

  Constructor names.

• dataSort :: Sort
• dataMutual :: Maybe [QName]

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

• dataAbstr :: IsAbstract

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 :: [Arg 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

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?

• conErased :: [Bool]

  Which arguments are erased at runtime (computed during compilation to treeless)

Primitive

Primitive or builtin functions.

Fields

• primAbstr :: IsAbstract
• primName :: String
• primClauses :: [Clause]

  null for primitive functions, not null for builtin functions.

• primCompiled :: Maybe CompiledClauses

  Nothing for primitive functions, Just something for builtin functions.

Instances

Data Defn

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 :: (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

Methods

showsPrec :: Int -> Defn -> ShowS

show :: Defn -> String

showList :: [Defn] -> ShowS

Pretty Defn

Methods

pretty :: Defn -> Doc

prettyPrec :: Int -> Defn -> Doc

prettyList :: [Defn] -> Doc

KillRange Defn

Methods

killRange :: KillRangeT Defn

NamesIn Defn

Methods

namesIn :: Defn -> Set QName

InstantiateFull Defn

Methods

instantiateFull' :: Defn -> ReduceM Defn

Occurs Defn

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> Defn -> TCM Defn

metaOccurs :: MetaId -> Defn -> TCM ()

recRecursive :: Defn -> Bool

Is the record type recursive?

recEtaEquality :: Defn -> Bool

emptyFunction :: Defn

A template for creating Function definitions, with sensible defaults.

funFlag :: FunctionFlag -> Lens' Bool Defn

funStatic :: Lens' Bool Defn

funInline :: Lens' Bool Defn

funMacro :: Lens' Bool Defn

isMacro :: Defn -> Bool

isEmptyFunction :: Defn -> Bool

Checking whether we are dealing with a function yet to be defined.

isCopatternLHS :: [Clause] -> Bool

recCon :: Defn -> QName

defIsRecord :: Defn -> Bool

defIsDataOrRecord :: Defn -> Bool

defConstructors :: Defn -> [QName]

newtype Fields

Constructors

Fields [(Name, Type)]

Instances

Null Fields

Methods

empty :: Fields

null :: Fields -> Bool

data Simplification

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?

Constructors

YesSimplification

NoSimplification

Instances

Eq Simplification

Methods

(==) :: Simplification -> Simplification -> Bool

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

Data Simplification

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 :: (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

Methods

showsPrec :: Int -> Simplification -> ShowS

show :: Simplification -> String

showList :: [Simplification] -> ShowS

Semigroup Simplification

Methods

(<>) :: Simplification -> Simplification -> Simplification

sconcat :: NonEmpty Simplification -> Simplification

stimes :: Integral b => b -> Simplification -> Simplification

Monoid Simplification

Methods

mempty :: Simplification

mappend :: Simplification -> Simplification -> Simplification

mconcat :: [Simplification] -> Simplification

Null Simplification

Methods

empty :: Simplification

null :: Simplification -> Bool

data Reduced no yes

Constructors

NoReduction no

YesReduction Simplification yes

Instances

Functor (Reduced no)

Methods

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

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

data IsReduced

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

Constructors

NotReduced

Reduced (Blocked ())

data MaybeReduced a

Constructors

MaybeRed

Fields

• isReduced :: IsReduced
• ignoreReduced :: a

Instances

Functor MaybeReduced

Methods

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

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

IsProjElim e => IsProjElim (MaybeReduced e)

Methods

isProjElim :: MaybeReduced e -> Maybe (ProjOrigin, QName)

PrettyTCM a => PrettyTCM (MaybeReduced a)

Methods

prettyTCM :: MaybeReduced a -> TCM Doc

type MaybeReducedArgs = [MaybeReduced (Arg Term)]

type MaybeReducedElims = [MaybeReduced Elim]

notReduced :: a -> MaybeReduced a

reduced :: Blocked (Arg Term) -> MaybeReduced (Arg Term)

data AllowedReduction

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.

UnconfirmedReductions

Functions whose termination has not (yet) been confirmed.

NonTerminatingReductions

Functions that have failed termination checking.

Instances

Bounded AllowedReduction

Methods

minBound :: AllowedReduction

maxBound :: AllowedReduction

Enum AllowedReduction

Methods

succ :: AllowedReduction -> AllowedReduction

pred :: AllowedReduction -> AllowedReduction

toEnum :: Int -> AllowedReduction

fromEnum :: AllowedReduction -> Int

enumFrom :: AllowedReduction -> [AllowedReduction]

enumFromThen :: AllowedReduction -> AllowedReduction -> [AllowedReduction]

enumFromTo :: AllowedReduction -> AllowedReduction -> [AllowedReduction]

enumFromThenTo :: AllowedReduction -> AllowedReduction -> AllowedReduction -> [AllowedReduction]

Eq AllowedReduction

Methods

(==) :: AllowedReduction -> AllowedReduction -> Bool

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

Data AllowedReduction

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 :: (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

Methods

compare :: AllowedReduction -> AllowedReduction -> Ordering

(<) :: AllowedReduction -> AllowedReduction -> Bool

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

(>) :: AllowedReduction -> AllowedReduction -> Bool

(>=) :: AllowedReduction -> AllowedReduction -> Bool

max :: AllowedReduction -> AllowedReduction -> AllowedReduction

min :: AllowedReduction -> AllowedReduction -> AllowedReduction

Show AllowedReduction

Methods

showsPrec :: Int -> AllowedReduction -> ShowS

show :: AllowedReduction -> String

showList :: [AllowedReduction] -> ShowS

type AllowedReductions = [AllowedReduction]

allReductions :: AllowedReductions

Not quite all reductions (skip non-terminating reductions)

data PrimFun

Constructors

PrimFun

Fields

• primFunName :: QName
• primFunArity :: Arity
• primFunImplementation :: [Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term)

defClauses :: Definition -> [Clause]

defCompiled :: Definition -> Maybe CompiledClauses

defParameters :: Definition -> Maybe Nat

defCompilerPragmas :: BackendName -> Definition -> [CompilerPragma]

defDelayed :: Definition -> Delayed

Are the clauses of this definition delayed?

defNonterminating :: Definition -> Bool

Has the definition failed the termination checker?

defTerminationUnconfirmed :: Definition -> Bool

Has the definition not termination checked or did the check fail?

defAbstract :: Definition -> IsAbstract

Injectivity

type FunctionInverse = FunctionInverse' Clause

data FunctionInverse' c

Constructors

NotInjective

Inverse (Map TermHead c)

Instances

Functor FunctionInverse'

Methods

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

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

InstantiateFull FunctionInverse

Methods

instantiateFull' :: FunctionInverse -> ReduceM FunctionInverse

DropArgs FunctionInverse

Methods

dropArgs :: Int -> FunctionInverse -> FunctionInverse

Data c => Data (FunctionInverse' c)

Methods

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

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

toConstr :: FunctionInverse' c -> Constr

dataTypeOf :: FunctionInverse' c -> DataType

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

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (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 :: (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)

Methods

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

show :: FunctionInverse' c -> String

showList :: [FunctionInverse' c] -> ShowS

KillRange c => KillRange (FunctionInverse' c)

Methods

killRange :: KillRangeT (FunctionInverse' c)

data TermHead

Constructors

SortHead

PiHead

ConsHead QName

Instances

Eq TermHead

Methods

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

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

Data TermHead

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 :: (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

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

Methods

showsPrec :: Int -> TermHead -> ShowS

show :: TermHead -> String

showList :: [TermHead] -> ShowS

Pretty TermHead

Methods

pretty :: TermHead -> Doc

prettyPrec :: Int -> TermHead -> Doc

prettyList :: [TermHead] -> Doc

KillRange TermHead

Methods

killRange :: KillRangeT TermHead

Mutual blocks

newtype MutualId

Constructors

MutId Int32

Instances

Enum MutualId

Methods

succ :: MutualId -> MutualId

pred :: MutualId -> MutualId

toEnum :: Int -> MutualId

fromEnum :: MutualId -> Int

enumFrom :: MutualId -> [MutualId]

enumFromThen :: MutualId -> MutualId -> [MutualId]

enumFromTo :: MutualId -> MutualId -> [MutualId]

enumFromThenTo :: MutualId -> MutualId -> MutualId -> [MutualId]

Eq MutualId

Methods

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

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

Data MutualId

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 :: (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

Methods

(+) :: MutualId -> MutualId -> MutualId

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

(*) :: MutualId -> MutualId -> MutualId

negate :: MutualId -> MutualId

abs :: MutualId -> MutualId

signum :: MutualId -> MutualId

fromInteger :: Integer -> MutualId

Ord MutualId

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

Methods

showsPrec :: Int -> MutualId -> ShowS

show :: MutualId -> String

showList :: [MutualId] -> ShowS

KillRange MutualId

Methods

killRange :: KillRangeT MutualId

HasFresh MutualId

Methods

freshLens :: Lens' MutualId TCState

nextFresh' :: MutualId -> MutualId

Statistics

type Statistics = Map String Integer

Trace

data Call

Constructors

CheckClause Type SpineClause

CheckPattern Pattern Telescope Type

CheckLetBinding LetBinding

InferExpr Expr

CheckExprCall Expr Type

CheckDotPattern Expr Term

CheckPatternShadowing SpineClause

CheckProjection Range QName Type

IsTypeCall Expr Sort

IsType_ Expr

InferVar Name

InferDef QName

CheckArguments Range [NamedArg Expr] Type Type

CheckDataDef Range Name [LamBinding] [Constructor]

CheckRecDef Range Name [LamBinding] [Constructor]

CheckConstructor QName Telescope Sort Constructor

CheckFunDef Range Name [Clause]

CheckPragma Range Pragma

CheckPrimitive Range Name Expr

CheckIsEmpty Range Type

CheckWithFunctionType Expr

CheckSectionApplication Range ModuleName ModuleApplication

ScopeCheckExpr Expr

ScopeCheckDeclaration NiceDeclaration

ScopeCheckLHS QName Pattern

NoHighlighting

ModuleContents

Interaction command: show module contents.

SetRange Range

used by setCurrentRange

Instances

Data Call

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 :: (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

Methods

pretty :: Call -> Doc

prettyPrec :: Int -> Call -> Doc

prettyList :: [Call] -> Doc

HasRange Call

Methods

getRange :: Call -> Range

Instance table

type InstanceTable = Map QName (Set QName)

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

type TempInstanceTable = (InstanceTable, Set QName)

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.

Builtin things

data BuiltinDescriptor

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.

data BuiltinInfo

Constructors

BuiltinInfo

Fields

• builtinName :: String
• builtinDesc :: BuiltinDescriptor

type BuiltinThings pf = Map String (Builtin pf)

data Builtin pf

Constructors

Builtin Term

Prim pf

Instances

Functor Builtin

Methods

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

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

Foldable Builtin

Methods

fold :: Monoid m => Builtin m -> 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

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)

Methods

showsPrec :: Int -> Builtin pf -> ShowS

show :: Builtin pf -> String

showList :: [Builtin pf] -> ShowS

InstantiateFull a => InstantiateFull (Builtin a)

Methods

instantiateFull' :: Builtin a -> ReduceM (Builtin a)

Highlighting levels

data HighlightingLevel

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

Eq HighlightingLevel

Methods

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

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

Data HighlightingLevel

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 :: (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

Methods

compare :: HighlightingLevel -> HighlightingLevel -> Ordering

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

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

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

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

max :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel

min :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel

Read HighlightingLevel

Methods

readsPrec :: Int -> ReadS HighlightingLevel

readList :: ReadS [HighlightingLevel]

readPrec :: ReadPrec HighlightingLevel

readListPrec :: ReadPrec [HighlightingLevel]

Show HighlightingLevel

Methods

showsPrec :: Int -> HighlightingLevel -> ShowS

show :: HighlightingLevel -> String

showList :: [HighlightingLevel] -> ShowS

data HighlightingMethod

How should highlighting be sent to the user interface?

Constructors

Direct

Via stdout.

Indirect

Both via files and via stdout.

Instances

Eq HighlightingMethod

Methods

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

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

Data HighlightingMethod

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 :: (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

Methods

readsPrec :: Int -> ReadS HighlightingMethod

readList :: ReadS [HighlightingMethod]

readPrec :: ReadPrec HighlightingMethod

readListPrec :: ReadPrec [HighlightingMethod]

Show HighlightingMethod

Methods

showsPrec :: Int -> HighlightingMethod -> ShowS

show :: HighlightingMethod -> String

showList :: [HighlightingMethod] -> ShowS

ifTopLevelAndHighlightingLevelIsOr :: MonadTCM tcm => HighlightingLevel -> Bool -> tcm () -> tcm ()

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 ()

ifTopLevelAndHighlightingLevelIs l m runs m when we're type-checking the top-level module and the highlighting level is at least l.

Type checking environment

data ModuleParameters

Constructors

ModuleParams

Fields

• mpSubstitution :: Substitution

  Δ ⊢ σ : Γ for a module M Γ where Δ is the current context envContext.

Instances

Data ModuleParameters

Methods

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

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

toConstr :: ModuleParameters -> Constr

dataTypeOf :: ModuleParameters -> DataType

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

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

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

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

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

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

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

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

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

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

Show ModuleParameters

Methods

showsPrec :: Int -> ModuleParameters -> ShowS

show :: ModuleParameters -> String

showList :: [ModuleParameters] -> ShowS

PrettyTCM ModuleParameters

Methods

prettyTCM :: ModuleParameters -> TCM Doc

defaultModuleParameters :: ModuleParameters

type ModuleParamDict

Arguments

 = Map ModuleName ModuleParameters

The map contains for each ModuleName M with module telescope Γ_M a substitution Γ ⊢ ρ_M : Γ_M from the current context Γ = envContext (clEnv).

data TCEnv

Constructors

TCEnv

Fields

• envContext :: Context
• envLetBindings :: LetBindings
• envCurrentModule :: ModuleName
• envCurrentPath :: Maybe AbsolutePath

  The path to the file that is currently being type-checked. Nothing if we do not have a file (like in interactive mode see CommandLine).

• envAnonymousModules :: [(ModuleName, Nat)]

  anonymous modules and their number of free variables

• envImportPath :: [TopLevelModuleName]

  to detect import cycles

• envMutualBlock :: Maybe MutualId

  the current (if any) mutual block

• envTerminationCheck :: TerminationCheck ()

  are we inside the scope of a termination pragma

• envSolvingConstraints :: Bool

  Are we currently in the process of solving active constraints?

• envCheckingWhere :: Bool

  Have we stepped into the where-declarations of a clause? Everything under a where will be checked with this flag on.

• envAssignMetas :: Bool

  Are we allowed to assign metas?

• envActiveProblems :: Set ProblemId
• envAbstractMode :: AbstractMode

  When checking the typesignature of a public definition or the body of a non-abstract definition this is true. To prevent information about abstract things leaking outside the module.

• envRelevance :: Relevance

  Are we checking an irrelevant argument? (=Irrelevant) Then top-level irrelevant declarations are enabled. Other value: Relevant, then only relevant decls. are avail.

• envDisplayFormsEnabled :: Bool

  Sometimes we want to disable display forms.

• envRange :: Range
• envHighlightingRange :: Range

  Interactive highlighting uses this range rather than envRange.

• envClause :: IPClause

  What is the current clause we are type-checking? Will be recorded in interaction points in this clause.

• envCall :: Maybe (Closure Call)

  what we're doing at the moment

• envHighlightingLevel :: HighlightingLevel

  Set to None when imported modules are type-checked.

• envHighlightingMethod :: HighlightingMethod
• envModuleNestingLevel :: !Int

  This number indicates how far away from the top-level module Agda has come when chasing modules. The level of a given module is not necessarily the same as the length, in the module dependency graph, of the shortest path from the top-level module; it depends on in which order Agda chooses to chase dependencies.

• envAllowDestructiveUpdate :: Bool

  When True, allows destructively shared updating terms during evaluation or unification. This is disabled when doing speculative checking, like solve instance metas, or when updating might break abstraction, as is the case when checking abstract definitions.

• envExpandLast :: ExpandHidden

  When type-checking an alias f=e, we do not want to insert hidden arguments in the end, because these will become unsolved metas.

• envAppDef :: Maybe QName

  We are reducing an application of this function. (For debugging of incomplete matches only.)

• envSimplification :: Simplification

  Did we encounter a simplification (proper match) during the current reduction process?

• envAllowedReductions :: AllowedReductions
• envCompareBlocked :: Bool

  Can we compare blocked things during conversion? No by default. Yes for rewriting feature.

• envPrintDomainFreePi :: Bool

  When True, types will be omitted from printed pi types if they can be inferred.

• envPrintMetasBare :: Bool

  When True, throw away meta numbers and meta elims. This is used for reifying terms for feeding into the user's source code, e.g., for the interaction tactics solveAll.

• envInsideDotPattern :: Bool

  Used by the scope checker to make sure that certain forms of expressions are not used inside dot patterns: extended lambdas and let-expressions.

• envUnquoteFlags :: UnquoteFlags
• envInstanceDepth :: !Int

  Until we get a termination checker for instance search (#1743) we limit the search depth to ensure termination.

Instances

Data TCEnv

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 :: (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

MonadReader TCEnv ReduceM

Methods

ask :: ReduceM TCEnv

local :: (TCEnv -> TCEnv) -> ReduceM a -> ReduceM a

reader :: (TCEnv -> a) -> ReduceM a

MonadReader TCEnv TerM

Methods

ask :: TerM TCEnv

local :: (TCEnv -> TCEnv) -> TerM a -> TerM a

reader :: (TCEnv -> a) -> TerM a

MonadIO m => MonadReader TCEnv (TCMT m)

Methods

ask :: TCMT m TCEnv

local :: (TCEnv -> TCEnv) -> TCMT m a -> TCMT m a

reader :: (TCEnv -> a) -> TCMT m a

initEnv :: TCEnv

disableDestructiveUpdate :: TCM a -> TCM a

data UnquoteFlags

Constructors

UnquoteFlags

Fields

• _unquoteNormalise :: Bool

Instances

Data UnquoteFlags

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 :: (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

defaultUnquoteFlags :: UnquoteFlags

unquoteNormalise :: Lens' Bool UnquoteFlags

eUnquoteNormalise :: Lens' Bool TCEnv

e-prefixed lenses

eContext :: Lens' Context TCEnv

eLetBindings :: Lens' LetBindings TCEnv

eCurrentModule :: Lens' ModuleName TCEnv

eCurrentPath :: Lens' (Maybe AbsolutePath) TCEnv

eAnonymousModules :: Lens' [(ModuleName, Nat)] TCEnv

eImportPath :: Lens' [TopLevelModuleName] TCEnv

eMutualBlock :: Lens' (Maybe MutualId) TCEnv

eTerminationCheck :: Lens' (TerminationCheck ()) TCEnv

eSolvingConstraints :: Lens' Bool TCEnv

eCheckingWhere :: Lens' Bool TCEnv

eAssignMetas :: Lens' Bool TCEnv

eActiveProblems :: Lens' (Set ProblemId) TCEnv

eAbstractMode :: Lens' AbstractMode TCEnv

eRelevance :: Lens' Relevance TCEnv

eDisplayFormsEnabled :: Lens' Bool TCEnv

eRange :: Lens' Range TCEnv

eHighlightingRange :: Lens' Range TCEnv

eCall :: Lens' (Maybe (Closure Call)) TCEnv

eHighlightingLevel :: Lens' HighlightingLevel TCEnv

eHighlightingMethod :: Lens' HighlightingMethod TCEnv

eModuleNestingLevel :: Lens' Int TCEnv

eAllowDestructiveUpdate :: Lens' Bool TCEnv

eExpandLast :: Lens' ExpandHidden TCEnv

eAppDef :: Lens' (Maybe QName) TCEnv

eSimplification :: Lens' Simplification TCEnv

eAllowedReductions :: Lens' AllowedReductions TCEnv

eCompareBlocked :: Lens' Bool TCEnv

ePrintDomainFreePi :: Lens' Bool TCEnv

eInsideDotPattern :: Lens' Bool TCEnv

eUnquoteFlags :: Lens' UnquoteFlags TCEnv

eInstanceDepth :: Lens' Int TCEnv

Context

type Context = [ContextEntry]

The Context is a stack of ContextEntrys.

data ContextEntry

Constructors

Ctx

Fields

• ctxId :: CtxId
• ctxEntry :: Dom (Name, Type)

Instances

Data ContextEntry

Methods

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

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

toConstr :: ContextEntry -> Constr

dataTypeOf :: ContextEntry -> DataType

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

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

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

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

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

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

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

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

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

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

PrettyTCM Context

Methods

prettyTCM :: Context -> TCM Doc

newtype CtxId

Constructors

CtxId Nat

Instances

Enum CtxId

Methods

succ :: CtxId -> CtxId

pred :: CtxId -> CtxId

toEnum :: Int -> CtxId

fromEnum :: CtxId -> Int

enumFrom :: CtxId -> [CtxId]

enumFromThen :: CtxId -> CtxId -> [CtxId]

enumFromTo :: CtxId -> CtxId -> [CtxId]

enumFromThenTo :: CtxId -> CtxId -> CtxId -> [CtxId]

Eq CtxId

Methods

(==) :: CtxId -> CtxId -> Bool

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

Integral CtxId

Methods

quot :: CtxId -> CtxId -> CtxId

rem :: CtxId -> CtxId -> CtxId

div :: CtxId -> CtxId -> CtxId

mod :: CtxId -> CtxId -> CtxId

quotRem :: CtxId -> CtxId -> (CtxId, CtxId)

divMod :: CtxId -> CtxId -> (CtxId, CtxId)

toInteger :: CtxId -> Integer

Data CtxId

Methods

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

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

toConstr :: CtxId -> Constr

dataTypeOf :: CtxId -> DataType

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

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

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

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

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

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

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

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

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

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

Num CtxId

Methods

(+) :: CtxId -> CtxId -> CtxId

(-) :: CtxId -> CtxId -> CtxId

(*) :: CtxId -> CtxId -> CtxId

negate :: CtxId -> CtxId

abs :: CtxId -> CtxId

signum :: CtxId -> CtxId

fromInteger :: Integer -> CtxId

Ord CtxId

Methods

compare :: CtxId -> CtxId -> Ordering

(<) :: CtxId -> CtxId -> Bool

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

(>) :: CtxId -> CtxId -> Bool

(>=) :: CtxId -> CtxId -> Bool

max :: CtxId -> CtxId -> CtxId

min :: CtxId -> CtxId -> CtxId

Real CtxId

Methods

toRational :: CtxId -> Rational

Show CtxId

Methods

showsPrec :: Int -> CtxId -> ShowS

show :: CtxId -> String

showList :: [CtxId] -> ShowS

KillRange CtxId

Methods

killRange :: KillRangeT CtxId

HasFresh CtxId

Methods

freshLens :: Lens' CtxId TCState

nextFresh' :: CtxId -> CtxId

PrettyTCM CtxId

Methods

prettyTCM :: CtxId -> TCM Doc

Let bindings

type LetBindings = Map Name (Open (Term, Dom Type))

Abstract mode

data AbstractMode

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

Eq AbstractMode

Methods

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

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

Data AbstractMode

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 :: (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

Methods

showsPrec :: Int -> AbstractMode -> ShowS

show :: AbstractMode -> String

showList :: [AbstractMode] -> ShowS

aDefToMode :: IsAbstract -> AbstractMode

aModeToDef :: AbstractMode -> IsAbstract

Insertion of implicit arguments

data ExpandHidden

Constructors

ExpandLast

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

DontExpandLast

Do not append implicit arguments.

Instances

Eq ExpandHidden

Methods

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

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

Data ExpandHidden

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 :: (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 ExplicitToInstance

Constructors

ExplicitToInstance

Explicit arguments are considered as instance arguments

ExplicitStayExplicit

Instances

Eq ExplicitToInstance

Methods

(==) :: ExplicitToInstance -> ExplicitToInstance -> Bool

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

Data ExplicitToInstance

Methods

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

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

toConstr :: ExplicitToInstance -> Constr

dataTypeOf :: ExplicitToInstance -> DataType

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

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

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

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

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

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

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

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

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

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

Show ExplicitToInstance

Methods

showsPrec :: Int -> ExplicitToInstance -> ShowS

show :: ExplicitToInstance -> String

showList :: [ExplicitToInstance] -> ShowS

data Candidate

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.

Constructors

Candidate

Fields

• candidateTerm :: Term
• candidateType :: Type
• candidateEti :: ExplicitToInstance
• candidateOverlappable :: Bool

Instances

Data Candidate

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 :: (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

Methods

showsPrec :: Int -> Candidate -> ShowS

show :: Candidate -> String

showList :: [Candidate] -> ShowS

Free Candidate

Methods

freeVars' :: IsVarSet c => Candidate -> FreeM c

InstantiateFull Candidate

Methods

instantiateFull' :: Candidate -> ReduceM Candidate

Normalise Candidate

Methods

normalise' :: Candidate -> ReduceM Candidate

Simplify Candidate

Methods

simplify' :: Candidate -> ReduceM Candidate

Reduce Candidate

Methods

reduce' :: Candidate -> ReduceM Candidate

reduceB' :: Candidate -> ReduceM (Blocked Candidate)

Instantiate Candidate

Methods

instantiate' :: Candidate -> ReduceM Candidate

Type checking warnings (aka non-fatal errors)

data Warning

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 [[NamedArg DeBruijnPattern]]

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

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

CoverageNoExactSplit QName [Clause]

NotStrictlyPositive QName 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

OldBuiltin String String

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

EmptyRewritePragma

If the user wrote just {--}.

UselessPublic

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

UselessInline QName

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]

SafeFlagNonTerminating

SafeFlagTerminating

SafeFlagPrimTrustMe

SafeFlagNoPositivityCheck

SafeFlagPolarity

ParseWarning ParseWarning

DeprecationWarning String String String

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

Instances

Data Warning

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 :: (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

Methods

showsPrec :: Int -> Warning -> ShowS

show :: Warning -> String

showList :: [Warning] -> ShowS

data TCWarning

Constructors

TCWarning

Fields

• tcWarningRange :: Range

  Range where the warning was raised

• tcWarning :: Warning

  The warning itself

• tcWarningPrintedWarning :: Doc

  The warning printed in the state and environment where it was raised

Instances

Eq TCWarning

Methods

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

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

Show TCWarning

Methods

showsPrec :: Int -> TCWarning -> ShowS

show :: TCWarning -> String

showList :: [TCWarning] -> ShowS

HasRange TCWarning

Methods

getRange :: TCWarning -> Range

tcWarningOrigin :: TCWarning -> SrcFile

equalHeadConstructors :: Warning -> Warning -> Bool

getPartialDefs :: ReadTCState tcm => tcm [QName]

Type checking errors

data CallInfo

Information about a call.

Constructors

CallInfo

Fields

• callInfoTarget :: QName

  Target function name.

• callInfoRange :: Range

  Range of the target function.

• callInfoCall :: Closure Term

  To be formatted representation of the call.

Instances

Data CallInfo

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 :: (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

Methods

showsPrec :: Int -> CallInfo -> ShowS

show :: CallInfo -> String

showList :: [CallInfo] -> ShowS

Pretty CallInfo

We only show the name of the callee.

Methods

pretty :: CallInfo -> Doc

prettyPrec :: Int -> CallInfo -> Doc

prettyList :: [CallInfo] -> Doc

AllNames CallInfo

Methods

allNames :: CallInfo -> Seq QName

data TerminationError

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

Constructors

TerminationError

Fields

• termErrFunctions :: [QName]

  The functions which failed to check. (May not include automatically generated functions.)

• termErrCalls :: [CallInfo]

  The problematic call sites.

Instances

Data TerminationError

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 :: (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

Methods

showsPrec :: Int -> TerminationError -> ShowS

show :: TerminationError -> String

showList :: [TerminationError] -> ShowS

data SplitError

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.

CoinductiveDatatype (Closure Type)

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

UnificationStuck

Fields

• cantSplitConName :: QName

  Constructor.

• cantSplitTel :: Telescope

  Context for indices.

• cantSplitConIdx :: Args

  Inferred indices (from type of constructor).

• cantSplitGivenIdx :: Args

  Expected indices (from checking pattern).

• cantSplitFailures :: [UnificationFailure]

  Reason(s) why unification got stuck.

GenericSplitError String

Instances

Show SplitError

Methods

showsPrec :: Int -> SplitError -> ShowS

show :: SplitError -> String

showList :: [SplitError] -> ShowS

data NegativeUnification

Constructors

UnifyConflict Telescope Term Term

UnifyCycle Telescope Int Term

Instances

Show NegativeUnification

Methods

showsPrec :: Int -> NegativeUnification -> ShowS

show :: NegativeUnification -> String

showList :: [NegativeUnification] -> ShowS

data UnificationFailure

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

Instances

Show UnificationFailure

Methods

showsPrec :: Int -> UnificationFailure -> ShowS

show :: UnificationFailure -> String

showList :: [UnificationFailure] -> ShowS

data UnquoteError

Constructors

BadVisibility String (Arg Term)

ConInsteadOfDef QName String String

DefInsteadOfCon QName String String

NonCanonical String Term

BlockedOnMeta TCState MetaId

UnquotePanic String

Instances

Show UnquoteError

Methods

showsPrec :: Int -> UnquoteError -> ShowS

show :: UnquoteError -> String

showList :: [UnquoteError] -> ShowS

data TypeError

Constructors

InternalError String

NotImplemented String

NotSupported String

CompilationError String

TerminationCheckFailed [TerminationError]

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

DifferentArities

Varying number of arguments for a function.

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)

A function is applied to a hidden named argument it does not have.

WrongIrrelevanceInLambda

Wrong user-given relevance annotation in lambda.

WrongInstanceDeclaration

A term is declared as an instance but it’s not allowed

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

IlltypedPattern Pattern Type

IllformedProjectionPattern Pattern

CannotEliminateWithPattern (NamedArg Pattern) Type

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

ShouldBeRecordType Type

ShouldBeRecordPattern DeBruijnPattern

NotAProjectionPattern (NamedArg Pattern)

NotAProperTerm

SetOmegaNotValidType

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 Pattern (Dom Type)

DefinitionIsIrrelevant QName

VariableIsIrrelevant Name

UnequalTerms Comparison Term Term Type

UnequalTypes Comparison Type Type

UnequalRelevance Comparison Term Term

The two function types have different relevance.

UnequalHiding Term Term

The two function types have different hiding.

UnequalSorts Sort Sort

UnequalBecauseOfUniverseConflict Comparison Term Term

NotLeqSort Sort Sort

MetaCannotDependOn MetaId [Nat] Nat

The arguments are the meta variable, the parameters it can depend on and the paratemeter that it wants to depend on.

MetaOccursInItself MetaId

GenericError String

GenericDocError Doc

BuiltinMustBeConstructor String Expr

NoSuchBuiltinName String

DuplicateBuiltinBinding String Term Term

NoBindingForBuiltin String

NoSuchPrimitiveFunction String

ShadowedModule Name [ModuleName]

BuiltinInParameterisedModule String

IllegalLetInTelescope TypedBinding

NoRHSRequiresAbsurdPattern [NamedArg Pattern]

AbsurdPatternRequiresNoRHS [NamedArg Pattern]

TooFewFields QName [Name]

TooManyFields QName [Name]

DuplicateFields [Name]

DuplicateConstructors [Name]

WithOnFreeVariable Expr Term

UnexpectedWithPatterns [Pattern]

WithClausePatternMismatch Pattern (NamedArg DeBruijnPattern)

FieldOutsideRecord

ModuleArityMismatch ModuleName Telescope [NamedArg Expr]

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 [QName]

AmbiguousModule QName [ModuleName]

UninstantiatedModule QName

ClashingDefinition QName QName

ClashingModule ModuleName ModuleName

ClashingImport Name QName

ClashingModuleImport Name ModuleName

PatternShadowsConstructor Name QName

ModuleDoesntExport QName [ImportedName]

DuplicateImports QName [ImportedName]

InvalidPattern Pattern

RepeatedVariablesInPattern [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 QName

TooFewArgumentsToPatternSynonym QName

UnusedVariableInPatternSynonym

NoParseForApplication [Expr]

AmbiguousParseForApplication [Expr] [Expr]

NoParseForLHS LHSOrPatSyn Pattern

AmbiguousParseForLHS LHSOrPatSyn Pattern [Pattern]

OperatorInformation [NotationSection] TypeError

IFSNoCandidateInScope Type

UnquoteFailed UnquoteError

DeBruijnIndexOutOfScope Nat Telescope [Name]

NeedOptionCopatterns

NeedOptionRewriting

NonFatalErrors [TCWarning]

InstanceSearchDepthExhausted Term Type Int

Instances

Show TypeError

Methods

showsPrec :: Int -> TypeError -> ShowS

show :: TypeError -> String

showList :: [TypeError] -> ShowS

data LHSOrPatSyn

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

Constructors

IsLHS

IsPatSyn

Instances

Eq LHSOrPatSyn

Methods

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

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

Show LHSOrPatSyn

Methods

showsPrec :: Int -> LHSOrPatSyn -> ShowS

show :: LHSOrPatSyn -> String

showList :: [LHSOrPatSyn] -> ShowS

data TCErr

Type-checking errors.

Constructors

TypeError

Fields

• tcErrState :: TCState

  The state in which the error was raised.

• tcErrClosErr :: Closure TypeError

  The environment in which the error as raised plus the error.

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

Show TCErr

Methods

showsPrec :: Int -> TCErr -> ShowS

show :: TCErr -> String

showList :: [TCErr] -> ShowS

Exception TCErr

Methods

toException :: TCErr -> SomeException

fromException :: SomeException -> Maybe TCErr

displayException :: TCErr -> String

Error TCErr

Methods

noMsg :: TCErr

strMsg :: String -> TCErr

HasRange TCErr

Methods

getRange :: TCErr -> Range

MonadError TCErr IM

Methods

throwError :: TCErr -> IM a

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

MonadError TCErr TerM

Methods

throwError :: TCErr -> TerM a

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

MonadError TCErr (TCMT IO)

Methods

throwError :: TCErr -> TCMT IO a

catchError :: TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a

Accessing options

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

Minimal complete definition

pragmaOptions, commandLineOptions

Methods

pragmaOptions :: m PragmaOptions

Returns the pragma options which are currently in effect.

commandLineOptions :: m CommandLineOptions

Returns the command line options which are currently in effect.

Instances

HasOptions TerM

Methods

pragmaOptions :: TerM PragmaOptions

commandLineOptions :: TerM CommandLineOptions

HasOptions m => HasOptions (MaybeT m)

Methods

pragmaOptions :: MaybeT m PragmaOptions

commandLineOptions :: MaybeT m CommandLineOptions

HasOptions m => HasOptions (ListT m)

Methods

pragmaOptions :: ListT m PragmaOptions

commandLineOptions :: ListT m CommandLineOptions

MonadIO m => HasOptions (TCMT m)

Methods

pragmaOptions :: TCMT m PragmaOptions

commandLineOptions :: TCMT m CommandLineOptions

HasOptions m => HasOptions (ExceptT e m)

Methods

pragmaOptions :: ExceptT e m PragmaOptions

commandLineOptions :: ExceptT e m CommandLineOptions

HasOptions m => HasOptions (StateT s m)

Methods

pragmaOptions :: StateT s m PragmaOptions

commandLineOptions :: StateT s m CommandLineOptions

(HasOptions m, Monoid w) => HasOptions (WriterT w m)

Methods

pragmaOptions :: WriterT w m PragmaOptions

commandLineOptions :: WriterT w m CommandLineOptions

HasOptions m => HasOptions (ReaderT * r m)

Methods

pragmaOptions :: ReaderT * r m PragmaOptions

commandLineOptions :: ReaderT * r m CommandLineOptions

The reduce monad

data ReduceEnv

Environment of the reduce monad.

Constructors

ReduceEnv

Fields

• redEnv :: TCEnv

  Read only access to environment.

• redSt :: TCState

  Read only access to state (signature, metas...).

mapRedEnv :: (TCEnv -> TCEnv) -> ReduceEnv -> ReduceEnv

mapRedSt :: (TCState -> TCState) -> ReduceEnv -> ReduceEnv

mapRedEnvSt :: (TCEnv -> TCEnv) -> (TCState -> TCState) -> ReduceEnv -> ReduceEnv

newtype ReduceM a

Constructors

ReduceM

Fields

• unReduceM :: ReduceEnv -> a

Instances

Monad ReduceM

Methods

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

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

return :: a -> ReduceM a

fail :: String -> ReduceM a

Functor ReduceM

Methods

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

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

Applicative ReduceM

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

ReadTCState ReduceM

Methods

getTCState :: ReduceM TCState

MonadReader TCEnv ReduceM

Methods

ask :: ReduceM TCEnv

local :: (TCEnv -> TCEnv) -> ReduceM a -> ReduceM a

reader :: (TCEnv -> a) -> ReduceM a

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

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

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

runReduceM :: ReduceM a -> TCM a

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

Type checking monad transformer

newtype TCMT m a

Constructors

TCM

Fields

• unTCM :: IORef TCState -> TCEnv -> m a

Instances

MonadTrans TCMT

Methods

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

MonadError TCErr IM

Methods

throwError :: TCErr -> IM a

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

MonadBench Phase TCM

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

Methods

getBenchmark :: TCM (Benchmark Phase)

getsBenchmark :: (Benchmark Phase -> c) -> TCM c

putBenchmark :: Benchmark Phase -> TCM ()

modifyBenchmark :: (Benchmark Phase -> Benchmark Phase) -> TCM ()

finally :: TCM b -> TCM c -> TCM b

Conversion TOM Clause (Maybe ([Pat O], MExp O))

Methods

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

Conversion TOM Type (MExp O)

Methods

convert :: Type -> TOM (MExp O)

Conversion TOM Term (MExp O)

Methods

convert :: Term -> TOM (MExp O)

Conversion TOM Args (MM (ArgList O) (RefInfo O))

Methods

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

MonadIO m => MonadState TCState (TCMT m)

Methods

get :: TCMT m TCState

put :: TCState -> TCMT m ()

state :: (TCState -> (a, TCState)) -> TCMT m a

MonadIO m => MonadReader TCEnv (TCMT m)

Methods

ask :: TCMT m TCEnv

local :: (TCEnv -> TCEnv) -> TCMT m a -> TCMT m a

reader :: (TCEnv -> a) -> TCMT m a

MonadError TCErr (TCMT IO)

Methods

throwError :: TCErr -> TCMT IO a

catchError :: TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a

Conversion TOM [Clause] [([Pat O], MExp O)]

Methods

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

Conversion TOM (Arg Pattern) (Pat O)

Methods

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

Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b)

Methods

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

MonadIO m => Monad (TCMT m)

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

fail :: String -> TCMT m a

MonadIO m => Functor (TCMT m)

Methods

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

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

MonadIO m => Applicative (TCMT m)

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 Any)

Short-cutting disjunction forms a monoid.

Methods

(<>) :: TCM Any -> TCM Any -> TCM Any

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

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

Monoid (TCM Any)

Methods

mempty :: TCM Any

mappend :: TCM Any -> TCM Any -> TCM Any

mconcat :: [TCM Any] -> TCM Any

MonadIO m => MonadIO (TCMT m)

Methods

liftIO :: IO a -> TCMT m a

Null (TCM Doc)

Methods

empty :: TCM Doc

null :: TCM Doc -> Bool

MonadIO m => MonadTCM (TCMT m)

Methods

liftTCM :: TCM a -> TCMT m a

MonadIO m => HasOptions (TCMT m)

Methods

pragmaOptions :: TCMT m PragmaOptions

commandLineOptions :: TCMT m CommandLineOptions

MonadIO m => ReadTCState (TCMT m)

Methods

getTCState :: TCMT m TCState

MonadIO m => MonadDebug (TCMT m)

Methods

displayDebugMessage :: Int -> String -> TCMT m ()

traceDebugMessage :: Int -> String -> TCMT m a -> TCMT m a

formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> TCMT m String

MonadIO m => HasBuiltins (TCMT m)

Methods

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

HasConstInfo (TCMT IO)

Methods

getConstInfo :: QName -> TCMT IO Definition

getConstInfo' :: QName -> TCMT IO (Either SigError Definition)

getRewriteRulesFor :: QName -> TCMT IO RewriteRules

type TCM = TCMT IO

class (Applicative tcm, MonadIO tcm, MonadReader TCEnv tcm, MonadState TCState tcm, HasOptions tcm) => MonadTCM tcm where

Minimal complete definition

liftTCM

Methods

liftTCM :: TCM a -> tcm a

Instances

MonadTCM TerM

Methods

liftTCM :: TCM a -> TerM a

MonadTCM tcm => MonadTCM (MaybeT tcm)

Methods

liftTCM :: TCM a -> MaybeT tcm a

MonadTCM tcm => MonadTCM (ListT tcm)

Methods

liftTCM :: TCM a -> ListT tcm a

MonadIO m => MonadTCM (TCMT m)

Methods

liftTCM :: TCM a -> TCMT m a

MonadTCM tcm => MonadTCM (ExceptT err tcm)

Methods

liftTCM :: TCM a -> ExceptT err tcm a

(Monoid w, MonadTCM tcm) => MonadTCM (WriterT w tcm)

Methods

liftTCM :: TCM a -> WriterT w tcm a

type IM = TCMT (InputT IO)

Interaction monad.

runIM :: IM a -> TCM a

catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a

Preserve the state of the failing computation.

finally_ :: TCM a -> TCM b -> TCM a

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.

mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n a

pureTCM :: MonadIO m => (TCState -> TCEnv -> a) -> TCMT m a

returnTCMT :: MonadIO m => a -> TCMT m a

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

thenTCMT :: MonadIO m => TCMT m a -> TCMT m b -> TCMT m b

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

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

patternViolation :: TCM a

internalError :: MonadTCM tcm => String -> tcm a

genericError :: MonadTCM tcm => String -> tcm a

genericDocError :: MonadTCM tcm => Doc -> tcm a

typeError :: MonadTCM tcm => TypeError -> tcm a

typeError_ :: MonadTCM tcm => TypeError -> tcm TCErr

runTCM :: MonadIO m => TCEnv -> TCState -> TCMT m a -> m (a, TCState)

Running the type checking monad (most general form).

runTCMTop :: TCM a -> IO (Either TCErr a)

Running the type checking monad on toplevel (with initial state).

runTCMTop' :: MonadIO m => TCMT m a -> m a

runSafeTCM :: TCM a -> TCState -> IO (a, TCState)

runSafeTCM runs a safe TCM action (a TCM action which cannot fail) in the initial environment.

forkTCM :: TCM a -> TCM ()

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.

extendedLambdaName :: String

Base name for extended lambda patterns

absurdLambdaName :: String

Name of absurdLambda definitions.

isAbsurdLambdaName :: QName -> Bool

Check whether we have an definition from an absurd lambda.

KillRange instances