Safe Haskell	None
Language	Haskell2010

Agda.Compiler.Backend

Description

Interface for compiler backend writers.

Synopsis

data Backend where
- Backend :: Backend' opts env menv mod def -> Backend
data Backend' opts env menv mod def = Backend' {
- backendName :: String
- backendVersion :: Maybe String
- options :: opts
- commandLineFlags :: [OptDescr (Flag opts)]
- isEnabled :: opts -> Bool
- preCompile :: opts -> TCM env
- postCompile :: env -> IsMain -> Map ModuleName mod -> TCM ()
- preModule :: env -> IsMain -> ModuleName -> FilePath -> TCM (Recompile menv mod)
- postModule :: env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod
- compileDef :: env -> menv -> IsMain -> Definition -> TCM def
- scopeCheckingSuffices :: Bool
- mayEraseType :: QName -> TCM Bool
}
data Recompile menv mod
- = Recompile menv
- | Skip mod
data IsMain
- = IsMain
- | NotMain
type Flag opts = opts -> OptM opts
toTreeless :: EvaluationStrategy -> QName -> TCM (Maybe TTerm)
module Agda.Syntax.Treeless
builtinNat :: String
builtinSuc :: String
builtinZero :: String
builtinNatPlus :: String
builtinNatMinus :: String
builtinNatTimes :: String
builtinNatDivSucAux :: String
builtinNatModSucAux :: String
builtinNatEquals :: String
builtinNatLess :: String
builtinWord64 :: String
builtinInteger :: String
builtinIntegerPos :: String
builtinIntegerNegSuc :: String
builtinFloat :: String
builtinChar :: String
builtinString :: String
builtinUnit :: String
builtinUnitUnit :: String
builtinSigma :: String
builtinBool :: String
builtinTrue :: String
builtinFalse :: String
builtinList :: String
builtinNil :: String
builtinCons :: String
builtinIO :: String
builtinId :: String
builtinConId :: String
builtinIdElim :: String
builtinPath :: String
builtinPathP :: String
builtinInterval :: String
builtinIMin :: String
builtinIMax :: String
builtinINeg :: String
builtinIZero :: String
builtinIOne :: String
builtinPartial :: String
builtinPartialP :: String
builtinIsOne :: String
builtinItIsOne :: String
builtinEquiv :: String
builtinEquivFun :: String
builtinEquivProof :: String
builtinTranspProof :: String
builtinGlue :: String
builtin_glue :: String
builtin_unglue :: String
builtin_glueU :: String
builtin_unglueU :: String
builtinFaceForall :: String
builtinIsOne1 :: String
builtinIsOne2 :: String
builtinIsOneEmpty :: String
builtinComp :: String
builtinPOr :: String
builtinTrans :: String
builtinHComp :: String
builtinSub :: String
builtinSubIn :: String
builtinSubOut :: String
builtinSizeUniv :: String
builtinSize :: String
builtinSizeLt :: String
builtinSizeSuc :: String
builtinSizeInf :: String
builtinSizeMax :: String
builtinInf :: String
builtinSharp :: String
builtinFlat :: String
builtinEquality :: String
builtinRefl :: String
builtinRewrite :: String
builtinLevelMax :: String
builtinLevel :: String
builtinLevelZero :: String
builtinLevelSuc :: String
builtinSetOmega :: String
builtinFromNat :: String
builtinFromNeg :: String
builtinFromString :: String
builtinQName :: String
builtinAgdaSort :: String
builtinAgdaSortSet :: String
builtinAgdaSortLit :: String
builtinAgdaSortUnsupported :: String
builtinHiding :: String
builtinHidden :: String
builtinInstance :: String
builtinVisible :: String
builtinRelevance :: String
builtinRelevant :: String
builtinIrrelevant :: String
builtinAssoc :: String
builtinAssocLeft :: String
builtinAssocRight :: String
builtinAssocNon :: String
builtinPrecedence :: String
builtinPrecRelated :: String
builtinPrecUnrelated :: String
builtinFixity :: String
builtinFixityFixity :: String
builtinArg :: String
builtinArgInfo :: String
builtinArgArgInfo :: String
builtinArgArg :: String
builtinAbs :: String
builtinAbsAbs :: String
builtinAgdaTerm :: String
builtinAgdaTermVar :: String
builtinAgdaTermLam :: String
builtinAgdaTermExtLam :: String
builtinAgdaTermDef :: String
builtinAgdaTermCon :: String
builtinAgdaTermPi :: String
builtinAgdaTermSort :: String
builtinAgdaTermLit :: String
builtinAgdaTermUnsupported :: String
builtinAgdaTermMeta :: String
builtinAgdaErrorPart :: String
builtinAgdaErrorPartString :: String
builtinAgdaErrorPartTerm :: String
builtinAgdaErrorPartName :: String
builtinAgdaLiteral :: String
builtinAgdaLitNat :: String
builtinAgdaLitWord64 :: String
builtinAgdaLitFloat :: String
builtinAgdaLitChar :: String
builtinAgdaLitString :: String
builtinAgdaLitQName :: String
builtinAgdaLitMeta :: String
builtinAgdaClause :: String
builtinAgdaClauseClause :: String
builtinAgdaClauseAbsurd :: String
builtinAgdaPattern :: String
builtinAgdaPatVar :: String
builtinAgdaPatCon :: String
builtinAgdaPatDot :: String
builtinAgdaPatLit :: String
builtinAgdaPatProj :: String
builtinAgdaPatAbsurd :: String
builtinAgdaDefinitionFunDef :: String
builtinAgdaDefinitionDataDef :: String
builtinAgdaDefinitionRecordDef :: String
builtinAgdaDefinitionDataConstructor :: String
builtinAgdaDefinitionPostulate :: String
builtinAgdaDefinitionPrimitive :: String
builtinAgdaDefinition :: String
builtinAgdaMeta :: String
builtinAgdaTCM :: String
builtinAgdaTCMReturn :: String
builtinAgdaTCMBind :: String
builtinAgdaTCMUnify :: String
builtinAgdaTCMTypeError :: String
builtinAgdaTCMInferType :: String
builtinAgdaTCMCheckType :: String
builtinAgdaTCMNormalise :: String
builtinAgdaTCMReduce :: String
builtinAgdaTCMCatchError :: String
builtinAgdaTCMGetContext :: String
builtinAgdaTCMExtendContext :: String
builtinAgdaTCMInContext :: String
builtinAgdaTCMFreshName :: String
builtinAgdaTCMDeclareDef :: String
builtinAgdaTCMDeclarePostulate :: String
builtinAgdaTCMDefineFun :: String
builtinAgdaTCMGetType :: String
builtinAgdaTCMGetDefinition :: String
builtinAgdaTCMBlockOnMeta :: String
builtinAgdaTCMCommit :: String
builtinAgdaTCMQuoteTerm :: String
builtinAgdaTCMUnquoteTerm :: String
builtinAgdaTCMIsMacro :: String
builtinAgdaTCMWithNormalisation :: String
builtinAgdaTCMDebugPrint :: String
builtinAgdaTCMNoConstraints :: String
builtinAgdaTCMRunSpeculative :: String
builtinsNoDef :: [String]
sizeBuiltins :: [String]
data Polarity
- = Covariant
- | Contravariant
- | Invariant
- | Nonvariant
newtype ProblemId = ProblemId Nat
data Comparison
- = CmpEq
- | CmpLeq
type BackendName = String
type ModuleToSource = Map TopLevelModuleName AbsolutePath
type TCM = TCMT IO
newtype TCMT m a = TCM {
- unTCM :: IORef TCState -> TCEnv -> m a
}
data TCState = TCSt {
- stPreScopeState :: !PreScopeState
- stPostScopeState :: !PostScopeState
- stPersistentState :: !PersistentTCState
}
data TCEnv = TCEnv {
- envContext :: Context
- envLetBindings :: LetBindings
- envCurrentModule :: ModuleName
- envCurrentPath :: Maybe AbsolutePath
- envAnonymousModules :: [(ModuleName, Nat)]
- envImportPath :: [TopLevelModuleName]
- envMutualBlock :: Maybe MutualId
- envTerminationCheck :: TerminationCheck ()
- envCoverageCheck :: CoverageCheck
- envMakeCase :: Bool
- envSolvingConstraints :: Bool
- envCheckingWhere :: Bool
- envWorkingOnTypes :: Bool
- envAssignMetas :: Bool
- envActiveProblems :: Set ProblemId
- envAbstractMode :: AbstractMode
- envModality :: Modality
- envDisplayFormsEnabled :: Bool
- envRange :: Range
- envHighlightingRange :: Range
- envClause :: IPClause
- envCall :: Maybe (Closure Call)
- envHighlightingLevel :: HighlightingLevel
- envHighlightingMethod :: HighlightingMethod
- envModuleNestingLevel :: !Int
- envExpandLast :: ExpandHidden
- envAppDef :: Maybe QName
- envSimplification :: Simplification
- envAllowedReductions :: AllowedReductions
- envInjectivityDepth :: Int
- envCompareBlocked :: Bool
- envPrintDomainFreePi :: Bool
- envPrintMetasBare :: Bool
- envInsideDotPattern :: Bool
- envUnquoteFlags :: UnquoteFlags
- envInstanceDepth :: !Int
- envIsDebugPrinting :: Bool
- envPrintingPatternLambdas :: [QName]
- envCallByNeed :: Bool
- envCurrentCheckpoint :: CheckpointId
- envCheckpoints :: Map CheckpointId Substitution
- envGeneralizeMetas :: DoGeneralize
- envGeneralizedVars :: Map QName GeneralizedValue
- envCheckOptionConsistency :: Bool
- envActiveBackendName :: Maybe BackendName
}
data HighlightingLevel
- = None
- | NonInteractive
- | Interactive
data HighlightingMethod
- = Direct
- | Indirect
data NamedMeta = NamedMeta {
- nmSuggestion :: MetaNameSuggestion
- nmid :: MetaId
}
data TCWarning = TCWarning {
- tcWarningRange :: Range
- tcWarning :: Warning
- tcWarningPrintedWarning :: Doc
- tcWarningCached :: Bool
}
data TCErr
- = TypeError {
  - tcErrState :: TCState
  - tcErrClosErr :: Closure TypeError
  }
