4ff3b25 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added --dumpc flag

commit4ff3b25441c231c2da55903eaff53054ca6b85f9 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 7 Oct 2012, 15:15 (14 years ago) parentbb76c6c

8 files changed+32−8

compare with master

unifiedsplit

CHANGELOG+3 src/IRTS/CodegenC.hs+7−4 src/IRTS/Compiler.hs+2−1 src/IRTS/LParser.hs+1−1 src/Idris/AbsSyntax.hs+12 src/Idris/AbsSyntaxTree.hs+4−2 src/Idris/REPL.hs+2 src/Main.hs+1

CHANGELOG+3

@@ -4,10 +4,13 @@ New in 0.9.4:

44User visible changes:

66* Simple packaging system

7+* Added --dumpc flag for displaying generated code

89Internal changes:

910

1011* Improve overloading resolution (especially where this is a type error)

12+* Various important bug fixes with evaluation and compilation

13+* More aggressive compile-time evaluation

1114

1215New in 0.9.3:

1316-------------

src/IRTS/CodegenC.hs+7−4

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

1616

1717data DbgLevel = NONE | DEBUG | TRACE

1818

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

19+codegenC :: Maybe FilePath -> -- dump output

20+ [(Name, SDecl)] ->

2021 String -> -- output file name

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

2223 [FilePath] -> -- include files

@@ -24,7 +25,7 @@ codegenC :: [(Name, SDecl)] ->

2425 String -> -- extra compiler flags

2526 DbgLevel ->

2627 IO ()

27−codegenC defs out exec incs objs libs dbg

28+codegenC dump defs out exec incs objs libs dbg

2829 = do -- print defs

2930 let bc = map toBC defs

3031 let h = concatMap toDecl (map fst bc)

@@ -45,12 +46,14 @@ codegenC defs out exec incs objs libs dbg

4546 " " ++ tmpn ++

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

4748 " -o " ++ out

48− -- putStrLn cout

49+ case dump of

50+ Just co -> do writeFile co cout

51+ Nothing -> return ()

4952 exit <- system gcc

5053 when (exit /= ExitSuccess) $

5154 putStrLn ("FAILURE: " ++ gcc)

5255

53−headers [] = "#include <idris_rts.h>\n#include <idris_stdfgn.h>\n#include<assert.h>\n"

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

5457headers (x : xs) = "#include <" ++ x ++ ">\n" ++ headers xs

5558

5659debug TRACE = "#define IDRIS_TRACE\n\n"

src/IRTS/Compiler.hs+2−1

@@ -46,9 +46,10 @@ compile target f tm

4646

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

4848 let checked = checkDefs defuns (toAlist defuns)

49+ dumpC <- getDumpC

4950 case checked of

5051 OK c -> case target of

51− ViaC -> liftIO $ codegenC c f True hdrs

52+ ViaC -> liftIO $ codegenC dumpC c f True hdrs

5253 (concatMap mkObj objs)

5354 (concatMap mkLib libs) NONE

5455 ViaJava -> liftIO $ codegenJava c f

src/IRTS/LParser.hs+1−1

@@ -54,7 +54,7 @@ fovm f = do defs <- parseFOVM f

5454 let checked = checkDefs defuns (toAlist defuns)

5555-- print checked

5656 case checked of

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

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

5858 Error e -> fail $ show e

5959

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

src/Idris/AbsSyntax.hs+12

@@ -194,6 +194,18 @@ setLogLevel l = do i <- get

194194 let opt' = opts { opt_logLevel = l }

195195 put (i { idris_options = opt' } )

196196

197+setCmdLine :: [Opt] -> Idris ()

198+setCmdLine opts = do i <- get

199+ let iopts = idris_options i

200+ put (i { idris_options = iopts { opt_cmdline = opts } })

201+

202+getDumpC :: Idris (Maybe FilePath)

203+getDumpC = do i <- get

204+ return $ findC (opt_cmdline (idris_options i))

205+ where findC [] = Nothing

206+ findC (DumpC x : _) = Just x

207+ findC (_ : xs) = findC xs

208+

197209logLevel :: Idris Int

198210logLevel = do i <- get

199211 return (opt_logLevel (idris_options i))

src/Idris/AbsSyntaxTree.hs+4−2

@@ -31,11 +31,12 @@ data IOption = IOption { opt_logLevel :: Int,

3131 opt_repl :: Bool,

3232 opt_verbose :: Bool,

3333 opt_ibcsubdir :: FilePath,

34− opt_importdirs :: [FilePath]

34+ opt_importdirs :: [FilePath],

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

3536 }

3637 deriving (Show, Eq)

3738

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

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

3940

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

4142-- without typechecking).

@@ -171,6 +172,7 @@ data Opt = Filename String

171172 | WarnOnly

172173 | Pkg String

173174 | BCAsm String

175+ | DumpC String

174176 | FOVM String

175177 deriving (Show, Eq)

176178

src/Idris/REPL.hs+2

@@ -392,6 +392,7 @@ parseArgs ("--install":n:ns) = PkgInstall n : (parseArgs ns)

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

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

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

395+parseArgs ("--dumpc":n:ns) = DumpC n : (parseArgs ns)

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

396397

397398help =

@@ -434,6 +435,7 @@ idrisMain opts =

434435 let pkgdirs = opt getPkgDir opts

435436 setREPL runrepl

436437 setVerbose runrepl

438+ setCmdLine opts

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

438440 mapM_ makeOption opts

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

src/Main.hs+1

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

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

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

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

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

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

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

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