Agda.TypeChecking.Monad.Base

Type checking state

data TCState

Constructors

TCSt

Fields

• stPreScopeState :: !PreScopeState

  The state which is frozen after scope checking.

• stPostScopeState :: !PostScopeState

  The state which is modified after scope checking.

• stPersistentState :: !PersistentTCState

  State which is forever, like a diamond.

Instances

Show TCState

Methods

showsPrec :: Int -> TCState -> ShowS

show :: TCState -> String

showList :: [TCState] -> ShowS

LensPersistentVerbosity TCState

Methods

getPersistentVerbosity :: TCState -> PersistentVerbosity

setPersistentVerbosity :: PersistentVerbosity -> TCState -> TCState

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

LensIncludePaths TCState

Methods

getIncludePaths :: TCState -> [FilePath]

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

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

getAbsoluteIncludePaths :: TCState -> [AbsolutePath]

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

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

LensSafeMode TCState

Methods

getSafeMode :: TCState -> SafeMode

setSafeMode :: SafeMode -> TCState -> TCState

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

LensCommandLineOptions TCState

Methods

getCommandLineOptions :: TCState -> CommandLineOptions

setCommandLineOptions :: CommandLineOptions -> TCState -> TCState

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

LensVerbosity TCState

Methods

getVerbosity :: TCState -> Verbosity

setVerbosity :: Verbosity -> TCState -> TCState

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

LensPragmaOptions TCState

Methods

getPragmaOptions :: TCState -> PragmaOptions

setPragmaOptions :: PragmaOptions -> TCState -> TCState

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

MonadState TCState TerM

Methods

get :: TerM TCState

put :: TCState -> TerM ()

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

MonadIO m => MonadState TCState (TCMT m)

Methods

get :: TCMT m TCState

put :: TCState -> TCMT m ()

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

class Monad m => ReadTCState m where

Minimal complete definition

getTCState

Methods

getTCState :: m TCState

Instances

ReadTCState ReduceM

Methods

getTCState :: ReduceM TCState

MonadIO m => ReadTCState (TCMT m)

Methods

getTCState :: TCMT m TCState

data PreScopeState

Constructors

PreScopeState

Fields

• stPreTokens :: !CompressedFile

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

• stPreImports :: !Signature

  Imported declared identifiers. Those most not be serialized!

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

  Pattern synonyms of the current file. Serialized.

• stPrePatternSynImports :: !PatternSynDefns

  Imported pattern synonyms. Must not be serialized!

• stPrePragmaOptions :: !PragmaOptions

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

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

  Display forms added by someone else to imported identifiers

• stPreImportedInstanceDefs :: !InstanceTable
• stPreHaskellImports :: !(Set String)

  Imports that should be generated by the compiler / MAlonzo (this includes imports from imported modules).

• stPreHaskellImportsUHC :: !(Set String)

  Imports that should be generated by the compiler / UHC backend (this includes imports from imported modules).

• stPreHaskellCode :: ![String]

  Inline Haskell code that should be inserted by the GHC backend

• 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
• stPostSolvedInteractionPoints :: !InteractionPoints

  Interaction points that have been filled by a give or solve action.

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

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

stHaskellImports :: Lens' (Set String) TCState

stHaskellImportsUHC :: Lens' (Set String) TCState

stHaskellCode :: Lens' [String] TCState

stFreshInteractionId :: Lens' InteractionId TCState

stFreshNameId :: Lens' NameId TCState

stSyntaxInfo :: Lens' CompressedFile TCState

stDisambiguatedNames :: Lens' DisambiguatedNames TCState

stMetaStore :: Lens' MetaStore TCState

stInteractionPoints :: Lens' InteractionPoints TCState

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

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

HasFresh ProblemId

Methods

freshLens :: Lens' ProblemId TCState

nextFresh' :: ProblemId -> ProblemId

PrettyTCM ProblemId

Methods

prettyTCM :: ProblemId -> TCM Doc

freshName :: (MonadState TCState m, HasFresh NameId) => Range -> String -> m Name

freshNoName :: (MonadState TCState m, HasFresh NameId) => Range -> m Name

freshNoName_ :: (MonadState TCState m, HasFresh NameId) => m Name

class FreshName a where

Create a fresh name from a.

Minimal complete definition

freshName_

Methods

freshName_ :: (MonadState TCState m, HasFresh NameId) => a -> m Name

Instances

FreshName ()

Methods

freshName_ :: (MonadState TCState m, HasFresh NameId) => () -> m Name

FreshName String

Methods

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

FreshName Range

Methods

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

FreshName (Range, String)

Methods

freshName_ :: (MonadState TCState m, HasFresh NameId) => (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 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.

• iInsideScope :: ScopeInfo

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

  Andreas, AIM XX: For performance reason, this field is not serialized, so if you deserialize an interface, iInsideScope will be empty. You need to type-check the file to get iInsideScope.

• iSignature :: Signature
• iDisplayForms :: DisplayForms

  Display forms added for imported identifiers.

• iBuiltin :: BuiltinThings (String, QName)
• iHaskellImports :: Set String

  Haskell imports listed in (transitively) imported modules are not included here.

• iHaskellImportsUHC :: Set String

  Haskell imports listed in (transitively) imported modules are not included here.

• iHaskellCode :: [String]

  Inline Haskell code

• iHighlighting :: HighlightingInfo
• iPragmaOptions :: [OptionsPragma]

  Pragma options set in the file.

• iPatternSyns :: PatternSynDefns

Instances

Show Interface

Methods

showsPrec :: Int -> Interface -> ShowS

show :: Interface -> String

showList :: [Interface] -> ShowS

Pretty Interface

Methods

pretty :: Interface -> Doc

prettyPrec :: Int -> 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

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

MentionsMeta a => MentionsMeta (Closure a)

Methods

mentionsMeta :: MetaId -> Closure a -> Bool

PrettyTCM a => PrettyTCM (Closure a)

Methods

prettyTCM :: Closure a -> TCM Doc

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 :: [ProblemId]
• theConstraint :: Closure Constraint

Instances

Show ProblemConstraint

Methods

showsPrec :: Int -> ProblemConstraint -> ShowS

show :: ProblemConstraint -> String

showList :: [ProblemConstraint] -> ShowS

HasRange ProblemConstraint

Methods

getRange :: ProblemConstraint -> Range

MentionsMeta ProblemConstraint

Methods

mentionsMeta :: MetaId -> ProblemConstraint -> Bool

PrettyTCM ProblemConstraint

Methods

prettyTCM :: ProblemConstraint -> TCM Doc

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

Show Constraint

Methods

showsPrec :: Int -> Constraint -> ShowS

show :: Constraint -> String

showList :: [Constraint] -> ShowS

HasRange Constraint

Methods

getRange :: Constraint -> Range

TermLike Constraint

Methods

traverseTerm :: (Term -> Term) -> Constraint -> Constraint

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

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

MentionsMeta Constraint

Methods

mentionsMeta :: MetaId -> Constraint -> Bool

PrettyTCM Constraint

Methods

prettyTCM :: Constraint -> TCM Doc

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

Free' Constraint c

Methods

freeVars' :: Constraint -> FreeM c

data Comparison

Constructors

CmpEq

CmpLeq

Instances

Eq Comparison

Methods

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

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

Show Comparison

Methods

showsPrec :: Int -> Comparison -> ShowS

show :: Comparison -> String

showList :: [Comparison] -> ShowS

Pretty Comparison

Methods

pretty :: Comparison -> Doc

prettyPrec :: Int -> 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

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

Decoration Open

Methods

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

distributeF :: Functor m => Open (m 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)

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

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.

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

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

Signature

data Signature

Constructors

Sig

Fields

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

  The rewrite rules defined in this file.

Instances

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]

data Section

Constructors

Section

Fields

• _secTelescope :: Telescope

Instances

Show Section

Methods

showsPrec :: Int -> Section -> ShowS

show :: Section -> String

showList :: [Section] -> ShowS

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

Show DisplayForm

Methods

showsPrec :: Int -> DisplayForm -> ShowS

show :: DisplayForm -> String

showList :: [DisplayForm] -> ShowS

KillRange DisplayForm

Methods

killRange :: KillRangeT DisplayForm

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

Free' DisplayForm c

Methods

freeVars' :: DisplayForm -> FreeM c

type LocalDisplayForm = Local DisplayForm

data DisplayTerm

A structured presentation of a Term for reification into Syntax.

Constructors

DWithApp DisplayTerm [DisplayTerm] Elims

(f vs | ws) es. The first DisplayTerm is the parent function f with its args vs. The list of DisplayTerms are the with expressions ws. The Elims are additional arguments es (possible in case the with-application is of function type) or projections (if it is of record type).