- | Exception Range Doc
- | IOException TCState Range IOException
- | PatternErr
data Warning
- = NicifierIssue DeclarationWarning
- | TerminationIssue [TerminationError]
- | UnreachableClauses QName [Range]
- | CoverageIssue QName [(Telescope, [NamedArg DeBruijnPattern])]
- | CoverageNoExactSplit QName [Clause]
- | NotStrictlyPositive QName (Seq OccursWhere)
- | UnsolvedMetaVariables [Range]
- | UnsolvedInteractionMetas [Range]
- | UnsolvedConstraints Constraints
- | CantGeneralizeOverSorts [MetaId]
- | AbsurdPatternRequiresNoRHS [NamedArg DeBruijnPattern]
- | OldBuiltin String String
- | EmptyRewritePragma
- | IllformedAsClause String
- | ClashesViaRenaming NameOrModule [Name]
- | UselessPublic
- | UselessInline QName
- | WrongInstanceDeclaration
- | InstanceWithExplicitArg QName
- | InstanceNoOutputTypeName Doc
- | InstanceArgWithExplicitArg Doc
- | InversionDepthReached QName
- | GenericWarning Doc
- | GenericNonFatalError Doc
- | SafeFlagPostulate Name
- | SafeFlagPragma [String]
- | SafeFlagNonTerminating
- | SafeFlagTerminating
- | SafeFlagWithoutKFlagPrimEraseEquality
- | WithoutKFlagPrimEraseEquality
- | SafeFlagNoPositivityCheck
- | SafeFlagPolarity
- | SafeFlagNoUniverseCheck
- | SafeFlagNoCoverageCheck
- | SafeFlagInjective
- | SafeFlagEta
- | ParseWarning ParseWarning
- | LibraryWarning LibWarning
- | DeprecationWarning String String String
- | UserWarning String
- | FixityInRenamingModule (NonEmpty Range)
- | ModuleDoesntExport QName [ImportedName]
- | InfectiveImport String ModuleName
- | CoInfectiveImport String ModuleName
- | RewriteNonConfluent Term Term Term Doc
- | RewriteMaybeNonConfluent Term Term [Doc]
- | PragmaCompileErased BackendName QName
- | NotInScopeW [QName]
type Verbosity = Trie VerboseKey VerboseLevel
type VerboseLevel = Int
type VerboseKey = String
class (Applicative tcm, MonadIO tcm, MonadTCEnv tcm, MonadTCState tcm, HasOptions tcm) => MonadTCM tcm where
- liftTCM :: TCM a -> tcm a
type IM = TCMT (InputT IO)
class Monad m => MonadTCState m where
- getTC :: m TCState
- putTC :: TCState -> m ()
- modifyTC :: (TCState -> TCState) -> m ()
class Monad m => MonadTCEnv m where
- askTC :: m TCEnv
- localTC :: (TCEnv -> TCEnv) -> m a -> m a
class (Applicative m, MonadTCEnv m, ReadTCState m, HasOptions m) => MonadReduce m where
- liftReduce :: ReduceM a -> m a
newtype ReduceM a = ReduceM {
- unReduceM :: ReduceEnv -> a
}
data ReduceEnv = ReduceEnv {
- redEnv :: TCEnv
- redSt :: TCState
}
class (Functor m, Applicative m, Monad m) => HasOptions m where
- pragmaOptions :: m PragmaOptions
- commandLineOptions :: m CommandLineOptions
data LHSOrPatSyn
- = IsLHS
- | IsPatSyn
data TypeError
- = InternalError String
- | NotImplemented String
- | NotSupported String
- | CompilationError String
- | PropMustBeSingleton
- | DataMustEndInSort Term
- | ShouldEndInApplicationOfTheDatatype Type
- | ShouldBeAppliedToTheDatatypeParameters Term Term
- | ShouldBeApplicationOf Type QName
- | ConstructorPatternInWrongDatatype QName QName
- | CantResolveOverloadedConstructorsTargetingSameDatatype QName [QName]
- | DoesNotConstructAnElementOf QName Type
- | WrongHidingInLHS
- | WrongHidingInLambda Type
- | WrongHidingInApplication Type
- | WrongNamedArgument (NamedArg Expr) [NamedName]
- | WrongIrrelevanceInLambda
- | WrongQuantityInLambda
- | WrongCohesionInLambda
- | QuantityMismatch Quantity Quantity
- | HidingMismatch Hiding Hiding
- | RelevanceMismatch Relevance Relevance
- | UninstantiatedDotPattern Expr
- | ForcedConstructorNotInstantiated Pattern
- | IlltypedPattern Pattern Type
- | IllformedProjectionPattern Pattern
- | CannotEliminateWithPattern (NamedArg Pattern) Type
- | WrongNumberOfConstructorArguments QName Nat Nat
- | ShouldBeEmpty Type [DeBruijnPattern]
- | ShouldBeASort Type
- | ShouldBePi Type
- | ShouldBePath Type
- | ShouldBeRecordType Type
- | ShouldBeRecordPattern DeBruijnPattern
- | NotAProjectionPattern (NamedArg Pattern)
- | NotAProperTerm
- | InvalidTypeSort Sort
- | InvalidType Term
- | FunctionTypeInSizeUniv Term
- | SplitOnIrrelevant (Dom Type)
- | SplitOnUnusableCohesion (Dom Type)
- | SplitOnNonVariable Term Type
- | DefinitionIsIrrelevant QName
- | DefinitionIsErased QName
- | VariableIsIrrelevant Name
- | VariableIsErased Name
- | VariableIsOfUnusableCohesion Name Cohesion
- | UnequalLevel Comparison Level Level
- | UnequalTerms Comparison Term Term CompareAs
- | UnequalTypes Comparison Type Type
- | UnequalRelevance Comparison Term Term
- | UnequalQuantity Comparison Term Term
- | UnequalCohesion Comparison Term Term
- | UnequalHiding Term Term
- | UnequalSorts Sort Sort
- | UnequalBecauseOfUniverseConflict Comparison Term Term
- | NotLeqSort Sort Sort
- | MetaCannotDependOn MetaId Nat
- | MetaOccursInItself MetaId
- | MetaIrrelevantSolution MetaId Term
- | MetaErasedSolution MetaId Term
- | GenericError String
- | GenericDocError Doc
- | BuiltinMustBeConstructor String Expr
- | NoSuchBuiltinName String
- | DuplicateBuiltinBinding String Term Term
- | NoBindingForBuiltin String
- | NoSuchPrimitiveFunction String
- | DuplicatePrimitiveBinding String QName QName
- | ShadowedModule Name [ModuleName]
- | BuiltinInParameterisedModule String
- | IllegalLetInTelescope TypedBinding
- | IllegalPatternInTelescope Binder
- | NoRHSRequiresAbsurdPattern [NamedArg Pattern]
- | TooManyFields QName [Name] [Name]
- | DuplicateFields [Name]
- | DuplicateConstructors [Name]
- | WithOnFreeVariable Expr Term
- | UnexpectedWithPatterns [Pattern]
- | WithClausePatternMismatch Pattern (NamedArg DeBruijnPattern)
- | FieldOutsideRecord
- | ModuleArityMismatch ModuleName Telescope [NamedArg Expr]
- | GeneralizeCyclicDependency
- | GeneralizeUnsolvedMeta
- | SplitError SplitError
- | ImpossibleConstructor QName NegativeUnification
- | TooManyPolarities QName Int
- | LocalVsImportedModuleClash ModuleName
- | SolvedButOpenHoles
- | CyclicModuleDependency [TopLevelModuleName]
- | FileNotFound TopLevelModuleName [AbsolutePath]
- | OverlappingProjects AbsolutePath TopLevelModuleName TopLevelModuleName
- | AmbiguousTopLevelModuleName TopLevelModuleName [AbsolutePath]
- | ModuleNameUnexpected TopLevelModuleName TopLevelModuleName
- | ModuleNameDoesntMatchFileName TopLevelModuleName [AbsolutePath]
- | ClashingFileNamesFor ModuleName [AbsolutePath]
- | ModuleDefinedInOtherFile TopLevelModuleName AbsolutePath AbsolutePath
- | BothWithAndRHS
- | AbstractConstructorNotInScope QName
- | NotInScope [QName]
- | NoSuchModule QName
- | AmbiguousName QName (NonEmpty QName)
- | AmbiguousModule QName (NonEmpty ModuleName)
- | ClashingDefinition QName QName
- | ClashingModule ModuleName ModuleName
- | ClashingImport Name QName
- | ClashingModuleImport Name ModuleName
- | PatternShadowsConstructor Name QName
- | DuplicateImports QName [ImportedName]
- | InvalidPattern Pattern
- | RepeatedVariablesInPattern [Name]
- | GeneralizeNotSupportedHere QName
- | MultipleFixityDecls [(Name, [Fixity'])]
- | MultiplePolarityPragmas [Name]
- | NotAModuleExpr Expr
- | NotAnExpression Expr
- | NotAValidLetBinding NiceDeclaration
- | NotValidBeforeField NiceDeclaration
- | NothingAppliedToHiddenArg Expr
- | NothingAppliedToInstanceArg Expr
- | BadArgumentsToPatternSynonym AmbiguousQName
- | TooFewArgumentsToPatternSynonym AmbiguousQName
- | CannotResolveAmbiguousPatternSynonym (NonEmpty (QName, PatternSynDefn))
- | UnusedVariableInPatternSynonym
- | NoParseForApplication [Expr]
- | AmbiguousParseForApplication [Expr] [Expr]
- | NoParseForLHS LHSOrPatSyn Pattern
- | AmbiguousParseForLHS LHSOrPatSyn Pattern [Pattern]
- | OperatorInformation [NotationSection] TypeError
- | InstanceNoCandidate Type [(Term, TCErr)]
- | UnquoteFailed UnquoteError
- | DeBruijnIndexOutOfScope Nat Telescope [Name]
- | NeedOptionCopatterns
- | NeedOptionRewriting
- | NeedOptionProp
- | NonFatalErrors [TCWarning]
- | InstanceSearchDepthExhausted Term Type Int
- | TriedToCopyConstrainedPrim QName
data UnquoteError
- = BadVisibility String (Arg Term)
- | ConInsteadOfDef QName String String
- | DefInsteadOfCon QName String String
- | NonCanonical String Term
- | BlockedOnMeta TCState MetaId
- | UnquotePanic String
data UnificationFailure
- = UnifyIndicesNotVars Telescope Type Term Term Args
- | UnifyRecursiveEq Telescope Type Int Term
- | UnifyReflexiveEq Telescope Type Term
- | UnifyUnusableModality Telescope Type Int Term Modality
data NegativeUnification
- = UnifyConflict Telescope Term Term
- | UnifyCycle Telescope Int Term
data SplitError
- = NotADatatype (Closure Type)
- | IrrelevantDatatype (Closure Type)
- | ErasedDatatype Bool (Closure Type)
- | CoinductiveDatatype (Closure Type)
- | UnificationStuck {
  - cantSplitConName :: QName
  - cantSplitTel :: Telescope
  - cantSplitConIdx :: Args
  - cantSplitGivenIdx :: Args
  - cantSplitFailures :: [UnificationFailure]
  }
- | CosplitCatchall
- | CosplitNoTarget
- | CosplitNoRecordType (Closure Type)
- | CannotCreateMissingClause QName (Telescope, [NamedArg DeBruijnPattern]) Doc (Closure (Abs Type))
- | GenericSplitError String
data TerminationError = TerminationError {
- termErrFunctions :: [QName]
- termErrCalls :: [CallInfo]
}
data CallInfo = CallInfo {
- callInfoTarget :: QName
- callInfoRange :: Range
- callInfoCall :: Closure Term
}
data Candidate = Candidate {
- candidateTerm :: Term
- candidateType :: Type
- candidateOverlappable :: Bool
}
data ExpandHidden
- = ExpandLast
- | DontExpandLast
- | ReallyDontExpandLast
data AbstractMode
- = AbstractMode
- | ConcreteMode
- | IgnoreAbstractMode
type LetBindings = Map Name (Open (Term, Dom Type))
type ContextEntry = Dom (Name, Type)
type Context = [ContextEntry]
data UnquoteFlags = UnquoteFlags {
- _unquoteNormalise :: Bool
}
class LensTCEnv a where
- lensTCEnv :: Lens' TCEnv a
data Builtin pf
- = Builtin Term
- | Prim pf
type BuiltinThings pf = Map String (Builtin pf)
data BuiltinInfo = BuiltinInfo {
- builtinName :: String
- builtinDesc :: BuiltinDescriptor
}
data BuiltinDescriptor
- = BuiltinData (TCM Type) [String]
- | BuiltinDataCons (TCM Type)
- | BuiltinPrim String (Term -> TCM ())
- | BuiltinPostulate Relevance (TCM Type)
- | BuiltinUnknown (Maybe (TCM Type)) (Term -> Type -> TCM ())
type TempInstanceTable = (InstanceTable, Set QName)
type InstanceTable = Map QName (Set QName)
data Call
- = CheckClause Type SpineClause
- | CheckLHS SpineLHS
- | CheckPattern Pattern Telescope Type
- | CheckLetBinding LetBinding
- | InferExpr Expr
- | CheckExprCall Comparison Expr Type
- | CheckDotPattern Expr Term
- | CheckProjection Range QName Type
- | IsTypeCall Comparison Expr Sort
- | IsType_ Expr
- | InferVar Name
- | InferDef QName
- | CheckArguments Range [NamedArg Expr] Type (Maybe Type)
- | CheckMetaSolution Range MetaId Type Term
- | CheckTargetType Range Type Type
- | CheckDataDef Range QName [LamBinding] [Constructor]
- | CheckRecDef Range QName [LamBinding] [Constructor]
- | CheckConstructor QName Telescope Sort Constructor
- | CheckConstructorFitsIn QName Type Sort
- | CheckFunDefCall Range QName [Clause]
- | CheckPragma Range Pragma
- | CheckPrimitive Range QName Expr
- | CheckIsEmpty Range Type
- | CheckConfluence QName QName
- | CheckWithFunctionType Type
- | CheckSectionApplication Range ModuleName ModuleApplication
- | CheckNamedWhere ModuleName
- | ScopeCheckExpr Expr
- | ScopeCheckDeclaration NiceDeclaration
- | ScopeCheckLHS QName Pattern
- | NoHighlighting
- | ModuleContents
- | SetRange Range
type Statistics = Map String Integer
newtype MutualId = MutId Int32
data TermHead
- = SortHead
- | PiHead
- | ConsHead QName
- | VarHead Nat
- | UnknownHead
data FunctionInverse' c
- = NotInjective
- | Inverse (InversionMap c)
type InversionMap c = Map TermHead [c]
type FunctionInverse = FunctionInverse' Clause
data PrimFun = PrimFun {
- primFunName :: QName
- primFunArity :: Arity
- primFunImplementation :: [Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
}
data PrimitiveImpl = PrimImpl Type PrimFun
type AllowedReductions = SmallSet AllowedReduction
data AllowedReduction
- = ProjectionReductions
- | InlineReductions
- | CopatternReductions
- | FunctionReductions
- | RecursiveReductions
- | LevelReductions
- | TypeLevelReductions
- | UnconfirmedReductions
- | NonTerminatingReductions
type MaybeReducedElims = [MaybeReduced Elim]
type MaybeReducedArgs = [MaybeReduced (Arg Term)]
data MaybeReduced a = MaybeRed {
- isReduced :: IsReduced
- ignoreReduced :: a
}
data IsReduced
- = NotReduced
- | Reduced (Blocked ())
data Reduced no yes
- = NoReduction no
- | YesReduction Simplification yes
data Simplification
- = YesSimplification
- | NoSimplification
newtype Fields = Fields [(Name, Type)]
data Defn
- = Axiom
- | DataOrRecSig {
  - datarecPars :: Int
  }
- | GeneralizableVar
- | AbstractDefn Defn
- | Function {
  - funClauses :: [Clause]
  - funCompiled :: Maybe CompiledClauses
  - funSplitTree :: Maybe SplitTree
  - funTreeless :: Maybe Compiled
  - funCovering :: [Clause]
  - funInv :: FunctionInverse
  - funMutual :: Maybe [QName]
  - funAbstr :: IsAbstract
  - funDelayed :: Delayed
  - funProjection :: Maybe Projection
  - funFlags :: Set FunctionFlag
  - funTerminates :: Maybe Bool
  - funExtLam :: Maybe ExtLamInfo
  - funWith :: Maybe QName
  }
- | Datatype {
  - dataPars :: Nat
  - dataIxs :: Nat
  - dataClause :: Maybe Clause
  - dataCons :: [QName]
  - dataSort :: Sort
  - dataMutual :: Maybe [QName]
  - dataAbstr :: IsAbstract
  - dataPathCons :: [QName]
  }
- | Record {
  - recPars :: Nat
  - recClause :: Maybe Clause
  - recConHead :: ConHead
  - recNamedCon :: Bool
  - recFields :: [Dom QName]
  - recTel :: Telescope
  - recMutual :: Maybe [QName]
  - recEtaEquality' :: EtaEquality
  - recInduction :: Maybe Induction
  - recAbstr :: IsAbstract
  - recComp :: CompKit
  }
- | Constructor {
  - conPars :: Int
  - conArity :: Int
  - conSrcCon :: ConHead
  - conData :: QName
  - conAbstr :: IsAbstract
  - conInd :: Induction
  - conComp :: CompKit
  - conProj :: Maybe [QName]
  - conForced :: [IsForced]
  - conErased :: Maybe [Bool]
  }
- | Primitive {
  - primAbstr :: IsAbstract
  - primName :: String
  - primClauses :: [Clause]
  - primInv :: FunctionInverse
  - primCompiled :: Maybe CompiledClauses
  }
data CompKit = CompKit {
- nameOfHComp :: Maybe QName
- nameOfTransp :: Maybe QName
}
data FunctionFlag
- = FunStatic
- | FunInline
- | FunMacro
data EtaEquality
- = Specified {
  - theEtaEquality :: !HasEta
  }
- | Inferred {
  - theEtaEquality :: !HasEta
  }
newtype ProjLams = ProjLams {
- getProjLams :: [Arg ArgName]
}
data Projection = Projection {
- projProper :: Maybe QName
- projOrig :: QName
- projFromType :: Arg QName
- projIndex :: Int
- projLams :: ProjLams
}
data ExtLamInfo = ExtLamInfo {
- extLamModule :: ModuleName
- extLamSys :: !(Maybe System)
}
data System = System {
- systemTel :: Telescope
- systemClauses :: [(Face, Term)]
}
type Face = [(Term, Bool)]
type CompiledRepresentation = Map BackendName [CompilerPragma]
data CompilerPragma = CompilerPragma Range String
data IsForced
- = Forced
- | NotForced
data NumGeneralizableArgs
- = NoGeneralizableArgs
- | SomeGeneralizableArgs Int
data Definition = Defn {
- defArgInfo :: ArgInfo
- defName :: QName
- defType :: Type
- defPolarity :: [Polarity]
- defArgOccurrences :: [Occurrence]
- defArgGeneralizable :: NumGeneralizableArgs
- defGeneralizedParams :: [Maybe Name]
- defDisplay :: [LocalDisplayForm]
- defMutual :: MutualId
- defCompiledRep :: CompiledRepresentation
- defInstance :: Maybe QName
- defCopy :: Bool
- defMatchable :: Set QName
- defNoCompilation :: Bool
- defInjective :: Bool
- defCopatternLHS :: Bool
- defBlocked :: Blocked_
- theDef :: Defn
}
data RewriteRule = RewriteRule {
- rewName :: QName
- rewContext :: Telescope
- rewHead :: QName
- rewPats :: PElims
- rewRHS :: Term
- rewType :: Type
}
type RewriteRules = [RewriteRule]
data NLPSort
- = PType NLPat
- | PProp NLPat
- | PInf
- | PSizeUniv
data NLPType = NLPType {
- nlpTypeSort :: NLPSort
- nlpTypeUnEl :: NLPat
}
type PElims = [Elim' NLPat]
data NLPat
- = PVar !Int [Arg Int]
- | PDef QName PElims
- | PLam ArgInfo (Abs NLPat)
- | PPi (Dom NLPType) (Abs NLPType)
- | PSort NLPSort
- | PBoundVar !Int PElims
- | PTerm Term
data DisplayTerm
- = DWithApp DisplayTerm [DisplayTerm] Elims
- | DCon ConHead ConInfo [Arg DisplayTerm]
- | DDef QName [Elim' DisplayTerm]
- | DDot Term
- | DTerm Term
type LocalDisplayForm = Open DisplayForm
data DisplayForm = Display {
- dfFreeVars :: Nat
- dfPats :: Elims
- dfRHS :: DisplayTerm
}
newtype Section = Section {
- _secTelescope :: Telescope
}
type DisplayForms = HashMap QName [LocalDisplayForm]
type RewriteRuleMap = HashMap QName RewriteRules
type Definitions = HashMap QName Definition
type Sections = Map ModuleName Section
data Signature = Sig {
- _sigSections :: Sections
- _sigDefinitions :: Definitions
- _sigRewriteRules :: RewriteRuleMap
}
data IPClause
- = IPClause {
  - ipcQName :: QName
  - ipcClauseNo :: Int
  - ipcType :: Type
  - ipcWithSub :: Maybe Substitution
  - ipcClause :: SpineClause
  - ipcClosure :: Closure ()
  - ipcBoundary :: [Closure IPBoundary]
  }
- | IPNoClause
type IPBoundary = IPBoundary' Term
data IPBoundary' t = IPBoundary {
- ipbEquations :: [(t, t)]
- ipbValue :: t
- ipbMetaApp :: t
- ipbOverapplied :: Overapplied
}
data Overapplied
- = Overapplied
- | NotOverapplied
type InteractionPoints = Map InteractionId InteractionPoint
data InteractionPoint = InteractionPoint {
- ipRange :: Range
- ipMeta :: Maybe MetaId
- ipSolved :: Bool
- ipClause :: IPClause
}
type MetaStore = IntMap MetaVariable
type MetaNameSuggestion = String
data MetaInfo = MetaInfo {
- miClosRange :: Closure Range
- miMetaOccursCheck :: RunMetaOccursCheck
- miNameSuggestion :: MetaNameSuggestion
- miGeneralizable :: Arg DoGeneralize
}
data RunMetaOccursCheck
- = RunMetaOccursCheck
- | DontRunMetaOccursCheck
newtype MetaPriority = MetaPriority Int
data TypeCheckingProblem
- = CheckExpr Comparison Expr Type
- | CheckArgs ExpandHidden Range [NamedArg Expr] Type Type ([Maybe Range] -> Elims -> Type -> CheckedTarget -> TCM Term)
- | CheckProjAppToKnownPrincipalArg Comparison Expr ProjOrigin (NonEmpty QName) Args Type Int Term Type
- | CheckLambda Comparison (Arg ([WithHiding Name], Maybe Type)) Expr Type
- | DoQuoteTerm Comparison Term Type
data CheckedTarget
- = CheckedTarget (Maybe ProblemId)
- | NotCheckedTarget
data MetaInstantiation
- = InstV [Arg String] Term
- | Open
- | OpenInstance
- | BlockedConst Term
- | PostponedTypeCheckingProblem (Closure TypeCheckingProblem) (TCM Bool)
data Frozen
- = Frozen
- | Instantiable
data Listener
- = EtaExpand MetaId
- | CheckConstraint Nat ProblemConstraint
data MetaVariable = MetaVar {
- mvInfo :: MetaInfo
- mvPriority :: MetaPriority
- mvPermutation :: Permutation
- mvJudgement :: Judgement MetaId
- mvInstantiation :: MetaInstantiation
- mvListeners :: Set Listener
- mvFrozen :: Frozen
- mvTwin :: Maybe MetaId
}
data GeneralizedValue = GeneralizedValue {
- genvalCheckpoint :: CheckpointId
- genvalTerm :: Term
- genvalType :: Type
}
data DoGeneralize
- = YesGeneralize
- | NoGeneralize
data Judgement a
- = HasType {
  - jMetaId :: a
  - jComparison :: Comparison
  - jMetaType :: Type
  }
- | IsSort {
  - jMetaId :: a
  - jMetaType :: Type
  }
data Open a = OpenThing {
- openThingCheckpoint :: CheckpointId
- openThing :: a
}
data CompareAs
- = AsTermsOf Type
- | AsSizes
- | AsTypes
data CompareDirection
- = DirEq
- | DirLeq
- | DirGeq
data Constraint
- = ValueCmp Comparison CompareAs Term Term
- | ValueCmpOnFace Comparison Term Type Term Term
- | ElimCmp [Polarity] [IsForced] Type Term [Elim] [Elim]
- | TelCmp Type Type Comparison Telescope Telescope
- | SortCmp Comparison Sort Sort
- | LevelCmp Comparison Level Level
- | HasBiggerSort Sort
- | HasPTSRule (Dom Type) (Abs Sort)
- | CheckMetaInst MetaId
- | UnBlock MetaId
- | Guarded Constraint ProblemId
- | IsEmpty Range Type
- | CheckSizeLtSat Term
- | FindInstance MetaId (Maybe MetaId) (Maybe [Candidate])
- | CheckFunDef Delayed DefInfo QName [Clause]
- | UnquoteTactic (Maybe MetaId) Term Term Type
data ProblemConstraint = PConstr {
- constraintProblems :: Set ProblemId
- theConstraint :: Closure Constraint
}
type Constraints = [ProblemConstraint]
class LensClosure a b | b -> a where
- lensClosure :: Lens' (Closure a) b
data Closure a = Closure {
- clSignature :: Signature
- clEnv :: TCEnv
- clScope :: ScopeInfo
- clModuleCheckpoints :: Map ModuleName CheckpointId
- clValue :: a
}
data Interface = Interface {
- iSourceHash :: Hash
- iSource :: Text
- iFileType :: FileType
- iImportedModules :: [(ModuleName, Hash)]
- iModuleName :: ModuleName
- iScope :: Map ModuleName Scope
- iInsideScope :: ScopeInfo
- iSignature :: Signature
- iDisplayForms :: DisplayForms
- iUserWarnings :: Map QName String
- iImportWarning :: Maybe String
- iBuiltin :: BuiltinThings (String, QName)
- iForeignCode :: Map BackendName [ForeignCode]
- iHighlighting :: HighlightingInfo
- iPragmaOptions :: [OptionsPragma]
- iOptionsUsed :: PragmaOptions
- iPatternSyns :: PatternSynDefns
- iWarnings :: [TCWarning]
- iPartialDefs :: Set QName
}
data ForeignCode = ForeignCode Range String
type DecodedModules = Map TopLevelModuleName Interface
type VisitedModules = Map TopLevelModuleName ModuleInfo
data ModuleInfo = ModuleInfo {
- miInterface :: Interface
- miWarnings :: Bool
- miPrimitive :: Bool
}
class Monad m => MonadStConcreteNames m where
- runStConcreteNames :: StateT ConcreteNames m a -> m a
- useConcreteNames :: m ConcreteNames
- modifyConcreteNames :: (ConcreteNames -> ConcreteNames) -> m ()
type SourceToModule = Map AbsolutePath TopLevelModuleName
class FreshName a where
- freshName_ :: MonadFresh NameId m => a -> m Name
newtype CheckpointId = CheckpointId Int
class Monad m => MonadFresh i m where
- fresh :: m i
class Enum i => HasFresh i where
- freshLens :: Lens' i TCState
- nextFresh' :: i -> i
data TypeCheckAction
- = EnterSection !ModuleInfo !ModuleName !Telescope
- | LeaveSection !ModuleName
- | Decl !Declaration
- | Pragmas !PragmaOptions
type CurrentTypeCheckLog = [(TypeCheckAction, PostScopeState)]
type CachedTypeCheckLog = [(TypeCheckAction, PostScopeState)]
data LoadedFileCache = LoadedFileCache {
- lfcCached :: !CachedTypeCheckLog
- lfcCurrent :: !CurrentTypeCheckLog
}
data PersistentTCState = PersistentTCSt {
- stDecodedModules :: DecodedModules
- stPersistentOptions :: CommandLineOptions
- stInteractionOutputCallback :: InteractionOutputCallback
- stBenchmark :: !Benchmark
- stAccumStatistics :: !Statistics
- stPersistLoadedFileCache :: !(Maybe LoadedFileCache)
- stPersistBackends :: [Backend]
}
data MutualBlock = MutualBlock {
- mutualInfo :: MutualInfo
- mutualNames :: Set QName
}
data PostScopeState = PostScopeState {
- stPostSyntaxInfo :: !CompressedFile
- stPostDisambiguatedNames :: !DisambiguatedNames
- stPostMetaStore :: !MetaStore
- stPostInteractionPoints :: !InteractionPoints
- stPostAwakeConstraints :: !Constraints
- stPostSleepingConstraints :: !Constraints
- stPostDirty :: !Bool
- stPostOccursCheckDefs :: !(Set QName)
- stPostSignature :: !Signature
- stPostModuleCheckpoints :: !(Map ModuleName CheckpointId)
- stPostImportsDisplayForms :: !DisplayForms
- stPostCurrentModule :: !(Maybe ModuleName)
- stPostInstanceDefs :: !TempInstanceTable
- stPostConcreteNames :: !ConcreteNames
- stPostUsedNames :: !(Map RawName [RawName])
- stPostShadowingNames :: !(Map Name [RawName])
- stPostStatistics :: !Statistics
- stPostTCWarnings :: ![TCWarning]
- stPostMutualBlocks :: !(Map MutualId MutualBlock)
- stPostLocalBuiltins :: !(BuiltinThings PrimFun)
- stPostFreshMetaId :: !MetaId
- stPostFreshMutualId :: !MutualId
- stPostFreshProblemId :: !ProblemId
- stPostFreshCheckpointId :: !CheckpointId
- stPostFreshInt :: !Int
- stPostFreshNameId :: !NameId
- stPostAreWeCaching :: !Bool
- stPostPostponeInstanceSearch :: !Bool
- stPostConsideringInstance :: !Bool
- stPostInstantiateBlocking :: !Bool
- stPostLocalPartialDefs :: !(Set QName)
}
type ConcreteNames = Map Name [Name]
type DisambiguatedNames = IntMap QName
data PreScopeState = PreScopeState {
- stPreTokens :: !CompressedFile
- stPreImports :: !Signature
- stPreImportedModules :: !(Set ModuleName)
- stPreModuleToSource :: !ModuleToSource
- stPreVisitedModules :: !VisitedModules
- stPreScope :: !ScopeInfo
- stPrePatternSyns :: !PatternSynDefns
- stPrePatternSynImports :: !PatternSynDefns
- stPreGeneralizedVars :: !(Maybe (Set QName))
- stPrePragmaOptions :: !PragmaOptions
- stPreImportedBuiltins :: !(BuiltinThings PrimFun)
- stPreImportedDisplayForms :: !DisplayForms
- stPreImportedInstanceDefs :: !InstanceTable
- stPreForeignCode :: !(Map BackendName [ForeignCode])
- stPreFreshInteractionId :: !InteractionId
- stPreImportedUserWarnings :: !(Map QName String)
- stPreLocalUserWarnings :: !(Map QName String)
- stPreWarningOnImport :: !(Maybe String)
- stPreImportedPartialDefs :: !(Set QName)
}
class Monad m => ReadTCState m where
- getTCState :: m TCState
- locallyTCState :: Lens' a TCState -> (a -> a) -> m b -> m b
- withTCState :: (TCState -> TCState) -> m a -> m a
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
stGeneralizedVars :: Lens' (Maybe (Set QName)) TCState
stPragmaOptions :: Lens' PragmaOptions TCState
stImportedBuiltins :: Lens' (BuiltinThings PrimFun) TCState
stForeignCode :: Lens' (Map BackendName [ForeignCode]) TCState
stFreshInteractionId :: Lens' InteractionId TCState
stImportedUserWarnings :: Lens' (Map QName String) TCState
stLocalUserWarnings :: Lens' (Map QName String) TCState
getUserWarnings :: ReadTCState m => m (Map QName String)
stWarningOnImport :: Lens' (Maybe String) TCState
stImportedPartialDefs :: Lens' (Set QName) TCState
stLocalPartialDefs :: Lens' (Set QName) TCState
getPartialDefs :: ReadTCState m => m (Set QName)
stLoadedFileCache :: Lens' (Maybe LoadedFileCache) TCState
stBackends :: Lens' [Backend] 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
stModuleCheckpoints :: Lens' (Map ModuleName CheckpointId) TCState
stImportsDisplayForms :: Lens' DisplayForms TCState
stImportedDisplayForms :: Lens' DisplayForms TCState
stCurrentModule :: Lens' (Maybe ModuleName) TCState
stImportedInstanceDefs :: Lens' InstanceTable TCState
stInstanceDefs :: Lens' TempInstanceTable TCState
stConcreteNames :: Lens' ConcreteNames TCState
stUsedNames :: Lens' (Map RawName [RawName]) TCState
stShadowingNames :: Lens' (Map Name [RawName]) TCState
stStatistics :: Lens' Statistics TCState
stTCWarnings :: Lens' [TCWarning] TCState
stMutualBlocks :: Lens' (Map MutualId MutualBlock) TCState
stLocalBuiltins :: Lens' (BuiltinThings PrimFun) TCState
stFreshMetaId :: Lens' MetaId TCState
stFreshMutualId :: Lens' MutualId TCState
stFreshProblemId :: Lens' ProblemId TCState
stFreshCheckpointId :: Lens' CheckpointId TCState
stFreshInt :: Lens' Int TCState
stAreWeCaching :: Lens' Bool TCState
stPostponeInstanceSearch :: Lens' Bool TCState
stConsideringInstance :: Lens' Bool TCState
stInstantiateBlocking :: Lens' Bool TCState
stBuiltinThings :: TCState -> BuiltinThings PrimFun
nextFresh :: HasFresh i => TCState -> (i, TCState)
freshName :: MonadFresh NameId m => Range -> String -> m Name
freshNoName :: MonadFresh NameId m => Range -> m Name
freshNoName_ :: MonadFresh NameId m => m Name
freshRecordName :: MonadFresh NameId m => m Name
sourceToModule :: TCM SourceToModule
lookupModuleFromSource :: ReadTCState m => AbsolutePath -> m (Maybe TopLevelModuleName)
iFullHash :: Interface -> Hash
buildClosure :: (MonadTCEnv m, ReadTCState m) => a -> m (Closure a)
fromCmp :: Comparison -> CompareDirection
flipCmp :: CompareDirection -> CompareDirection
dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c
normalMetaPriority :: MetaPriority
lowMetaPriority :: MetaPriority
highMetaPriority :: MetaPriority
getMetaInfo :: MetaVariable -> Closure Range
getMetaScope :: MetaVariable -> ScopeInfo
getMetaEnv :: MetaVariable -> TCEnv
getMetaSig :: MetaVariable -> Signature
getMetaRelevance :: MetaVariable -> Relevance
getMetaModality :: MetaVariable -> Modality
metaFrozen :: Lens' Frozen MetaVariable
_mvInfo :: Lens' MetaInfo MetaVariable
sigSections :: Lens' Sections Signature
sigDefinitions :: Lens' Definitions Signature
sigRewriteRules :: Lens' RewriteRuleMap Signature
secTelescope :: Lens' Telescope Section
emptySignature :: Signature
defaultDisplayForm :: QName -> [LocalDisplayForm]
theDefLens :: Lens' Defn Definition
defaultDefn :: ArgInfo -> QName -> Type -> Defn -> Definition
jsBackendName :: BackendName
ghcBackendName :: BackendName
noCompiledRep :: CompiledRepresentation
modifySystem :: (System -> System) -> ExtLamInfo -> ExtLamInfo
projDropPars :: Projection -> ProjOrigin -> Term
projArgInfo :: Projection -> ArgInfo
setEtaEquality :: EtaEquality -> HasEta -> EtaEquality
emptyCompKit :: CompKit
recRecursive :: Defn -> Bool
recEtaEquality :: Defn -> HasEta
emptyFunction :: Defn
funFlag :: FunctionFlag -> Lens' Bool Defn
funStatic :: Lens' Bool Defn
funInline :: Lens' Bool Defn
funMacro :: Lens' Bool Defn
isMacro :: Defn -> Bool
isEmptyFunction :: Defn -> Bool
isCopatternLHS :: [Clause] -> Bool
recCon :: Defn -> QName
defIsRecord :: Defn -> Bool
defIsDataOrRecord :: Defn -> Bool
defConstructors :: Defn -> [QName]
redReturn :: a -> ReduceM (Reduced a' a)
redBind :: ReduceM (Reduced a a') -> (a -> b) -> (a' -> ReduceM (Reduced b b')) -> ReduceM (Reduced b b')
notReduced :: a -> MaybeReduced a
reduced :: Blocked (Arg Term) -> MaybeReduced (Arg Term)
allReductions :: AllowedReductions
reallyAllReductions :: AllowedReductions
primFun :: QName -> Arity -> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term)) -> PrimFun
defClauses :: Definition -> [Clause]
defCompiled :: Definition -> Maybe CompiledClauses
defParameters :: Definition -> Maybe Nat
defInverse :: Definition -> FunctionInverse
defCompilerPragmas :: BackendName -> Definition -> [CompilerPragma]
defDelayed :: Definition -> Delayed
defNonterminating :: Definition -> Bool
defTerminationUnconfirmed :: Definition -> Bool
defAbstract :: Definition -> IsAbstract
defForced :: Definition -> [IsForced]
ifTopLevelAndHighlightingLevelIsOr :: MonadTCM tcm => HighlightingLevel -> Bool -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs :: MonadTCM tcm => HighlightingLevel -> tcm () -> tcm ()
initEnv :: TCEnv
defaultUnquoteFlags :: UnquoteFlags
unquoteNormalise :: Lens' Bool UnquoteFlags
eUnquoteNormalise :: Lens' Bool TCEnv
eContext :: Lens' Context TCEnv
eLetBindings :: Lens' LetBindings TCEnv
eCurrentModule :: Lens' ModuleName TCEnv
eCurrentPath :: Lens' (Maybe AbsolutePath) TCEnv
eAnonymousModules :: Lens' [(ModuleName, Nat)] TCEnv
eImportPath :: Lens' [TopLevelModuleName] TCEnv
eMutualBlock :: Lens' (Maybe MutualId) TCEnv
eTerminationCheck :: Lens' (TerminationCheck ()) TCEnv
eCoverageCheck :: Lens' CoverageCheck TCEnv
eMakeCase :: Lens' Bool TCEnv
eSolvingConstraints :: Lens' Bool TCEnv
eCheckingWhere :: Lens' Bool TCEnv
eWorkingOnTypes :: Lens' Bool TCEnv
eAssignMetas :: Lens' Bool TCEnv
eActiveProblems :: Lens' (Set ProblemId) TCEnv
eAbstractMode :: Lens' AbstractMode TCEnv
eModality :: Lens' Modality TCEnv
eRelevance :: Lens' Relevance TCEnv
eQuantity :: Lens' Quantity TCEnv
eDisplayFormsEnabled :: Lens' Bool TCEnv
eRange :: Lens' Range TCEnv
eHighlightingRange :: Lens' Range TCEnv
eCall :: Lens' (Maybe (Closure Call)) TCEnv
eHighlightingLevel :: Lens' HighlightingLevel TCEnv
eHighlightingMethod :: Lens' HighlightingMethod TCEnv
eModuleNestingLevel :: Lens' Int TCEnv
eExpandLast :: Lens' ExpandHidden TCEnv
eAppDef :: Lens' (Maybe QName) TCEnv
eSimplification :: Lens' Simplification TCEnv
eAllowedReductions :: Lens' AllowedReductions TCEnv
eInjectivityDepth :: Lens' Int TCEnv
eCompareBlocked :: Lens' Bool TCEnv
ePrintDomainFreePi :: Lens' Bool TCEnv
eInsideDotPattern :: Lens' Bool TCEnv
eUnquoteFlags :: Lens' UnquoteFlags TCEnv
eInstanceDepth :: Lens' Int TCEnv
eIsDebugPrinting :: Lens' Bool TCEnv
ePrintingPatternLambdas :: Lens' [QName] TCEnv
eCallByNeed :: Lens' Bool TCEnv
eCurrentCheckpoint :: Lens' CheckpointId TCEnv
eCheckpoints :: Lens' (Map CheckpointId Substitution) TCEnv
eGeneralizeMetas :: Lens' DoGeneralize TCEnv
eGeneralizedVars :: Lens' (Map QName GeneralizedValue) TCEnv
eActiveBackendName :: Lens' (Maybe BackendName) TCEnv
aDefToMode :: IsAbstract -> AbstractMode
aModeToDef :: AbstractMode -> Maybe IsAbstract
isDontExpandLast :: ExpandHidden -> Bool
warningName :: Warning -> WarningName
tcWarningOrigin :: TCWarning -> SrcFile
sizedTypesOption :: HasOptions m => m Bool
guardednessOption :: HasOptions m => m Bool
withoutKOption :: HasOptions m => m Bool
getIncludeDirs :: HasOptions m => m [AbsolutePath]
enableCaching :: HasOptions m => m Bool
mapRedEnv :: (TCEnv -> TCEnv) -> ReduceEnv -> ReduceEnv
mapRedSt :: (TCState -> TCState) -> ReduceEnv -> ReduceEnv
mapRedEnvSt :: (TCEnv -> TCEnv) -> (TCState -> TCState) -> ReduceEnv -> ReduceEnv
reduceEnv :: Lens' TCEnv ReduceEnv
reduceSt :: Lens' TCState ReduceEnv
onReduceEnv :: (ReduceEnv -> ReduceEnv) -> ReduceM a -> ReduceM a
fmapReduce :: (a -> b) -> ReduceM a -> ReduceM b
apReduce :: ReduceM (a -> b) -> ReduceM a -> ReduceM b
bindReduce :: ReduceM a -> (a -> ReduceM b) -> ReduceM b
runReduceM :: ReduceM a -> TCM a
runReduceF :: (a -> ReduceM b) -> TCM (a -> b)
useR :: ReadTCState m => Lens' a TCState -> m a
askR :: ReduceM ReduceEnv
localR :: (ReduceEnv -> ReduceEnv) -> ReduceM a -> ReduceM a
asksTC :: MonadTCEnv m => (TCEnv -> a) -> m a
viewTC :: MonadTCEnv m => Lens' a TCEnv -> m a
locallyTC :: MonadTCEnv m => Lens' a TCEnv -> (a -> a) -> m b -> m b
getsTC :: ReadTCState m => (TCState -> a) -> m a
modifyTC' :: MonadTCState m => (TCState -> TCState) -> m ()
useTC :: ReadTCState m => Lens' a TCState -> m a
setTCLens :: MonadTCState m => Lens' a TCState -> a -> m ()
modifyTCLens :: MonadTCState m => Lens' a TCState -> (a -> a) -> m ()
modifyTCLensM :: MonadTCState m => Lens' a TCState -> (a -> m a) -> m ()
stateTCLens :: MonadTCState m => Lens' a TCState -> (a -> (r, a)) -> m r
stateTCLensM :: MonadTCState m => Lens' a TCState -> (a -> m (r, a)) -> m r
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
runIM :: IM a -> TCM a
catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a
finally_ :: TCM a -> TCM b -> TCM a
patternViolation :: MonadError TCErr m => m a
internalError :: MonadTCM tcm => String -> tcm a
genericError :: (MonadTCEnv m, ReadTCState m, MonadError TCErr m) => String -> m a
genericDocError :: (MonadTCEnv m, ReadTCState m, MonadError TCErr m) => Doc -> m a
typeError :: (MonadTCEnv m, ReadTCState m, MonadError TCErr m) => TypeError -> m a
typeError_ :: (MonadTCEnv m, ReadTCState m) => TypeError -> m 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 ()
patternInTeleName :: String
extendedLambdaName :: String
isExtendedLambdaName :: QName -> Bool
absurdLambdaName :: String
isAbsurdLambdaName :: QName -> Bool
generalizedFieldName :: String
getGeneralizedFieldName :: QName -> Maybe String
class (MonadTCEnv m, ReadTCState m) => MonadInteractionPoints m where
- freshInteractionId :: m InteractionId
- modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> m ()
addImport :: ModuleName -> TCM ()
addImportCycleCheck :: TopLevelModuleName -> TCM a -> TCM a
getImports :: TCM (Set ModuleName)
isImported :: ModuleName -> TCM Bool
getImportPath :: TCM [TopLevelModuleName]
visitModule :: ModuleInfo -> TCM ()
setVisitedModules :: VisitedModules -> TCM ()
getVisitedModules :: TCM VisitedModules
isVisited :: TopLevelModuleName -> TCM Bool
getVisitedModule :: TopLevelModuleName -> TCM (Maybe ModuleInfo)
mapVisitedModule :: TopLevelModuleName -> (ModuleInfo -> ModuleInfo) -> TCM ()
getDecodedModules :: TCM DecodedModules
setDecodedModules :: DecodedModules -> TCM ()
getDecodedModule :: TopLevelModuleName -> TCM (Maybe Interface)
storeDecodedModule :: Interface -> TCM ()
dropDecodedModule :: TopLevelModuleName -> TCM ()
withImportPath :: [TopLevelModuleName] -> TCM a -> TCM a
checkForImportCycle :: TCM ()
currentModule :: MonadTCEnv m => m ModuleName
withCurrentModule :: MonadTCEnv m => ModuleName -> m a -> m a
getCurrentPath :: MonadTCEnv m => m AbsolutePath
getAnonymousVariables :: MonadTCEnv m => ModuleName -> m Nat
withAnonymousModule :: ModuleName -> Nat -> TCM a -> TCM a
withEnv :: MonadTCEnv m => TCEnv -> m a -> m a
getEnv :: TCM TCEnv
withIncreasedModuleNestingLevel :: TCM a -> TCM a
withHighlightingLevel :: HighlightingLevel -> TCM a -> TCM a
withoutOptionsChecking :: TCM a -> TCM a
doExpandLast :: TCM a -> TCM a
dontExpandLast :: TCM a -> TCM a
reallyDontExpandLast :: TCM a -> TCM a
performedSimplification :: MonadTCEnv m => m a -> m a
performedSimplification' :: MonadTCEnv m => Simplification -> m a -> m a
getSimplification :: MonadTCEnv m => m Simplification
updateAllowedReductions :: (AllowedReductions -> AllowedReductions) -> TCEnv -> TCEnv
modifyAllowedReductions :: MonadTCEnv m => (AllowedReductions -> AllowedReductions) -> m a -> m a
putAllowedReductions :: MonadTCEnv m => AllowedReductions -> m a -> m a
onlyReduceProjections :: MonadTCEnv m => m a -> m a
allowAllReductions :: MonadTCEnv m => m a -> m a
allowNonTerminatingReductions :: MonadTCEnv m => m a -> m a
onlyReduceTypes :: MonadTCEnv m => m a -> m a
typeLevelReductions :: MonadTCEnv m => m a -> m a
insideDotPattern :: TCM a -> TCM a
isInsideDotPattern :: TCM Bool
callByName :: TCM a -> TCM a
class MonadTCEnv m => MonadAddContext m where
- addCtx :: Name -> Dom Type -> m a -> m a
- addLetBinding' :: Name -> Term -> Dom Type -> m a -> m a
- updateContext :: Substitution -> (Context -> Context) -> m a -> m a
- withFreshName :: Range -> ArgName -> (Name -> m a) -> m a
checkpointSubstitution :: MonadTCEnv tcm => CheckpointId -> tcm Substitution
class (Functor m, Applicative m, MonadFail m) => HasBuiltins m where
- getBuiltinThing :: String -> m (Maybe (Builtin PrimFun))
class TraceS a where
- traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> a -> m c -> m c
class ReportS a where
- reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> a -> m ()
class (Functor m, Applicative m, Monad m) => MonadDebug m where
- displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> m ()
- traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> m a -> m a
- formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> m String
- getVerbosity :: m Verbosity
- isDebugPrinting :: m Bool
- nowDebugPrinting :: m a -> m a
- verboseBracket :: VerboseKey -> VerboseLevel -> String -> m a -> m a
catchAndPrintImpossible :: (CatchImpossible m, Monad m) => VerboseKey -> VerboseLevel -> m String -> m String
reportSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()
__IMPOSSIBLE_VERBOSE__ :: (HasCallStack, MonadDebug m) => String -> m a
reportSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportResult :: MonadDebug m => VerboseKey -> VerboseLevel -> (a -> TCM Doc) -> m a -> m a
unlessDebugPrinting :: MonadDebug m => m () -> m ()
traceSLn :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m a -> m a
traceSDoc :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m a -> m a
openVerboseBracket :: MonadDebug m => VerboseKey -> VerboseLevel -> String -> m ()
closeVerboseBracket :: MonadDebug m => VerboseKey -> VerboseLevel -> m ()
parseVerboseKey :: VerboseKey -> [String]
hasVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m Bool
hasExactVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m Bool
whenExactVerbosity :: MonadDebug m => VerboseKey -> VerboseLevel -> m () -> m ()
__CRASH_WHEN__ :: (HasCallStack, MonadTCM m, MonadDebug m) => VerboseKey -> VerboseLevel -> m ()
verboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> m () -> m ()
applyWhenVerboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
verbosity :: VerboseKey -> Lens' VerboseLevel TCState
class ReadTCState m => MonadStatistics m where
- modifyCounter :: String -> (Integer -> Integer) -> m ()
getStatistics :: ReadTCState m => m Statistics
modifyStatistics :: (Statistics -> Statistics) -> TCM ()
tick :: MonadStatistics m => String -> m ()
tickN :: MonadStatistics m => String -> Integer -> m ()
tickMax :: MonadStatistics m => String -> Integer -> m ()
printStatistics :: (MonadDebug m, MonadTCEnv m, HasOptions m) => Int -> Maybe TopLevelModuleName -> Statistics -> m ()
class (Functor m, Applicative m, MonadFail m, HasOptions m, MonadDebug m, MonadTCEnv m) => HasConstInfo m where
- getConstInfo :: QName -> m Definition
- getConstInfo' :: QName -> m (Either SigError Definition)
- getRewriteRulesFor :: QName -> m RewriteRules
data SigError
- = SigUnknown String
- | SigAbstract
lookupSection :: (Functor m, ReadTCState m) => ModuleName -> m Telescope
inFreshModuleIfFreeParams :: TCM a -> TCM a
cachingStarts :: (MonadTCState m, ReadTCState m) => m ()
areWeCaching :: ReadTCState m => m Bool
writeToCurrentLog :: (MonadDebug m, MonadTCState m, ReadTCState m) => TypeCheckAction -> m ()
restorePostScopeState :: (MonadDebug m, MonadTCState m) => PostScopeState -> m ()
localCache :: (MonadTCState m, ReadTCState m) => m a -> m a
withoutCache :: (MonadTCState m, ReadTCState m) => m a -> m a
readFromCachedLog :: (MonadDebug m, MonadTCState m, ReadTCState m) => m (Maybe (TypeCheckAction, PostScopeState))
cleanCachedLog :: (MonadDebug m, MonadTCState m) => m ()
activateLoadedFileCache :: (HasOptions m, MonadDebug m, MonadTCState m) => m ()
cacheCurrentLog :: (MonadDebug m, MonadTCState m) => m ()
data SpeculateResult
- = SpeculateAbort
- | SpeculateCommit
resetState :: TCM ()
resetAllState :: TCM ()
localTCState :: TCM a -> TCM a
localTCStateSaving :: TCM a -> TCM (a, TCState)
localTCStateSavingWarnings :: TCM a -> TCM a
speculateTCState :: TCM (a, SpeculateResult) -> TCM a
speculateTCState_ :: TCM SpeculateResult -> TCM ()
freshTCM :: TCM a -> TCM (Either TCErr a)
lensPersistentState :: Lens' PersistentTCState TCState
updatePersistentState :: (PersistentTCState -> PersistentTCState) -> TCState -> TCState
modifyPersistentState :: (PersistentTCState -> PersistentTCState) -> TCM ()
lensAccumStatisticsP :: Lens' Statistics PersistentTCState
lensAccumStatistics :: Lens' Statistics TCState
getScope :: ReadTCState m => m ScopeInfo
setScope :: ScopeInfo -> TCM ()
modifyScope_ :: MonadTCState m => (ScopeInfo -> ScopeInfo) -> m ()
modifyScope :: MonadTCState m => (ScopeInfo -> ScopeInfo) -> m ()
useScope :: ReadTCState m => Lens' a ScopeInfo -> m a
locallyScope :: ReadTCState m => Lens' a ScopeInfo -> (a -> a) -> m b -> m b
withScope :: ReadTCState m => ScopeInfo -> m a -> m (a, ScopeInfo)
withScope_ :: ReadTCState m => ScopeInfo -> m a -> m a
localScope :: TCM a -> TCM a
notInScopeError :: QName -> TCM a
notInScopeWarning :: QName -> TCM ()
printScope :: String -> Int -> String -> TCM ()
modifySignature :: (Signature -> Signature) -> TCM ()
modifyImportedSignature :: (Signature -> Signature) -> TCM ()
getSignature :: ReadTCState m => m Signature
modifyGlobalDefinition :: QName -> (Definition -> Definition) -> TCM ()
setSignature :: Signature -> TCM ()
withSignature :: Signature -> TCM a -> TCM a
addRewriteRulesFor :: QName -> RewriteRules -> [QName] -> Signature -> Signature
setMatchableSymbols :: QName -> [QName] -> Signature -> Signature
lookupDefinition :: QName -> Signature -> Maybe Definition
updateDefinitions :: (Definitions -> Definitions) -> Signature -> Signature
updateDefinition :: QName -> (Definition -> Definition) -> Signature -> Signature
updateTheDef :: (Defn -> Defn) -> Definition -> Definition
updateDefType :: (Type -> Type) -> Definition -> Definition
updateDefArgOccurrences :: ([Occurrence] -> [Occurrence]) -> Definition -> Definition
updateDefPolarity :: ([Polarity] -> [Polarity]) -> Definition -> Definition
updateDefCompiledRep :: (CompiledRepresentation -> CompiledRepresentation) -> Definition -> Definition
addCompilerPragma :: BackendName -> CompilerPragma -> Definition -> Definition
updateFunClauses :: ([Clause] -> [Clause]) -> Defn -> Defn
updateCovering :: ([Clause] -> [Clause]) -> Defn -> Defn
updateCompiledClauses :: (Maybe CompiledClauses -> Maybe CompiledClauses) -> Defn -> Defn
updateDefCopatternLHS :: (Bool -> Bool) -> Definition -> Definition
updateDefBlocked :: (Blocked_ -> Blocked_) -> Definition -> Definition
setTopLevelModule :: QName -> TCM ()
withTopLevelModule :: QName -> TCM a -> TCM a
addForeignCode :: BackendName -> String -> TCM ()
getInteractionOutputCallback :: TCM InteractionOutputCallback
appInteractionOutputCallback :: Response -> TCM ()
setInteractionOutputCallback :: InteractionOutputCallback -> TCM ()
getPatternSyns :: ReadTCState m => m PatternSynDefns
setPatternSyns :: PatternSynDefns -> TCM ()
modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()
getPatternSynImports :: ReadTCState m => m PatternSynDefns
getAllPatternSyns :: ReadTCState m => m PatternSynDefns
lookupPatternSyn :: AmbiguousQName -> TCM PatternSynDefn
lookupSinglePatternSyn :: QName -> TCM PatternSynDefn
theBenchmark :: TCState -> Benchmark
updateBenchmark :: (Benchmark -> Benchmark) -> TCState -> TCState
modifyBenchmark :: (Benchmark -> Benchmark) -> TCM ()
addImportedInstances :: Signature -> TCM ()
updateInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCState -> TCState
modifyInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCM ()
getAllInstanceDefs :: TCM TempInstanceTable
getAnonInstanceDefs :: TCM (Set QName)
clearAnonInstanceDefs :: TCM ()
addUnknownInstance :: QName -> TCM ()
addNamedInstance :: QName -> QName -> TCM ()
interestingCall :: Call -> Bool
traceCallM :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => tcm Call -> tcm a -> tcm a
traceCallCPS :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => Call -> ((a -> tcm b) -> tcm b) -> (a -> tcm b) -> tcm b
traceCall :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => Call -> tcm a -> tcm a
traceClosureCall :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) => Closure Call -> tcm a -> tcm a
getCurrentRange :: MonadTCEnv m => m Range
setCurrentRange :: (MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) => x -> tcm a -> tcm a
highlightAsTypeChecked :: (MonadTCM tcm, ReadTCState tcm) => Range -> Range -> tcm a -> tcm a
printHighlightingInfo :: (MonadTCM tcm, ReadTCState tcm) => RemoveTokenBasedHighlighting -> HighlightingInfo -> tcm ()
noMutualBlock :: TCM a -> TCM a
inMutualBlock :: (MutualId -> TCM a) -> TCM a
setMutualBlockInfo :: MutualId -> MutualInfo -> TCM ()
insertMutualBlockInfo :: MutualId -> MutualInfo -> TCM ()
setMutualBlock :: MutualId -> QName -> TCM ()
currentOrFreshMutualBlock :: TCM MutualId
lookupMutualBlock :: MutualId -> TCM MutualBlock
mutualBlockOf :: QName -> TCM MutualId
enterClosure :: (MonadTCEnv m, ReadTCState m, LensClosure a c) => c -> (a -> m b) -> m b
withClosure :: (MonadTCEnv m, ReadTCState m) => Closure a -> (a -> m b) -> m (Closure b)
mapClosure :: (MonadTCEnv m, ReadTCState m) => (a -> m b) -> Closure a -> m (Closure b)
class (MonadTCEnv m, ReadTCState m, MonadError TCErr m, HasOptions m, MonadDebug m) => MonadConstraint m where
- addConstraint :: Constraint -> m ()
- addAwakeConstraint :: Constraint -> m ()
- catchPatternErr :: m a -> m a -> m a
- solveConstraint :: Constraint -> m ()
- solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> m ()
- wakeConstraints :: (ProblemConstraint -> m Bool) -> m ()
- stealConstraints :: ProblemId -> m ()
- modifyAwakeConstraints :: (Constraints -> Constraints) -> m ()
- modifySleepingConstraints :: (Constraints -> Constraints) -> m ()
data ConstraintStatus
- = AwakeConstraint
- | SleepingConstraint
solvingProblem :: MonadConstraint m => ProblemId -> m a -> m a
solvingProblems :: MonadConstraint m => Set ProblemId -> m a -> m a
isProblemSolved :: (MonadTCEnv m, ReadTCState m) => ProblemId -> m Bool
getConstraintsForProblem :: ReadTCState m => ProblemId -> m Constraints
getAwakeConstraints :: ReadTCState m => m Constraints
dropConstraints :: MonadConstraint m => (ProblemConstraint -> Bool) -> m ()
takeConstraints :: MonadConstraint m => (ProblemConstraint -> Bool) -> m Constraints
putConstraintsToSleep :: MonadConstraint m => (ProblemConstraint -> Bool) -> m ()
putAllConstraintsToSleep :: MonadConstraint m => m ()
holdConstraints :: (ConstraintStatus -> ProblemConstraint -> Bool) -> TCM a -> TCM a
takeAwakeConstraint :: MonadConstraint m => m (Maybe ProblemConstraint)
takeAwakeConstraint' :: MonadConstraint m => (ProblemConstraint -> Bool) -> m (Maybe ProblemConstraint)
getAllConstraints :: ReadTCState m => m Constraints
withConstraint :: MonadConstraint m => (Constraint -> m a) -> ProblemConstraint -> m a
buildProblemConstraint :: (MonadTCEnv m, ReadTCState m) => Set ProblemId -> Constraint -> m ProblemConstraint
buildProblemConstraint_ :: (MonadTCEnv m, ReadTCState m) => Constraint -> m ProblemConstraint
buildConstraint :: Constraint -> TCM ProblemConstraint
addConstraint' :: Constraint -> TCM ()
addAwakeConstraint' :: Constraint -> TCM ()
addConstraintTo :: Lens' Constraints TCState -> Constraint -> TCM ()
nowSolvingConstraints :: MonadTCEnv m => m a -> m a
isSolvingConstraints :: MonadTCEnv m => m Bool
catchConstraint :: MonadConstraint m => Constraint -> m () -> m ()
mapAwakeConstraints :: (Constraints -> Constraints) -> TCState -> TCState
mapSleepingConstraints :: (Constraints -> Constraints) -> TCState -> TCState
setPragmaOptions :: PragmaOptions -> TCM ()
setCommandLineOptions :: CommandLineOptions -> TCM ()
setCommandLineOptions' :: AbsolutePath -> CommandLineOptions -> TCM ()
libToTCM :: LibM a -> TCM a
setLibraryPaths :: AbsolutePath -> CommandLineOptions -> TCM CommandLineOptions
setLibraryIncludes :: CommandLineOptions -> TCM CommandLineOptions
addDefaultLibraries :: AbsolutePath -> CommandLineOptions -> TCM CommandLineOptions
setOptionsFromPragma :: OptionsPragma -> TCM ()
enableDisplayForms :: MonadTCEnv m => m a -> m a
disableDisplayForms :: MonadTCEnv m => m a -> m a
displayFormsEnabled :: MonadTCEnv m => m Bool
setIncludeDirs :: [FilePath] -> AbsolutePath -> TCM ()
setInputFile :: FilePath -> TCM ()
getInputFile :: TCM AbsolutePath
getInputFile' :: TCM (Maybe AbsolutePath)
hasInputFile :: HasOptions m => m Bool
isPropEnabled :: HasOptions m => m Bool
hasUniversePolymorphism :: HasOptions m => m Bool
showImplicitArguments :: HasOptions m => m Bool
showIrrelevantArguments :: HasOptions m => m Bool
withShowAllArguments :: ReadTCState m => m a -> m a
withShowAllArguments' :: ReadTCState m => Bool -> m a -> m a
withPragmaOptions :: ReadTCState m => (PragmaOptions -> PragmaOptions) -> m a -> m a
ignoreInterfaces :: HasOptions m => m Bool
ignoreAllInterfaces :: HasOptions m => m Bool
positivityCheckEnabled :: HasOptions m => m Bool
typeInType :: HasOptions m => m Bool
etaEnabled :: HasOptions m => m Bool
maxInstanceSearchDepth :: HasOptions m => m Int
maxInversionDepth :: HasOptions m => m Int
makeOpen :: MonadTCEnv m => a -> m (Open a)
getOpen :: (Subst Term a, MonadTCEnv m) => Open a -> m a
tryGetOpen :: (Subst Term a, MonadTCEnv m) => Open a -> m (Maybe a)
isClosed :: Open a -> Bool
newtype KeepNames a = KeepNames a
class AddContext b where
- addContext :: MonadAddContext m => b -> m a -> m a
- contextSize :: b -> Nat
unsafeModifyContext :: MonadTCEnv tcm => (Context -> Context) -> tcm a -> tcm a
modifyContextInfo :: MonadTCEnv tcm => (forall e. Dom e -> Dom e) -> tcm a -> tcm a
inTopContext :: (MonadTCEnv tcm, ReadTCState tcm) => tcm a -> tcm a
unsafeInTopContext :: (MonadTCEnv m, ReadTCState m) => m a -> m a
unsafeEscapeContext :: MonadTCM tcm => Int -> tcm a -> tcm a
escapeContext :: MonadAddContext m => Empty -> Int -> m a -> m a
checkpoint :: (MonadDebug tcm, MonadTCM tcm, MonadFresh CheckpointId tcm, ReadTCState tcm) => Substitution -> tcm a -> tcm a
checkpointSubstitution' :: MonadTCEnv tcm => CheckpointId -> tcm (Maybe Substitution)
getModuleParameterSub :: (MonadTCEnv m, ReadTCState m) => ModuleName -> m (Maybe Substitution)
defaultAddCtx :: MonadAddContext m => Name -> Dom Type -> m a -> m a
withFreshName_ :: MonadAddContext m => ArgName -> (Name -> m a) -> m a
withShadowingNameTCM :: Name -> TCM b -> TCM b
addRecordNameContext :: (MonadAddContext m, MonadFresh NameId m) => Dom Type -> m b -> m b
underAbstraction :: (Subst t a, MonadAddContext m) => Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction' :: (Subst t a, MonadAddContext m, AddContext (name, Dom Type)) => (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs :: (Subst t a, MonadAddContext m) => Dom Type -> Abs a -> (a -> m b) -> m b
underAbstractionAbs' :: (Subst t a, MonadAddContext m, AddContext (name, Dom Type)) => (String -> name) -> Dom Type -> Abs a -> (a -> m b) -> m b
underAbstraction_ :: (Subst t a, MonadAddContext m) => Abs a -> (a -> m b) -> m b
mapAbstraction :: (Subst t a, Subst t' b, Free b, MonadAddContext m) => Dom Type -> (a -> m b) -> Abs a -> m (Abs b)
getLetBindings :: MonadTCM tcm => tcm [(Name, (Term, Dom Type))]
defaultAddLetBinding' :: MonadTCEnv m => Name -> Term -> Dom Type -> m a -> m a
addLetBinding :: MonadAddContext m => ArgInfo -> Name -> Term -> Type -> m a -> m a
getContext :: MonadTCEnv m => m [Dom (Name, Type)]
getContextSize :: (Applicative m, MonadTCEnv m) => m Nat
getContextArgs :: (Applicative m, MonadTCEnv m) => m Args
getContextTerms :: (Applicative m, MonadTCEnv m) => m [Term]
getContextTelescope :: (Applicative m, MonadTCEnv m) => m Telescope
getContextNames :: (Applicative m, MonadTCEnv m) => m [Name]
lookupBV' :: MonadTCEnv m => Nat -> m (Maybe (Dom (Name, Type)))
lookupBV :: (MonadFail m, MonadTCEnv m) => Nat -> m (Dom (Name, Type))
domOfBV :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m (Dom Type)
typeOfBV :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m Type
nameOfBV' :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m (Maybe Name)
nameOfBV :: (Applicative m, MonadFail m, MonadTCEnv m) => Nat -> m Name
getVarInfo :: (MonadFail m, MonadTCEnv m) => Name -> m (Term, Dom Type)
data CoinductionKit = CoinductionKit {
- nameOfInf :: QName
- nameOfSharp :: QName
- nameOfFlat :: QName
}
litType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => Literal -> m Type
setBuiltinThings :: BuiltinThings PrimFun -> TCM ()
bindBuiltinName :: String -> Term -> TCM ()
bindPrimitive :: String -> PrimFun -> TCM ()
getBuiltin :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => String -> m Term
getBuiltin' :: HasBuiltins m => String -> m (Maybe Term)
getPrimitive' :: HasBuiltins m => String -> m (Maybe PrimFun)
getPrimitive :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => String -> m PrimFun
getPrimitiveTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => String -> m Term
getPrimitiveTerm' :: HasBuiltins m => String -> m (Maybe Term)
getTerm' :: HasBuiltins m => String -> m (Maybe Term)
getName' :: HasBuiltins m => String -> m (Maybe QName)
getTerm :: HasBuiltins m => String -> String -> m Term
constructorForm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => Term -> m Term
constructorForm' :: Applicative m => m Term -> m Term -> Term -> m Term
primInteger :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primIntegerPos :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primIntegerNegSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primFloat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primChar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primBool :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primSigma :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primUnit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primUnitUnit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primTrue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primFalse :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primList :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primNil :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primCons :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primIO :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primId :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primConId :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primIdElim :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primPath :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primPathP :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primInterval :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primIZero :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primIOne :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primIMin :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primIMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primINeg :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primPartial :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primPartialP :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primIsOne :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primItIsOne :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primTrans :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primHComp :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primEquiv :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primEquivFun :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primEquivProof :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primTranspProof :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
prim_glueU :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
prim_unglueU :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primGlue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
prim_glue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
prim_unglue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primFaceForall :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primIsOne1 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primIsOne2 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primIsOneEmpty :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primSub :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primSubIn :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primSubOut :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primNat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primZero :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primNatPlus :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primNatMinus :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primNatTimes :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primNatDivSucAux :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primNatModSucAux :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primNatEquality :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primNatLess :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primWord64 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primSizeUniv :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primSize :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primSizeLt :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primSizeSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primSizeInf :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primSizeMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primInf :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primSharp :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primFlat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primEquality :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primRefl :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primRewrite :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primLevel :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primLevelZero :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primLevelSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primLevelMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primSetOmega :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primFromNat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primFromNeg :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primFromString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primQName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primArg :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primArgArg :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAbs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAbsAbs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaSort :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primHiding :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primHidden :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primInstance :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primVisible :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primRelevance :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primRelevant :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primIrrelevant :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAssoc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAssocLeft :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAssocRight :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAssocNon :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primPrecedence :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primPrecRelated :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primPrecUnrelated :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primFixity :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primFixityFixity :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primArgInfo :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primArgArgInfo :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaSortSet :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaSortLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaSortUnsupported :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTermVar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTermLam :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTermExtLam :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTermDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTermCon :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTermPi :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTermSort :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTermLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTermUnsupported :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTermMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaErrorPart :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaErrorPartString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaErrorPartTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaErrorPartName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaLiteral :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaLitNat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaLitWord64 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaLitFloat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaLitChar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaLitString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaLitQName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaLitMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaPattern :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaPatCon :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaPatVar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaPatDot :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaPatLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaPatProj :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaPatAbsurd :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaClause :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaClauseClause :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaClauseAbsurd :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaDefinitionFunDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaDefinitionDataDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaDefinitionRecordDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaDefinitionDataConstructor :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaDefinitionPostulate :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaDefinitionPrimitive :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaDefinition :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCM :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMReturn :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMBind :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMUnify :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMTypeError :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMInferType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMCheckType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMNormalise :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMReduce :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMCatchError :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMGetContext :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMExtendContext :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMInContext :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMFreshName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMDeclareDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMDeclarePostulate :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMDefineFun :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMGetType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMGetDefinition :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMQuoteTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMUnquoteTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMBlockOnMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMCommit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMIsMacro :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMWithNormalisation :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMDebugPrint :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMNoConstraints :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMRunSpeculative :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
coinductionKit' :: TCM CoinductionKit
coinductionKit :: TCM (Maybe CoinductionKit)
getPrimName :: Term -> QName
getBuiltinName' :: HasBuiltins m => String -> m (Maybe QName)
getPrimitiveName' :: HasBuiltins m => String -> m (Maybe QName)
isPrimitive :: HasBuiltins m => String -> QName -> m Bool
intervalView' :: HasBuiltins m => m (Term -> IntervalView)
intervalView :: HasBuiltins m => Term -> m IntervalView
intervalUnview :: HasBuiltins m => IntervalView -> m Term
intervalUnview' :: HasBuiltins m => m (IntervalView -> Term)
pathView :: HasBuiltins m => Type -> m PathView
pathView' :: HasBuiltins m => m (Type -> PathView)
idViewAsPath :: HasBuiltins m => Type -> m PathView
boldPathView :: Type -> PathView
pathUnview :: PathView -> Type
primEqualityName :: TCM QName
equalityView :: Type -> TCM EqualityView
equalityUnview :: EqualityView -> Type
constrainedPrims :: [String]
getNameOfConstrained :: HasBuiltins m => String -> m (Maybe QName)
type SizeMaxView' = [DeepSizeView]
type SizeMaxView = NonEmpty DeepSizeView
data SizeViewComparable a
- = NotComparable
- | YesAbove DeepSizeView a
- | YesBelow DeepSizeView a
data DeepSizeView
- = DSizeInf
- | DSizeVar Nat Offset
- | DSizeMeta MetaId Elims Offset
- | DOtherSize Term
type Offset = Nat
data SizeView
- = SizeInf
- | SizeSuc Term
- | OtherSize Term
class IsSizeType a where
- isSizeType :: (HasOptions m, HasBuiltins m) => a -> m (Maybe BoundedSize)
data BoundedSize
- = BoundedLt Term
- | BoundedNo
isSizeTypeTest :: (HasOptions m, HasBuiltins m) => m (Term -> Maybe BoundedSize)
getBuiltinDefName :: HasBuiltins m => String -> m (Maybe QName)
getBuiltinSize :: HasBuiltins m => m (Maybe QName, Maybe QName)
isSizeNameTest :: (HasOptions m, HasBuiltins m) => m (QName -> Bool)
isSizeNameTestRaw :: (HasOptions m, HasBuiltins m) => m (QName -> Bool)
haveSizedTypes :: TCM Bool
haveSizeLt :: TCM Bool
builtinSizeHook :: String -> QName -> Type -> TCM ()
sizeSort :: Sort
sizeUniv :: Type
sizeType_ :: QName -> Type
sizeType :: (HasBuiltins m, MonadTCEnv m, ReadTCState m) => m Type
sizeSucName :: (HasBuiltins m, HasOptions m) => m (Maybe QName)
sizeSuc :: HasBuiltins m => Nat -> Term -> m Term
sizeSuc_ :: QName -> Term -> Term
sizeMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => NonEmpty Term -> m Term
sizeView :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => Term -> m SizeView
sizeViewComparable :: DeepSizeView -> DeepSizeView -> SizeViewComparable ()
sizeViewSuc_ :: QName -> DeepSizeView -> DeepSizeView
sizeViewPred :: Nat -> DeepSizeView -> DeepSizeView
sizeViewOffset :: DeepSizeView -> Maybe Offset
removeSucs :: (DeepSizeView, DeepSizeView) -> (DeepSizeView, DeepSizeView)
unSizeView :: SizeView -> TCM Term
unDeepSizeView :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => DeepSizeView -> m Term
maxViewMax :: SizeMaxView -> SizeMaxView -> SizeMaxView
maxViewCons :: DeepSizeView -> SizeMaxView -> SizeMaxView
sizeViewComparableWithMax :: DeepSizeView -> SizeMaxView -> SizeViewComparable SizeMaxView'
maxViewSuc_ :: QName -> SizeMaxView -> SizeMaxView
unMaxView :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => SizeMaxView -> m Term
addConstant :: QName -> Definition -> TCM ()
setTerminates :: QName -> Bool -> TCM ()
setCompiledClauses :: QName -> CompiledClauses -> TCM ()
setSplitTree :: QName -> SplitTree -> TCM ()
modifyFunClauses :: QName -> ([Clause] -> [Clause]) -> TCM ()
addClauses :: QName -> [Clause] -> TCM ()
mkPragma :: String -> TCM CompilerPragma
addPragma :: BackendName -> QName -> String -> TCM ()
getUniqueCompilerPragma :: BackendName -> QName -> TCM (Maybe CompilerPragma)
setFunctionFlag :: FunctionFlag -> Bool -> QName -> TCM ()
markStatic :: QName -> TCM ()
markInline :: Bool -> QName -> TCM ()
markInjective :: QName -> TCM ()
unionSignatures :: [Signature] -> Signature
addSection :: ModuleName -> TCM ()
setModuleCheckpoint :: ModuleName -> TCM ()
getSection :: (Functor m, ReadTCState m) => ModuleName -> m (Maybe Section)
addDisplayForms :: QName -> TCM ()
applySection :: ModuleName -> Telescope -> ModuleName -> Args -> ScopeCopyInfo -> TCM ()
applySection' :: ModuleName -> Telescope -> ModuleName -> Args -> ScopeCopyInfo -> TCM ()
addDisplayForm :: QName -> DisplayForm -> TCM ()
isLocal :: ReadTCState m => QName -> m Bool
getDisplayForms :: (HasConstInfo m, ReadTCState m) => QName -> m [LocalDisplayForm]
chaseDisplayForms :: QName -> TCM (Set QName)
hasLoopingDisplayForm :: QName -> TCM Bool
canonicalName :: HasConstInfo m => QName -> m QName
sameDef :: HasConstInfo m => QName -> QName -> m (Maybe QName)
whatInduction :: MonadTCM tcm => QName -> tcm Induction
singleConstructorType :: QName -> TCM Bool
sigError :: (String -> a) -> a -> SigError -> a
defaultGetRewriteRulesFor :: Monad m => m TCState -> QName -> m RewriteRules
getOriginalProjection :: HasConstInfo m => QName -> m QName
defaultGetConstInfo :: (HasOptions m, MonadDebug m, MonadTCEnv m) => TCState -> TCEnv -> QName -> m (Either SigError Definition)
getConInfo :: HasConstInfo m => ConHead -> m Definition
getPolarity :: HasConstInfo m => QName -> m [Polarity]
getPolarity' :: HasConstInfo m => Comparison -> QName -> m [Polarity]
setPolarity :: QName -> [Polarity] -> TCM ()
getForcedArgs :: HasConstInfo m => QName -> m [IsForced]
getArgOccurrence :: QName -> Nat -> TCM Occurrence
setArgOccurrences :: QName -> [Occurrence] -> TCM ()
modifyArgOccurrences :: QName -> ([Occurrence] -> [Occurrence]) -> TCM ()
setTreeless :: QName -> TTerm -> TCM ()
setCompiledArgUse :: QName -> [Bool] -> TCM ()
getCompiled :: QName -> TCM (Maybe Compiled)
getErasedConArgs :: QName -> TCM [Bool]
setErasedConArgs :: QName -> [Bool] -> TCM ()
getTreeless :: QName -> TCM (Maybe TTerm)
getCompiledArgUse :: QName -> TCM [Bool]
addDataCons :: QName -> [QName] -> TCM ()
getMutual :: QName -> TCM (Maybe [QName])
getMutual_ :: Defn -> Maybe [QName]
setMutual :: QName -> [QName] -> TCM ()
mutuallyRecursive :: QName -> QName -> TCM Bool
definitelyNonRecursive_ :: Defn -> Bool
getCurrentModuleFreeVars :: TCM Nat
getDefModule :: HasConstInfo m => QName -> m (Either SigError ModuleName)
getDefFreeVars :: (Functor m, Applicative m, ReadTCState m, MonadTCEnv m) => QName -> m Nat
freeVarsToApply :: (Functor m, HasConstInfo m, HasOptions m, ReadTCState m, MonadTCEnv m, MonadDebug m) => QName -> m Args
getModuleFreeVars :: (Functor m, Applicative m, MonadTCEnv m, ReadTCState m) => ModuleName -> m Nat
moduleParamsToApply :: (Functor m, Applicative m, HasOptions m, MonadTCEnv m, ReadTCState m, MonadDebug m) => ModuleName -> m Args
instantiateDef :: (Functor m, HasConstInfo m, HasOptions m, ReadTCState m, MonadTCEnv m, MonadDebug m) => Definition -> m Definition
instantiateRewriteRule :: (Functor m, HasConstInfo m, HasOptions m, ReadTCState m, MonadTCEnv m, MonadDebug m) => RewriteRule -> m RewriteRule
instantiateRewriteRules :: (Functor m, HasConstInfo m, HasOptions m, ReadTCState m, MonadTCEnv m, MonadDebug m) => RewriteRules -> m RewriteRules
makeAbstract :: Definition -> Maybe Definition
inAbstractMode :: MonadTCEnv m => m a -> m a
inConcreteMode :: MonadTCEnv m => m a -> m a
ignoreAbstractMode :: MonadTCEnv m => m a -> m a
inConcreteOrAbstractMode :: (MonadTCEnv m, HasConstInfo m) => QName -> (Definition -> m a) -> m a
treatAbstractly :: MonadTCEnv m => QName -> m Bool
treatAbstractly' :: QName -> TCEnv -> Bool
typeOfConst :: (HasConstInfo m, ReadTCState m) => QName -> m Type
relOfConst :: HasConstInfo m => QName -> m Relevance
modalityOfConst :: HasConstInfo m => QName -> m Modality
droppedPars :: Definition -> Int
isProjection :: HasConstInfo m => QName -> m (Maybe Projection)
isProjection_ :: Defn -> Maybe Projection
isStaticFun :: Defn -> Bool
isInlineFun :: Defn -> Bool
isProperProjection :: Defn -> Bool
projectionArgs :: Defn -> Int
usesCopatterns :: HasConstInfo m => QName -> m Bool
applyDef :: HasConstInfo m => ProjOrigin -> QName -> Arg Term -> m Term
class UnFreezeMeta a where
- unfreezeMeta :: MonadMetaSolver m => a -> m ()
class IsInstantiatedMeta a where
- isInstantiatedMeta :: (MonadFail m, ReadTCState m) => a -> m Bool
class (MonadConstraint m, MonadReduce m, MonadAddContext m, MonadTCEnv m, ReadTCState m, HasBuiltins m, HasConstInfo m, MonadDebug m) => MonadMetaSolver m where
- newMeta' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> m MetaId
- assignV :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> m ()
- assignTerm' :: MonadMetaSolver m => MetaId -> [Arg ArgName] -> Term -> m ()
- etaExpandMeta :: [MetaKind] -> MetaId -> m ()
- updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> m ()
- speculateMetas :: m () -> m KeepMetas -> m ()
data KeepMetas
- = KeepMetas
- | RollBackMetas
data MetaKind
- = Records
- | SingletonRecords
- | Levels
allMetaKinds :: [MetaKind]
dontAssignMetas :: (MonadTCEnv m, HasOptions m, MonadDebug m) => m a -> m a
getMetaStore :: ReadTCState m => m MetaStore
modifyMetaStore :: (MetaStore -> MetaStore) -> TCM ()
metasCreatedBy :: ReadTCState m => m a -> m (a, IntSet)
lookupMeta' :: ReadTCState m => MetaId -> m (Maybe MetaVariable)
lookupMeta :: (MonadFail m, ReadTCState m) => MetaId -> m MetaVariable
metaType :: (MonadFail m, ReadTCState m) => MetaId -> m Type
updateMetaVarTCM :: MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
insertMetaVar :: MetaId -> MetaVariable -> TCM ()
getMetaPriority :: (MonadFail m, ReadTCState m) => MetaId -> m MetaPriority
isSortMeta :: (MonadFail m, ReadTCState m) => MetaId -> m Bool
isSortMeta_ :: MetaVariable -> Bool
getMetaType :: (MonadFail m, ReadTCState m) => MetaId -> m Type
getMetaContextArgs :: MonadTCEnv m => MetaVariable -> m Args
getMetaTypeInContext :: (MonadFail m, MonadTCEnv m, ReadTCState m, MonadReduce m) => MetaId -> m Type
isGeneralizableMeta :: (ReadTCState m, MonadFail m) => MetaId -> m DoGeneralize
isInstantiatedMeta' :: (MonadFail m, ReadTCState m) => MetaId -> m (Maybe Term)
constraintMetas :: Constraint -> TCM (Set MetaId)
createMetaInfo :: (MonadTCEnv m, ReadTCState m) => m MetaInfo
createMetaInfo' :: (MonadTCEnv m, ReadTCState m) => RunMetaOccursCheck -> m MetaInfo
setValueMetaName :: MonadMetaSolver m => Term -> MetaNameSuggestion -> m ()
getMetaNameSuggestion :: (MonadFail m, ReadTCState m) => MetaId -> m MetaNameSuggestion
setMetaNameSuggestion :: MonadMetaSolver m => MetaId -> MetaNameSuggestion -> m ()
setMetaArgInfo :: MonadMetaSolver m => MetaId -> ArgInfo -> m ()
updateMetaVarRange :: MonadMetaSolver m => MetaId -> Range -> m ()
setMetaOccursCheck :: MonadMetaSolver m => MetaId -> RunMetaOccursCheck -> m ()
registerInteractionPoint :: forall m. MonadInteractionPoints m => Bool -> Range -> Maybe Nat -> m InteractionId
findInteractionPoint_ :: Range -> InteractionPoints -> Maybe InteractionId
connectInteractionPoint :: MonadInteractionPoints m => InteractionId -> MetaId -> m ()
removeInteractionPoint :: MonadInteractionPoints m => InteractionId -> m ()
getInteractionPoints :: ReadTCState m => m [InteractionId]
getInteractionMetas :: ReadTCState m => m [MetaId]
getInteractionIdsAndMetas :: ReadTCState m => m [(InteractionId, MetaId)]
isInteractionMeta :: ReadTCState m => MetaId -> m (Maybe InteractionId)
lookupInteractionPoint :: (MonadFail m, ReadTCState m, MonadError TCErr m) => InteractionId -> m InteractionPoint
lookupInteractionId :: (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) => InteractionId -> m MetaId
lookupInteractionMeta :: ReadTCState m => InteractionId -> m (Maybe MetaId)
lookupInteractionMeta_ :: InteractionId -> InteractionPoints -> Maybe MetaId
newMeta :: MonadMetaSolver m => Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> m MetaId
newMetaTCM' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> TCM MetaId
getInteractionRange :: (MonadInteractionPoints m, MonadFail m, MonadError TCErr m) => InteractionId -> m Range
getMetaRange :: (MonadFail m, ReadTCState m) => MetaId -> m Range
getInteractionScope :: InteractionId -> TCM ScopeInfo
withMetaInfo' :: MetaVariable -> TCM a -> TCM a
withMetaInfo :: Closure Range -> TCM a -> TCM a
getMetaVariableSet :: ReadTCState m => m IntSet
getMetaVariables :: ReadTCState m => (MetaVariable -> Bool) -> m [MetaId]
getInstantiatedMetas :: ReadTCState m => m [MetaId]
getOpenMetas :: ReadTCState m => m [MetaId]
isOpenMeta :: MetaInstantiation -> Bool
listenToMeta :: MonadMetaSolver m => Listener -> MetaId -> m ()
unlistenToMeta :: MonadMetaSolver m => Listener -> MetaId -> m ()
getMetaListeners :: (MonadFail m, ReadTCState m) => MetaId -> m [Listener]
clearMetaListeners :: MonadMetaSolver m => MetaId -> m ()
withFreezeMetas :: TCM a -> TCM a
freezeMetas :: TCM [MetaId]
freezeMetas' :: (MetaId -> Bool) -> TCM [MetaId]
unfreezeMetas :: TCM ()
unfreezeMetas' :: (MetaId -> Bool) -> TCM ()
isFrozen :: (MonadFail m, ReadTCState m) => MetaId -> m Bool
activeBackendMayEraseType :: QName -> TCM Bool
backendInteraction :: [Backend] -> (TCM (Maybe Interface) -> TCM ()) -> TCM (Maybe Interface) -> TCM ()
parseBackendOptions :: [Backend] -> [String] -> CommandLineOptions -> OptM ([Backend], CommandLineOptions)
callBackend :: String -> IsMain -> Interface -> TCM ()
lookupBackend :: BackendName -> TCM (Maybe Backend)
activeBackend :: TCM (Maybe Backend)

Documentation

data Backend where Source #

Constructors

Backend :: Backend' opts env menv mod def -> Backend

data Backend' opts env menv mod def Source #

Constructors

Backend'

Fields

backendName :: String
backendVersion :: Maybe String
Optional version information to be printed with --version.
options :: opts
Default options
commandLineFlags :: [OptDescr (Flag opts)]
Backend-specific command-line flags. Should at minimum contain a flag to enable the backend.
isEnabled :: opts -> Bool
Unless the backend has been enabled, runAgda will fall back to vanilla Agda behaviour.
preCompile :: opts -> TCM env
Called after type checking completes, but before compilation starts.
postCompile :: env -> IsMain -> Map ModuleName mod -> TCM ()
Called after module compilation has completed. The IsMain argument is NotMain if the --no-main flag is present.
preModule :: env -> IsMain -> ModuleName -> FilePath -> TCM (Recompile menv mod)
Called before compilation of each module. Gets the path to the .agdai file to allow up-to-date checking of previously written compilation results. Should return Skip m if compilation is not required.
postModule :: env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod
Called after all definitions of a module have been compiled.
compileDef :: env -> menv -> IsMain -> Definition -> TCM def
Compile a single definition.
scopeCheckingSuffices :: Bool
True if the backend works if --only-scope-checking is used.
mayEraseType :: QName -> TCM Bool
The treeless compiler may ask the Backend if elements of the given type maybe possibly erased. The answer should be False if the compilation of the type is used by a third party, e.g. in a FFI binding.

data Recompile menv mod Source #

Constructors

Recompile menv
Skip mod

data IsMain Source #

Constructors

IsMain
NotMain

Instances

Instances details

Eq IsMain Source #
Instance details Defined in Agda.Compiler.Common Methods (==) :: IsMain -> IsMain -> Bool (/=) :: IsMain -> IsMain -> Bool
Show IsMain Source #
Instance details Defined in Agda.Compiler.Common Methods showsPrec :: Int -> IsMain -> ShowS show :: IsMain -> String showList :: [IsMain] -> ShowS
Semigroup IsMain Source #	Conjunctive semigroup (`NotMain` is absorbing).
Instance details Defined in Agda.Compiler.Common Methods (<>) :: IsMain -> IsMain -> IsMain # sconcat :: NonEmpty IsMain -> IsMain stimes :: Integral b => b -> IsMain -> IsMain
Monoid IsMain Source #
Instance details Defined in Agda.Compiler.Common Methods mempty :: IsMain mappend :: IsMain -> IsMain -> IsMain mconcat :: [IsMain] -> IsMain

type Flag opts = opts -> OptM opts Source #

f :: Flag opts is an action on the option record that results from parsing an option. f opts produces either an error message or an updated options record

toTreeless :: EvaluationStrategy -> QName -> TCM (Maybe TTerm) Source #

Converts compiled clauses to treeless syntax.

Note: Do not use any of the concrete names in the returned term for identification purposes! If you wish to do so, first apply the Agda.Compiler.Treeless.NormalizeNames transformation.

module Agda.Syntax.Treeless

builtinNat :: String Source #

builtinSuc :: String Source #

builtinZero :: String Source #

builtinNatPlus :: String Source #

builtinNatMinus :: String Source #

builtinNatTimes :: String Source #

builtinNatDivSucAux :: String Source #

builtinNatModSucAux :: String Source #

builtinNatEquals :: String Source #

builtinNatLess :: String Source #

builtinWord64 :: String Source #

builtinInteger :: String Source #

builtinIntegerPos :: String Source #

builtinIntegerNegSuc :: String Source #

builtinFloat :: String Source #

builtinChar :: String Source #

builtinString :: String Source #

builtinUnit :: String Source #

builtinUnitUnit :: String Source #

builtinSigma :: String Source #

builtinBool :: String Source #

builtinTrue :: String Source #

builtinFalse :: String Source #

builtinList :: String Source #

builtinNil :: String Source #

builtinCons :: String Source #

builtinIO :: String Source #

builtinId :: String Source #

builtinConId :: String Source #

builtinIdElim :: String Source #

builtinPath :: String Source #

builtinPathP :: String Source #

builtinInterval :: String Source #

builtinIMin :: String Source #

builtinIMax :: String Source #

builtinINeg :: String Source #

builtinIZero :: String Source #

builtinIOne :: String Source #

builtinPartial :: String Source #

builtinPartialP :: String Source #

builtinIsOne :: String Source #

builtinItIsOne :: String Source #

builtinEquiv :: String Source #

builtinEquivFun :: String Source #

builtinEquivProof :: String Source #

builtinTranspProof :: String Source #

builtinGlue :: String Source #

builtin_glue :: String Source #

builtin_unglue :: String Source #

builtin_glueU :: String Source #

builtin_unglueU :: String Source #

builtinFaceForall :: String Source #

builtinIsOne1 :: String Source #

builtinIsOne2 :: String Source #

builtinIsOneEmpty :: String Source #

builtinComp :: String Source #

builtinPOr :: String Source #

builtinTrans :: String Source #

builtinHComp :: String Source #

builtinSub :: String Source #

builtinSubIn :: String Source #

builtinSubOut :: String Source #

builtinSizeUniv :: String Source #

builtinSize :: String Source #

builtinSizeLt :: String Source #

builtinSizeSuc :: String Source #

builtinSizeInf :: String Source #

builtinSizeMax :: String Source #

builtinInf :: String Source #

builtinSharp :: String Source #

builtinFlat :: String Source #

builtinEquality :: String Source #

builtinRefl :: String Source #

builtinRewrite :: String Source #

builtinLevelMax :: String Source #

builtinLevel :: String Source #

builtinLevelZero :: String Source #

builtinLevelSuc :: String Source #

builtinSetOmega :: String Source #

builtinFromNat :: String Source #

builtinFromNeg :: String Source #

builtinFromString :: String Source #

builtinQName :: String Source #

builtinAgdaSort :: String Source #

builtinAgdaSortSet :: String Source #

builtinAgdaSortLit :: String Source #

builtinAgdaSortUnsupported :: String Source #

builtinHiding :: String Source #

builtinHidden :: String Source #

builtinInstance :: String Source #

builtinVisible :: String Source #

builtinRelevance :: String Source #

builtinRelevant :: String Source #

builtinIrrelevant :: String Source #

builtinAssoc :: String Source #

builtinAssocLeft :: String Source #

builtinAssocRight :: String Source #

builtinAssocNon :: String Source #

builtinPrecedence :: String Source #

builtinPrecRelated :: String Source #

builtinPrecUnrelated :: String Source #

builtinFixity :: String Source #

builtinFixityFixity :: String Source #

builtinArg :: String Source #

builtinArgInfo :: String Source #

builtinArgArgInfo :: String Source #

builtinArgArg :: String Source #

builtinAbs :: String Source #

builtinAbsAbs :: String Source #

builtinAgdaTerm :: String Source #

builtinAgdaTermVar :: String Source #

builtinAgdaTermLam :: String Source #

builtinAgdaTermExtLam :: String Source #

builtinAgdaTermDef :: String Source #

builtinAgdaTermCon :: String Source #

builtinAgdaTermPi :: String Source #

builtinAgdaTermSort :: String Source #

builtinAgdaTermLit :: String Source #

builtinAgdaTermUnsupported :: String Source #

builtinAgdaTermMeta :: String Source #

builtinAgdaErrorPart :: String Source #

builtinAgdaErrorPartString :: String Source #

builtinAgdaErrorPartTerm :: String Source #

builtinAgdaErrorPartName :: String Source #

builtinAgdaLiteral :: String Source #

builtinAgdaLitNat :: String Source #

builtinAgdaLitWord64 :: String Source #

builtinAgdaLitFloat :: String Source #

builtinAgdaLitChar :: String Source #

builtinAgdaLitString :: String Source #

builtinAgdaLitQName :: String Source #

builtinAgdaLitMeta :: String Source #

builtinAgdaClause :: String Source #

builtinAgdaClauseClause :: String Source #

builtinAgdaClauseAbsurd :: String Source #

builtinAgdaPattern :: String Source #

builtinAgdaPatVar :: String Source #

builtinAgdaPatCon :: String Source #

builtinAgdaPatDot :: String Source #

builtinAgdaPatLit :: String Source #

builtinAgdaPatProj :: String Source #

builtinAgdaPatAbsurd :: String Source #

builtinAgdaDefinitionFunDef :: String Source #

builtinAgdaDefinitionDataDef :: String Source #

builtinAgdaDefinitionRecordDef :: String Source #

builtinAgdaDefinitionDataConstructor :: String Source #

builtinAgdaDefinitionPostulate :: String Source #

builtinAgdaDefinitionPrimitive :: String Source #

builtinAgdaDefinition :: String Source #

builtinAgdaMeta :: String Source #

builtinAgdaTCM :: String Source #

builtinAgdaTCMReturn :: String Source #

builtinAgdaTCMBind :: String Source #

builtinAgdaTCMUnify :: String Source #

builtinAgdaTCMTypeError :: String Source #

builtinAgdaTCMInferType :: String Source #

builtinAgdaTCMCheckType :: String Source #

builtinAgdaTCMNormalise :: String Source #

builtinAgdaTCMReduce :: String Source #

builtinAgdaTCMCatchError :: String Source #

builtinAgdaTCMGetContext :: String Source #

builtinAgdaTCMExtendContext :: String Source #

builtinAgdaTCMInContext :: String Source #

builtinAgdaTCMFreshName :: String Source #

builtinAgdaTCMDeclareDef :: String Source #

builtinAgdaTCMDeclarePostulate :: String Source #

builtinAgdaTCMDefineFun :: String Source #

builtinAgdaTCMGetType :: String Source #

builtinAgdaTCMGetDefinition :: String Source #

builtinAgdaTCMBlockOnMeta :: String Source #

builtinAgdaTCMCommit :: String Source #

builtinAgdaTCMQuoteTerm :: String Source #

builtinAgdaTCMUnquoteTerm :: String Source #

builtinAgdaTCMIsMacro :: String Source #

builtinAgdaTCMWithNormalisation :: String Source #

builtinAgdaTCMDebugPrint :: String Source #

builtinAgdaTCMNoConstraints :: String Source #

builtinAgdaTCMRunSpeculative :: String Source #

builtinsNoDef :: [String] Source #

Builtins that come without a definition in Agda syntax. These are giving names to Agda internal concepts which cannot be assigned an Agda type.

An example would be a user-defined name for Set.

{--}

The type of Type would be Type : Level → Setω which is not valid Agda.

sizeBuiltins :: [String] Source #

data Polarity Source #

Polarity for equality and subtype checking.

Constructors

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

Instances

Instances details

Eq Polarity Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: Polarity -> Polarity -> Bool (/=) :: Polarity -> Polarity -> Bool
Data Polarity Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Polarity -> c Polarity gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Polarity toConstr :: Polarity -> Constr dataTypeOf :: Polarity -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Polarity) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Polarity) gmapT :: (forall b. Data b => b -> b) -> Polarity -> Polarity gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Polarity -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Polarity -> r gmapQ :: (forall d. Data d => d -> u) -> Polarity -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Polarity -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Polarity -> m Polarity gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Polarity -> m Polarity gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Polarity -> m Polarity
Show Polarity Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Polarity -> ShowS show :: Polarity -> String showList :: [Polarity] -> ShowS
Pretty Polarity Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Polarity -> Doc Source # prettyPrec :: Int -> Polarity -> Doc Source # prettyList :: [Polarity] -> Doc Source #
KillRange Polarity Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods killRange :: KillRangeT Polarity Source #
EmbPrj Polarity Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Polarity -> S Int32 Source # icod_ :: Polarity -> S Int32 Source # value :: Int32 -> R Polarity Source #
PrettyTCM Polarity Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Polarity -> m Doc Source #
Abstract [Polarity] Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> [Polarity] -> [Polarity] Source #
Apply [Polarity] Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: [Polarity] -> Args -> [Polarity] Source # applyE :: [Polarity] -> Elims -> [Polarity] Source #

newtype ProblemId Source #

Constructors

ProblemId Nat

Instances

Instances details

Enum ProblemId Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods succ :: ProblemId -> ProblemId pred :: ProblemId -> ProblemId toEnum :: Int -> ProblemId fromEnum :: ProblemId -> Int enumFrom :: ProblemId -> [ProblemId] enumFromThen :: ProblemId -> ProblemId -> [ProblemId] enumFromTo :: ProblemId -> ProblemId -> [ProblemId] enumFromThenTo :: ProblemId -> ProblemId -> ProblemId -> [ProblemId]
Eq ProblemId Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: ProblemId -> ProblemId -> Bool (/=) :: ProblemId -> ProblemId -> Bool
Integral ProblemId Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods quot :: ProblemId -> ProblemId -> ProblemId rem :: ProblemId -> ProblemId -> ProblemId div :: ProblemId -> ProblemId -> ProblemId mod :: ProblemId -> ProblemId -> ProblemId quotRem :: ProblemId -> ProblemId -> (ProblemId, ProblemId) divMod :: ProblemId -> ProblemId -> (ProblemId, ProblemId) toInteger :: ProblemId -> Integer
Data ProblemId Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProblemId -> c ProblemId gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProblemId toConstr :: ProblemId -> Constr dataTypeOf :: ProblemId -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProblemId) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProblemId) gmapT :: (forall b. Data b => b -> b) -> ProblemId -> ProblemId gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProblemId -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProblemId -> r gmapQ :: (forall d. Data d => d -> u) -> ProblemId -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ProblemId -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemId -> m ProblemId
Num ProblemId Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (+) :: ProblemId -> ProblemId -> ProblemId (-) :: ProblemId -> ProblemId -> ProblemId (*) :: ProblemId -> ProblemId -> ProblemId negate :: ProblemId -> ProblemId abs :: ProblemId -> ProblemId signum :: ProblemId -> ProblemId fromInteger :: Integer -> ProblemId
Ord ProblemId Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods compare :: ProblemId -> ProblemId -> Ordering (<) :: ProblemId -> ProblemId -> Bool (<=) :: ProblemId -> ProblemId -> Bool (>) :: ProblemId -> ProblemId -> Bool (>=) :: ProblemId -> ProblemId -> Bool max :: ProblemId -> ProblemId -> ProblemId min :: ProblemId -> ProblemId -> ProblemId
Real ProblemId Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods toRational :: ProblemId -> Rational
Show ProblemId Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> ProblemId -> ShowS show :: ProblemId -> String showList :: [ProblemId] -> ShowS
ToJSON ProblemId Source #
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: ProblemId -> Value Source # toEncoding :: ProblemId -> Encoding Source # toJSONList :: [ProblemId] -> Value Source # toEncodingList :: [ProblemId] -> Encoding Source #
Pretty ProblemId Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: ProblemId -> Doc Source # prettyPrec :: Int -> ProblemId -> Doc Source # prettyList :: [ProblemId] -> Doc Source #
HasFresh ProblemId Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freshLens :: Lens' ProblemId TCState Source # nextFresh' :: ProblemId -> ProblemId Source #
PrettyTCM ProblemId Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => ProblemId -> m Doc Source #
EncodeTCM ProblemId Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: ProblemId -> TCM Value Source #
Monad m => MonadFresh ProblemId (PureConversionT m) Source #
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods fresh :: PureConversionT m ProblemId Source #

data Comparison Source #

Constructors

CmpEq
CmpLeq

Instances

Instances details

Eq Comparison Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods (==) :: Comparison -> Comparison -> Bool (/=) :: Comparison -> Comparison -> Bool
Data Comparison Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Comparison -> c Comparison gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Comparison toConstr :: Comparison -> Constr dataTypeOf :: Comparison -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Comparison) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Comparison) gmapT :: (forall b. Data b => b -> b) -> Comparison -> Comparison gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Comparison -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Comparison -> r gmapQ :: (forall d. Data d => d -> u) -> Comparison -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Comparison -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Comparison -> m Comparison gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Comparison -> m Comparison gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Comparison -> m Comparison
Show Comparison Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods showsPrec :: Int -> Comparison -> ShowS show :: Comparison -> String showList :: [Comparison] -> ShowS
Pretty Comparison Source #
Instance details Defined in Agda.TypeChecking.Monad.Base Methods pretty :: Comparison -> Doc Source # prettyPrec :: Int -> Comparison -> Doc Source # prettyList :: [Comparison] -> Doc Source #
PrettyTCM Comparison Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Comparison -> m Doc Source #

