- data TCState = TCSt {
- stFreshThings :: FreshThings
- stMetaStore :: MetaStore
- stInteractionPoints :: InteractionPoints
- stConstraints :: Constraints
- stSignature :: Signature
- stImports :: Signature
- stImportedModules :: Set ModuleName
- stModuleToSource :: ModuleToSource
- stVisitedModules :: VisitedModules
- stDecodedModules :: DecodedModules
- stCurrentModule :: Maybe ModuleName
- stScope :: ScopeInfo
- stPersistentOptions :: CommandLineOptions
- stPragmaOptions :: CommandLineOptions
- stStatistics :: Statistics
- stTrace :: CallTrace
- stMutualBlocks :: Map MutualId (Set QName)
- stLocalBuiltins :: BuiltinThings PrimFun
- stImportedBuiltins :: BuiltinThings PrimFun
- stHaskellImports :: Set String
- data FreshThings = Fresh {}
- initState :: TCState
- stBuiltinThings :: TCState -> BuiltinThings PrimFun
- data ModuleInfo = ModuleInfo {}
- type VisitedModules = Map TopLevelModuleName ModuleInfo
- type DecodedModules = Map TopLevelModuleName (Interface, ClockTime)
- data Interface = Interface {}
- data Closure a = Closure {}
- buildClosure :: MonadTCM tcm => a -> tcm (Closure a)
- type ConstraintClosure = Closure Constraint
- data Constraint
- data Comparison
- type Constraints = [ConstraintClosure]
- data Open a = OpenThing [CtxId] a
- data Judgement t a
- data MetaVariable = MetaVar {}
- data MetaInstantiation
- newtype MetaPriority = MetaPriority Int
- type MetaInfo = Closure Range
- type MetaStore = Map MetaId MetaVariable
- normalMetaPriority :: MetaPriority
- lowMetaPriority :: MetaPriority
- highMetaPriority :: MetaPriority
- getMetaInfo :: MetaVariable -> MetaInfo
- getMetaScope :: MetaVariable -> ScopeInfo
- getMetaEnv :: MetaVariable -> TCEnv
- getMetaSig :: MetaVariable -> Signature
- type InteractionPoints = Map InteractionId MetaId
- newtype InteractionId = InteractionId Nat
- data Signature = Sig {}
- type Sections = Map ModuleName Section
- type Definitions = Map QName Definition
- data Section = Section {}
- emptySignature :: Signature
- data DisplayForm = Display Nat [Term] DisplayTerm
- data DisplayTerm
- = DWithApp [DisplayTerm] Args
- | DTerm Term
- defaultDisplayForm :: QName -> [Open DisplayForm]
- data Definition = Defn {}
- type HaskellCode = String
- type HaskellType = String
- data HaskellRepresentation
- data Polarity
- = Covariant
- | Contravariant
- | Invariant
- data Occurrence
- data Defn
- = Axiom { }
- | Function {
- funClauses :: [Clause]
- funInv :: FunctionInverse
- funPolarity :: [Polarity]
- funArgOccurrences :: [Occurrence]
- funAbstr :: IsAbstract
- funDelayed :: Delayed
- | Datatype {
- dataPars :: Nat
- dataIxs :: Nat
- dataInduction :: Induction
- dataClause :: Maybe Clause
- dataCons :: [QName]
- dataSort :: Sort
- dataPolarity :: [Polarity]
- dataArgOccurrences :: [Occurrence]
- dataHsType :: Maybe HaskellType
- dataAbstr :: IsAbstract
- | Record {
- recPars :: Nat
- recClause :: Maybe Clause
- recCon :: Maybe QName
- recConType :: Type
- recFields :: [(Hiding, QName)]
- recTel :: Telescope
- recPolarity :: [Polarity]
- recArgOccurrences :: [Occurrence]
- recAbstr :: IsAbstract
- | Constructor {
- conPars :: Nat
- conSrcCon :: QName
- conData :: QName
- conHsCode :: Maybe (HaskellType, HaskellCode)
- conAbstr :: IsAbstract
- conInd :: Induction
- | Primitive {
- primAbstr :: IsAbstract
- primName :: String
- primClauses :: Maybe [Clause]
- newtype Fields = Fields [(Name, Type)]
- data Reduced no yes
- = NoReduction no
- | YesReduction yes
- data PrimFun = PrimFun {
- primFunName :: QName
- primFunArity :: Arity
- primFunImplementation :: MonadTCM tcm => [Arg Term] -> tcm (Reduced [Arg Term] Term)
- defClauses :: Definition -> [Clause]
- data Delayed
- = Delayed
- | NotDelayed
- defDelayed :: Definition -> Delayed
- defAbstract :: Definition -> IsAbstract
- data FunctionInverse
- = NotInjective
- | Inverse (Map TermHead Clause)
- data TermHead
- newtype MutualId = MutId Int
- type Statistics = Map String Int
- type CallTrace = Trace (Closure Call)
- noTrace :: CallTrace
- 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, Constraints))
- | 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 ())
- | CheckSectionApplication Range ModuleName Telescope ModuleName [NamedArg Expr] (Maybe ())
- | ScopeCheckExpr Expr (Maybe Expr)
- | ScopeCheckDeclaration NiceDeclaration (Maybe [Declaration])
- | ScopeCheckLHS Name Pattern (Maybe LHS)
- | ScopeCheckDefinition NiceDefinition (Maybe Definition)
- | forall a . TermFunDef Range Name [Clause] (Maybe a)
- | forall a . SetRange Range (Maybe a)
- type BuiltinThings pf = Map String (Builtin pf)
- data Builtin pf
- data TCEnv = TCEnv {
- envContext :: Context
- envLetBindings :: LetBindings
- envCurrentModule :: ModuleName
- envAnonymousModules :: [(ModuleName, Nat)]
- envImportPath :: [TopLevelModuleName]
- envMutualBlock :: Maybe MutualId
- envAbstractMode :: AbstractMode
- envReplace :: Bool
- envDisplayFormsEnabled :: Bool
- envReifyInteractionPoints :: Bool
- initEnv :: TCEnv
- type Context = [ContextEntry]
- data ContextEntry = Ctx {}
- newtype CtxId = CtxId Nat
- type LetBindings = Map Name (Open (Term, Type))
- data AbstractMode
- data Occ
- = OccCon { }
- | OccClause {
- occFunction :: QName
- occClause :: Int
- occPosition :: OccPos
- data OccPos
- data TypeError
- = InternalError String
- | NotImplemented String
- | NotSupported String
- | CompilationError String
- | TerminationCheckFailed [([QName], [Range])]
- | PropMustBeSingleton
- | DataMustEndInSort Term
- | ShouldEndInApplicationOfTheDatatype Type
- | ShouldBeAppliedToTheDatatypeParameters Term Term
- | ShouldBeApplicationOf Type QName
- | ConstructorPatternInWrongDatatype QName QName
- | DoesNotConstructAnElementOf QName Term
- | DifferentArities
- | WrongHidingInLHS Type
- | WrongHidingInLambda Type
- | WrongHidingInApplication Type
- | DependentPatternMatchingOnCodata
- | NotInductive Term
- | UninstantiatedDotPattern Expr
- | IlltypedPattern Pattern Type
- | TooManyArgumentsInLHS Nat Type
- | WrongNumberOfConstructorArguments QName Nat Nat
- | ShouldBeEmpty Type [Pattern]
- | ShouldBeASort Type
- | ShouldBePi Type
- | ShouldBeRecordType Type
- | NotAProperTerm
- | UnequalTerms Comparison Term Term Type
- | UnequalTypes Comparison Type Type
- | UnequalTelescopes Comparison Telescope Telescope
- | UnequalHiding Type Type
- | UnequalSorts Sort Sort
- | NotLeqSort Sort Sort
- | MetaCannotDependOn MetaId [Nat] Nat
- | MetaOccursInItself MetaId
- | GenericError String
- | BuiltinMustBeConstructor String Expr
- | NoSuchBuiltinName String
- | DuplicateBuiltinBinding String Term Term
- | NoBindingForBuiltin String
- | NoSuchPrimitiveFunction String
- | ShadowedModule [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
- | 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]
- | InvalidPattern Pattern
- | RepeatedVariablesInPattern [Name]
- | NotAModuleExpr Expr
- | NotAnExpression Expr
- | NotAValidLetBinding NiceDeclaration
- | NothingAppliedToHiddenArg Expr
- | NoParseForApplication [Expr]
- | AmbiguousParseForApplication [Expr] [Expr]
- | NoParseForLHS Pattern
- | AmbiguousParseForLHS Pattern [Pattern]
- data TCErr'
- data TCErr = TCErr {}
- newtype TCMT m a = TCM {}
- type TCM = TCMT IO
- class (Applicative tcm, MonadIO tcm, MonadReader TCEnv tcm, MonadState TCState tcm) => MonadTCM tcm where
- mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n a
- pureTCM :: Monad m => (TCState -> TCEnv -> a) -> TCMT m a
- patternViolation :: MonadTCM tcm => tcm a
- internalError :: MonadTCM tcm => String -> tcm a
- typeError :: MonadTCM tcm => TypeError -> tcm a
- runTCM :: TCMT IO a -> IO (Either TCErr a)
- runTCM' :: Monad m => TCMT m a -> m a
Type checking state
TCSt | |
|
MonadState TCState Unify | |
HasFresh i FreshThings => HasFresh i TCState | |
MonadIO m => MonadState TCState (TCMT m) |
data FreshThings Source
Interface
data ModuleInfo Source
ModuleInfo | |
|
Interface | |
|
Closure
Typeable1 Closure | |
Data a => Data (Closure a) | |
Show a => Show (Closure a) | |
HasRange a => HasRange (Closure a) | |
InstantiateFull a => InstantiateFull (Closure a) | |
Normalise a => Normalise (Closure a) | |
Reduce a => Reduce (Closure a) | |
Instantiate a => Instantiate (Closure a) | |
PrettyTCM a => PrettyTCM (Closure a) |
buildClosure :: MonadTCM tcm => a -> tcm (Closure a)Source
Constraints
data Constraint Source
data Comparison Source
type Constraints = [ConstraintClosure]Source
Open things
A thing tagged with the context it came from.
Judgements
Meta variables
data MetaVariable Source
MetaVar | |
|
data MetaInstantiation Source
type MetaStore = Map MetaId MetaVariableSource
Interaction meta variables
newtype InteractionId Source
Signature
type Sections = Map ModuleName SectionSource
type Definitions = Map QName DefinitionSource
Section | |
|
data DisplayForm Source
Display Nat [Term] DisplayTerm | The three arguments are:
|
data DisplayTerm Source
defaultDisplayForm :: QName -> [Open DisplayForm]Source
data Definition Source
type HaskellCode = StringSource
type HaskellType = StringSource
data Occurrence Source
PrimFun | |
|
defClauses :: Definition -> [Clause]Source
Used to specify whether something should be delayed.
defDelayed :: Definition -> DelayedSource
Are the clauses of this definition delayed?
Injectivity
data FunctionInverse Source
Mutual blocks
Statistics
type Statistics = Map String IntSource
Trace
Builtin things
type BuiltinThings pf = Map String (Builtin pf)Source
Type checking environment
TCEnv | |
|
Context
type Context = [ContextEntry]Source
data ContextEntry Source
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 |
Type checking errors
OccCon | |
| |
OccClause | |
|
Type-checking errors.
TypeError TCState (Closure TypeError) | |
Exception Range String | |
IOException Range IOException | |
PatternErr TCState | for pattern violations |
AbortAssign TCState | used to abort assignment to meta when there are instantiations |
Type-checking errors, potentially paired with relevant syntax highlighting information.
TCErr | |
|
Type checking monad transformer
class (Applicative tcm, MonadIO tcm, MonadReader TCEnv tcm, MonadState TCState tcm) => MonadTCM tcm whereSource
patternViolation :: MonadTCM tcm => tcm aSource
internalError :: MonadTCM tcm => String -> tcm aSource