d2a8c3e · Idris-dev · git.iko.soy

codegen/idris-codegen-c/Main.hs+1−1

compare with master

unifiedsplit

@@ -40,7 +40,7 @@ c_main opts = do runIO setupBundledCC

40 mainProg <- if interface opts

41 then liftM Just elabMain

42 else return Nothing

43− ir <- compile (Via "c") (output opts) mainProg

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

44 runIO $ codegenC ir

45

46main :: IO ()

codegen/idris-codegen-javascript/Main.hs+1−1

@@ -34,7 +34,7 @@ jsMain :: Opts -> Idris ()

34jsMain opts = do elabPrims

35 loadInputs (inputs opts) Nothing

36 mainProg <- elabMain

37− ir <- compile (Via "javascript") (output opts) (Just mainProg)

37+ ir <- compile (Via IBCFormat "javascript") (output opts) (Just mainProg)

38 runIO $ codegenJavaScript ir

39

40main :: IO ()

codegen/idris-codegen-node/Main.hs+1−1

@@ -33,7 +33,7 @@ jsMain :: Opts -> Idris ()

33jsMain opts = do elabPrims

34 loadInputs (inputs opts) Nothing

35 mainProg <- elabMain

36− ir <- compile (Via "node") (output opts) (Just mainProg)

36+ ir <- compile (Via IBCFormat "node") (output opts) (Just mainProg)

37 runIO $ codegenNode ir

38

39main :: IO ()

idris.cabal+1−1

@@ -1052,7 +1052,7 @@ Library

1052 , Tools_idris

1053

1054 Build-depends: base >=4 && <5

1055− , aeson >= 0.11 && < 0.12

1055+ , aeson >= 0.6 && < 0.12

1056 , annotated-wl-pprint >= 0.7 && < 0.8

1057 , ansi-terminal < 0.7

1058 , ansi-wl-pprint < 0.7

src/IRTS/Compiler.hs+16−16

@@ -122,25 +122,25 @@ compile codegen f mtm

122 [] -> return ()

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

124

125−generate :: Codegen -> FilePath -> Bool -> CodegenInfo -> IO ()

125+generate :: Codegen -> FilePath -> CodegenInfo -> IO ()

126−generate codegen mainmod port ir

126+generate codegen mainmod ir

127 = case codegen of

128 -- Built-in code generators (FIXME: lift these out!)

129− Via "c" -> codegenC ir

129+ Via _ "c" -> codegenC ir

130 -- Any external code generator

131− Via cg -> do input <- if port

131+ Via fm cg -> do input <- case fm of

132− then do

132+ IBCFormat -> return mainmod

133+ JSONFormat -> do

133− tempdir <- getTemporaryDirectory

134+ tempdir <- getTemporaryDirectory

134− (fn, h) <- openTempFile tempdir "idris-cg.json"

135+ (fn, h) <- openTempFile tempdir "idris-cg.json"

135− writePortable h ir

136+ writePortable h ir

136− hClose h

137+ hClose h

137− return fn

138+ return fn

138− else return mainmod

139− let cmd = "idris-codegen-" ++ cg

139+ let cmd = "idris-codegen-" ++ cg

140− args = [input, "-o", outputFile ir] ++ compilerFlags ir

140+ args = [input, "-o", outputFile ir] ++ compilerFlags ir

141− exit <- rawSystem cmd args

141+ exit <- rawSystem cmd args

142− when (exit /= ExitSuccess) $

142+ when (exit /= ExitSuccess) $

143− putStrLn ("FAILURE: " ++ show cmd ++ " " ++ show args)

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

144 Bytecode -> dumpBC (simpleDecls ir) (outputFile ir)

145

146irMain :: TT Name -> Idris LDecl

src/Idris/AbsSyntax.hs+5−11

@@ -45,7 +45,11 @@ getContext :: Idris Context

45getContext = do i <- getIState; return (tt_ctxt i)

46

47forCodegen :: Codegen -> [(Codegen, a)] -> [a]

48−forCodegen tgt xs = [x | (tgt', x) <- xs, tgt == tgt']

48+forCodegen tgt xs = [x | (tgt', x) <- xs, eqLang tgt tgt']

49+ where

50+ eqLang (Via _ x) (Via _ y) = x == y

51+ eqLang Bytecode Bytecode = True

52+ eqLang _ _ = False

49

53

50getObjectFiles :: Codegen -> Idris [FilePath]

54getObjectFiles :: Codegen -> Idris [FilePath]

51getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)

55getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)

@@ -946,16 +950,6 @@ codegen :: Idris Codegen

946codegen = do i <- getIState

950codegen = do i <- getIState