type BackendName = String Source #

type ModuleToSource = Map TopLevelModuleName AbsolutePath Source #

Maps top-level module names to the corresponding source file names.

type TCM = TCMT IO Source #

Type checking monad.

newtype TCMT m a Source #

The type checking monad transformer. Adds readonly TCEnv and mutable TCState.

Constructors

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

Instances

Instances details

QName ->href=td><./usr/share/doc/libghc-agda-doc/html/Agda-Auto-Typecheck.html0000644000000000000000000012523713710313424022577 0ct.Name">Name TCErr m, MonadTCEnv m,

->href=td>

<e m, warnUnknownNamesInFixityDecl :: [Name] -> ScopeM () Source Doc Source #

Methods

addCtx :: Name -> Dom ReadTCState m) =>

= mref="Agda-Name -> Dom #Name TCErr m, ReduceM a -> ReduceM a

builtinAgdaLiteral :: String ">O], MExp O)] Source #

icode :: addCEnd" class="selflink">#

Source #

icode :: Sourli>= mref="Agda-rt">TOM (Name -> EE (MyMB (Maybe (ICArgList o, [

Source

#

icode :: Sourli>= mref="Agda-rt">TOM (gda-Syntax-InSyntils>

on" title="Agda.Compiler.Backend">Definition -> NameSource #

nowDebugPrinting ::

Defined in

on" title="Agda.Compiler.Backendpiler-Backend.nting" class="sd

= Recompile menv
| Skip mod

data NameSource

Pattern) (Pat O)Source #on" title="Agda.Compiler.Backendckend.html#t:TCM" title="Agda.Compiler.ert.html#t:O" title="Agda.Auto.Convert">O)Source #TOM<="#v:modifyCounter" class="selflnd">TCMink">Source<Pattd>nd">TC"lass="seltaie#

catchError :: TCM a #

catchError :: TCM a -> (=;>>TC"lass="seltao-Convert.htmleConvert.htmllflink">#

Pat #TCM acatchError/p>

catchError :: :: ModuleName -> m (Maybe #lass="selfli-Convert.h.Backend">TCMflink">#

#

ExpandM clasax"rt

on" titl href="Agda-CompsExp arkea href=creteNames" cl >>ternal">Pattern) (#

arkea href=creteNames" chregda.TypeChe="subs instances">

on" titl href>PatTCMon" titl href="Agda-CompsExp arkea href=creteNames" cl >> href="Agda-Compiler-Backend.html#t:KeepMetas" title="Agda.Compiler.Backend">KeepMetas -> cthandles :: IORef"-ndM clasax"rtackend.html#t:MeAuto-x">PatO], MExp O)]TCMSource #

Instance details

DefineCompiler.Backend">TCM a MExp class="link"a-Comflink">#

arkea href=creteNames" cl >>ternry>

Defitax.html#t:MAgda.Compiler.Be details"2">>funFlags :: Set Functiond>

Instance details

DefineCompiler.Backend">TCM a MExp class="link"a-Comflink">#

arkea href=creteNames" cl >>ternry>

Defitax.html#t:MAgda.Compiler.Be detailsunctionFlag" title="Agda.Compiler.Backend">Functiond>

nd">TCMink">Source<Functiond>

Methods

addWarning :: TCMink">Source<Functiond>

nd">TCMinkend.html#ternry>

Def>nd">TCMink">Source<e="Agda.Compiler.Backend">Functiond>

nd">TCMink">Source<Functiond>nd">TCMink">Source<e="Agda.Compiler.Backend">Functiond>nd">Co"Env mref="Agda-rt">TOM (gda-Syntax-InSyntils>nd">TCMink">Sourml#ternry>

Degda.Auto.Convert">Conversion Functiond>

nd">Co"Env mref="Agda-rt">TOMMExax.html#t:Eef="Agda-Syntax-Internal.html#t:Dom" title="Agda.Syntax.Internal">DomTOM (gda-Syntax-InSyntils><.n="2">QName Strin/a>ComnablepandM class="srInteractionPoints) -> TOM Functiond>

InteractionPoints

) -> TOM TOM Functiond>

InteractionPoints

) -> TOM MExp O) nd">Functiond>lass="link">Sourceyntax-Concrclass="src"LltipleFixityD#t:O" tit/tr>on" titlwingSearch.html#t:CTree" title="Agdass="src">refinements :: Sourceyn/a> Sourceyn/a> Sourceyn/a> on" titlwingSearch.html#t:CTree"title="Agdass=tle="Agda.Auto.Convele.html#catchImwinbuiltinIZero :: Sc/Agda.Syn> on" titl>"2">

Benchma/Agda.SyntAgda.CompilebuiltinIZero" class="link">Sourceyn/a>

on" titl>"2">

Benchma/Agda.SyntAgda.CompilebuiltinIZero" class="link">Sourceyn/a>

on" titlwingSearch.2">

on" titlwingSearch.html#t:CTree"title="Agdass=tle="Agda.Auto.Convele.html#catchImwinbuiltinIZero :: Sc/Agda.Syn> on" titlwingSearch.2">

on" titlwingSearch.html#t:CTree"title="Agdass=tle="Agda.Auto.Convele.ht:O" tit/tr>on" titl>"2">

on" titpan> "2"> x.hM class="sel> :: Sc/Agbet >>NatchImwn class21">

on" titlcl :: Sc/Agda.Syn>

on" titlcl :: Sc/Agda.Syn> "2">Source

on"ncrclass="src"Llhtml#t:CTree"title="Agdass=tle="Agda.Auto.Convele.ht:O" tit/tr>on" titl>"2">

on" titpan> on" titl>"2">

on" titpan> o#catchImwn hretinI titlwinhtml#t:CTree" on" titl>"2">

tinIZero rt.htorssia-Syitle="Agda idt/tr>

oe="Agda.Auto.Coert" class="ulass="src"Lltipvert">Conversionggle-control de>

tinIZero

tinIZero rt.htorssia-Syitle="Agda isinIZegle-control de>ils idt/tr>

on" titpan> o#catchImwn hretinI titlwinhtml#t:CTree" on" titl>"2">

on" titpan>

tinIZero

tinIZero rt.htorssia-Syitle="Agda isinionggle-contro classinIrt.htorssia-Syi tit/tr>

on" titl>"2">

on" titpan>

tinIZero

arkea href=.htorssia-Syi tiee" "2">

ilsassinIZero"2">

on" titpan> on" titl>"2">

&nbsrch.2">

"2">

on" titpan> on" titpan> on" titl>"2">

on" tiImclass="dgle-contrIZenbuil &nbrc/Agda.Typegda.Syntax.Abstract.Name">QName String

on" tiImclass="dgle-contrIZenb>

&nbsrch.2"t.Name">QNam/Agda.Typegda.Sygd�s idogg=x">&nbs="doc empet de>

"2">Has idt/tr>

on" w="dgle-contrIidoggle-control de>

on" titpan>

&nbsrch.2"t.Name">QNam/Agda.Typegda.Sygd�s idogg=x">&nbs="doc empet de>

">

on" tiImclass="dgle-contrIZenb>

&nbsrch.2"t.Name">QNam/Agda.Typegda.Sygd�s idogg=x">&nbs="doc empet de>

on" tiImclasl>">on" w="dgle-contrIidogName String

on" tiImclass="dgle-contrIZenb>

&nbsrch.ntrol de>QN"2">

on" tiImclasl>">on" tiImclass="dgle-contrIZenb>

QN"2">Has idt/tr>

on" w="dgle-contrIidogName Striix">&nbsrch.ntrol de>QN"2">

QN"2">Has idt/tr>

on" wd>QNHas idt/tr>on" wd>

on" tiImclasl>"><>

on" tiImclasl>"><>">tails s>

"2">inas>">tails s>

"2">

inas>

"2"><#t:HasFrrIZsssia-

"2">rIZenbuil i""src"rrIZenbuil lan ctailntrn ctailntrtr/line-289" e-ImlntrIZenIZel rIZenbuil ili:ata289""src#��:liili:="dgles u"Syitlan cteli:l rc/Agdlntline-28n cli:="dgles s>"2">"2">derIZbsssia-Syitlan cteli:l>"2">"2l lan ctailntrn ctailntrtr/line-289" e> :: ("2erIZbsssia-td> {
"2">PB (Source PB (Muil rIZenbu"2"de"#ml#t:PB" title="Agda.Auto.NarrowingSearch">PB (Subst PB (Muil rIZenbu"2"deAgda-Synta> (Subst t a, Muil rIZenbu"2"deAgda-Synnbuil ili:Muil rIZenbu"2"deAgda-Synta> (Su"2"deAgdantax">e.Class">Su class="def">ArnCompiler.Back.Compiler.Backe" class="lyPrompiler.agmas">Muil rIZenbu"2"deAgda-Synta> (Muil rIZenbref=" titlf=" title="Agdt">Fore" class="lyPragmas">Muil rIZenbu"2"deAgda-Synta> (Muil rIZenbu"2"deAgda-Synnbuil ili:Su"2"deAgdantax">e.Class">Su class="def">ArnSu class=""deAgda-Synnbuil">Muil rIZ/Agda.Auto.lle="Agdt">
Instances details

MonadTrans TCMT Source #

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

lift :: Monad m => m a -> TCMT m a

CatchImpossible TCM Source #

Like catchError, but resets the state completely before running the handler. This means it also loses changes to the stPersistentState.

The intended use is to catch internal errors during debug printing. In debug printing, we are not expecting state changes.

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

catchImpossible :: TCM a -> (Impossible -> TCM a) -> TCM a Source #

catchImpossibleJust :: (Impossible -> Maybe b) -> TCM a -> (b -> TCM a) -> TCM a Source #

handleImpossible :: (Impossible -> TCM a) -> TCM a -> TCM a Source #

handleImpossibleJust :: (Impossible -> Maybe b) -> (b -> TCM a) -> TCM a -> TCM a Source #

MonadFixityError ScopeM Source #

Instance details

Defined in Agda.Syntax.Scope.Monad

Methods

throwMultipleFixityDecls :: [(Name, [Fixity'])] -> ScopeM a Source #

throwMultiplePolarityPragmas :: [Name] -> ScopeM a Source #

warnUnknownNamesInFixityDecl :: [Name] -> ScopeM () Source #

warnUnknownNamesInPolarityPragmas :: [Name] -> ScopeM () Source #

warnUnknownFixityInMixfixDecl :: [Name] -> ScopeM () Source #

warnPolarityPragmasButNotPostulates :: [Name] -> ScopeM () Source #

MonadStConcreteNames TCM Source #

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

runStConcreteNames :: StateT ConcreteNames TCM a -> TCM a Source #

useConcreteNames :: TCM ConcreteNames Source #

modifyConcreteNames :: (ConcreteNames -> ConcreteNames) -> TCM () Source #

MonadInteractionPoints TCM Source #

Instance details

Defined in Agda.TypeChecking.Monad.MetaVars

Methods

freshInteractionId :: TCM InteractionId Source #

modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> TCM () Source #

MonadAddContext TCM Source #

Instance details

Defined in Agda.TypeChecking.Monad.Context

Methods

addCtx :: Name -> Dom Type -> TCM a -> TCM a Source #

addLetBinding' :: Name -> Term -> Dom Type -> TCM a -> TCM a Source #

updateContext :: Substitution -> (Context -> Context) -> TCM a -> TCM a Source #

withFreshName :: Range -> ArgName -> (Name -> TCM a) -> TCM a Source #

MonadDebug TCM Source #

Instance details

Defined in Agda.TypeChecking.Monad.Debug

Methods

displayDebugMessage :: VerboseKey -> VerboseLevel -> String -> TCM () Source #

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> TCM a -> TCM a Source #

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> TCM String Source #

getVerbosity :: TCM Verbosity Source #

isDebugPrinting :: TCM Bool Source #

nowDebugPrinting :: TCM a -> TCM a Source #

verboseBracket :: VerboseKey -> VerboseLevel -> String -> TCM a -> TCM a Source #

MonadStatistics TCM Source #

Instance details

Defined in Agda.TypeChecking.Monad.Statistics

Methods

modifyCounter :: String -> (Integer -> Integer) -> TCM () Source #

MonadWarning TCM Source #

Instance details

Defined in Agda.TypeChecking.Warnings

Methods

addWarning :: TCWarning -> TCM () Source #

MonadConstraint TCM Source #

Instance details

Defined in Agda.TypeChecking.Constraints

Methods

addConstraint :: Constraint -> TCM () Source #

addAwakeConstraint :: Constraint -> TCM () Source #

catchPatternErr :: TCM a -> TCM a -> TCM a Source #

solveConstraint :: Constraint -> TCM () Source #

solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> TCM () Source #

wakeConstraints :: (ProblemConstraint -> TCM Bool) -> TCM () Source #

stealConstraints :: ProblemId -> TCM () Source #

modifyAwakeConstraints :: (Constraints -> Constraints) -> TCM () Source #

modifySleepingConstraints :: (Constraints -> Constraints) -> TCM () Source #

MonadMetaSolver TCM Source #

Instance details

Defined in Agda.TypeChecking.MetaVars

Methods

newMeta' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> TCM MetaId Source #

assignV :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> TCM () Source #

assignTerm' :: MetaId -> [Arg ArgName] -> Term -> TCM () Source #

etaExpandMeta :: [MetaKind] -> MetaId -> TCM () Source #

updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> TCM () Source #

speculateMetas :: TCM () -> TCM KeepMetas -> TCM () Source #

MonadError TCErr TCM Source #

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

throwError :: TCErr -> TCM a #

catchError :: TCM a -> (TCErr -> TCM a) -> TCM a #

MonadError TCErr IM Source #

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

throwError :: TCErr -> IM a #

catchError :: IM a -> (TCErr -> IM a) -> IM a #

MonadBench Phase TCM Source #

We store benchmark statistics in an IORef. This enables benchmarking pure computation, see Agda.Benchmarking.

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

getBenchmark :: TCM (Benchmark Phase) Source #

getsBenchmark :: (Benchmark Phase -> c) -> TCM c Source #

putBenchmark :: Benchmark Phase -> TCM () Source #

modifyBenchmark :: (Benchmark Phase -> Benchmark Phase) -> TCM () Source #

finally :: TCM b -> TCM c -> TCM b Source #

HasFresh i => MonadFresh i TCM Source #

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

fresh :: TCM i Source #

Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source #

Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) Source #

Conversion TOM Type (MExp O) Source #

Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Type -> TOM (MExp O) Source #

Conversion TOM Term (MExp O) Source #

Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Term -> TOM (MExp O) Source #

Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source #

Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) Source #

Conversion TOM [Clause] [([Pat O], MExp O)] Source #

Instance details

Defined in Agda.Auto.Convert

Methods

convert :: [Clause] -> TOM [([Pat O], MExp O)] Source #

Conversion TOM (Arg Pattern) (Pat O) Source #

Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Arg Pattern -> TOM (Pat O)href="src/Agda.Auto.Convert.html#convert" class="link">Source #

Source #

Instance details

Defined in Agda.Auto.Convert

UnificationFailure

= UnifyIndicesNotVars Telescope Type.Auto.Convert.htmlVariable) -> TCMml#t:Term" title="Agda.Syntax.Interls-toggle-control details-toggle" data-details-id="i:id:TCMT:Conversion:21"> Conversion TOM (Name] -> ScopeM () TOMdError ScopeM () Instance details
Defined in CTree blk))
cthandles :: IORef [TOM [([Agda.TypeChecking.Monad.Base

Methods
(==) :: MExp to-NarrowingSearch.html#t:CTree" title="Agdass="src">refinements :: Renaming (ScopeM () MetaIdempty"> opeM () r>

Agda.TypeChecking.Monad.Base

Methods

(==) :: TCM a refinements :: :: (Impossible -> Maybe b) -> TCM a -> (b ->

builtinIZero :: String Sourceyntax-Concrclass="src"List" title="Agda.Auto.Syntax">ArgList refinements :: refinements :: refinements :: Sourceyntax-Concrclass="src"LltipleFixityD#t:O" title="Atml#catchImwingSearch.html#t:CTree" title="Agdass="src">refinements :: Sourceyntax-Concrclass=.Convele.html#cax-Abstract-Name.html#t:ModuleName" title="Agda.Syntax.Abstract.Name">ModuleName -> FilePath ->ipleFixityD#t:O" title="Atml#catchImwingSearch.html#t:CTree" title="Agdass="src">refinementrch.html#t:CTree> -> FilePath ->ipleFixityD#t:O" title="Atml#catchImwingSearch.html#t:CTree" title="Agdass="src">refinementrch.html#t:CTree> -> FilePath -&ghen-js-enabled">Instance details

Defined in Agda.TypeChecking.Monad.Base

ArgList #

uptance detailsModuleName -> FilePath ->ipleFixityD#t:O" title="Atax.html#t:Ms="link">Source #

Lens' (Map QName String) TCState

refinements :: #

Constraints

#

warnUnknownN :: IORef (Maybe (Constraints

#

warnUnknow

MonadFresh i TCM Source #

&nbslink">#

Source #

showsPrec :: Int -> convert" class="efinementrch.htm-Auto-Syntax NotLeqSort Source #

Source defaultDefn :: ArgInfo -> QName ->href="Agda-Syntax-Abstract-Name.html#t:Name" title="Agda.Syntax.Abstract.Name">Name -> Defn -> Definition

jsBackendName :: Arga>

yD#t:O" title="A>href=td>

NotLe1">

Instance details

Defined in Agda.TypeChecking.Monad.Base

Methods

an="2">

warnPolarity#t:QName" title=tulates :: [Name]="#v:UniltinAbs">builtda-Compiler-Backend.html#t:VerboseLeflink">#

In"4ance details

Defined in Agda.Auto.Convert

dataPattern) (Pat Source TCM a Source #

dataPattern) ( #

PatSource # TCM a

dataPattern) (Pa"link">Source<

ng" class="link">Source TCM a cthandles :: IORef [TOM<="#v:modifyCounter" class="selfl

O)PatSobugPrinting" class="selfstances details-toggle-control details-toggle"Verbosebsp;

O)Pat>ef="Agda>

TCM #

TOM<="#v:modifyCounter" class="selfl

O)

O)TOM<="#v:modifyCounter" class="selfl

O)

O)TCM a #

catchError :: TCM a -> (lass="link/a>

O)

">TOM<="#v:modifyCounter" class="selfl

O)

O)Ext:MonadMetaSolver" title="Agda.Compiler.Backend">MonadMetaSolver TOM<="#v:modifyCounter" class#
>O)#

arkea href=creteNames" cl >>ternal">Pattern) (Pat Source

cthandles :: IORef"-ndM clasax"rtackend.html#t:MeAuto-Syntax.hM class="selfld c�>O)

Patmary class="hide-when-js-enabled">Instance details

DefineCompiler.Backend">TCM a MExp class="link">Source #

TOM<="#v:modifyCounter" class#

>O)#

arkea href=creteNames" cl >>ternal">Pattern) ( -> InteractionPoints) -> TCM ()

Patmary class="hide-when-js-enabled">Instance details

DefineCompiler.Backend">TCM a MExp class="link"a-Comflink">#

arkea href=creteNames" cl >>ternry>

Defitax.html#t:MAgda.Compiler.Backend">ReduceM a

builtinAgdaLiteral :nd.html#t:-Comflink">#

arkea href=cr#

arkea href=creteNames" cl >>ternry>

Defitax.htle"rt.htm #

getVerbosity :: "2">

>O)#

arkea href=creteNames" cl >>ternal">Pattern -> ConcreteNames) -> ExpandM clasax"rt

l#t:KfreshIuteractionId" class=iler-Backend.html#t:TCM" title="Agda.Comd>

">"2">S">Liter"Agda-Compiler-Backend.html#t:ConcreteNames" title="Agda.Compiler.Backend">ConcreteNames) -> TCM :: (<>

O)

:: (

) -> MExa href="Agda-Compiler-Backend.html#ternry>

Def>

unctionFlag" title="Agda.Compiler.Backend">Functiond>

unctionFlag" title="Agda.Compiler.Backend"nctionFlag" title="Agda.Compiler.Backend">Functiond>

) -> MExa href="Agda-Compiler-Backend.html#ternry>

Def>

) -> MExa href="Agda-Compiler-Backend.html#ternry>

Def>

unctionFlag"end"nctionFlag" title="Agda.Compiler.Backend">Func;

TCMinkend.html#ternry>

Def>

) -> MExa href="Agda-Compiler-Backend.html#ternry>

Def>

O) Source er-Backend.html#ternry>

Def>

) ->

Def>

Funebug.html#forml#ternry>

Denvert">O) Source Conversion

) -> Source Co"Env mnvert.html#convert" class="link">Source Conversion

Conversion Functiond>

) ->

Def>tml#t:TCM" title="Agda.Compiler.Backend">TCM Source #

Conversion

NotLe1">

QName ->href=td>

Conversion Functiond>

) -&g>

Conversion Source #

) -&g>

TOM<="#v:m(ConversionConversion)/a> Functiond>

Source ) -&g>

="src clearfix">TOM<="#v:m(TOM<="#v:m(Source #

Functiond>

">TOM<="#v:m(MyMB (Maybe (ICArgList o, [MetaVariable -> MetaVariable) -> TCM () "Agda-Compiler-Backnk">Source #s="src gda.Auto->nting" cla="Agda-Auto-Syntax.html#t:ICArgList" title="Agda.Auto.Syntax">ICArgList o, [MetaVariable -> TCM a -> TCM a builtinAgdaLiteral :: String

">TO="Agda.Compiler.Backend">TCM () "Agda-Compiler-Backnk">Source TCCM" title="Agda.Compiler.Backend">TCM () "Agda-Compiler-Backngda.Compiler.Backend">TCM a builtinAgdaLiteral :: String

