{-# 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 (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
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
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
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')
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 :: forall a b. FromUsr a b -> a -> b
coerceFromUsr = forall a b. a -> b
unsafeCoerce