f149970 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Rename --target to --codegen and add options to specify target triple and CPU, defaulting to that of host

commitf14997006ce9f4af52861ca7fd542117ebca3bc6 authorBenjamin Saunders <besaunde@sfu.ca> dateFri 5 Jul 2013, 13:35 (13 years ago) parent7ebf672

9 files changed+152−96

compare with master

unifiedsplit

idris.cabal+1−1 src/IRTS/CodegenLLVM.hs+7−6 src/IRTS/Compiler.hs+9−7 src/IRTS/LParser.hs+3−3 src/Idris/AbsSyntax.hs+39−19 src/Idris/AbsSyntaxTree.hs+23−16 src/Idris/IBC.hs+8−8 src/Idris/Parser.hs+16−15 src/Idris/REPL.hs+46−21

idris.cabal+1−1

@@ -272,7 +272,7 @@ Executable idris

272272 haskeline>=0.7, split, directory,

273273 containers, process, transformers, filepath,

274274 directory, binary, bytestring, text, pretty,

275− language-java>=0.2.2, libffi, llvm-general==3.3.2.*

275+ language-java>=0.2.2, libffi, llvm-general==3.3.3.*

276276

277277 Extensions: MultiParamTypeClasses, FunctionalDependencies,

278278 FlexibleInstances, TemplateHaskell

src/IRTS/CodegenLLVM.hs+7−6

@@ -52,17 +52,16 @@ import Debug.Trace

5252data Target = Target { triple :: String, dataLayout :: DataLayout }

5353

5454codegenLLVM :: [(TT.Name, SDecl)] ->

55+ String -> -- target triple

56+ String -> -- target CPU

5557 FilePath -> -- output file name

5658 OutputType ->

5759 IO ()

58−codegenLLVM defs file outty = withContext $ \context -> do

59− triple <- getDefaultTargetTriple

60− cpu <- getHostCPUName

61− features <- getHostCPUFeatures

60+codegenLLVM defs triple cpu file outty = withContext $ \context -> do

6261 initializeAllTargets

6362 (target, _) <- failInIO $ lookupTarget Nothing triple

6463 withTargetOptions $ \options ->

65− withTargetMachine target triple cpu features options R.Default CM.Default CGO.Default $ \tm ->

64+ withTargetMachine target triple cpu S.empty options R.Default CM.Default CGO.Default $ \tm ->

6665 do layout <- getTargetMachineDataLayout tm

6766 let ast = codegen (Target triple layout) (map snd defs)

6867 result <- runErrorT . M.withModuleFromAST context ast $ \m ->

@@ -160,10 +159,12 @@ initDefs tgt =

160159 (Do $ Ret (Just (LocalReference (UnName 1))) [])

161160 ]

162161 , exfun "llvm.trap" VoidType [] False

162+ -- , exfun "llvm.llvm.memcpy.p0i8.p0i8.i32" VoidType [ptrI8, ptrI8, IntegerType 32, IntegerType 32, IntegerType 1] False

163+ -- , exfun "llvm.llvm.memcpy.p0i8.p0i8.i64" VoidType [ptrI8, ptrI8, IntegerType 64, IntegerType 32, IntegerType 1] False

164+ , exfun "memcpy" ptrI8 [ptrI8, ptrI8, intPtr] False

163165 , exfun "snprintf" (IntegerType 32) [ptrI8, intPtr, ptrI8] True

164166 , exfun "strcmp" (IntegerType 32) [ptrI8, ptrI8] False

165167 , exfun "strlen" intPtr [ptrI8] False

166− , exfun "memcpy" ptrI8 [ptrI8, ptrI8, intPtr] False

167168 , exfun "GC_init" VoidType [] False

168169 , exfun "GC_malloc" ptrI8 [intPtr] False

169170 , exfun "GC_malloc_atomic" ptrI8 [intPtr] False

src/IRTS/Compiler.hs+9−7

@@ -30,8 +30,8 @@ import System.FilePath ((</>), addTrailingPathSeparator)

3030

3131import Paths_idris

3232

33−compile :: Target -> FilePath -> Term -> Idris ()

34−compile target f tm

33+compile :: Codegen -> FilePath -> Term -> Idris ()

34+compile codegen f tm

3535 = do checkMVs

3636 let tmnames = namesUsed (STerm tm)

3737 usedIn <- mapM (allNames []) tmnames

@@ -39,9 +39,9 @@ compile target f tm

3939 defsIn <- mkDecls tm (concat used)

4040 findUnusedArgs (concat used)

4141 maindef <- irMain tm

42− objs <- getObjectFiles target

43− libs <- getLibs target

44− hdrs <- getHdrs target

42+ objs <- getObjectFiles codegen

43+ libs <- getLibs codegen

44+ hdrs <- getHdrs codegen

4545 let defs = defsIn ++ [(MN 0 "runMain", maindef)]

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

4747 let (nexttag, tagged) = addTags 65536 (liftAll defs)

@@ -64,9 +64,11 @@ compile target f tm

6464 case dumpDefun of

6565 Nothing -> return ()

6666 Just f -> liftIO $ writeFile f (dumpDefuns defuns)

67+ triple <- targetTriple

68+ cpu <- targetCPU

6769 iLOG "Building output"

6870 case checked of

69− OK c -> liftIO $ case target of

71+ OK c -> liftIO $ case codegen of

7072 ViaC ->

7173 codegenC c f outty hdrs

7274 (concatMap mkObj objs)

@@ -77,7 +79,7 @@ compile target f tm

7779 codegenJavaScript JavaScript c f outty

7880 ViaNode ->

7981 codegenJavaScript Node c f outty

80− ViaLLVM -> codegenLLVM c f outty

82+ ViaLLVM -> codegenLLVM c triple cpu f outty

8183

8284 Bytecode -> dumpBC c f

8385 Error e -> fail $ show e

src/IRTS/LParser.hs+3−3

@@ -49,8 +49,8 @@ strlit = PTok.stringLiteral lexer

4949chlit = PTok.charLiteral lexer

5050lchar = lexeme.char

5151

52−fovm :: Target -> OutputType -> FilePath -> IO ()

53−fovm tgt outty f

52+fovm :: Codegen -> OutputType -> FilePath -> IO ()

53+fovm cgn outty f

5454 = do defs <- parseFOVM f

5555 let (nexttag, tagged) = addTags 0 (liftAll defs)

5656 ctxtIn = addAlist tagged emptyContext

@@ -59,7 +59,7 @@ fovm tgt outty f

5959 let checked = checkDefs defuns (toAlist defuns)

6060-- print checked

6161 case checked of

62− OK c -> case tgt of

62+ OK c -> case cgn of

6363 ViaC -> codegenC c "a.out" outty ["math.h"] "" "" TRACE

6464 ViaJava -> codegenJava [] c "a.out" [] [] outty

6565 Error e -> fail $ show e

src/Idris/AbsSyntax.hs+39−19

@@ -30,19 +30,19 @@ import Util.System

3030getContext :: Idris Context

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

3232

33−forTarget :: Target -> [(Target, a)] -> [a]

34−forTarget tgt xs = [x | (tgt', x) <- xs, tgt == tgt']

33+forCodegen :: Codegen -> [(Codegen, a)] -> [a]

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

3535

36−getObjectFiles :: Target -> Idris [FilePath]

37−getObjectFiles tgt = do i <- getIState; return (forTarget tgt $ idris_objs i)

36+getObjectFiles :: Codegen -> Idris [FilePath]

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

3838

39−addObjectFile :: Target -> FilePath -> Idris ()

39+addObjectFile :: Codegen -> FilePath -> Idris ()

4040addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = (tgt, f) : idris_objs i }

4141

42−getLibs :: Target -> Idris [String]

43−getLibs tgt = do i <- getIState; return (forTarget tgt $ idris_libs i)

42+getLibs :: Codegen -> Idris [String]

43+getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)

4444

45−addLib :: Target -> String -> Idris ()

45+addLib :: Codegen -> String -> Idris ()

4646addLib tgt f = do i <- getIState; putIState $ i { idris_libs = (tgt, f) : idris_libs i }

4747

4848addDyLib :: [String] -> Idris (Either DynamicLib String)

@@ -55,7 +55,7 @@ addDyLib libs = do i <- getIState

5555 putIState $ i { idris_dynamic_libs = x:ls }

5656 return (Left x)

5757

58−addHdr :: Target -> String -> Idris ()

58+addHdr :: Codegen -> String -> Idris ()

5959addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = (tgt, f) : idris_hdrs i }

6060

6161addLangExt :: LanguageExt -> Idris ()

@@ -163,8 +163,8 @@ addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }

163163clearIBC :: Idris ()

164164clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }

165165

166−getHdrs :: Target -> Idris [String]

167−getHdrs tgt = do i <- getIState; return (forTarget tgt $ idris_hdrs i)

166+getHdrs :: Codegen -> Idris [String]

167+getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)

168168

169169setErrLine :: Int -> Idris ()

170170setErrLine x = do i <- getIState;

@@ -345,15 +345,15 @@ getQuiet = do i <- getIState

345345 let opts = idris_options i

346346 return (opt_quiet opts)

347347

348−setTarget :: Target -> Idris ()

349−setTarget t = do i <- getIState

350− let opts = idris_options i

351− let opt' = opts { opt_target = t }

352− putIState $ i { idris_options = opt' }

348+setCodegen :: Codegen -> Idris ()

349+setCodegen t = do i <- getIState

350+ let opts = idris_options i

351+ let opt' = opts { opt_codegen = t }

352+ putIState $ i { idris_options = opt' }

353353

354−target :: Idris Target

355−target = do i <- getIState

356− return (opt_target (idris_options i))

354+codegen :: Idris Codegen

355+codegen = do i <- getIState

356+ return (opt_codegen (idris_options i))

357357

358358setOutputTy :: OutputType -> Idris ()

359359setOutputTy t = do i <- getIState

@@ -370,6 +370,26 @@ setIdeSlave True = do i <- getIState

370370 putIState $ i { idris_outputmode = (IdeSlave 0) }

371371setIdeSlave False = return ()

372372

373+setTargetTriple :: String -> Idris ()

374+setTargetTriple t = do i <- getIState

375+ let opts = idris_options i

376+ opt' = opts { opt_triple = t }

377+ putIState $ i { idris_options = opt' }

378+

379+targetTriple :: Idris String

380+targetTriple = do i <- getIState

381+ return (opt_triple (idris_options i))

382+

383+setTargetCPU :: String -> Idris ()

384+setTargetCPU t = do i <- getIState

385+ let opts = idris_options i

386+ opt' = opts { opt_cpu = t }

387+ putIState $ i { idris_options = opt' }

388+

389+targetCPU :: Idris String

390+targetCPU = do i <- getIState

391+ return (opt_cpu (idris_options i))

392+

373393verbose :: Idris Bool

374394verbose = do i <- getIState

375395 return (opt_verbose (idris_options i))

src/Idris/AbsSyntaxTree.hs+23−16

@@ -33,10 +33,12 @@ data IOption = IOption { opt_logLevel :: Int,

3333 opt_repl :: Bool,

3434 opt_verbose :: Bool,

3535 opt_quiet :: Bool,

36− opt_target :: Target,

36+ opt_codegen :: Codegen,

3737 opt_outputTy :: OutputType,

3838 opt_ibcsubdir :: FilePath,

3939 opt_importdirs :: [FilePath],

40+ opt_triple :: String,

41+ opt_cpu :: String,

4042 opt_cmdline :: [Opt] -- remember whole command line

4143 }

4244 deriving (Show, Eq)

@@ -50,10 +52,12 @@ defaultOpts = IOption { opt_logLevel = 0

5052 , opt_repl = True

5153 , opt_verbose = True

5254 , opt_quiet = False

53− , opt_target = ViaC

55+ , opt_codegen = ViaC

5456 , opt_outputTy = Executable

5557 , opt_ibcsubdir = ""

5658 , opt_importdirs = []

59+ , opt_triple = ""

60+ , opt_cpu = ""

5761 , opt_cmdline = []

5862 }

5963

@@ -95,9 +99,9 @@ data IState = IState {

9599 syntax_keywords :: [String],

96100 imported :: [FilePath], -- ^ The imported modules

97101 idris_scprims :: [(Name, (Int, PrimFn))],

98− idris_objs :: [(Target, FilePath)],

99− idris_libs :: [(Target, String)],

100− idris_hdrs :: [(Target, String)],

102+ idris_objs :: [(Codegen, FilePath)],

103+ idris_libs :: [(Codegen, String)],

104+ idris_hdrs :: [(Codegen, String)],

101105 proof_list :: [(Name, [String])],

102106 errLine :: Maybe Int,

103107 lastParse :: Maybe Name,

@@ -145,10 +149,10 @@ data IBCWrite = IBCFix FixDecl

145149 | IBCSyntax Syntax

146150 | IBCKeyword String

147151 | IBCImport FilePath

148− | IBCObj Target FilePath

149− | IBCLib Target String

152+ | IBCObj Codegen FilePath

153+ | IBCLib Codegen String

150154 | IBCDyLib String

151− | IBCHeader Target String

155+ | IBCHeader Codegen String

152156 | IBCAccess Name Accessibility

153157 | IBCTotal Name Totality

154158 | IBCFlags Name [FnOpt]

@@ -171,12 +175,12 @@ type Idris = StateT IState IO

171175

172176-- Commands in the REPL

173177

174−data Target = ViaC

175− | ViaJava

176− | ViaNode

177− | ViaJavaScript

178− | ViaLLVM

179− | Bytecode

178+data Codegen = ViaC

179+ | ViaJava

180+ | ViaNode

181+ | ViaJavaScript

182+ | ViaLLVM

183+ | Bytecode

180184 deriving (Show, Eq)

181185

182186-- | REPL commands

@@ -191,7 +195,7 @@ data Command = Quit

191195 | ChangeDirectory FilePath

192196 | ModImport String

193197 | Edit

194− | Compile Target String

198+ | Compile Codegen String

195199 | Execute

196200 | ExecVal PTerm

197201 | NewCompile String

@@ -251,10 +255,13 @@ data Opt = Filename String

251255 | DumpDefun String

252256 | DumpCases String

253257 | FOVM String

254− | UseTarget Target

258+ | UseCodegen Codegen

255259 | OutputTy OutputType

256260 | Extension LanguageExt

257261 | InterpretScript String

262+ | TargetTriple String

263+ | TargetCPU String

264+ | OptLevel Int

258265 deriving (Show, Eq)

259266

260267-- Parsed declarations

src/Idris/IBC.hs+8−8

@@ -38,10 +38,10 @@ data IBCFile = IBCFile { ver :: Word8,

3838 ibc_optimise :: [(Name, OptInfo)],

3939 ibc_syntax :: [Syntax],

4040 ibc_keywords :: [String],

41− ibc_objs :: [(Target, FilePath)],

42− ibc_libs :: [(Target, String)],

41+ ibc_objs :: [(Codegen, FilePath)],

42+ ibc_libs :: [(Codegen, String)],

4343 ibc_dynamic_libs :: [String],

44− ibc_hdrs :: [(Target, String)],

44+ ibc_hdrs :: [(Codegen, String)],

4545 ibc_access :: [(Name, Accessibility)],

4646 ibc_total :: [(Name, Totality)],

4747 ibc_flags :: [(Name, [FnOpt])],

@@ -243,10 +243,10 @@ pKeywords :: [String] -> Idris ()

243243pKeywords k = do i <- getIState

244244 putIState (i { syntax_keywords = k ++ syntax_keywords i })

245245

246−pObjs :: [(Target, FilePath)] -> Idris ()

246+pObjs :: [(Codegen, FilePath)] -> Idris ()

247247pObjs os = mapM_ (uncurry addObjectFile) os

248248

249−pLibs :: [(Target, String)] -> Idris ()

249+pLibs :: [(Codegen, String)] -> Idris ()

250250pLibs ls = mapM_ (uncurry addLib) ls

251251

252252pDyLibs :: [String] -> Idris ()

@@ -256,7 +256,7 @@ pDyLibs ls = do res <- mapM (addDyLib . return) ls

256256 where checkLoad (Left _) = return ()

257257 checkLoad (Right err) = fail err

258258

259−pHdrs :: [(Target, String)] -> Idris ()

259+pHdrs :: [(Codegen, String)] -> Idris ()

260260pHdrs hs = mapM_ (uncurry addHdr) hs

261261

262262pDefs :: [(Name, Def)] -> Idris ()

@@ -1678,7 +1678,7 @@ instance Binary SSymbol where

16781678 return (Binding x1)

16791679 _ -> error "Corrupted binary data for SSymbol"

16801680

1681−instance Binary Target where

1681+instance Binary Codegen where

16821682 put x

16831683 = case x of

16841684 ViaC -> putWord8 0

@@ -1694,5 +1694,5 @@ instance Binary Target where

16941694 2 -> return ViaNode

16951695 3 -> return ViaJavaScript

16961696 4 -> return Bytecode

1697− _ -> error "Corrupted binary data for Target"

1697+ _ -> error "Corrupted binary data for Codegen"

16981698

src/Idris/Parser.hs+16−15

@@ -1535,25 +1535,26 @@ pWhereblock n syn

15351535 closeBlock

15361536 return (concat ds, map (\x -> (x, decoration syn x)) dns)

15371537

1538−pTarget :: IParser Target

1539−pTarget = try (do reserved "C"; return ViaC)

1540− <|> try (do reserved "Java"; return ViaJava)

1541− <|> try (do reserved "JavaScript"; return ViaJavaScript)

1542− <|> try (do reserved "Node"; return ViaNode)

1543− <|> try (do reserved "Bytecode"; return Bytecode)

1538+pCodegen :: IParser Codegen

1539+pCodegen = try (do reserved "C"; return ViaC)

1540+ <|> try (do reserved "Java"; return ViaJava)

1541+ <|> try (do reserved "JavaScript"; return ViaJavaScript)

1542+ <|> try (do reserved "Node"; return ViaNode)

1543+ <|> try (do reserved "LLVM"; return ViaLLVM)

1544+ <|> try (do reserved "Bytecode"; return Bytecode)

15441545

15451546pDirective :: SyntaxInfo -> IParser [PDecl]

1546−pDirective syn = try (do lchar '%'; reserved "lib"; tgt <- pTarget; lib <- strlit;

1547− return [PDirective (do addLib tgt lib

1548− addIBC (IBCLib tgt lib))])

1549− <|> try (do lchar '%'; reserved "link"; tgt <- pTarget; obj <- strlit;

1547+pDirective syn = try (do lchar '%'; reserved "lib"; cgn <- pCodegen; lib <- strlit;

1548+ return [PDirective (do addLib cgn lib

1549+ addIBC (IBCLib cgn lib))])

1550+ <|> try (do lchar '%'; reserved "link"; cgn <- pCodegen; obj <- strlit;

15501551 return [PDirective (do datadir <- liftIO getDataDir

15511552 o <- liftIO $ findInPath [".", datadir] obj

1552− addIBC (IBCObj tgt o)

1553− addObjectFile tgt o)])

1554− <|> try (do lchar '%'; reserved "include"; tgt <- pTarget; hdr <- strlit;

1555− return [PDirective (do addHdr tgt hdr

1556− addIBC (IBCHeader tgt hdr))])

1553+ addIBC (IBCObj cgn o)

1554+ addObjectFile cgn o)])

1555+ <|> try (do lchar '%'; reserved "include"; cgn <- pCodegen; hdr <- strlit;

1556+ return [PDirective (do addHdr cgn hdr

1557+ addIBC (IBCHeader cgn hdr))])

15571558 <|> try (do lchar '%'; reserved "hide"; n <- iName []

15581559 return [PDirective (do setAccessibility n Hidden

15591560 addIBC (IBCAccess n Hidden))])

src/Idris/REPL.hs+46−21

@@ -39,6 +39,8 @@ import IRTS.CodegenCommon

3939-- import RTS.PreC

4040-- import RTS.CodegenC

4141

42+import LLVM.General.Target

43+

4244import System.Console.Haskeline as H

4345import System.FilePath

4446import System.Exit

@@ -155,8 +157,8 @@ ideslaveProcess fn Execute = do process fn Execute

155157 iResult ""

156158ideslaveProcess fn (NewCompile f) = do process fn (NewCompile f)

157159 iResult ""

158−ideslaveProcess fn (Compile target f) = do process fn (Compile target f)

159− iResult ""

160+ideslaveProcess fn (Compile codegen f) = do process fn (Compile codegen f)

161+ iResult ""

160162ideslaveProcess fn (LogLvl i) = do process fn (LogLvl i)

161163 iResult ""

162164ideslaveProcess fn (Pattelab t) = process fn (Pattelab t)

@@ -465,7 +467,7 @@ process fn Execute = do (m, _) <- elabVal toplevel False

465467-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))

466468 (tmpn, tmph) <- liftIO tempfile

467469 liftIO $ hClose tmph

468− t <- target

470+ t <- codegen

469471 compile t tmpn m

470472 liftIO $ system tmpn

471473 return ()

@@ -476,11 +478,11 @@ process fn (NewCompile f)

476478 [pexp $ PRef fc (NS (UN "main") ["Main"])])

477479 compileEpic f m

478480 where fc = FC "main" 0

479−process fn (Compile target f)

481+process fn (Compile codegen f)

480482 = do (m, _) <- elabVal toplevel False

481483 (PApp fc (PRef fc (UN "run__IO"))

482484 [pexp $ PRef fc (NS (UN "main") ["Main"])])

483− compile target f m

485+ compile codegen f m

484486 where fc = FC "main" 0

485487process fn (LogLvl i) = setLogLevel i

486488-- Elaborate as if LHS of a pattern (debug command)

@@ -560,14 +562,14 @@ displayHelp = let vstr = showVersion version in

560562 l ++ take (c1 - length l) (repeat ' ') ++

561563 m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"

562564

563−parseTarget :: String -> Target

564−parseTarget "C" = ViaC

565−parseTarget "Java" = ViaJava

566−parseTarget "bytecode" = Bytecode

567−parseTarget "javascript" = ViaJavaScript

568−parseTarget "node" = ViaNode

569−parseTarget "llvm" = ViaLLVM

570−parseTarget _ = error "unknown target" -- FIXME: partial function

565+parseCodegen :: String -> Codegen

566+parseCodegen "C" = ViaC

567+parseCodegen "Java" = ViaJava

568+parseCodegen "bytecode" = Bytecode

569+parseCodegen "javascript" = ViaJavaScript

570+parseCodegen "node" = ViaNode

571+parseCodegen "llvm" = ViaLLVM

572+parseCodegen _ = error "unknown codegen" -- FIXME: partial function

571573

572574parseArgs :: [String] -> [Opt]

573575parseArgs [] = []

@@ -605,10 +607,17 @@ parseArgs ("-S":ns) = OutputTy Raw : (parseArgs ns)

605607parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)

