d2a8c3e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fold portable into Codegen

commitd2a8c3e3c78323d779fa89bedb8e698a502d084a authorNiklas Larsson <niklas@mm.st> dateMon 16 May 2016, 19:21 (10 years ago) parent80225af

13 files changed+68−65

compare with master

unifiedsplit

codegen/idris-codegen-c/Main.hs+1−1 codegen/idris-codegen-javascript/Main.hs+1−1 codegen/idris-codegen-node/Main.hs+1−1 idris.cabal+1−1 src/IRTS/Compiler.hs+16−16 src/Idris/AbsSyntax.hs+5−11 src/Idris/AbsSyntaxTree.hs+4−10 src/Idris/CmdOptions.hs+8−2 src/Idris/DeepSeq.hs+4−3 src/Idris/IBC.hs+16−4 src/Idris/Parser.hs+6−6 src/Idris/REPL.hs+3−7 src/Idris/REPL/Parser.hs+2−2

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

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

4040 mainProg <- if interface opts

4141 then liftM Just elabMain

4242 else return Nothing

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

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

4444 runIO $ codegenC ir

4545

4646main :: IO ()

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

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

3434jsMain opts = do elabPrims

3535 loadInputs (inputs opts) Nothing

3636 mainProg <- elabMain

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

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

3838 runIO $ codegenJavaScript ir

3939

4040main :: IO ()

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

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

3333jsMain opts = do elabPrims

3434 loadInputs (inputs opts) Nothing

3535 mainProg <- elabMain

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

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

3737 runIO $ codegenNode ir

3838

3939main :: IO ()

idris.cabal+1−1

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

10521052 , Tools_idris

10531053

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

1055− , aeson >= 0.11 && < 0.12

1055+ , aeson >= 0.6 && < 0.12

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

10571057 , ansi-terminal < 0.7

10581058 , ansi-wl-pprint < 0.7

src/IRTS/Compiler.hs+16−16

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

122122 [] -> return ()

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

124124

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

126−generate codegen mainmod port ir

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

126+generate codegen mainmod ir

127127 = case codegen of

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

129− Via "c" -> codegenC ir

129+ Via _ "c" -> codegenC ir

130130 -- Any external code generator

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

132− then do

133− tempdir <- getTemporaryDirectory

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

135− writePortable h ir

136− hClose h

137− return fn

138− else return mainmod

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

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

141− exit <- rawSystem cmd args

142− when (exit /= ExitSuccess) $

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

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

132+ IBCFormat -> return mainmod

133+ JSONFormat -> do

134+ tempdir <- getTemporaryDirectory

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

136+ writePortable h ir

137+ hClose h

138+ return fn

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

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

141+ exit <- rawSystem cmd args

142+ when (exit /= ExitSuccess) $

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

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

145145

146146irMain :: TT Name -> Idris LDecl

src/Idris/AbsSyntax.hs+5−11

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

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

4646

4747forCodegen :: 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

4953

5054getObjectFiles :: Codegen -> Idris [FilePath]

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

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

946950codegen = do i <- getIState

947951 return (opt_codegen (idris_options i))

948952

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)

959953

960954setOutputTy :: OutputType -> Idris ()

961955setOutputTy t = do i <- getIState

src/Idris/AbsSyntaxTree.hs+4−10

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

8585 , opt_nobanner :: Bool

8686 , opt_quiet :: Bool

8787 , opt_codegen :: Codegen

88− , opt_portableCG :: Bool

8988 , opt_outputTy :: OutputType

9089 , opt_ibcsubdir :: FilePath

9190 , opt_importdirs :: [FilePath]

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

113112 , opt_verbose = True

114113 , opt_nobanner = False

115114 , opt_quiet = False

116− , opt_codegen = Via "c"

117− , opt_portableCG = False

115+ , opt_codegen = Via IBCFormat "c"

118116 , opt_outputTy = Executable

119117 , opt_ibcsubdir = ""

120118 , opt_importdirs = []

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

388386

389387-- Commands in the REPL

390388

391−data Codegen = Via String

392−-- | ViaC

393−-- | ViaJava

394−-- | ViaNode

395−-- | ViaJavaScript

396−-- | ViaLLVM

389+data Codegen = Via IRFormat String

397390 | Bytecode

398391 deriving (Show, Eq)

399392{-!

400393deriving instance NFData Codegen

401394!-}

402395

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

397+

