idris- Functional Programming Language with Dependent Types

Safe HaskellNone




repl Source


:: IState

The initial state

-> [FilePath]

The loaded modules

-> InputT Idris () 

Run the REPL

startServer :: IState -> [FilePath] -> Idris () Source

Run the REPL server

runClient :: String -> IO () Source

Run a command on the server on localhost

ideslaveStart :: Bool -> IState -> [FilePath] -> Idris () Source

Run the IdeSlave

runIdeSlaveCommand Source


:: Handle

^ The handle for communication

-> Integer

^ The continuation ID for the client

-> IState

^ The original IState

-> FilePath

^ The current open file

-> [FilePath]

^ The currently loaded modules

-> IdeSlaveCommand

^ The command to process

-> Idris () 

Run IDESlave commands

ideSlaveForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris () Source

Show a term for IDESlave with the specified implicitness

mkPrompt :: [FilePath] -> [Char] Source

The prompt consists of the currently loaded modules, or Idris if there are none

lit :: FilePath -> Bool Source

Determine whether a file uses literate syntax

helphead :: [([[Char]], CmdArg, [Char])] Source

idris :: [Opt] -> IO (Maybe IState) Source

Invoke as if from command line. It is an error if there are unresolved totality problems.

runMain :: Idris () -> IO () Source

getIdrisUserDataDir :: Idris FilePath Source

Get the platform-specific, user-specific Idris dir

getInitScript :: Idris FilePath Source

Locate the platform-specific location for the init script

initScript :: Idris () Source

Run the initialisation script

getPkgMkDoc Source


:: Opt

Opt to extract

-> Maybe String


Returns None if given an Opt which is not PkgMkDoc Otherwise returns Just x, where x is the contents of PkgMkDoc

getPkgTest Source


:: Opt

the option to extract

-> Maybe String

the package file to test

opt :: (Opt -> Maybe a) -> [Opt] -> [a] Source