content: {-|
  Module      : IRTS.DumpBC
  Description : Serialise Idris to its IBC format.
  
  License     : BSD3
  Maintainer  : The Idris Community.
  -}
  module IRTS.DumpBC where
  
  import Idris.Core.TT
  import IRTS.Bytecode
  import IRTS.Simplified
  
  import Data.List
  
  interMap :: [a] -> [b] -> (a -> [b]) -> [b]
  interMap xs y f = concat (intersperse y (map f xs))
  
  indent :: Int -> String
  indent n = replicate (n*4) ' '
  
  serializeReg :: Reg -> String
  serializeReg (L n) = "L" ++ show n
  serializeReg (T n) = "T" ++ show n
  serializeReg r = show r
  
  serializeCase :: Show a => Int -> (a, [BC]) -> String
  serializeCase n (x, bcs) =
    indent n ++ show x ++ ":\n" ++ interMap bcs "\n" (serializeBC (n + 1))
  
  serializeDefault :: Int -> [BC] -> String
  serializeDefault n bcs =
    indent n ++ "default:\n" ++ interMap bcs "\n" (serializeBC (n + 1))
  
  serializeBC :: Int -> BC -> String
  serializeBC n bc = indent n ++
      case bc of
        ASSIGN a b ->
          "ASSIGN " ++ serializeReg a ++ " " ++ serializeReg b
        ASSIGNCONST a b ->
          "ASSIGNCONST " ++ serializeReg a ++ " " ++ show b
        UPDATE a b ->
          "UPDATE " ++ serializeReg a ++ " " ++ serializeReg b
        MKCON a Nothing b xs ->
          "MKCON " ++ serializeReg a ++ " " ++ show b ++ " [" ++ (interMap xs ", " serializeReg) ++ "]"
        MKCON a (Just r) b xs ->
          "MKCON@" ++ serializeReg r ++ " " ++ serializeReg a ++ " " ++ show b ++ " [" ++ (interMap xs ", " serializeReg) ++ "]"
        CASE safe r cases def ->
          "CASE " ++ serializeReg r ++ ":\n" ++ interMap cases "\n" (serializeCase (n + 1)) ++
          maybe "" (\def' -> "\n" ++ serializeDefault (n + 1) def') def
        PROJECT a b c ->
          "PROJECT " ++ serializeReg a ++ " " ++ show b ++ " " ++ show c
        PROJECTINTO a b c ->
          "PROJECTINTO " ++ serializeReg a ++ " " ++ serializeReg b ++ " " ++ show c
        CONSTCASE r cases def ->
          "CONSTCASE " ++ serializeReg r ++ ":\n" ++ interMap cases "\n" (serializeCase (n + 1)) ++
          maybe "" (\def' -> "\n" ++ serializeDefault (n + 1) def') def
        CALL x -> "CALL " ++ show x
        TAILCALL x -> "TAILCALL " ++ show x
        FOREIGNCALL r ret name args ->
          "FOREIGNCALL " ++ serializeReg r ++ " \"" ++ show name ++ "\" " ++ show ret ++
          " [" ++ interMap args ", " (\(ty, r) -> serializeReg r ++ " : " ++ show ty) ++ "]"
        SLIDE n -> "SLIDE " ++ show n
        REBASE -> "REBASE"
        RESERVE n -> "RESERVE " ++ show n
        RESERVENOALLOC n -> "RESERVENOALLOC " ++ show n
        ADDTOP n -> "ADDTOP " ++ show n
        TOPBASE n -> "TOPBASE " ++ show n
        BASETOP n -> "BASETOP " ++ show n
        STOREOLD -> "STOREOLD"
        OP a b c ->
          "OP " ++ serializeReg a ++ " " ++ show b ++ " [" ++ interMap c ", " serializeReg ++ "]"
        NULL r -> "NULL " ++ serializeReg r
        ERROR s -> "ERROR \"" ++ s ++ "\"" -- FIXME: s may contain quotes
                                           -- Issue #1596
  serialize :: [(Name, [BC])] -> String
  serialize decls =
      interMap decls "\n\n" serializeDecl
    where
      serializeDecl :: (Name, [BC]) -> String
      serializeDecl (name, bcs) =
        show name ++ ":\n" ++ interMap bcs "\n" (serializeBC 1)
  
  dumpBC :: [(Name, SDecl)] -> String -> IO ()
  dumpBC c output = writeFile output $ serialize $ map toBC c
  