idris-0.9.17: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.IBC

Synopsis

Documentation

data IBCFile Source

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]
 

loadIBC Source

Arguments

:: Bool

True = reexport, False = make everything private

-> FilePath 
-> Idris () 

loadPkgIndex :: String -> Idris () Source

Load an entire package from its index file

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

process Source

Arguments

:: Bool

Reexporting

-> IBCFile 
-> FilePath 
-> Idris () 

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

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

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

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

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

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

pAccess Source

Arguments

:: Bool

Reexporting?

-> [(Name, Accessibility)] 
-> Idris () 

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

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

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

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

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