c254c61 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

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

c254c61Edwin Brady13 years ago

CHANGELOG+2

compare with master

unifiedsplit

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

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

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

10* 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

12Internal changes

14Internal changes

src/Idris/AbsSyntax.hs+16−7

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

22import Data.List

23import Data.Char

24import Data.Either

25+import Data.Maybe

26import Debug.Trace

27import Debug.Trace

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

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

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

56addDyLib libs = do i <- getIState

57addDyLib libs = do i <- getIState

58+ let ls = idris_dynamic_libs i

59+ case mapMaybe (findDyLib ls) libs of

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

61+ [] -> do

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

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

58− case msum handle of

63+ case msum handle of

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

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

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

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

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

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

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

63− return (Left x)

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+

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

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

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

75addHdr 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

113 do let fn = case mods of

114 (f:_) -> f

115 _ -> ""

116− case parseCmd i cmd of

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

117 Left err -> iFail $ show err

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

119 idrisCatch

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

214 let fn = case inputs of

215 (f:_) -> f

216 _ -> ""

217− case parseCmd i cmd of

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

218 Left err -> do liftIO $ print err

219 return (Just inputs)

220 Right Reload ->

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

524 case handle of

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

526 Just x -> do let libs = idris_dynamic_libs i

527+ if x `elem` libs

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

529+ return ()

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

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

528 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace

531 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace

529process fn ListDynamic = do i <- getIState

532process fn ListDynamic = do i <- getIState

530 iputStrLn "Dynamic libraries:"

533 iputStrLn "Dynamic libraries:"

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

655 ]

658 ]

656

659

657

660

658−replSettings :: Settings Idris

661+replSettings :: Maybe FilePath -> Settings Idris

659−replSettings = setComplete replCompletion defaultSettings

662+replSettings hFile = setComplete replCompletion $ defaultSettings {

663+ historyFile = hFile

664+ }

660

665

661-- invoke as if from command line

666-- invoke as if from command line

662idris :: [Opt] -> IO IState

667idris :: [Opt] -> IO IState

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

725

730

726 ibc (IBC _ _) = True

731 ibc (IBC _ _) = True

727 ibc _ = False

732 ibc _ = False

728−

733+

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

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

730idrisMain opts =

735idrisMain opts =

731 do let inputs = opt getFile opts

736 do let inputs = opt getFile opts

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

794 return ()

799 return ()

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

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

796 ist <- getIState

801 ist <- getIState

797−

802+

798 loadInputs inputs

803 loadInputs inputs

799

804

800 liftIO $ hSetBuffering stdout LineBuffering

805 liftIO $ hSetBuffering stdout LineBuffering

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

806 case script of

811 case script of

807 Nothing -> return ()

812 Nothing -> return ()

808 Just expr -> execScript expr

813 Just expr -> execScript expr

814+

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

816+

817+ when runrepl $ initScript

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

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

810 when (idesl) $ ideslaveStart ist inputs

819 when (idesl) $ ideslaveStart ist inputs

811 ok <- noErrors

820 ok <- noErrors

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

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

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

819 makeOption _ = return ()

828 makeOption _ = return ()

820

829

821 addPkgDir :: String -> Idris ()

830 addPkgDir :: String -> Idris ()

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

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

823 addImportDir (ddir </> p)

832 addImportDir (ddir </> p)

824

833

825execScript :: String -> Idris ()

834execScript :: String -> Idris ()

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

832 res <- execute tm

841 res <- execute tm

833 liftIO $ exitWith ExitSuccess

842 liftIO $ exitWith ExitSuccess

834

843

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+

835getFile :: Opt -> Maybe String

881getFile :: Opt -> Maybe String

836getFile (Filename str) = Just str

882getFile (Filename str) = Just str

837getFile _ = Nothing

883getFile _ = Nothing

src/Idris/REPLParser.hs+2−1

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

18import Data.List.Split(splitOn)

19import Data.Char(toLower)

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

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

22+parseCmd i inputname = runParser pCmd i inputname

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

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

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

25cmd 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

36 , lib_handle :: DL

37 }

39+instance Eq DynamicLib where

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

41+

39#ifndef WINDOWS

42#ifndef WINDOWS

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

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

41tryLoadLib lib = do exactName <- doesFileExist lib

44tryLoadLib lib = do exactName <- doesFileExist lib