c6574b4 · Idris-dev · git.iko.soy

codegen/idris-c/Main.hsnew file+44

compare with master

unifiedsplit

@@ -0,0 +1,44 @@

1+module Main where

2+

3+import Idris.Core.TT

4+import Idris.AbsSyntax

5+import Idris.ElabDecls

6+import Idris.REPL

7+

8+import IRTS.Compiler

9+import IRTS.CodegenC

10+

11+import System.Environment

12+import System.Exit

13+

14+import Paths_idris

15+

16+data Opts = Opts { inputs :: [FilePath],

17+ output :: FilePath }

18+

19+showUsage = do putStrLn "Usage: idris-c <ibc-files> [-o <output-file>]"

20+ exitWith ExitSuccess

21+

22+getOpts :: IO Opts

23+getOpts = do xs <- getArgs

24+ return $ process (Opts [] "a.out") xs

25+ where

26+ process opts ("-o":o:xs) = process (opts { output = o }) xs

27+ process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs

28+ process opts [] = opts

29+

30+c_main :: Opts -> Idris ()

31+c_main opts = do elabPrims

32+ loadInputs (inputs opts) Nothing

33+ mainProg <- elabMain

34+ ir <- compile (Via "c") (output opts) mainProg

35+ runIO $ codegenC ir

36+

37+main :: IO ()

38+main = do opts <- getOpts

39+ if (null (inputs opts))

40+ then showUsage

41+ else runMain (c_main opts)

42+

43+

44+

idris.cabal+12

@@ -743,4 +743,16 @@ Executable idris

743 ghc-prof-options: -auto-all -caf-all

744 ghc-options: -threaded -rtsopts -funbox-strict-fields

745

746+Executable idris-c

747+ Main-is: Main.hs

748+ hs-source-dirs: codegen/idris-c

749+

750+ Build-depends: idris

751+ , base

752+ , filepath

753+ , haskeline >= 0.7

754+ , transformers

755+

756+ ghc-prof-options: -auto-all -caf-all

757+ ghc-options: -threaded -rtsopts -funbox-strict-fields

746

758

main/Main.hs+1−4

@@ -38,10 +38,7 @@ import Paths_idris

38-- on with the REPL.

39

40main = do opts <- runArgParser

41− result <- runErrorT $ execStateT (runIdris opts) idrisInit

41+ runMain (runIdris opts)

42− case result of

43− Left err -> putStrLn $ "Uncaught error: " ++ show err

44− Right _ -> return ()

45

42

46runIdris :: [Opt] -> Idris ()

43runIdris :: [Opt] -> Idris ()

47runIdris [Client c] = do setVerbose False

44runIdris [Client c] = do setVerbose False

src/Idris/ElabDecls.hs+8

@@ -63,6 +63,14 @@ import Util.Pretty(pretty, text)

63recinfo :: ElabInfo

64recinfo = EInfo [] emptyContext id Nothing elabDecl'

65

66+-- | Return the elaborated term which calls 'main'

67+elabMain :: Idris Term

68+elabMain = do (m, _) <- elabVal recinfo ERHS

69+ (PApp fc (PRef fc (sUN "run__IO"))

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

71+ return m

72+ where fc = fileFC "toplevel"

73+

66-- | Elaborate primitives

74-- | Elaborate primitives

67elabPrims :: Idris ()

75elabPrims :: Idris ()

68elabPrims = do mapM_ (elabDecl' EAll recinfo)

76elabPrims = do mapM_ (elabDecl' EAll recinfo)

src/Idris/REPL.hs+6

@@ -1472,6 +1472,12 @@ idrisMain opts =

1472 addImportDir (ddir </> p)

1473 addIBC (IBCImportDir (ddir </> p))

1474

1475+runMain :: Idris () -> IO ()

1476+runMain prog = do res <- runErrorT $ execStateT prog idrisInit

1477+ case res of

1478+ Left err -> putStrLn $ "Uncaught error: " ++ show err

1479+ Right _ -> return ()

1480+

1475execScript :: String -> Idris ()

1481execScript :: String -> Idris ()

1476execScript expr = do i <- getIState

1482execScript expr = do i <- getIState

1477 c <- colourise

1483 c <- colourise