be36353 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

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

be36353Edwin Brady13 years ago

src/Idris/AbsSyntax.hs+5

compare with master

unifiedsplit

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

340 let opt' = opts { opt_quiet = q }

341 putIState $ i { idris_options = opt' }

342

343+getQuiet :: Idris Bool

344+getQuiet = do i <- getIState

345+ let opts = idris_options i

346+ return (opt_quiet opts)

347+

343setTarget :: Target -> Idris ()

348setTarget :: Target -> Idris ()

344setTarget t = do i <- getIState

349setTarget t = do i <- getIState

345 let opts = idris_options i

350 let opts = idris_options i

src/Idris/AbsSyntaxTree.hs+1

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

253 | UseTarget Target

254 | OutputTy OutputType

255 | Extension LanguageExt

256+ | InterpretScript String

256 deriving (Show, Eq)

257 deriving (Show, Eq)

257

258

258-- Parsed declarations

259-- Parsed declarations

src/Idris/IBC.hs+3−2

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

134process i fn

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

136 fail "Incorrect ibc version"

137− | otherwise =

137+ | otherwise =

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

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

140 v <- verbose

141+ quiet <- getQuiet

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

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

142 pImports (ibc_imports i)

143 pImports (ibc_imports i)

143 pImps (ibc_implicits i)

144 pImps (ibc_implicits i)

144 pFixes (ibc_fixes i)

145 pFixes (ibc_fixes i)

src/Idris/REPL.hs+28−4

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

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

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

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

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

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

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

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

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

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

610

612

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

640 let tgt = case opt getTarget opts of

642 let tgt = case opt getTarget opts of

641 [] -> ViaC

643 [] -> ViaC

642 xs -> last xs

644 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)

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

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

644 putIState (i { default_total = True })

651 putIState (i { default_total = True })

645 mapM_ addLangExt (opt getLanguageExt opts)

652 mapM_ addLangExt (opt getLanguageExt opts)

646 setREPL runrepl

653 setREPL runrepl

647− setQuiet quiet

654+ setQuiet (quiet || isJust script)

648 setIdeSlave idesl

655 setIdeSlave idesl

649 setVerbose runrepl

656 setVerbose runrepl

650 setCmdLine opts

657 setCmdLine opts

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

670 elabPrims

677 elabPrims

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

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

672 return ()

679 return ()

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

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

674 ist <- getIState

681 ist <- getIState

675 mods <- mapM loadModule inputs

682 mods <- mapM loadModule inputs

676 ok <- noErrors

683 ok <- noErrors

677 when ok $ case output of

684 when ok $ case output of

678 [] -> return ()

685 [] -> return ()

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

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

680 when ok $ case newoutput of

687 when ok $ case newoutput of

681 [] -> return ()

688 [] -> return ()

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

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

690+ case script of

691+ Nothing -> return ()

692+ Just expr -> execScript expr

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

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

684 when (idesl) $ ideslaveStart ist inputs

694 when (idesl) $ ideslaveStart ist inputs

685 ok <- noErrors

695 ok <- noErrors

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

696 addPkgDir p = do ddir <- liftIO $ getDataDir

706 addPkgDir p = do ddir <- liftIO $ getDataDir

697 addImportDir (ddir </> p)

707 addImportDir (ddir </> p)

698

708

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+

699getFile :: Opt -> Maybe String

719getFile :: Opt -> Maybe String

700getFile (Filename str) = Just str

720getFile (Filename str) = Just str

701getFile _ = Nothing

721getFile _ = Nothing

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

741getTarget (UseTarget x) = Just x

761getTarget (UseTarget x) = Just x

742getTarget _ = Nothing

762getTarget _ = Nothing

743

763

764+getExecScript :: Opt -> Maybe String

765+getExecScript (InterpretScript expr) = Just expr

766+getExecScript _ = Nothing

767+

744getOutputTy :: Opt -> Maybe OutputType

768getOutputTy :: Opt -> Maybe OutputType

745getOutputTy (OutputTy t) = Just t

769getOutputTy (OutputTy t) = Just t

746getOutputTy _ = Nothing

770getOutputTy _ = Nothing

src/Main.hs+2

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

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

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

93 "\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" ++

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

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

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

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

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

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