be157aa · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #2604 from melted/clean_compile

Remove the --yes-really flag from codegens

commitbe157aabd75a8389b076adde636923bfbb1e9aff authorNiklas Larsson <metaniklas@gmail.com> dateFri 11 Sep 2015, 19:09 (11 years ago) parentfa6a50a b19d03c

4 files changed+17−117

compare with master

unifiedsplit

codegen/idris-codegen-c/Main.hs+4−11 codegen/idris-codegen-javascript/Main.hs+5−11 codegen/idris-codegen-node/Main.hs+4−11 src/IRTS/Compiler.hs+4−84

codegen/idris-codegen-c/Main.hs+4−11

@@ -16,21 +16,18 @@ import Paths_idris

1616

1717import Util.System

1818

19−data Opts = Opts { really :: Bool,

20− inputs :: [FilePath],

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

2120 interface :: Bool,

2221 output :: FilePath }

2322

2423showUsage = 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>]"

24+ putStrLn "Usage: idris-codegen-c <ibc-files> [-o <output-file>]"

2725 exitWith ExitSuccess

2826

2927getOpts :: IO Opts

3028getOpts = do xs <- getArgs

31− return $ process (Opts False [] False "a.out") xs

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

3230 where

33− process opts ("--yes-really":xs) = process (opts { really = True }) xs

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

3532 process opts ("--interface":xs) = process (opts { interface = True }) xs

3633 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs

@@ -50,8 +47,4 @@ main :: IO ()

5047main = do opts <- getOpts

5148 if (null (inputs opts))

5249 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)

50+ else runMain (c_main opts)

codegen/idris-codegen-javascript/Main.hs+5−11

@@ -13,21 +13,19 @@ import System.Exit

1313

1414import Paths_idris

1515

16−data Opts = Opts { really :: Bool

17− , inputs :: [FilePath]

16+data Opts = Opts {

17+ inputs :: [FilePath]

1818 , output :: FilePath

1919 }

2020

2121showUsage = 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>]"

22+ putStrLn "Usage: idris-codegen-javascript <ibc-files> [-o <output-file>]"

2423 exitWith ExitSuccess

2524

2625getOpts :: IO Opts

2726getOpts = do xs <- getArgs

28− return $ process (Opts False [] "main.js") xs

27+ return $ process (Opts [] "main.js") xs

2928 where

30− process opts ("--yes-really":xs) = process (opts { really = True }) xs

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

3230 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs

3331 process opts [] = opts

@@ -43,8 +41,4 @@ main :: IO ()

4341main = do opts <- getOpts

4442 if (null (inputs opts))

4543 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)

44+ else runMain (jsMain opts)

codegen/idris-codegen-node/Main.hs+4−11

@@ -13,21 +13,18 @@ import System.Exit

1313

1414import Paths_idris

1515

16−data Opts = Opts { really :: Bool

17− , inputs :: [FilePath]

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

1817 , output :: FilePath

1918 }

2019

2120showUsage = 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>]"

21+ putStrLn "Usage: idris-codegen-node <ibc-files> [-o <output-file>]"

2422 exitWith ExitSuccess

2523

2624getOpts :: IO Opts

2725getOpts = do xs <- getArgs

28− return $ process (Opts False [] "main.js") xs

26+ return $ process (Opts [] "main.js") xs

2927 where

30− process opts ("--yes-really":xs) = process (opts { really = True }) xs

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

3229 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs

3330 process opts [] = opts

@@ -43,8 +40,4 @@ main :: IO ()

4340main = do opts <- getOpts

4441 if (null (inputs opts))

4542 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)

43+ else runMain (jsMain opts)

src/IRTS/Compiler.hs+4−84

@@ -44,8 +44,7 @@ import System.Directory

4444import System.Environment

4545import System.FilePath ((</>), addTrailingPathSeparator)

4646

47−-- | Given a 'main' term to compiler, return the IRs which can be used to

48−-- generate code.

47+-- | Compile to simplified forms and return CodegenInfo

4948compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo

5049compile codegen f mtm

5150 = do checkMVs -- check for undefined metavariables

@@ -74,7 +73,7 @@ compile codegen f mtm

7473 Just _ -> False

7574

7675 let defs = defsIn ++ maindef

77− -- iputStrLn $ showSep "\n" (map show defs)

76+

7877 -- Inlined top level LDecl made here

7978 let defsInlined = inlineAll defs

8079 let defsUniq = map (allocUnique (addAlist defsInlined emptyContext))

@@ -90,7 +89,7 @@ compile codegen f mtm

9089 let defuns = inline defuns_in

9190 logLvl 5 $ show defuns

9291 logLvl 1 "Resolving variables for CG"

93− -- iputStrLn $ showSep "\n" (map show (toAlist defuns))

92+

9493 let checked = simplifyDefs defuns (toAlist defuns)

