Core.Directory

Definitions

pkgGlobalDirectory : Ref Ctxt Defs => Core String

Totality: total
Visibility: export

pkgLocalDirectory : Ref Ctxt Defs => Core String

Totality: total
Visibility: export

ttcBuildDirectory : Ref Ctxt Defs => Core String

Totality: total
Visibility: export

libInstallDirectory : Ref Ctxt Defs => String -> Core String

Totality: total
Visibility: export

ttcInstallDirectory : Ref Ctxt Defs => String -> Core String

Totality: total
Visibility: export

srcInstallDirectory : Ref Ctxt Defs => String -> Core String

Totality: total
Visibility: export

extraSearchDirectories : Ref Ctxt Defs => Core (List String)

Totality: total
Visibility: export

data IdrSrcExt : Type

Totality: total
Visibility: public export
Constructors:

E_idr : IdrSrcExt

E_lidr : IdrSrcExt

E_yaff : IdrSrcExt

E_org : IdrSrcExt

E_md : IdrSrcExt

Hints:

Eq IdrSrcExt

Show IdrSrcExt

listOfExtensions : List IdrSrcExt

  This does not include the complete set of literate extensions as supported by Idris.

Totality: total
Visibility: public export

listOfExtensionsStr : List String

  List of valid extensions in Idris as strings.
  
  Extensions have a leading "." separator *and* may include multiple extensions to support literate mode extensions for the form ".org.idr".
  

Totality: total
Visibility: public export

splitIdrisFileName : String -> Maybe (String, String)

  Return the basename and extension used *if* given filename is a valid idris filename.
  
  Extensions are returned with a leading "." separator.

Totality: total
Visibility: export

firstAvailable : Ref Ctxt Defs => List String -> Core (Maybe String)

Totality: total
Visibility: export

findDataFile : Ref Ctxt Defs => String -> Core String

Visibility: export

readDataFile : Ref Ctxt Defs => String -> Core String

Visibility: export

findLibraryFile : Ref Ctxt Defs => String -> Core String

  Look for a library file required by a code generator. Look in the
  library directories, and in the lib/ subdirectory of all the 'extra import'
  directories and the package directory roots.

Totality: total
Visibility: export

nsToPath : Ref Ctxt Defs => FC -> ModuleIdent -> Core (Either Error String)

Totality: total
Visibility: export

nsToSource : Ref Ctxt Defs => FC -> ModuleIdent -> Core String

Totality: total
Visibility: export

mbPathToNS : String -> Maybe String -> String -> Maybe ModuleIdent

Totality: total
Visibility: export

corePathToNS : String -> Maybe String -> String -> Core ModuleIdent

Totality: total
Visibility: export

ctxtPathToNS : Ref Ctxt Defs => String -> Core ModuleIdent

Totality: total
Visibility: export

mkdirAll : String -> IO (Either FileError ())

Visibility: export

makeBuildDirectory : Ref Ctxt Defs => ModuleIdent -> Core ()

Visibility: export

ensureDirectoryExists : String -> Core ()

Visibility: export

getTTCFileName : Ref Ctxt Defs => String -> String -> Core String

Totality: total
Visibility: export

getObjFileName : Ref Ctxt Defs => String -> String -> Core String

Totality: total
Visibility: export

getExecFileName : Ref Ctxt Defs => String -> Core String

Totality: total
Visibility: export

findIpkgFile : IO (Maybe (String, (String, String)))

Visibility: export