git.iko.soy/Idris-dev
on master help sign in
Idris-dev/src/IRTS/DumpBC.hs
85 lines 3.3 kB history raw
1{-|
2Module : IRTS.DumpBC
3Description : Serialise Idris to its IBC format.
5License : BSD3
6Maintainer : The Idris Community.
7-}
8module IRTS.DumpBC where
10import Idris.Core.TT
11import IRTS.Bytecode
12import IRTS.Simplified
14import Data.List
16interMap :: [a] -> [b] -> (a -> [b]) -> [b]
17interMap xs y f = concat (intersperse y (map f xs))
19indent :: Int -> String
20indent n = replicate (n*4) ' '
22serializeReg :: Reg -> String
23serializeReg (L n) = "L" ++ show n
24serializeReg (T n) = "T" ++ show n
25serializeReg r = show r
27serializeCase :: Show a => Int -> (a, [BC]) -> String
28serializeCase n (x, bcs) =
29 indent n ++ show x ++ ":\n" ++ interMap bcs "\n" (serializeBC (n + 1))
31serializeDefault :: Int -> [BC] -> String
32serializeDefault n bcs =
33 indent n ++ "default:\n" ++ interMap bcs "\n" (serializeBC (n + 1))
35serializeBC :: Int -> BC -> String
36serializeBC n bc = indent n ++
37 case bc of
38 ASSIGN a b ->
39 "ASSIGN " ++ serializeReg a ++ " " ++ serializeReg b
40 ASSIGNCONST a b ->
41 "ASSIGNCONST " ++ serializeReg a ++ " " ++ show b
42 UPDATE a b ->
43 "UPDATE " ++ serializeReg a ++ " " ++ serializeReg b
44 MKCON a Nothing b xs ->
45 "MKCON " ++ serializeReg a ++ " " ++ show b ++ " [" ++ (interMap xs ", " serializeReg) ++ "]"
46 MKCON a (Just r) b xs ->
47 "MKCON@" ++ serializeReg r ++ " " ++ serializeReg a ++ " " ++ show b ++ " [" ++ (interMap xs ", " serializeReg) ++ "]"
48 CASE safe r cases def ->
49 "CASE " ++ serializeReg r ++ ":\n" ++ interMap cases "\n" (serializeCase (n + 1)) ++
50 maybe "" (\def' -> "\n" ++ serializeDefault (n + 1) def') def
51 PROJECT a b c ->
52 "PROJECT " ++ serializeReg a ++ " " ++ show b ++ " " ++ show c
53 PROJECTINTO a b c ->
54 "PROJECTINTO " ++ serializeReg a ++ " " ++ serializeReg b ++ " " ++ show c
55 CONSTCASE r cases def ->
56 "CONSTCASE " ++ serializeReg r ++ ":\n" ++ interMap cases "\n" (serializeCase (n + 1)) ++
57 maybe "" (\def' -> "\n" ++ serializeDefault (n + 1) def') def
58 CALL x -> "CALL " ++ show x
59 TAILCALL x -> "TAILCALL " ++ show x
60 FOREIGNCALL r ret name args ->
61 "FOREIGNCALL " ++ serializeReg r ++ " \"" ++ show name ++ "\" " ++ show ret ++
62 " [" ++ interMap args ", " (\(ty, r) -> serializeReg r ++ " : " ++ show ty) ++ "]"
63 SLIDE n -> "SLIDE " ++ show n
64 REBASE -> "REBASE"
65 RESERVE n -> "RESERVE " ++ show n
66 RESERVENOALLOC n -> "RESERVENOALLOC " ++ show n
67 ADDTOP n -> "ADDTOP " ++ show n
68 TOPBASE n -> "TOPBASE " ++ show n
69 BASETOP n -> "BASETOP " ++ show n
70 STOREOLD -> "STOREOLD"
71 OP a b c ->
72 "OP " ++ serializeReg a ++ " " ++ show b ++ " [" ++ interMap c ", " serializeReg ++ "]"
73 NULL r -> "NULL " ++ serializeReg r
74 ERROR s -> "ERROR \"" ++ s ++ "\"" -- FIXME: s may contain quotes
75 -- Issue #1596
76serialize :: [(Name, [BC])] -> String
77serialize decls =
78 interMap decls "\n\n" serializeDecl
79 where
80 serializeDecl :: (Name, [BC]) -> String
81 serializeDecl (name, bcs) =
82 show name ++ ":\n" ++ interMap bcs "\n" (serializeBC 1)
84dumpBC :: [(Name, SDecl)] -> String -> IO ()
85dumpBC c output = writeFile output $ serialize $ map toBC c