">TO="Agda.Compiler.Backend">TCM () "Agda-Compiler-Backnk">Source TCCM" title="Agda.Compiler.Backend">TCM () "Agda-Compiler-Backngda.Compiler.Backend">TCM a builtinAgdaLiteral :: Stra.TypeCheckinMonad="defa-details-id="i:id:EqReasoningState:Eq:1"> Eq

type lspan="2">

builtinAgdaLiteral :: Stra.TypeCheckinMonad= Source

Methods

convert :: lspan="2">

builad= Source

Methods

TCl#t:Lens-39-" Auto-Syntax.pan>

O)#

l#t:TCM" title="Agda.Compiler.Bac="caption"e="Agda.Auto.Convele.html#catchImwingSearch.html#t:CTree" title lspan="2">

builad= Source

Methods

TCl#t:Lens-39-" Auto-Syntax.pan> Name

builad= Agda.TypeChecking.Monad.BaseTOM<="#v:modifyCouBackend">l#tler.BackendAuto.Syntax">Pa href="#f="src/&aints">modifyAoml#HNNBlks" class="link">Source

Source

ra.TypeChecef="#>

TCl#t:Lens-39-" Auto-Syntax.pan> Pat

#

TCErr -> v:refinements="src/&aints"tr>on" tit.Co"6:Expan"sub/div>

