Documentation

traceExtrM :: Monad m => String -> m () Source #

runExtract :: Signature -> TypeCheck a -> IO (Either TraceError (a, TCState)) Source #

type FExpr = Expr Source #

type FDeclaration = Declaration Source #

type FClause = Clause Source #

type FPattern = Pattern Source #

type FConstructor = Constructor Source #

type FTypeSig = TypeSig Source #

type FFun = Fun Source #

type FTelescope = Telescope Source #

type FTVal = TVal Source #

extractDecls :: [EDeclaration] -> TypeCheck [FDeclaration] Source #

extractDecl :: EDeclaration -> TypeCheck [FDeclaration] Source #

extractFuns :: Co -> [Fun] -> TypeCheck [FDeclaration] Source #

extractFun :: Co -> Fun -> TypeCheck [FDeclaration] Source #

extractFunTypeSig :: Fun -> TypeCheck [Fun] Source #

extractLet :: Bool -> Name -> Type -> Expr -> TypeCheck [FDeclaration] Source #

extractTypeSig :: TypeSig -> TypeCheck FTypeSig Source #

extractIfTerm :: Name -> TypeCheck [a] -> TypeCheck [a] Source #

extractDataDecl :: Name -> Co -> Telescope -> Type -> [Constructor] -> TypeCheck [FDeclaration] Source #

extractConstructor :: Telescope -> Constructor -> TypeCheck FConstructor Source #

extractClause :: Name -> FTVal -> Clause -> TypeCheck [FClause] Source #

extractPatterns :: FTVal -> [Pattern] -> ([FPattern] -> FTVal -> TypeCheck a) -> TypeCheck a Source #

extractPattern :: FTVal -> Pattern -> ([FPattern] -> FTVal -> TypeCheck a) -> TypeCheck a Source #

extractPattern' :: FTVal -> Pattern -> ([FPattern] -> TypeCheck a) -> TypeCheck a Source #

extrConType :: QName -> FTVal -> TypeCheck FTVal Source #

extractInfer :: Expr -> TypeCheck (FExpr, FTVal) Source #

extractCheck :: Expr -> FTVal -> TypeCheck FExpr Source #

insertCast :: FExpr -> FTVal -> FTVal -> TypeCheck FExpr Source #

funView :: FTVal -> TypeCheck FunView Source #

data FunView Source #

prodView :: FTVal -> TypeCheck ProdView Source #

data ProdView Source #

type FKind = Expr Source #

star :: FKind Source #

extractSet :: Sort Val -> Maybe FKind Source #

extractKindTel :: Telescope -> TypeCheck FTelescope Source #

extractKindDom :: Domain -> TypeCheck (Dom FKind) Source #

extractKind :: TVal -> TypeCheck (Maybe FKind) Source #

type FType = Expr Source #

newTyVar :: Name -> FKind -> (Int -> TypeCheck a) -> TypeCheck a Source #

addFKindTel :: FTelescope -> TypeCheck a -> TypeCheck a Source #

extractTeleVal :: TeleVal -> TypeCheck FTelescope Source #

extractType :: TVal -> TypeCheck FType Source #

extractTypeAt :: FKind -> TVal -> TypeCheck FType Source #

extractTypes :: FKind -> [TVal] -> TypeCheck [FType] Source #