c254c61 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'master' of github.com:edwinb/Idris-dev

commitc254c61a576ed9762bd312db85324ebac6560a04 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 14 Sep 2013, 13:48 (13 years ago) parent8ae2240 f6fe5ea

5 files changed+78−17

compare with master

unifiedsplit

CHANGELOG+2 src/Idris/AbsSyntax.hs+16−7 src/Idris/REPL.hs+55−9 src/Idris/REPLParser.hs+2−1 src/Util/DynamicLinker.hs+3

CHANGELOG+2

@@ -8,6 +8,8 @@ New in 0.9.10:

88* At the REPL, "it" now refers to the previous expression

99* Semantic colouring at the REPL. Turn this off with --nocolour.

1010* Some prettifying of error message

11+* The contents of ~/.idris/repl/init are run at REPL start-up.

12+* The REPL stores a command history in ~/.idris/repl/history

1113

1214Internal changes

1315

src/Idris/AbsSyntax.hs+16−7

@@ -22,6 +22,7 @@ import Control.Monad.State

2222import Data.List

2323import Data.Char

2424import Data.Either

25+import Data.Maybe

2526

2627import Debug.Trace

2728

@@ -54,13 +55,21 @@ addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ (tgt, f

5455

5556addDyLib :: [String] -> Idris (Either DynamicLib String)

5657addDyLib libs = do i <- getIState

57− handle <- lift $ mapM (\l -> catchIO (tryLoadLib l) (\_ -> return Nothing)) libs

58− case msum handle of

59− Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++

60− concat (intersperse "," libs) ++ "\"")

61− Just x -> do let ls = idris_dynamic_libs i

62− putIState $ i { idris_dynamic_libs = x:ls }

63− return (Left x)

58+ let ls = idris_dynamic_libs i

59+ case mapMaybe (findDyLib ls) libs of

60+ x:_ -> return (Left x)

61+ [] -> do

62+ handle <- lift $ mapM (\l -> catchIO (tryLoadLib l) (\_ -> return Nothing)) $ libs

63+ case msum handle of

64+ Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++

65+ concat (intersperse "," libs) ++ "\"")

66+ Just x -> do putIState $ i { idris_dynamic_libs = x:ls }

67+ return (Left x)

68+ where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib

69+ findDyLib [] l = Nothing

70+ findDyLib (lib:libs) l | l == lib_name lib = Just lib

71+ | otherwise = findDyLib libs l

72+

6473

6574addHdr :: Codegen -> String -> Idris ()

6675addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }

src/Idris/REPL.hs+55−9

@@ -113,7 +113,7 @@ ideslave orig mods

113113 do let fn = case mods of

114114 (f:_) -> f

115115 _ -> ""

116− case parseCmd i cmd of

116+ case parseCmd i "(input)" cmd of

117117 Left err -> iFail $ show err

118118 Right (Prove n') -> do iResult ""

119119 idrisCatch

@@ -214,7 +214,7 @@ processInput cmd orig inputs

214214 let fn = case inputs of

215215 (f:_) -> f

216216 _ -> ""

217− case parseCmd i cmd of

217+ case parseCmd i "(input)" cmd of

218218 Left err -> do liftIO $ print err

219219 return (Just inputs)

220220 Right Reload ->

@@ -524,7 +524,10 @@ process fn (DynamicLink l) = do i <- getIState

524524 case handle of

525525 Nothing -> iFail $ "Could not load dynamic lib \"" ++ l ++ "\""

526526 Just x -> do let libs = idris_dynamic_libs i

527− putIState $ i { idris_dynamic_libs = x:libs }

527+ if x `elem` libs

528+ then do iLOG ("Tried to load duplicate library " ++ lib_name x)

529+ return ()

530+ else putIState $ i { idris_dynamic_libs = x:libs }

528531 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace

529532process fn ListDynamic = do i <- getIState

530533 iputStrLn "Dynamic libraries:"

@@ -655,8 +658,10 @@ helphead =

655658 ]

656659

657660

658−replSettings :: Settings Idris

659−replSettings = setComplete replCompletion defaultSettings

661+replSettings :: Maybe FilePath -> Settings Idris

662+replSettings hFile = setComplete replCompletion $ defaultSettings {

663+ historyFile = hFile

664+ }

660665

661666-- invoke as if from command line

662667idris :: [Opt] -> IO IState

@@ -725,7 +730,7 @@ loadInputs inputs

725730

726731 ibc (IBC _ _) = True

