{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Language.Embedded.Signature where

import Data.Proxy

import Language.C.Monad
import Language.Embedded.Expression
import Language.Embedded.Backend.C.Expression

import Language.C.Quote.C


-- * Language

-- | Signature annotations
data Ann exp a where
  Empty  :: Ann exp a
  Native :: (FreePred exp a) => exp len -> Ann exp [a]
  Named  :: String -> Ann exp a

-- | Signatures
data Signature exp pred a where
  Ret    :: pred a => String -> exp a -> Signature exp pred a
  Ptr    :: pred a => String -> exp a -> Signature exp pred a
  Lam    :: pred a => Ann exp a -> (Val a -> Signature exp pred b)
         -> Signature exp pred (a -> b)


-- * Combinators

lam :: (pred a, FreeExp exp, FreePred exp a)
    => (exp a -> Signature exp pred b) -> Signature exp pred (a -> b)
lam :: (exp a -> Signature exp pred b) -> Signature exp pred (a -> b)
lam exp a -> Signature exp pred b
f = Ann exp a
-> (Val a -> Signature exp pred b) -> Signature exp pred (a -> b)
forall (pred :: * -> Constraint) a (exp :: * -> *) b.
pred a =>
Ann exp a
-> (Val a -> Signature exp pred b) -> Signature exp pred (a -> b)
Lam Ann exp a
forall (exp :: * -> *) a. Ann exp a
Empty ((Val a -> Signature exp pred b) -> Signature exp pred (a -> b))
-> (Val a -> Signature exp pred b) -> Signature exp pred (a -> b)
forall a b. (a -> b) -> a -> b
$ \Val a
x -> exp a -> Signature exp pred b
f (Val a -> exp a
forall (exp :: * -> *) a.
(FreeExp exp, FreePred exp a) =>
Val a -> exp a
valToExp Val a
x)

name :: (pred a, FreeExp exp, FreePred exp a)
     => String -> (exp a -> Signature exp pred b) -> Signature exp pred (a -> b)
name :: String
-> (exp a -> Signature exp pred b) -> Signature exp pred (a -> b)
name String
s exp a -> Signature exp pred b
f = Ann exp a
-> (Val a -> Signature exp pred b) -> Signature exp pred (a -> b)
forall (pred :: * -> Constraint) a (exp :: * -> *) b.
pred a =>
Ann exp a
-> (Val a -> Signature exp pred b) -> Signature exp pred (a -> b)
Lam (String -> Ann exp a
forall (exp :: * -> *) a. String -> Ann exp a
Named String
s) ((Val a -> Signature exp pred b) -> Signature exp pred (a -> b))
-> (Val a -> Signature exp pred b) -> Signature exp pred (a -> b)
forall a b. (a -> b) -> a -> b
$ \Val a
x -> exp a -> Signature exp pred b
f (Val a -> exp a
forall (exp :: * -> *) a.
(FreeExp exp, FreePred exp a) =>
Val a -> exp a
valToExp Val a
x)

ret,ptr :: (pred a)
        => String -> exp a -> Signature exp pred a
ret :: String -> exp a -> Signature exp pred a
ret = String -> exp a -> Signature exp pred a
forall (pred :: * -> Constraint) a (exp :: * -> *).
pred a =>
String -> exp a -> Signature exp pred a
Ret
ptr :: String -> exp a -> Signature exp pred a
ptr = String -> exp a -> Signature exp pred a
forall (pred :: * -> Constraint) a (exp :: * -> *).
pred a =>
String -> exp a -> Signature exp pred a
Ptr

arg :: (pred a, FreeExp exp, FreePred exp a)
    => Ann exp a
    -> (exp a -> exp b)
    -> (exp b -> Signature exp pred c)
    -> Signature exp pred (a -> c)
arg :: Ann exp a
-> (exp a -> exp b)
-> (exp b -> Signature exp pred c)
-> Signature exp pred (a -> c)
arg Ann exp a
s exp a -> exp b
g exp b -> Signature exp pred c
f = Ann exp a
-> (Val a -> Signature exp pred c) -> Signature exp pred (a -> c)
forall (pred :: * -> Constraint) a (exp :: * -> *) b.
pred a =>
Ann exp a
-> (Val a -> Signature exp pred b) -> Signature exp pred (a -> b)
Lam Ann exp a
s ((Val a -> Signature exp pred c) -> Signature exp pred (a -> c))
-> (Val a -> Signature exp pred c) -> Signature exp pred (a -> c)
forall a b. (a -> b) -> a -> b
$ \Val a
x -> exp b -> Signature exp pred c
f (exp b -> Signature exp pred c) -> exp b -> Signature exp pred c
forall a b. (a -> b) -> a -> b
$ exp a -> exp b
g (exp a -> exp b) -> exp a -> exp b
forall a b. (a -> b) -> a -> b
$ Val a -> exp a
forall (exp :: * -> *) a.
(FreeExp exp, FreePred exp a) =>
Val a -> exp a
valToExp Val a
x



-- * Compilation

-- | Compile a function @Signature@ to C code
translateFunction :: forall m exp a. (MonadC m, CompExp exp)
                  => Signature exp CType a -> m ()
translateFunction :: Signature exp CType a -> m ()
translateFunction Signature exp CType a
sig = Signature exp CType a -> m () -> m ()
forall d. Signature exp CType d -> m () -> m ()
go Signature exp CType a
sig (() -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
  where
    go :: Signature exp CType d -> m () -> m ()
    go :: Signature exp CType d -> m () -> m ()
go (Ret String
n exp d
a) m ()
prelude = do
      Type
t <- exp d -> m Type
forall a (m :: * -> *) (proxy :: * -> *).
(CType a, MonadC m) =>
proxy a -> m Type
cType exp d
a
      Type -> String -> m () -> m ()
forall (m :: * -> *) a. MonadC m => Type -> String -> m a -> m a
inFunctionTy Type
t String
n (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
        m ()
prelude
        Exp
e <- exp d -> m Exp
forall (exp :: * -> *) (m :: * -> *) a.
(CompExp exp, MonadC m) =>
exp a -> m Exp
compExp exp d
a
        Stm -> m ()
forall (m :: * -> *). MonadC m => Stm -> m ()
addStm [cstm| return $e; |]
    go (Ptr String
n exp d
a) m ()
prelude = do
      Type
t <- exp d -> m Type
forall a (m :: * -> *) (proxy :: * -> *).
(CType a, MonadC m) =>
proxy a -> m Type
cType exp d
a
      String -> m () -> m ()
forall (m :: * -> *) a. MonadC m => String -> m a -> m a
inFunction String
n (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
        m ()
prelude
        Exp
e <- exp d -> m Exp
forall (exp :: * -> *) (m :: * -> *) a.
(CompExp exp, MonadC m) =>
exp a -> m Exp
compExp exp d
a
        Param -> m ()
forall (m :: * -> *). MonadC m => Param -> m ()
addParam [cparam| $ty:t *out |]
        Stm -> m ()
forall (m :: * -> *). MonadC m => Stm -> m ()
addStm [cstm| *out = $e; |]
    go fun :: Signature exp CType d
fun@(Lam Ann exp a
Empty Val a -> Signature exp CType b
f) m ()
prelude = do
      Type
t <- Proxy a -> m Type
forall a (m :: * -> *) (proxy :: * -> *).
(CType a, MonadC m) =>
proxy a -> m Type
cType (Signature exp CType (a -> b) -> Proxy a
forall (exp :: * -> *) (pred :: * -> Constraint) b c.
Signature exp pred (b -> c) -> Proxy b
argProxy Signature exp CType d
Signature exp CType (a -> b)
fun)
      Val a
v <- Proxy CType -> m (Val a)
forall (m :: * -> *) (ct :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *) a.
(MonadC m, CompTypeClass ct, ct a) =>
proxy ct -> m (Val a)
freshVar (Proxy CType
forall k (t :: k). Proxy t
Proxy :: Proxy CType)
      Signature exp CType b -> m () -> m ()
forall d. Signature exp CType d -> m () -> m ()
go (Val a -> Signature exp CType b
f Val a
v) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ m ()
prelude m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Param -> m ()
forall (m :: * -> *). MonadC m => Param -> m ()
addParam [cparam| $ty:t $id:v |]
    go fun :: Signature exp CType d
fun@(Lam n :: Ann exp a
n@(Native exp len
l) Val a -> Signature exp CType b
f) m ()
prelude = do
      Type
t <- Ann exp a -> m Type
forall a (m :: * -> *) (proxy :: * -> *).
(CType a, MonadC m) =>
proxy a -> m Type
cType Ann exp a
n
      Integer
i <- m Integer
forall (m :: * -> *). MonadC m => m Integer
freshId
      let vi :: String
vi = Char
'v' Char -> String -> String
forall a. a -> [a] -> [a]
: Integer -> String
forall a. Show a => a -> String
show Integer
i
      let w :: Val a
w = String -> Val a
forall a. String -> Val a
ValComp String
vi
      let n :: String
n = String
vi String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_buf"
      Integer -> String -> m () -> m ()
forall (m :: * -> *) a. MonadC m => Integer -> String -> m a -> m a
withAlias Integer
i (Char
'&'Char -> String -> String
forall a. a -> [a] -> [a]
:String
vi) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Signature exp CType b -> m () -> m ()
forall d. Signature exp CType d -> m () -> m ()
go (Val a -> Signature exp CType b
f Val a
w) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
        m ()
prelude
        Exp
len <- exp len -> m Exp
forall (exp :: * -> *) (m :: * -> *) a.
(CompExp exp, MonadC m) =>
exp a -> m Exp
compExp exp len
l
        InitGroup -> m ()
forall (m :: * -> *). MonadC m => InitGroup -> m ()
addLocal [cdecl| struct array $id:vi = { .buffer = $id:n
                                               , .length=$len
                                               , .elemSize=sizeof($ty:t)
                                               , .bytes=sizeof($ty:t)*$len
                                               }; |]
        Param -> m ()
forall (m :: * -> *). MonadC m => Param -> m ()
addParam [cparam| $ty:t * $id:n |]
    go fun :: Signature exp CType d
fun@(Lam (Named String
s) Val a -> Signature exp CType b
f) m ()
prelude = do
      Type
t <- Proxy a -> m Type
forall a (m :: * -> *) (proxy :: * -> *).
(CType a, MonadC m) =>
proxy a -> m Type
cType (Signature exp CType (a -> b) -> Proxy a
forall (exp :: * -> *) (pred :: * -> Constraint) b c.
Signature exp pred (b -> c) -> Proxy b
argProxy Signature exp CType d
Signature exp CType (a -> b)
fun)
      Integer
i <- m Integer
forall (m :: * -> *). MonadC m => m Integer
freshId
      let w :: Val a
w = String -> Val a
forall a. String -> Val a
ValComp (Char
'v' Char -> String -> String
forall a. a -> [a] -> [a]
: Integer -> String
forall a. Show a => a -> String
show Integer
i)
      Integer -> String -> m () -> m ()
forall (m :: * -> *) a. MonadC m => Integer -> String -> m a -> m a
withAlias Integer
i String
s (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Signature exp CType b -> m () -> m ()
forall d. Signature exp CType d -> m () -> m ()
go (Val a -> Signature exp CType b
f Val a
w) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ m ()
prelude m () -> m () -> m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Param -> m ()
forall (m :: * -> *). MonadC m => Param -> m ()
addParam [cparam| $ty:t $id:s |]

argProxy :: Signature exp pred (b -> c) -> Proxy b
argProxy :: Signature exp pred (b -> c) -> Proxy b
argProxy Signature exp pred (b -> c)
_ = Proxy b
forall k (t :: k). Proxy t
Proxy