606608parseArgs ("--dumpdefuns":n:ns) = DumpDefun n : (parseArgs ns)

607609parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)

608−parseArgs ("--target":n:ns) = UseTarget (parseTarget n) : (parseArgs ns)

610+parseArgs ("--codegen":n:ns) = UseCodegen (parseCodegen n) : (parseArgs ns)

609611parseArgs ["--exec"] = InterpretScript "Main.main" : []

610612parseArgs ("--exec":expr:ns) = InterpretScript expr : parseArgs ns

611613parseArgs ("-XTypeProviders":ns) = Extension TypeProviders : (parseArgs ns)

614+parseArgs ("-O3":ns) = OptLevel 3 : parseArgs ns

615+parseArgs ("-O2":ns) = OptLevel 2 : parseArgs ns

616+parseArgs ("-O1":ns) = OptLevel 1 : parseArgs ns

617+parseArgs ("-O0":ns) = OptLevel 0 : parseArgs ns

618+parseArgs ("-O":n:ns) = OptLevel (read n) : parseArgs ns

619+parseArgs ("--target":n:ns) = TargetTriple n : parseArgs ns

620+parseArgs ("--cpu":n:ns) = TargetCPU n : parseArgs ns

612621parseArgs (n:ns) = Filename n : (parseArgs ns)

