f50f006 · Idris-dev · git.iko.soy

src/IRTS/CodegenC.hs+24−26

@@ -1,9 +1,10 @@

1−module IRTS.CodegenC where

1+module IRTS.CodegenC (codegenC) where

22

33import Idris.AbsSyntax

44import IRTS.Bytecode

55import IRTS.Lang

66import IRTS.Simplified

7+import IRTS.CodegenCommon

78import Core.TT

89import Paths_idris

910import Util.System

@@ -15,18 +16,15 @@ import System.IO

1516import System.Directory

1617import Control.Monad

1718

18−data DbgLevel = NONE | DEBUG | TRACE

19−

20−codegenC :: Maybe FilePath -> -- dump output

21− [(Name, SDecl)] ->

19+codegenC :: [(Name, SDecl)] ->

2220 String -> -- output file name

23− Bool -> -- generate executable if True, only .o if False

21+ OutputType -> -- generate executable if True, only .o if False

2422 [FilePath] -> -- include files

2523 String -> -- extra object files

2624 String -> -- extra compiler flags

2725 DbgLevel ->

2826 IO ()

29−codegenC dump defs out exec incs objs libs dbg

27+codegenC defs out exec incs objs libs dbg

3028 = do -- print defs

3129 let bc = map toBC defs

3230 let h = concatMap toDecl (map fst bc)

@@ -34,25 +32,25 @@ codegenC dump defs out exec incs objs libs dbg

3432 d <- getDataDir

3533 mprog <- readFile (d ++ "/rts/idris_main.c")

3634 let cout = headers incs ++ debug dbg ++ h ++ cc ++

37− (if exec then mprog else "")

38− (tmpn, tmph) <- tempfile

39− hPutStr tmph cout

40− hFlush tmph

41− hClose tmph

42− let useclang = False

43− comp <- getCC

44− let gcc = comp ++ " -I. " ++ objs ++ " -x c " ++

45− (if exec then "" else " - c ") ++

46− gccDbg dbg ++

47− " " ++ tmpn ++

48− " `idris --link` `idris --include` " ++ libs ++

49− " -o " ++ out

50− case dump of

51− Just co -> do writeFile co cout

52− Nothing -> return ()

53− exit <- system gcc

54− when (exit /= ExitSuccess) $

55− putStrLn ("FAILURE: " ++ gcc)

35+ (if (exec == Executable) then mprog else "")

36+ case exec of

37+ Raw -> writeFile out cout

38+ _ -> do

39+ (tmpn, tmph) <- tempfile

40+ hPutStr tmph cout

41+ hFlush tmph

42+ hClose tmph

43+ let useclang = False

44+ comp <- getCC

45+ let gcc = comp ++ " -I. " ++ objs ++ " -x c " ++

46+ (if (exec == Executable) then "" else " -c ") ++

47+ gccDbg dbg ++

48+ " " ++ tmpn ++

49+ " `idris --link` `idris --include` " ++ libs ++

50+ " -o " ++ out

51+ exit <- system gcc

52+ when (exit /= ExitSuccess) $

53+ putStrLn ("FAILURE: " ++ gcc)

5654

5755headers [] = "#include <idris_rts.h>\n#include <idris_stdfgn.h>\n" ++

5856 "#include <gmp.h>\n#include <assert.h>\n"

src/IRTS/CodegenCommon.hsnew file+22

@@ -0,0 +1,22 @@