403398data HowMuchDocs = FullDocs | OverviewDocs

404399

405400-- | REPL commands

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

560555 | DumpDefun String

561556 | DumpCases String

562557 | UseCodegen Codegen

563− | PortableCodegen

564558 | CodegenArgs String

565559 | OutputTy OutputType

566560 | Extension LanguageExt

src/Idris/CmdOptions.hs+8−2

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

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

150150 <> metavar "TARGET"

151151 <> 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+

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

154159 <> metavar "ARG"

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

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

207212

208213parseCodegen :: String -> Codegen

209214parseCodegen "bytecode" = Bytecode

210−parseCodegen cg = Via (map toLower cg)

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

216+

211217

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

213219parseLogCats s =

src/Idris/DeepSeq.hs+4−3

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

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

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

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

152− rnf (PortableCodegen) = ()

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

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

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

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

188187 opt_nobanner

189188 opt_quiet

190189 opt_codegen

191− opt_portableCG

192190 opt_outputTy

193191 opt_ibcsubdir

194192 opt_importdirs

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

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

364362

365363instance NFData Codegen where

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

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

367365 rnf Bytecode = ()

368366

367+instance NFData IRFormat where

368+ rnf _ = ()

369+

369370instance NFData LogCat where

370371 rnf _ = ()

371372

src/Idris/IBC.hs+16−4

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

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 142

43+ibcVersion = 143

4444

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

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

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

24612461instance Binary Codegen where

24622462 put x

24632463 = case x of

2464− Via str -> do putWord8 0

2465− put str

2464+ Via ir str -> do putWord8 0

2465+ put ir

2466+ put str

24662467 Bytecode -> putWord8 1

24672468 get

24682469 = do i <- getWord8

24692470 case i of

24702471 0 -> do x1 <- get

2471− return (Via x1)

2472+ x2 <- get

2473+ return (Via x1 x2)

24722474 1 -> return Bytecode

24732475 _ -> 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 =

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

782782 <?> "parameters declaration"

783783

784−{- | Parses an open block

784+{- | Parses an open block

785785

786786-}

787787

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

790790 do reservedHL "using"

791791 reservedHL "implementation"

792792 fc <- getFC

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

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

794794

795795 openBlock

796796 ds <- many (decl syn)

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

799799 <?> "open interface declaration"

800800

801801

802−

802+

803803

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

805805

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

877877 ist <- get

878878 let cd' = annotate syn ist cd

879879

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

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

881881 <|> do x <- data_ syn

882882 return [x]

883883 <|> fnDecl syn)

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

13241324-}

13251325codegen_ :: IdrisParser Codegen

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

1327− return (Via (map toLower n))

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

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

13291329 <?> "code generation language"

13301330

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

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

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

18141814 case tot of

1815− Total _ ->

1815+ Total _ ->

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

18171817 Just os -> os

18181818 Nothing -> []

src/Idris/REPL.hs+3−7

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

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

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

12301230 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

12331232 case idris_outputmode ist of

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

12351234 return ()

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

12501249 [pexp $ PRef fc [] mainname])

12511250 return (Just m')

12521251 ir <- compile codegen f m

1253− port <- getPortableCodegen

12541252 i <- getIState

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

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

12561254 where fc = fileFC "main"

12571255process fn (LogLvl i) = setLogLevel i

12581256process fn (LogCategory cs) = setLogCats cs

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

16891687 Object else Executable

16901688 xs -> last xs

16911689 let cgn = case opt getCodegen opts of

1692− [] -> Via "c"

1690+ [] -> Via IBCFormat "c"

16931691 xs -> last xs

1694− let portable = PortableCodegen `elem` opts

16951692 let cgFlags = opt getCodegenArgs opts

16961693

16971694 -- Now set/unset specifically chosen optimisations

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

17191716 setOutputTy outty

17201717 setNoBanner nobanner

17211718 setCodegen cgn

1722− setPortableCodegen portable

17231719 mapM_ (addFlag cgn) cgFlags

17241720 mapM_ makeOption opts

17251721 -- 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

358358

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

360360cmd_compile name = do

361− let defaultCodegen = Via "c"

361+ let defaultCodegen = Via IBCFormat "c"

362362

363363 let codegenOption :: P.IdrisParser Codegen

364364 codegenOption = do

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

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

367− return (Via (map toLower x))

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

368368 bytecodeCodegen <|> viaCodegen

369369

370370 let hasOneArg = do