git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2604 from melted/clean_compile
be157aaNiklas Larsson
codegen/idris-codegen-c/Main.hs+4−11
compare with master
unifiedsplit
@@ -16,21 +16,18 @@ import Paths_idris
16
16
17import Util.System
17import Util.System
18
18
19−data Opts = Opts { really :: Bool,
20− inputs :: [FilePath],
19+data Opts = Opts { inputs :: [FilePath],
21 interface :: Bool,
20 interface :: Bool,
22 output :: FilePath }
21 output :: FilePath }
23
22
24showUsage = do putStrLn "A code generator which is intended to be called by the compiler, not by a user."
23showUsage = 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>]"
27 exitWith ExitSuccess
25 exitWith ExitSuccess
28
26
29getOpts :: IO Opts
27getOpts :: IO Opts
30getOpts = do xs <- getArgs
28getOpts = do xs <- getArgs
31− return $ process (Opts False [] False "a.out") xs
29+ return $ process (Opts [] False "a.out") xs
32 where
30 where
33− process opts ("--yes-really":xs) = process (opts { really = True }) xs
34 process opts ("-o":o:xs) = process (opts { output = o }) xs
31 process opts ("-o":o:xs) = process (opts { output = o }) xs
35 process opts ("--interface":xs) = process (opts { interface = True }) xs
32 process opts ("--interface":xs) = process (opts { interface = True }) xs
36 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs
33 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs
@@ -50,8 +47,4 @@ main :: IO ()
50main = do opts <- getOpts
47main = do opts <- getOpts
51 if (null (inputs opts))
48 if (null (inputs opts))
52 then showUsage
49 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
13
13
14import Paths_idris
14import Paths_idris
15
15
16−data Opts = Opts { really :: Bool
16+data Opts = Opts {
17− , inputs :: [FilePath]
17+ inputs :: [FilePath]
18 , output :: FilePath
18 , output :: FilePath
19 }
19 }
20
20
21showUsage = do putStrLn "A code generator which is intended to be called by the compiler, not by a user."
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>]"
22+ putStrLn "Usage: idris-codegen-javascript <ibc-files> [-o <output-file>]"
24 exitWith ExitSuccess
23 exitWith ExitSuccess
25
24
26getOpts :: IO Opts
25getOpts :: IO Opts
27getOpts = do xs <- getArgs
26getOpts = do xs <- getArgs
28− return $ process (Opts False [] "main.js") xs
27+ return $ process (Opts [] "main.js") xs
29 where
28 where
30− process opts ("--yes-really":xs) = process (opts { really = True }) xs
31 process opts ("-o":o:xs) = process (opts { output = o }) xs
29 process opts ("-o":o:xs) = process (opts { output = o }) xs
32 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs
30 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs
33 process opts [] = opts
31 process opts [] = opts
@@ -43,8 +41,4 @@ main :: IO ()
43main = do opts <- getOpts
41main = do opts <- getOpts
44 if (null (inputs opts))
42 if (null (inputs opts))
45 then showUsage
43 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
13
13
14import Paths_idris
14import Paths_idris
15
15
16−data Opts = Opts { really :: Bool
17− , inputs :: [FilePath]
16+data Opts = Opts { inputs :: [FilePath]
18 , output :: FilePath
17 , output :: FilePath
19 }
18 }
20
19
21showUsage = do putStrLn "A code generator which is intended to be called by the compiler, not by a user."
20showUsage = 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>]"
24 exitWith ExitSuccess
22 exitWith ExitSuccess
25
23
26getOpts :: IO Opts
24getOpts :: IO Opts
27getOpts = do xs <- getArgs
25getOpts = do xs <- getArgs
28− return $ process (Opts False [] "main.js") xs
26+ return $ process (Opts [] "main.js") xs
29 where
27 where
30− process opts ("--yes-really":xs) = process (opts { really = True }) xs
31 process opts ("-o":o:xs) = process (opts { output = o }) xs
28 process opts ("-o":o:xs) = process (opts { output = o }) xs
32 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs
29 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs
33 process opts [] = opts
30 process opts [] = opts
@@ -43,8 +40,4 @@ main :: IO ()
43main = do opts <- getOpts
40main = do opts <- getOpts
44 if (null (inputs opts))
41 if (null (inputs opts))
45 then showUsage
42 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
44import System.Environment
44import System.Environment
45import System.FilePath ((</>), addTrailingPathSeparator)
45import System.FilePath ((</>), addTrailingPathSeparator)
46
46
47−-- | Given a 'main' term to compiler, return the IRs which can be used to
47+-- | Compile to simplified forms and return CodegenInfo
48−-- generate code.
49compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo
48compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo
50compile codegen f mtm
49compile codegen f mtm
51 = do checkMVs -- check for undefined metavariables
50 = do checkMVs -- check for undefined metavariables
@@ -74,7 +73,7 @@ compile codegen f mtm
74 Just _ -> False
73 Just _ -> False
75
74
76 let defs = defsIn ++ maindef
75 let defs = defsIn ++ maindef
77− -- iputStrLn $ showSep "\n" (map show defs)
76+
78 -- Inlined top level LDecl made here
77 -- Inlined top level LDecl made here
79 let defsInlined = inlineAll defs
78 let defsInlined = inlineAll defs
80 let defsUniq = map (allocUnique (addAlist defsInlined emptyContext))
79 let defsUniq = map (allocUnique (addAlist defsInlined emptyContext))
@@ -90,7 +89,7 @@ compile codegen f mtm
90 let defuns = inline defuns_in
89 let defuns = inline defuns_in
91 logLvl 5 $ show defuns
90 logLvl 5 $ show defuns
92 logLvl 1 "Resolving variables for CG"
91 logLvl 1 "Resolving variables for CG"
93− -- iputStrLn $ showSep "\n" (map show (toAlist defuns))
92+
94 let checked = simplifyDefs defuns (toAlist defuns)
93 let checked = simplifyDefs defuns (toAlist defuns)
95 outty <- outputTy
94 outty <- outputTy
96 dumpCases <- getDumpCases
95 dumpCases <- getDumpCases
@@ -109,13 +108,6 @@ compile codegen f mtm
109 hdrs impdirs objs libs flags
108 hdrs impdirs objs libs flags
110 NONE c (toAlist defuns)
109 NONE c (toAlist defuns)
111 tagged iface exports
110 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
119 Error e -> ierror e
111 Error e -> ierror e
120 where checkMVs = do i <- getIState
112 where checkMVs = do i <- getIState
121 case map fst (idris_metavars i) \\ primDefs of
113 case map fst (idris_metavars i) \\ primDefs of
@@ -125,9 +117,6 @@ compile codegen f mtm
125 case idris_totcheckfail i of
117 case idris_totcheckfail i of
126 [] -> return ()
118 [] -> return ()
127 ((fc, msg):fs) -> ierror . At fc . Msg $ "Cannot compile:\n " ++ msg
119 ((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
131
120
132generate :: Codegen -> FilePath -> CodegenInfo -> IO ()
121generate :: Codegen -> FilePath -> CodegenInfo -> IO ()
133generate codegen mainmod ir
122generate codegen mainmod ir
@@ -136,7 +125,7 @@ generate codegen mainmod ir
136 Via "c" -> codegenC ir
125 Via "c" -> codegenC ir
137 -- Any external code generator
126 -- Any external code generator
138 Via cg -> do let cmd = "idris-codegen-" ++ cg
127 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
140 exit <- rawSystem cmd args
129 exit <- rawSystem cmd args
141 when (exit /= ExitSuccess) $
130 when (exit /= ExitSuccess) $
142 putStrLn ("FAILURE: " ++ show cmd ++ " " ++ show args)
131 putStrLn ("FAILURE: " ++ show cmd ++ " " ++ show args)
@@ -485,75 +474,6 @@ doForeign vs env (ret : fname : world : args)
485 deNS n = n
474 deNS n = n
486doForeign vs env xs = ifail "Badly formed foreign function call"
475doForeign vs env xs = ifail "Badly formed foreign function call"
487
476
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−
557irTree :: [Name] -> SC -> Idris LExp
477irTree :: [Name] -> SC -> Idris LExp
558irTree args tree = do
478irTree args tree = do
559 logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
479 logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree