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

git.iko.soy/Idris-dev

:exec can take an expression as an argument

This compiles the expression and evaluates it. It will either print the expression (if its type is an instance of Show) or run it (if its type is IO ()), or give an error otherwise.

commit5d269e39d1a2894881763f755ec73b7ff03117b3 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 3 Apr 2015, 11:48 (12 years ago) parenta2b3c79

7 files changed+33−28

compare with master

unifiedsplit

src/IRTS/Compiler.hs+5−1 src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/Elab/Value.hs+10−1 src/Idris/Erasure.hs+3−16 src/Idris/REPL.hs+4−7 src/Idris/REPLParser.hs+9−1 test/basic010/Main.idr+1−1

src/IRTS/Compiler.hs+5−1

@@ -51,8 +51,12 @@ compile codegen f mtm

5151 = do checkMVs -- check for undefined metavariables

5252 checkTotality -- refuse to compile if there are totality problems

5353 exports <- findExports

54+ let rootNames = case mtm of

55+ Nothing -> []

56+ Just t -> freeNames t

5457

55− reachableNames <- performUsageAnalysis (getExpNames exports)

58+ reachableNames <- performUsageAnalysis

59+ (rootNames ++ getExpNames exports)

5660 maindef <- case mtm of

5761 Nothing -> return []

5862 Just tm -> do md <- irMain tm

src/Idris/AbsSyntaxTree.hs+1−1

@@ -369,7 +369,7 @@ data Command = Quit

369369 | ModImport String

370370 | Edit

371371 | Compile Codegen String

372− | Execute

372+ | Execute PTerm

373373 | ExecVal PTerm

374374 | Metavars

375375 | Prove Name

src/Idris/Elab/Value.hs+10−1

@@ -1,6 +1,6 @@

