Set up C generator

idris.cabal

@@ -40,7 +40,7 @@ Description:    Idris is a general purpose language with full dependent types.
 Cabal-Version:  >= 1.6
 Build-type:     Custom
 
-Data-files:            rts/libidris_rts.a rts/idris_rts.h
+Data-files:            rts/libidris_rts.a rts/idris_rts.h rts/idris_main.c
 Extra-source-files:    lib/Makefile  lib/*.idr lib/prelude/*.idr lib/network/*.idr
                        lib/control/monad/*.idr lib/language/*.idr
                        tutorial/examples/*.idr
@@ -71,6 +71,7 @@ Executable     idris
 
                               RTS.Bytecode, RTS.SC, RTS.PreC, RTS.CodegenC,
                               IRTS.Lang, IRTS.LParser, IRTS.Bytecode, IRTS.Simplified,
+                              IRTS.CodegenC,
 
                               Paths_idris
 

rts/idris_main.c

@@ -0,0 +1,5 @@
+int main(int argc, char* argv[]) {
+    VM* vm = init_vm(1024000, 1024000);
+
+    _idris_main(vm, NULL);
+}

src/IRTS/CodegenC.hs

@@ -0,0 +1,34 @@
+module IRTS.CodegenC where
+
+import IRTS.Bytecode
+import IRTS.Lang
+import Core.TT
+import Paths_idris
+
+import Data.Char
+
+cname :: Name -> String
+cname n = "_idris_" ++ concatMap cchar (show n)
+  where cchar x | isAlpha x || isDigit x = [x]
+                | otherwise = "_" ++ show (fromEnum x) ++ "_"
+
+indent i = take (i * 4) (repeat ' ')
+
+creg RVal = "RVAL"
+creg (L i) = "LOC(" ++ show i ++ ")"
+creg (T i) = "TOP(" ++ show i ++ ")"
+
+toDecl :: Name -> String
+toDecl f = "void " ++ cname f ++ "(VM*, VAL*);\n" 
+
+toC :: Name -> [BC] -> String
+toC f code 
+    = -- "/* " ++ show code ++ "*/\n\n" ++ 
+      "void " ++ cname f ++ "(VM* vm, VAL* oldbase) {" ++
+                 concatMap (bcc 1) code ++ "}\n\n"
+
+bcc :: Int -> BC -> String
+bcc i (ASSIGN l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"
+
+bcc i _ = indent i ++ "// not done yet\n"
+

src/IRTS/LParser.hs

@@ -5,6 +5,8 @@ import Core.TT
 import IRTS.Lang
 import IRTS.Simplified
 import IRTS.Bytecode
+import IRTS.CodegenC
+import Paths_idris
 
 import Text.ParserCombinators.Parsec
 import Text.ParserCombinators.Parsec.Error
@@ -47,10 +49,17 @@ fovm f = do defs <- parseFOVM f
             let tagged = addTags defs
             let ctxtIn = addAlist tagged emptyContext
             let checked = checkDefs ctxtIn tagged 
-            print checked
+            -- print checked
             case checked of
                    OK c -> do let bc = map toBC c
-                              print bc
+                              -- print bc
+                              let h = concatMap toDecl (map fst bc)
+                              let cc = concatMap (uncurry toC) bc
+                              putStrLn h
+                              putStrLn cc
+                              d <- getDataDir
+                              mprog <- readFile (d ++ "/rts/idris_main.c")
+                              putStrLn mprog
 
 parseFOVM :: FilePath -> IO [(Name, LDecl)]
 parseFOVM fname = do putStrLn $ "Reading " ++ fname