Idris.IBC

Documentation

ibcVersion :: Word8

data IBCFile

Constructors

IBCFile

Fields

ver :: Word8

sourcefile :: FilePath

symbols :: [Name]

ibc_imports :: [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, [(Name, Docstring)]))]

ibc_transforms :: [(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

Instances

Show IBCFile

Binary IBCFile

initIBC :: IBCFile

loadIBC :: FilePath -> Idris ()

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

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

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

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

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

process :: IBCFile -> FilePath -> Idris ()

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

pPostulates :: [Name] -> Idris ()

pParsedSpan :: Maybe FC -> Idris ()

pImportDirs :: [FilePath] -> Idris ()

pImports :: [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 :: [Name] -> [(Name, Def)] -> Idris ()

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

pAccess :: [(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 :: [(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