Safe Haskell	None
Language	Haskell2010

Mikan.TypeChecking.Monad.Builtin

Synopsis

pattern EqualityType :: Range -> Sort -> QName -> Args -> Arg Term -> Arg Term -> Arg Term -> EqualityView
bindBuiltinName :: BuiltinId -> Term -> TCM ()
bindPrimitive :: PrimitiveId -> PrimFun -> TCM ()
boldPathView :: Type -> PathView
builtinPrimitives :: [PrimitiveId]
constrainedPrims :: [PrimitiveId]
constructorForm :: HasBuiltins m => Term -> m Term
constructorForm' :: Applicative m => m Term -> m Term -> Term -> m Term
constructorFormer :: HasBuiltins m => m (Term -> Term)
eqtLhs :: EqualityView -> Arg Term
eqtName :: EqualityView -> QName
eqtParams :: EqualityView -> Args
eqtRange :: EqualityView -> Range
eqtRhs :: EqualityView -> Arg Term
eqtSort :: EqualityView -> Sort
eqtType :: EqualityView -> Arg Term
equalityView :: Range -> Type -> TCM EqualityView
getBuiltin :: (HasBuiltins m, MonadTCError m) => BuiltinId -> m Term
getBuiltin' :: HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltinName' :: HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName_ :: (HasBuiltins m, MonadTCError m) => BuiltinId -> m QName
getName' :: (HasBuiltins m, IsBuiltin a) => a -> m (Maybe QName)
getNameOfConstrained :: HasBuiltins m => PrimitiveId -> m (Maybe QName)
getPrimName :: Term -> QName
getPrimitive :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => PrimitiveId -> m PrimFun
getPrimitive' :: HasBuiltins m => PrimitiveId -> m (Maybe PrimFun)
getPrimitiveName' :: HasBuiltins m => PrimitiveId -> m (Maybe QName)
getPrimitiveTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => PrimitiveId -> m Term
getPrimitiveTerm' :: HasBuiltins m => PrimitiveId -> m (Maybe Term)
getTerm :: (HasBuiltins m, IsBuiltin a) => ShortText -> a -> m Term
getTerm' :: (HasBuiltins m, IsBuiltin a) => a -> m (Maybe Term)
infallibleSortKit :: HasBuiltins m => m SortKit
intervalSort :: Sort
intervalUnview :: HasBuiltins m => IntervalView -> m Term
intervalUnview' :: HasBuiltins m => m (IntervalView -> Term)
intervalView :: HasBuiltins m => Term -> m IntervalView
intervalView' :: HasBuiltins m => m (Term -> IntervalView)
isEqualityType :: EqualityView -> Bool
isIOne :: IntervalView -> Bool
isPathType :: PathView -> Bool
isPrimitive :: HasBuiltins m => PrimitiveId -> QName -> m Bool
litType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => Literal -> m Type
mkSortKit :: QName -> QName -> QName -> QName -> QName -> QName -> SortKit
pathUnview :: PathView -> Type
pathView :: HasBuiltins m => Type -> m PathView
pathView' :: HasBuiltins m => m (Type -> PathView)
primAbs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAbsAbs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaBlocker :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaBlockerAll :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaBlockerAny :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaBlockerMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaClause :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaClauseAbsurd :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaClauseClause :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaDefinition :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaDefinitionDataConstructor :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaDefinitionDataDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaDefinitionFunDef :: (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
primAgdaDefinitionRecordDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaErrorPart :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaErrorPartName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaErrorPartPatt :: (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
primAgdaLitChar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaLitFloat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaLitMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaLitNat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaLitQName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaLitString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaLiteral :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaPatAbsurd :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaPatCon :: (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
primAgdaPatVar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaPattern :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaSort :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaSortInf :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaSortLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaSortProp :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaSortPropLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaSortType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaSortUnsupported :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCM :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMAskExpandLast :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMAskNormalisation :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMAskReconstructed :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMAskReduceDefs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMBind :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMBlock :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMCatchError :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMCheckFromString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMCheckType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMCommit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMDebugPrint :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMDeclareData :: (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
primAgdaTCMDefineData :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMDefineFun :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMExec :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMExtendContext :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMFormatErrorParts :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMFreshName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMGetContext :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMGetDefinition :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMGetInstances :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMGetType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMInContext :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMInferType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMIsMacro :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMNoConstraints :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMNormalise :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMPragmaCompile :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMPragmaForeign :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMQuoteOmegaTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMQuoteTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMReduce :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMReturn :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMRunSpeculative :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMSolveInstances :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMTypeError :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMUnify :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMUnquoteTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMWithExpandLast :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMWithNormalisation :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMWithReconstructed :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTCMWithReduceDefs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTermCon :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTermDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTermExtLam :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTermLam :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTermLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTermMeta :: (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
primAgdaTermUnsupported :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAgdaTermVar :: (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
primArgArgInfo :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primArgInfo :: (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
primAssocNon :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primAssocRight :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primBool :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primChar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primCons :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primEquality :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primEqualityName :: TCM QName
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
primFaceForall :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primFalse :: (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
primFloat :: (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
primGlue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primHComp :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primHidden :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primHiding :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primIMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primIMin :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primINeg :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primIOne :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primIZero :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primInstance :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primInteger :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primIntegerNegSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primIntegerPos :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primInterval :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primIntervalUniv :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primIsOne :: (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
primItIsOne :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primJust :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primLevel :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primLevelMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primLevelSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primLevelUniv :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primLevelZero :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primList :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primMaybe :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primNat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primNatDivSucAux :: (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
primNatMinus :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primNatModSucAux :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primNatPlus :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primNatTimes :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primNil :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primNothing :: (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
primPath :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primPathP :: (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
primPrecedence :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primProp :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primPropOmega :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primQName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primRefl :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primSSetOmega :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primSigma :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primStrictSet :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primString :: (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
primSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primTrans :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primTranspProof :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primTrue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primTypeOmega :: (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
primVisible :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primZero :: (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_glueU :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
prim_unglue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
prim_unglueU :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
runBuiltinAccess :: TCState -> BuiltinAccess a -> a
setBuiltinThings :: BuiltinThings -> TCM ()
sortKit :: (HasBuiltins m, MonadTCError m) => m SortKit
newtype BuiltinAccess a = BuiltinAccess {
- unBuiltinAccess :: TCState -> a
}
data EqualityTypeData = EqualityTypeData {
- _eqtRange :: Range
- _eqtSort :: Sort
- _eqtName :: QName
- _eqtParams :: Args
- _eqtType :: Arg Term
- _eqtLhs :: Arg Term
- _eqtRhs :: Arg Term
}
class EqualityUnview a where
- equalityUnview :: a -> Type
data EqualityView
- = EqualityViewType EqualityTypeData
- | OtherType Type
- | IdiomType Type
class (Functor m, Applicative m, Monad m) => HasBuiltins (m :: Type -> Type) where
- getBuiltinThing :: SomeBuiltin -> m (Maybe (Builtin PrimFun))
data IntervalView
- = IZero
- | IOne
- | IMin (Arg Term) (Arg Term)
- | IMax (Arg Term) (Arg Term)
- | INeg (Arg Term)
- | OTerm Term
data PathView
- = PathType {
  - pathSort :: Sort
  - pathName :: QName
  - pathLevel :: Arg Term
  - pathType :: Arg Term
  - pathLhs :: Arg Term
  - pathRhs :: Arg Term
  }
- | OType Type
data SortKit = SortKit {
- nameOfUniv :: UnivSize -> Univ -> QName
- isNameOfUniv :: QName -> Maybe (UnivSize, Univ)
}
module Mikan.Syntax.Builtin

Documentation

pattern EqualityType :: Range -> Sort -> QName -> Args -> Arg Term -> Arg Term -> Arg Term -> EqualityView Source #

bindBuiltinName :: BuiltinId -> Term -> TCM () Source #

bindPrimitive :: PrimitiveId -> PrimFun -> TCM () Source #

boldPathView :: Type -> PathView Source #

builtinPrimitives :: [PrimitiveId] Source #

Identifiers of "primitive" functions which must be given a user-written definition and bound by a BUILTIN pragma, instead of being defined in a primitive block.

constrainedPrims :: [PrimitiveId] Source #

Primitives with typechecking constrants.

constructorForm :: HasBuiltins m => Term -> m Term Source #

Rewrite a literal to constructor form if possible.

constructorForm' :: Applicative m => m Term -> m Term -> Term -> m Term Source #

constructorFormer :: HasBuiltins m => m (Term -> Term) Source #

Produce a function that rewrites a literal to constructor form if possible.

eqtLhs :: EqualityView -> Arg Term Source #

eqtName :: EqualityView -> QName Source #

eqtParams :: EqualityView -> Args Source #

eqtRange :: EqualityView -> Range Source #

eqtRhs :: EqualityView -> Arg Term Source #

eqtSort :: EqualityView -> Sort Source #

eqtType :: EqualityView -> Arg Term Source #

equalityView Source #

Arguments

:: Range	Range of the `rewrite` expression, if any.
-> Type	Identity type?
-> TCM EqualityView

Check whether the type is actually an equality (lhs ≡ rhs) and extract lhs, rhs, and their type.

Precondition: type is reduced.

getBuiltin :: (HasBuiltins m, MonadTCError m) => BuiltinId -> m Term Source #

getBuiltin' :: HasBuiltins m => BuiltinId -> m (Maybe Term) Source #

Returns Nothing if built-in is not bound or bound to a Prim.

getBuiltinName' :: HasBuiltins m => BuiltinId -> m (Maybe QName) Source #

getBuiltinName_ :: (HasBuiltins m, MonadTCError m) => BuiltinId -> m QName Source #

getName' :: (HasBuiltins m, IsBuiltin a) => a -> m (Maybe QName) Source #

getNameOfConstrained :: HasBuiltins m => PrimitiveId -> m (Maybe QName) Source #

getPrimName :: Term -> QName Source #

getPrimitive :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => PrimitiveId -> m PrimFun Source #

getPrimitive' :: HasBuiltins m => PrimitiveId -> m (Maybe PrimFun) Source #

Returns Nothing if primitive is not bound or bound to a Builtin.

getPrimitiveName' :: HasBuiltins m => PrimitiveId -> m (Maybe QName) Source #

getPrimitiveTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => PrimitiveId -> m Term Source #

getPrimitiveTerm' :: HasBuiltins m => PrimitiveId -> m (Maybe Term) Source #

getTerm :: (HasBuiltins m, IsBuiltin a) => ShortText -> a -> m Term Source #

getTerm use name looks up name as a primitive or builtin, and throws an error otherwise. The use argument describes how the name is used for the sake of the error message.

getTerm' :: (HasBuiltins m, IsBuiltin a) => a -> m (Maybe Term) Source #

infallibleSortKit :: HasBuiltins m => m SortKit Source #

Compute a SortKit in contexts that do not support failure (e.g. Reify). This should only be used when we are sure that the primitive sorts have been bound, i.e. because it is "after" type checking.

intervalSort :: Sort Source #

intervalUnview :: HasBuiltins m => IntervalView -> m Term Source #

intervalUnview' :: HasBuiltins m => m (IntervalView -> Term) Source #

intervalView :: HasBuiltins m => Term -> m IntervalView Source #

intervalView' :: HasBuiltins m => m (Term -> IntervalView) Source #

isEqualityType :: EqualityView -> Bool Source #

isIOne :: IntervalView -> Bool Source #

isPathType :: PathView -> Bool Source #

isPrimitive :: HasBuiltins m => PrimitiveId -> QName -> m Bool Source #

litType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => Literal -> m Type Source #

mkSortKit :: QName -> QName -> QName -> QName -> QName -> QName -> SortKit Source #

pathUnview :: PathView -> Type Source #

Revert the PathView.

Postcondition: type is reduced.

pathView :: HasBuiltins m => Type -> m PathView Source #

Check whether the type is actually an path (lhs ≡ rhs) and extract lhs, rhs, and their type.

Precondition: type is reduced.

pathView' :: HasBuiltins m => m (Type -> PathView) Source #

primAbs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAbsAbs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaBlocker :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaBlockerAll :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaBlockerAny :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaBlockerMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaClause :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaClauseAbsurd :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaClauseClause :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaDefinition :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaDefinitionDataConstructor :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaDefinitionDataDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaDefinitionFunDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaDefinitionPostulate :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaDefinitionPrimitive :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaDefinitionRecordDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaErrorPart :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaErrorPartName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaErrorPartPatt :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaErrorPartString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaErrorPartTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaLitChar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaLitFloat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaLitMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaLitNat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaLitQName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaLitString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaLiteral :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaPatAbsurd :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaPatCon :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaPatDot :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaPatLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaPatProj :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaPatVar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaPattern :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaSort :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaSortInf :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaSortLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaSortProp :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaSortPropLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaSortType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaSortUnsupported :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCM :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMAskExpandLast :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMAskNormalisation :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMAskReconstructed :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMAskReduceDefs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMBind :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMBlock :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMCatchError :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMCheckFromString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMCheckType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMCommit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMDebugPrint :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMDeclareData :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMDeclareDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMDeclarePostulate :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMDefineData :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMDefineFun :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMExec :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMExtendContext :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMFormatErrorParts :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMFreshName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMGetContext :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMGetDefinition :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMGetInstances :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMGetType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMInContext :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMInferType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMIsMacro :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMNoConstraints :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMNormalise :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMPragmaCompile :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMPragmaForeign :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMQuoteOmegaTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMQuoteTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMReduce :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMReturn :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMRunSpeculative :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMSolveInstances :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMTypeError :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMUnify :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMUnquoteTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMWithExpandLast :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMWithNormalisation :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMWithReconstructed :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTCMWithReduceDefs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTermCon :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTermDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTermExtLam :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTermLam :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTermLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTermMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTermPi :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTermSort :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTermUnsupported :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAgdaTermVar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primArg :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primArgArg :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primArgArgInfo :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primArgInfo :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAssoc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAssocLeft :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAssocNon :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primAssocRight :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primBool :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primChar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primCons :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primEquality :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primEqualityName :: TCM QName Source #

Get the name of the equality type.

primEquiv :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primEquivFun :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primEquivProof :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primFaceForall :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primFalse :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primFixity :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primFixityFixity :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primFloat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primFromNat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primFromNeg :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primFromString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primGlue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primHComp :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primHidden :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primHiding :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primIMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primIMin :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primINeg :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primIOne :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primIZero :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primInstance :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primInteger :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primIntegerNegSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primIntegerPos :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primInterval :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primIntervalUniv :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primIsOne :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primIsOne1 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primIsOne2 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primIsOneEmpty :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primItIsOne :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primJust :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primLevel :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primLevelMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primLevelSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primLevelUniv :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primLevelZero :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primList :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primMaybe :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primNat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primNatDivSucAux :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primNatEquality :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primNatLess :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primNatMinus :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primNatModSucAux :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primNatPlus :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primNatTimes :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primNil :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primNothing :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primPartial :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primPartialP :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primPath :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primPathP :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primPrecedence :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primProp :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primPropOmega :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primQName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primRefl :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primSSetOmega :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primSigma :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primStrictSet :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primSub :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primSubIn :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primSubOut :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primTrans :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primTranspProof :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primTrue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primTypeOmega :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primUnit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primUnitUnit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primVisible :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

primZero :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

prim_glue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

prim_glueU :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

prim_unglue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

prim_unglueU :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term Source #

runBuiltinAccess :: TCState -> BuiltinAccess a -> a Source #

Run a BuiltinAccess monad.

setBuiltinThings :: BuiltinThings -> TCM () Source #

sortKit :: (HasBuiltins m, MonadTCError m) => m SortKit Source #

Compute a SortKit in an environment that supports failures.

When optLoadPrimitives is set to False, sortKit is a fallible operation, so for the uses of sortKit in fallible contexts (e.g. TCM), we report a type error rather than exploding.

newtype BuiltinAccess a Source #

The trivial implementation of HasBuiltins, using a constant TCState.

This may be used instead of TCMT/ReduceM where builtins must be accessed in a pure context.

Constructors

BuiltinAccess
Fields unBuiltinAccess :: TCState -> a

Instances

Instances details

HasBuiltins BuiltinAccess Source #
Instance details Defined in Mikan.TypeChecking.Monad.Builtin Methods getBuiltinThing :: SomeBuiltin -> BuiltinAccess (Maybe (Builtin PrimFun)) Source #
Applicative BuiltinAccess Source #
Instance details Defined in Mikan.TypeChecking.Monad.Builtin Methods pure :: a -> BuiltinAccess a # (<>) :: BuiltinAccess (a -> b) -> BuiltinAccess a -> BuiltinAccess b # liftA2 :: (a -> b -> c) -> BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess c # (>) :: BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess b # (<*) :: BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess a #
Functor BuiltinAccess Source #
Instance details Defined in Mikan.TypeChecking.Monad.Builtin Methods fmap :: (a -> b) -> BuiltinAccess a -> BuiltinAccess b # (<$) :: a -> BuiltinAccess b -> BuiltinAccess a #
Monad BuiltinAccess Source #
Instance details Defined in Mikan.TypeChecking.Monad.Builtin Methods (>>=) :: BuiltinAccess a -> (a -> BuiltinAccess b) -> BuiltinAccess b # (>>) :: BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess b # return :: a -> BuiltinAccess a #
MonadFail BuiltinAccess Source #
Instance details Defined in Mikan.TypeChecking.Monad.Builtin Methods fail :: String -> BuiltinAccess a #

data EqualityTypeData Source #

Constructors

EqualityTypeData
Fields _eqtRange :: Range Range of the `rewrite` expression, if any. _eqtSort :: Sort Sort of this type. _eqtName :: QName Builtin EQUALITY. _eqtParams :: Args Hidden. Empty or `Level`. _eqtType :: Arg Term Hidden. _eqtLhs :: Arg Term NotHidden. _eqtRhs :: Arg Term NotHidden.

Instances

Instances details

EqualityUnview EqualityTypeData Source #

Instance details

Defined in Mikan.TypeChecking.Monad.Builtin

Methods

equalityUnview :: EqualityTypeData -> Type Source #

Subst EqualityTypeData Source #

Instance details

Defined in Mikan.TypeChecking.Monad.Builtin

Associated Types

type SubstArg EqualityTypeData
Instance details Defined in Mikan.TypeChecking.Monad.Builtin type SubstArg EqualityTypeData = Term

Methods

applySubst :: Substitution' (SubstArg EqualityTypeData) -> EqualityTypeData -> EqualityTypeData Source #

type SubstArg EqualityTypeData Source #

Instance details

Defined in Mikan.TypeChecking.Monad.Builtin

type SubstArg EqualityTypeData = Term

class EqualityUnview a where Source #

Revert the EqualityView.

Postcondition: type is reduced.

Methods

equalityUnview :: a -> Type Source #

Instances

Instances details

EqualityUnview EqualityTypeData Source #
Instance details Defined in Mikan.TypeChecking.Monad.Builtin Methods equalityUnview :: EqualityTypeData -> Type Source #
EqualityUnview EqualityView Source #
Instance details Defined in Mikan.TypeChecking.Monad.Builtin Methods equalityUnview :: EqualityView -> Type Source #

data EqualityView Source #

View type as equality type.

Constructors

EqualityViewType EqualityTypeData	A type of the form `u ≡ v` decomposed into its parts. Used as type for the `rewrite` expression.
OtherType Type	A reduced type used as type for a `with` expression.
IdiomType Type	A reduced type used as type for the `with` inspect idiom.

Instances

Instances details

TermLike EqualityView Source #

Instance details

Defined in Mikan.TypeChecking.Monad.Builtin

Methods

traverseTermM :: Monad m => (Term -> m Term) -> EqualityView -> m EqualityView Source #

foldTerm :: Monoid m => (Term -> m) -> EqualityView -> m Source #

Free EqualityView Source #

Instance details

Defined in Mikan.TypeChecking.Monad.Builtin

Methods

freeVars :: ComputeFree r => EqualityView -> Reader r (Collect r) Source #

EqualityUnview EqualityView Source #

Instance details

Defined in Mikan.TypeChecking.Monad.Builtin

Methods

equalityUnview :: EqualityView -> Type Source #

PrettyTCM EqualityView Source #

Instance details

Defined in Mikan.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => EqualityView -> m Doc Source #

Instantiate EqualityView Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

instantiate' :: EqualityView -> ReduceM EqualityView Source #

InstantiateFull EqualityView Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

instantiateFull' :: EqualityView -> ReduceM EqualityView Source #

Normalise EqualityView Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

normalise' :: EqualityView -> ReduceM EqualityView Source #

Reduce EqualityView Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

reduce' :: EqualityView -> ReduceM EqualityView Source #

reduceB' :: EqualityView -> ReduceM (Blocked EqualityView) Source #

Simplify EqualityView Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

simplify' :: EqualityView -> ReduceM EqualityView

Subst EqualityView Source #

Instance details

Defined in Mikan.TypeChecking.Monad.Builtin

Associated Types

type SubstArg EqualityView
Instance details Defined in Mikan.TypeChecking.Monad.Builtin type SubstArg EqualityView = Term

Methods

applySubst :: Substitution' (SubstArg EqualityView) -> EqualityView -> EqualityView Source #

type SubstArg EqualityView Source #

Instance details

Defined in Mikan.TypeChecking.Monad.Builtin

type SubstArg EqualityView = Term

class (Functor m, Applicative m, Monad m) => HasBuiltins (m :: Type -> Type) where Source #

Minimal complete definition

Nothing

Methods

getBuiltinThing :: SomeBuiltin -> m (Maybe (Builtin PrimFun)) Source #

default getBuiltinThing :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type). (MonadTrans t, HasBuiltins n, t n ~ m) => SomeBuiltin -> m (Maybe (Builtin PrimFun)) Source #

Instances

Instances details

HasBuiltins TerM Source #
Instance details Defined in Mikan.Termination.Monad Methods getBuiltinThing :: SomeBuiltin -> TerM (Maybe (Builtin PrimFun)) Source #
HasBuiltins ReduceM Source #
Instance details Defined in Mikan.TypeChecking.Reduce.Monad Methods getBuiltinThing :: SomeBuiltin -> ReduceM (Maybe (Builtin PrimFun)) Source #
HasBuiltins BuiltinAccess Source #
Instance details Defined in Mikan.TypeChecking.Monad.Builtin Methods getBuiltinThing :: SomeBuiltin -> BuiltinAccess (Maybe (Builtin PrimFun)) Source #
HasBuiltins m => HasBuiltins (BlockT m) Source #
Instance details Defined in Mikan.TypeChecking.Monad.Builtin Methods getBuiltinThing :: SomeBuiltin -> BlockT m (Maybe (Builtin PrimFun)) Source #
MonadIO m => HasBuiltins (TCMT m) Source #
Instance details Defined in Mikan.TypeChecking.Monad.Builtin Methods getBuiltinThing :: SomeBuiltin -> TCMT m (Maybe (Builtin PrimFun)) Source #
HasBuiltins m => HasBuiltins (NamesT m) Source #
Instance details Defined in Mikan.TypeChecking.Names Methods getBuiltinThing :: SomeBuiltin -> NamesT m (Maybe (Builtin PrimFun)) Source #
HasBuiltins m => HasBuiltins (ListT m) Source #
Instance details Defined in Mikan.TypeChecking.Monad.Builtin Methods getBuiltinThing :: SomeBuiltin -> ListT m (Maybe (Builtin PrimFun)) Source #
HasBuiltins m => HasBuiltins (ChangeT m) Source #
Instance details Defined in Mikan.TypeChecking.Monad.Builtin Methods getBuiltinThing :: SomeBuiltin -> ChangeT m (Maybe (Builtin PrimFun)) Source #
HasBuiltins m => HasBuiltins (MaybeT m) Source #
Instance details Defined in Mikan.TypeChecking.Monad.Builtin Methods getBuiltinThing :: SomeBuiltin -> MaybeT m (Maybe (Builtin PrimFun)) Source #
HasBuiltins m => HasBuiltins (ReaderT e m) Source #
Instance details Defined in Mikan.TypeChecking.Monad.Builtin Methods getBuiltinThing :: SomeBuiltin -> ReaderT e m (Maybe (Builtin PrimFun)) Source #
HasBuiltins m => HasBuiltins (StateT s m) Source #
Instance details Defined in Mikan.TypeChecking.Monad.Builtin Methods getBuiltinThing :: SomeBuiltin -> StateT s m (Maybe (Builtin PrimFun)) Source #
(HasBuiltins m, Monoid w) => HasBuiltins (WriterT w m) Source #
Instance details Defined in Mikan.TypeChecking.Monad.Builtin Methods getBuiltinThing :: SomeBuiltin -> WriterT w m (Maybe (Builtin PrimFun)) Source #
HasBuiltins m => HasBuiltins (ExceptT e m) Source #
Instance details Defined in Mikan.TypeChecking.Monad.Builtin Methods getBuiltinThing :: SomeBuiltin -> ExceptT e m (Maybe (Builtin PrimFun)) Source #
HasBuiltins m => HasBuiltins (IdentityT m) Source #
Instance details Defined in Mikan.TypeChecking.Monad.Builtin Methods getBuiltinThing :: SomeBuiltin -> IdentityT m (Maybe (Builtin PrimFun)) Source #
HasBuiltins m => HasBuiltins (ReaderT e m) Source #
Instance details Defined in Mikan.TypeChecking.Monad.Builtin Methods getBuiltinThing :: SomeBuiltin -> ReaderT e m (Maybe (Builtin PrimFun)) Source #
HasBuiltins m => HasBuiltins (StateT s m) Source #
Instance details Defined in Mikan.TypeChecking.Monad.Builtin Methods getBuiltinThing :: SomeBuiltin -> StateT s m (Maybe (Builtin PrimFun)) Source #
(HasBuiltins m, Monoid w) => HasBuiltins (WriterT w m) Source #
Instance details Defined in Mikan.TypeChecking.Monad.Builtin Methods getBuiltinThing :: SomeBuiltin -> WriterT w m (Maybe (Builtin PrimFun)) Source #

data IntervalView Source #

Constructors

IZero
IOne
IMin (Arg Term) (Arg Term)
IMax (Arg Term) (Arg Term)
INeg (Arg Term)
OTerm Term

Instances

Instances details

Show IntervalView Source #
Instance details Defined in Mikan.TypeChecking.Monad.Builtin Methods showsPrec :: Int -> IntervalView -> ShowS # show :: IntervalView -> String # showList :: [IntervalView] -> ShowS #

data PathView Source #

View type as path type.

Constructors

PathType
Fields pathSort :: Sort Sort of this type. pathName :: QName Builtin PATH. pathLevel :: Arg Term Hidden pathType :: Arg Term Hidden pathLhs :: Arg Term NotHidden pathRhs :: Arg Term NotHidden
OType Type	reduced

data SortKit Source #

Sort primitives.

Constructors

SortKit
Fields nameOfUniv :: UnivSize -> Univ -> QName isNameOfUniv :: QName -> Maybe (UnivSize, Univ)

module Mikan.Syntax.Builtin