d1ee911 · Idris-dev · git.iko.soy

idris.cabal+1−1

compare with master

unifiedsplit

@@ -84,7 +84,7 @@ Executable idris

84 IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified,

85 IRTS.CodegenC, IRTS.Defunctionalise, IRTS.Inliner,

86 IRTS.Compiler, IRTS.CodegenJava, IRTS.BCImp,

87− IRTS.CodegenCommon

87+ IRTS.CodegenCommon, IRTS.DumpBC

88

89 Paths_idris

90

src/IRTS/CodegenC.hs+6−4

@@ -59,9 +59,10 @@ codegenC defs out exec incs objs libs dbg

59 when (exit /= ExitSuccess) $

60 putStrLn ("FAILURE: " ++ gcc)

61

62+headers xs =

63+ concatMap

64+ (\h -> "#include <" ++ h ++ ">\n")

62−headers [] = "#include <idris_rts.h>\n#include <idris_stdfgn.h>\n" ++

65+ (xs ++ ["idris_rts.h", "idris_stdfgn.h", "gmp.h", "assert.h"])

63− "#include <gmp.h>\n#include <assert.h>\n"

64−headers (x : xs) = "#include <" ++ x ++ ">\n" ++ headers xs

65

66

66debug TRACE = "#define IDRIS_TRACE\n\n"

67debug TRACE = "#define IDRIS_TRACE\n\n"

67debug _ = ""

68debug _ = ""

@@ -75,7 +76,8 @@ cname n = "_idris_" ++ concatMap cchar (show n)

75 where cchar x | isAlpha x || isDigit x = [x]

76 where cchar x | isAlpha x || isDigit x = [x]

76 | otherwise = "_" ++ show (fromEnum x) ++ "_"

77 | otherwise = "_" ++ show (fromEnum x) ++ "_"

77

78

78−indent i = take (i * 4) (repeat ' ')

79+indent :: Int -> String

80+indent n = replicate (n*4) ' '

79

81

80creg RVal = "RVAL"

82creg RVal = "RVAL"

81creg (L i) = "LOC(" ++ show i ++ ")"

83creg (L i) = "LOC(" ++ show i ++ ")"

src/IRTS/Compiler.hs+2

@@ -8,6 +8,7 @@ import IRTS.Simplified

8import IRTS.CodegenCommon

9import IRTS.CodegenC

10import IRTS.CodegenJava

11+import IRTS.DumpBC

11import IRTS.Inliner

12import IRTS.Inliner

12

13

13import Idris.AbsSyntax

14import Idris.AbsSyntax

@@ -68,6 +69,7 @@ compile target f tm

68 (concatMap mkObj objs)

69 (concatMap mkObj objs)

69 (concatMap mkLib libs) NONE

70 (concatMap mkLib libs) NONE

70 ViaJava -> liftIO $ codegenJava c f outty

71 ViaJava -> liftIO $ codegenJava c f outty

72+ Bytecode -> liftIO $ dumpBC c f

71 Error e -> fail $ show e

73 Error e -> fail $ show e

72 where checkMVs = do i <- get

74 where checkMVs = do i <- get

73 case idris_metavars i \\ primDefs of

75 case idris_metavars i \\ primDefs of

src/IRTS/DumpBC.hsnew file+76

@@ -0,0 +1,76 @@

1+module IRTS.DumpBC where

2+

3+import IRTS.Lang

4+import IRTS.Simplified

5+import Core.TT

6+

7+import IRTS.Bytecode

8+import Data.List

9+

10+interMap :: [a] -> [b] -> (a -> [b]) -> [b]

11+interMap xs y f = concat (intersperse y (map f xs))

12+

13+indent :: Int -> String

14+indent n = replicate (n*4) ' '

15+

16+serializeReg :: Reg -> String

17+serializeReg (L n) = "L" ++ show n

18+serializeReg (T n) = "T" ++ show n

19+serializeReg r = show r

20+

21+serializeCase :: Show a => Int -> (a, [BC]) -> String

22+serializeCase n (x, bcs) =

23+ indent n ++ show x ++ ":\n" ++ interMap bcs "\n" (serializeBC (n + 1))

24+

25+serializeDefault :: Int -> [BC] -> String

26+serializeDefault n bcs =

27+ indent n ++ "default:\n" ++ interMap bcs "\n" (serializeBC (n + 1))

28+

29+serializeBC :: Int -> BC -> String

30+serializeBC n bc = indent n ++

31+ case bc of

32+ ASSIGN a b ->

33+ "ASSIGN " ++ serializeReg a ++ " " ++ serializeReg b

34+ ASSIGNCONST a b ->

35+ "ASSIGNCONST " ++ serializeReg a ++ " " ++ show b

36+ UPDATE a b ->

37+ "UPDATE " ++ serializeReg a ++ " " ++ serializeReg b

38+ MKCON a b xs ->

39+ "MKCON " ++ serializeReg a ++ " " ++ show b ++ " [" ++ (interMap xs ", " serializeReg) ++ "]"

40+ CASE r cases def ->

41+ "CASE " ++ serializeReg r ++ ":\n" ++ interMap cases "\n" (serializeCase (n + 1)) ++

