Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.TypeChecking.Monad.Base

Contents

- Type checking state
  - Interface
  - Closure
  - Constraints
- Open things
- Judgements
  - Meta variables
  - Interaction meta variables
  - Signature
  - Injectivity
  - Mutual blocks
  - Statistics
  - Trace
  - Builtin things
- Highlighting levels
- Type checking environment
  - Context
  - Let bindings
  - Abstract mode
  - Insertion of implicit arguments
- Type checking errors
- Type checking monad transformer

Synopsis

- data TCState = TCSt {
  - stFreshThings :: FreshThings
  - stSyntaxInfo :: CompressedFile
  - stTokens :: CompressedFile
  - stTermErrs :: Seq TerminationError
  - stMetaStore :: MetaStore
  - stInteractionPoints :: InteractionPoints
  - stAwakeConstraints :: Constraints
  - stSleepingConstraints :: Constraints
  - stDirty :: Bool
  - stOccursCheckDefs :: Set QName
  - stSignature :: Signature
  - stImports :: Signature
  - stImportedModules :: Set ModuleName
  - stModuleToSource :: ModuleToSource
  - stVisitedModules :: VisitedModules
  - stCurrentModule :: Maybe ModuleName
  - stScope :: ScopeInfo
  - stPatternSyns :: PatternSynDefns
  - stPatternSynImports :: PatternSynDefns
  - stPragmaOptions :: PragmaOptions
  - stStatistics :: Statistics
  - stExtLambdaTele :: Map QName (Int, Int)
  - stMutualBlocks :: Map MutualId (Set QName)
  - stLocalBuiltins :: BuiltinThings PrimFun
  - stImportedBuiltins :: BuiltinThings PrimFun
  - stHaskellImports :: Set String
  - stPersistent :: PersistentTCState
  - stInteractionOutputCallback :: InteractionOutputCallback
  }
- data PersistentTCState = PersistentTCSt {
  - stDecodedModules :: DecodedModules
  - stPersistentOptions :: CommandLineOptions
  }
- data FreshThings = Fresh {
  - fMeta :: MetaId
  - fInteraction :: InteractionId
  - fMutual :: MutualId
  - fName :: NameId
  - fCtx :: CtxId
  - fProblem :: ProblemId
  - fInt :: Int
  }
- initState :: TCState
- stBuiltinThings :: TCState -> BuiltinThings PrimFun
- newtype ProblemId = ProblemId Nat
- data ModuleInfo = ModuleInfo {
  - miInterface :: Interface
  - miWarnings :: Bool
  - miTimeStamp :: ClockTime
  }
- type VisitedModules = Map TopLevelModuleName ModuleInfo
- type DecodedModules = Map TopLevelModuleName (Interface, ClockTime)
- data Interface = Interface {
  - iImportedModules :: [ModuleName]
  - iModuleName :: ModuleName
  - iScope :: Map ModuleName Scope
  - iInsideScope :: ScopeInfo
  - iSignature :: Signature
  - iBuiltin :: BuiltinThings (String, QName)
  - iHaskellImports :: Set String
  - iHighlighting :: HighlightingInfo
  - iPragmaOptions :: [OptionsPragma]
  - iPatternSyns :: PatternSynDefns
  }
- data Closure a = Closure {
  - clSignature :: Signature
  - clEnv :: TCEnv
  - clScope :: ScopeInfo
  - clValue :: a
  }
- buildClosure :: a -> TCM (Closure a)
- type Constraints = [ProblemConstraint]
- data ProblemConstraint = PConstr {
  - constraintProblem :: ProblemId
  - theConstraint :: Closure Constraint
  }
- data Constraint
  - = ValueCmp Comparison Type Term Term
  - | ElimCmp [Polarity] Type Term [Elim] [Elim]
  - | TypeCmp Comparison Type Type
  - | TelCmp Type Type Comparison Telescope Telescope
  - | SortCmp Comparison Sort Sort
  - | LevelCmp Comparison Level Level
  - | UnBlock MetaId
  - | Guarded Constraint ProblemId
  - | IsEmpty Range Type
  - | FindInScope MetaId [(Term, Type)]
- data Comparison
  - = CmpEq
  - | CmpLeq
- data Open a = OpenThing [CtxId] a
- data Judgement t a
  - = HasType {
    - jMetaId :: a
    - jMetaType :: t
    }
  - | IsSort {
    - jMetaId :: a
    - jMetaType :: t
    }
- data MetaVariable = MetaVar {
  - mvInfo :: MetaInfo
  - mvPriority :: MetaPriority
  - mvPermutation :: Permutation
  - mvJudgement :: Judgement Type MetaId
  - mvInstantiation :: MetaInstantiation
  - mvListeners :: Set Listener
  - mvFrozen :: Frozen
  }
- data Listener
  - = EtaExpand MetaId
  - | CheckConstraint Nat ProblemConstraint
- data Frozen
  - = Frozen
  - | Instantiable
- data MetaInstantiation
  - = InstV Term
  - | InstS Term
  - | Open
  - | OpenIFS
  - | BlockedConst Term
  - | PostponedTypeCheckingProblem (Closure (Expr, Type, TCM Bool))
- newtype MetaPriority = MetaPriority Int
- data RunMetaOccursCheck
  - = RunMetaOccursCheck
  - | DontRunMetaOccursCheck
- data MetaInfo = MetaInfo {
  - miClosRange :: Closure Range
  - miMetaOccursCheck :: RunMetaOccursCheck
  - miNameSuggestion :: MetaNameSuggestion
  }
- type MetaNameSuggestion = String
- data NamedMeta = NamedMeta {
  - nmSuggestion :: MetaNameSuggestion
  - nmid :: MetaId
  }
- 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
- type InteractionPoints = Map InteractionId MetaId
- newtype InteractionId = InteractionId Nat
- data Signature = Sig {
  - sigSections :: Sections
  - sigDefinitions :: Definitions
  }
- type Sections = Map ModuleName Section
- type Definitions = HashMap QName Definition
- data Section = Section {
  - secTelescope :: Telescope
  - secFreeVars :: Nat
  }
