{-# LANGUAGE CPP #-}

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

import Data.Aeson (Value)
import Data.ByteString qualified as BS.Strict
import Data.ByteString.Lazy qualified as BS.Lazy
import Data.HashMap.Internal.Array qualified as HashMap (Array)
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.Primitive.Array qualified as Prim (Array)
import Data.Primitive.ByteArray qualified as Prim (ByteArray)
import Data.Ratio
import Data.Sequence (Seq)
import Data.Set (Set)
import Data.SOP
import Data.SOP.Dict
import Data.Text qualified as Text.Strict
import Data.Text.Lazy qualified as Text.Lazy
import Data.Tree (Tree)
import Data.Vector qualified as Vector.Boxed
import Data.Void
import Data.Word

#if !MIN_VERSION_bytestring(0,12,0)
import Data.ByteString.Short qualified as BS.Short
#endif

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 Text.Strict.Text
  , c Text.Lazy.Text

#if !MIN_VERSION_bytestring(0,12,0)
  , c BS.Short.ShortByteString
#endif

  -- 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
  , c Prim.ByteArray
  , c SomeMutableByteArray
  )

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

    -- String types

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

#if !MIN_VERSION_bytestring(0,12,0)
    go C_BS_Short    = Dict
#endif

    -- Aeson

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

    -- Reference cells

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

    -- Functions

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

    -- Containers with no type arguments

    go PrimClassifier a
C_IntSet            = Dict c a
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Prim_ArrayM       = Dict c a
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Vector_Storable   = Dict c a
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Vector_StorableM  = Dict c a
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Vector_Primitive  = Dict c a
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_Vector_PrimitiveM = Dict c a
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_ByteArray         = Dict c a
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go PrimClassifier a
C_MutableByteArray  = Dict c a
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 = Classifier_ o a -> Dict c a
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) = PrimClassifier a -> Dict c a
forall a. PrimClassifier a -> Dict c a
forall (c :: * -> Constraint) a.
PrimSatisfies c =>
PrimClassifier a -> Dict c a
primSatisfies  PrimClassifier a
c
    go (C_Other o a
c) = o a -> Dict c a
forall a. o a -> Dict c a
otherSatisfies o a
c

    -- Compound
    go (C_Maybe        Elems o '[a1]
c) = Elems o '[a1] -> (All c '[a1] => Dict c a) -> Dict c a
forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a1]
c ((All c '[a1] => Dict c a) -> Dict c a)
-> (All c '[a1] => Dict c a) -> Dict c a
forall a b. (a -> b) -> a -> b
$ Dict c a
All c '[a1] => Dict c a
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_Either       Elems o '[a1, b]
c) = Elems o '[a1, b] -> (All c '[a1, b] => Dict c a) -> Dict c a
forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a1, b]
c ((All c '[a1, b] => Dict c a) -> Dict c a)
-> (All c '[a1, b] => Dict c a) -> Dict c a
forall a b. (a -> b) -> a -> b
$ Dict c a
All c '[a1, b] => Dict c a
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_List         Elems o '[a1]
c) = Elems o '[a1] -> (All c '[a1] => Dict c a) -> Dict c a
forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a1]
c ((All c '[a1] => Dict c a) -> Dict c a)
-> (All c '[a1] => Dict c a) -> Dict c a
forall a b. (a -> b) -> a -> b
$ Dict c a
All c '[a1] => Dict c a
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_Ratio        Elems o '[a1]
c) = Elems o '[a1] -> (All c '[a1] => Dict c a) -> Dict c a
forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a1]
c ((All c '[a1] => Dict c a) -> Dict c a)
-> (All c '[a1] => Dict c a) -> Dict c a
forall a b. (a -> b) -> a -> b
$ Dict c a
All c '[a1] => Dict c a
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_Set          Elems o '[a1]
c) = Elems o '[a1] -> (All c '[a1] => Dict c a) -> Dict c a
forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a1]
c ((All c '[a1] => Dict c a) -> Dict c a)
-> (All c '[a1] => Dict c a) -> Dict c a
forall a b. (a -> b) -> a -> b
$ Dict c a
All c '[a1] => Dict c a
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_Map          Elems o '[a1, b]
c) = Elems o '[a1, b] -> (All c '[a1, b] => Dict c a) -> Dict c a
forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a1, b]
c ((All c '[a1, b] => Dict c a) -> Dict c a)
-> (All c '[a1, b] => Dict c a) -> Dict c a
forall a b. (a -> b) -> a -> b
$ Dict c a
All c '[a1, b] => Dict c a
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_IntMap       Elems o '[a1]
c) = Elems o '[a1] -> (All c '[a1] => Dict c a) -> Dict c a
forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a1]
c ((All c '[a1] => Dict c a) -> Dict c a)
-> (All c '[a1] => Dict c a) -> Dict c a
forall a b. (a -> b) -> a -> b
$ Dict c a
All c '[a1] => Dict c a
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_Sequence     Elems o '[a1]
c) = Elems o '[a1] -> (All c '[a1] => Dict c a) -> Dict c a
forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a1]
c ((All c '[a1] => Dict c a) -> Dict c a)
-> (All c '[a1] => Dict c a) -> Dict c a
forall a b. (a -> b) -> a -> b
$ Dict c a
All c '[a1] => Dict c a
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_Tree         Elems o '[a1]
c) = Elems o '[a1] -> (All c '[a1] => Dict c a) -> Dict c a
forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a1]
c ((All c '[a1] => Dict c a) -> Dict c a)
-> (All c '[a1] => Dict c a) -> Dict c a
forall a b. (a -> b) -> a -> b
$ Dict c a
All c '[a1] => Dict c a
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_HashSet      Elems o '[a1]
c) = Elems o '[a1] -> (All c '[a1] => Dict c a) -> Dict c a
forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a1]
c ((All c '[a1] => Dict c a) -> Dict c a)
-> (All c '[a1] => Dict c a) -> Dict c a
forall a b. (a -> b) -> a -> b
$ Dict c a
All c '[a1] => Dict c a
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_HashMap      Elems o '[a1, b]
c) = Elems o '[a1, b] -> (All c '[a1, b] => Dict c a) -> Dict c a
forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a1, b]
c ((All c '[a1, b] => Dict c a) -> Dict c a)
-> (All c '[a1, b] => Dict c a) -> Dict c a
forall a b. (a -> b) -> a -> b
$ Dict c a
All c '[a1, b] => Dict c a
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_HM_Array     Elems o '[a1]
c) = Elems o '[a1] -> (All c '[a1] => Dict c a) -> Dict c a
forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a1]
c ((All c '[a1] => Dict c a) -> Dict c a)
-> (All c '[a1] => Dict c a) -> Dict c a
forall a b. (a -> b) -> a -> b
$ Dict c a
All c '[a1] => Dict c a
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_Prim_Array   Elems o '[a1]
c) = Elems o '[a1] -> (All c '[a1] => Dict c a) -> Dict c a
forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a1]
c ((All c '[a1] => Dict c a) -> Dict c a)
-> (All c '[a1] => Dict c a) -> Dict c a
forall a b. (a -> b) -> a -> b
$ Dict c a
All c '[a1] => Dict c a
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_Vector_Boxed Elems o '[a1]
c) = Elems o '[a1] -> (All c '[a1] => Dict c a) -> Dict c a
forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o '[a1]
c ((All c '[a1] => Dict c a) -> Dict c a)
-> (All c '[a1] => Dict c a) -> Dict c a
forall a b. (a -> b) -> a -> b
$ Dict c a
All c '[a1] => Dict c a
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
    go (C_Tuple        Elems o xs
c) = Elems o xs -> (All c xs => Dict c a) -> Dict c a
forall (as :: [*]) r.
SListI as =>
Elems o as -> (All c as => r) -> r
goElems Elems o xs
c ((All c xs => Dict c a) -> Dict c a)
-> (All c xs => Dict c a) -> Dict c a
forall a b. (a -> b) -> a -> b
$ Dict c a
All c xs => Dict c a
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 NP (Dict c) as -> Dict (All c) as
forall {k} (c :: k -> Constraint) (xs :: [k]).
NP (Dict c) xs -> Dict (All c) xs
all_NP ((forall a. Elem o a -> Dict c a)
-> NP (Elem o) as -> NP (Dict c) as
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 Elem o a -> Dict c a
forall a. Elem o a -> Dict c a
goElem NP (Elem o) as
cs) of Dict (All c) as
Dict -> r
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) = Classifier_ o a -> Dict c a
forall a. Classifier_ o a -> Dict c a
go Classifier_ o a
c
    goElem Elem o a
NoElem   = Dict c a
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict