git.iko.soy/Idris-dev
on f4bcbbc help sign in
Idris-dev/codegen/idris-codegen-javascript/Main.hs
50 lines 1.8 kB history raw
1module Main where
3import Idris.Core.TT
4import Idris.AbsSyntax
5import Idris.ElabDecls
6import Idris.REPL
8import IRTS.Compiler
9import IRTS.CodegenJavaScript
11import System.Environment
12import System.Exit
14import Paths_idris
16data Opts = Opts { really :: Bool
17 , inputs :: [FilePath]
18 , output :: FilePath
19 }
21showUsage = do putStrLn "A code generator which is intended to be called by the compiler, not by a user."
22 putStrLn "To call the code generator manually, pass the --yes-really option.\n"
23 putStrLn "Usage: idris-codegen-c [--yes-really] <ibc-files> [-o <output-file>]"
24 exitWith ExitSuccess
26getOpts :: IO Opts
27getOpts = do xs <- getArgs
28 return $ process (Opts False [] "main.js") xs
29 where
30 process opts ("--yes-really":xs) = process (opts { really = True }) xs
31 process opts ("-o":o:xs) = process (opts { output = o }) xs
32 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs
33 process opts [] = opts
35jsMain :: Opts -> Idris ()
36jsMain opts = do elabPrims
37 loadInputs (inputs opts) Nothing
38 mainProg <- elabMain
39 ir <- compile (Via "javascript") (output opts) (Just mainProg)
40 runIO $ codegenJavaScript ir
42main :: IO ()
43main = do opts <- getOpts
44 if (null (inputs opts))
45 then showUsage
46 else if (not $ really opts)
47 then do putStrLn "This code generator is intended to be called by the Idris compiler. \
48 \Please pass Idris the '--codegen' flag to choose a backend."
49 exitWith ExitSuccess
50 else runMain (jsMain opts)