42+ maybe "" (\def' -> "\n" ++ serializeDefault (n + 1) def') def

43+ PROJECT a b c ->

44+ "PROJECT " ++ serializeReg a ++ " " ++ show b ++ " " ++ show c

45+ PROJECTINTO a b c ->

46+ "PROJECTINTO " ++ serializeReg a ++ " " ++ serializeReg b ++ " " ++ show c

47+ CONSTCASE r cases def ->

48+ "CONSTCASE " ++ serializeReg r ++ ":\n" ++ interMap cases "\n" (serializeCase (n + 1)) ++

49+ maybe "" (\def' -> "\n" ++ serializeDefault (n + 1) def') def

50+ CALL x -> "CALL " ++ show x

51+ TAILCALL x -> "TAILCALL " ++ show x

52+ FOREIGNCALL r _ ret name args ->

53+ "FOREIGNCALL " ++ serializeReg r ++ " \"" ++ name ++ "\" " ++ show ret ++

54+ " [" ++ interMap args ", " (\(ty, r) -> serializeReg r ++ " : " ++ show ty) ++ "]"

55+ SLIDE n -> "SLIDE " ++ show n

56+ REBASE -> "REBASE"

57+ RESERVE n -> "RESERVE " ++ show n

58+ ADDTOP n -> "ADDTOP " ++ show n

59+ TOPBASE n -> "TOPBASE " ++ show n

60+ BASETOP n -> "BASETOP " ++ show n

61+ STOREOLD -> "STOREOLD"

62+ OP a b c ->

63+ "OP " ++ serializeReg a ++ " " ++ show b ++ " [" ++ interMap c ", " serializeReg ++ "]"

64+ NULL r -> "NULL " ++ show r

65+ ERROR s -> "ERROR \"" ++ s ++ "\"" -- FIXME: s may contain quotes

66+

67+serialize :: [(Name, [BC])] -> String

68+serialize decls =

69+ interMap decls "\n\n" serializeDecl

70+ where

71+ serializeDecl :: (Name, [BC]) -> String

72+ serializeDecl (name, bcs) =

73+ show name ++ ":\n" ++ interMap bcs "\n" (serializeBC 1)

74+

75+dumpBC :: [(Name, SDecl)] -> String -> IO ()

76+dumpBC c output = writeFile output $ serialize $ map toBC c

src/Idris/AbsSyntaxTree.hs+1−1

@@ -140,7 +140,7 @@ type Idris = StateT IState (InputT IO)

140

141-- Commands in the REPL

142

143−data Target = ViaC | ViaJava

143+data Target = ViaC | ViaJava | Bytecode

144 deriving (Show, Eq)

145

146data Command = Quit

src/Idris/REPL.hs+11−4

@@ -416,6 +416,12 @@ displayHelp = let vstr = showVersion version in

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

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

418

419+parseTarget :: String -> Target

420+parseTarget "C" = ViaC

421+parseTarget "Java" = ViaJava

422+parseTarget "bytecode" = Bytecode

423+parseTarget _ = error "unknown target" -- FIXME: partial function

424+

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

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

420parseArgs [] = []

426parseArgs [] = []

421parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)

427parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)

@@ -450,6 +456,7 @@ parseArgs ("-S":ns) = OutputTy Raw : (parseArgs ns)

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

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

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

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

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

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

459+parseArgs ("--target":n:ns) = UseTarget (parseTarget n) : (parseArgs ns)

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

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

454

461

455help =

462help =

@@ -510,12 +517,12 @@ idrisMain opts =

510 mapM_ makeOption opts

517 mapM_ makeOption opts

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

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

512 case vm of

519 case vm of

513− [] -> return ()

520+ [] -> return ()

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

521+ xs -> liftIO $ mapM_ (fovm tgt outty) xs

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

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

516 case bcs of

523 case bcs of

517− [] -> return ()

524+ [] -> return ()

518− xs -> return () -- liftIO $ mapM_ bcAsm xs

525+ xs -> return () -- liftIO $ mapM_ bcAsm xs

519 case ibcsubdir of

526 case ibcsubdir of

520 [] -> setIBCSubDir ""

527 [] -> setIBCSubDir ""

521 (d:_) -> setIBCSubDir d

528 (d:_) -> setIBCSubDir d

src/Main.hs+4−3

@@ -89,6 +89,7 @@ usagemsg = "Idris version " ++ ver ++ "\n" ++

89 "\t--log [level] Set debugging log level\n" ++

90 "\t-S Do no further compilation of code generator output\n" ++

91 "\t-c Compile to object files rather than an executable\n" ++

92− "\t--libdir Show library install directory and exit\n" ++

92+ "\t--libdir Show library install directory and exit\n" ++

93− "\t--link Show C library directories and exit (for C linking)\n" ++

93+ "\t--link Show C library directories and exit (for C linking)\n" ++

94− "\t--include Show C include directories and exit (for C linking)\n"

94+ "\t--include Show C include directories and exit (for C linking)\n" ++

95+ "\t--target [target] Set the target: C, Java, bytecode\n"