ra.TypeChecef="#>

TCNodeK PostLeftsK Pre.Auto.Convele.html#catchImwingSearch.n="2">

builad= #

arkea href=Internal.html#t/a> <="2"ef="#v:formatDebugMessage" class="selflink">#

showsPrec :: Int -> convert" class="efinementrch.htm-Auto-Syntax NotLeqSort Source TCErr -> vK Pre.Auto.Convele.html#catchImwingSearch.n="2">

ra.TypeChecef="#>

TCNodeK PostLeftsK Pre.Auto.Convele.html#catchImwingSearch.n="2">

Source TCNodeKhowsPrec :: Int -> Soselhtml#t:TCErr" title="Agda.Compiler.Backend">TCErrPat

Source TCNodeKhowsPrec :: Int -> TCErrSougda-Compiler-Backend.html#t:Polarity" tirt" claSyntatle="Agda.ref="#v:modifyCou.Utils.Benchma"#v:modifyCou.Utils.Benchmark.=="selflinknm>

Source showList :: [ :: Int -&gr-Backend.html#t:Polarity" title="Agda.Compiler.Backend">convert" class="efinementrch.htm-Auto-Syntax NotLeqSort Source #

:: Int -&gr-Backend.html#t:Polarity"CM" class="selhtml#t:TCErr" tigt; UIdConvert

TCM a Atml#t:TCM" title="a>)uto-Convert.html#t:O" title="Agda.Auto.Convert">O], UIdConvert

TCM ref=".Auto.Syntax"rec :: Int -&gr-Backend.html#t:Polarity"CM" class="seltml#t:MonadD.Compiler.Bacleft">end.html#t:TCM,>mmit :: String

UIdConvert

TCM ref=".Auto.Syntax"rec :: Int -&gr-Backend.html#t:Polarity"CM" class="seltml#t:MonadD.Compiler.Bacleft">Atml#t:TCM" title="a>)uto-Convert.html#t:O" title��.html:: String

Agda.TypeChecking.MetaVars

o)] Source

getsBenchmark :: ( :: Int -&gr-f="#uto-Convert.html#t:O" title��.html:: String

">O"instance details-toggle-controla :: Strods

:: ( arkea href=creteNames" cl >>ternal">li>

="inst-left NotLe1">��a href="Agda-Utils-Benchmark.html#t:MonadBench" title> ::>O"instance details-toggle-controla :: Strods

Recompile menv

| Skip mod

dataSource

:: Strods

Recompile menv

| Skit">="inst-left NotLe1">��a href="Agda-Utils-Benchmark.html#t:MonadBench" title> ::>O"instance details-toggle-controla :: Strods

Recompile menv

| oggle-controla :: Strods

NotLe1">��a href="Agda-Utils-Benchmark.html#td>nd">TCMink">Source<Pattd>

O)builtinUnitUnit :: String Source Recompilrce<

Recompilend">TCMink">Source<

::>O"instance details-toggle-controla :: Strods

Recompile menv

| d>

OMyGtOs"eqSort">NotLe1">��a href="Agda-Utils-Benchmark.html#

)builtinUnitUnit :: String Source<=>#v:Recompile">Recovert.html#t:t:Conversih title="Agda.Syn"�tey2">

::>O"instance details-toggle-controla :: Strods

Recompile menv

| d>

OMyGtOs"eqSort">NotLe1">��a href="Agda-Utils-BenchmarkqSort">NotLe1">��a href="Agda-Utils-Benchmark.html#

MonadError Instance details#

TOM<="#v:modifyCounter" class#

>O)#

arkea href=creteNames" cl >>ternal">Pattern) ( -> InteractionPoints) -> MonadError #

InteractionPoints) ->

>O)Skit title="Agda.Utils.Except">MonadError #

arkea h" title="Agda.Compief="Agda-Auto-k"a-Comflitml#t:KfreshIuteractionId" class=iler-Backend.ht

MonadError #

arkea h" title="Agda.Compief="Agda-Auto-k"a-Comflitml#t:KfreshIuteractionId" class=iler-Backend.ht

Functiond>

) -> InteractionPoints) ->

>OFunctiond>) ->

) ->iond>

&nbrc/Agda.Typegda.Syntax.Abstract.Name">QN"2">Has idt/tr>

rfix">

&nble="as/tr>

