2832517 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Move main setup code to Idris.REPL

2832517Edwin Brady14 years ago

src/Idris/REPL.hs+98

compare with master

unifiedsplit

@@ -12,6 +12,7 @@ import Idris.Delaborate

12import Idris.Compiler

13import Idris.Prover

14import Idris.Parser

15+import Idris.Primitives

15import Idris.Coverage

16import Idris.Coverage

16import Paths_idris

17import Paths_idris

17import Util.System

18import Util.System

@@ -22,6 +23,7 @@ import Core.TT

22import Core.Constraints

23import Core.Constraints

24import IRTS.Compiler

25import IRTS.Compiler

26+import IRTS.LParser

26-- import RTS.SC

28-- import RTS.SC

27-- import RTS.Bytecode

29-- import RTS.Bytecode

@@ -30,12 +32,14 @@ import IRTS.Compiler

31import System.Console.Haskeline as H

33import System.Console.Haskeline as H

32import System.FilePath

34import System.FilePath

35+import System.Exit

33import System.Environment

36import System.Environment

34import System.Process

37import System.Process

35import System.Directory

38import System.Directory

36import System.IO

39import System.IO

37import Control.Monad

40import Control.Monad

38import Control.Monad.State

41import Control.Monad.State

42+import Data.Maybe

39import Data.List

43import Data.List

40import Data.Char

44import Data.Char

41import Data.Version

45import Data.Version

@@ -384,3 +388,97 @@ help =

384 ([":q",":quit"], "", "Exit the Idris system")

388 ([":q",":quit"], "", "Exit the Idris system")

385 ]

389 ]

386

390

391+-- invoke as if from command line

392+idris :: [Opt] -> IO IState

393+idris opts = runInputT defaultSettings $ execStateT (idrisMain opts) idrisInit

394+

395+idrisMain :: [Opt] -> Idris ()

396+idrisMain opts =

397+ do let inputs = opt getFile opts

398+ let runrepl = not (NoREPL `elem` opts)

399+ let output = opt getOutput opts

400+ let newoutput = opt getNewOutput opts

401+ let ibcsubdir = opt getIBCSubDir opts

402+ let importdirs = opt getImportDir opts

403+ let bcs = opt getBC opts

404+ let vm = opt getFOVM opts

405+ setREPL runrepl

406+ setVerbose runrepl

407+ when (Verbose `elem` opts) $ setVerbose True

408+ mapM_ makeOption opts

409+ -- if we have the --fovm flag, drop into the first order VM testing

410+ case vm of

411+ [] -> return ()

412+ xs -> liftIO $ mapM_ fovm xs

413+ -- if we have the --bytecode flag, drop into the bytecode assembler

414+ case bcs of

415+ [] -> return ()

416+ xs -> return () -- liftIO $ mapM_ bcAsm xs

417+ case ibcsubdir of

418+ [] -> setIBCSubDir ""

419+ (d:_) -> setIBCSubDir d

420+ setImportDirs importdirs

421+ elabPrims

422+ when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"

423+ return ()

424+ when runrepl $ iputStrLn banner

425+ ist <- get

426+ mods <- mapM loadModule inputs

427+ ok <- noErrors

428+ when ok $ case output of

429+ [] -> return ()

430+ (o:_) -> process "" (Compile ViaC o)

431+ when ok $ case newoutput of

432+ [] -> return ()

433+ (o:_) -> process "" (NewCompile o)

434+ when runrepl $ repl ist inputs

435+ ok <- noErrors

436+ when (not ok) $ liftIO (exitWith (ExitFailure 1))

437+ where

438+ makeOption (OLogging i) = setLogLevel i

439+ makeOption TypeCase = setTypeCase True

440+ makeOption TypeInType = setTypeInType True

441+ makeOption NoCoverage = setCoverage False

442+ makeOption ErrContext = setErrContext True

443+ makeOption _ = return ()

444+

445+getFile :: Opt -> Maybe String

446+getFile (Filename str) = Just str

447+getFile _ = Nothing

448+

449+getBC :: Opt -> Maybe String

450+getBC (BCAsm str) = Just str

451+getBC _ = Nothing

452+

453+getFOVM :: Opt -> Maybe String

454+getFOVM (FOVM str) = Just str

455+getFOVM _ = Nothing

456+

457+getOutput :: Opt -> Maybe String

458+getOutput (Output str) = Just str

459+getOutput _ = Nothing

460+

461+getNewOutput :: Opt -> Maybe String

462+getNewOutput (NewOutput str) = Just str

463+getNewOutput _ = Nothing

464+

465+getIBCSubDir :: Opt -> Maybe String

466+getIBCSubDir (IBCSubDir str) = Just str

467+getIBCSubDir _ = Nothing

468+

469+getImportDir :: Opt -> Maybe String

470+getImportDir (ImportDir str) = Just str

471+getImportDir _ = Nothing

472+

473+opt :: (Opt -> Maybe a) -> [Opt] -> [a]

474+opt = mapMaybe

475+

476+ver = showVersion version

477+

478+banner = " ____ __ _ \n" ++

479+ " / _/___/ /____(_)____ \n" ++

480+ " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++

481+ " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++

482+ " /___/\\__,_/_/ /_/____/ Type :? for help \n"

483+

484+

src/Main.hs+2−91

@@ -25,9 +25,6 @@ import Idris.Primitives

25import Idris.Imports

26import Idris.Error

28−import IRTS.Lang

29−import IRTS.LParser

30−

31import Paths_idris

28import Paths_idris