- emptySignature :: Signature
- data DisplayForm = Display Nat [Term] DisplayTerm
- data DisplayTerm
  - = DWithApp [DisplayTerm] Args
  - | DCon QName [Arg DisplayTerm]
  - | DDef QName [Arg DisplayTerm]
  - | DDot Term
  - | DTerm Term
- defaultDisplayForm :: QName -> [Open DisplayForm]
- data Definition = Defn {
  - defRelevance :: Relevance
  - defName :: QName
  - defType :: Type
  - defPolarity :: [Polarity]
  - defArgOccurrences :: [Occurrence]
  - defDisplay :: [Open DisplayForm]
  - defMutual :: MutualId
  - defCompiledRep :: CompiledRepresentation
  - theDef :: Defn
  }
- type HaskellCode = String
- type HaskellType = String
- type EpicCode = String
- type JSCode = Exp
- data HaskellRepresentation
  - = HsDefn HaskellType HaskellCode
  - | HsType HaskellType
- data Polarity
  - = Covariant
  - | Contravariant
  - | Invariant
  - | Nonvariant
- data CompiledRepresentation = CompiledRep {
  - compiledHaskell :: Maybe HaskellRepresentation
  - compiledEpic :: Maybe EpicCode
  - compiledJS :: Maybe JSCode
  }
- noCompiledRep :: CompiledRepresentation
- data Occurrence
  - = Mixed
  - | JustNeg
  - | JustPos
  - | StrictPos
  - | GuardPos
  - | Unused
- data Defn
  - = Axiom
  - | Function {
    - funClauses :: [Clause]
    - funCompiled :: CompiledClauses
    - funInv :: FunctionInverse
    - funMutual :: [QName]
    - funAbstr :: IsAbstract
    - funDelayed :: Delayed
    - funProjection :: Maybe (QName, Int)
    - funStatic :: Bool
    - funCopy :: Bool
    - funTerminates :: Maybe Bool
    }
  - | Datatype {
    - dataPars :: Nat
    - dataIxs :: Nat
    - dataInduction :: Induction
    - dataClause :: Maybe Clause
    - dataCons :: [QName]
    - dataSort :: Sort
    - dataMutual :: [QName]
    - dataAbstr :: IsAbstract
    }
  - | Record {
    - recPars :: Nat
    - recClause :: Maybe Clause
    - recCon :: QName
    - recNamedCon :: Bool
    - recConType :: Type
    - recFields :: [Arg QName]
    - recTel :: Telescope
    - recMutual :: [QName]
    - recEtaEquality :: Bool
    - recInduction :: Induction
    - recRecursive :: Bool
    - recAbstr :: IsAbstract
    }
  - | Constructor {
    - conPars :: Nat
    - conSrcCon :: QName
    - conData :: QName
    - conAbstr :: IsAbstract
    - conInd :: Induction
    }
  - | Primitive {
    - primAbstr :: IsAbstract
    - primName :: String
    - primClauses :: Maybe [Clause]
    - primCompiled :: Maybe CompiledClauses
    }
- defIsRecord :: Defn -> Bool
- defIsDataOrRecord :: Defn -> Bool
- newtype Fields = Fields [(Name, Type)]
- data Reduced no yes
  - = NoReduction no
  - | YesReduction yes
- data IsReduced
  - = NotReduced
  - | Reduced (Blocked ())
- data MaybeReduced a = MaybeRed {
  - isReduced :: IsReduced
  - ignoreReduced :: a
  }
- type MaybeReducedArgs = [MaybeReduced (Arg Term)]
- notReduced :: a -> MaybeReduced a
- reduced :: Blocked (Arg Term) -> MaybeReduced (Arg Term)
- data PrimFun = PrimFun {
  - primFunName :: QName
  - primFunArity :: Arity
  - primFunImplementation :: [Arg Term] -> TCM (Reduced MaybeReducedArgs Term)
  }
- defClauses :: Definition -> [Clause]
- defCompiled :: Definition -> Maybe CompiledClauses
- defJSDef :: Definition -> Maybe JSCode
- defEpicDef :: Definition -> Maybe EpicCode
- defDelayed :: Definition -> Delayed
- defCopy :: Definition -> Bool
- defAbstract :: Definition -> IsAbstract
- type FunctionInverse = FunctionInverse' Clause
- data FunctionInverse' c
  - = NotInjective
  - | Inverse (Map TermHead c)
- data TermHead
  - = SortHead
  - | PiHead
  - | ConHead QName
- newtype MutualId = MutId Int32
- type Statistics = Map String Integer
- data Call
  - = CheckClause Type Clause (Maybe Clause)
  - | forall a . CheckPattern Pattern Telescope Type (Maybe a)
  - | CheckLetBinding LetBinding (Maybe ())
  - | InferExpr Expr (Maybe (Term, Type))
  - | CheckExpr Expr Type (Maybe Term)
  - | CheckDotPattern Expr Term (Maybe Constraints)
  - | CheckPatternShadowing Clause (Maybe ())
  - | IsTypeCall Expr Sort (Maybe Type)
  - | IsType_ Expr (Maybe Type)
  - | InferVar Name (Maybe (Term, Type))
  - | InferDef Range QName (Maybe (Term, Type))
  - | CheckArguments Range [NamedArg Expr] Type Type (Maybe (Args, Type))
  - | CheckDataDef Range Name [LamBinding] [Constructor] (Maybe ())
  - | CheckRecDef Range Name [LamBinding] [Constructor] (Maybe ())
  - | CheckConstructor QName Telescope Sort Constructor (Maybe ())
  - | CheckFunDef Range Name [Clause] (Maybe ())
  - | CheckPragma Range Pragma (Maybe ())
  - | CheckPrimitive Range Name Expr (Maybe ())
  - | CheckIsEmpty Range Type (Maybe ())
  - | CheckWithFunctionType Expr (Maybe ())
  - | CheckSectionApplication Range ModuleName ModuleApplication (Maybe ())
  - | ScopeCheckExpr Expr (Maybe Expr)
  - | ScopeCheckDeclaration NiceDeclaration (Maybe [Declaration])
  - | ScopeCheckLHS Name Pattern (Maybe LHS)
  - | forall a . NoHighlighting (Maybe a)
  - | forall a . SetRange Range (Maybe a)
