{-|
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 :: forall a b. [a] -> [b] -> (a -> [b]) -> [b]
interMap [a]
xs [b]
y 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 Int
n = Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
4) Char
' '

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

serializeCase :: Show a => Int -> (a, [BC]) -> String
serializeCase :: forall a. Show a => Int -> (a, [BC]) -> String
serializeCase Int
n (a
x, [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]
++ String
":\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 String
"\n" (Int -> BC -> String
serializeBC (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))

serializeDefault :: Int -> [BC] -> String
serializeDefault :: Int -> [BC] -> String
serializeDefault Int
n [BC]
bcs =
  Int -> String
indent Int
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"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 String
"\n" (Int -> BC -> String
serializeBC (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))

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

dumpBC :: [(Name, SDecl)] -> String -> IO ()
dumpBC :: [(Name, SDecl)] -> String -> IO ()
dumpBC [(Name, SDecl)]
c 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