783ddc3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Invoke external code generator

If --codegen specifies somethng which isn't one of the built-in code generators, invoke an external CG. For --codegen foo, this should be a command which takes the following form: idris-foo <ibc-file-list> [-o <output-file>] idris-foo should read the ibc files, and generate an output file called <output-file>. Naturally it's easiest to use Idris as a library to do this. See the codegen/ directory in the Idris-dev repository for examples.

commit783ddc3a9822b125e64a63670fe8165d2bf8bfde authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 7 Aug 2014, 18:05 (12 years ago) parent44b38a6

3 files changed+26−11

compare with master

unifiedsplit

src/IRTS/Compiler.hs+17−8 src/Idris/REPL.hs+3−2 src/Idris/REPLParser.hs+6−1

src/IRTS/Compiler.hs+17−8

@@ -43,6 +43,7 @@ import qualified Data.Map as M

4343import qualified Data.Set as S

4444import System.Process

4545import System.IO

46+import System.Exit

4647import System.Directory

4748import System.Environment

4849import System.FilePath ((</>), addTrailingPathSeparator)

@@ -114,14 +115,22 @@ compile codegen f tm

114115 ex <- doesFileExist f

115116 if ex then return f else return h

116117

117−generate :: Codegen -> CodegenInfo -> IO ()

118−generate codegen ir = case codegen of

119− Via "c" -> codegenC ir

120− Via "java" -> codegenJava ir

121− Via "javascript" -> codegenJavaScript ir

122− Via "node" -> codegenNode ir

123− Via "llvm" -> codegenLLVM ir

124− Bytecode -> dumpBC (simpleDecls ir) (outputFile ir)

118+generate :: Codegen -> FilePath -> CodegenInfo -> IO ()

119+generate codegen mainmod ir

120+ = case codegen of

121+ -- Built-in code generators (FIXME: lift these out!)

122+ Via "c" -> codegenC ir

123+ Via "java" -> codegenJava ir

124+ Via "javascript" -> codegenJavaScript ir

125+ Via "node" -> codegenNode ir

126+ Via "llvm" -> codegenLLVM ir

127+ -- Any external code generator

128+ Via cg -> do let cmd = "idris-" ++ cg ++ " " ++ mainmod ++

129+ " -o " ++ outputFile ir

130+ exit <- system cmd

131+ when (exit /= ExitSuccess) $

132+ putStrLn ("FAILURE: " ++ show cmd)

133+ Bytecode -> dumpBC (simpleDecls ir) (outputFile ir)

125134

126135irMain :: TT Name -> Idris LDecl

127136irMain tm = do

src/Idris/REPL.hs+3−2

@@ -1040,7 +1040,7 @@ process fn Execute

10401040 runIO $ hClose tmph

10411041 t <- codegen

10421042 ir <- compile t tmpn m

1043− runIO $ generate t ir

1043+ runIO $ generate t (head (idris_imported ist)) ir

10441044 case idris_outputmode ist of

10451045 RawOutput h -> do runIO $ system tmpn

10461046 return ()

@@ -1053,7 +1053,8 @@ process fn (Compile codegen f)

10531053 (PApp fc (PRef fc (sUN "run__IO"))

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

10551055 ir <- compile codegen f m

1056− runIO $ generate codegen ir

1056+ i <- getIState

1057+ runIO $ generate codegen (head (idris_imported i)) ir

10571058 where fc = fileFC "main"

10581059process fn (LogLvl i) = setLogLevel i

10591060-- Elaborate as if LHS of a pattern (debug command)

src/Idris/REPLParser.hs+6−1

@@ -41,9 +41,14 @@ pCmd = do P.whiteSpace; do cmd ["q", "quit"]; eof; return Quit

4141 return (ModImport (toPath f))

4242 <|> do cmd ["e", "edit"]; eof; return Edit

4343 <|> do cmd ["exec", "execute"]; eof; return Execute

44+ <|> try (do cmd ["c", "compile"]

45+ i <- get

46+ f <- P.identifier

47+ eof

48+ return (Compile (Via "c") f))

4449 <|> do cmd ["c", "compile"]

4550 i <- get

46− c <- option (opt_codegen $ idris_options i) codegenOption

51+ c <- codegenOption

4752 f <- P.identifier

4853 eof

4954 return (Compile c f)