Idris.IBC

Synopsis

• ibcVersion :: Word8
• data IBCFile = IBCFile {
  • 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]
  }
• initIBC :: IBCFile
• loadIBC :: Bool -> FilePath -> Idris ()
• loadPkgIndex :: String -> Idris ()
• 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 :: Bool -> 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 :: Bool -> [(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

Documentation