613622

614623helphead =

@@ -637,10 +646,16 @@ idrisMain opts =

637646 let bcs = opt getBC opts

638647 let vm = opt getFOVM opts

639648 let pkgdirs = opt getPkgDir opts

649+ trpl <- case opt getTriple opts of

650+ [] -> liftIO $ getDefaultTargetTriple

651+ xs -> return (last xs)

652+ tcpu <- case opt getCPU opts of

653+ [] -> liftIO $ getHostCPUName

654+ xs -> return (last xs)

640655 let outty = case opt getOutputTy opts of

641656 [] -> Executable

642657 xs -> last xs

643− let tgt = case opt getTarget opts of

658+ let cgn = case opt getCodegen opts of

644659 [] -> ViaC

645660 xs -> last xs

646661 script <- case opt getExecScript opts of

@@ -657,13 +672,15 @@ idrisMain opts =

657672 setVerbose runrepl

658673 setCmdLine opts

659674 setOutputTy outty

660− setTarget tgt

675+ setCodegen cgn

676+ setTargetTriple trpl

677+ setTargetCPU tcpu

661678 when (Verbose `elem` opts) $ setVerbose True

662679 mapM_ makeOption opts

663680 -- if we have the --fovm flag, drop into the first order VM testing

664681 case vm of