- data BuiltinDescriptor
  - = BuiltinData (TCM Type) [String]
  - | BuiltinDataCons (TCM Type)
  - | BuiltinPrim String (Term -> TCM ())
  - | BuiltinPostulate Relevance (TCM Type)
  - | BuiltinUnknown (Maybe (TCM Type)) (Term -> TCM ())
- data BuiltinInfo = BuiltinInfo {
  - builtinName :: String
  - builtinDesc :: BuiltinDescriptor
  }
- type BuiltinThings pf = Map String (Builtin pf)
- data Builtin pf
  - = Builtin Term
  - | Prim pf
- data HighlightingLevel
  - = None
  - | NonInteractive
  - | Interactive
- data HighlightingMethod
  - = Direct
  - | Indirect
- ifTopLevelAndHighlightingLevelIs :: MonadTCM tcm => HighlightingLevel -> tcm () -> tcm ()
- data TCEnv = TCEnv {
  - envContext :: Context
  - envLetBindings :: LetBindings
  - envCurrentModule :: ModuleName
  - envCurrentPath :: AbsolutePath
  - envAnonymousModules :: [(ModuleName, Nat)]
  - envImportPath :: [TopLevelModuleName]
  - envMutualBlock :: Maybe MutualId
  - envSolvingConstraints :: Bool
  - envAssignMetas :: Bool
  - envActiveProblems :: [ProblemId]
  - envAbstractMode :: AbstractMode
  - envRelevance :: Relevance
  - envDisplayFormsEnabled :: Bool
  - envReifyInteractionPoints :: Bool
  - envEtaContractImplicit :: Bool
  - envRange :: Range
  - envHighlightingRange :: Range
  - envCall :: Maybe (Closure Call)
  - envEmacs :: Bool
  - envHighlightingLevel :: HighlightingLevel
  - envHighlightingMethod :: HighlightingMethod
  - envModuleNestingLevel :: Integer
  - envAllowDestructiveUpdate :: Bool
  }
- initEnv :: TCEnv
- type Context = [ContextEntry]
- data ContextEntry = Ctx {
  - ctxId :: CtxId
  - ctxEntry :: Dom (Name, Type)
  }
- newtype CtxId = CtxId Nat
- type LetBindings = Map Name (Open (Term, Dom Type))
- data AbstractMode
  - = AbstractMode
  - | ConcreteMode
  - | IgnoreAbstractMode
- data ExpandHidden
  - = ExpandLast
  - | DontExpandLast
- data ExpandInstances
  - = ExpandInstanceArguments
  - | DontExpandInstanceArguments
- data Occ
  - = OccCon {
    - occDatatype :: QName
    - occConstructor :: QName
    - occPosition :: OccPos
    }
  - | OccClause {
    - occFunction :: QName
    - occClause :: Int
    - occPosition :: OccPos
    }
- data OccPos
  - = NonPositively
  - | ArgumentTo Nat QName
- data CallInfo = CallInfo {
  - callInfoRange :: Range
  - callInfoCall :: String
  }
- data TerminationError = TerminationError {
  - termErrFunctions :: [QName]
  - termErrCalls :: [CallInfo]
  }
- data TypeError
  - = InternalError String
  - | NotImplemented String
  - | NotSupported String
  - | CompilationError String
  - | TerminationCheckFailed [TerminationError]
  - | PropMustBeSingleton
  - | DataMustEndInSort Term
  - | ShouldEndInApplicationOfTheDatatype Type
  - | ShouldBeAppliedToTheDatatypeParameters Term Term
  - | ShouldBeApplicationOf Type QName
  - | ConstructorPatternInWrongDatatype QName QName
  - | IndicesNotConstructorApplications [Arg Term]
  - | IndexVariablesNotDistinct [Nat] [Arg Term]
  - | IndicesFreeInParameters [Nat] [Arg Term] [Arg Term]
  - | DoesNotConstructAnElementOf QName Term
  - | DifferentArities
  - | WrongHidingInLHS Type
  - | WrongHidingInLambda Type
  - | WrongHidingInApplication Type
  - | WrongIrrelevanceInLambda Type
  - | NotInductive Term
  - | UninstantiatedDotPattern Expr
  - | IlltypedPattern Pattern Type
  - | TooManyArgumentsInLHS Type
  - | WrongNumberOfConstructorArguments QName Nat Nat
  - | ShouldBeEmpty Type [Pattern]
  - | ShouldBeASort Type
  - | ShouldBePi Type
  - | ShouldBeRecordType Type
  - | ShouldBeRecordPattern Pattern
  - | NotAProperTerm
  - | SetOmegaNotValidType
  - | SplitOnIrrelevant Pattern (Dom Type)
  - | DefinitionIsIrrelevant QName
  - | VariableIsIrrelevant Name
  - | UnequalLevel Comparison Term Term
  - | UnequalTerms Comparison Term Term Type
  - | UnequalTypes Comparison Type Type
  - | UnequalTelescopes Comparison Telescope Telescope
  - | UnequalRelevance Comparison Term Term
  - | UnequalHiding Term Term
  - | UnequalSorts Sort Sort
  - | UnequalBecauseOfUniverseConflict Comparison Term Term
  - | HeterogeneousEquality Term Type Term Type
  - | NotLeqSort Sort Sort
  - | MetaCannotDependOn MetaId [Nat] Nat
  - | MetaOccursInItself MetaId
  - | GenericError String
  - | GenericDocError Doc
  - | BuiltinMustBeConstructor String Expr
  - | NoSuchBuiltinName String
  - | DuplicateBuiltinBinding String Term Term
  - | NoBindingForBuiltin String
  - | NoSuchPrimitiveFunction String
  - | ShadowedModule Name [ModuleName]
  - | BuiltinInParameterisedModule String
  - | NoRHSRequiresAbsurdPattern [NamedArg Pattern]
  - | AbsurdPatternRequiresNoRHS [NamedArg Pattern]
  - | TooFewFields QName [Name]
  - | TooManyFields QName [Name]
  - | DuplicateFields [Name]
  - | DuplicateConstructors [Name]
  - | UnexpectedWithPatterns [Pattern]
  - | WithClausePatternMismatch Pattern Pattern
  - | FieldOutsideRecord
  - | ModuleArityMismatch ModuleName Telescope [NamedArg Expr]
  - | IncompletePatternMatching Term Args
  - | CoverageFailure QName [[Arg Pattern]]
  - | UnreachableClauses QName [[Arg Pattern]]
  - | CoverageCantSplitOn QName Telescope Args Args
  - | CoverageCantSplitIrrelevantType Type
  - | CoverageCantSplitType Type
  - | NotStrictlyPositive QName [Occ]
  - | LocalVsImportedModuleClash ModuleName
  - | UnsolvedMetas [Range]
  - | UnsolvedConstraints Constraints
  - | CyclicModuleDependency [TopLevelModuleName]
  - | FileNotFound TopLevelModuleName [AbsolutePath]
  - | OverlappingProjects AbsolutePath TopLevelModuleName TopLevelModuleName
  - | AmbiguousTopLevelModuleName TopLevelModuleName [AbsolutePath]
  - | ModuleNameDoesntMatchFileName TopLevelModuleName [AbsolutePath]
  - | ClashingFileNamesFor ModuleName [AbsolutePath]
  - | ModuleDefinedInOtherFile TopLevelModuleName AbsolutePath AbsolutePath
  - | 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
  - | NotAnExpression Expr
  - | NotAValidLetBinding NiceDeclaration
  - | NothingAppliedToHiddenArg Expr
  - | NothingAppliedToInstanceArg Expr
  - | UnusedVariableInPatternSynonym
  - | PatternSynonymArityMismatch QName
  - | NoParseForApplication [Expr]
  - | AmbiguousParseForApplication [Expr] [Expr]
  - | NoParseForLHS LHSOrPatSyn Pattern
  - | AmbiguousParseForLHS LHSOrPatSyn Pattern [Pattern]
  - | IFSNoCandidateInScope Type
  - | SafeFlagPostulate Name
  - | SafeFlagPragma [String]
  - | SafeFlagNoTerminationCheck
  - | SafeFlagPrimTrustMe
  - | NeedOptionCopatterns