11{-# LANGUAGE PatternGuards #-}

22{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

3−module Idris.Elab.Value(elabVal, elabValBind, elabDocTerms) where

3+module Idris.Elab.Value(elabVal, elabValBind, elabDocTerms, elabExec) where

55import Idris.AbsSyntax

66import Idris.ASTUtils

@@ -114,3 +114,12 @@ elabDocTerms info str = do typechecked <- Traversable.mapM decorate str

114114 then Example tm

115115 else Checked tm

116116 | otherwise = Unchecked

117+

118+elabExec :: FC -> PTerm -> PTerm

119+elabExec fc tm = runtm (PAlternative False

120+ [PApp fc (PRef fc (sUN "printLn"))

121+ [pimp (sUN "ffi") (PRef fc (sUN "FFI_C")) False, pexp tm],

122+ tm])

123+ where

124+ runtm t = PApp fc (PRef fc (sUN "run__IO")) [pexp t]

125+

src/Idris/Erasure.hs+3−16

@@ -66,13 +66,11 @@ type Vars = Map Name VarInfo

6666-- Perform usage analysis, write the relevant information in the internal

6767-- structures, returning the list of reachable names.

6868performUsageAnalysis :: [Name] -> Idris [Name]

69−performUsageAnalysis roots = do

69+performUsageAnalysis startNames = do

7070 ctx <- tt_ctxt <$> getIState

71− startNames <- getStartNames <$> getIState

72−

7371 case startNames of

74− Left reason -> return [] -- no main -> not compiling -> reachability irrelevant

75− Right main -> do

72+ [] -> return [] -- no main -> not compiling -> reachability irrelevant

73+ main -> do

7674 ci <- idris_classes <$> getIState

7775 cg <- idris_callgraph <$> getIState

7876 opt <- idris_optimisation <$> getIState

@@ -107,17 +105,6 @@ performUsageAnalysis roots = do

107105

108106 return $ S.toList reachableNames

109107 where

110− getStartNames :: IState -> Either Err [Name]

111− getStartNames ist

112− = case lookupCtxtName n (idris_implicits ist) of

113− [(n', _)] -> Right (n' : roots)

114− [] -> if null roots

115− then Left (NoSuchVariable n)

116− else Right roots

117− more -> Left (CantResolveAlts (map fst more))

118− where

119− n = sNS (sUN "main") ["Main"]

120−

121108 indent = (" " ++)

122109

123110 fmtItem :: (Cond, DepSet) -> String

src/Idris/REPL.hs+4−7

@@ -582,8 +582,8 @@ idemodeProcess fn (HNF t) = process fn (HNF t)

582582--idemodeProcess fn TTShell = process fn TTShell -- need some prove mode!

583583idemodeProcess fn (TestInline t) = process fn (TestInline t)

584584

585−idemodeProcess fn Execute = do process fn Execute

586− iPrintResult ""

585+idemodeProcess fn (Execute t) = do process fn (Execute t)

586+ iPrintResult ""

587587idemodeProcess fn (Compile codegen f) = do process fn (Compile codegen f)

588588 iPrintResult ""

589589idemodeProcess fn (LogLvl i) = do process fn (LogLvl i)

@@ -1115,13 +1115,10 @@ process fn (TestInline t)

11151115 let tm' = inlineTerm ist tm

11161116 c <- colourise

11171117 iPrintResult (showTm ist (delab ist tm'))

1118−process fn Execute

1118+process fn (Execute tm)

11191119 = idrisCatch

11201120 (do ist <- getIState

1121− (m, _) <- elabVal recinfo ERHS

1122− (PApp fc

1123− (PRef fc (sUN "run__IO"))

1124− [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

1121+ (m, _) <- elabVal recinfo ERHS (elabExec fc tm)

11251122 (tmpn, tmph) <- runIO tempfile

11261123 runIO $ hClose tmph

11271124 t <- codegen

src/Idris/REPLParser.hs+9−1

@@ -71,7 +71,7 @@ parserCommandsForHelp =

7171 , noArgCmd ["proofs"] Proofs "Show available proofs"

7272 , exprArgCmd ["x"] ExecVal "Execute IO actions resulting from an expression using the interpreter"

7373 , (["c", "compile"], FileArg, "Compile to an executable [codegen] <filename>", cmd_compile)

74− , noArgCmd ["exec", "execute"] Execute "Compile to an executable and run"

74+ , (["exec", "execute"], OptionalArg ExprArg, "Compile to an executable and run", cmd_execute)

7575 , (["dynamic"], FileArg, "Dynamically load a C library (similar to %dynamic)", cmd_dynamic)

7676 , (["dynamic"], NoArg, "List dynamically loaded C libraries", cmd_dynamic)

7777 , noArgCmd ["?", "h", "help"] Help "Display this help text"

@@ -276,6 +276,14 @@ cmd_consolewidth name = do

276276 <|> do discard (P.symbol "infinite"); return InfinitelyWide

277277 <|> do n <- fmap fromInteger P.natural; return (ColsWide n)

278278

279+cmd_execute :: String -> P.IdrisParser (Either String Command)

280+cmd_execute name = do

281+ tm <- option maintm (P.fullExpr defaultSyntax)

282+ return (Right (Execute tm))

283+ where

284+ maintm = PRef (fileFC "(repl)") (sNS (sUN "main") ["Main"])

285+

286+

279287cmd_dynamic :: String -> P.IdrisParser (Either String Command)

280288cmd_dynamic name = do

281289 let emptyArgs = noArgs ListDynamic name

test/basic010/Main.idr+1−1

@@ -38,6 +38,6 @@ fmt (axiom n) = "axiom " ++ show n

3838

3939main : IO ()

4040main = do

41− n <- map (const 10000) (putStrLn "*oink*")

41+ n <- map (const (the Nat 10000)) (putStrLn "*oink*")

4242 putStrLn . show $ getWitness (f 4 n)

4343 putStrLn . fmt $ getProof (g 4 n)