Su"2il ili:
il ili:Muil rIZ/Agda.Auto.lle="Agdt">Su"2Su"2S>Su"2gda.Compiler.Backend">MonadTCEnv m, Muil rIZ/Agda.Auto.lle=>Agdt">Su"2
"deA">"deA">o catch inf="#v:detecterIZbsssiaclass="src clearft">Su"2Su"2
Defined in Agda.Tyspanf=" a-detairs-id="gda."#o.lref=>ttute.Class">Su->
"deuil rIZ/Aid="gda."#o.a href="#v:codetails>lref="4.lref="#v:s="subs">
=
"deA">"deA">o catch inf="#v:detecttml">Agda.Tyspanf=" a-detairs-id="gda."#o.lref=>ttute.C>Agda.Tyspanf=" a-detairs-id="gda."#o.lref=>ttute.Claeuil rIZ/AidAid="gda."#o.a href="#v:codetails>lref="4.lref="#v:s="subs">
=
"deA">"deA">o catch inf="#v:detecttml">Agda.Tyspanf=" a-detairs-id="gda."#o.lref=o catch inf="#v:detecttml">Agda.Tyspanf=" a-detairs-id="gda."#o.lref=>ttute.C>Aglnordtit>="#v:formatDebugMessage" class="selflink">#
o catch inf="#v:detecttml">Agda.Tyspanf=" a-d.a href="#v:codackend">TCErr m, Agda.Tyspanf=" a-detairs-id="gda."#o.lref=>ttute.C>Aglnordtit>="#v:formatDebugMessage" class="selfl:formatDebuZ/Aid="gda."#o.lrclass="src sho"#v:dete.li:;TCErr m, Agda.TTCErr m, Highlightinsage" class="selttute.C>Aglnord=" a-detairs-i"="gdayspanf=" a-detairs-id="gda."#o.lref=>ttute.C>Aglnordtito.lrclass="src sho"#v:dete.li:;Agda.Tyspanf=" a-detairs-id="gda."#o.lrddsho"#v:dete.li:;lref=>ttute.C>Iaighlightinsda.TTCErr mref="A(1ch inf="#v:deto catch inf="#v:detecttml">Agda.uiltinAgd="gda."#o.lref=o catch inf="#v:detecttml">Agda.TTCErr m, Higehd">Highlightpan="2">
vnord=" a-detairs-i"="gdayspanf=" a-detairs-id="gda."#oto.lrclass="src sho"#v:dete.li:;Iaighlightinsl">Agda.Tyspanf=" a-detairs-id="gda."#o.lrddsho"#v:dete.li:;lref=>ttute.C>Iaighlightinsda.TTCErr mref="A(1ch inf="#v:deto catch inf="#v:detecttml">Agda.uiltinAgd="gda."#o.lref=o catch inf="#v:detecttml">Agda.TTCErr m, Iaighlightinsl">Agda.Tyspanf=" a-detairs-id="gda."#o.lrddsho"#v:dete.li:;lref=>ttute.C>Iaighlight="#v:tecttml">Agda.l#t:ICExp"o catch inef=>ttute.C>Ia/>lref=>ttute.oetairs-id="gdag"A(1ch inf="#v:deto catch inf="#v:detecttml">Agda.uiass="sris list of="#v:detecttml"etecttml">Agoetairs-id="insl">Agda.Tyspanf=" a-detairs-id="gda."#o.lrddsho"#v:dete.li:;lref=>ttute.C>Iaighlight="#v:tecttml">Agda.l#t:ICExp"o catch inef=>ttute.C>Ia/>lref=>ttute.oetairs-id="gdag"A(1ch inf="#v:d omrssg v:det te.C>Ia/>lref=>tiass="sris list p >5 inC>Iaighlightinsl">Agda.Tyspanf=" a-detairs-id="gda."#o.lrddsho"#v:dete.li:;lref=>ttute.C>Iaighlight="#v:tecttml">Agda.l#t:ICExp"o catch inef=>ttute.C>Ia/>lref=>ttute.oetairs-id="gdag"A(1ch inf="#v:deto catch inf="#v:detecttml">Agda.uiass="sris list of="#v:detecttp >5 inC>Iaigute.C>Iaighlight<.ass="sris listsl">Agda.Tyspa inf="#v:d omute.oetairs-idda."#o.lrddsho"#v:dete.li:;lref=>ttute.C>Iaighlight="#v:tecttml">Agda.l#irs-id="gdag"A(1ch inf="#v:deto catch inf="#v:detecttml">Agda.uiass="sris list of="#v:detecttp >5 inC>Iaigute.C>Iaighlight<.ass="sris listsl">Agda.Tyspa inf="#v:d omute.oetairs-idda."#o.lrddsho"#v:dete.li:;lref=>ttute.C>Iaighlight="#v:tecttml">Agda.l#irs-id="gdag"nf="#v:detecttlight<.ass="sri="#v:d omute.oehlight<.asse.oetairs-i 2rddsho"#v:dete.liairs-idda."#o.lrdReplace" class="selflink">#
on" titpan> PatSource
on" t�Ausy.>3Dndsye tr>on" titpan>
on" t�Ausy.>3Dndsye tr>on" titpan> "#v:5 inCwo">e."doc ems="doc�a> �Xt

EE ( "doc�a>
ances"doc em ems="doc ems="doc ems="doc ems="doc ems="doc ems="docSyntax.html#t:EE" title="Agda.Auto.Syntax">EE (
on" t�Ausy.>3Dnds.Syntax">Es="doc ems"ref="Agda-Auto-Syntax.html#t:MyMB" title="Agd="doc "doc�a>
e."doc ems="doc�� Int -&�lacess61" co an s)0 0>src clearf">EE (3Dnds.Syntax">
on" t�Ausy">Es="doc eeltax">EE ances"doc em ems="doc ems="doc ems="do semdoc ems="doc emu"Agda-Auto-Syntaiv an ss=f sr.Cos">
3Dnds.Syntax">
on" t�Ausy">Es="doc eeltax">EE Es="doc eelta"doc em ems="d#t:Clion on" t�Ausy">Edoc em ems="d#t:Clion > > Es="don #v:convert" cl.Compiler. hion > !{io Es="don #v:convert" cl.Compiler. hion > hion hion > hion <>11>hion )1> > > < hion #v:convert" cl.Compiler. hion > /a> #v:convert" c/a> ass="keyword">daion)> Pk > hion <>11>hion )1> > /a> /a>gcl.Ca> h> #v:convert" cl.Compiler. hiona> > ionk#v:convert" c/a> ass="k >d>to-Syntax.html#t: /a>gcl.Ca>> h> a href="src/Agda.Auto.Convert.html#ly">hio <>1a hio ex >ex.Positioo ht >ex.Posdionex.Positi /a>gcl.Ca>> h> a href="src/Agda.Auto.Convert.html#line-321" class="link">Source #on" tiImclasl>"> E <>ypeCheckinMls-id=pan> Eq q:1"> Eq
>t >h"s id.Convhref="Agda-A-ConCon
/.HasFresh"s s="s> (Maybe!sn <>ypeCheckinMonad="pan> Eq q:1"> Eq
>t >h"s id.Convhref="Agda-A-ConCon
<>on" tgda-A-ConCon
/.HasFree="as/tr>
o:Con/span> Ees" cl >> Eq
Ees%/div>
/.Hbiv>
/.Hv>
/.HasFrr>
on" tgda-A-ConCon
/.HAConvhref="Agda-A-ConCon > Ebs"h/
class="efinementrch.htm-Auto-Synas:3"> ExpandMetasd.Base.html#runStConcreison" title="Agda.Compiler.Backeclass="efinementrch.htm-Auto-Syntax NotLeqSort#tr>##

Muil rIZ/Agda.Auto.lle=>Agdt">Su"2Su"2Su"2gda.Compiler.Backend">Mo>
Agda.TyspA(1ch inf="#v inf="#v:deto1ch inf="#d omute.oetairs-idda."#o.lrddsho"#v:dete.li:;lref=>ttute.C>Iaighlightsl">Agda.Tyspa inf="#v:d omute.oetairs-idda."#o.lrddsho"#v:dete.lttlight<.ass="ieid="gdaghtinsage="Agda.Compilel">Agda.l#irs-s="sri="#v="gdag"nf="#v:detecttlight<.ass="sri="#v:d omute.oehli��&ace" class="senflink">##	Agda.TyspA(1ch inf="#v inf="#v:deto1ch inf="#d omute.oetairs-idda."#o.lrddsho"#v:dete.li:;lref=>ttute.C>Iaighlightsl">Agda.Tyspa inf="#v:d rddsho"#v:deteidda."#o.lrddsho"#v:dete.lttlight<.ass="ieid="gdaghtinsage="Agda.Compilel">Agdaete.liairs-idda."#o.lrdReplace" class="selflink">#	#lref=>ttute.C>Iaighlightsl">Agda.Tyspa inf="#v:d rddsho"#v:mnsage="Agda.Compiho"#v:dete.ltto detart">TOM<="#v:modifyCounter" class="selfl	O)Patlref=>ttute.C>Iaighligheplace" class=e.liairstd clali��&ace" claslace" claslass="doc emputo.stte.li:;<="selflink"#v:5 inCwo">e.liairstd class="doc etecttp >5 inC>Iaigute.C>Iaighlight<.ass="sris/span"src clearfix">PatTO"insttp >5 inC>Iaigute.C>Iaighlight<.ass="sris listte.li:;lref=>ttute.C>ast-left">e.>lref=>ttute.C>:5 inCwo">e.listte.li:;lrdoc etecttp >5 inC>Iaigute.C>Iaighlight<.ass="sris/span"src clearfix">ighligheplss=e.liairstd clali��&ace" claslace" claslass="doc empuCtto detart"n"src clearfix">Patlref=>ttss="sris listte.li:;lref=>ttute.C>ast-left">e.>lref=>te.>lref=>ttute.C>:5 inCwo">e.listte.li:;ttute.C>ast-left">e.>lref=>ttute.C>:5 inCwo">e.listte.li:;lrdoc etecttp >5 inC>Iaigute.C>Iaighlight<.ai��&ace" caigute.C>Iaighlight<.ass="sris/span"src clearfix">ighligheplss=e.liairstd clali��&ace" claslace" claslass="doc empuCtto detart"n"src clearfix">Patlref=>ttss="sris listlight<.ass="sris/span"src clearfix">PatTO"insttp >5 inC>Iaigute.C>Iaigpan cnk"#v:5 i_ 7fix">PatPatlref=>ttss="sris listligh��А<��lace" clasla detart"n"src clearfix">PatTO"insttp >5 inC>Iaigute.C>Iaigpan cnk"#v:5 i_ 7fix">PatPatTO"instix">PatPatPatPatPatPaan cl>PatInstance details Defined in PatPatPat
O>)> Pk hion <>11>hion )1> > > /a>gcl.Ca>> h> hion )a>hionndne"62>21 ;ion >d>er. hiona> > ionk hion< hion >d><	O>a>hionndne"62>21 ;ion >d>er. hiona> > <hio <>1a hio ex.Position">Ran /a>gcl.Ca>> h> a href="src/Agda.Auto.Convert.html#line-321" class="link">Source #	class="selflink">#	hio">#	class="selflink">#piler. hion /a>gcl.Ca>> h> a href="src/Agda.Auto.Convert.html#ly">hio <>1a hio ex >ex.Positioo ht >ex.Posdionex.Positi /a>gcl.Ca>> h> a href="src/Agda.Auto.Convert.html#line-321" class="link">Source Source #1a hio ex >ex.Positioo ht >ex.Posdionex.Positi <>>t >ex.PosdioPositi ex.Positi /a>gcl.Ca>> h> a href="src/Agda.Auto.Convert.html#line-321" class="link">Source o <>1asion" cex.Positi /a>gcl.Ca>> h> a href="srionex.Positi <>>t >ex.PosdioPositi ex.Positi /a>gcl.Ca>> h> a href="src/Agda.Auto.Convert.htlink">#1a hio ex >ex.Posex.Positi )a>hina>/a>gcl.Ca>> h> a href="srionex.Positi <>>t >ex.PosdioPox.Posdiref="s/a hion/a>gcl.Ca/a> o ti ex)link">#>#>#>#>#>#>#>Agda.Auto.C<>1a hiti /a>gcl.Ca>> h> a href="srionex.Positi <>>t > hion /a>gcl.Ca>> h> a href="src/Agda.Auto.Convert.htlink">#dioPo> >t >ex.Posk <>>#>t >n <>>#>#>#>Agda.Auto.C<>1a hiti /a>gcl.Ca>> h> a href="srionex.Positi <>>t > hion /a>gcl.Ca>> h> a href="src/Agda.Auto.Convert.htlink">#dioPo> #dioPo> >t >ex.Posk <>>#>t >n <>>#>#>#>Agda.Auto.C<>1 hion/aa> /a>gcl.Ca>> h> a href="src/Agda.Auto.Convert.htlinhref="sn <>dioPo> /a>gcl.Ca>> h> a href="src/Agda.Auto.Convert.htlink">#dio.Convert.htlinsk <>>#>a hi. #>#>Agda.Auto.C<>1 hion/ax.Posf:htlink">#dioPo> >t >ex.Posk <>>#>t >n <>hion/a>>#>Agda.Auto.C<>1 hion/.Auto.Converda.Auto.Convhref="Agda-A-ConCon t >n <>>#>#>A
&nbrc/Agda.Typegda.Syntax.Abstract.Name">QN"2">t >n <>>#
MyMB (Maybe!sn <>dhio hion"2">t >n <>>#piler-Backend.html#t:Cons/tr>
MyMB (Maybe!sn <>dhio hiontra.TypeCheckinMonad="defa-details-id="i:id:EqReasoningState:Eq:1"> Eq type#>t >h"s idogg=">>#">
MyMB (Maybe!sn <>dhio hiontra.TypeCheckinMonad="defa-details-id="i:id:EqReasoningState:Eq:1"> Eq /.HasFresh"s s="s> (Maybe!sn <>ypeCheckinMonad="pan> Eq q:1"> Eq >t >h"s id.Convhref="Agda-A-ConCon
type#>t >h"s idogg=">>#">
type#>t >h"s idogg=">># /.HasFres" cl >>) E <>ypeCheckinMls-id=pan> Eq q:1"> Eq >t >h"s id.Convhref="Agda-A-ConCon /.HasFresh"s s="s> (Maybe!s>>t >h"s id.Cors/tr>
Eq as/tr>
Eq as/tr>
HasFrr>	on" tgda-A-ConCon /.HAConvhref="Agda-A-ConCon > Ebs"h/<>> Ebs"h/<>> Ebs"h/<>> <>> Ebs"h/<>> Eb"subsa-A-Cond="subs"h/<>> Ebs"h/<>> Eb"s/<>> Eb"subsa-Aubs"h/Functiond>MExp class="linkubs"h/<>> Ebs"h/<>> <>>nd>MExp class="l) h/Functiond>MExp class="linkubs"h/ (<>> <>>nd>Mendnd.hasConCon (<>> <>> / :: aints :: aints :: aints :: aints :: aints :: aints :: aints :: aints :: aints :: aints#t:CTree"title="/ :: aints :: aints :: aints :: aints :: aints :: aints :: aints :: aintss=tlegdass=tlegdass=t.Auto.li:; :: rc/AgdlntrIRtml#linegda.Syntax.l#linegda.Syntass=tlegdass=t.Auto.li:; :: rc/AgdlntrIRtml#linegda.Syntax.l#linegda.Syntass=tlegdass=t.Auto.li:; :: aints :: aintss=tlegdass=tlegdass=t.Auto.li:dass=t.Auto.nbuil itmlss=t.Auto.li:dass=t.Auto.nbuil itmlss=t.Auto.li:dass=t.Auto.nbuil itmlss=t.A> :: rc/Agda.Syntax.l#linegda.Syntass=tlegdass=legdass=t.Auto.li:o.li:; :: rc/AgdlntrIRtml#linegda.Syntax.l#linegda.Syntass=tlegdass=t.Auto.li:;TCM a -> TCM a :: rc/AgdlntrIRtml"7ss=ledass=bbAuto.nbCos-Auto-="Agdiler.Backend">TCM a -> a ckend">AgdlntrIRtml"7ss=ledass=bbAuto.nbCos-Auto-="Agdiler.Backend">TCM a -> builad= a -> TCM a -> Trav (TCM a -> a -> Source Agda.Compiler.Common Es="doc eelta"doc em ems="d#t:Clion Muil > 6c >gdale="Ag-> gdBackea -> gda-Autonk#medoc ems"ref="Ahion gda-Autonk#medoc ems"le.dile\|edht; ; gdBackeatttle="AAuto-="Agdileh"doc e.dile\|edht; ; gdBackeatttle="AAuto-="Agdileh"doc ems"reomp.; 5 inC>Iaigute.C>Iaighlight<.ass="sris listsl">Agda.Tyspa inf="#v:d omute.oetairs-idda."#o.lrckea -> Iaighlight<.ass="sris listsl">Agda.Tyspa inf="#v:d omute.oetairs-idda."#o.lrckea -> Iaighlight<.ass="sris listsl">Agda.Tyspa inf==ledt -Cos-Auto-="ie"sris list="#-Autonk#marme�irs-idda."#o.lrckea -> Agda.Tysptax">Elr o) (8�">Elr o) (8�">Elr o) ( a I�irs-idda."#tonk#marme� Inckea -ckea -> a I�irs-idda."#tonk#marme� Inckea -ckea -> :: Int -&gr-Backend.html#t:Polarity" title="Agda.Compiler.Backend">convert" class="efinementrch.htm-Auto-Syntax NotLeqSort Source #
Import

#
NotLeqSort :: Int -&gr-Backend.html#t:Polarity" title="Agda.Compiler.BackendNotLeqSort

#


#
>
#

td class="src">
#

>

#



		Hanl}nmnotd class="doc empty">
#	>		< s="src">		Hanl}nmnotd class="doc empty">

#>		< s="src">	< s="src">		< s="src">	:: String builtinNatTimes :: String builtinNatDivSucAux :: String :: String builtinNatTimes :: String builtinNatDivSucAux :: String builtinNatDivSucAux :: String :: String :: String builtinNatDivSucAux :: String builtinNatDivSucAux :: String :: String builtinNatDivSucAux :: String builtinNatDivSucAux :: S"aoclass="src short)>builtinNatDivSucAux :: String	::="Agda.Compiler.Backend">Flag opts)] isEnabled :: opts -> Bo/th>	None builtinNatDivSucAux :: S"aoclass="src short)>ails-toggle-control details-toggle" � Inckea id="v/tr>
::="Agda.Compiler.Backendr>
Source #
ails-toggle-control details-ler.Backendr>
Source SizeMaxView Pri PB Source SizeMaxViewrking">PhaseSizeMaxView Sovrce SizeMaxViewrking">Phase -> Constr -> c class="link">Sovrce SizeMaxViewrking">Phase -> Constr -> c SizeMaxViewrking">Phase ->ss="src shor kend">SizeMaxView<-Coei class="src shor-> -> Constr -t"4s="src shorSynss="src short"" cort"> SizeMaxViewrking">Phase -> Constr -t"4s="src shorSynss="src short"" cort">ClashingModule rking">Phaend">SizeMaxViewrking">Phase -> Constr -t"4s="src shorSynss="src short"" cort">rking">Phaend">SizeMaxViewrking">Phase -> Constr -t"4s="src shorSynss="src short"" cort">rking">Phaend">SizeMaxViewrking">Phase -> Constr -t"4s="src shorSynss="src short"" cort">rking">Phaend">SizeMaxViewrking">PhaseSource SizeMaxViewrking">Phase SizeMaxViewrking">Phase SizeMaxa> Phase \| ="src shckenConstr -t"hor kend">SizeMaxViewrking">PhasePhase -> Constr -t"4s="src sef="#v"Ag/a> SizeMaxa> ew ="src shckenConstr -t"hor kend">SizeMaxViewrking">Phase"Agda-Syntax-Abstraclass="src shor kencarch.hi>\| ="src shckenaseSizeMaxViewrking">PhasePhase ewSizeMaxa> ew ="src shcken">where PhasePhase ="src shcken">wherePhasePhase SizeMaxVis kc line-1mpilcdks">="src shcken">wherePhase="src shcken">where="src shcken"src sh="s kc line-1mpilcdks">="src shcken">where ="src shckenConstr -t"hor kend">SizeMaxViewrking">Phase"Agda-Synt"src sh="src line-17" cPhase where="src shckenaseSizeMaxV href="#li claPhase="src shckenConstr -t"hor e"Agda-Synt"src sh="src line-17" cPhase ="src shcken">where where ="src shcken">where Sou/a> where ="src shcken">where ="src shcken">where ="src shcken">where ="src shcken">where="s="src shf="#li sh="s kc line-1mpilcdks">="src shcken">where ="src shcken">whcdks"rc"="src shcken">where="src shcken">wne="#li cla sh="s kc line-="src"src scdPhase"Agda-Syntax-Abstraclass="src shor kencs">="src shcken">where="s="src shf="#li sh="s kc line-1mpilcdks">="src shcken">where ="src shcken">where="src shcken">where="s="src shf="#li sh="s kc line-1mpilcdks">="src shcken">where

Documentation

Instances

Instances

Instances

Instances

Instances

EE ( "doc�a> ances"doc em ems="doc ems="doc ems="doc ems="doc ems="doc ems="docSyntax.html#t:EE" title="Agda.Auto.Syntax">EE (

ances"doc em ems="doc ems="doc ems="doc ems="doc ems="doc ems="docSyntax.html#t:EE" title="Agda.Auto.Syntax">EE (

e."doc ems="doc� � Int -&�lacess61" co an s)0 0>src clearf">EE (3Dnds.Syntax">

3Dnds.Syntax">

EE ( "doc�a>
ances"doc em ems="doc ems="doc ems="doc ems="doc ems="doc ems="docSyntax.html#t:EE" title="Agda.Auto.Syntax">EE (

e."doc ems="doc�� Int -&�lacess61" co an s)0 0>src clearf">EE (3Dnds.Syntax">