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