git.iko.soy/Idris-dev
on master help sign in
Move main setup code to Idris.REPL
commit28325170b326bd37724c3d24feb27c099af3666c authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 25 Sep 2012, 11:15 (14 years ago) parent7580119
2 files changed+100−91
compare with master
unifiedsplit
src/Idris/REPL.hs+98 src/Main.hs+2−91
src/Idris/REPL.hs+98
@@ -12,6 +12,7 @@ import Idris.Delaborate
1212import Idris.Compiler
1313import Idris.Prover
1414import Idris.Parser
15+import Idris.Primitives
1516import Idris.Coverage
1617import Paths_idris
1718import Util.System
@@ -22,6 +23,7 @@ import Core.TT
2223import Core.Constraints
2324
2425import IRTS.Compiler
26+import IRTS.LParser
2527
2628-- import RTS.SC
2729-- import RTS.Bytecode
@@ -30,12 +32,14 @@ import IRTS.Compiler
3032
3133import System.Console.Haskeline as H
3234import System.FilePath
35+import System.Exit
3336import System.Environment
3437import System.Process
3538import System.Directory
3639import System.IO
3740import Control.Monad
3841import Control.Monad.State
42+import Data.Maybe
3943import Data.List
4044import Data.Char
4145import Data.Version
@@ -384,3 +388,97 @@ help =
384388 ([":q",":quit"], "", "Exit the Idris system")
385389 ]
386390
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
2525import Idris.Imports
2626import Idris.Error
2727
28−import IRTS.Lang
29−import IRTS.LParser
30−
3128import Paths_idris
3229
3330-- Main program reads command line options, parses the main program, and gets
@@ -38,91 +35,13 @@ main = do xs <- getArgs
3835 runInputT defaultSettings $ execStateT (runIdris opts) idrisInit
3936
4037runIdris :: [Opt] -> Idris ()
41−runIdris opts =
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−
38+runIdris opts = do
5139 when (Ver `elem` opts) $ liftIO showver
5240 when (Usage `elem` opts) $ liftIO usage
5341 when (ShowIncs `elem` opts) $ liftIO showIncs
5442 when (ShowLibs `elem` opts) $ liftIO showLibs
5543 when (ShowLibdir `elem` opts) $ liftIO showLibdir
56− setREPL runrepl
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
44+ idrisMain opts -- in Idris.REPL
12645
12746usage = do putStrLn usagemsg
12847 exitWith ExitSuccess
@@ -165,14 +84,6 @@ parseArgs ("--bytecode":n:ns) = liftM (\x -> NoREPL : BCAsm n : x) (parseArgs
16584parseArgs ("--fovm":n:ns) = liftM (\x -> NoREPL : FOVM n : x) (parseArgs ns)
16685parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)
16786
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−
17687usagemsg = "Idris version " ++ ver ++ "\n" ++
17788 "--------------" ++ map (\x -> '-') ver ++ "\n" ++
17889 "Usage: idris [input file] [options]\n" ++