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

src/IRTS/Compiler.hs+5−1

compare with master

unifiedsplit

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

51 = do checkMVs -- check for undefined metavariables

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

53 exports <- findExports

54+ let rootNames = case mtm of

55+ Nothing -> []

56+ Just t -> freeNames t

54

57

55− reachableNames <- performUsageAnalysis (getExpNames exports)

58+ reachableNames <- performUsageAnalysis

59+ (rootNames ++ getExpNames exports)

56 maindef <- case mtm of

60 maindef <- case mtm of

57 Nothing -> return []

61 Nothing -> return []

58 Just tm -> do md <- irMain tm

62 Just tm -> do md <- irMain tm

src/Idris/AbsSyntaxTree.hs+1−1

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

369 | ModImport String

370 | Edit

371 | Compile Codegen String

372− | Execute

372+ | Execute PTerm

373 | ExecVal PTerm

374 | Metavars

375 | Prove Name

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

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

1{-# LANGUAGE PatternGuards #-}

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

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

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

4

5import Idris.AbsSyntax

6import Idris.ASTUtils

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

114 then Example tm

115 else Checked tm

116 | 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

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

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

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

69−performUsageAnalysis roots = do

69+performUsageAnalysis startNames = do

70 ctx <- tt_ctxt <$> getIState

71− startNames <- getStartNames <$> getIState

72−

73 case startNames of

71 case startNames of

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

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

75− Right main -> do

73+ main -> do

76 ci <- idris_classes <$> getIState

74 ci <- idris_classes <$> getIState

77 cg <- idris_callgraph <$> getIState

75 cg <- idris_callgraph <$> getIState

78 opt <- idris_optimisation <$> getIState

76 opt <- idris_optimisation <$> getIState

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

107

105

108 return $ S.toList reachableNames

106 return $ S.toList reachableNames

109 where

107 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−

121 indent = (" " ++)

108 indent = (" " ++)

122

109

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

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

src/Idris/REPL.hs+4−7

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

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

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

584

585−idemodeProcess fn Execute = do process fn Execute

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

586− iPrintResult ""

586+ iPrintResult ""

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

588 iPrintResult ""

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

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

1115 let tm' = inlineTerm ist tm

1116 c <- colourise

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

1118−process fn Execute

1118+process fn (Execute tm)

1119 = idrisCatch

1120 (do ist <- getIState

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

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

1122− (PApp fc

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

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

1125 (tmpn, tmph) <- runIO tempfile

1122 (tmpn, tmph) <- runIO tempfile

1126 runIO $ hClose tmph

1123 runIO $ hClose tmph

1127 t <- codegen

1124 t <- codegen

src/Idris/REPLParser.hs+9−1

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

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

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

73 , (["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)

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

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

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

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

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

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

278

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+

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

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

280cmd_dynamic name = do

288cmd_dynamic name = do

281 let emptyArgs = noArgs ListDynamic name

289 let emptyArgs = noArgs ListDynamic name

test/basic010/Main.idr+1−1

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

38

39main : IO ()

40main = do

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

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

42 putStrLn . show $ getWitness (f 4 n)

43 putStrLn . fmt $ getProof (g 4 n)