f50f006 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Expand backend control options and infrastructure

f50f006Benjamin Saunders14 years ago

src/IRTS/CodegenC.hs+24−26

compare with master

unifiedsplit

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

1−module IRTS.CodegenC where

1+module IRTS.CodegenC (codegenC) where

3import Idris.AbsSyntax

4import IRTS.Bytecode

5import IRTS.Lang

6import IRTS.Simplified

7+import IRTS.CodegenCommon

7import Core.TT

8import Core.TT

8import Paths_idris

9import Paths_idris

9import Util.System

10import Util.System

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

15import System.Directory

16import System.Directory

16import Control.Monad

17import Control.Monad

18−data DbgLevel = NONE | DEBUG | TRACE

19−

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

21− [(Name, SDecl)] ->

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

22 String -> -- output file name

20 String -> -- output file name

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

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

24 [FilePath] -> -- include files

22 [FilePath] -> -- include files

25 String -> -- extra object files

23 String -> -- extra object files

26 String -> -- extra compiler flags

24 String -> -- extra compiler flags

27 DbgLevel ->

25 DbgLevel ->

28 IO ()

26 IO ()

29−codegenC dump defs out exec incs objs libs dbg

27+codegenC defs out exec incs objs libs dbg

30 = do -- print defs

28 = do -- print defs

31 let bc = map toBC defs

29 let bc = map toBC defs

32 let h = concatMap toDecl (map fst bc)

30 let h = concatMap toDecl (map fst bc)

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

34 d <- getDataDir

32 d <- getDataDir

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

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

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

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

37− (if exec then mprog else "")

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

36+ case exec of

37+ Raw -> writeFile out cout

38+ _ -> do

38− (tmpn, tmph) <- tempfile

39+ (tmpn, tmph) <- tempfile

39− hPutStr tmph cout

40+ hPutStr tmph cout

40− hFlush tmph

41+ hFlush tmph

41− hClose tmph

42+ hClose tmph

42− let useclang = False

43+ let useclang = False

43− comp <- getCC

44+ comp <- getCC

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

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

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

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

46− gccDbg dbg ++

47+ gccDbg dbg ++

47− " " ++ tmpn ++

48+ " " ++ tmpn ++

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

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

49− " -o " ++ out

50+ " -o " ++ out

50− case dump of

51− Just co -> do writeFile co cout

52− Nothing -> return ()

53− exit <- system gcc

51+ exit <- system gcc

54− when (exit /= ExitSuccess) $

52+ when (exit /= ExitSuccess) $

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

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

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

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

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

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

src/IRTS/CodegenCommon.hsnew file+22

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

