{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
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
data Reclassified o a where
Reclassified :: o b -> FromUsr a b -> Reclassified o a
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 a. o a -> m (Reclassified o' a))
-> forall a. Classifier_ o a -> m (Classifier_ (Reclassified o') a)
reclassify_ = (forall a. o a -> m (Reclassified o' a))
-> Classifier_ o a -> m (Classifier_ (Reclassified o') a)
forall (m :: * -> *) (o :: * -> *) (o' :: * -> *).
Applicative m =>
(forall a. o a -> m (o' a))
-> forall a. Classifier_ o a -> m (Classifier_ o' a)
mapClassifier
distribReclassified :: forall o.
(forall a. Classifier_ (Reclassified o) a -> Reclassified (Classifier_ o) a)
distribReclassified :: Classifier_ (Reclassified o) a -> Reclassified (Classifier_ o) a
distribReclassified = Classifier_ (Reclassified o) a -> Reclassified (Classifier_ o) a
forall a.
Classifier_ (Reclassified o) a -> Reclassified (Classifier_ o) a
go
where
go :: forall a. Classifier_ (Reclassified o) a -> Reclassified (Classifier_ o) a
go :: Classifier_ (Reclassified o) a -> Reclassified (Classifier_ o) a
go (C_Prim PrimClassifier a
c) = Classifier_ o a -> FromUsr a a -> Reclassified (Classifier_ o) a
forall (o :: * -> *) b a. o b -> FromUsr a b -> Reclassified o a
Reclassified (PrimClassifier a -> Classifier_ o a
forall a (o :: * -> *). PrimClassifier a -> Classifier_ o a
C_Prim PrimClassifier a
c) FromUsr a a
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 -> Classifier_ o b -> FromUsr a b -> Reclassified (Classifier_ o) a
forall (o :: * -> *) b a. o b -> FromUsr a b -> Reclassified o a
Reclassified (o b -> Classifier_ o b
forall (o :: * -> *) a. o a -> Classifier_ o a
C_Other o b
c') FromUsr a b
f
go (C_Maybe Elems (Reclassified o) '[a]
c) = (forall a'. Elems o '[a'] -> Classifier_ o (Maybe a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (Maybe a)
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 (Maybe a')
forall (o :: * -> *) a. Elems o '[a] -> Classifier_ o (Maybe a)
C_Maybe Elems (Reclassified o) '[a]
c
go (C_Either Elems (Reclassified o) '[a, b]
c) = (forall a' b'. Elems o '[a', b'] -> Classifier_ o (Either a' b'))
-> Elems (Reclassified o) '[a, b]
-> Reclassified (Classifier_ o) (Either a b)
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 (Either a' b')
forall (o :: * -> *) a b.
Elems o '[a, b] -> Classifier_ o (Either a b)
C_Either Elems (Reclassified o) '[a, b]
c
go (C_List Elems (Reclassified o) '[a]
c) = (forall a'. Elems o '[a'] -> Classifier_ o [a'])
-> Elems (Reclassified o) '[a] -> Reclassified (Classifier_ o) [a]
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 [a']
forall (o :: * -> *) a. Elems o '[a] -> Classifier_ o [a]
C_List Elems (Reclassified o) '[a]
c
go (C_Ratio Elems (Reclassified o) '[a]
c) = (forall a'. Elems o '[a'] -> Classifier_ o (Ratio a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (Ratio a)
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 (Ratio a')
forall (o :: * -> *) a. Elems o '[a] -> Classifier_ o (Ratio a)
C_Ratio Elems (Reclassified o) '[a]
c
go (C_Set Elems (Reclassified o) '[a]
c) = (forall a'. Elems o '[a'] -> Classifier_ o (Set a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (Set a)
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 (Set a')
forall (o :: * -> *) a. Elems o '[a] -> Classifier_ o (Set a)
C_Set Elems (Reclassified o) '[a]
c
go (C_Map Elems (Reclassified o) '[a, b]
c) = (forall a' b'. Elems o '[a', b'] -> Classifier_ o (Map a' b'))
-> Elems (Reclassified o) '[a, b]
-> Reclassified (Classifier_ o) (Map a b)
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 (Map a' b')
forall (o :: * -> *) a b.
Elems o '[a, b] -> Classifier_ o (Map a b)
C_Map Elems (Reclassified o) '[a, b]
c
go (C_IntMap Elems (Reclassified o) '[a]
c) = (forall a'. Elems o '[a'] -> Classifier_ o (IntMap a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (IntMap a)
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 (IntMap a')
forall (o :: * -> *) a. Elems o '[a] -> Classifier_ o (IntMap a)
C_IntMap Elems (Reclassified o) '[a]
c
go (C_Sequence Elems (Reclassified o) '[a]
c) = (forall a'. Elems o '[a'] -> Classifier_ o (Seq a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (Seq a)
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 (Seq a')
forall (o :: * -> *) a. Elems o '[a] -> Classifier_ o (Seq a)
C_Sequence Elems (Reclassified o) '[a]
c
go (C_Tree Elems (Reclassified o) '[a]
c) = (forall a'. Elems o '[a'] -> Classifier_ o (Tree a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (Tree a)
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 (Tree a')
forall (o :: * -> *) a. Elems o '[a] -> Classifier_ o (Tree a)
C_Tree Elems (Reclassified o) '[a]
c
go (C_HashSet Elems (Reclassified o) '[a]
c) = (forall a'. Elems o '[a'] -> Classifier_ o (HashSet a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (HashSet a)
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 (HashSet a')
forall (o :: * -> *) a. Elems o '[a] -> Classifier_ o (HashSet a)
C_HashSet Elems (Reclassified o) '[a]
c
go (C_HashMap Elems (Reclassified o) '[a, b]
c) = (forall a' b'. Elems o '[a', b'] -> Classifier_ o (HashMap a' b'))
-> Elems (Reclassified o) '[a, b]
-> Reclassified (Classifier_ o) (HashMap a b)
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 (HashMap a' b')
forall (o :: * -> *) a b.
Elems o '[a, b] -> Classifier_ o (HashMap a b)
C_HashMap Elems (Reclassified o) '[a, b]
c
go (C_HM_Array Elems (Reclassified o) '[a]
c) = (forall a'. Elems o '[a'] -> Classifier_ o (Array a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (Array a)
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 (Array a')
forall (o :: * -> *) a. Elems o '[a] -> Classifier_ o (Array a)
C_HM_Array Elems (Reclassified o) '[a]
c
go (C_Prim_Array Elems (Reclassified o) '[a]
c) = (forall a'. Elems o '[a'] -> Classifier_ o (Array a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (Array a)
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 (Array a')
forall (o :: * -> *) a. Elems o '[a] -> Classifier_ o (Array a)
C_Prim_Array Elems (Reclassified o) '[a]
c
go (C_Vector_Boxed Elems (Reclassified o) '[a]
c) = (forall a'. Elems o '[a'] -> Classifier_ o (Vector a'))
-> Elems (Reclassified o) '[a]
-> Reclassified (Classifier_ o) (Vector a)
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 (Vector a')
forall (o :: * -> *) a. Elems o '[a] -> Classifier_ o (Vector a)
C_Vector_Boxed Elems (Reclassified o) '[a]
c
go (C_Tuple Elems (Reclassified o) xs
c) = (forall (as' :: [*]).
(SListI as', Length as' ~ Length xs) =>
Elems o as' -> Classifier_ o (WrappedTuple as'))
-> Elems (Reclassified o) xs
-> Reclassified (Classifier_ o) (WrappedTuple xs)
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 xs) =>
Elems o as' -> Classifier_ o (WrappedTuple as')
forall (xs :: [*]) (o :: * -> *).
(SListI xs, IsValidSize (Length xs)) =>
Elems o xs -> Classifier_ o (WrappedTuple xs)
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 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 Elems (Reclassified o) '[a] -> ReclassifiedElems o '[a]
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) -> Classifier_ o (f y)
-> FromUsr (f x) (f y) -> Reclassified (Classifier_ o) (f x)
forall (o :: * -> *) b a. o b -> FromUsr a b -> Reclassified o a
Reclassified (Elems o '[y] -> Classifier_ o (f y)
forall a'. Elems o '[a'] -> Classifier_ o (f a')
cf Elems o bs
Elems o '[y]
c') (FromUsr x y -> FromUsr (f x) (f y)
forall a1 b1 (f :: * -> *). FromUsr a1 b1 -> FromUsr (f a1) (f b1)
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 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 Elems (Reclassified o) '[a, b] -> ReclassifiedElems o '[a, b]
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)) -> Classifier_ o (f y y)
-> FromUsr (f x x) (f y y) -> Reclassified (Classifier_ o) (f x x)
forall (o :: * -> *) b a. o b -> FromUsr a b -> Reclassified o a
Reclassified (Elems o '[y, y] -> Classifier_ o (f y y)
forall a' b'. Elems o '[a', b'] -> Classifier_ o (f a' b')
cf Elems o bs
Elems o '[y, y]
c') (FromUsr x y -> FromUsr x y -> FromUsr (f x x) (f y y)
forall a1 b1 a2 b2 (f :: * -> * -> *).
FromUsr a1 b1 -> FromUsr a2 b2 -> FromUsr (f a1 a2) (f b1 b2)
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 (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 Elems (Reclassified o) as -> ReclassifiedElems o as
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 -> Classifier_ o (f bs)
-> FromUsr (f as) (f bs) -> Reclassified (Classifier_ o) (f as)
forall (o :: * -> *) b a. o b -> FromUsr a b -> Reclassified o a
Reclassified (Elems o bs -> Classifier_ o (f bs)
forall (as' :: [*]).
(SListI as', Length as' ~ Length as) =>
Elems o as' -> Classifier_ o (f as')
cf Elems o bs
c') (PairWise FromUsr as bs -> FromUsr (f as) (f bs)
forall (as :: [*]) (bs :: [*]) (f :: [*] -> *).
PairWise FromUsr as bs -> FromUsr (f as) (f bs)
FN PairWise FromUsr as bs
fs)
distribElem :: Elem (Reclassified o) a -> Reclassified (Elem o) a
distribElem :: Elem (Reclassified o) a -> Reclassified (Elem o) a
distribElem = \case
Elem (Reclassified o) a
NoElem -> Elem o Void -> FromUsr Void Void -> Reclassified (Elem o) Void
forall (o :: * -> *) b a. o b -> FromUsr a b -> Reclassified o a
Reclassified Elem o Void
forall (o :: * -> *). Elem o Void
NoElem FromUsr Void Void
forall a. FromUsr Void a
Absurd
Elem Classifier_ (Reclassified o) a
c -> case Classifier_ (Reclassified o) a -> Reclassified (Classifier_ o) a
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 -> Elem o b -> FromUsr a b -> Reclassified (Elem o) a
forall (o :: * -> *) b a. o b -> FromUsr a b -> Reclassified o a
Reclassified (Classifier_ o b -> Elem o b
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 :: Elems (Reclassified o) xs -> ReclassifiedElems o xs
distribElems = \(Elems NP (Elem (Reclassified o)) xs
cs) -> NP (Reclassified (Elem o)) xs -> ReclassifiedElems o xs
forall (o :: * -> *) (xs :: [*]).
NP (Reclassified (Elem o)) xs -> ReclassifiedElems o xs
go (NP (Reclassified (Elem o)) xs -> ReclassifiedElems o xs)
-> NP (Reclassified (Elem o)) xs -> ReclassifiedElems o xs
forall a b. (a -> b) -> a -> b
$ (forall a. Elem (Reclassified o) a -> Reclassified (Elem o) a)
-> NP (Elem (Reclassified o)) xs -> NP (Reclassified (Elem o)) xs
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 (Reclassified o) a -> Reclassified (Elem o) a
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 :: NP (Reclassified (Elem o)) xs -> ReclassifiedElems o xs
go NP (Reclassified (Elem o)) xs
Nil = Elems o '[] -> PairWise FromUsr '[] '[] -> ReclassifiedElems o '[]
forall (bs :: [*]) (as :: [*]) (o :: * -> *).
(SListI bs, Length bs ~ Length as) =>
Elems o bs -> PairWise FromUsr as bs -> ReclassifiedElems o as
RElems (NP (Elem o) '[] -> Elems o '[]
forall (o :: * -> *) (xs :: [*]). NP (Elem o) xs -> Elems o xs
Elems NP (Elem o) '[]
forall k (a :: k -> *). NP a '[]
Nil) PairWise FromUsr '[] '[]
forall (f :: * -> * -> *). PairWise f '[] '[]
PNil
go (Reclassified Elem o b
c FromUsr x b
f :* NP (Reclassified (Elem o)) xs
cs) = case NP (Reclassified (Elem o)) xs -> ReclassifiedElems o xs
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' ->
Elems o (b : bs)
-> PairWise FromUsr (x : xs) (b : bs)
-> ReclassifiedElems o (x : xs)
forall (bs :: [*]) (as :: [*]) (o :: * -> *).
(SListI bs, Length bs ~ Length as) =>
Elems o bs -> PairWise FromUsr as bs -> ReclassifiedElems o as
RElems (NP (Elem o) (b : bs) -> Elems o (b : bs)
forall (o :: * -> *) (xs :: [*]). NP (Elem o) xs -> Elems o xs
Elems (Elem o b
c Elem o b -> NP (Elem o) bs -> NP (Elem o) (b : bs)
forall k (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP (Elem o) bs
cs')) (FromUsr x b
-> PairWise FromUsr xs bs -> PairWise FromUsr (x : xs) (b : bs)
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')
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
coerceFromUsr :: FromUsr a b -> a -> b
coerceFromUsr :: FromUsr a b -> a -> b
coerceFromUsr = FromUsr a b -> a -> b
forall a b. a -> b
unsafeCoerce