git.iko.soy/Idris-dev
on aeb032a help sign in
Idris-dev/src/IRTS/DumpBC.hs
84 lines 3.2 kB history raw
1{-|
2Module : IRTS.DumpBC
3Description : Serialise Idris to its IBC format.
4Copyright :
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 ADDTOP n -> "ADDTOP " ++ show n
67 TOPBASE n -> "TOPBASE " ++ show n
68 BASETOP n -> "BASETOP " ++ show n
69 STOREOLD -> "STOREOLD"
70 OP a b c ->
71 "OP " ++ serializeReg a ++ " " ++ show b ++ " [" ++ interMap c ", " serializeReg ++ "]"
72 NULL r -> "NULL " ++ serializeReg r
73 ERROR s -> "ERROR \"" ++ s ++ "\"" -- FIXME: s may contain quotes
74 -- Issue #1596
75serialize :: [(Name, [BC])] -> String
76serialize decls =
77 interMap decls "\n\n" serializeDecl
78 where
79 serializeDecl :: (Name, [BC]) -> String
80 serializeDecl (name, bcs) =
81 show name ++ ":\n" ++ interMap bcs "\n" (serializeBC 1)
83dumpBC :: [(Name, SDecl)] -> String -> IO ()
84dumpBC c output = writeFile output $ serialize $ map toBC c