727732 ibc _ = False

728−

733+

729734idrisMain :: [Opt] -> Idris ()

730735idrisMain opts =

731736 do let inputs = opt getFile opts

@@ -794,7 +799,7 @@ idrisMain opts =

794799 return ()

795800 when (runrepl && not quiet && not idesl && not (isJust script)) $ iputStrLn banner

796801 ist <- getIState

797−

802+

798803 loadInputs inputs

799804

800805 liftIO $ hSetBuffering stdout LineBuffering

@@ -806,7 +811,11 @@ idrisMain opts =

806811 case script of

807812 Nothing -> return ()

808813 Just expr -> execScript expr

809− when (runrepl && not idesl) $ runInputT replSettings $ repl ist inputs

814+

815+ historyFile <- fmap (</> "repl" </> "history") getIdrisUserDataDir

816+

817+ when runrepl $ initScript

818+ when (runrepl && not idesl) $ runInputT (replSettings (Just historyFile)) $ repl ist inputs

810819 when (idesl) $ ideslaveStart ist inputs

811820 ok <- noErrors

812821 when (not ok) $ liftIO (exitWith (ExitFailure 1))

@@ -819,7 +828,7 @@ idrisMain opts =

819828 makeOption _ = return ()

820829

821830 addPkgDir :: String -> Idris ()

822− addPkgDir p = do ddir <- liftIO $ getDataDir

831+ addPkgDir p = do ddir <- liftIO $ getDataDir

823832 addImportDir (ddir </> p)

824833

825834execScript :: String -> Idris ()

@@ -832,6 +841,43 @@ execScript expr = do i <- getIState

832841 res <- execute tm

833842 liftIO $ exitWith ExitSuccess

834843

844+-- | Get the platform-specific, user-specific Idris dir

845+getIdrisUserDataDir :: Idris FilePath

846+getIdrisUserDataDir = liftIO $ getAppUserDataDirectory "idris"

847+

848+-- | Locate the platform-specific location for the init script

849+getInitScript :: Idris FilePath

850+getInitScript = do idrisDir <- getIdrisUserDataDir

851+ return $ idrisDir </> "repl" </> "init"

852+

853+-- | Run the initialisation script

854+initScript :: Idris ()

855+initScript = do script <- getInitScript

856+ idrisCatch (do go <- liftIO $ doesFileExist script

857+ when go $ do

858+ h <- liftIO $ openFile script ReadMode

859+ runInit h

860+ liftIO $ hClose h)

861+ (\e -> iFail $ "Error reading init file: " ++ show e)

862+ where runInit :: Handle -> Idris ()

863+ runInit h = do eof <- lift (hIsEOF h)

864+ ist <- getIState

865+ unless eof $ do

866+ line <- liftIO $ hGetLine h

867+ script <- getInitScript

868+ processLine ist line script

869+ runInit h

870+ processLine i cmd input =

871+ case parseCmd i input cmd of

872+ Left err -> liftIO $ print err

873+ Right Reload -> iFail "Init scripts cannot reload the file"

874+ Right (Load f) -> iFail "Init scripts cannot load files"

875+ Right (ModImport f) -> iFail "Init scripts cannot import modules"

876+ Right Edit -> iFail "Init scripts cannot invoke the editor"

877+ Right Proofs -> proofs i

878+ Right Quit -> iFail "Init scripts cannot quit Idris"

879+ Right cmd -> process [] cmd

880+

835881getFile :: Opt -> Maybe String

836882getFile (Filename str) = Just str

837883getFile _ = Nothing

src/Idris/REPLParser.hs+2−1

@@ -18,7 +18,8 @@ import Data.List

1818import Data.List.Split(splitOn)

1919import Data.Char(toLower)

2020

21−parseCmd i = runParser pCmd i "(input)"

21+parseCmd :: IState -> String -> String -> Either ParseError Command

22+parseCmd i inputname = runParser pCmd i inputname

2223

2324cmd :: [String] -> IParser ()

2425cmd xs = do lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs)

src/Util/DynamicLinker.hs+3

@@ -36,6 +36,9 @@ data DynamicLib = Lib { lib_name :: String

3636 , lib_handle :: DL

3737 }

3838

39+instance Eq DynamicLib where

40+ (Lib a _) == (Lib b _) = a == b

41+

3942#ifndef WINDOWS

4043tryLoadLib :: String -> IO (Maybe DynamicLib)

4144tryLoadLib lib = do exactName <- doesFileExist lib