git.iko.soy/Idris-dev
on f88a377 help sign in
Idris-dev/codegen/idris-codegen-c/Main.hs
57 lines 2.0 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 { really :: Bool,
20 inputs :: [FilePath],
21 interface :: Bool,
22 output :: FilePath }
24showUsage = do putStrLn "A code generator which is intended to be called by the compiler, not by a user."
25 putStrLn "To call the code generator manually, pass the --yes-really option.\n"
26 putStrLn "Usage: idris-codegen-c [--yes-really] <ibc-files> [-o <output-file>]"
27 exitWith ExitSuccess
29getOpts :: IO Opts
30getOpts = do xs <- getArgs
31 return $ process (Opts False [] False "a.out") xs
32 where
33 process opts ("--yes-really":xs) = process (opts { really = True }) xs
34 process opts ("-o":o:xs) = process (opts { output = o }) xs
35 process opts ("--interface":xs) = process (opts { interface = True }) xs
36 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs
37 process opts [] = opts
39c_main :: Opts -> Idris ()
40c_main opts = do runIO setupBundledCC
41 elabPrims
42 loadInputs (inputs opts) Nothing
43 mainProg <- if interface opts
44 then liftM Just elabMain
45 else return Nothing
46 ir <- compile (Via "c") (output opts) mainProg
47 runIO $ codegenC ir
49main :: IO ()
50main = do opts <- getOpts
51 if (null (inputs opts))
52 then showUsage
53 else if (not $ really opts)
54 then do putStrLn "This code generator is intended to be called by the Idris compiler. \
55 \Please pass Idris the '--codegen' flag to choose a backend."
56 exitWith ExitSuccess
57 else runMain (c_main opts)