9594 outty <- outputTy

9695 dumpCases <- getDumpCases

@@ -109,13 +108,6 @@ compile codegen f mtm

109108 hdrs impdirs objs libs flags

110109 NONE c (toAlist defuns)

111110 tagged iface exports

112−-- runIO $ case codegen of

113−-- ViaC -> codegenC cginfo

114−-- ViaJava -> codegenJava cginfo

115−-- ViaJavaScript -> codegenJavaScript cginfo

116−-- ViaNode -> codegenNode cginfo

117−-- ViaLLVM -> codegenLLVM cginfo

118−-- Bytecode -> dumpBC c f

119111 Error e -> ierror e

120112 where checkMVs = do i <- getIState

121113 case map fst (idris_metavars i) \\ primDefs of

@@ -125,9 +117,6 @@ compile codegen f mtm

125117 case idris_totcheckfail i of

126118 [] -> return ()

127119 ((fc, msg):fs) -> ierror . At fc . Msg $ "Cannot compile:\n " ++ msg

128− inDir d h = do let f = d </> h

129− ex <- doesFileExist f

130− if ex then return f else return h

131120

132121generate :: Codegen -> FilePath -> CodegenInfo -> IO ()

133122generate codegen mainmod ir

@@ -136,7 +125,7 @@ generate codegen mainmod ir

136125 Via "c" -> codegenC ir

137126 -- Any external code generator

138127 Via cg -> do let cmd = "idris-codegen-" ++ cg

139− args = ["--yes-really", mainmod, "-o", outputFile ir] ++ compilerFlags ir

128+ args = [mainmod, "-o", outputFile ir] ++ compilerFlags ir

140129 exit <- rawSystem cmd args

141130 when (exit /= ExitSuccess) $

142131 putStrLn ("FAILURE: " ++ show cmd ++ " " ++ show args)

@@ -485,75 +474,6 @@ doForeign vs env (ret : fname : world : args)

485474 deNS n = n

486475doForeign vs env xs = ifail "Badly formed foreign function call"

487476

488−{-

489− - | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn

490− = case getFTypes fgnArgTys of

491− Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)

492− Just tys -> do

493− args' <- mapM (irTerm vs env) (init args)

494− return $ LForeign LANG_C (mkIty' ret) fgnName (zip tys args')

495−

496− | otherwise = ifail "Badly formed foreign function call"

497− where

498− getFTypes :: TT Name -> Maybe [FType]

499− getFTypes tm = case unApply tm of

500− -- nil : {a : Type} -> List a

501− (nil, [_]) -> Just []

502− -- cons : {a : Type} -> a -> List a -> List a

503− (cons, [_, ty, xs]) -> (mkIty' ty :) <$> getFTypes xs

504− _ -> Nothing

505−

506− mkIty' (P _ (UN ty) _) = mkIty (str ty)

507− mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))

508− | fi == txt "FIntT"

509− = mkIntIty (str intTy)

510−

511− mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))

512− | ff == txt "FFunction"

513− , fa == txt "FAny"

514− , io == txt "IO"

515− = FFunctionIO

516−

517− mkIty' (App (App (P _ (UN ff) _) _) _)

518− | ff == txt "FFunction"

519− = FFunction

520−

521− mkIty' _ = FAny

522−

523− -- would be better if these FInt types were evaluated at compile time

524− -- TODO: add %eval directive for such things

525− -- Issue #1742 on the issue tracker.

526− -- https://github.com/idris-lang/Idris-dev/issues/1742

527− mkIty "FFloat" = FArith ATFloat

528− mkIty "FInt" = mkIntIty "ITNative"

529− mkIty "FChar" = mkIntIty "ITChar"

530− mkIty "FByte" = mkIntIty "IT8"

531− mkIty "FShort" = mkIntIty "IT16"

532− mkIty "FLong" = mkIntIty "IT64"

533− mkIty "FBits8" = mkIntIty "IT8"

534− mkIty "FBits16" = mkIntIty "IT16"

535− mkIty "FBits32" = mkIntIty "IT32"

536− mkIty "FBits64" = mkIntIty "IT64"

537− mkIty "FString" = FString

538− mkIty "FPtr" = FPtr

539− mkIty "FManagedPtr" = FManagedPtr

540− mkIty "FUnit" = FUnit

541− mkIty "FFunction" = FFunction

542− mkIty "FFunctionIO" = FFunctionIO

543− mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))

544− mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))

545− mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))

546− mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))

547− mkIty x = error $ "Unknown type " ++ x

548−

549− mkIntIty "ITNative" = FArith (ATInt ITNative)

550− mkIntIty "ITChar" = FArith (ATInt ITChar)

551− mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))

552− mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))

553− mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))

554− mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))

555−-}

556−

557477irTree :: [Name] -> SC -> Idris LExp

558478irTree args tree = do

559479 logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree