be36353 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #362 from david-christiansen/cmdline-exec

Add scripts

commitbe3635329477a1974a43d4f1276191a6898ec984 authorEdwin Brady <edwin.brady@gmail.com> dateFri 28 Jun 2013, 07:25 (13 years ago) parent77bf616 db18c51

5 files changed+39−6

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+5 src/Idris/AbsSyntaxTree.hs+1 src/Idris/IBC.hs+3−2 src/Idris/REPL.hs+28−4 src/Main.hs+2

src/Idris/AbsSyntax.hs+5

@@ -340,6 +340,11 @@ setQuiet q = do i <- getIState

340340 let opt' = opts { opt_quiet = q }

341341 putIState $ i { idris_options = opt' }

342342

343+getQuiet :: Idris Bool

344+getQuiet = do i <- getIState

345+ let opts = idris_options i

346+ return (opt_quiet opts)

347+

343348setTarget :: Target -> Idris ()

344349setTarget t = do i <- getIState

345350 let opts = idris_options i

src/Idris/AbsSyntaxTree.hs+1

@@ -253,6 +253,7 @@ data Opt = Filename String

253253 | UseTarget Target

254254 | OutputTy OutputType

255255 | Extension LanguageExt

256+ | InterpretScript String

256257 deriving (Show, Eq)

257258

258259-- Parsed declarations

src/Idris/IBC.hs+3−2

@@ -134,11 +134,12 @@ process :: IBCFile -> FilePath -> Idris ()

134134process i fn

135135 | ver i /= ibcVersion = do iLOG "ibc out of date"

136136 fail "Incorrect ibc version"

137− | otherwise =

137+ | otherwise =

138138 do srcok <- liftIO $ doesFileExist (sourcefile i)

139139 when srcok $ liftIO $ timestampOlder (sourcefile i) fn

140140 v <- verbose

141− when (v && srcok) $ iputStrLn $ "Skipping " ++ sourcefile i

141+ quiet <- getQuiet

142+ when (v && srcok && not quiet) $ iputStrLn $ "Skipping " ++ sourcefile i

142143 pImports (ibc_imports i)

143144 pImps (ibc_implicits i)

144145 pFixes (ibc_fixes i)

src/Idris/REPL.hs+28−4

@@ -605,6 +605,8 @@ parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)

605605parseArgs ("--dumpdefuns":n:ns) = DumpDefun n : (parseArgs ns)

606606parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)

607607parseArgs ("--target":n:ns) = UseTarget (parseTarget n) : (parseArgs ns)

608+parseArgs ["--exec"] = InterpretScript "Main.main" : []

609+parseArgs ("--exec":expr:ns) = InterpretScript expr : parseArgs ns

608610parseArgs ("-XTypeProviders":ns) = Extension TypeProviders : (parseArgs ns)

609611parseArgs (n:ns) = Filename n : (parseArgs ns)

610612

@@ -640,11 +642,16 @@ idrisMain opts =

640642 let tgt = case opt getTarget opts of

641643 [] -> ViaC

642644 xs -> last xs

645+ script <- case opt getExecScript opts of

646+ [] -> return Nothing

647+ x:y:xs -> do iputStrLn "More than one interpreter expression found."

648+ liftIO $ exitWith (ExitFailure 1)

649+ [expr] -> return (Just expr)

643650 when (DefaultTotal `elem` opts) $ do i <- getIState

644651 putIState (i { default_total = True })

645652 mapM_ addLangExt (opt getLanguageExt opts)

646653 setREPL runrepl

647− setQuiet quiet

654+ setQuiet (quiet || isJust script)

648655 setIdeSlave idesl

649656 setVerbose runrepl

650657 setCmdLine opts

@@ -670,16 +677,19 @@ idrisMain opts =

670677 elabPrims

671678 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"

672679 return ()

673− when (runrepl && not quiet && not idesl) $ iputStrLn banner

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

674681 ist <- getIState

675682 mods <- mapM loadModule inputs

676683 ok <- noErrors

677684 when ok $ case output of

678685 [] -> return ()

679− (o:_) -> process "" (Compile tgt o)

686+ (o:_) -> process "" (Compile tgt o)

680687 when ok $ case newoutput of

681688 [] -> return ()

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

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

690+ case script of

691+ Nothing -> return ()

692+ Just expr -> execScript expr

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

684694 when (idesl) $ ideslaveStart ist inputs

685695 ok <- noErrors

@@ -696,6 +706,16 @@ idrisMain opts =

696706 addPkgDir p = do ddir <- liftIO $ getDataDir

697707 addImportDir (ddir </> p)

698708

709+execScript :: String -> Idris ()

710+execScript expr = do i <- getIState

711+ case parseExpr i expr of

712+ Left err -> do iputStrLn $ show err

713+ liftIO $ exitWith (ExitFailure 1)

714+ Right term -> do ctxt <- getContext

715+ (tm, _) <- elabVal toplevel False term

716+ res <- execute tm

717+ liftIO $ exitWith ExitSuccess

718+

699719getFile :: Opt -> Maybe String

700720getFile (Filename str) = Just str

701721getFile _ = Nothing

@@ -741,6 +761,10 @@ getTarget :: Opt -> Maybe Target

741761getTarget (UseTarget x) = Just x

742762getTarget _ = Nothing

743763

764+getExecScript :: Opt -> Maybe String

765+getExecScript (InterpretScript expr) = Just expr

766+getExecScript _ = Nothing

767+

744768getOutputTy :: Opt -> Maybe OutputType

745769getOutputTy (OutputTy t) = Just t

746770getOutputTy _ = Nothing

src/Main.hs+2

@@ -91,6 +91,8 @@ usagemsg = "Idris version " ++ ver ++ "\n" ++

9191 "\t--log [level] Type debugging log level\n" ++

9292 "\t-S Do no further compilation of code generator output\n" ++

9393 "\t-c Compile to object files rather than an executable\n" ++

94+ "\t--exec [expr] Execute the expression expr in the interpreter, defaulting to\n" ++

95+ "\t Main.main if none provided, and exit.\n" ++

9496 "\t--ideslave Ideslave mode (for editors; in/ouput wrapped in s-expressions)\n" ++

9597 "\t--libdir Show library install directory and exit\n" ++

9698 "\t--link Show C library directories and exit (for C linking)\n" ++