mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-19 04:57:24 +03:00
Added idris-c executable
Eventually, this should be the only way to invoke code generators (by invoking "idris-foo Main.ibc" for the code generator for backend foo. For the moment, this serves as an example 'main' for any new code generators, and *all* new code generators should be implemented this way.
This commit is contained in:
parent
93f407d65e
commit
c6574b43c6
44
codegen/idris-c/Main.hs
Normal file
44
codegen/idris-c/Main.hs
Normal file
@ -0,0 +1,44 @@
|
||||
module Main where
|
||||
|
||||
import Idris.Core.TT
|
||||
import Idris.AbsSyntax
|
||||
import Idris.ElabDecls
|
||||
import Idris.REPL
|
||||
|
||||
import IRTS.Compiler
|
||||
import IRTS.CodegenC
|
||||
|
||||
import System.Environment
|
||||
import System.Exit
|
||||
|
||||
import Paths_idris
|
||||
|
||||
data Opts = Opts { inputs :: [FilePath],
|
||||
output :: FilePath }
|
||||
|
||||
showUsage = do putStrLn "Usage: idris-c <ibc-files> [-o <output-file>]"
|
||||
exitWith ExitSuccess
|
||||
|
||||
getOpts :: IO Opts
|
||||
getOpts = do xs <- getArgs
|
||||
return $ process (Opts [] "a.out") xs
|
||||
where
|
||||
process opts ("-o":o:xs) = process (opts { output = o }) xs
|
||||
process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs
|
||||
process opts [] = opts
|
||||
|
||||
c_main :: Opts -> Idris ()
|
||||
c_main opts = do elabPrims
|
||||
loadInputs (inputs opts) Nothing
|
||||
mainProg <- elabMain
|
||||
ir <- compile (Via "c") (output opts) mainProg
|
||||
runIO $ codegenC ir
|
||||
|
||||
main :: IO ()
|
||||
main = do opts <- getOpts
|
||||
if (null (inputs opts))
|
||||
then showUsage
|
||||
else runMain (c_main opts)
|
||||
|
||||
|
||||
|
12
idris.cabal
12
idris.cabal
@ -743,4 +743,16 @@ Executable idris
|
||||
ghc-prof-options: -auto-all -caf-all
|
||||
ghc-options: -threaded -rtsopts -funbox-strict-fields
|
||||
|
||||
Executable idris-c
|
||||
Main-is: Main.hs
|
||||
hs-source-dirs: codegen/idris-c
|
||||
|
||||
Build-depends: idris
|
||||
, base
|
||||
, filepath
|
||||
, haskeline >= 0.7
|
||||
, transformers
|
||||
|
||||
ghc-prof-options: -auto-all -caf-all
|
||||
ghc-options: -threaded -rtsopts -funbox-strict-fields
|
||||
|
||||
|
@ -38,10 +38,7 @@ import Paths_idris
|
||||
-- on with the REPL.
|
||||
|
||||
main = do opts <- runArgParser
|
||||
result <- runErrorT $ execStateT (runIdris opts) idrisInit
|
||||
case result of
|
||||
Left err -> putStrLn $ "Uncaught error: " ++ show err
|
||||
Right _ -> return ()
|
||||
runMain (runIdris opts)
|
||||
|
||||
runIdris :: [Opt] -> Idris ()
|
||||
runIdris [Client c] = do setVerbose False
|
||||
|
@ -63,6 +63,14 @@ import Util.Pretty(pretty, text)
|
||||
recinfo :: ElabInfo
|
||||
recinfo = EInfo [] emptyContext id Nothing elabDecl'
|
||||
|
||||
-- | Return the elaborated term which calls 'main'
|
||||
elabMain :: Idris Term
|
||||
elabMain = do (m, _) <- elabVal recinfo ERHS
|
||||
(PApp fc (PRef fc (sUN "run__IO"))
|
||||
[pexp $ PRef fc (sNS (sUN "main") ["Main"])])
|
||||
return m
|
||||
where fc = fileFC "toplevel"
|
||||
|
||||
-- | Elaborate primitives
|
||||
elabPrims :: Idris ()
|
||||
elabPrims = do mapM_ (elabDecl' EAll recinfo)
|
||||
|
@ -1472,6 +1472,12 @@ idrisMain opts =
|
||||
addImportDir (ddir </> p)
|
||||
addIBC (IBCImportDir (ddir </> p))
|
||||
|
||||
runMain :: Idris () -> IO ()
|
||||
runMain prog = do res <- runErrorT $ execStateT prog idrisInit
|
||||
case res of
|
||||
Left err -> putStrLn $ "Uncaught error: " ++ show err
|
||||
Right _ -> return ()
|
||||
|
||||
execScript :: String -> Idris ()
|
||||
execScript expr = do i <- getIState
|
||||
c <- colourise
|
||||
|
Loading…
Reference in New Issue
Block a user