{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | Support for reclassification
module Debug.RecoverRTTI.Reclassify (
    Reclassified(..)
  , reclassify_
  , distribReclassified
  , FromUsr(..)
  , coerceFromUsr
  ) where

import Data.Kind
import Data.SOP hiding (NS(..))
import Data.Void
import Unsafe.Coerce (unsafeCoerce)

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

-- | Reclassified values
--
-- Reclassification can be done by user code which want to take advantage of
-- the classification infrastructure for @recover-rtti@ but add some additional
-- classification for domain-specific types known only to that client code.
--
-- When we reclassify a value, a value that might previously be classified as
-- @UserDefined@ may now be classified as some concrete type; therefore we
-- compute a classifier for a potentially /different/ type along with
-- evidence that we can coerce between the two.
data Reclassified o a where
  Reclassified :: o b -> FromUsr a b -> Reclassified o a

-- | Extension of 'Reclassified' to multiple elems
--
-- This is used internally only.
data ReclassifiedElems o as where
  RElems ::
       (SListI bs, Length bs ~ Length as)
    => Elems o bs -> PairWise FromUsr as bs -> ReclassifiedElems o as

reclassify_ :: forall m o o'. Applicative m
  => (forall a. o a -> m (Reclassified o' a))
  -> (forall a. Classifier_ o a -> m (Classifier_ (Reclassified o') a))
reclassify_ :: forall (m :: * -> *) (o :: * -> *) (o' :: * -> *).
Applicative m =>
(forall a. o a -> m (Reclassified o' a))
-> forall a. Classifier_ o a -> m (Classifier_ (Reclassified o') a)
reclassify_ = forall (m :: * -> *) (o :: * -> *) (o' :: * -> *).
Applicative m =>
(forall a. o a -> m (o' a))
-> forall a. Classifier_ o a -> m (Classifier_ o' a)
mapClassifier

-- | Lift 'Reclassified' to the top-level
--
-- Given a classifier with user-defined classifiers at the levels, along with
-- coercion functions, leave the user-defined classifiers in place but lift the
-- coercion function to the top-level.
distribReclassified :: forall o.
     (forall a. Classifier_ (Reclassified o) a -> Reclassified (Classifier_ o) a)
distribReclassified :: forall (o :: * -> *) a.
Classifier_ (Reclassified o) a -> Reclassified (Classifier_ o) a
distribReclassified = forall a.
Classifier_ (Reclassified o) a -> Reclassified (Classifier_ o) a
go
  where
    go :: forall a. Classifier_ (Reclassified o) a -> Reclassified (Classifier_ o) a
    -- Primitive and user-defined
    go :: forall a.
Classifier_ (Reclassified o) a -> Reclassified (Classifier_ o) a
go (C_Prim  PrimClassifier a
c) = forall (o :: * -> *) x a. o x -> FromUsr a x -> Reclassified o a
Reclassified (forall a (o :: * -> *). PrimClassifier a -> Classifier_ o a
C_Prim PrimClassifier a
c) forall a. FromUsr a a
Id
    go (C_Other Reclassified o a
c) = case Reclassified o a
c of Reclassified o b
c' FromUsr a b
f -> forall (o :: * -> *) x a. o x -> FromUsr a x -> Reclassified o a
Reclassified (forall (o :: * -> *) a. o a -> Classifier_ o a
C_Other o b
c') FromUsr a b
f

    -- Compound
    go (C_Maybe        Elems (Reclassified o) '[a]
c) = forall (f :: * -> *) a.
(forall a'. Elems o '[a'] -> Classifier_ o (f a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (f a)
go1 forall (o :: * -> *) x. Elems o '[x] -> Classifier_ o (Maybe x)
C_Maybe        Elems (Reclassified o) '[a]
c
    go (C_Either       Elems (Reclassified o) '[a, b]
c) = forall (f :: * -> * -> *) a b.
(forall a' b'. Elems o '[a', b'] -> Classifier_ o (f a' b'))
-> Elems (Reclassified o) '[a, b]
-> Reclassified (Classifier_ o) (f a b)
go2 forall (o :: * -> *) x y.
Elems o '[x, y] -> Classifier_ o (Either x y)
C_Either       Elems (Reclassified o) '[a, b]
c
    go (C_List         Elems (Reclassified o) '[a]
c) = forall (f :: * -> *) a.
(forall a'. Elems o '[a'] -> Classifier_ o (f a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (f a)
go1 forall (o :: * -> *) x. Elems o '[x] -> Classifier_ o [x]
C_List         Elems (Reclassified o) '[a]
c
    go (C_Ratio        Elems (Reclassified o) '[a]
c) = forall (f :: * -> *) a.
(forall a'. Elems o '[a'] -> Classifier_ o (f a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (f a)
go1 forall (o :: * -> *) x. Elems o '[x] -> Classifier_ o (Ratio x)
C_Ratio        Elems (Reclassified o) '[a]
c
    go (C_Set          Elems (Reclassified o) '[a]
c) = forall (f :: * -> *) a.
(forall a'. Elems o '[a'] -> Classifier_ o (f a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (f a)
go1 forall (o :: * -> *) x. Elems o '[x] -> Classifier_ o (Set x)
C_Set          Elems (Reclassified o) '[a]
c
    go (C_Map          Elems (Reclassified o) '[a, b]
c) = forall (f :: * -> * -> *) a b.
(forall a' b'. Elems o '[a', b'] -> Classifier_ o (f a' b'))
-> Elems (Reclassified o) '[a, b]
-> Reclassified (Classifier_ o) (f a b)
go2 forall (o :: * -> *) x y.
Elems o '[x, y] -> Classifier_ o (Map x y)
C_Map          Elems (Reclassified o) '[a, b]
c
    go (C_IntMap       Elems (Reclassified o) '[a]
c) = forall (f :: * -> *) a.
(forall a'. Elems o '[a'] -> Classifier_ o (f a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (f a)
go1 forall (o :: * -> *) x. Elems o '[x] -> Classifier_ o (IntMap x)
C_IntMap       Elems (Reclassified o) '[a]
c
    go (C_Sequence     Elems (Reclassified o) '[a]
c) = forall (f :: * -> *) a.
(forall a'. Elems o '[a'] -> Classifier_ o (f a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (f a)
go1 forall (o :: * -> *) x. Elems o '[x] -> Classifier_ o (Seq x)
C_Sequence     Elems (Reclassified o) '[a]
c
    go (C_Tree         Elems (Reclassified o) '[a]
c) = forall (f :: * -> *) a.
(forall a'. Elems o '[a'] -> Classifier_ o (f a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (f a)
go1 forall (o :: * -> *) x. Elems o '[x] -> Classifier_ o (Tree x)
C_Tree         Elems (Reclassified o) '[a]
c
    go (C_HashSet      Elems (Reclassified o) '[a]
c) = forall (f :: * -> *) a.
(forall a'. Elems o '[a'] -> Classifier_ o (f a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (f a)
go1 forall (o :: * -> *) x. Elems o '[x] -> Classifier_ o (HashSet x)
C_HashSet      Elems (Reclassified o) '[a]
c
    go (C_HashMap      Elems (Reclassified o) '[a, b]
c) = forall (f :: * -> * -> *) a b.
(forall a' b'. Elems o '[a', b'] -> Classifier_ o (f a' b'))
-> Elems (Reclassified o) '[a, b]
-> Reclassified (Classifier_ o) (f a b)
go2 forall (o :: * -> *) x y.
Elems o '[x, y] -> Classifier_ o (HashMap x y)
C_HashMap      Elems (Reclassified o) '[a, b]
c
    go (C_HM_Array     Elems (Reclassified o) '[a]
c) = forall (f :: * -> *) a.
(forall a'. Elems o '[a'] -> Classifier_ o (f a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (f a)
go1 forall (o :: * -> *) x. Elems o '[x] -> Classifier_ o (Array x)
C_HM_Array     Elems (Reclassified o) '[a]
c
    go (C_Prim_Array   Elems (Reclassified o) '[a]
c) = forall (f :: * -> *) a.
(forall a'. Elems o '[a'] -> Classifier_ o (f a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (f a)
go1 forall (o :: * -> *) x. Elems o '[x] -> Classifier_ o (Array x)
C_Prim_Array   Elems (Reclassified o) '[a]
c
    go (C_Vector_Boxed Elems (Reclassified o) '[a]
c) = forall (f :: * -> *) a.
(forall a'. Elems o '[a'] -> Classifier_ o (f a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (f a)
go1 forall (o :: * -> *) x. Elems o '[x] -> Classifier_ o (Vector x)
C_Vector_Boxed Elems (Reclassified o) '[a]
c
    go (C_Tuple        Elems (Reclassified o) xs
c) = forall (f :: [*] -> *) (as :: [*]).
SListI as =>
(forall (as' :: [*]).
 (SListI as', Length as' ~ Length as) =>
 Elems o as' -> Classifier_ o (f as'))
-> Elems (Reclassified o) as -> Reclassified (Classifier_ o) (f as)
goN forall (x :: [*]) (o :: * -> *).
(SListI x, IsValidSize (Length x)) =>
Elems o x -> Classifier_ o (WrappedTuple x)
C_Tuple        Elems (Reclassified o) xs
c

    go1 :: forall f a.
         (forall a'. Elems o '[a'] -> Classifier_ o (f a'))
      -> Elems (Reclassified o) '[a]
      -> Reclassified (Classifier_ o) (f a)
    go1 :: forall (f :: * -> *) a.
(forall a'. Elems o '[a'] -> Classifier_ o (f a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (f a)
go1 forall a'. Elems o '[a'] -> Classifier_ o (f a')
cf Elems (Reclassified o) '[a]
c =
        case forall (xs :: [*]) (o :: * -> *).
SListI xs =>
Elems (Reclassified o) xs -> ReclassifiedElems o xs
distribElems Elems (Reclassified o) '[a]
c of
          RElems Elems o bs
c' (PCons FromUsr x y
f PairWise FromUsr xs ys
PNil) -> forall (o :: * -> *) x a. o x -> FromUsr a x -> Reclassified o a
Reclassified (forall a'. Elems o '[a'] -> Classifier_ o (f a')
cf Elems o bs
c') (forall x y (xs :: * -> *). FromUsr x y -> FromUsr (xs x) (xs y)
F1 FromUsr x y
f)

    go2 :: forall f a b.
         (forall a' b'. Elems o '[a', b'] -> Classifier_ o (f a' b'))
      -> Elems (Reclassified o) '[a, b]
      -> Reclassified (Classifier_ o) (f a b)
    go2 :: forall (f :: * -> * -> *) a b.
(forall a' b'. Elems o '[a', b'] -> Classifier_ o (f a' b'))
-> Elems (Reclassified o) '[a, b]
-> Reclassified (Classifier_ o) (f a b)
go2 forall a' b'. Elems o '[a', b'] -> Classifier_ o (f a' b')
cf Elems (Reclassified o) '[a, b]
c =
        case forall (xs :: [*]) (o :: * -> *).
SListI xs =>
Elems (Reclassified o) xs -> ReclassifiedElems o xs
distribElems Elems (Reclassified o) '[a, b]
c of
          RElems Elems o bs
c' (PCons FromUsr x y
f (PCons FromUsr x y
f' PairWise FromUsr xs ys
PNil)) -> forall (o :: * -> *) x a. o x -> FromUsr a x -> Reclassified o a
Reclassified (forall a' b'. Elems o '[a', b'] -> Classifier_ o (f a' b')
cf Elems o bs
c') (forall x y xs ys (f :: * -> * -> *).
FromUsr x y -> FromUsr xs ys -> FromUsr (f x xs) (f y ys)
F2 FromUsr x y
f FromUsr x y
f')

    goN :: forall f as.
         SListI as
      => (forall as'.
               (SListI as', Length as' ~ Length as)
            => Elems o as' -> Classifier_ o (f as'))
      -> Elems (Reclassified o) as
      -> Reclassified (Classifier_ o) (f as)
    goN :: forall (f :: [*] -> *) (as :: [*]).
SListI as =>
(forall (as' :: [*]).
 (SListI as', Length as' ~ Length as) =>
 Elems o as' -> Classifier_ o (f as'))
-> Elems (Reclassified o) as -> Reclassified (Classifier_ o) (f as)
goN forall (as' :: [*]).
(SListI as', Length as' ~ Length as) =>
Elems o as' -> Classifier_ o (f as')
cf Elems (Reclassified o) as
c =
        case forall (xs :: [*]) (o :: * -> *).
SListI xs =>
Elems (Reclassified o) xs -> ReclassifiedElems o xs
distribElems Elems (Reclassified o) as
c of
          RElems Elems o bs
c' PairWise FromUsr as bs
fs -> forall (o :: * -> *) x a. o x -> FromUsr a x -> Reclassified o a
Reclassified (forall (as' :: [*]).
(SListI as', Length as' ~ Length as) =>
Elems o as' -> Classifier_ o (f as')
cf Elems o bs
c') (forall (x :: [*]) (y :: [*]) (xs :: [*] -> *).
PairWise FromUsr x y -> FromUsr (xs x) (xs y)
FN PairWise FromUsr as bs
fs)

distribElem :: Elem (Reclassified o) a -> Reclassified (Elem o) a
distribElem :: forall (o :: * -> *) a.
Elem (Reclassified o) a -> Reclassified (Elem o) a
distribElem = \case
    Elem (Reclassified o) a
NoElem -> forall (o :: * -> *) x a. o x -> FromUsr a x -> Reclassified o a
Reclassified forall (o :: * -> *). Elem o Void
NoElem forall a. FromUsr Void a
Absurd
    Elem Classifier_ (Reclassified o) a
c -> case forall (o :: * -> *) a.
Classifier_ (Reclassified o) a -> Reclassified (Classifier_ o) a
distribReclassified Classifier_ (Reclassified o) a
c of
                Reclassified Classifier_ o b
c' FromUsr a b
f -> forall (o :: * -> *) x a. o x -> FromUsr a x -> Reclassified o a
Reclassified (forall (o :: * -> *) a. Classifier_ o a -> Elem o a
Elem Classifier_ o b
c') FromUsr a b
f

distribElems ::
     SListI xs
  => Elems (Reclassified o) xs -> ReclassifiedElems o xs
distribElems :: forall (xs :: [*]) (o :: * -> *).
SListI xs =>
Elems (Reclassified o) xs -> ReclassifiedElems o xs
distribElems = \(Elems NP (Elem (Reclassified o)) xs
cs) -> forall (o :: * -> *) (xs :: [*]).
NP (Reclassified (Elem o)) xs -> ReclassifiedElems o xs
go forall a b. (a -> b) -> a -> b
$ 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 (o :: * -> *) a.
Elem (Reclassified o) a -> Reclassified (Elem o) a
distribElem NP (Elem (Reclassified o)) xs
cs
  where
    go :: NP (Reclassified (Elem o)) xs -> ReclassifiedElems o xs
    go :: forall (o :: * -> *) (xs :: [*]).
NP (Reclassified (Elem o)) xs -> ReclassifiedElems o xs
go NP (Reclassified (Elem o)) xs
Nil                      = forall (x :: [*]) (as :: [*]) (o :: * -> *).
(SListI x, Length x ~ Length as) =>
Elems o x -> PairWise FromUsr as x -> ReclassifiedElems o as
RElems (forall (o :: * -> *) (xs :: [*]). NP (Elem o) xs -> Elems o xs
Elems forall {k} (a :: k -> *). NP a '[]
Nil) forall (f :: * -> * -> *). PairWise f '[] '[]
PNil
    go (Reclassified Elem o b
c FromUsr x b
f :* NP (Reclassified (Elem o)) xs
cs) = case forall (o :: * -> *) (xs :: [*]).
NP (Reclassified (Elem o)) xs -> ReclassifiedElems o xs
go NP (Reclassified (Elem o)) xs
cs of
                                    RElems (Elems NP (Elem o) bs
cs') PairWise FromUsr xs bs
fs' ->
                                      forall (x :: [*]) (as :: [*]) (o :: * -> *).
(SListI x, Length x ~ Length as) =>
Elems o x -> PairWise FromUsr as x -> ReclassifiedElems o as
RElems (forall (o :: * -> *) (xs :: [*]). NP (Elem o) xs -> Elems o xs
Elems (Elem o b
c forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP (Elem o) bs
cs')) (forall (f :: * -> * -> *) x y (xs :: [*]) (ys :: [*]).
f x y -> PairWise f xs ys -> PairWise f (x : xs) (y : ys)
PCons FromUsr x b
f PairWise FromUsr xs bs
fs')

{-------------------------------------------------------------------------------
  Evidence that we are only doing conversions from Any
-------------------------------------------------------------------------------}

-- | Evidence that we can convert between two types
--
-- The only actual conversion we ever do is from 'UserDefined' (aka 'Any') to
-- whatever type the reclassification gives.
data FromUsr :: Type -> Type -> Type where
  Id      :: FromUsr a a
  Absurd  :: FromUsr Void a
  FromUsr :: FromUsr UserDefined a
  F1      :: FromUsr a1 b1 -> FromUsr (f a1) (f b1)
  F2      :: FromUsr a1 b1 -> FromUsr a2 b2 -> FromUsr (f a1 a2) (f b1 b2)
  FN      :: PairWise FromUsr as bs -> FromUsr (f as) (f bs)
  Compose :: FromUsr b c -> FromUsr a b -> FromUsr a c

-- | Coerce, given some evidence that the coercion is sound.
coerceFromUsr :: FromUsr a b -> a -> b
coerceFromUsr :: forall a b. FromUsr a b -> a -> b
coerceFromUsr = forall a b. a -> b
unsafeCoerce