git.iko.soy/Idris-dev
on ff7ea9d help sign in
Idris-dev/codegen/idris-codegen-c/Main.hs
50 lines 1.5 kB history raw
1module Main where
3import Idris.Core.TT
4import Idris.AbsSyntax
5import Idris.ElabDecls
6import Idris.REPL
8import IRTS.Compiler
9import IRTS.CodegenC
11import System.Environment
12import System.Exit
13import Control.Monad
15import Paths_idris
17import Util.System
19data Opts = Opts { inputs :: [FilePath],
20 interface :: Bool,
21 output :: FilePath }
23showUsage = do putStrLn "A code generator which is intended to be called by the compiler, not by a user."
24 putStrLn "Usage: idris-codegen-c <ibc-files> [-o <output-file>]"
25 exitWith ExitSuccess
27getOpts :: IO Opts
28getOpts = do xs <- getArgs
29 return $ process (Opts [] False "a.out") xs
30 where
31 process opts ("-o":o:xs) = process (opts { output = o }) xs
32 process opts ("--interface":xs) = process (opts { interface = True }) xs
33 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs
34 process opts [] = opts
36c_main :: Opts -> Idris ()
37c_main opts = do runIO setupBundledCC
38 elabPrims
39 loadInputs (inputs opts) Nothing
40 mainProg <- if interface opts
41 then liftM Just elabMain
42 else return Nothing
43 ir <- compile (Via IBCFormat "c") (output opts) mainProg
44 runIO $ codegenC ir
46main :: IO ()
47main = do opts <- getOpts
48 if (null (inputs opts))
49 then showUsage
50 else runMain (c_main opts)