{-# LANGUAGE ConstraintKinds           #-}
{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ExplicitNamespaces        #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE IncoherentInstances       #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE PolyKinds                 #-}
{-# LANGUAGE Rank2Types                #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE TypeInType                #-}
{-# LANGUAGE TypeOperators             #-}
{-# LANGUAGE UndecidableInstances      #-}
{-# LANGUAGE UndecidableSuperClasses   #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Test.StateMachine.Types
-- Copyright   :  (C) 2017, ATS Advanced Telematic Systems GmbH
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Stevan Andjelkovic <stevan@advancedtelematic.com>
-- Stability   :  provisional
-- Portability :  non-portable (GHC extensions)
--
-- This module contains the main types exposed to the user. The module
-- is perhaps best read indirectly, on a per need basis, via the main
-- module "Test.StateMachine".
--
-----------------------------------------------------------------------------

module Test.StateMachine.Types
  ( StateMachineModel(..)
  , ShowCmd
  , showCmd
  , Signature
  , Response(..)
  , SResponse(..)
  , Response_
  , GetResponse_
  , HasResponse
  , response
  , CommandConstraint
  , Untyped(..)
  , RefPlaceholder
  -- * Indexed variant of 'Functor', 'Foldable' and 'Traversable'.
  , Ex(..)
  , IxFunctor
  , ifmap
  , IxFoldable
  , ifoldMap
  , itoList
  , iany
  , IxTraversable
  , itraverse
  , ifor
  -- * Indexed variants of some 'constraints' package combinators.
  , IxForallF
  , Ords
  , Ords'
  , iinstF
  -- * Re-export
  , (\\)
  , type (@@)
  , Property
  , property
  , Proxy(..)
  ) where

import           Data.Constraint
import           Data.Constraint.Forall
import           Data.Kind
                   (Type)
import           Data.Proxy
                   (Proxy(..))
import           Data.Singletons.Prelude
                   (type (@@), Apply, ConstSym1, Sing, TyFun)
import           Data.Singletons.TH
                   (DemoteRep, SDecide, SingKind)
import           Data.Typeable
                   (Typeable)
import           Test.QuickCheck.Property
                   (Property, property)

import           Test.StateMachine.Internal.Types.IntRef

------------------------------------------------------------------------

-- | A state machine based model.
data StateMachineModel model cmd = StateMachineModel
  { precondition :: forall refs resp. IxForallF Ord refs =>
      model refs -> cmd refs resp -> Bool
  , postcondition :: forall refs resp. IxForallF Ord refs =>
      model refs -> cmd refs resp -> Response_ refs resp -> Property
  , transition    :: forall refs resp. IxForallF Ord refs =>
      model refs -> cmd refs resp -> Response_ refs resp -> model refs
  , initialModel  :: forall refs. model refs
  }

-- | Given a command, how can we show it?
class ShowCmd (cmd :: Signature ix) where

  -- | How to show a typed command with internal refereces.
  showCmd :: forall resp. cmd (ConstSym1 String) resp -> String

------------------------------------------------------------------------

-- | Signatures of commands contain a family of references and a
--   response type.
type Signature ix = (TyFun ix Type -> Type) -> Response ix -> Type

------------------------------------------------------------------------

-- | A response of a command is either of some type or a referece at
--   some index.
data Response ix
  = Response Type
  | Reference ix

-- | The singleton type of responses.
data SResponse ix :: Response ix -> Type where
  SResponse  ::                     SResponse ix ('Response  t)
  SReference :: Sing (i :: ix)   -> SResponse ix ('Reference i)

-- | Given a command, what kind of response does it have?
class HasResponse cmd where

  -- | What type of response a typed command has.
  response :: cmd refs resp -> SResponse ix resp

-- | Type-level function that returns a response type.
type family Response_ (refs :: TyFun ix Type -> Type)
                      (resp :: Response ix) :: Type where
  Response_ refs ('Response  t) = t
  Response_ refs ('Reference i) = refs @@ i

-- | Type-level function that maybe returns a response.
type family GetResponse_ (resp :: Response ix) :: k where
  GetResponse_ ('Response  t) = t
  GetResponse_ ('Reference i) = ()

------------------------------------------------------------------------

-- | The constraints on commands (and their indices) that the
--   'Test.StateMachine.sequentialProperty' and
--   'Test.StateMachine.parallelProperty' helpers require.
type CommandConstraint ix cmd =
  ( Ord       ix
  , SDecide   ix
  , SingKind  ix
  , DemoteRep ix ~ ix
  , ShowCmd       cmd
  , IxTraversable cmd
  , HasResponse   cmd
  )

------------------------------------------------------------------------

-- | Untyped commands are command where we hide the response type. This
--   is used in generation of commands.
data Untyped (f :: Signature ix) refs where
  Untyped :: ( Show     (GetResponse_ resp)
             , Typeable (Response_ ConstIntRef resp)
             , Typeable resp
             ) => f refs resp -> Untyped f refs

------------------------------------------------------------------------

-- | When generating commands it is enough to provide a reference
--   placeholder.
data RefPlaceholder ix :: (TyFun ix k) -> Type

type instance Apply (RefPlaceholder _) i = Sing i

------------------------------------------------------------------------

-- | Dependent pairs.
data Ex (p :: TyFun a Type -> Type) = forall (x :: a). Ex (Sing x) (p @@ x)

-- | Predicate transformers.
class IxFunctor (f :: (TyFun ix Type -> Type) -> jx -> Type) where

  -- | Indexed 'fmap'.
  ifmap
    :: forall p q j. (forall i. Sing (i :: ix) -> p @@ i -> q @@ i)
    -> f p j -> f q j

-- | Foldable for predicate transformers.
class IxFoldable (t :: (TyFun ix Type -> Type) -> jx -> Type) where

  -- | Indexed 'foldMap'.
  ifoldMap :: Monoid m => (forall i. Sing (i :: ix) -> p @@ i -> m) -> t p j -> m

  -- | Indexed 'toList'.
  itoList :: t p j -> [Ex p]
  itoList = ifoldMap (\s px -> [Ex s px])

  -- | Indexed 'foldr'.
  ifoldr :: (forall i. Sing (i :: ix) -> p @@ i -> b -> b) -> b -> t p j -> b
  ifoldr f z = foldr (\(Ex i x) -> f i x) z . itoList

  -- | Indexed 'any'.
  iany :: (forall i. Sing (i :: ix) -> p @@ i -> Bool) -> t p j -> Bool
  iany p = ifoldr (\i x ih -> p i x || ih) False

-- | Tranversable for predicate transformers.
class (IxFunctor t, IxFoldable t) =>
  IxTraversable (t :: (TyFun ix Type -> Type) -> jx -> Type) where

  -- | Indexed traverse function.
  itraverse
    :: Applicative f
    => Proxy q
    -> (forall x. Sing x -> p @@ x -> f (q @@ x))
    -> t p j
    -> f (t q j)
  itraverse pq f tp = ifor pq tp f

  -- | Same as above, with arguments flipped.
  ifor
    :: Applicative f
    => Proxy q
    -> t p j
    -> (forall x. Sing x -> p @@ x -> f (q @@ x))
    -> f (t q j)
  ifor pq tp f = itraverse pq f tp

  {-# MINIMAL itraverse | ifor #-}

------------------------------------------------------------------------

class p (f @@ a) =>
  IxComposeC (p :: k2 -> Constraint) (f :: TyFun k1 k2 -> Type) (a :: k1)

instance p (f @@ a) => IxComposeC p f a

-- | Indexed variant of 'ForallF'.
class Forall (IxComposeC p f) =>
  IxForallF (p :: k2 -> Constraint) (f :: TyFun k1 k2 -> Type)

instance Forall (IxComposeC p f) => IxForallF p f

-- | Indexed variant of 'instF'.
iinstF :: forall a p f. Proxy a -> IxForallF p f :- p (f @@ a)
iinstF _ = Sub $
  case inst :: Forall (IxComposeC p f) :- IxComposeC p f a of
    Sub Dict -> Dict

-- | Type alias that is helpful when defining state machine models.
type Ords refs = IxForallF Ord refs :- Ord (refs @@ '())

-- | Same as the above.
type Ords' refs i = IxForallF Ord refs :- Ord (refs @@ i)