- data LHSOrPatSyn
  - = IsLHS
  - | IsPatSyn
- data TCErr
  - = TypeError TCState (Closure TypeError)
  - | Exception Range String
  - | IOException Range IOException
  - | PatternErr TCState
- newtype TCMT m a = TCM {
  - unTCM :: IORef TCState -> TCEnv -> m a
  }
- type TCM = TCMT IO
- class (Applicative tcm, MonadIO tcm, MonadReader TCEnv tcm, MonadState TCState tcm) => MonadTCM tcm where
  - liftTCM :: TCM a -> tcm a
- catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a
- 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
- typeError :: MonadTCM tcm => TypeError -> tcm a
- runTCM :: TCMT IO a -> IO (Either TCErr a)
- runTCM' :: MonadIO m => TCMT m a -> m a
- forkTCM :: TCM a -> TCM ()
- extendlambdaname :: [Char]

# Type checking state

data TCState

Constructors

TCSt |
Fields stFreshThings :: FreshThings stSyntaxInfo :: CompressedFile Highlighting info. stTokens :: CompressedFile Highlighting info for tokens (but not those tokens for which highlighting exists in `stSyntaxInfo`). stTermErrs :: Seq TerminationError stMetaStore :: MetaStore stInteractionPoints :: InteractionPoints stAwakeConstraints :: Constraints stSleepingConstraints :: Constraints stDirty :: Bool stOccursCheckDefs :: Set QName Definitions to be considered during occurs check. Initialized to the current mutual block before the check. stSignature :: Signature stImports :: Signature stImportedModules :: Set ModuleName stModuleToSource :: ModuleToSource stVisitedModules :: VisitedModules stCurrentModule :: Maybe ModuleName The current module is available after it has been type checked. stScope :: ScopeInfo stPatternSyns :: PatternSynDefns stPatternSynImports :: PatternSynDefns stPragmaOptions :: PragmaOptions Options applying to the current file. `OPTIONS` pragmas only affect this field. stStatistics :: Statistics stExtLambdaTele :: Map QName (Int, Int) stMutualBlocks :: Map MutualId (Set QName) stLocalBuiltins :: BuiltinThings PrimFun stImportedBuiltins :: BuiltinThings PrimFun stHaskellImports :: Set String Imports that should be generated by the compiler (this includes imports from imported modules). stPersistent :: PersistentTCState stInteractionOutputCallback :: InteractionOutputCallback Callback fuction to call when there is a response to give to the interactive frontend. See the documentation of `InteractionOutputCallback`.

Instances

MonadState TCState RecPatM |
MonadState TCState Unify |
HasFresh i FreshThings => HasFresh i TCState |
MonadIO m => MonadState TCState (TCMT m) |

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 Options which apply to all files, unless overridden.

data FreshThings

Constructors

Fresh |
Fields fMeta :: MetaId fInteraction :: InteractionId fMutual :: MutualId fName :: NameId fCtx :: CtxId fProblem :: ProblemId fInt :: Int Can be used for various things.

Instances

Show FreshThings |
HasFresh Int FreshThings |
HasFresh NameId FreshThings |
HasFresh MetaId FreshThings |
HasFresh CtxId FreshThings |
HasFresh MutualId FreshThings |
HasFresh InteractionId FreshThings |
HasFresh ProblemId FreshThings |

initState :: TCState

stBuiltinThings :: TCState -> BuiltinThings PrimFun

newtype ProblemId

Constructors

ProblemId Nat |

Instances

Enum ProblemId |
Eq ProblemId |
Integral ProblemId |
Num ProblemId |
Ord ProblemId |
Real ProblemId |
Show ProblemId |
Typeable ProblemId |
HasFresh ProblemId FreshThings |

## Interface

data ModuleInfo

Constructors

ModuleInfo |
Fields miInterface :: Interface miWarnings :: Bool `True` if warnings were encountered when the module was type checked. miTimeStamp :: ClockTime The modification time stamp of the interface file when the interface was read or written. Alternatively, if warnings were encountered (in which case there may not be any up-to-date interface file), the time at which the interface was produced (approximately).

type VisitedModules = Map TopLevelModuleName ModuleInfo

type DecodedModules = Map TopLevelModuleName (Interface, ClockTime)

data Interface

Constructors

Interface |
Fields iImportedModules :: [ModuleName] iModuleName :: ModuleName iScope :: Map ModuleName Scope iInsideScope :: ScopeInfo iSignature :: Signature iBuiltin :: BuiltinThings (String, QName) iHaskellImports :: Set String Haskell imports listed in (transitively) imported modules are not included here. iHighlighting :: HighlightingInfo iPragmaOptions :: [OptionsPragma] Pragma options set in the file. iPatternSyns :: PatternSynDefns

Instances

Show Interface |
Typeable Interface |
InstantiateFull Interface |
EmbPrj Interface |

## Closure

data Closure a

Constructors

Closure |
Fields clSignature :: Signature clEnv :: TCEnv clScope :: ScopeInfo clValue :: a

Instances

Typeable1 Closure |
Reify ProblemConstraint (Closure (OutputForm Expr Expr)) |
Show a => Show (Closure a) |
HasRange a => HasRange (Closure a) |
PrettyTCM a => PrettyTCM (Closure a) |
InstantiateFull a => InstantiateFull (Closure a) |
Normalise a => Normalise (Closure a) |
Reduce a => Reduce (Closure a) |
Instantiate a => Instantiate (Closure a) |
MentionsMeta a => MentionsMeta (Closure a) |

buildClosure :: a -> TCM (Closure a)

## Constraints

type Constraints = [ProblemConstraint]

data ProblemConstraint

Constructors

PConstr |
Fields constraintProblem :: ProblemId theConstraint :: Closure Constraint

Instances

Show ProblemConstraint |
Typeable ProblemConstraint |
PrettyTCM ProblemConstraint |
InstantiateFull ProblemConstraint |
Normalise ProblemConstraint |
MentionsMeta ProblemConstraint |
Reify ProblemConstraint (Closure (OutputForm Expr Expr)) |

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
FindInScope MetaId [(Term, Type)] |

Instances

Eq Constraint |
Show Constraint |
Typeable Constraint |
Subst Constraint |
PrettyTCM Constraint |
InstantiateFull Constraint |
Normalise Constraint |
Reduce Constraint |
Instantiate Constraint |
MentionsMeta Constraint |
Reify Constraint (OutputConstraint Expr Expr) |

data Comparison

Constructors

CmpEq |
CmpLeq |

Instances

Eq Comparison |
Show Comparison |
Typeable Comparison |
PrettyTCM Comparison |

# Open things

data Open a

A thing tagged with the context it came from.

Constructors

OpenThing [CtxId] a |

Instances

Functor Open |
Typeable1 Open |
Show a => Show (Open a) |
InstantiateFull a => InstantiateFull (Open a) |
EmbPrj a => EmbPrj (Open a) |

# Judgements

data Judgement t a

Constructors

HasType |
Fields jMetaId :: a jMetaType :: t
IsSort |
Fields jMetaId :: a jMetaType :: t

Instances

Typeable2 Judgement |
Functor (Judgement t) |
Foldable (Judgement t) |
Traversable (Judgement t) |
(Show t, Show a) => Show (Judgement t a) |
(PrettyTCM a, PrettyTCM b) => PrettyTCM (Judgement a b) |
(Reify t t', Reify a a') => Reify (Judgement t a) (Judgement t' a') |

## 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 Type 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

Typeable MetaVariable |
SetRange MetaVariable |
HasRange MetaVariable |

data Listener

Constructors

EtaExpand MetaId |
CheckConstraint Nat ProblemConstraint |

Instances

Eq Listener |
Ord Listener |
Typeable 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 |
Show Frozen |

data MetaInstantiation

Constructors

InstV Term | solved by term
InstS Term | solved by `Lam .. Sort s`
Open | unsolved
OpenIFS | open, to be instantiated as implicit from scope
BlockedConst Term | solution blocked by unsolved constraints
PostponedTypeCheckingProblem (Closure (Expr, Type, TCM Bool)) |

Instances

Show MetaInstantiation |
Typeable MetaInstantiation |

newtype MetaPriority

Constructors

MetaPriority Int |

Instances

Eq MetaPriority |
Ord MetaPriority |
Show MetaPriority |

data RunMetaOccursCheck

Constructors

RunMetaOccursCheck |
DontRunMetaOccursCheck |

Instances

Eq RunMetaOccursCheck |
Ord RunMetaOccursCheck |
Show RunMetaOccursCheck |

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

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

Show NamedMeta |
ToConcrete NamedMeta Expr |

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

type InteractionPoints = Map InteractionId MetaId

newtype InteractionId

Constructors

InteractionId Nat |

Instances

Enum InteractionId |
Eq InteractionId |
Integral InteractionId |
Num InteractionId |
Ord InteractionId |
Read InteractionId |
Real InteractionId |
Show InteractionId |
HasFresh InteractionId FreshThings |
ToConcrete InteractionId Expr |

## Signature

data Signature

Constructors

Sig |
Fields sigSections :: Sections sigDefinitions :: Definitions

Instances

Show Signature |
Typeable Signature |
InstantiateFull Signature |
EmbPrj Signature |

type Sections = Map ModuleName Section

type Definitions = HashMap QName Definition

data Section

Constructors

Section |
Fields secTelescope :: Telescope secFreeVars :: Nat This is the number of parameters when we're inside the section and 0 outside. It's used to know how much of the context to apply function from the section to when translating from abstract to internal syntax.

Instances

Show Section |
Typeable Section |
InstantiateFull Section |
EmbPrj Section |

emptySignature :: Signature

data DisplayForm

Constructors

Display Nat [Term] DisplayTerm | The three arguments are: `n`: number of free variables; Patterns for arguments, one extra free var which represents pattern vars. There should `n` of them. Display form. `n` free variables.

Instances

Show DisplayForm |
Typeable DisplayForm |
Subst DisplayForm |
InstantiateFull DisplayForm |
Normalise DisplayForm |
EmbPrj DisplayForm |

data DisplayTerm

Constructors

DWithApp [DisplayTerm] Args |
DCon QName [Arg DisplayTerm] |
DDef QName [Arg DisplayTerm] |
DDot Term |
DTerm Term |

Instances

Show DisplayTerm |
Typeable DisplayTerm |
Subst DisplayTerm |
Apply DisplayTerm |
PrettyTCM DisplayTerm |
InstantiateFull DisplayTerm |
EmbPrj DisplayTerm |
Reify DisplayTerm Expr |

defaultDisplayForm :: QName -> [Open DisplayForm]

data Definition

Constructors

Defn |
Fields defRelevance :: Relevance Some defs can be irrelevant (but not hidden). defName :: QName defType :: Type Type of the lifted definition. defPolarity :: [Polarity] defArgOccurrences :: [Occurrence] defDisplay :: [Open DisplayForm] defMutual :: MutualId defCompiledRep :: CompiledRepresentation theDef :: Defn

Instances

Show Definition |
Typeable Definition |
Abstract Definition |
Apply Definition |
InstantiateFull Definition |
EmbPrj Definition |

type HaskellCode = String

type HaskellType = String

type EpicCode = String

type JSCode = Exp

data HaskellRepresentation

Constructors

HsDefn HaskellType HaskellCode |
HsType HaskellType |

Instances

Show HaskellRepresentation |
Typeable HaskellRepresentation |
EmbPrj HaskellRepresentation |

data Polarity

Polarity for equality and subtype checking.

Constructors

Covariant | monotone
Contravariant | antitone
Invariant | no information (mixed variance)
Nonvariant | constant

Instances

Eq Polarity |
Show Polarity |
Typeable Polarity |
EmbPrj Polarity |
Abstract [Polarity] |
Apply [Polarity] |

data CompiledRepresentation

Constructors

CompiledRep |
Fields compiledHaskell :: Maybe HaskellRepresentation compiledEpic :: Maybe EpicCode compiledJS :: Maybe JSCode

Instances

Show CompiledRepresentation |
Typeable CompiledRepresentation |
EmbPrj CompiledRepresentation |

noCompiledRep :: CompiledRepresentation

data Occurrence

Subterm occurrences for positivity checking. The constructors are listed in increasing information they provide: `Mixed <= JustPos <= StrictPos <= GuardPos <= Unused` `Mixed <= JustNeg <= Unused`.

Constructors

Mixed | Arbitrary occurrence (positive and negative).
JustNeg | Negative occurrence.
JustPos | Positive occurrence, but not strictly positive.
StrictPos | Strictly positive occurrence.
GuardPos | Guarded strictly positive occurrence (i.e., under ∞). For checking recursive records.
Unused |

Instances

Eq Occurrence |
Ord Occurrence |
Show Occurrence |
Typeable Occurrence |
NFData Occurrence |
SemiRing Occurrence | `Occurrence` is a complete lattice with least element `Mixed` and greatest element `Unused`. It forms a commutative semiring where `oplus` is meet (glb) and `otimes` is composition. Both operations are idempotent. For `oplus`, `Unused` is neutral (zero) and `Mixed` is dominant. For `otimes`, `StrictPos` is neutral (one) and `Unused` is dominant.
PrettyTCM Occurrence |
EmbPrj Occurrence |
Abstract [Occurrence] |
Apply [Occurrence] |
PrettyTCM n => PrettyTCM (n, Occurrence) |

data Defn

Constructors

Axiom |
Function |
Fields funClauses :: [Clause] funCompiled :: CompiledClauses funInv :: FunctionInverse funMutual :: [QName] Mutually recursive functions, `data`s and `record`s. funAbstr :: IsAbstract funDelayed :: Delayed Are the clauses of this definition delayed? funProjection :: Maybe (QName, Int) 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. funStatic :: Bool Should calls to this function be normalised at compile-time? funCopy :: Bool Has this function been created by a module instantiation? funTerminates :: Maybe Bool Has this function been termination checked? Did it pass?
Datatype |
Fields dataPars :: Nat dataIxs :: Nat dataInduction :: Induction dataClause :: Maybe Clause dataCons :: [QName] dataSort :: Sort dataMutual :: [QName] Mutually recursive functions, `data`s and `record`s. dataAbstr :: IsAbstract
Record |
Fields recPars :: Nat Number of parameters. recClause :: Maybe Clause recCon :: QName Constructor name. recNamedCon :: Bool recConType :: Type The record constructor's type. recFields :: [Arg QName] recTel :: Telescope The record field telescope recMutual :: [QName] Mutually recursive functions, `data`s and `record`s. recEtaEquality :: Bool Eta-expand at this record type. `False` for unguarded recursive records. recInduction :: Induction `Inductive` or `Coinductive`? Matters only for recursive records. recRecursive :: Bool Recursive record. Implies `recEtaEquality = False`. Projections are not size-preserving. recAbstr :: IsAbstract
Constructor |
Fields conPars :: Nat conSrcCon :: QName conData :: QName conAbstr :: IsAbstract conInd :: Induction Inductive or coinductive?
Primitive | Primitive or builtin functions.
Fields primAbstr :: IsAbstract primName :: String primClauses :: Maybe [Clause] `Nothing` for primitive functions, ``Just` something` for builtin functions. primCompiled :: Maybe CompiledClauses `Nothing` for primitive functions, ``Just` something` for builtin functions.

Instances

Show Defn |
Typeable Defn |
Abstract Defn |
Apply Defn |
InstantiateFull Defn |
EmbPrj Defn |
Occurs Defn |

defIsRecord :: Defn -> Bool

defIsDataOrRecord :: Defn -> Bool

newtype Fields

Constructors

Fields [(Name, Type)] |

Instances

Typeable Fields |

data Reduced no yes

Constructors

NoReduction no |
YesReduction yes |

Instances

Typeable2 Reduced |
Functor (Reduced no) |

data IsReduced

Constructors

NotReduced |
Reduced (Blocked ()) |

data MaybeReduced a

Constructors

MaybeRed |
Fields isReduced :: IsReduced ignoreReduced :: a

Instances

Functor MaybeReduced |

type MaybeReducedArgs = [MaybeReduced (Arg Term)]

notReduced :: a -> MaybeReduced a

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

data PrimFun

Constructors

PrimFun |
Fields primFunName :: QName primFunArity :: Arity primFunImplementation :: [Arg Term] -> TCM (Reduced MaybeReducedArgs Term)

Instances

Typeable PrimFun |
Abstract PrimFun |
Apply PrimFun |

defClauses :: Definition -> [Clause]

defCompiled :: Definition -> Maybe CompiledClauses

defJSDef :: Definition -> Maybe JSCode

defEpicDef :: Definition -> Maybe EpicCode

defDelayed :: Definition -> Delayed

Are the clauses of this definition delayed?

defCopy :: Definition -> Bool

Is the definition just a copy created by a module instantiation?

defAbstract :: Definition -> IsAbstract

## Injectivity

type FunctionInverse = FunctionInverse' Clause

data FunctionInverse' c

Constructors

NotInjective |
Inverse (Map TermHead c) |

Instances