33-- Main program reads command line options, parses the main program, and gets

30-- Main program reads command line options, parses the main program, and gets

@@ -38,91 +35,13 @@ main = do xs <- getArgs

38 runInputT defaultSettings $ execStateT (runIdris opts) idrisInit

35 runInputT defaultSettings $ execStateT (runIdris opts) idrisInit

40runIdris :: [Opt] -> Idris ()

37runIdris :: [Opt] -> Idris ()

41−runIdris opts =

38+runIdris opts = do

42− do let inputs = opt getFile opts

43− let runrepl = not (NoREPL `elem` opts)

44− let output = opt getOutput opts

45− let newoutput = opt getNewOutput opts

46− let ibcsubdir = opt getIBCSubDir opts

47− let importdirs = opt getImportDir opts

48− let bcs = opt getBC opts

49− let vm = opt getFOVM opts

50−

51 when (Ver `elem` opts) $ liftIO showver

39 when (Ver `elem` opts) $ liftIO showver

52 when (Usage `elem` opts) $ liftIO usage

40 when (Usage `elem` opts) $ liftIO usage

53 when (ShowIncs `elem` opts) $ liftIO showIncs

41 when (ShowIncs `elem` opts) $ liftIO showIncs

54 when (ShowLibs `elem` opts) $ liftIO showLibs

42 when (ShowLibs `elem` opts) $ liftIO showLibs

55 when (ShowLibdir `elem` opts) $ liftIO showLibdir

43 when (ShowLibdir `elem` opts) $ liftIO showLibdir

56− setREPL runrepl

44+ idrisMain opts -- in Idris.REPL

57− setVerbose runrepl

58− when (Verbose `elem` opts) $ setVerbose True

59− mapM_ makeOption opts

60− -- if we have the --fovm flag, drop into the first order VM testing

61− case vm of

62− [] -> return ()

63− xs -> liftIO $ mapM_ fovm xs

64− -- if we have the --bytecode flag, drop into the bytecode assembler

65− case bcs of

66− [] -> return ()

67− xs -> return () -- liftIO $ mapM_ bcAsm xs

68− case ibcsubdir of

69− [] -> setIBCSubDir ""

70− (d:_) -> setIBCSubDir d

71− setImportDirs importdirs

72− elabPrims

73− when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"

74− return ()

75− when runrepl $ iputStrLn banner

76− ist <- get

77− mods <- mapM loadModule inputs

78− ok <- noErrors

79− when ok $ case output of

80− [] -> return ()

81− (o:_) -> process "" (Compile ViaC o)

82− when ok $ case newoutput of

83− [] -> return ()

84− (o:_) -> process "" (NewCompile o)

85− when runrepl $ repl ist inputs

86− ok <- noErrors

87− when (not ok) $ liftIO (exitWith (ExitFailure 1))

88− where

89− makeOption (OLogging i) = setLogLevel i

90− makeOption TypeCase = setTypeCase True

91− makeOption TypeInType = setTypeInType True

92− makeOption NoCoverage = setCoverage False

93− makeOption ErrContext = setErrContext True

94− makeOption _ = return ()

95−

96−getFile :: Opt -> Maybe String

97−getFile (Filename str) = Just str

98−getFile _ = Nothing

99−

100−getBC :: Opt -> Maybe String

101−getBC (BCAsm str) = Just str

102−getBC _ = Nothing

103−

104−getFOVM :: Opt -> Maybe String

105−getFOVM (FOVM str) = Just str

106−getFOVM _ = Nothing

107−

108−getOutput :: Opt -> Maybe String

109−getOutput (Output str) = Just str

110−getOutput _ = Nothing

111−

112−getNewOutput :: Opt -> Maybe String

113−getNewOutput (NewOutput str) = Just str

114−getNewOutput _ = Nothing

115−

116−getIBCSubDir :: Opt -> Maybe String

117−getIBCSubDir (IBCSubDir str) = Just str

118−getIBCSubDir _ = Nothing

119−

120−getImportDir :: Opt -> Maybe String

121−getImportDir (ImportDir str) = Just str

122−getImportDir _ = Nothing

123−

124−opt :: (Opt -> Maybe a) -> [Opt] -> [a]

125−opt = mapMaybe

126

127usage = do putStrLn usagemsg

46usage = do putStrLn usagemsg

128 exitWith ExitSuccess

47 exitWith ExitSuccess

@@ -165,14 +84,6 @@ parseArgs ("--bytecode":n:ns) = liftM (\x -> NoREPL : BCAsm n : x) (parseArgs

165parseArgs ("--fovm":n:ns) = liftM (\x -> NoREPL : FOVM n : x) (parseArgs ns)

84parseArgs ("--fovm":n:ns) = liftM (\x -> NoREPL : FOVM n : x) (parseArgs ns)

166parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)

85parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)

167

168−ver = showVersion version

169−

170−banner = " ____ __ _ \n" ++

171− " / _/___/ /____(_)____ \n" ++

172− " / // __ / ___/ / ___/ Version " ++ ver ++ "\n" ++

173− " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++

174− " /___/\\__,_/_/ /_/____/ Type :? for help \n"

175−

176usagemsg = "Idris version " ++ ver ++ "\n" ++

87usagemsg = "Idris version " ++ ver ++ "\n" ++

177 "--------------" ++ map (\x -> '-') ver ++ "\n" ++

88 "--------------" ++ map (\x -> '-') ver ++ "\n" ++

178 "Usage: idris [input file] [options]\n" ++

89 "Usage: idris [input file] [options]\n" ++