5bd1695 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add -e EXPR to evaluate expressions w/out REPL

The command line option follows the convention from Perl. This causes Idris to evaluate the provided expressions, pretty-printing them without line breaks. Then, test results need not depend on terminal widths any longer. If multiple -e options are provided, then the expressions are evaluated in order.

commit5bd169539bcd115c8763f9f5ffdefe161873127f authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 21 Apr 2014, 07:38 (13 years ago) parent6a011d8

4 files changed+33−2

compare with master

unifiedsplit

CHANGELOG+2 main/Main.hs+1 src/Idris/AbsSyntaxTree.hs+1 src/Idris/REPL.hs+29−2

CHANGELOG+2

@@ -3,6 +3,8 @@ New in 0.9.13:

33* IDE support for retrieving structured information about metavariables

44* Experimental Bits support for JavaScript

55* IdrisDoc: a Haddock- and JavaDoc-like HTML documentation generator

6+* Command line option -e (or --eval) to evaluate expressions without loading the

7+ REPL. This is useful for writing more portable tests.

79Internal changes

810

main/Main.hs+1

@@ -100,6 +100,7 @@ usagemsg = usagemsghdr ++ "\n" ++

100100 "\t --clean IPKG Clean package\n" ++

101101 "\t --build IPKG Build package\n" ++

102102 "\t --mkdoc IPKG Generate IdrisDoc for package\n" ++

103+ "\t -e --eval EXPR Evaluate an expression without loading the REPL" ++

103104 "\t --exec EXPR Execute as idris\n" ++

104105 "\t --libdir Display library directory\n" ++

105106 "\t --link Display link directory\n" ++

src/Idris/AbsSyntaxTree.hs+1

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

357357 | OutputTy OutputType

358358 | Extension LanguageExt

359359 | InterpretScript String

360+ | EvalExpr String

360361 | TargetTriple String

361362 | TargetCPU String

362363 | OptLevel Word

src/Idris/REPL.hs+29−2

@@ -1200,6 +1200,8 @@ parseArgs ("--mvn":ns) = OutputTy MavenProject : (parseArgs ns)

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

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

12021202parseArgs ("--codegen":n:ns) = UseCodegen (parseCodegen n) : (parseArgs ns)

1203+parseArgs ("--eval":expr:ns) = EvalExpr expr : parseArgs ns

1204+parseArgs ("-e":expr:ns) = EvalExpr expr : parseArgs ns

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

12041206parseArgs ("--exec":expr:ns) = InterpretScript expr : parseArgs ns

12051207parseArgs (('-':'X':extName):ns) = case maybeRead extName of

@@ -1372,13 +1374,15 @@ idrisMain opts =

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

13731375 runIO $ exitWith (ExitFailure 1)

13741376 [expr] -> return (Just expr)

1377+ let immediate = opt getEvalExpr opts

1378+

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

13761380 putIState (i { default_total = True })

13771381 setColourise $ not quiet && last (True : opt getColour opts)

13781382 when (not runrepl) $ setWidth InfinitelyWide

13791383 mapM_ addLangExt (opt getLanguageExt opts)

13801384 setREPL runrepl

1381− setQuiet (quiet || isJust script)

1385+ setQuiet (quiet || isJust script || not (null immediate))

13821386 setIdeSlave idesl

13831387 setVerbose verbose

13841388 setCmdLine opts

@@ -1406,7 +1410,13 @@ idrisMain opts =

14061410 return ()

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

14081412 return ()

1409− when (runrepl && not quiet && not idesl && not (isJust script) && not nobanner) $ iputStrLn banner

1413+ when (runrepl &&

1414+ not quiet &&

1415+ not idesl &&

1416+ not (isJust script) &&

1417+ not nobanner &&

1418+ null immediate) $

1419+ iputStrLn banner

14101420

14111421 orig <- getIState

14121422 loadInputs stdout inputs

@@ -1422,6 +1432,19 @@ idrisMain opts =

14221432 (o:_) -> idrisCatch (process stdout "" (Compile cgn o))

14231433 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)

14241434

1435+ case immediate of

1436+ [] -> return ()

1437+ exprs -> do setWidth InfinitelyWide

1438+ mapM_ (\str -> do ist <- getIState

1439+ c <- colourise

1440+ case parseExpr ist str of

1441+ Failure err -> do iputStrLn $ show (fixColour c err)

1442+ runIO $ exitWith (ExitFailure 1)

1443+ Success e -> process stdout "" (Eval e))

1444+ exprs

1445+ runIO $ exitWith ExitSuccess

1446+

1447+

14251448 case script of

14261449 Nothing -> return ()

14271450 Just expr -> execScript expr

@@ -1558,6 +1581,10 @@ getExecScript :: Opt -> Maybe String

15581581getExecScript (InterpretScript expr) = Just expr

15591582getExecScript _ = Nothing

15601583

1584+getEvalExpr :: Opt -> Maybe String

1585+getEvalExpr (EvalExpr expr) = Just expr

1586+getEvalExpr _ = Nothing

1587+

15611588getOutputTy :: Opt -> Maybe OutputType

15621589getOutputTy (OutputTy t) = Just t

15631590getOutputTy _ = Nothing