Functor FunctionInverse' |
Typeable1 FunctionInverse' |
Abstract FunctionInverse |
Apply FunctionInverse |
DropArgs FunctionInverse |
InstantiateFull FunctionInverse |
EmbPrj FunctionInverse |
Show c => Show (FunctionInverse' c) |

data TermHead

Constructors

SortHead |
PiHead |
ConHead QName |

Instances

Eq TermHead |
Ord TermHead |
Show TermHead |
Typeable TermHead |
EmbPrj TermHead |

## Mutual blocks

newtype MutualId

Constructors

MutId Int32 |

Instances

Eq MutualId |
Num MutualId |
Ord MutualId |
Show MutualId |
Typeable MutualId |
EmbPrj MutualId |
HasFresh MutualId FreshThings |

## Statistics

type Statistics = Map String Integer

## Trace

data Call

Constructors

CheckClause Type Clause (Maybe Clause) |
forall a . CheckPattern Pattern Telescope Type (Maybe a) |
CheckLetBinding LetBinding (Maybe ()) |
InferExpr Expr (Maybe (Term, Type)) |
CheckExpr Expr Type (Maybe Term) |
CheckDotPattern Expr Term (Maybe Constraints) |
CheckPatternShadowing Clause (Maybe ()) |
IsTypeCall Expr Sort (Maybe Type) |
IsType_ Expr (Maybe Type) |
InferVar Name (Maybe (Term, Type)) |
InferDef Range QName (Maybe (Term, Type)) |
CheckArguments Range [NamedArg Expr] Type Type (Maybe (Args, Type)) |
CheckDataDef Range Name [LamBinding] [Constructor] (Maybe ()) |
CheckRecDef Range Name [LamBinding] [Constructor] (Maybe ()) |
CheckConstructor QName Telescope Sort Constructor (Maybe ()) |
CheckFunDef Range Name [Clause] (Maybe ()) |
CheckPragma Range Pragma (Maybe ()) |
CheckPrimitive Range Name Expr (Maybe ()) |
CheckIsEmpty Range Type (Maybe ()) |
CheckWithFunctionType Expr (Maybe ()) |
CheckSectionApplication Range ModuleName ModuleApplication (Maybe ()) |
ScopeCheckExpr Expr (Maybe Expr) |
ScopeCheckDeclaration NiceDeclaration (Maybe [Declaration]) |
ScopeCheckLHS Name Pattern (Maybe LHS) |
forall a . NoHighlighting (Maybe a) |
forall a . SetRange Range (Maybe a) | used by `setCurrentRange`

Instances

Typeable Call |
HasRange Call |
PrettyTCM Call |

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

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 |
Typeable1 Builtin |
Foldable Builtin |
Traversable Builtin |
Show pf => Show (Builtin pf) |
InstantiateFull a => InstantiateFull (Builtin a) |
EmbPrj a => EmbPrj (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 |
Ord HighlightingLevel |
Read HighlightingLevel |
Show HighlightingLevel |

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 |
Read HighlightingMethod |
Show HighlightingMethod |

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 TCEnv

Constructors

TCEnv |
Fields envContext :: Context envLetBindings :: LetBindings envCurrentModule :: ModuleName envCurrentPath :: AbsolutePath The path to the file that is currently being type-checked. 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 envSolvingConstraints :: Bool Are we currently in the process of solving active constraints? 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. envReifyInteractionPoints :: Bool should we try to recover interaction points when reifying? disabled when generating types for with functions envEtaContractImplicit :: Bool it's safe to eta contract implicit lambdas as long as we're not going to reify and retypecheck (like when doing with abstraction) envRange :: Range envHighlightingRange :: Range Interactive highlighting uses this range rather than `envRange`. envCall :: Maybe (Closure Call) what we're doing at the moment envEmacs :: Bool True when called from the Emacs mode. envHighlightingLevel :: HighlightingLevel Set to `None` when imported modules are type-checked. envHighlightingMethod :: HighlightingMethod envModuleNestingLevel :: Integer 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.

Instances

Typeable TCEnv |
MonadReader TCEnv RecPatM |
MonadReader TCEnv Unify |
MonadIO m => MonadReader TCEnv (TCMT m) |

initEnv :: TCEnv

## Context

type Context = [ContextEntry]

The `Context` is a stack of `ContextEntry`s.

data ContextEntry

Constructors

Ctx |
Fields ctxId :: CtxId ctxEntry :: Dom (Name, Type)

Instances

Typeable ContextEntry |
PrettyTCM Context |

newtype CtxId

Constructors

CtxId Nat |

Instances

Enum CtxId |
Eq CtxId |
Integral CtxId |
Num CtxId |
Ord CtxId |
Real CtxId |
Show CtxId |
Typeable CtxId |
EmbPrj CtxId |
HasFresh CtxId FreshThings |

## 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

Typeable AbstractMode |

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

data ExpandInstances

Constructors

ExpandInstanceArguments |
DontExpandInstanceArguments |

Instances

Eq ExpandInstances |

# Type checking errors

data Occ

Constructors

OccCon |
Fields occDatatype :: QName occConstructor :: QName occPosition :: OccPos
OccClause |
Fields occFunction :: QName occClause :: Int occPosition :: OccPos

Instances

Show Occ |

data OccPos

Constructors

NonPositively |
ArgumentTo Nat QName |

Instances

Show OccPos |

data CallInfo

Information about a call.

Constructors

CallInfo |
Fields callInfoRange :: Range Range of the head identifier. callInfoCall :: String Formatted representation of the call. (`Doc` would perhaps be better here, but `Doc` doesn't come with an `Ord` instance.)

Instances

Eq CallInfo |
Ord CallInfo |
Show CallInfo |
Typeable CallInfo |

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

Eq TerminationError |
Show TerminationError |
Typeable TerminationError |

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.
DoesNotConstructAnElementOf QName Term | constructor, type
DifferentArities | Varying number of arguments for a function.
WrongHidingInLHS Type | 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.
WrongIrrelevanceInLambda Type | Expected a relevant function and found an irrelevant lambda.
NotInductive Term | The term does not correspond to an inductive data type.
UninstantiatedDotPattern Expr |
IlltypedPattern Pattern Type |
TooManyArgumentsInLHS Type |
WrongNumberOfConstructorArguments QName Nat Nat |
ShouldBeEmpty Type [Pattern] |
ShouldBeASort Type | The given type should have been a sort.
ShouldBePi Type | The given type should have been a pi.
ShouldBeRecordType Type |
ShouldBeRecordPattern Pattern |
NotAProperTerm |
SetOmegaNotValidType |
SplitOnIrrelevant Pattern (Dom Type) |
DefinitionIsIrrelevant QName |
VariableIsIrrelevant Name |
UnequalLevel Comparison Term Term |
UnequalTerms Comparison Term Term Type |
UnequalTypes Comparison Type Type |
UnequalTelescopes Comparison Telescope Telescope |
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 |
NoRHSRequiresAbsurdPattern [NamedArg Pattern] |
AbsurdPatternRequiresNoRHS [NamedArg Pattern] |
TooFewFields QName [Name] |
TooManyFields QName [Name] |
DuplicateFields [Name] |
DuplicateConstructors [Name] |
UnexpectedWithPatterns [Pattern] |
WithClausePatternMismatch Pattern Pattern |
FieldOutsideRecord |
ModuleArityMismatch ModuleName Telescope [NamedArg Expr] |
IncompletePatternMatching Term Args |
CoverageFailure QName [[Arg Pattern]] |
UnreachableClauses QName [[Arg Pattern]] |
CoverageCantSplitOn QName Telescope Args Args |
CoverageCantSplitIrrelevantType Type |
CoverageCantSplitType Type |
NotStrictlyPositive QName [Occ] |
LocalVsImportedModuleClash ModuleName |
UnsolvedMetas [Range] |
UnsolvedConstraints Constraints |
CyclicModuleDependency [TopLevelModuleName] |
FileNotFound TopLevelModuleName [AbsolutePath] |
OverlappingProjects AbsolutePath TopLevelModuleName TopLevelModuleName |
AmbiguousTopLevelModuleName TopLevelModuleName [AbsolutePath] |
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 |
NothingAppliedToHiddenArg Expr |
NothingAppliedToInstanceArg Expr |
UnusedVariableInPatternSynonym |
PatternSynonymArityMismatch QName |
NoParseForApplication [Expr] |
AmbiguousParseForApplication [Expr] [Expr] |
NoParseForLHS LHSOrPatSyn Pattern |
AmbiguousParseForLHS LHSOrPatSyn Pattern [Pattern] |
IFSNoCandidateInScope Type |
SafeFlagPostulate Name |
SafeFlagPragma [String] |
SafeFlagNoTerminationCheck |
SafeFlagPrimTrustMe |
NeedOptionCopatterns |

Instances

Show TypeError |
Typeable TypeError |
Error TypeError |
PrettyTCM TypeError |

data LHSOrPatSyn

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

Constructors

IsLHS |
IsPatSyn |

Instances

Eq LHSOrPatSyn |
Show LHSOrPatSyn |

data TCErr

Type-checking errors.

Constructors

TypeError TCState (Closure TypeError) |
Exception Range String |
IOException Range IOException |
PatternErr TCState | for pattern violations

Instances

Show TCErr |
Typeable TCErr |
Exception TCErr |
Error TCErr |
HasRange TCErr |
PrettyTCM TCErr |
MonadError TCErr IM |
MonadError TCErr CommandM |
MonadError TCErr (TCMT IO) |

# Type checking monad transformer

newtype TCMT m a

Constructors

TCM |
Fields unTCM :: IORef TCState -> TCEnv -> m a

Instances

MonadTrans TCMT |
MonadError TCErr IM |
MonadError TCErr (TCMT IO) |
MonadIO m => MonadReader TCEnv (TCMT m) |
MonadIO m => MonadState TCState (TCMT m) |
MonadIO m => Monad (TCMT m) |
MonadIO m => Functor (TCMT m) |
MonadIO m => Applicative (TCMT m) |
MonadIO m => MonadIO (TCMT m) |
MonadIO m => MonadTCM (TCMT m) |

type TCM = TCMT IO

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

Methods

liftTCM :: TCM a -> tcm a

Instances

MonadTCM RecPatM |
MonadTCM Unify |
MonadIO m => MonadTCM (TCMT m) |
(Error err, MonadTCM tcm) => MonadTCM (ErrorT err tcm) |
(Error err, MonadTCM tcm) => MonadTCM (ExceptionT err tcm) |

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

Preserve the state of the failing computation.

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

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

runTCM :: TCMT IO a -> IO (Either TCErr a)

Running the type checking monad

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

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.

extendlambdaname :: [Char]

Base name for extended lambda patterns