947 return (opt_codegen (idris_options i))

951 return (opt_codegen (idris_options i))

948

952

949−setPortableCodegen :: Bool -> Idris ()

950−setPortableCodegen p = do i <- getIState

951− let opts = idris_options i

952− let opt' = opts { opt_portableCG = p }

953− putIState $ i { idris_options = opt' }

954−

955−getPortableCodegen :: Idris Bool

956−getPortableCodegen = do i <- getIState

957− let opts = idris_options i

958− return (opt_portableCG opts)

959

953

960setOutputTy :: OutputType -> Idris ()

954setOutputTy :: OutputType -> Idris ()

961setOutputTy t = do i <- getIState

955setOutputTy t = do i <- getIState

src/Idris/AbsSyntaxTree.hs+4−10

@@ -85,7 +85,6 @@ data IOption = IOption {

85 , opt_nobanner :: Bool

86 , opt_quiet :: Bool

87 , opt_codegen :: Codegen

88− , opt_portableCG :: Bool

89 , opt_outputTy :: OutputType

88 , opt_outputTy :: OutputType

90 , opt_ibcsubdir :: FilePath

89 , opt_ibcsubdir :: FilePath

91 , opt_importdirs :: [FilePath]

90 , opt_importdirs :: [FilePath]

@@ -113,8 +112,7 @@ defaultOpts = IOption { opt_logLevel = 0

113 , opt_verbose = True

112 , opt_verbose = True

114 , opt_nobanner = False

113 , opt_nobanner = False

115 , opt_quiet = False

114 , opt_quiet = False

116− , opt_codegen = Via "c"

115+ , opt_codegen = Via IBCFormat "c"

117− , opt_portableCG = False

118 , opt_outputTy = Executable

116 , opt_outputTy = Executable

119 , opt_ibcsubdir = ""

117 , opt_ibcsubdir = ""

120 , opt_importdirs = []

118 , opt_importdirs = []

@@ -388,18 +386,15 @@ throwError = Trans.lift . throwE

388

386

389-- Commands in the REPL

387-- Commands in the REPL

390

388

391−data Codegen = Via String

389+data Codegen = Via IRFormat String

392−-- | ViaC

393−-- | ViaJava

394−-- | ViaNode

395−-- | ViaJavaScript

396−-- | ViaLLVM

397 | Bytecode

390 | Bytecode

398 deriving (Show, Eq)

391 deriving (Show, Eq)

399{-!

392{-!

400deriving instance NFData Codegen

393deriving instance NFData Codegen

401!-}

394!-}

402

395

396+data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq)

397+

403data HowMuchDocs = FullDocs | OverviewDocs

398data HowMuchDocs = FullDocs | OverviewDocs

404

399

405-- | REPL commands

400-- | REPL commands

@@ -560,7 +555,6 @@ data Opt = Filename String

560 | DumpDefun String

555 | DumpDefun String

561 | DumpCases String

556 | DumpCases String

562 | UseCodegen Codegen

557 | UseCodegen Codegen

563− | PortableCodegen

564 | CodegenArgs String

558 | CodegenArgs String

565 | OutputTy OutputType

559 | OutputTy OutputType

566 | Extension LanguageExt

560 | Extension LanguageExt

src/Idris/CmdOptions.hs+8−2

@@ -149,7 +149,12 @@ parseFlags = many $

149 <|> ((\s -> UseCodegen $ parseCodegen s) <$> strOption (long "codegen"

150 <> metavar "TARGET"

151 <> help "Select code generator: C, Javascript, Node and bytecode are bundled with Idris"))

152− <|> flag' PortableCodegen (long "portable" <> help "Call codegen with json-formatted codegen info")

152+

153+

154+ <|> ((\s -> UseCodegen $ Via JSONFormat s) <$> strOption (long "portable-codegen"

155+ <> metavar "TARGET"

156+ <> help "Pass the name of the code generator. This option is for codegens that take JSON formatted IR."))

157+

153 <|> (CodegenArgs <$> strOption (long "cg-opt"

158 <|> (CodegenArgs <$> strOption (long "cg-opt"

154 <> metavar "ARG"

159 <> metavar "ARG"

155 <> help "Arguments to pass to code generator"))

160 <> help "Arguments to pass to code generator"))

@@ -207,7 +212,8 @@ preProcOpts (x:xs) ys = preProcOpts xs (x:ys)

207

212

208parseCodegen :: String -> Codegen

213parseCodegen :: String -> Codegen

209parseCodegen "bytecode" = Bytecode

214parseCodegen "bytecode" = Bytecode

210−parseCodegen cg = Via (map toLower cg)

215+parseCodegen cg = Via IBCFormat (map toLower cg)

216+

211

217

212parseLogCats :: Monad m => String -> m [LogCat]

218parseLogCats :: Monad m => String -> m [LogCat]

213parseLogCats s =

219parseLogCats s =

src/Idris/DeepSeq.hs+4−3

@@ -149,7 +149,6 @@ instance NFData Opt where

149 rnf (DumpDefun str) = rnf str `seq` ()

150 rnf (DumpCases str) = rnf str `seq` ()

151 rnf (UseCodegen cg) = rnf cg `seq` ()

152− rnf (PortableCodegen) = ()

153 rnf (CodegenArgs str) = rnf str `seq` ()

152 rnf (CodegenArgs str) = rnf str `seq` ()

154 rnf (OutputTy ot) = rnf ot `seq` ()

153 rnf (OutputTy ot) = rnf ot `seq` ()

155 rnf (Extension le) = rnf le `seq` ()

154 rnf (Extension le) = rnf le `seq` ()

@@ -188,7 +187,6 @@ instance NFData IOption where

188 opt_nobanner

187 opt_nobanner

189 opt_quiet

188 opt_quiet

190 opt_codegen

189 opt_codegen

191− opt_portableCG

192 opt_outputTy

190 opt_outputTy

193 opt_ibcsubdir

191 opt_ibcsubdir

194 opt_importdirs

192 opt_importdirs

@@ -363,9 +361,12 @@ instance NFData FnInfo where

363 rnf (FnInfo x1) = rnf x1 `seq` ()

361 rnf (FnInfo x1) = rnf x1 `seq` ()

364

362

365instance NFData Codegen where

363instance NFData Codegen where

366− rnf (Via x1) = rnf x1 `seq` ()

364+ rnf (Via x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

367 rnf Bytecode = ()

365 rnf Bytecode = ()

368

366

367+instance NFData IRFormat where

368+ rnf _ = ()

369+

369instance NFData LogCat where

370instance NFData LogCat where

370 rnf _ = ()

371 rnf _ = ()

371

372

src/Idris/IBC.hs+16−4

@@ -40,7 +40,7 @@ import System.Directory

40import Codec.Archive.Zip

41

42ibcVersion :: Word16

43−ibcVersion = 142

43+ibcVersion = 143

44

45-- When IBC is being loaded - we'll load different things (and omit different

46-- structures/definitions) depending on which phase we're in

@@ -2461,13 +2461,25 @@ instance Binary SSymbol where

2461instance Binary Codegen where

2462 put x

2463 = case x of

2464− Via str -> do putWord8 0

2464+ Via ir str -> do putWord8 0

2465+ put ir

2465− put str

2466+ put str

2466 Bytecode -> putWord8 1

2467 Bytecode -> putWord8 1

2467 get

2468 get

2468 = do i <- getWord8

2469 = do i <- getWord8

2469 case i of

2470 case i of

2470 0 -> do x1 <- get

2471 0 -> do x1 <- get

2472+ x2 <- get

2471− return (Via x1)

2473+ return (Via x1 x2)

2472 1 -> return Bytecode

2474 1 -> return Bytecode

2473 _ -> error "Corrupted binary data for Codegen"

2475 _ -> error "Corrupted binary data for Codegen"

2476+

2477+instance Binary IRFormat where

2478+ put x = case x of

2479+ IBCFormat -> putWord8 0

2480+ JSONFormat -> putWord8 1

2481+ get = do i <- getWord8

2482+ case i of

2483+ 0 -> return IBCFormat

2484+ 1 -> return JSONFormat

2485+ _ -> error "Corrupted binary data for IRFormat"

src/Idris/Parser.hs+6−6

@@ -781,7 +781,7 @@ params syn =

781 return [PParams fc ns' (concat ds)]

782 <?> "parameters declaration"

783

784−{- | Parses an open block

784+{- | Parses an open block

785

786-}

787

@@ -790,7 +790,7 @@ openInterface syn =

790 do reservedHL "using"

791 reservedHL "implementation"

792 fc <- getFC

793− ns <- sepBy1 fnName (lchar ',')

793+ ns <- sepBy1 fnName (lchar ',')

794

795 openBlock

796 ds <- many (decl syn)

@@ -799,7 +799,7 @@ openInterface syn =

799 <?> "open interface declaration"

800

801

802−

802+

803

804{- | Parses a mutual declaration (for mutually recursive functions)

805

@@ -877,7 +877,7 @@ classBlock syn = do reservedHL "where"

877 ist <- get

878 let cd' = annotate syn ist cd

879

880− ds <- many (notEndBlock >> try (instance_ True syn)

880+ ds <- many (notEndBlock >> try (instance_ True syn)

881 <|> do x <- data_ syn

882 return [x]

883 <|> fnDecl syn)

@@ -1324,7 +1324,7 @@ Codegen ::= 'C'

1324-}

1325codegen_ :: IdrisParser Codegen

1326codegen_ = do n <- fst <$> identifier

1327− return (Via (map toLower n))

1327+ return (Via IBCFormat (map toLower n))

1328 <|> do reserved "Bytecode"; return Bytecode

1329 <?> "code generation language"

1330

@@ -1812,7 +1812,7 @@ loadSource lidr f toline

1812 logLvl 2 $ "Totality checking " ++ show deftots

1813 mapM_ (\x -> do tot <- getTotality x

1814 case tot of

1815− Total _ ->

1815+ Total _ ->

1816 do let opts = case lookupCtxtExact x (idris_flags i) of

1817 Just os -> os

1818 Nothing -> []

src/Idris/REPL.hs+3−7

@@ -1228,8 +1228,7 @@ process fn (Execute tm)

1228 -- gcc adds .exe when it builds windows programs

1229 progName <- return $ if isWindows then tmpn ++ ".exe" else tmpn

1230 ir <- compile t tmpn (Just m)

1231− port <- getPortableCodegen

1232− runIO $ generate t (fst (head (idris_imported ist))) port ir

1231+ runIO $ generate t (fst (head (idris_imported ist))) ir

1233 case idris_outputmode ist of

1232 case idris_outputmode ist of

1234 RawOutput h -> do runIO $ rawSystem progName []

1233 RawOutput h -> do runIO $ rawSystem progName []

1235 return ()

1234 return ()

@@ -1250,9 +1249,8 @@ process fn (Compile codegen f)

1250 [pexp $ PRef fc [] mainname])

1249 [pexp $ PRef fc [] mainname])

1251 return (Just m')

1250 return (Just m')

1252 ir <- compile codegen f m

1251 ir <- compile codegen f m

1253− port <- getPortableCodegen

1254 i <- getIState

1252 i <- getIState

1255− runIO $ generate codegen (fst (head (idris_imported i))) port ir

1253+ runIO $ generate codegen (fst (head (idris_imported i))) ir

1256 where fc = fileFC "main"

1254 where fc = fileFC "main"

1257process fn (LogLvl i) = setLogLevel i

1255process fn (LogLvl i) = setLogLevel i

1258process fn (LogCategory cs) = setLogCats cs

1256process fn (LogCategory cs) = setLogCats cs

@@ -1689,9 +1687,8 @@ idrisMain opts =

1689 Object else Executable

1687 Object else Executable

1690 xs -> last xs

1688 xs -> last xs

1691 let cgn = case opt getCodegen opts of

1689 let cgn = case opt getCodegen opts of

1692− [] -> Via "c"

1690+ [] -> Via IBCFormat "c"

1693 xs -> last xs

1691 xs -> last xs

1694− let portable = PortableCodegen `elem` opts

1695 let cgFlags = opt getCodegenArgs opts

1692 let cgFlags = opt getCodegenArgs opts

1696

1693

1697 -- Now set/unset specifically chosen optimisations

1694 -- Now set/unset specifically chosen optimisations

@@ -1719,7 +1716,6 @@ idrisMain opts =

1719 setOutputTy outty

1716 setOutputTy outty

1720 setNoBanner nobanner

1717 setNoBanner nobanner

1721 setCodegen cgn

1718 setCodegen cgn

1722− setPortableCodegen portable

1723 mapM_ (addFlag cgn) cgFlags

1719 mapM_ (addFlag cgn) cgFlags

1724 mapM_ makeOption opts

1720 mapM_ makeOption opts

1725 -- if we have the --bytecode flag, drop into the bytecode assembler

1721 -- if we have the --bytecode flag, drop into the bytecode assembler

src/Idris/REPL/Parser.hs+2−2

@@ -358,13 +358,13 @@ cmd_pprint name = do

358

359cmd_compile :: String -> P.IdrisParser (Either String Command)

360cmd_compile name = do

361− let defaultCodegen = Via "c"

361+ let defaultCodegen = Via IBCFormat "c"

362

363 let codegenOption :: P.IdrisParser Codegen

364 codegenOption = do

365 let bytecodeCodegen = discard (P.symbol "bytecode") *> return Bytecode

366 viaCodegen = do x <- fst <$> P.identifier

367− return (Via (map toLower x))

367+ return (Via IBCFormat (map toLower x))

368 bytecodeCodegen <|> viaCodegen

369

370 let hasOneArg = do