{-|
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 :: [a] -> [b] -> (a -> [b]) -> [b]
interMap xs :: [a]
xs y :: [b]
y f :: a -> [b]
f = [[b]] -> [b]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([b] -> [[b]] -> [[b]]
forall a. a -> [a] -> [a]
intersperse [b]
y ((a -> [b]) -> [a] -> [[b]]
forall a b. (a -> b) -> [a] -> [b]
map a -> [b]
f [a]
xs))

indent :: Int -> String
indent :: Int -> String
indent n :: Int
n = Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
*4) ' '

serializeReg :: Reg -> String
serializeReg :: Reg -> String
serializeReg (L n :: Int
n) = "L" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
serializeReg (T n :: Int
n) = "T" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
serializeReg r :: Reg
r = Reg -> String
forall a. Show a => a -> String
show Reg
r

serializeCase :: Show a => Int -> (a, [BC]) -> String
serializeCase :: Int -> (a, [BC]) -> String
serializeCase n :: Int
n (x :: a
x, bcs :: [BC]
bcs) =
  Int -> String
indent Int
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ ":\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [BC] -> String -> (BC -> String) -> String
forall a b. [a] -> [b] -> (a -> [b]) -> [b]
interMap [BC]
bcs "\n" (Int -> BC -> String
serializeBC (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1))

serializeDefault :: Int -> [BC] -> String
serializeDefault :: Int -> [BC] -> String
serializeDefault n :: Int
n bcs :: [BC]
bcs =
  Int -> String
indent Int
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ "default:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [BC] -> String -> (BC -> String) -> String
forall a b. [a] -> [b] -> (a -> [b]) -> [b]
interMap [BC]
bcs "\n" (Int -> BC -> String
serializeBC (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1))

serializeBC :: Int -> BC -> String
serializeBC :: Int -> BC -> String
serializeBC n :: Int
n bc :: BC
bc = Int -> String
indent Int
n String -> String -> String
forall a. [a] -> [a] -> [a]
++
    case BC
bc of
      ASSIGN a :: Reg
a b :: Reg
b ->
        "ASSIGN " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Reg -> String
serializeReg Reg
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Reg -> String
serializeReg Reg
b
      ASSIGNCONST a :: Reg
a b :: Const
b ->
        "ASSIGNCONST " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Reg -> String
serializeReg Reg
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Const -> String
forall a. Show a => a -> String
show Const
b
      UPDATE a :: Reg
a b :: Reg
b ->
        "UPDATE " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Reg -> String
serializeReg Reg
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Reg -> String
serializeReg Reg
b
      MKCON a :: Reg
a Nothing b :: Int
b xs :: [Reg]
xs ->
        "MKCON " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Reg -> String
serializeReg Reg
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ " [" String -> String -> String
forall a. [a] -> [a] -> [a]
++ ([Reg] -> String -> (Reg -> String) -> String
forall a b. [a] -> [b] -> (a -> [b]) -> [b]
interMap [Reg]
xs ", " Reg -> String
serializeReg) String -> String -> String
forall a. [a] -> [a] -> [a]
++ "]"
      MKCON a :: Reg
a (Just r :: Reg
r) b :: Int
b xs :: [Reg]
xs ->
        "MKCON@" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Reg -> String
serializeReg Reg
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Reg -> String
serializeReg Reg
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ " [" String -> String -> String
forall a. [a] -> [a] -> [a]
++ ([Reg] -> String -> (Reg -> String) -> String
forall a b. [a] -> [b] -> (a -> [b]) -> [b]
interMap [Reg]
xs ", " Reg -> String
serializeReg) String -> String -> String
forall a. [a] -> [a] -> [a]
++ "]"
      CASE safe :: Bool
safe r :: Reg
r cases :: [(Int, [BC])]
cases def :: Maybe [BC]
def ->
        "CASE " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Reg -> String