DCon ConHead ConInfo [Arg DisplayTerm]

c vs.

DDef QName [Elim' DisplayTerm]

d vs.

DDot Term

.v.

DTerm Term

v.

Instances

Show DisplayTerm

Methods

showsPrec :: Int -> DisplayTerm -> ShowS

show :: DisplayTerm -> String

showList :: [DisplayTerm] -> ShowS

KillRange DisplayTerm

Methods

killRange :: KillRangeT DisplayTerm

NamesIn DisplayTerm

Methods

namesIn :: DisplayTerm -> Set QName

PrettyTCM DisplayTerm

Methods

prettyTCM :: DisplayTerm -> TCM Doc

InstantiateFull DisplayTerm

Methods

instantiateFull' :: DisplayTerm -> ReduceM DisplayTerm

Free' DisplayTerm c

Methods

freeVars' :: DisplayTerm -> FreeM c

Reify DisplayTerm Expr

Methods

reify :: DisplayTerm -> TCM Expr

reifyWhen :: Bool -> DisplayTerm -> TCM Expr

PrettyTCM (Elim' DisplayTerm)

Methods

prettyTCM :: Elim' DisplayTerm -> TCM Doc

defaultDisplayForm :: QName -> [LocalDisplayForm]

By default, we have no display form.

defRelevance :: Definition -> Relevance

data NLPat

Non-linear (non-constructor) first-order pattern.

Constructors

PVar (Maybe CtxId) !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

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

RaiseNLP NLPat

Methods

raiseNLPFrom :: Int -> Int -> NLPat -> NLPat

raiseNLP :: Int -> NLPat -> NLPat

GetMatchables NLPat

Methods

getMatchables :: NLPat -> [QName]

KillCtxId NLPat

Methods

killCtxId :: NLPat -> NLPat

NLPatVars NLPat

Methods

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

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

RaiseNLP NLPType

Methods

raiseNLPFrom :: Int -> Int -> NLPType -> NLPType

raiseNLP :: Int -> NLPType -> NLPType

KillCtxId NLPType

Methods

killCtxId :: NLPType -> NLPType

NLPatVars NLPType

Methods

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

  Γ ⊢ ps : t.

• rewRHS :: Term

  Γ ⊢ rhs : t.

• rewType :: Type

  Γ ⊢ t.

Instances

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]

KillCtxId RewriteRule

Methods

killCtxId :: RewriteRule -> RewriteRule

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?

• theDef :: Defn

Instances

Show Definition

Methods

showsPrec :: Int -> Definition -> ShowS

show :: Definition -> String

showList :: [Definition] -> ShowS

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.

type HaskellCode = String

type HaskellType = String

type EpicCode = String

type JSCode = String

data HaskellRepresentation

Constructors

HsDefn HaskellType HaskellCode

HsType HaskellType

Instances

Show HaskellRepresentation

Methods

showsPrec :: Int -> HaskellRepresentation -> ShowS

show :: HaskellRepresentation -> String

showList :: [HaskellRepresentation] -> ShowS

data HaskellExport

Constructors

HsExport HaskellType String

Instances

Show HaskellExport

Methods

showsPrec :: Int -> HaskellExport -> ShowS

show :: HaskellExport -> String

showList :: [HaskellExport] -> ShowS

data CoreRepresentation

Constructors

CrDefn CoreExpr

Core code for functions.

CrType CoreType

Core type for agda type.

CrConstr CoreConstr

Core constructor for agda constructor.

Instances

Show CoreRepresentation

Methods

showsPrec :: Int -> CoreRepresentation -> ShowS

show :: CoreRepresentation -> String

showList :: [CoreRepresentation] -> ShowS

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

Show Polarity

Methods

showsPrec :: Int -> Polarity -> ShowS

show :: Polarity -> String

showList :: [Polarity] -> ShowS

KillRange Polarity

Methods

killRange :: KillRangeT Polarity

PrettyTCM Polarity

Methods

prettyTCM :: Polarity -> TCM Doc

data CompiledRepresentation

Constructors

CompiledRep

Fields

• compiledHaskell :: Maybe HaskellRepresentation
• exportHaskell :: Maybe HaskellExport
• compiledEpic :: Maybe EpicCode
• compiledJS :: Maybe JSCode
• compiledCore :: Maybe CoreRepresentation

Instances

Show CompiledRepresentation

Methods

showsPrec :: Int -> CompiledRepresentation -> ShowS

show :: CompiledRepresentation -> String

showList :: [CompiledRepresentation] -> ShowS

KillRange CompiledRepresentation

Methods

killRange :: KillRangeT CompiledRepresentation

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

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

  False if only projection-like, True if record projection.

• projOrig :: QName

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

• projFromType :: Arg QName

  Type projected from. Record type if projProper = Just{}. Also stores ArgInfo of the principal argument.

• 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

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

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

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

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

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

  Mutually recursive functions, datas and records. Does not include this function.

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

  Mutually recursive functions, datas and records. Does not include this data type.

• dataAbstr :: IsAbstract

Record

Fields

• recPars :: Nat

  Number of parameters.

• recClause :: Maybe Clause
• recConHead :: ConHead

  Constructor name and fields.

• recNamedCon :: Bool
• recFields :: [Arg QName]
• recTel :: Telescope

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

• recMutual :: [QName]

  Mutually recursive functions, datas and records. Does not include this record.

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

• recRecursive :: Bool

  Recursive record. Infers recEtaEquality = False. Projections are not size-preserving.

• recAbstr :: IsAbstract

Constructor

Fields

• conPars :: Nat

  Number of 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

Show Defn

Methods

showsPrec :: Int -> Defn -> ShowS

show :: Defn -> String

showList :: [Defn] -> ShowS

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

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

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

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

Functions which are not projections may be reduced.

LevelReductions

Reduce Level terms.

NonTerminatingReductions

Functions that have not passed 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

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

defJSDef :: Definition -> Maybe JSCode

defEpicDef :: Definition -> Maybe EpicCode

defCoreDef :: Definition -> Maybe CoreRepresentation

defDelayed :: Definition -> Delayed

Are the clauses of this definition delayed?

defNonterminating :: Definition -> Bool

Has the definition failed the termination checker?

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

DropArgs FunctionInverse

Methods

dropArgs :: Int -> FunctionInverse -> FunctionInverse

InstantiateFull FunctionInverse

Methods

instantiateFull' :: FunctionInverse -> ReduceM FunctionInverse

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

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

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

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

Pretty Call

Methods

pretty :: Call -> Doc

prettyPrec :: Int -> 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

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

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

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

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

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

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' [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

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

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

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 ExplicitToInstance

Constructors

ExplicitToInstance

Explicit arguments are considered as instance arguments

ExplicitStayExplicit

Instances

Eq ExplicitToInstance

Methods

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

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

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

Show Candidate

Methods

showsPrec :: Int -> Candidate -> ShowS

show :: Candidate -> String

showList :: [Candidate] -> ShowS

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

Free' Candidate c

Methods

freeVars' :: Candidate -> FreeM c

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

TerminationIssue [TerminationError]

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 {--}.

ParseWarning ParseWarning

Instances

Show Warning

Methods

showsPrec :: Int -> Warning -> ShowS

show :: Warning -> String

showList :: [Warning] -> ShowS

data TCWarning

Constructors

TCWarning

Fields

• tcWarningState :: TCState

  The state in which the warning was raised.

• tcWarningClosure :: Closure Warning

  The warning and the environment in which it was raised.

Instances

Show TCWarning

Methods

showsPrec :: Int -> TCWarning -> ShowS

show :: TCWarning -> String

showList :: [TCWarning] -> ShowS

tcWarning :: TCWarning -> Warning

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

Show CallInfo

We only show the name of the callee.

Methods

showsPrec :: Int -> CallInfo -> ShowS

show :: CallInfo -> String

showList :: [CallInfo] -> ShowS

Pretty CallInfo

Methods

pretty :: CallInfo -> Doc

prettyPrec :: Int -> 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

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

CantSplit

Fields

• cantSplitConName :: QName

  Constructor.

• cantSplitTel :: Telescope

  Context for indices.

• cantSplitConIdx :: Args

  Inferred indices (from type of constructor).

• cantSplitGivenIdx :: Args

  Expected indices (from checking pattern).

GenericSplitError String

Instances

Show SplitError

Methods

showsPrec :: Int -> SplitError -> ShowS

show :: SplitError -> String

showList :: [SplitError] -> ShowS

Error SplitError

Methods

noMsg :: SplitError

strMsg :: String -> SplitError

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

Error UnquoteError

Methods

noMsg :: UnquoteError

strMsg :: String -> UnquoteError

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

IndicesNotConstructorApplications [Arg Term]

Indices.

IndexVariablesNotDistinct [Nat] [Arg Term]

Variables, indices.

IndicesFreeInParameters [Nat] [Arg Term] [Arg Term]

Indices (variables), index expressions (with constructors applied to reconstructed parameters), parameters.

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 Type

Expected a relevant function and found an irrelevant 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.

NotInductive Term

The term does not correspond to an inductive data type.

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

HeterogeneousEquality Term Type Term Type

We ended up with an equality constraint where the terms have different types. This is not supported.

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 Pattern

FieldOutsideRecord

ModuleArityMismatch ModuleName Telescope [NamedArg Expr]

IncompletePatternMatching Term [Elim]

CoverageFailure QName [[NamedArg DeBruijnPattern]]

UnreachableClauses QName [[NamedArg DeBruijnPattern]]

CoverageCantSplitOn QName Telescope Args Args

CoverageCantSplitIrrelevantType Type

CoverageCantSplitType Type

CoverageNoExactSplit QName Clause

WithoutKError Type Term Term

UnifyConflict ConHead ConHead

UnifyCycle Int Term

UnifyIndicesNotVars Type Term Term Args

UnificationRecursiveEq Type Int Term

UnificationStuck Telescope [Term] [Term]

SplitError SplitError

TooManyPolarities QName Integer

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

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

OperatorChangeMessage TypeError

IFSNoCandidateInScope Type

UnquoteFailed UnquoteError

DeBruijnIndexOutOfScope Nat Telescope [Name]

SafeFlagPostulate Name

SafeFlagPragma [String]

SafeFlagNonTerminating

SafeFlagTerminating

SafeFlagPrimTrustMe

SafeFlagNoPositivityCheck

SafeFlagPolarity

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 Range IOException

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

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

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

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

ReadTCState ReduceM

Methods

getTCState :: ReduceM TCState

HasOptions NLM

Methods

pragmaOptions :: NLM PragmaOptions

commandLineOptions :: NLM CommandLineOptions

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

MonadError TCErr (TCMT IO)

Methods

throwError :: TCErr -> TCMT IO a

catchError :: TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO 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

MonadIO m => MonadState TCState (TCMT m)

Methods

get :: TCMT m TCState

put :: TCState -> TCMT m ()

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

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

(*>) :: 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 => ReadTCState (TCMT m)

Methods

getTCState :: TCMT m TCState

MonadIO m => HasOptions (TCMT m)

Methods

pragmaOptions :: TCMT m PragmaOptions

commandLineOptions :: TCMT m CommandLineOptions

MonadIO m => HasBuiltins (TCMT m)

Methods

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

HasConstInfo (TCMT IO)

Methods

getConstInfo :: QName -> TCMT IO Definition

getRewriteRulesFor :: QName -> TCMT IO RewriteRules

type TCM = TCMT IO

class (Applicative tcm, MonadIO tcm, MonadReader TCEnv tcm, MonadState TCState 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 m => MonadTCM (CompileT m)

Methods

liftTCM :: TCM a -> CompileT 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

(Error err, MonadTCM tcm) => MonadTCM (ExceptionT err tcm)

Methods

liftTCM :: TCM a -> ExceptionT err tcm a

runPM :: PM a -> TCM a

Parse monad

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

warning_ :: MonadTCM tcm => Warning -> tcm TCWarning

warning :: MonadTCM tcm => Warning -> tcm ()

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

Running the type checking monad (most general form).

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

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

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

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

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

forkTCM :: TCM a -> TCM ()

Runs the given computation in a separate thread, with a copy of the current state and environment.

Note that Agda sometimes uses actual, mutable state. If the computation given to forkTCM tries to modify this state, then bad things can happen, because accesses are not mutually exclusive. The forkTCM function has been added mainly to allow the thread to read (a snapshot of) the current state in a convenient way.

Note also that exceptions which are raised in the thread are not propagated to the parent, so the thread should not do anything important.

extendedLambdaName :: String

Base name for extended lambda patterns

absurdLambdaName :: String

Name of absurdLambda definitions.

isAbsurdLambdaName :: QName -> Bool

Check whether we have an definition from an absurd lambda.

KillRange instances