----------------------------------------------------------------------------
-- |
-- Module      :  Data.Emacs.Module.Args
-- Copyright   :  (c) Sergey Vinokurov 2018
-- License     :  Apache-2.0 (see LICENSE)
-- Maintainer  :  serg.foo@gmail.com
----------------------------------------------------------------------------

{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE UndecidableInstances   #-}

module Data.Emacs.Module.Args
  ( Nat(..)
  , EmacsArgs
  , EmacsInvocation(..)
  , GetArities(..)

    -- * Argument inference
  , R(..)
  , O(..)
  , Rest(..)
  , Stop(..)
  ) where

import Control.Monad.Base

import Data.Kind
import Data.Proxy
import Foreign
import Foreign.C.Types (CPtrdiff)

import Data.Emacs.Module.Raw.Env (variadicFunctionArgs)
import Data.Emacs.Module.Raw.Value

-- | Type-level Peano numbers.
--
-- Indented to be used with @DataKinds@ extension enabled.
data Nat = Z | S Nat

class NatValue (n :: Nat) where
  natValue :: Proxy n -> Int

instance NatValue 'Z where
  {-# INLINE natValue #-}
  natValue :: Proxy 'Z -> Int
natValue Proxy 'Z
_ = Int
0

instance forall n. NatValue n => NatValue ('S n) where
  {-# INLINE natValue #-}
  natValue :: Proxy ('S n) -> Int
natValue Proxy ('S n)
_ = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Proxy n -> Int
forall (n :: Nat). NatValue n => Proxy n -> Int
natValue (forall {k} (t :: k). Proxy t
forall (t :: Nat). Proxy t
Proxy @n)

-- | Required argument of an exported function.
data R a b = R !a !b

-- | Optional argument of an exported function.
data O a b = O !(Maybe a) !b

-- | All other arguments of an exported function as a list.
newtype Rest a = Rest [a]

-- | End of argument list of an exported funciton.
data Stop a = Stop

-- | Specification of the arguments that exposed functions can receive from Emacs.
--
-- This type family allows to declaratively specify how many required and
-- optional arguments a function can take and whether it accepts rest arguments.
-- It's a direct translation of argument lists in Emacs lisp, e.g.
--
-- > (defun foo (x y z &optional w t &rest quux)
-- >   (+ (* x y z) (* (or w 1) (or t 2)) (length quux)))
--
-- The function above has 3 required arguments, 2 optional and also has
-- rest arguments. The type family below has two 'Nat's and one 'Bool'
-- to provide that info.
type family EmacsArgs (req :: Nat) (opt :: Nat) (rest :: Bool) (a :: Type) = (r :: Type) | r -> req opt rest a where
  EmacsArgs ('S n) opt    rest   a = R a (EmacsArgs n  opt rest a)
  EmacsArgs 'Z     ('S k) rest   a = O a (EmacsArgs 'Z k   rest a)
  EmacsArgs 'Z     'Z     'True  a = Rest a
  EmacsArgs 'Z     'Z     'False a = Stop a

class EmacsInvocation req opt rest where
  supplyEmacsArgs
    :: MonadBase IO m
    => Int
    -> Ptr (RawValue 'Regular)
    -> (RawValue 'Regular -> m a)
    -> (EmacsArgs req opt rest a -> m b)
    -> m b

instance EmacsInvocation 'Z 'Z 'False where
  {-# INLINE supplyEmacsArgs #-}
  supplyEmacsArgs :: forall (m :: * -> *) a b.
MonadBase IO m =>
Int
-> Ptr (RawValue 'Regular)
-> (RawValue 'Regular -> m a)
-> (EmacsArgs 'Z 'Z 'False a -> m b)
-> m b
supplyEmacsArgs Int
_nargs Ptr (RawValue 'Regular)
_startPtr RawValue 'Regular -> m a
_mkInput EmacsArgs 'Z 'Z 'False a -> m b
f = EmacsArgs 'Z 'Z 'False a -> m b
f EmacsArgs 'Z 'Z 'False a
Stop a
forall {k} (a :: k). Stop a
Stop

instance EmacsInvocation 'Z 'Z 'True where
  {-# INLINE supplyEmacsArgs #-}
  supplyEmacsArgs
    :: MonadBase IO m
    => Int
    -> Ptr (RawValue 'Regular)
    -> (RawValue 'Regular -> m a)
    -> (Rest a -> m b)
    -> m b
  supplyEmacsArgs :: forall (m :: * -> *) a b.
MonadBase IO m =>
Int
-> Ptr (RawValue 'Regular)
-> (RawValue 'Regular -> m a)
-> (Rest a -> m b)
-> m b
supplyEmacsArgs Int
nargs Ptr (RawValue 'Regular)
startPtr RawValue 'Regular -> m a
mkArg Rest a -> m b
f =
    case Int
nargs of
      Int
0 -> Rest a -> m b
f ([a] -> Rest a
forall a. [a] -> Rest a
Rest [])
      Int
n -> Rest a -> m b
f (Rest a -> m b) -> ([a] -> Rest a) -> [a] -> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Rest a
forall a. [a] -> Rest a
Rest ([a] -> m b) -> m [a] -> m b
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (RawValue 'Regular -> m a) -> [RawValue 'Regular] -> m [a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse RawValue 'Regular -> m a
mkArg ([RawValue 'Regular] -> m [a]) -> m [RawValue 'Regular] -> m [a]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO [RawValue 'Regular] -> m [RawValue 'Regular]
forall α. IO α -> m α
forall (b :: * -> *) (m :: * -> *) α. MonadBase b m => b α -> m α
liftBase (Int -> Ptr (RawValue 'Regular) -> IO [RawValue 'Regular]
forall a. Storable a => Int -> Ptr a -> IO [a]
peekArray Int
n Ptr (RawValue 'Regular)
startPtr)

{-# INLINE advanceEmacsValuePtr #-}
advanceEmacsValuePtr :: forall p. Ptr (RawValue p) -> Ptr (RawValue p)
advanceEmacsValuePtr :: forall (p :: Pinning). Ptr (RawValue p) -> Ptr (RawValue p)
advanceEmacsValuePtr =
  (Ptr (RawValue p) -> Int -> Ptr (RawValue p)
forall a b. Ptr a -> Int -> Ptr b
`plusPtr` (RawValue p -> Int
forall a. Storable a => a -> Int
sizeOf (RawValue p
forall a. HasCallStack => a
undefined :: RawValue p)))

instance EmacsInvocation 'Z n rest => EmacsInvocation 'Z ('S n) rest where
  {-# INLINE supplyEmacsArgs #-}
  supplyEmacsArgs
    :: forall m a b. MonadBase IO m
    => Int
    -> Ptr (RawValue 'Regular)
    -> (RawValue 'Regular -> m a)
    -> (O a (EmacsArgs 'Z n rest a) -> m b)
    -> m b
  supplyEmacsArgs :: forall (m :: * -> *) a b.
MonadBase IO m =>
Int
-> Ptr (RawValue 'Regular)
-> (RawValue 'Regular -> m a)
-> (O a (EmacsArgs 'Z n rest a) -> m b)
-> m b
supplyEmacsArgs Int
nargs Ptr (RawValue 'Regular)
startPtr RawValue 'Regular -> m a
mkArg O a (EmacsArgs 'Z n rest a) -> m b
f =
    case Int
nargs of
      Int
0 -> Int
-> Ptr (RawValue 'Regular)
-> (RawValue 'Regular -> m a)
-> (EmacsArgs 'Z n rest a -> m b)
-> m b
forall (req :: Nat) (opt :: Nat) (rest :: Bool) (m :: * -> *) a b.
(EmacsInvocation req opt rest, MonadBase IO m) =>
Int
-> Ptr (RawValue 'Regular)
-> (RawValue 'Regular -> m a)
-> (EmacsArgs req opt rest a -> m b)
-> m b
forall (m :: * -> *) a b.
MonadBase IO m =>
Int
-> Ptr (RawValue 'Regular)
-> (RawValue 'Regular -> m a)
-> (EmacsArgs 'Z n rest a -> m b)
-> m b
supplyEmacsArgs Int
nargs Ptr (RawValue 'Regular)
startPtr RawValue 'Regular -> m a
mkArg (O a (EmacsArgs 'Z n rest a) -> m b
f (O a (EmacsArgs 'Z n rest a) -> m b)
-> (EmacsArgs 'Z n rest a -> O a (EmacsArgs 'Z n rest a))
-> EmacsArgs 'Z n rest a
-> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe a -> EmacsArgs 'Z n rest a -> O a (EmacsArgs 'Z n rest a)
forall a b. Maybe a -> b -> O a b
O Maybe a
forall a. Maybe a
Nothing)
      Int
_ -> do
        a
arg <- RawValue 'Regular -> m a
mkArg (RawValue 'Regular -> m a) -> m (RawValue 'Regular) -> m a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO (RawValue 'Regular) -> m (RawValue 'Regular)
forall α. IO α -> m α
forall (b :: * -> *) (m :: * -> *) α. MonadBase b m => b α -> m α
liftBase (Ptr (RawValue 'Regular) -> IO (RawValue 'Regular)
forall a. Storable a => Ptr a -> IO a
peek Ptr (RawValue 'Regular)
startPtr)
        Int
-> Ptr (RawValue 'Regular)
-> (RawValue 'Regular -> m a)
-> (EmacsArgs 'Z n rest a -> m b)
-> m b
forall (req :: Nat) (opt :: Nat) (rest :: Bool) (m :: * -> *) a b.
(EmacsInvocation req opt rest, MonadBase IO m) =>
Int
-> Ptr (RawValue 'Regular)
-> (RawValue 'Regular -> m a)
-> (EmacsArgs req opt rest a -> m b)
-> m b
forall (m :: * -> *) a b.
MonadBase IO m =>
Int
-> Ptr (RawValue 'Regular)
-> (RawValue 'Regular -> m a)
-> (EmacsArgs 'Z n rest a -> m b)
-> m b
supplyEmacsArgs
          (Int
nargs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
          (Ptr (RawValue 'Regular) -> Ptr (RawValue 'Regular)
forall (p :: Pinning). Ptr (RawValue p) -> Ptr (RawValue p)
advanceEmacsValuePtr Ptr (RawValue 'Regular)
startPtr)
          RawValue 'Regular -> m a
mkArg
          (O a (EmacsArgs 'Z n rest a) -> m b
f (O a (EmacsArgs 'Z n rest a) -> m b)
-> (EmacsArgs 'Z n rest a -> O a (EmacsArgs 'Z n rest a))
-> EmacsArgs 'Z n rest a
-> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe a -> EmacsArgs 'Z n rest a -> O a (EmacsArgs 'Z n rest a)
forall a b. Maybe a -> b -> O a b
O (a -> Maybe a
forall a. a -> Maybe a
Just a
arg))

instance EmacsInvocation n opt rest => EmacsInvocation ('S n) opt rest where
  {-# INLINE supplyEmacsArgs #-}
  supplyEmacsArgs
    :: MonadBase IO m
    => Int
    -> Ptr (RawValue 'Regular)
    -> (RawValue 'Regular -> m a)
    -> (R a (EmacsArgs n opt rest a) -> m b)
    -> m b
  supplyEmacsArgs :: forall (m :: * -> *) a b.
MonadBase IO m =>
Int
-> Ptr (RawValue 'Regular)
-> (RawValue 'Regular -> m a)
-> (R a (EmacsArgs n opt rest a) -> m b)
-> m b
supplyEmacsArgs Int
nargs Ptr (RawValue 'Regular)
startPtr RawValue 'Regular -> m a
mkArg R a (EmacsArgs n opt rest a) -> m b
f = do
    a
arg <- RawValue 'Regular -> m a
mkArg (RawValue 'Regular -> m a) -> m (RawValue 'Regular) -> m a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO (RawValue 'Regular) -> m (RawValue 'Regular)
forall α. IO α -> m α
forall (b :: * -> *) (m :: * -> *) α. MonadBase b m => b α -> m α
liftBase (Ptr (RawValue 'Regular) -> IO (RawValue 'Regular)
forall a. Storable a => Ptr a -> IO a
peek Ptr (RawValue 'Regular)
startPtr)
    Int
-> Ptr (RawValue 'Regular)
-> (RawValue 'Regular -> m a)
-> (EmacsArgs n opt rest a -> m b)
-> m b
forall (req :: Nat) (opt :: Nat) (rest :: Bool) (m :: * -> *) a b.
(EmacsInvocation req opt rest, MonadBase IO m) =>
Int
-> Ptr (RawValue 'Regular)
-> (RawValue 'Regular -> m a)
-> (EmacsArgs req opt rest a -> m b)
-> m b
forall (m :: * -> *) a b.
MonadBase IO m =>
Int
-> Ptr (RawValue 'Regular)
-> (RawValue 'Regular -> m a)
-> (EmacsArgs n opt rest a -> m b)
-> m b
supplyEmacsArgs (Int
nargs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Ptr (RawValue 'Regular) -> Ptr (RawValue 'Regular)
forall (p :: Pinning). Ptr (RawValue p) -> Ptr (RawValue p)
advanceEmacsValuePtr Ptr (RawValue 'Regular)
startPtr) RawValue 'Regular -> m a
mkArg (R a (EmacsArgs n opt rest a) -> m b
f (R a (EmacsArgs n opt rest a) -> m b)
-> (EmacsArgs n opt rest a -> R a (EmacsArgs n opt rest a))
-> EmacsArgs n opt rest a
-> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> EmacsArgs n opt rest a -> R a (EmacsArgs n opt rest a)
forall a b. a -> b -> R a b
R a
arg)


-- | Helper to retrieve number of arguments a function takes for Emacs.
class GetArities (req :: Nat) (opt :: Nat) (rest :: Bool) where
  arities :: Proxy req -> Proxy opt -> Proxy rest -> (CPtrdiff, CPtrdiff)

instance (NatValue req, NatValue opt) => GetArities req opt 'False where
  {-# INLINE arities #-}
  arities :: Proxy req -> Proxy opt -> Proxy 'False -> (CPtrdiff, CPtrdiff)
arities Proxy req
preq Proxy opt
popt Proxy 'False
_ = (CPtrdiff
req, CPtrdiff
req CPtrdiff -> CPtrdiff -> CPtrdiff
forall a. Num a => a -> a -> a
+ CPtrdiff
opt)
    where
      req :: CPtrdiff
req = Int -> CPtrdiff
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy req -> Int
forall (n :: Nat). NatValue n => Proxy n -> Int
natValue Proxy req
preq)
      opt :: CPtrdiff
opt = Int -> CPtrdiff
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy opt -> Int
forall (n :: Nat). NatValue n => Proxy n -> Int
natValue Proxy opt
popt)

instance NatValue req => GetArities req opt 'True where
  {-# INLINE arities #-}
  arities :: Proxy req -> Proxy opt -> Proxy 'True -> (CPtrdiff, CPtrdiff)
arities Proxy req
preq Proxy opt
_ Proxy 'True
_ =
    (Int -> CPtrdiff
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy req -> Int
forall (n :: Nat). NatValue n => Proxy n -> Int
natValue Proxy req
preq), CPtrdiff
variadicFunctionArgs)


-- data Args (req :: Nat) (opt :: Nat) (rest :: Bool) (a :: Type) where
--   NoArgs   ::                                   Args 'Z       'Z       'False a
--   ReqArg   :: a       -> Args req opt rest a -> Args ('S req) opt      rest   a
--   OptArg   :: Maybe a -> Args req opt rest a -> Args req      ('S opt) rest   a
--   RestArgs :: [a]                            -> Args 'Z       'Z       'True  a
--
-- deriving instance Functor     (Args req opt rest)
-- deriving instance Foldable    (Args req opt rest)
-- deriving instance Traversable (Args req opt rest)

-- class GetArgs (req :: Nat) (opt :: Nat) (rest :: Bool) where
--   getArgs :: Storable a => Int -> Ptr a -> IO (Args req opt rest a)
--
-- instance GetArgs 'Z 'Z 'False where
--   {-# INLINE getArgs #-}
--   getArgs !_nargs _startPtr = pure NoArgs
--
-- instance GetArgs 'Z 'Z 'True where
--   {-# INLINE getArgs #-}
--   getArgs !nargs startPtr =
--     case nargs of
--       0 -> pure $ RestArgs []
--       n -> RestArgs <$> peekArray n startPtr
--
-- instance (GetArgs req n rest, DefaultArgs req n rest) => GetArgs req ('S n) rest where
--   {-# INLINE getArgs #-}
--   getArgs :: forall a. Storable a => Int -> Ptr a -> IO (Args req ('S n) rest a)
--   getArgs !nargs startPtr = do
--     case nargs of
--       0 -> pure $ OptArg Nothing defaultArgs
--       _ -> OptArg <$> (Just <$> peek startPtr) <*> getArgs (nargs - 1) (plusPtr startPtr (sizeOf (undefined :: a)))
--
-- instance GetArgs n opt rest => GetArgs ('S n) opt rest where
--   {-# INLINE getArgs #-}
--   getArgs :: forall a. Storable a => Int -> Ptr a -> IO (Args ('S n) opt rest a)
--   getArgs !nargs startPtr = do
--     ReqArg <$> peek startPtr <*> getArgs (nargs - 1) (plusPtr startPtr (sizeOf (undefined :: a)))
--
--
-- class DefaultArgs (req :: Nat) (opt :: Nat) (rest :: Bool) where
--   defaultArgs :: Args req opt rest a
--
-- instance DefaultArgs 'Z 'Z 'False where
--   {-# INLINE defaultArgs #-}
--   defaultArgs = NoArgs
--
-- instance DefaultArgs 'Z 'Z 'True where
--   {-# INLINE defaultArgs #-}
--   defaultArgs = RestArgs []
--
-- instance DefaultArgs req n rest => DefaultArgs req ('S n) rest where
--   {-# INLINE defaultArgs #-}
--   defaultArgs = OptArg Nothing defaultArgs