Idris.IBC

Documentation

ibcVersion :: Word8

data IBCFile

Constructors

IBCFile

Fields

ver :: Word8

sourcefile :: FilePath

symbols :: ![Name]

ibc_imports :: ![(Bool, FilePath)]

ibc_importdirs :: ![FilePath]

ibc_implicits :: ![(Name, [PArg])]

ibc_fixes :: ![FixDecl]

ibc_statics :: ![(Name, [Bool])]

ibc_classes :: ![(Name, ClassInfo)]

ibc_instances :: ![(Bool, Name, Name)]

ibc_dsls :: ![(Name, DSL)]

ibc_datatypes :: ![(Name, TypeInfo)]

ibc_optimise :: ![(Name, OptInfo)]

ibc_syntax :: ![Syntax]

ibc_keywords :: ![String]

ibc_objs :: ![(Codegen, FilePath)]

ibc_libs :: ![(Codegen, String)]

ibc_cgflags :: ![(Codegen, String)]

ibc_dynamic_libs :: ![String]

ibc_hdrs :: ![(Codegen, String)]

ibc_access :: ![(Name, Accessibility)]

ibc_total :: ![(Name, Totality)]

ibc_totcheckfail :: ![(FC, String)]

ibc_flags :: ![(Name, [FnOpt])]

ibc_fninfo :: ![(Name, FnInfo)]

ibc_cg :: ![(Name, CGInfo)]

ibc_defs :: ![(Name, Def)]

ibc_docstrings :: ![(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]

ibc_moduledocs :: ![(Name, Docstring DocTerm)]

ibc_transforms :: ![(Name, (Term, Term))]

ibc_errRev :: ![(Term, Term)]

ibc_coercions :: ![Name]

ibc_lineapps :: ![(FilePath, Int, PTerm)]

ibc_namehints :: ![(Name, Name)]

ibc_metainformation :: ![(Name, MetaInformation)]

ibc_errorhandlers :: ![Name]

ibc_function_errorhandlers :: ![(Name, Name, Name)]

ibc_metavars :: ![(Name, (Maybe Name, Int, Bool))]

ibc_patdefs :: ![(Name, ([([Name], Term, Term)], [PTerm]))]

ibc_postulates :: ![Name]

ibc_parsedSpan :: !(Maybe FC)

ibc_usage :: ![(Name, Int)]

ibc_exports :: ![Name]

Instances

Show IBCFile

Binary IBCFile

initIBC :: IBCFile

loadIBC

Arguments

:: Bool

True = reexport, False = make everything private

-> FilePath

-> Idris ()

loadPkgIndex :: String -> Idris ()

Load an entire package from its index file

bencode :: Binary a => FilePath -> a -> IO ()

bdecode :: Binary b => FilePath -> IO b

writeIBC :: FilePath -> FilePath -> Idris ()

writePkgIndex :: FilePath -> Idris ()

mkIBC :: [IBCWrite] -> IBCFile -> Idris IBCFile

ibc :: IState -> IBCWrite -> IBCFile -> Idris IBCFile

process

Arguments

:: Bool

Reexporting

-> IBCFile

-> FilePath

-> Idris ()

timestampOlder :: FilePath -> FilePath -> Idris ()

pPostulates :: [Name] -> Idris ()

pParsedSpan :: Maybe FC -> Idris ()

pUsage :: [(Name, Int)] -> Idris ()

pExports :: [Name] -> Idris ()

pImportDirs :: [FilePath] -> Idris ()

pImports :: [(Bool, FilePath)] -> Idris ()

pImps :: [(Name, [PArg])] -> Idris ()

pFixes :: [FixDecl] -> Idris ()

pStatics :: [(Name, [Bool])] -> Idris ()

pClasses :: [(Name, ClassInfo)] -> Idris ()

pInstances :: [(Bool, Name, Name)] -> Idris ()

pDSLs :: [(Name, DSL)] -> Idris ()

pDatatypes :: [(Name, TypeInfo)] -> Idris ()

pOptimise :: [(Name, OptInfo)] -> Idris ()

pSyntax :: [Syntax] -> Idris ()

pKeywords :: [String] -> Idris ()

pObjs :: [(Codegen, FilePath)] -> Idris ()

pLibs :: [(Codegen, String)] -> Idris ()

pCGFlags :: [(Codegen, String)] -> Idris ()

pDyLibs :: [String] -> Idris ()

pHdrs :: [(Codegen, String)] -> Idris ()

pPatdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))] -> Idris ()

pDefs :: Bool -> [Name] -> [(Name, Def)] -> Idris ()

pDocs :: [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))] -> Idris ()

pMDocs :: [(Name, Docstring DocTerm)] -> Idris ()

pAccess

Arguments

:: Bool

Reexporting?

-> [(Name, Accessibility)]

-> Idris ()

pFlags :: [(Name, [FnOpt])] -> Idris ()

pFnInfo :: [(Name, FnInfo)] -> Idris ()

pTotal :: [(Name, Totality)] -> Idris ()

pTotCheckErr :: [(FC, String)] -> Idris ()

pCG :: [(Name, CGInfo)] -> Idris ()

pCoercions :: [Name] -> Idris ()

pTrans :: [(Name, (Term, Term))] -> Idris ()

pErrRev :: [(Term, Term)] -> Idris ()

pLineApps :: [(FilePath, Int, PTerm)] -> Idris ()

pNameHints :: [(Name, Name)] -> Idris ()

pMetaInformation :: [(Name, MetaInformation)] -> Idris ()

pErrorHandlers :: [Name] -> Idris ()

pFunctionErrorHandlers :: [(Name, Name, Name)] -> Idris ()

pMetavars :: [(Name, (Maybe Name, Int, Bool))] -> Idris ()

safeToEnum :: (Enum a, Bounded a, Integral int) => String -> int -> a