serializeReg Reg
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ ":\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Int, [BC])] -> String -> ((Int, [BC]) -> String) -> String
forall a b. [a] -> [b] -> (a -> [b]) -> [b]
interMap [(Int, [BC])]
cases "\n" (Int -> (Int, [BC]) -> String
forall a. Show a => Int -> (a, [BC]) -> String
serializeCase (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)) String -> String -> String
forall a. [a] -> [a] -> [a]
++
        String -> ([BC] -> String) -> Maybe [BC] -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "" (\def' :: [BC]
def' -> "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> [BC] -> String
serializeDefault (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) [BC]
def') Maybe [BC]
def
      PROJECT a :: Reg
a b :: Int
b c :: Int
c ->
        "PROJECT " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Reg -> String
serializeReg Reg
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
c
      PROJECTINTO a :: Reg
a b :: Reg
b c :: Int
c ->
        "PROJECTINTO " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Reg -> String
serializeReg Reg
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Reg -> String
serializeReg Reg
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
c
      CONSTCASE r :: Reg
r cases :: [(Const, [BC])]
cases def :: Maybe [BC]
def ->
        "CONSTCASE " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Reg -> String
serializeReg Reg
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ ":\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Const, [BC])] -> String -> ((Const, [BC]) -> String) -> String
forall a b. [a] -> [b] -> (a -> [b]) -> [b]
interMap [(Const, [BC])]
cases "\n" (Int -> (Const, [BC]) -> String
forall a. Show a => Int -> (a, [BC]) -> String
serializeCase (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)) String -> String -> String
forall a. [a] -> [a] -> [a]
++
        String -> ([BC] -> String) -> Maybe [BC] -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "" (\def' :: [BC]
def' -> "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> [BC] -> String
serializeDefault (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) [BC]
def') Maybe [BC]
def
      CALL x :: Name
x -> "CALL " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
x
      TAILCALL x :: Name
x -> "TAILCALL " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
x
      FOREIGNCALL r :: Reg
r ret :: FDesc
ret name :: FDesc
name args :: [(FDesc, Reg)]
args ->
        "FOREIGNCALL " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Reg -> String
serializeReg Reg
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ " \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ FDesc -> String
forall a. Show a => a -> String
show FDesc
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FDesc -> String
forall a. Show a => a -> String
show FDesc
ret String -> String -> String
forall a. [a] -> [a] -> [a]
++
        " [" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(FDesc, Reg)] -> String -> ((FDesc, Reg) -> String) -> String
forall a b. [a] -> [b] -> (a -> [b]) -> [b]
interMap [(FDesc, Reg)]
args ", " (\(ty :: FDesc
ty, r :: Reg
r) -> Reg -> String
serializeReg Reg
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ " : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FDesc -> String
forall a. Show a => a -> String
show FDesc
ty) String -> String -> String
forall a. [a] -> [a] -> [a]
++ "]"
      SLIDE n :: Int
n -> "SLIDE " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
      REBASE -> "REBASE"
      RESERVE n :: Int
n -> "RESERVE " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
      RESERVENOALLOC n :: Int
n -> "RESERVENOALLOC " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
      ADDTOP n :: Int
n -> "ADDTOP " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
      TOPBASE n :: Int
n -> "TOPBASE " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
      BASETOP n :: Int
n -> "BASETOP " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
      STOREOLD -> "STOREOLD"
      OP a :: Reg
a b :: PrimFn
b c :: [Reg]
c ->
        "OP " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Reg -> String
serializeReg Reg
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PrimFn -> String
forall a. Show a => a -> String
show PrimFn
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ " [" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Reg] -> String -> (Reg -> String) -> String
forall a b. [a] -> [b] -> (a -> [b]) -> [b]
interMap [Reg]
c ", " Reg -> String
serializeReg String -> String -> String
forall a. [a] -> [a] -> [a]
++ "]"
      NULL r :: Reg
r -> "NULL " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Reg -> String
serializeReg Reg
r
      ERROR s :: String
s -> "ERROR \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\"" -- FIXME: s may contain quotes
                                         -- Issue #1596
serialize :: [(Name, [BC])] -> String
serialize :: [(Name, [BC])] -> String
serialize decls :: [(Name, [BC])]
decls =
    [(Name, [BC])] -> String -> ((Name, [BC]) -> String) -> String
forall a b. [a] -> [b] -> (a -> [b]) -> [b]
interMap [(Name, [BC])]
decls "\n\n" (Name, [BC]) -> String
serializeDecl
  where
    serializeDecl :: (Name, [BC]) -> String
    serializeDecl :: (Name, [BC]) -> String
serializeDecl (name :: Name
name, bcs :: [BC]
bcs) =
      Name -> String
forall a. Show a => a -> String
show Name
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ ":\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [BC] -> String -> (BC -> String) -> String
forall a b. [a] -> [b] -> (a -> [b]) -> [b]
interMap [BC]
bcs "\n" (Int -> BC -> String
serializeBC 1)

dumpBC :: [(Name, SDecl)] -> String -> IO ()
dumpBC :: [(Name, SDecl)] -> String -> IO ()
dumpBC c :: [(Name, SDecl)]
c output :: String
output = String -> String -> IO ()
writeFile String
output (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [(Name, [BC])] -> String
serialize ([(Name, [BC])] -> String) -> [(Name, [BC])] -> String
forall a b. (a -> b) -> a -> b
$ ((Name, SDecl) -> (Name, [BC]))
-> [(Name, SDecl)] -> [(Name, [BC])]
forall a b. (a -> b) -> [a] -> [b]
map (Name, SDecl) -> (Name, [BC])
toBC [(Name, SDecl)]
c