Safe Haskell | None |
---|---|
Language | Haskell98 |
- data TCState = TCSt {}
- data PreScopeState = PreScopeState {
- stPreTokens :: CompressedFile
- stPreInteractionPoints :: InteractionPoints
- stPreImports :: Signature
- stPreImportedModules :: Set ModuleName
- stPreModuleToSource :: ModuleToSource
- stPreVisitedModules :: VisitedModules
- stPreScope :: ScopeInfo
- stPrePatternSyns :: PatternSynDefns
- stPrePatternSynImports :: PatternSynDefns
- stPrePragmaOptions :: PragmaOptions
- stPreImportedBuiltins :: BuiltinThings PrimFun
- stPreHaskellImports :: Set String
- stPreFreshInteractionId :: InteractionId
- stPreFreshNameId :: NameId
- type DisambiguatedNames = IntMap QName
- data PostScopeState = PostScopeState {
- stPostSyntaxInfo :: CompressedFile
- stPostDisambiguatedNames :: !DisambiguatedNames
- stPostMetaStore :: MetaStore
- stPostInteractionPoints :: InteractionPoints
- stPostAwakeConstraints :: Constraints
- stPostSleepingConstraints :: Constraints
- stPostDirty :: Bool
- stPostOccursCheckDefs :: Set QName
- stPostSignature :: Signature
- stPostCurrentModule :: Maybe ModuleName
- stPostInstanceDefs :: TempInstanceTable
- stPostStatistics :: Statistics
- stPostMutualBlocks :: Map MutualId (Set QName)
- stPostLocalBuiltins :: BuiltinThings PrimFun
- stPostFreshMetaId :: MetaId
- stPostFreshMutualId :: MutualId
- stPostFreshCtxId :: CtxId
- stPostFreshProblemId :: ProblemId
- stPostFreshInt :: Int
- data PersistentTCState = PersistentTCSt {}
- initPersistentState :: PersistentTCState
- initPreScopeState :: PreScopeState
- initPostScopeState :: PostScopeState
- initState :: TCState
- stTokens :: Lens' CompressedFile TCState
- stImports :: Lens' Signature TCState
- stImportedModules :: Lens' (Set ModuleName) TCState
- stModuleToSource :: Lens' ModuleToSource TCState
- stVisitedModules :: Lens' VisitedModules TCState
- stScope :: Lens' ScopeInfo TCState
- stPatternSyns :: Lens' PatternSynDefns TCState
- stPatternSynImports :: Lens' PatternSynDefns TCState
- stPragmaOptions :: Lens' PragmaOptions TCState
- stImportedBuiltins :: Lens' (BuiltinThings PrimFun) TCState
- stHaskellImports :: Lens' (Set String) TCState
- stFreshInteractionId :: Lens' InteractionId TCState
- stFreshNameId :: Lens' NameId TCState
- stSyntaxInfo :: Lens' CompressedFile TCState
- stDisambiguatedNames :: Lens' DisambiguatedNames TCState
- stMetaStore :: Lens' MetaStore TCState
- stInteractionPoints :: Lens' InteractionPoints TCState
- stAwakeConstraints :: Lens' Constraints TCState
- stSleepingConstraints :: Lens' Constraints TCState
- stDirty :: Lens' Bool TCState
- stOccursCheckDefs :: Lens' (Set QName) TCState
- stSignature :: Lens' Signature TCState
- stCurrentModule :: Lens' (Maybe ModuleName) TCState
- stInstanceDefs :: Lens' TempInstanceTable TCState
- stStatistics :: Lens' Statistics TCState
- stMutualBlocks :: Lens' (Map MutualId (Set QName)) TCState
- stLocalBuiltins :: Lens' (BuiltinThings PrimFun) TCState
- stFreshMetaId :: Lens' MetaId TCState
- stFreshMutualId :: Lens' MutualId TCState
- stFreshCtxId :: Lens' CtxId TCState
- stFreshProblemId :: Lens' ProblemId TCState
- stFreshInt :: Lens' Int TCState
- stBuiltinThings :: TCState -> BuiltinThings PrimFun
- class Enum i => HasFresh i where
- nextFresh :: HasFresh i => TCState -> (i, TCState)
- fresh :: (HasFresh i, MonadState TCState m) => m i
- newtype ProblemId = ProblemId Nat
- freshName :: (MonadState TCState m, HasFresh NameId) => Range -> String -> m Name
- freshNoName :: (MonadState TCState m, HasFresh NameId) => Range -> m Name
- freshNoName_ :: (MonadState TCState m, HasFresh NameId) => m Name
- class FreshName a where
- freshName_ :: (MonadState TCState m, HasFresh NameId) => a -> m Name
- type ModuleToSource = Map TopLevelModuleName AbsolutePath
- type SourceToModule = Map AbsolutePath TopLevelModuleName
- sourceToModule :: TCM SourceToModule
- data ModuleInfo = ModuleInfo {}
- type VisitedModules = Map TopLevelModuleName ModuleInfo
- type DecodedModules = Map TopLevelModuleName Interface
- data Interface = Interface {
- iSourceHash :: Hash
- iImportedModules :: [(ModuleName, Hash)]
- iModuleName :: ModuleName
- iScope :: Map ModuleName Scope
- iInsideScope :: ScopeInfo
- iSignature :: Signature
- iBuiltin :: BuiltinThings (String, QName)
- iHaskellImports :: Set String
- iHighlighting :: HighlightingInfo
- iPragmaOptions :: [OptionsPragma]
- iPatternSyns :: PatternSynDefns
- iFullHash :: Interface -> Hash
- data Closure a = Closure {}
- buildClosure :: a -> TCM (Closure a)
- type Constraints = [ProblemConstraint]
- data ProblemConstraint = PConstr {}
- 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 (Maybe [(Term, Type)])
- data Comparison
- data CompareDirection
- fromCmp :: Comparison -> CompareDirection
- flipCmp :: CompareDirection -> CompareDirection
- dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c
- data Open a = OpenThing {
- openThingCtxIds :: [CtxId]
- openThing :: a
- data Judgement a
- data MetaVariable = MetaVar {}
- data Listener
- data Frozen
- data MetaInstantiation
- data TypeCheckingProblem
- newtype MetaPriority = MetaPriority Int
- data RunMetaOccursCheck
- data MetaInfo = MetaInfo {}
- type MetaNameSuggestion = String
- data NamedMeta = NamedMeta {}
- 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
- getMetaColors :: MetaVariable -> [Color]
- data InteractionPoint = InteractionPoint {}
- type InteractionPoints = Map InteractionId InteractionPoint
- data Signature = Sig {}
- type Sections = Map ModuleName Section
- type Definitions = HashMap QName Definition
- data Section = Section {}
- emptySignature :: Signature
- data DisplayForm = Display {
- dfFreeVars :: Nat
- dfPats :: [Term]
- dfRHS :: DisplayTerm
- data DisplayTerm
- = DWithApp DisplayTerm [DisplayTerm] Args
- | DCon ConHead [Arg DisplayTerm]
- | DDef QName [Elim' DisplayTerm]
- | DDot Term
- | DTerm Term
- defaultDisplayForm :: QName -> [Open DisplayForm]
- defRelevance :: Definition -> Relevance
- defColors :: Definition -> [Color]
- data NLPat
- type PElims = [Elim' NLPat]
- type RewriteRules = [RewriteRule]
- data RewriteRule = RewriteRule {}
- data Definition = Defn {}
- defaultDefn :: ArgInfo -> QName -> Type -> Defn -> Definition
- type HaskellCode = String
- type HaskellType = String
- type EpicCode = String
- type JSCode = Exp
- data HaskellRepresentation
- data HaskellExport = HsExport HaskellType String
- data Polarity
- data CompiledRepresentation = CompiledRep {}
- noCompiledRep :: CompiledRepresentation
- data Occurrence
- data Projection = Projection {
- projProper :: Maybe QName
- projFromType :: QName
- projIndex :: Int
- projDropPars :: Term
- projArgInfo :: ArgInfo
- data Defn
- = Axiom
- | Function {
- funClauses :: [Clause]
- funCompiled :: Maybe CompiledClauses
- funInv :: FunctionInverse
- funMutual :: [QName]
- funAbstr :: IsAbstract
- funDelayed :: Delayed
- funProjection :: Maybe Projection
- funStatic :: Bool
- funCopy :: Bool
- funTerminates :: Maybe Bool
- funExtLam :: Maybe (Int, Int)
- funWith :: Maybe QName
- funCopatternLHS :: Bool
- | Datatype {
- dataPars :: Nat
- dataSmallPars :: Permutation
- dataNonLinPars :: Drop Permutation
- dataIxs :: Nat
- dataInduction :: Induction
- dataClause :: Maybe Clause
- dataCons :: [QName]
- dataSort :: Sort
- dataMutual :: [QName]
- dataAbstr :: IsAbstract
- | Record {
- recPars :: Nat
- recClause :: Maybe Clause
- recConHead :: ConHead
- recNamedCon :: Bool
- recConType :: Type
- recFields :: [Arg QName]
- recTel :: Telescope
- recMutual :: [QName]
- recEtaEquality :: Bool
- recInduction :: Maybe Induction
- recRecursive :: Bool
- recAbstr :: IsAbstract
- | Constructor { }
- | Primitive { }
- emptyFunction :: Defn
- isCopatternLHS :: [Clause] -> Bool
- recCon :: Defn -> QName
- defIsRecord :: Defn -> Bool
- defIsDataOrRecord :: Defn -> Bool
- newtype Fields = Fields [(Name, Type)]
- data Simplification
- data Reduced no yes
- = NoReduction no
- | YesReduction Simplification yes
- data IsReduced
- = NotReduced
- | Reduced (Blocked ())
- data MaybeReduced a = MaybeRed {
- isReduced :: IsReduced
- ignoreReduced :: a
- type MaybeReducedArgs = [MaybeReduced (Arg Term)]
- type MaybeReducedElims = [MaybeReduced Elim]
- notReduced :: a -> MaybeReduced a
- reduced :: Blocked (Arg Term) -> MaybeReduced (Arg Term)
- data AllowedReduction
- type AllowedReductions = [AllowedReduction]
- allReductions :: AllowedReductions
- data PrimFun = PrimFun {
- primFunName :: QName
- primFunArity :: Arity
- primFunImplementation :: [Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term)
- defClauses :: Definition -> [Clause]
- defCompiled :: Definition -> Maybe CompiledClauses
- defJSDef :: Definition -> Maybe JSCode
- defEpicDef :: Definition -> Maybe EpicCode
- defDelayed :: Definition -> Delayed
- defNonterminating :: Definition -> Bool
- defCopy :: Definition -> Bool
- defAbstract :: Definition -> IsAbstract
- type FunctionInverse = FunctionInverse' Clause
- data FunctionInverse' c
- = NotInjective
- | Inverse (Map TermHead c)
- data TermHead
- newtype MutualId = MutId Int32
- type Statistics = Map String Integer
- data Call
- = CheckClause Type SpineClause (Maybe Clause)
- | forall a . CheckPattern Pattern Telescope Type (Maybe a)
- | CheckLetBinding LetBinding (Maybe ())
- | InferExpr Expr (Maybe (Term, Type))
- | CheckExprCall Expr Type (Maybe Term)
- | CheckDotPattern Expr Term (Maybe Constraints)
- | CheckPatternShadowing SpineClause (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)
- type InstanceTable = Map QName [QName]
- type TempInstanceTable = (InstanceTable, [QName])
- data BuiltinDescriptor
- = BuiltinData (TCM Type) [String]
- | BuiltinDataCons (TCM Type)
- | BuiltinPrim String (Term -> TCM ())
- | BuiltinPostulate Relevance (TCM Type)
- | BuiltinUnknown (Maybe (TCM Type)) (Term -> Type -> TCM ())
- data BuiltinInfo = BuiltinInfo {}
- type BuiltinThings pf = Map String (Builtin pf)
- data Builtin pf
- data HighlightingLevel
- data HighlightingMethod
- ifTopLevelAndHighlightingLevelIs :: MonadTCM tcm => HighlightingLevel -> tcm () -> tcm ()
- data TCEnv = TCEnv {
- envContext :: Context
- envLetBindings :: LetBindings
- envCurrentModule :: ModuleName
- envCurrentPath :: Maybe AbsolutePath
- envAnonymousModules :: [(ModuleName, Nat)]
- envImportPath :: [TopLevelModuleName]
- envMutualBlock :: Maybe MutualId
- envTerminationCheck :: TerminationCheck ()
- envSolvingConstraints :: Bool
- envAssignMetas :: Bool
- envActiveProblems :: [ProblemId]
- envAbstractMode :: AbstractMode
- envRelevance :: Relevance
- envColors :: [Color]
- envDisplayFormsEnabled :: Bool
- envReifyInteractionPoints :: Bool
- envEtaContractImplicit :: Bool
- envRange :: Range
- envHighlightingRange :: Range
- envCall :: Maybe (Closure Call)
- envHighlightingLevel :: HighlightingLevel
- envHighlightingMethod :: HighlightingMethod
- envModuleNestingLevel :: Integer
- envAllowDestructiveUpdate :: Bool
- envExpandLast :: ExpandHidden
- envAppDef :: Maybe QName
- envSimplification :: Simplification
- envAllowedReductions :: AllowedReductions
- envCompareBlocked :: Bool
- envPrintDomainFreePi :: Bool
- envInsideDotPattern :: Bool
- envReifyUnquoted :: Bool
- initEnv :: TCEnv
- type Context = [ContextEntry]
- data ContextEntry = Ctx {}
- newtype CtxId = CtxId Nat
- type LetBindings = Map Name (Open (Term, Dom Type))
- data AbstractMode
- data ExpandHidden
- data ExpandInstances
- data Occ
- = OccCon { }
- | OccClause {
- occFunction :: QName
- occClause :: Int
- occPosition :: OccPos
- data OccPos
- data CallInfo = CallInfo {}
- data TerminationError = TerminationError {
- termErrFunctions :: [QName]
- termErrCalls :: [CallInfo]
- data SplitError
- data UnquoteError
- 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]
- | CantResolveOverloadedConstructorsTargetingSameDatatype QName [QName]
- | DoesNotConstructAnElementOf QName Type
- | DifferentArities
- | WrongHidingInLHS
- | WrongHidingInLambda Type
- | WrongHidingInApplication Type
- | WrongNamedArgument (NamedArg Expr)
- | WrongIrrelevanceInLambda Type
- | HidingMismatch Hiding Hiding
- | RelevanceMismatch Relevance Relevance
- | ColorMismatch [Color] [Color]
- | NotInductive Term
- | UninstantiatedDotPattern Expr
- | IlltypedPattern Pattern Type
- | IllformedProjectionPattern Pattern
- | CannotEliminateWithPattern (NamedArg Pattern) Type
- | TooManyArgumentsInLHS Type
- | WrongNumberOfConstructorArguments QName Nat Nat
- | ShouldBeEmpty Type [Pattern]
- | ShouldBeASort Type
- | ShouldBePi Type
- | ShouldBeRecordType Type
- | ShouldBeRecordPattern Pattern
- | NotAProjectionPattern (NamedArg Pattern)
- | NotAProperTerm
- | SetOmegaNotValidType
- | InvalidTypeSort Sort
- | InvalidType Term
- | FunctionTypeInSizeUniv Term
- | SplitOnIrrelevant Pattern (Dom Type)
- | DefinitionIsIrrelevant QName
- | VariableIsIrrelevant Name
- | UnequalTerms Comparison Term Term Type
- | UnequalTypes Comparison Type Type
- | UnequalRelevance Comparison Term Term
- | UnequalHiding Term Term
- | UnequalColors 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
- | IllegalLetInTelescope TypedBinding
- | NoRHSRequiresAbsurdPattern [NamedArg Pattern]
- | AbsurdPatternRequiresNoRHS [NamedArg Pattern]
- | TooFewFields QName [Name]
- | TooManyFields QName [Name]
- | DuplicateFields [Name]
- | DuplicateConstructors [Name]
- | WithOnFreeVariable Expr
- | UnexpectedWithPatterns [Pattern]
- | WithClausePatternMismatch Pattern Pattern
- | FieldOutsideRecord
- | ModuleArityMismatch ModuleName Telescope [NamedArg Expr]
- | IncompletePatternMatching Term [Elim]
- | CoverageFailure QName [[Arg Pattern]]
- | UnreachableClauses QName [[Arg Pattern]]
- | CoverageCantSplitOn QName Telescope Args Args
- | CoverageCantSplitIrrelevantType Type
- | CoverageCantSplitType Type
- | WithoutKError Type Term Term
- | SplitError SplitError
- | NotStrictlyPositive QName [Occ]
- | LocalVsImportedModuleClash ModuleName
- | UnsolvedMetas [Range]
- | UnsolvedConstraints Constraints
- | SolvedButOpenHoles
- | 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
- | BadArgumentsToPatternSynonym QName
- | TooFewArgumentsToPatternSynonym QName
- | UnusedVariableInPatternSynonym
- | NoParseForApplication [Expr]
- | AmbiguousParseForApplication [Expr] [Expr]
- | NoParseForLHS LHSOrPatSyn Pattern
- | AmbiguousParseForLHS LHSOrPatSyn Pattern [Pattern]
- | IFSNoCandidateInScope Type
- | UnquoteFailed UnquoteError
- | SafeFlagPostulate Name
- | SafeFlagPragma [String]
- | SafeFlagNoTerminationCheck
- | SafeFlagNonTerminating
- | SafeFlagTerminating
- | SafeFlagPrimTrustMe
- | NeedOptionCopatterns
- data LHSOrPatSyn
- data TCErr
- data ReduceEnv = ReduceEnv {}
- mapRedEnv :: (TCEnv -> TCEnv) -> ReduceEnv -> ReduceEnv
- mapRedSt :: (TCState -> TCState) -> ReduceEnv -> ReduceEnv
- mapRedEnvSt :: (TCEnv -> TCEnv) -> (TCState -> TCState) -> ReduceEnv -> ReduceEnv
- newtype ReduceM a = ReduceM {}
- runReduceM :: ReduceM a -> TCM a
- runReduceF :: (a -> ReduceM b) -> TCM (a -> b)
- newtype TCMT m a = TCM {}
- type TCM = TCMT IO
- class (Applicative tcm, MonadIO tcm, MonadReader TCEnv tcm, MonadState TCState tcm) => MonadTCM tcm where
- 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
- genericError :: MonadTCM tcm => String -> tcm a
- typeError :: MonadTCM tcm => TypeError -> tcm a
- typeError_ :: MonadTCM tcm => TypeError -> tcm TCErr
- runTCM :: MonadIO m => TCEnv -> TCState -> TCMT m a -> m (a, TCState)
- runTCMTop :: TCM a -> IO (Either TCErr a)
- runTCMTop' :: MonadIO m => TCMT m a -> m a
- runSafeTCM :: TCM a -> TCState -> IO (a, TCState)
- forkTCM :: TCM a -> TCM ()
- extendedLambdaName :: String
- absurdLambdaName :: String
- isAbsurdLambdaName :: QName -> Bool
Type checking state
TCSt | |
|
LensPersistentVerbosity TCState Source | |
LensIncludeDirs TCState Source | |
LensSafeMode TCState Source | |
LensCommandLineOptions TCState Source | |
LensVerbosity TCState Source | |
LensPragmaOptions TCState Source | |
MonadState TCState TerM | |
MonadState TCState Unify | |
MonadIO m => MonadState TCState (TCMT m) Source |
data PreScopeState Source
PreScopeState | |
|
type DisambiguatedNames = IntMap QName Source
data PostScopeState Source
PostScopeState | |
|
data PersistentTCState Source
A part of the state which is not reverted when an error is thrown or the state is reset.
PersistentTCSt | |
|
initPersistentState :: PersistentTCState Source
Empty persistent state.
initPreScopeState :: PreScopeState Source
Empty state of type checker.
st-prefixed lenses
Fresh things
Managing file names
type ModuleToSource = Map TopLevelModuleName AbsolutePath Source
Maps top-level module names to the corresponding source file names.
type SourceToModule = Map AbsolutePath TopLevelModuleName Source
Maps source file names to the corresponding top-level module names.
sourceToModule :: TCM SourceToModule Source
Creates a SourceToModule
map based on stModuleToSource
.
Interface
data ModuleInfo Source
ModuleInfo | |
|
Interface | |
|
iFullHash :: Interface -> Hash Source
Combines the source hash and the (full) hashes of the imported modules.
Closure
Show a => Show (Closure a) Source | |
HasRange a => HasRange (Closure a) Source | |
PrettyTCM a => PrettyTCM (Closure a) Source | |
MentionsMeta a => MentionsMeta (Closure a) Source | |
InstantiateFull a => InstantiateFull (Closure a) Source | |
Normalise a => Normalise (Closure a) Source | |
Simplify a => Simplify (Closure a) Source | |
Reduce a => Reduce (Closure a) Source | |
Instantiate a => Instantiate (Closure a) Source |
buildClosure :: a -> TCM (Closure a) Source
Constraints
type Constraints = [ProblemConstraint] Source
data ProblemConstraint Source
data Constraint Source
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 (Maybe [(Term, Type)]) |
data Comparison Source
data CompareDirection Source
An extension of Comparison
to >=
.
fromCmp :: Comparison -> CompareDirection Source
Embed Comparison
into CompareDirection
.
flipCmp :: CompareDirection -> CompareDirection Source
Flip the direction of comparison.
dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c Source
Turn a Comparison
function into a CompareDirection
function.
Property: dirToCmp f (fromCmp cmp) = f cmp
Open things
A thing tagged with the context it came from.
OpenThing | |
|
Judgements
Parametrized since it is used without MetaId when creating a new meta.
Meta variables
data MetaVariable Source
MetaVar | |
|
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).
Frozen | Do not instantiate. |
Instantiable |
data MetaInstantiation Source
InstV [Arg String] Term | solved by term (abstracted over some free variables) |
InstS Term | solved by |
Open | unsolved |
OpenIFS | open, to be instantiated as "implicit from scope" |
BlockedConst Term | solution blocked by unsolved constraints |
PostponedTypeCheckingProblem (Closure TypeCheckingProblem) (TCM Bool) |
data TypeCheckingProblem Source
CheckExpr Expr Type | |
CheckArgs ExpandHidden ExpandInstances Range [NamedArg Expr] Type Type (Args -> Type -> TCM Term) | |
CheckLambda (Arg ([WithHiding Name], Maybe Type)) Expr Type |
|
newtype MetaPriority Source
Meta variable priority: When we have an equation between meta-variables, which one should be instantiated?
Higher value means higher priority to be instantiated.
data RunMetaOccursCheck Source
MetaInfo
is cloned from one meta to the next during pruning.
MetaInfo | |
|
type MetaNameSuggestion = String Source
Name suggestion for meta variable. Empty string means no suggestion.
For printing, we couple a meta with its name suggestion.
type MetaStore = Map MetaId MetaVariable Source
getMetaEnv :: MetaVariable -> TCEnv Source
getMetaColors :: MetaVariable -> [Color] Source
Interaction meta variables
data InteractionPoint Source
Interaction points are created by the scope checker who sets the range. The meta variable is created by the type checker and then hooked up to the interaction point.
type InteractionPoints = Map InteractionId InteractionPoint Source
Data structure managing the interaction points.
Signature
type Sections = Map ModuleName Section Source
type Definitions = HashMap QName Definition Source
Section | |
|
data DisplayForm Source
A DisplayForm
is in essence a rewrite rule
q ts --> dt
for a defined symbol (could be a constructor as well) q
.
The right hand side is a DisplayTerm
which is used to
reify
to a more readable Syntax
.
The patterns ts
are just terms, but var 0
is interpreted
as a hole. Each occurrence of var 0
is a new hole (pattern var).
For each *occurrence* of var0
the rhs dt
has a free variable.
These are instantiated when matching a display form against a
term q vs
succeeds.
Display | |
|
data DisplayTerm Source
DWithApp DisplayTerm [DisplayTerm] Args |
|
DCon ConHead [Arg DisplayTerm] |
|
DDef QName [Elim' DisplayTerm] |
|
DDot Term |
|
DTerm Term |
|
defaultDisplayForm :: QName -> [Open DisplayForm] Source
By default, we have no display form.
defColors :: Definition -> [Color] Source
Non-linear (non-constructor) first-order pattern.
type RewriteRules = [RewriteRule] Source
data RewriteRule Source
Rewrite rules can be added independently from function clauses.
Show RewriteRule Source | |
Abstract RewriteRule Source |
|
Apply RewriteRule Source | |
PrettyTCM RewriteRule Source | |
EmbPrj RewriteRule Source | |
InstantiateFull RewriteRule Source |
data Definition Source
Defn | |
|
defaultDefn :: ArgInfo -> QName -> Type -> Defn -> Definition Source
Create a definition with sensible defaults.
type HaskellCode = String Source
type HaskellType = String Source
data HaskellExport Source
Polarity for equality and subtype checking.
Covariant | monotone |
Contravariant | antitone |
Invariant | no information (mixed variance) |
Nonvariant | constant |
data Occurrence Source
Subterm occurrences for positivity checking.
The constructors are listed in increasing information they provide:
Mixed <= JustPos <= StrictPos <= GuardPos <= Unused
Mixed <= JustNeg <= Unused
.
data Projection Source
Additional information for projection Function
s.
Projection | |
|
Axiom | Postulate. |
Function | |
| |
Datatype | |
| |
Record | |
| |
Constructor | |
Primitive | Primitive or builtin functions. |
|
A template for creating Function
definitions, with sensible defaults.
isCopatternLHS :: [Clause] -> Bool Source
defIsRecord :: Defn -> Bool Source
defIsDataOrRecord :: Defn -> Bool Source
data Simplification Source
Did we encounter a simplifying reduction? In terms of CIC, that would be a iota-reduction. In terms of Agda, this is a constructor or literal pattern that matched. Just beta-reduction (substitution) or delta-reduction (unfolding of definitions) does not count as simplifying?
Three cases: 1. not reduced, 2. reduced, but blocked, 3. reduced, not blocked.
NotReduced | |
Reduced (Blocked ()) |
data MaybeReduced a Source
MaybeRed | |
|
Functor MaybeReduced Source | |
IsProjElim e => IsProjElim (MaybeReduced e) Source | |
PrettyTCM a => PrettyTCM (MaybeReduced a) Source |
type MaybeReducedArgs = [MaybeReduced (Arg Term)] Source
type MaybeReducedElims = [MaybeReduced Elim] Source
notReduced :: a -> MaybeReduced a Source
data AllowedReduction Source
Controlling reduce
.
ProjectionReductions | (Projection and) projection-like functions may be reduced. |
FunctionReductions | Functions which are not projections may be reduced. |
LevelReductions | Reduce |
NonTerminatingReductions | Functions that have not passed termination checking. |
type AllowedReductions = [AllowedReduction] Source
allReductions :: AllowedReductions Source
Not quite all reductions (skip non-terminating reductions)
PrimFun | |
|
defClauses :: Definition -> [Clause] Source
defJSDef :: Definition -> Maybe JSCode Source
defEpicDef :: Definition -> Maybe EpicCode Source
defDelayed :: Definition -> Delayed Source
Are the clauses of this definition delayed?
defNonterminating :: Definition -> Bool Source
Has the definition failed the termination checker?
defCopy :: Definition -> Bool Source
Is the definition just a copy created by a module instantiation?
Injectivity
data FunctionInverse' c Source
Mutual blocks
Statistics
type Statistics = Map String Integer Source
Trace
Instance table
type InstanceTable = Map QName [QName] Source
The instance table is a Map
associating to every name of
recorddata typepostulate its list of instances
type TempInstanceTable = (InstanceTable, [QName]) Source
When typechecking something of the following form:
instance x : _ x = y
it's not yet known where to add x
, so we add it to a list of
unresolved instances and we'll deal with it later.
Builtin things
data BuiltinDescriptor Source
BuiltinData (TCM Type) [String] | |
BuiltinDataCons (TCM Type) | |
BuiltinPrim String (Term -> TCM ()) | |
BuiltinPostulate Relevance (TCM Type) | |
BuiltinUnknown (Maybe (TCM Type)) (Term -> Type -> TCM ()) | Builtin of any kind.
Type can be checked ( |
type BuiltinThings pf = Map String (Builtin pf) Source
Highlighting levels
data HighlightingLevel Source
How much highlighting should be sent to the user interface?
None | |
NonInteractive | |
Interactive | This includes both non-interactive highlighting and interactive highlighting of the expression that is currently being type-checked. |
data HighlightingMethod Source
How should highlighting be sent to the user interface?
ifTopLevelAndHighlightingLevelIs :: MonadTCM tcm => HighlightingLevel -> tcm () -> tcm () Source
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
TCEnv | |
|
Context
type Context = [ContextEntry] Source
The Context
is a stack of ContextEntry
s.
Let bindings
Abstract mode
data AbstractMode Source
AbstractMode | Abstract things in the current module can be accessed. |
ConcreteMode | No abstract things can be accessed. |
IgnoreAbstractMode | All abstract things can be accessed. |
Insertion of implicit arguments
data ExpandHidden Source
ExpandLast | Add implicit arguments in the end until type is no longer hidden |
DontExpandLast | Do not append implicit arguments. |
data ExpandInstances Source
Type checking errors
OccCon | |
| |
OccClause | |
|
Information about a call.
CallInfo | |
|
data TerminationError Source
Information about a mutual block which did not pass the termination checker.
TerminationError | |
|
data SplitError Source
Error when splitting a pattern variable into possible constructor patterns.
NotADatatype (Closure Type) | Neither data type nor record. |
IrrelevantDatatype (Closure Type) | Data type, but in irrelevant position. |
CoinductiveDatatype (Closure Type) | Split on codata not allowed. UNUSED, but keep! -- | NoRecordConstructor Type -- ^ record type, but no constructor |
CantSplit | |
| |
GenericSplitError String |
data UnquoteError Source
BadVisibility String (Arg Term) | |
ConInsteadOfDef QName String String | |
DefInsteadOfCon QName String String | |
NotAConstructor String Term | NotAConstructor kind term |
NotALiteral String Term | |
RhsUsesDottedVar [Int] Term | |
BlockedOnMeta MetaId | |
UnquotePanic String |
data LHSOrPatSyn Source
Distinguish error message when parsing lhs or pattern synonym, resp.
Type-checking errors.
The reduce monad
Environment of the reduce monad.
runReduceM :: ReduceM a -> TCM a Source
runReduceF :: (a -> ReduceM b) -> TCM (a -> b) Source
Type checking monad transformer
MonadTrans TCMT Source | |
MonadIO m => MonadState TCState (TCMT m) Source | |
MonadIO m => MonadReader TCEnv (TCMT m) Source | |
MonadError TCErr (TCMT IO) Source | |
MonadIO m => Monad (TCMT m) Source | |
MonadIO m => Functor (TCMT m) Source | |
MonadIO m => Applicative (TCMT m) Source | |
MonadIO m => MonadIO (TCMT m) Source | |
MonadIO m => MonadTCM (TCMT m) Source | |
MonadIO m => HasBuiltins (TCMT m) Source | |
MonadIO m => HasOptions (TCMT m) Source | |
HasConstInfo (TCMT IO) Source |
class (Applicative tcm, MonadIO tcm, MonadReader TCEnv tcm, MonadState TCState tcm) => MonadTCM tcm where Source
MonadTCM TerM Source | |
MonadTCM Unify Source | |
MonadTCM tcm => MonadTCM (MaybeT tcm) Source | |
MonadTCM tcm => MonadTCM (ListT tcm) Source | |
MonadIO m => MonadTCM (TCMT m) Source | |
(Monoid w, MonadTCM tcm) => MonadTCM (WriterT w tcm) Source | |
(Error err, MonadTCM tcm) => MonadTCM (ExceptT err tcm) Source | |
(Error err, MonadTCM tcm) => MonadTCM (ExceptionT err tcm) Source |
catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a Source
Preserve the state of the failing computation.
returnTCMT :: MonadIO m => a -> TCMT m a Source
patternViolation :: TCM a Source
internalError :: MonadTCM tcm => String -> tcm a Source
genericError :: MonadTCM tcm => String -> tcm a Source
typeError_ :: MonadTCM tcm => TypeError -> tcm TCErr Source
runTCM :: MonadIO m => TCEnv -> TCState -> TCMT m a -> m (a, TCState) Source
Running the type checking monad (most general form).
runTCMTop :: TCM a -> IO (Either TCErr a) Source
Running the type checking monad on toplevel (with initial state).
runTCMTop' :: MonadIO m => TCMT m a -> m a Source
runSafeTCM :: TCM a -> TCState -> IO (a, TCState) Source
runSafeTCM
runs a safe TCM
action (a TCM
action which cannot fail)
in the initial environment.
forkTCM :: TCM a -> TCM () Source
Runs the given computation in a separate thread, with a copy of the current state and environment.
Note that Agda sometimes uses actual, mutable state. If the
computation given to forkTCM
tries to modify this state, then
bad things can happen, because accesses are not mutually exclusive.
The forkTCM
function has been added mainly to allow the thread to
read (a snapshot of) the current state in a convenient way.
Note also that exceptions which are raised in the thread are not propagated to the parent, so the thread should not do anything important.
extendedLambdaName :: String Source
Base name for extended lambda patterns
absurdLambdaName :: String Source
Name of absurdLambda definitions.
isAbsurdLambdaName :: QName -> Bool Source
Check whether we have an definition from an absurd lambda.