1+{-# LANGUAGE CPP #-}

2+

3+module IRTS.CodegenCommon where

4+

5+import Core.TT

6+import IRTS.Simplified

7+

8+import Control.Exception

9+import System.Environment

10+

11+data DbgLevel = NONE | DEBUG | TRACE deriving Eq

12+data OutputType = Raw | Object | Executable deriving (Eq, Show)

13+

14+environment :: String -> IO (Maybe String)

15+environment x = catch (do e <- getEnv x

16+ return (Just e))

17+#if MIN_VERSION_base(4,6,0)

18+ (\y-> do return (y::SomeException); return Nothing)

19+#endif

20+#if !MIN_VERSION_base(4,6,0)

21+ (\_-> return Nothing)

22+#endif

src/IRTS/CodegenJava.hs+3−2

@@ -1,4 +1,4 @@

1−module IRTS.CodegenJava where

1+module IRTS.CodegenJava (codegenJava) where

22

33import IRTS.BCImp

44import IRTS.Lang

@@ -16,6 +16,7 @@ import Control.Monad

1616

1717codegenJava :: [(Name, SDecl)] ->

1818 String -> -- output file name

19+ OutputType ->

1920 IO ()

20−codegenJava defs out = putStrLn "Not implemented yet"

21+codegenJava defs out exec = putStrLn "Not implemented yet"

2122

src/IRTS/Compiler.hs+4−3

@@ -5,6 +5,7 @@ module IRTS.Compiler where

55import IRTS.Lang

66import IRTS.Defunctionalise

77import IRTS.Simplified

8+import IRTS.CodegenCommon

89import IRTS.CodegenC

910import IRTS.CodegenJava

1011import IRTS.Inliner

@@ -49,7 +50,7 @@ compile target f tm

4950 iLOG "Resolving variables for CG"

5051 -- iputStrLn $ showSep "\n" (map show (toAlist defuns))

5152 let checked = checkDefs defuns (toAlist defuns)

52− dumpC <- getDumpC

53+ outty <- outputTy

5354 dumpCases <- getDumpCases

5455 dumpDefun <- getDumpDefun

5556 case dumpCases of

@@ -61,10 +62,10 @@ compile target f tm

6162 iLOG "Building output"

6263 case checked of

6364 OK c -> case target of

64− ViaC -> liftIO $ codegenC dumpC c f True hdrs

65+ ViaC -> liftIO $ codegenC c f outty hdrs

6566 (concatMap mkObj objs)

6667 (concatMap mkLib libs) NONE

67− ViaJava -> liftIO $ codegenJava c f

68+ ViaJava -> liftIO $ codegenJava c f outty

6869 Error e -> fail $ show e

6970 where checkMVs = do i <- get

7071 case idris_metavars i \\ primDefs of

src/IRTS/LParser.hs+16−11

@@ -1,10 +1,12 @@

11module IRTS.LParser where

22

3+import Idris.AbsSyntaxTree

34import Core.CoreParser

45import Core.TT

56import IRTS.Lang

67import IRTS.Simplified

78import IRTS.Bytecode

9+import IRTS.CodegenCommon

810import IRTS.CodegenC

911import IRTS.Defunctionalise

1012import Paths_idris

@@ -45,17 +47,20 @@ strlit = PTok.stringLiteral lexer

4547chlit = PTok.charLiteral lexer

4648lchar = lexeme.char

4749

48−fovm :: FilePath -> IO ()

49−fovm f = do defs <- parseFOVM f

50− let (nexttag, tagged) = addTags 0 (liftAll defs)

51− let ctxtIn = addAlist tagged emptyContext

52− let defuns = defunctionalise nexttag ctxtIn

53− putStrLn $ showSep "\n" (map show (toAlist defuns))

54− let checked = checkDefs defuns (toAlist defuns)

55−-- print checked

56− case checked of

57− OK c -> codegenC Nothing c "a.out" True ["math.h"] "" "" TRACE

58− Error e -> fail $ show e

50+fovm :: Target -> OutputType -> FilePath -> IO ()

51+fovm tgt outty f

52+ = do defs <- parseFOVM f

53+ let (nexttag, tagged) = addTags 0 (liftAll defs)

54+ ctxtIn = addAlist tagged emptyContext

55+ defuns = defunctionalise nexttag ctxtIn

56+ putStrLn $ showSep "\n" (map show (toAlist defuns))

57+ let checked = checkDefs defuns (toAlist defuns)

58+-- print checked

59+ case checked of

60+ OK c -> case tgt of

61+ ViaC -> codegenC c "a.out" outty ["math.h"] "" "" TRACE

62+ ViaJava -> codegenJava c "a.out" outty

63+ Error e -> fail $ show e

5964

6065parseFOVM :: FilePath -> IO [(Name, LDecl)]

6166parseFOVM fname = do -- putStrLn $ "Reading " ++ fname

src/Idris/AbsSyntax.hs+21−7

@@ -8,6 +8,7 @@ import Core.Evaluate

88import Core.Elaborate hiding (Tactic(..))

99import Core.Typecheck

1010import Idris.AbsSyntaxTree

11+import IRTS.CodegenCommon

1112

1213import Paths_idris

1314

@@ -221,13 +222,6 @@ setCmdLine opts = do i <- get

221222 let iopts = idris_options i

222223 put (i { idris_options = iopts { opt_cmdline = opts } })

223224

224−getDumpC :: Idris (Maybe FilePath)

225−getDumpC = do i <- get

226− return $ findC (opt_cmdline (idris_options i))

227− where findC [] = Nothing

228− findC (DumpC x : _) = Just x

229− findC (_ : xs) = findC xs

230−

231225getDumpDefun :: Idris (Maybe FilePath)

232226getDumpDefun = do i <- get

233227 return $ findC (opt_cmdline (idris_options i))

@@ -266,6 +260,26 @@ setREPL t = do i <- get

266260 let opt' = opts { opt_repl = t }

267261 put (i { idris_options = opt' })

268262

263+setTarget :: Target -> Idris ()

264+setTarget t = do i <- get

265+ let opts = idris_options i

266+ let opt' = opts { opt_target = t }

267+ put (i { idris_options = opt' })

268+

269+target :: Idris Target

270+target = do i <- get

271+ return (opt_target (idris_options i))

272+

273+setOutputTy :: OutputType -> Idris ()

274+setOutputTy t = do i <- get

275+ let opts = idris_options i

276+ let opt' = opts { opt_outputTy = t }

277+ put (i { idris_options = opt' })

278+

279+outputTy :: Idris OutputType

280+outputTy = do i <- get

281+ return $ opt_outputTy $ idris_options i

282+

269283verbose :: Idris Bool

270284verbose = do i <- get

271285 return (opt_verbose (idris_options i))

src/Idris/AbsSyntaxTree.hs+7−3

@@ -8,6 +8,7 @@ import Core.Evaluate

88import Core.Elaborate hiding (Tactic(..))

99import Core.Typecheck

1010import IRTS.Lang

11+import IRTS.CodegenCommon

1112import Util.Pretty

1213

1314import Paths_idris

@@ -30,13 +31,15 @@ data IOption = IOption { opt_logLevel :: Int,

3031 opt_errContext :: Bool,

3132 opt_repl :: Bool,

3233 opt_verbose :: Bool,

34+ opt_target :: Target,

35+ opt_outputTy :: OutputType,

3336 opt_ibcsubdir :: FilePath,

3437 opt_importdirs :: [FilePath],

3538 opt_cmdline :: [Opt] -- remember whole command line

3639 }

3740 deriving (Show, Eq)

3841

39−defaultOpts = IOption 0 False False True False False True True "" [] []

42+defaultOpts = IOption 0 False False True False False True True ViaC Executable "" [] []

4043

4144-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

4245-- without typechecking).

@@ -138,6 +141,7 @@ type Idris = StateT IState (InputT IO)

138141-- Commands in the REPL

139142

140143data Target = ViaC | ViaJava

144+ deriving (Show, Eq)

141145

142146data Command = Quit

143147 | Help

@@ -202,13 +206,13 @@ data Opt = Filename String

202206 | WarnOnly

203207 | Pkg String

204208 | BCAsm String

205− | DumpC String

206209 | DumpDefun String

207210 | DumpCases String

208211 | FOVM String

212+ | UseTarget Target

213+ | OutputTy OutputType

209214 deriving (Show, Eq)

210215

211−

212216-- Parsed declarations

213217

214218data Fixity = Infixl { prec :: Int }

src/Idris/REPL.hs+25−5

@@ -27,6 +27,7 @@ import Core.Constraints

2727

2828import IRTS.Compiler

2929import IRTS.LParser

30+import IRTS.CodegenCommon

3031

3132-- import RTS.SC

3233-- import RTS.Bytecode

@@ -178,7 +179,8 @@ process fn (ExecVal t)

178179-- [pexp t])

179180 (tmpn, tmph) <- liftIO tempfile

180181 liftIO $ hClose tmph

181− compile ViaC tmpn tm

182+ t <- target

183+ compile t tmpn tm

182184 liftIO $ system tmpn

183185 return ()

184186 where fc = FC "(input)" 0

@@ -334,7 +336,8 @@ process fn Execute = do (m, _) <- elabVal toplevel False

334336-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))

335337 (tmpn, tmph) <- liftIO tempfile

336338 liftIO $ hClose tmph

337− compile ViaC tmpn m

339+ t <- target

340+ compile t tmpn m

338341 liftIO $ system tmpn

339342 return ()

340343 where fc = FC "main" 0

@@ -443,7 +446,8 @@ parseArgs ("--install":n:ns) = PkgInstall n : (parseArgs ns)

443446parseArgs ("--clean":n:ns) = PkgClean n : (parseArgs ns)

444447parseArgs ("--bytecode":n:ns) = NoREPL : BCAsm n : (parseArgs ns)

445448parseArgs ("--fovm":n:ns) = NoREPL : FOVM n : (parseArgs ns)

446−parseArgs ("--dumpc":n:ns) = DumpC n : (parseArgs ns)

449+parseArgs ("-S":ns) = OutputTy Raw : (parseArgs ns)

450+parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)

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

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

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

@@ -489,17 +493,25 @@ idrisMain opts =

489493 let bcs = opt getBC opts

490494 let vm = opt getFOVM opts

491495 let pkgdirs = opt getPkgDir opts

496+ let outty = case opt getOutputTy opts of

497+ [] -> Executable

498+ xs -> last xs

499+ let tgt = case opt getTarget opts of

500+ [] -> ViaC

501+ xs -> last xs

492502 when (DefaultTotal `elem` opts) $ do i <- get

493503 put (i { default_total = True })

494504 setREPL runrepl

495505 setVerbose runrepl

496506 setCmdLine opts

507+ setOutputTy outty

508+ setTarget tgt

497509 when (Verbose `elem` opts) $ setVerbose True

498510 mapM_ makeOption opts

499511 -- if we have the --fovm flag, drop into the first order VM testing

500512 case vm of

501513 [] -> return ()

502− xs -> liftIO $ mapM_ fovm xs

514+ xs -> liftIO $ mapM_ (fovm tgt outty) xs

503515 -- if we have the --bytecode flag, drop into the bytecode assembler

504516 case bcs of

505517 [] -> return ()

@@ -519,7 +531,7 @@ idrisMain opts =

519531 ok <- noErrors

520532 when ok $ case output of

521533 [] -> return ()

522− (o:_) -> process "" (Compile ViaC o)

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

523535 when ok $ case newoutput of

524536 [] -> return ()

525537 (o:_) -> process "" (NewCompile o)

@@ -579,6 +591,14 @@ getPkgClean :: Opt -> Maybe String

579591getPkgClean (PkgClean str) = Just str

580592getPkgClean _ = Nothing

581593

594+getTarget :: Opt -> Maybe Target

595+getTarget (UseTarget x) = Just x

596+getTarget _ = Nothing

597+

598+getOutputTy :: Opt -> Maybe OutputType

599+getOutputTy (OutputTy t) = Just t

600+getOutputTy _ = Nothing

601+

582602opt :: (Opt -> Maybe a) -> [Opt] -> [a]

583603opt = mapMaybe

584604

src/Main.hs+3−3

@@ -76,7 +76,7 @@ usagemsg = "Idris version " ++ ver ++ "\n" ++

7676 "Usage: idris [input file] [options]\n" ++

7777 "Options:\n" ++

7878 "\t--check Type check only\n" ++

79− "\t-o [file] Generate executable\n" ++

79+ "\t-o [file] Specify output filename\n" ++

8080 "\t-i [dir] Add directory to the list of import paths\n" ++

8181 "\t--ibcsubdir [dir] Write IBC files into sub directory\n" ++

8282 "\t--noprelude Don't import the prelude\n" ++

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

8484 "\t--warnpartial Warn about undeclared partial functions\n" ++

8585 "\t--typeintype Disable universe checking\n" ++

8686 "\t--log [level] Set debugging log level\n" ++

87− "\t--dumpc [file] Dump generated C code\n" ++

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

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

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

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

9091 "\t--include Show C include directories and exit (for C linking)\n"

91−