665682 [] -> return ()

666− xs -> liftIO $ mapM_ (fovm tgt outty) xs

683+ xs -> liftIO $ mapM_ (fovm cgn outty) xs

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

668685 case bcs of

669686 [] -> return ()

@@ -684,7 +701,7 @@ idrisMain opts =

684701 ok <- noErrors

685702 when ok $ case output of

686703 [] -> return ()

687− (o:_) -> process "" (Compile tgt o)

704+ (o:_) -> process "" (Compile cgn o)

688705 when ok $ case newoutput of

689706 [] -> return ()

690707 (o:_) -> process "" (NewCompile o)

@@ -758,9 +775,9 @@ getPkgClean :: Opt -> Maybe String

758775getPkgClean (PkgClean str) = Just str

759776getPkgClean _ = Nothing

760777

761−getTarget :: Opt -> Maybe Target

762−getTarget (UseTarget x) = Just x

763−getTarget _ = Nothing

778+getCodegen :: Opt -> Maybe Codegen

779+getCodegen (UseCodegen x) = Just x

780+getCodegen _ = Nothing

764781

765782getExecScript :: Opt -> Maybe String

766783getExecScript (InterpretScript expr) = Just expr

@@ -774,6 +791,14 @@ getLanguageExt :: Opt -> Maybe LanguageExt

774791getLanguageExt (Extension e) = Just e

775792getLanguageExt _ = Nothing

776793

794+getTriple :: Opt -> Maybe String

795+getTriple (TargetTriple x) = Just x

796+getTriple _ = Nothing

797+

798+getCPU :: Opt -> Maybe String

799+getCPU (TargetCPU x) = Just x

800+getCPU _ = Nothing

801+

777802opt :: (Opt -> Maybe a) -> [Opt] -> [a]

778803opt = mapMaybe

779804