{-# LANGUAGE ConstraintKinds         #-}
{-# LANGUAGE DataKinds               #-}
{-# LANGUAGE FlexibleContexts        #-}
{-# LANGUAGE FlexibleInstances       #-}
{-# LANGUAGE GADTs                   #-}
{-# LANGUAGE KindSignatures          #-}
{-# LANGUAGE QuantifiedConstraints   #-}
{-# LANGUAGE RankNTypes              #-}
{-# LANGUAGE ScopedTypeVariables     #-}
{-# LANGUAGE UndecidableInstances    #-}
{-# LANGUAGE UndecidableSuperClasses #-}

-- | Establish that a constraint holds for all classified types
module Debug.RecoverRTTI.Constraint (
    PrimSatisfies
  , primSatisfies
  , ClassifiedSatisfies
  , classifiedSatisfies
  ) where

import Data.Aeson (Value)
import Data.HashMap.Lazy (HashMap)
import Data.HashSet (HashSet)
import Data.Int
import Data.IntMap (IntMap)
import Data.IntSet (IntSet)
import Data.Kind
import Data.Map (Map)
import Data.Ratio
import Data.Sequence (Seq)
import Data.Set (Set)
import Data.SOP
import Data.SOP.Dict
import Data.Tree (Tree)
import Data.Void
import Data.Word

import qualified Data.ByteString             as BS.Strict
import qualified Data.ByteString.Lazy        as BS.Lazy
import qualified Data.ByteString.Short       as BS.Short
import qualified Data.HashMap.Internal.Array as HashMap (Array)
import qualified Data.Primitive.Array        as Prim (Array)
import qualified Data.Text                   as Text.Strict
import qualified Data.Text.Lazy              as Text.Lazy
import qualified Data.Vector                 as Vector.Boxed

import Debug.RecoverRTTI.Classifier
import Debug.RecoverRTTI.Nat
import Debug.RecoverRTTI.Tuple
import Debug.RecoverRTTI.Wrappers

{-------------------------------------------------------------------------------
  Primitives
-------------------------------------------------------------------------------}

type PrimSatisfies (c :: Type -> Constraint) = (
  -- Primitive types

    c Bool
  , c Char
  , c Double
  , c Float
  , c Int
  , c Int16
  , c Int8
  , c Int32
  , c Int64
  , c Integer
  , c Ordering
  , c ()
  , c Word
  , c Word8
  , c Word16
  , c Word32
  , c Word64

  -- String types

  , c String
  , c BS.Strict.ByteString
  , c BS.Lazy.ByteString
  , c BS.Short.ShortByteString
  , c Text.Strict.Text
  , c Text.Lazy.Text

  -- Aeson

  , c Value

  -- Reference cells

  , c SomeSTRef
  , c SomeTVar
  , c SomeMVar

  -- Functions

  , c SomeFun

  -- Containers with no type arguments

  , c IntSet
  , c SomePrimArrayM
  , c SomeStorableVector
  , c SomeStorableVectorM
  , c SomePrimitiveVector
  , c SomePrimitiveVectorM
  )

primSatisfies :: forall c.
     PrimSatisfies c
  => (forall a. PrimClassifier a -> Dict c a)
primSatisfies :: forall (c :: * -> Constraint) a.
PrimSatisfies c =>
PrimClassifier a -> Dict c a
primSatisfies = forall a. PrimClassifier a -> Dict c a
go
  where
    go :: PrimClassifier a -> Dict c a

    -- Primitive types

    go :: forall a. PrimClassifier a -> Dict c a
go PrimClassifier a
C_Bool     = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Char     = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Double   = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Float    = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Int      = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Int16    = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Int8     = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Int32    = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Int64    = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Integer  = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Ordering = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Unit     = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Word     = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Word8    = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Word16   = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Word32   = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Word64   = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict

    -- String types

    go PrimClassifier a
C_String      = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_BS_Strict   = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_BS_Lazy     = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_BS_Short    = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Text_Strict = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Text_Lazy   = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict

    -- Aeson

    go PrimClassifier a
C_Value = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict

    -- Reference cells

    go PrimClassifier a
C_STRef = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_TVar  = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_MVar  = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict

    -- Functions

    go PrimClassifier a
C_Fun = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict

    -- Containers with no type arguments

    go PrimClassifier a
C_IntSet            = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Prim_ArrayM       = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Vector_Storable   = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Vector_StorableM  = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Vector_Primitive  = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Vector_PrimitiveM = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict

{-------------------------------------------------------------------------------
  Compound

  We can't use a type alias for the constraint here as ghc doesn't like
  quantified constraints in constraint type aliases.
-------------------------------------------------------------------------------}

class (
    PrimSatisfies c
    -- Compound
  , forall a.   (c a)      => c (Maybe a)
  , forall a b. (c a, c b) => c (Either a b)
  , forall a.   (c a)      => c [a]
  , forall a.   (c a)      => c (Ratio a)
  , forall a.   (c a)      => c (Set a)
  , forall a b. (c a, c b) => c (Map a b)
  , forall a.   (c a)      => c (IntMap a)
  , forall a.   (c a)      => c (Seq a)
  , forall a.   (c a)      => c (Tree a)
  , forall a.   (c a)      => c (HashSet a)
  , forall a b. (c a, c b) => c (HashMap a b)
  , forall a.   (c a)      => c (HashMap.Array a)
  , forall a.   (c a)      => c (Prim.Array a)
  , forall a.   (c a)      => c (Vector.Boxed.Vector a)
  , forall xs. (All c xs,  IsValidSize (Length xs)) => c (WrappedTuple xs)
  ) => ClassifiedSatisfies (c :: Type -> Constraint)

instance (
    PrimSatisfies c
    -- Compound
  , forall a.   (c a)      => c (Maybe a)
  , forall a b. (c a, c b) => c (Either a b)
  , forall a.   (c a)      => c [a]
  , forall a.   (c a)      => c (Ratio a)
  , forall a.   (c a)      => c (Set a)
  , forall a b. (c a, c b) => c (Map a b)
  , forall a.   (c a)      => c (IntMap a)
  , forall a.   (c a)      => c (Seq a)
  , forall a.   (c a)      => c (Tree a)
  , forall a.   (c a)      => c (HashSet a)
  , forall a b. (c a, c b) => c (HashMap a b)
  , forall a.   (c a)      => c (HashMap.Array a)
  , forall a.   (c a)      => c (Prim.Array a)
  , forall a.   (c a)      => c (Vector.Boxed.Vector a)
  , forall xs. (All c xs,  IsValidSize (Length xs)) => c (WrappedTuple xs)
  ) => ClassifiedSatisfies (c :: Type -> Constraint)

classifiedSatisfies :: forall c o.
     (ClassifiedSatisfies c, c Void)
  => (forall a. o a -> Dict c a)
  -> (forall a. Classifier_ o a -> Dict c a)
classifiedSatisfies :: forall (c :: * -> Constraint) (o :: * -> *).
(ClassifiedSatisfies c, c Void) =>
(forall a. o a -> Dict c a)
-> forall a. Classifier_ o a -> Dict c a
classifiedSatisfies forall a. o a -> Dict c a
otherSatisfies = forall a. Classifier_ o a -> Dict c a
go
  where
    go :: Classifier_ o a -> Dict c a
    go :: forall a. Classifier_ o a -> Dict c a
go (C_Prim  PrimClassifier a
c) = forall (c :: * -> Constraint) a.
PrimSatisfies c =>
PrimClassifier a -> Dict c a
primSatisfies  PrimClassifier a
c
    go (C_Other o a
c) = forall a. o a -> Dict c a
otherSatisfies o a
c

    -- Compound
    go (C_Maybe        Elems o '[a]
c) = forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a]
c forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_Either       Elems o '[a, b]
c) = forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a, b]
c forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_List         Elems o '[a]
c) = forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a]
c forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_Ratio        Elems o '[a]
c) = forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a]
c forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_Set          Elems o '[a]
c) = forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a]
c forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_Map          Elems o '[a, b]
c) = forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a, b]
c forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_IntMap       Elems o '[a]
c) = forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a]
c forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_Sequence     Elems o '[a]
c) = forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a]
c forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_Tree         Elems o '[a]
c) = forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a]
c forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_HashSet      Elems o '[a]
c) = forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a]
c forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_HashMap      Elems o '[a, b]
c) = forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a, b]
c forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_HM_Array     Elems o '[a]
c) = forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a]
c forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_Prim_Array   Elems o '[a]
c) = forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a]
c forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_Vector_Boxed Elems o '[a]
c) = forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a]
c forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_Tuple        Elems o xs
c) = forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o xs
c forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict

    goElems :: SListI as => Elems o as -> (All c as => r) -> r
    goElems :: forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems (Elems NP (Elem o) as
cs) All c as => r
k = case forall {k} (c :: k -> Constraint) (xs :: [k]).
NP (Dict c) xs -> Dict (All c) xs
all_NP (forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hmap forall a. Elem o a -> Dict c a
goElem NP (Elem o) as
cs) of Dict (All c) as
Dict -> All c as => r
k

    goElem :: Elem o a -> Dict c a
    goElem :: forall a. Elem o a -> Dict c a
goElem (Elem Classifier_ o a
c) = forall a. Classifier_ o a -> Dict c a
go Classifier_ o a
c
    goElem Elem o a
NoElem   = forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict