Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Monad.Base

Contents

Type checking state
st-prefixed lenses
Fresh things
Open things
Judgements
Highlighting levels
Type checking environment
e-prefixed lenses
Type checking warnings (aka non-fatal errors)
Type checking errors
Accessing options
The reduce monad
Type checking monad transformer
KillRange instances

Synopsis

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 `DisplayTerm`s 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, `data`s and `record`s. 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, `data`s and `record`s. 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, `data`s and `record`s. 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 #

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.

Type checking state

st-prefixed lenses

Fresh things

Managing file names

Interface

Closure

Constraints

Open things

Judgements

Meta variables

Interaction meta variables

Signature

Injectivity

Mutual blocks

Statistics

Trace

Instance table

Builtin things

Highlighting levels

Type checking environment

e-prefixed lenses

Context

Let bindings

Abstract mode

Insertion of implicit arguments

Type checking warnings (aka non-fatal errors)

Type checking errors

Accessing options

The reduce monad

Type checking monad transformer

KillRange instances