1+{-# LANGUAGE CPP #-}

3+module IRTS.CodegenCommon where

5+import Core.TT

6+import IRTS.Simplified

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

3import IRTS.BCImp

4import IRTS.Lang

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

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

18 String -> -- output file name

19+ OutputType ->

19 IO ()

20 IO ()

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

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

src/IRTS/Compiler.hs+4−3

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

5import IRTS.Lang

6import IRTS.Defunctionalise

7import IRTS.Simplified

8+import IRTS.CodegenCommon

8import IRTS.CodegenC

9import IRTS.CodegenC

9import IRTS.CodegenJava

10import IRTS.CodegenJava

10import IRTS.Inliner

11import IRTS.Inliner

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

49 iLOG "Resolving variables for CG"

50 iLOG "Resolving variables for CG"

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

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

51 let checked = checkDefs defuns (toAlist defuns)

52 let checked = checkDefs defuns (toAlist defuns)

52− dumpC <- getDumpC

53+ outty <- outputTy

53 dumpCases <- getDumpCases

54 dumpCases <- getDumpCases

54 dumpDefun <- getDumpDefun

55 dumpDefun <- getDumpDefun

55 case dumpCases of

56 case dumpCases of

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

61 iLOG "Building output"

62 iLOG "Building output"

62 case checked of

63 case checked of

63 OK c -> case target of

64 OK c -> case target of

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

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

65 (concatMap mkObj objs)

66 (concatMap mkObj objs)

66 (concatMap mkLib libs) NONE

67 (concatMap mkLib libs) NONE

67− ViaJava -> liftIO $ codegenJava c f

68+ ViaJava -> liftIO $ codegenJava c f outty

68 Error e -> fail $ show e

69 Error e -> fail $ show e

69 where checkMVs = do i <- get

70 where checkMVs = do i <- get

70 case idris_metavars i \\ primDefs of

71 case idris_metavars i \\ primDefs of

src/IRTS/LParser.hs+16−11

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

1module IRTS.LParser where

3+import Idris.AbsSyntaxTree

3import Core.CoreParser

4import Core.CoreParser

4import Core.TT

5import Core.TT

5import IRTS.Lang

6import IRTS.Lang

6import IRTS.Simplified

7import IRTS.Simplified

7import IRTS.Bytecode

8import IRTS.Bytecode

9+import IRTS.CodegenCommon

8import IRTS.CodegenC

10import IRTS.CodegenC

9import IRTS.Defunctionalise

11import IRTS.Defunctionalise

10import Paths_idris

12import Paths_idris

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

45chlit = PTok.charLiteral lexer

47chlit = PTok.charLiteral lexer

46lchar = lexeme.char

48lchar = lexeme.char

48−fovm :: FilePath -> IO ()

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

51+fovm tgt outty f

49−fovm f = do defs <- parseFOVM f

52+ = do defs <- parseFOVM f

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

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

51− let ctxtIn = addAlist tagged emptyContext

54+ ctxtIn = addAlist tagged emptyContext

52− let defuns = defunctionalise nexttag ctxtIn

55+ defuns = defunctionalise nexttag ctxtIn

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

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

54− let checked = checkDefs defuns (toAlist defuns)

57+ let checked = checkDefs defuns (toAlist defuns)

55−-- print checked

58+-- print checked

56− case checked of

59+ case checked of

60+ OK c -> case tgt of

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

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

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

58− Error e -> fail $ show e

63+ Error e -> fail $ show e

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

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

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

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

src/Idris/AbsSyntax.hs+21−7

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

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

9import Core.Typecheck

10import Idris.AbsSyntaxTree

11+import IRTS.CodegenCommon

12import Paths_idris

13import Paths_idris

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

221 let iopts = idris_options i

222 let iopts = idris_options i

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

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

223

224

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−

231getDumpDefun :: Idris (Maybe FilePath)

225getDumpDefun :: Idris (Maybe FilePath)

232getDumpDefun = do i <- get

226getDumpDefun = do i <- get

233 return $ findC (opt_cmdline (idris_options i))

227 return $ findC (opt_cmdline (idris_options i))

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

266 let opt' = opts { opt_repl = t }

260 let opt' = opts { opt_repl = t }

267 put (i { idris_options = opt' })

261 put (i { idris_options = opt' })

268

262

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+

269verbose :: Idris Bool

283verbose :: Idris Bool

270verbose = do i <- get

284verbose = do i <- get

271 return (opt_verbose (idris_options i))

285 return (opt_verbose (idris_options i))

src/Idris/AbsSyntaxTree.hs+7−3

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

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

9import Core.Typecheck

10import IRTS.Lang

11+import IRTS.CodegenCommon

11import Util.Pretty

12import Util.Pretty

13import Paths_idris

14import Paths_idris

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

30 opt_errContext :: Bool,

31 opt_errContext :: Bool,

31 opt_repl :: Bool,

32 opt_repl :: Bool,

32 opt_verbose :: Bool,

33 opt_verbose :: Bool,

34+ opt_target :: Target,

35+ opt_outputTy :: OutputType,

33 opt_ibcsubdir :: FilePath,

36 opt_ibcsubdir :: FilePath,

34 opt_importdirs :: [FilePath],

37 opt_importdirs :: [FilePath],

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

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

36 }

39 }

37 deriving (Show, Eq)

40 deriving (Show, Eq)

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

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

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

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

42-- without typechecking).

45-- without typechecking).

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

138-- Commands in the REPL

141-- Commands in the REPL

139

142

140data Target = ViaC | ViaJava

143data Target = ViaC | ViaJava

144+ deriving (Show, Eq)

141

145

142data Command = Quit

146data Command = Quit

143 | Help

147 | Help

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

202 | WarnOnly

206 | WarnOnly

203 | Pkg String

207 | Pkg String

204 | BCAsm String

208 | BCAsm String

205− | DumpC String

206 | DumpDefun String

209 | DumpDefun String

207 | DumpCases String

210 | DumpCases String

208 | FOVM String

211 | FOVM String

212+ | UseTarget Target

213+ | OutputTy OutputType

209 deriving (Show, Eq)

214 deriving (Show, Eq)

210

215

211−

212-- Parsed declarations

216-- Parsed declarations

213

217

214data Fixity = Infixl { prec :: Int }

218data Fixity = Infixl { prec :: Int }

src/Idris/REPL.hs+25−5

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

28import IRTS.Compiler

29import IRTS.LParser

30+import IRTS.CodegenCommon

31-- import RTS.SC

32-- import RTS.SC

32-- import RTS.Bytecode

33-- import RTS.Bytecode

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

178-- [pexp t])

179-- [pexp t])

179 (tmpn, tmph) <- liftIO tempfile

180 (tmpn, tmph) <- liftIO tempfile

180 liftIO $ hClose tmph

181 liftIO $ hClose tmph

182+ t <- target

181− compile ViaC tmpn tm

183+ compile t tmpn tm

182 liftIO $ system tmpn

184 liftIO $ system tmpn

183 return ()

185 return ()

184 where fc = FC "(input)" 0

186 where fc = FC "(input)" 0

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

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

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

335 (tmpn, tmph) <- liftIO tempfile

337 (tmpn, tmph) <- liftIO tempfile

336 liftIO $ hClose tmph

338 liftIO $ hClose tmph

339+ t <- target

337− compile ViaC tmpn m

340+ compile t tmpn m

338 liftIO $ system tmpn

341 liftIO $ system tmpn

339 return ()

342 return ()

340 where fc = FC "main" 0

343 where fc = FC "main" 0

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

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

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

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

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

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

448parseArgs ("--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)

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

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

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

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

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

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

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

489 let bcs = opt getBC opts

493 let bcs = opt getBC opts

490 let vm = opt getFOVM opts

494 let vm = opt getFOVM opts

491 let pkgdirs = opt getPkgDir opts

495 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

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

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

493 put (i { default_total = True })

503 put (i { default_total = True })

494 setREPL runrepl

504 setREPL runrepl

495 setVerbose runrepl

505 setVerbose runrepl

496 setCmdLine opts

506 setCmdLine opts

507+ setOutputTy outty

508+ setTarget tgt

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

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

498 mapM_ makeOption opts

510 mapM_ makeOption opts

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

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

500 case vm of

512 case vm of

501 [] -> return ()

513 [] -> return ()

502− xs -> liftIO $ mapM_ fovm xs

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

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

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

504 case bcs of

516 case bcs of

505 [] -> return ()

517 [] -> return ()

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

519 ok <- noErrors

531 ok <- noErrors

520 when ok $ case output of

532 when ok $ case output of

521 [] -> return ()

533 [] -> return ()

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

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

523 when ok $ case newoutput of

535 when ok $ case newoutput of

524 [] -> return ()

536 [] -> return ()

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

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

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

579getPkgClean (PkgClean str) = Just str

591getPkgClean (PkgClean str) = Just str

580getPkgClean _ = Nothing

592getPkgClean _ = Nothing

581

593

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+

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

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

583opt = mapMaybe

603opt = mapMaybe

584

604

src/Main.hs+3−3

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

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

77 "Options:\n" ++

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

91−