79e6bf7 · Idris-dev · git.iko.soy

idris.cabal+2−1

compare with master

unifiedsplit

@@ -40,7 +40,7 @@ Description: Idris is a general purpose language with full dependent types.

40Cabal-Version: >= 1.6

41Build-type: Custom

42

43−Data-files: rts/libidris_rts.a rts/idris_rts.h

43+Data-files: rts/libidris_rts.a rts/idris_rts.h rts/idris_main.c

44Extra-source-files: lib/Makefile lib/*.idr lib/prelude/*.idr lib/network/*.idr

45 lib/control/monad/*.idr lib/language/*.idr

46 tutorial/examples/*.idr

@@ -71,6 +71,7 @@ Executable idris

71

72 RTS.Bytecode, RTS.SC, RTS.PreC, RTS.CodegenC,

73 IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified,

74+ IRTS.CodegenC,

74

75

75 Paths_idris

76 Paths_idris

76

77

rts/idris_main.cnew file+5

@@ -0,0 +1,5 @@

1+int main(int argc, char* argv[]) {

2+ VM* vm = init_vm(1024000, 1024000);

3+

4+ _idris_main(vm, NULL);

5+}

src/IRTS/CodegenC.hsnew file+34

@@ -0,0 +1,34 @@

1+module IRTS.CodegenC where

2+

3+import IRTS.Bytecode

4+import IRTS.Lang

5+import Core.TT

6+import Paths_idris

7+

8+import Data.Char

9+

10+cname :: Name -> String

11+cname n = "_idris_" ++ concatMap cchar (show n)

12+ where cchar x | isAlpha x || isDigit x = [x]

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

14+

15+indent i = take (i * 4) (repeat ' ')

16+

17+creg RVal = "RVAL"

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

19+creg (T i) = "TOP(" ++ show i ++ ")"

20+

21+toDecl :: Name -> String

22+toDecl f = "void " ++ cname f ++ "(VM*, VAL*);\n"

23+

24+toC :: Name -> [BC] -> String

25+toC f code

26+ = -- "/* " ++ show code ++ "*/\n\n" ++

27+ "void " ++ cname f ++ "(VM* vm, VAL* oldbase) {" ++

28+ concatMap (bcc 1) code ++ "}\n\n"

29+

30+bcc :: Int -> BC -> String

31+bcc i (ASSIGN l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"

32+

33+bcc i _ = indent i ++ "// not done yet\n"

34+

src/IRTS/LParser.hs+11−2

@@ -5,6 +5,8 @@ import Core.TT

5import IRTS.Lang

6import IRTS.Simplified

7import IRTS.Bytecode

8+import IRTS.CodegenC

9+import Paths_idris

8

10

9import Text.ParserCombinators.Parsec

11import Text.ParserCombinators.Parsec

10import Text.ParserCombinators.Parsec.Error

12import Text.ParserCombinators.Parsec.Error

@@ -47,10 +49,17 @@ fovm f = do defs <- parseFOVM f

47 let tagged = addTags defs

49 let tagged = addTags defs

48 let ctxtIn = addAlist tagged emptyContext

50 let ctxtIn = addAlist tagged emptyContext

49 let checked = checkDefs ctxtIn tagged

51 let checked = checkDefs ctxtIn tagged

50− print checked

52+ -- print checked

51 case checked of

53 case checked of

52 OK c -> do let bc = map toBC c

54 OK c -> do let bc = map toBC c

53− print bc

55+ -- print bc

56+ let h = concatMap toDecl (map fst bc)

57+ let cc = concatMap (uncurry toC) bc

58+ putStrLn h

59+ putStrLn cc

60+ d <- getDataDir

61+ mprog <- readFile (d ++ "/rts/idris_main.c")

62+ putStrLn mprog

54

63

55parseFOVM :: FilePath -> IO [(Name, LDecl)]

64parseFOVM :: FilePath -> IO [(Name, LDecl)]

56parseFOVM fname = do putStrLn $ "Reading " ++ fname

65parseFOVM fname = do putStrLn $ "Reading " ++ fname