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