{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Generics.Simplistic.Deep
(
HolesAnn(..)
, SFix , pattern SFix , pattern Prim
, SFixAnn , pattern SFixAnn , pattern PrimAnn
, Holes , pattern Roll , pattern Hole
, CompoundCnstr , PrimCnstr
, holesToSFix , sfixToHoles
, holesMapAnn , holesMap , holesMapM , holesMapAnnM , getAnn
, holesJoin , holesSize, holesHolesList
, holesRefineM , holesRefineHoles , holesRefineHolesM
, synthesize , synthesizeM , cataM
, lgg
, Deep(..) , GDeep(..)
) where
import Data.Proxy
import Control.Monad.Identity
import Control.DeepSeq
import GHC.Generics (from , to)
import Unsafe.Coerce
import Generics.Simplistic
import Generics.Simplistic.Util
type PrimCnstr kappa fam b
= (Elem b kappa , NotElem b fam)
type CompoundCnstr kappa fam a
= (Elem a fam , NotElem a kappa , Generic a)
data HolesAnn kappa fam ann h a where
Hole' :: ann a
-> h a -> HolesAnn kappa fam ann h a
Prim' :: (PrimCnstr kappa fam a)
=> ann a
-> a -> HolesAnn kappa fam ann h a
Roll' :: (CompoundCnstr kappa fam a)
=> ann a
-> SRep (HolesAnn kappa fam ann h) (Rep a)
-> HolesAnn kappa fam ann h a
instance (All Eq kappa , EqHO h) => EqHO (Holes kappa fam h) where
eqHO :: Holes kappa fam h k -> Holes kappa fam h k -> Bool
eqHO x :: Holes kappa fam h k
x y :: Holes kappa fam h k
y = (Exists (Holes kappa fam h :*: Holes kappa fam h) -> Bool)
-> [Exists (Holes kappa fam h :*: Holes kappa fam h)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((forall x. (:*:) (Holes kappa fam h) (Holes kappa fam h) x -> Bool)
-> Exists (Holes kappa fam h :*: Holes kappa fam h) -> Bool
forall k (f :: k -> *) a.
(forall (x :: k). f x -> a) -> Exists f -> a
exElim ((forall x.
(:*:) (Holes kappa fam h) (Holes kappa fam h) x -> Bool)
-> Exists (Holes kappa fam h :*: Holes kappa fam h) -> Bool)
-> (forall x.
(:*:) (Holes kappa fam h) (Holes kappa fam h) x -> Bool)
-> Exists (Holes kappa fam h :*: Holes kappa fam h)
-> Bool
forall a b. (a -> b) -> a -> b
$ (HolesAnn kappa fam U1 h x -> HolesAnn kappa fam U1 h x -> Bool)
-> (:*:) (Holes kappa fam h) (Holes kappa fam h) x -> Bool
forall k (f :: k -> *) (x :: k) (g :: k -> *) a.
(f x -> g x -> a) -> (:*:) f g x -> a
uncurry' HolesAnn kappa fam U1 h x -> HolesAnn kappa fam U1 h x -> Bool
forall k. Holes kappa fam h k -> Holes kappa fam h k -> Bool
go) ([Exists (Holes kappa fam h :*: Holes kappa fam h)] -> Bool)
-> [Exists (Holes kappa fam h :*: Holes kappa fam h)] -> Bool
forall a b. (a -> b) -> a -> b
$ HolesAnn kappa fam U1 (Holes kappa fam h :*: Holes kappa fam h) k
-> [Exists (Holes kappa fam h :*: Holes kappa fam h)]
forall (kappa :: [*]) (fam :: [*]) (ann :: * -> *) (f :: * -> *) a.
HolesAnn kappa fam ann f a -> [Exists f]
holesHolesList (Holes kappa fam h k
-> Holes kappa fam h k
-> HolesAnn
kappa fam U1 (Holes kappa fam h :*: Holes kappa fam h) k
forall (kappa :: [*]) (fam :: [*]) (h :: * -> *) (i :: * -> *) a.
All Eq kappa =>
Holes kappa fam h a
-> Holes kappa fam i a
-> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) a
lgg Holes kappa fam h k
x Holes kappa fam h k
y)
where
go :: Holes kappa fam h a -> Holes kappa fam h a -> Bool
go :: Holes kappa fam h a -> Holes kappa fam h a -> Bool
go (Hole h1 :: h a
h1) (Hole h2 :: h a
h2) = h a -> h a -> Bool
forall ki (f :: ki -> *) (k :: ki). EqHO f => f k -> f k -> Bool
eqHO h a
h1 h a
h2
go _ _ = Bool
False
instance (All Eq kappa , EqHO h) => Eq (Holes kappa fam h t) where
== :: Holes kappa fam h t -> Holes kappa fam h t -> Bool
(==) = Holes kappa fam h t -> Holes kappa fam h t -> Bool
forall ki (f :: ki -> *) (k :: ki). EqHO f => f k -> f k -> Bool
eqHO
type SFix kappa fam = HolesAnn kappa fam U1 V1
pattern SFix :: () => (CompoundCnstr kappa fam a)
=> SRep (SFix kappa fam) (Rep a)
-> SFix kappa fam a
pattern $bSFix :: SRep (SFix kappa fam) (Rep a) -> SFix kappa fam a
$mSFix :: forall r (kappa :: [*]) (fam :: [*]) a.
SFix kappa fam a
-> (CompoundCnstr kappa fam a =>
SRep (SFix kappa fam) (Rep a) -> r)
-> (Void# -> r)
-> r
SFix x = Roll x
{-# COMPLETE SFix , Prim #-}
type Holes kappa fam = HolesAnn kappa fam U1
pattern Hole :: h a -> Holes kappa fam h a
pattern $bHole :: h a -> Holes kappa fam h a
$mHole :: forall r (h :: * -> *) a (kappa :: [*]) (fam :: [*]).
Holes kappa fam h a -> (h a -> r) -> (Void# -> r) -> r
Hole x = Hole' U1 x
pattern Prim :: () => (PrimCnstr kappa fam a)
=> a -> Holes kappa fam h a
pattern $bPrim :: a -> Holes kappa fam h a
$mPrim :: forall r (kappa :: [*]) (fam :: [*]) a (h :: * -> *).
Holes kappa fam h a
-> (PrimCnstr kappa fam a => a -> r) -> (Void# -> r) -> r
Prim a = Prim' U1 a
pattern Roll :: () => (CompoundCnstr kappa fam a)
=> SRep (Holes kappa fam h) (Rep a)
-> Holes kappa fam h a
pattern $bRoll :: SRep (Holes kappa fam h) (Rep a) -> Holes kappa fam h a
$mRoll :: forall r (kappa :: [*]) (fam :: [*]) a (h :: * -> *).
Holes kappa fam h a
-> (CompoundCnstr kappa fam a =>
SRep (Holes kappa fam h) (Rep a) -> r)
-> (Void# -> r)
-> r
Roll x = Roll' U1 x
{-# COMPLETE Hole , Prim , Roll #-}
type SFixAnn kappa fam ann = HolesAnn kappa fam ann V1
pattern PrimAnn :: () => (PrimCnstr kappa fam a)
=> ann a -> a -> SFixAnn kappa fam ann a
pattern $bPrimAnn :: ann a -> a -> SFixAnn kappa fam ann a
$mPrimAnn :: forall r (kappa :: [*]) (fam :: [*]) a (ann :: * -> *).
SFixAnn kappa fam ann a
-> (PrimCnstr kappa fam a => ann a -> a -> r) -> (Void# -> r) -> r
PrimAnn ann a = Prim' ann a
pattern SFixAnn :: () => (CompoundCnstr kappa fam a)
=> ann a
-> SRep (SFixAnn kappa fam ann) (Rep a)
-> SFixAnn kappa fam ann a
pattern $bSFixAnn :: ann a
-> SRep (SFixAnn kappa fam ann) (Rep a) -> SFixAnn kappa fam ann a
$mSFixAnn :: forall r (kappa :: [*]) (fam :: [*]) a (ann :: * -> *).
SFixAnn kappa fam ann a
-> (CompoundCnstr kappa fam a =>
ann a -> SRep (SFixAnn kappa fam ann) (Rep a) -> r)
-> (Void# -> r)
-> r
SFixAnn ann x = Roll' ann x
{-# COMPLETE SFixAnn , PrimAnn #-}
sfixToHoles :: SFix kappa fam at -> Holes kappa fam h at
sfixToHoles :: SFix kappa fam at -> Holes kappa fam h at
sfixToHoles = SFix kappa fam at -> Holes kappa fam h at
forall a b. a -> b
unsafeCoerce
holesToSFix :: Holes kappa fam V1 at -> SFix kappa fam at
holesToSFix :: Holes kappa fam V1 at -> Holes kappa fam V1 at
holesToSFix = Holes kappa fam V1 at -> Holes kappa fam V1 at
forall a. a -> a
id
instance (forall x . NFData (ann x) , forall x . NFData (h x))
=> NFData (HolesAnn kappa fam ann h f) where
rnf :: HolesAnn kappa fam ann h f -> ()
rnf (Prim' ann :: ann f
ann _) = ann f -> ()
forall a. NFData a => a -> ()
rnf ann f
ann
rnf (Hole' ann :: ann f
ann h :: h f
h) = ann f -> ()
forall a. NFData a => a -> ()
rnf ann f
ann () -> () -> ()
forall a b. a -> b -> b
`seq` h f -> ()
forall a. NFData a => a -> ()
rnf h f
h
rnf (Roll' ann :: ann f
ann x :: SRep (HolesAnn kappa fam ann h) (Rep f)
x) = ann f -> ()
forall a. NFData a => a -> ()
rnf ann f
ann () -> () -> ()
forall a b. a -> b -> b
`seq` SRep (HolesAnn kappa fam ann h) (Rep f) -> ()
forall a. NFData a => a -> ()
rnf SRep (HolesAnn kappa fam ann h) (Rep f)
x
instance NFData (V1 x) where
rnf :: V1 x -> ()
rnf _ = ()
instance NFData (U1 x) where
rnf :: U1 x -> ()
rnf U1 = ()
getAnn :: HolesAnn kappa fam ann h a -> ann a
getAnn :: HolesAnn kappa fam ann h a -> ann a
getAnn (Hole' ann :: ann a
ann _) = ann a
ann
getAnn (Prim' ann :: ann a
ann _) = ann a
ann
getAnn (Roll' ann :: ann a
ann _) = ann a
ann
holesMapAnnM :: (Monad m)
=> (forall x . f x -> m (g x))
-> (forall x . ann x -> m (psi x))
-> HolesAnn kappa fam ann f a -> m (HolesAnn kappa fam psi g a)
holesMapAnnM :: (forall x. f x -> m (g x))
-> (forall x. ann x -> m (psi x))
-> HolesAnn kappa fam ann f a
-> m (HolesAnn kappa fam psi g a)
holesMapAnnM f :: forall x. f x -> m (g x)
f g :: forall x. ann x -> m (psi x)
g (Hole' a :: ann a
a x :: f a
x) = psi a -> g a -> HolesAnn kappa fam psi g a
forall (ann :: * -> *) a (h :: * -> *) (kappa :: [*]) (fam :: [*]).
ann a -> h a -> HolesAnn kappa fam ann h a
Hole' (psi a -> g a -> HolesAnn kappa fam psi g a)
-> m (psi a) -> m (g a -> HolesAnn kappa fam psi g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ann a -> m (psi a)
forall x. ann x -> m (psi x)
g ann a
a m (g a -> HolesAnn kappa fam psi g a)
-> m (g a) -> m (HolesAnn kappa fam psi g a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f a -> m (g a)
forall x. f x -> m (g x)
f f a
x
holesMapAnnM _ g :: forall x. ann x -> m (psi x)
g (Prim' a :: ann a
a x :: a
x) = (psi a -> a -> HolesAnn kappa fam psi g a)
-> a -> psi a -> HolesAnn kappa fam psi g a
forall a b c. (a -> b -> c) -> b -> a -> c
flip psi a -> a -> HolesAnn kappa fam psi g a
forall (kappa :: [*]) (fam :: [*]) a (ann :: * -> *) (h :: * -> *).
PrimCnstr kappa fam a =>
ann a -> a -> HolesAnn kappa fam ann h a
Prim' a
x (psi a -> HolesAnn kappa fam psi g a)
-> m (psi a) -> m (HolesAnn kappa fam psi g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ann a -> m (psi a)
forall x. ann x -> m (psi x)
g ann a
a
holesMapAnnM f :: forall x. f x -> m (g x)
f g :: forall x. ann x -> m (psi x)
g (Roll' a :: ann a
a x :: SRep (HolesAnn kappa fam ann f) (Rep a)
x) = psi a
-> SRep (HolesAnn kappa fam psi g) (Rep a)
-> HolesAnn kappa fam psi g a
forall (kappa :: [*]) (fam :: [*]) a (ann :: * -> *) (h :: * -> *).
CompoundCnstr kappa fam a =>
ann a
-> SRep (HolesAnn kappa fam ann h) (Rep a)
-> HolesAnn kappa fam ann h a
Roll' (psi a
-> SRep (HolesAnn kappa fam psi g) (Rep a)
-> HolesAnn kappa fam psi g a)
-> m (psi a)
-> m (SRep (HolesAnn kappa fam psi g) (Rep a)
-> HolesAnn kappa fam psi g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ann a -> m (psi a)
forall x. ann x -> m (psi x)
g ann a
a m (SRep (HolesAnn kappa fam psi g) (Rep a)
-> HolesAnn kappa fam psi g a)
-> m (SRep (HolesAnn kappa fam psi g) (Rep a))
-> m (HolesAnn kappa fam psi g a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall y.
HolesAnn kappa fam ann f y -> m (HolesAnn kappa fam psi g y))
-> SRep (HolesAnn kappa fam ann f) (Rep a)
-> m (SRep (HolesAnn kappa fam psi g) (Rep a))
forall k (m :: * -> *) (f :: * -> *) (g :: * -> *) (rep :: k -> *).
Monad m =>
(forall y. f y -> m (g y)) -> SRep f rep -> m (SRep g rep)
repMapM ((forall x. f x -> m (g x))
-> (forall x. ann x -> m (psi x))
-> HolesAnn kappa fam ann f y
-> m (HolesAnn kappa fam psi g y)
forall (m :: * -> *) (f :: * -> *) (g :: * -> *) (ann :: * -> *)
(psi :: * -> *) (kappa :: [*]) (fam :: [*]) a.
Monad m =>
(forall x. f x -> m (g x))
-> (forall x. ann x -> m (psi x))
-> HolesAnn kappa fam ann f a
-> m (HolesAnn kappa fam psi g a)
holesMapAnnM forall x. f x -> m (g x)
f forall x. ann x -> m (psi x)
g) SRep (HolesAnn kappa fam ann f) (Rep a)
x
holesMapM :: (Monad m)
=> (forall x . f x -> m (g x))
-> HolesAnn kappa fam ann f a -> m (HolesAnn kappa fam ann g a)
holesMapM :: (forall x. f x -> m (g x))
-> HolesAnn kappa fam ann f a -> m (HolesAnn kappa fam ann g a)
holesMapM f :: forall x. f x -> m (g x)
f = (forall x. f x -> m (g x))
-> (forall x. ann x -> m (ann x))
-> HolesAnn kappa fam ann f a
-> m (HolesAnn kappa fam ann g a)
forall (m :: * -> *) (f :: * -> *) (g :: * -> *) (ann :: * -> *)
(psi :: * -> *) (kappa :: [*]) (fam :: [*]) a.
Monad m =>
(forall x. f x -> m (g x))
-> (forall x. ann x -> m (psi x))
-> HolesAnn kappa fam ann f a
-> m (HolesAnn kappa fam psi g a)
holesMapAnnM forall x. f x -> m (g x)
f forall x. ann x -> m (ann x)
forall (m :: * -> *) a. Monad m => a -> m a
return
holesMap :: (forall x . f x -> g x)
-> HolesAnn kappa fam ann f a -> HolesAnn kappa fam ann g a
holesMap :: (forall x. f x -> g x)
-> HolesAnn kappa fam ann f a -> HolesAnn kappa fam ann g a
holesMap f :: forall x. f x -> g x
f = Identity (HolesAnn kappa fam ann g a) -> HolesAnn kappa fam ann g a
forall a. Identity a -> a
runIdentity (Identity (HolesAnn kappa fam ann g a)
-> HolesAnn kappa fam ann g a)
-> (HolesAnn kappa fam ann f a
-> Identity (HolesAnn kappa fam ann g a))
-> HolesAnn kappa fam ann f a
-> HolesAnn kappa fam ann g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall x. f x -> Identity (g x))
-> HolesAnn kappa fam ann f a
-> Identity (HolesAnn kappa fam ann g a)
forall (m :: * -> *) (f :: * -> *) (g :: * -> *) (kappa :: [*])
(fam :: [*]) (ann :: * -> *) a.
Monad m =>
(forall x. f x -> m (g x))
-> HolesAnn kappa fam ann f a -> m (HolesAnn kappa fam ann g a)
holesMapM (g x -> Identity (g x)
forall (m :: * -> *) a. Monad m => a -> m a
return (g x -> Identity (g x)) -> (f x -> g x) -> f x -> Identity (g x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> g x
forall x. f x -> g x
f)
holesMapAnn :: (forall x . f x -> g x)
-> (forall x . ann x -> phi x)
-> HolesAnn kappa fam ann f a -> HolesAnn kappa fam phi g a
holesMapAnn :: (forall x. f x -> g x)
-> (forall x. ann x -> phi x)
-> HolesAnn kappa fam ann f a
-> HolesAnn kappa fam phi g a
holesMapAnn f :: forall x. f x -> g x
f g :: forall x. ann x -> phi x
g = Identity (HolesAnn kappa fam phi g a) -> HolesAnn kappa fam phi g a
forall a. Identity a -> a
runIdentity (Identity (HolesAnn kappa fam phi g a)
-> HolesAnn kappa fam phi g a)
-> (HolesAnn kappa fam ann f a
-> Identity (HolesAnn kappa fam phi g a))
-> HolesAnn kappa fam ann f a
-> HolesAnn kappa fam phi g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall x. f x -> Identity (g x))
-> (forall x. ann x -> Identity (phi x))
-> HolesAnn kappa fam ann f a
-> Identity (HolesAnn kappa fam phi g a)
forall (m :: * -> *) (f :: * -> *) (g :: * -> *) (ann :: * -> *)
(psi :: * -> *) (kappa :: [*]) (fam :: [*]) a.
Monad m =>
(forall x. f x -> m (g x))
-> (forall x. ann x -> m (psi x))
-> HolesAnn kappa fam ann f a
-> m (HolesAnn kappa fam psi g a)
holesMapAnnM (g x -> Identity (g x)
forall (m :: * -> *) a. Monad m => a -> m a
return (g x -> Identity (g x)) -> (f x -> g x) -> f x -> Identity (g x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> g x
forall x. f x -> g x
f) (phi x -> Identity (phi x)
forall (m :: * -> *) a. Monad m => a -> m a
return (phi x -> Identity (phi x))
-> (ann x -> phi x) -> ann x -> Identity (phi x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann x -> phi x
forall x. ann x -> phi x
g)
holesJoin :: HolesAnn kappa fam ann (HolesAnn kappa fam ann f) a
-> HolesAnn kappa fam ann f a
holesJoin :: HolesAnn kappa fam ann (HolesAnn kappa fam ann f) a
-> HolesAnn kappa fam ann f a
holesJoin (Hole' _ x :: HolesAnn kappa fam ann f a
x) = HolesAnn kappa fam ann f a
x
holesJoin (Prim' a :: ann a
a x :: a
x) = ann a -> a -> HolesAnn kappa fam ann f a
forall (kappa :: [*]) (fam :: [*]) a (ann :: * -> *) (h :: * -> *).
PrimCnstr kappa fam a =>
ann a -> a -> HolesAnn kappa fam ann h a
Prim' ann a
a a
x
holesJoin (Roll' a :: ann a
a x :: SRep (HolesAnn kappa fam ann (HolesAnn kappa fam ann f)) (Rep a)
x) = ann a
-> SRep (HolesAnn kappa fam ann f) (Rep a)
-> HolesAnn kappa fam ann f a
forall (kappa :: [*]) (fam :: [*]) a (ann :: * -> *) (h :: * -> *).
CompoundCnstr kappa fam a =>
ann a
-> SRep (HolesAnn kappa fam ann h) (Rep a)
-> HolesAnn kappa fam ann h a
Roll' ann a
a ((forall y.
HolesAnn kappa fam ann (HolesAnn kappa fam ann f) y
-> HolesAnn kappa fam ann f y)
-> SRep (HolesAnn kappa fam ann (HolesAnn kappa fam ann f)) (Rep a)
-> SRep (HolesAnn kappa fam ann f) (Rep a)
forall k (f :: * -> *) (g :: * -> *) (rep :: k -> *).
(forall y. f y -> g y) -> SRep f rep -> SRep g rep
repMap forall (kappa :: [*]) (fam :: [*]) (ann :: * -> *) (f :: * -> *) a.
HolesAnn kappa fam ann (HolesAnn kappa fam ann f) a
-> HolesAnn kappa fam ann f a
forall y.
HolesAnn kappa fam ann (HolesAnn kappa fam ann f) y
-> HolesAnn kappa fam ann f y
holesJoin SRep (HolesAnn kappa fam ann (HolesAnn kappa fam ann f)) (Rep a)
x)
holesHolesList :: HolesAnn kappa fam ann f a -> [Exists f]
holesHolesList :: HolesAnn kappa fam ann f a -> [Exists f]
holesHolesList (Hole' _ x :: f a
x) = [f a -> Exists f
forall k (f :: k -> *) (x :: k). f x -> Exists f
Exists f a
x]
holesHolesList (Prim' _ _) = []
holesHolesList (Roll' _ x :: SRep (HolesAnn kappa fam ann f) (Rep a)
x) = (Exists (HolesAnn kappa fam ann f) -> [Exists f])
-> [Exists (HolesAnn kappa fam ann f)] -> [Exists f]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((forall x. HolesAnn kappa fam ann f x -> [Exists f])
-> Exists (HolesAnn kappa fam ann f) -> [Exists f]
forall k (f :: k -> *) a.
(forall (x :: k). f x -> a) -> Exists f -> a
exElim forall (kappa :: [*]) (fam :: [*]) (ann :: * -> *) (f :: * -> *) a.
HolesAnn kappa fam ann f a -> [Exists f]
forall x. HolesAnn kappa fam ann f x -> [Exists f]
holesHolesList) ([Exists (HolesAnn kappa fam ann f)] -> [Exists f])
-> [Exists (HolesAnn kappa fam ann f)] -> [Exists f]
forall a b. (a -> b) -> a -> b
$ SRep (HolesAnn kappa fam ann f) (Rep a)
-> [Exists (HolesAnn kappa fam ann f)]
forall k (w :: * -> *) (rep :: k -> *). SRep w rep -> [Exists w]
repLeavesList SRep (HolesAnn kappa fam ann f) (Rep a)
x
holesRefineHolesM :: (Monad m)
=> (forall b . f b -> m (Holes kappa fam g b))
-> Holes kappa fam f a
-> m (Holes kappa fam g a)
holesRefineHolesM :: (forall b. f b -> m (Holes kappa fam g b))
-> Holes kappa fam f a -> m (Holes kappa fam g a)
holesRefineHolesM f :: forall b. f b -> m (Holes kappa fam g b)
f = (HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a
-> Holes kappa fam g a)
-> m (HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a)
-> m (Holes kappa fam g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a
-> Holes kappa fam g a
forall (kappa :: [*]) (fam :: [*]) (ann :: * -> *) (f :: * -> *) a.
HolesAnn kappa fam ann (HolesAnn kappa fam ann f) a
-> HolesAnn kappa fam ann f a
holesJoin (m (HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a)
-> m (Holes kappa fam g a))
-> (Holes kappa fam f a
-> m (HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a))
-> Holes kappa fam f a
-> m (Holes kappa fam g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall b. f b -> m (Holes kappa fam g b))
-> Holes kappa fam f a
-> m (HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a)
forall (m :: * -> *) (f :: * -> *) (g :: * -> *) (kappa :: [*])
(fam :: [*]) (ann :: * -> *) a.
Monad m =>
(forall x. f x -> m (g x))
-> HolesAnn kappa fam ann f a -> m (HolesAnn kappa fam ann g a)
holesMapM forall b. f b -> m (Holes kappa fam g b)
f
holesRefineHoles :: (forall b . f b -> Holes kappa fam g b)
-> Holes kappa fam f a
-> Holes kappa fam g a
holesRefineHoles :: (forall b. f b -> Holes kappa fam g b)
-> Holes kappa fam f a -> Holes kappa fam g a
holesRefineHoles f :: forall b. f b -> Holes kappa fam g b
f = HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a
-> Holes kappa fam g a
forall (kappa :: [*]) (fam :: [*]) (ann :: * -> *) (f :: * -> *) a.
HolesAnn kappa fam ann (HolesAnn kappa fam ann f) a
-> HolesAnn kappa fam ann f a
holesJoin (HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a
-> Holes kappa fam g a)
-> (Holes kappa fam f a
-> HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a)
-> Holes kappa fam f a
-> Holes kappa fam g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity (HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a)
-> HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a
forall a. Identity a -> a
runIdentity (Identity (HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a)
-> HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a)
-> (Holes kappa fam f a
-> Identity (HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a))
-> Holes kappa fam f a
-> HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall x. f x -> Identity (HolesAnn kappa fam U1 g x))
-> Holes kappa fam f a
-> Identity (HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a)
forall (m :: * -> *) (f :: * -> *) (g :: * -> *) (kappa :: [*])
(fam :: [*]) (ann :: * -> *) a.
Monad m =>
(forall x. f x -> m (g x))
-> HolesAnn kappa fam ann f a -> m (HolesAnn kappa fam ann g a)
holesMapM (Holes kappa fam g x -> Identity (Holes kappa fam g x)
forall (m :: * -> *) a. Monad m => a -> m a
return (Holes kappa fam g x -> Identity (Holes kappa fam g x))
-> (f x -> Holes kappa fam g x)
-> f x
-> Identity (Holes kappa fam g x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> Holes kappa fam g x
forall b. f b -> Holes kappa fam g b
f)
holesRefineM :: (Monad m)
=> (forall b . f b -> m (Holes kappa fam g b))
-> (forall b . (PrimCnstr kappa fam b)
=> b -> m (Holes kappa fam g b))
-> Holes kappa fam f a
-> m (Holes kappa fam g a)
holesRefineM :: (forall b. f b -> m (Holes kappa fam g b))
-> (forall b.
PrimCnstr kappa fam b =>
b -> m (Holes kappa fam g b))
-> Holes kappa fam f a
-> m (Holes kappa fam g a)
holesRefineM f :: forall b. f b -> m (Holes kappa fam g b)
f _ (Hole x :: f a
x) = f a -> m (Holes kappa fam g a)
forall b. f b -> m (Holes kappa fam g b)
f f a
x
holesRefineM _ g :: forall b. PrimCnstr kappa fam b => b -> m (Holes kappa fam g b)
g (Prim x :: a
x) = a -> m (Holes kappa fam g a)
forall b. PrimCnstr kappa fam b => b -> m (Holes kappa fam g b)
g a
x
holesRefineM f :: forall b. f b -> m (Holes kappa fam g b)
f g :: forall b. PrimCnstr kappa fam b => b -> m (Holes kappa fam g b)
g (Roll x :: SRep (Holes kappa fam f) (Rep a)
x) = SRep (Holes kappa fam g) (Rep a) -> Holes kappa fam g a
forall (kappa :: [*]) (fam :: [*]) a (h :: * -> *).
CompoundCnstr kappa fam a =>
SRep (Holes kappa fam h) (Rep a) -> Holes kappa fam h a
Roll (SRep (Holes kappa fam g) (Rep a) -> Holes kappa fam g a)
-> m (SRep (Holes kappa fam g) (Rep a)) -> m (Holes kappa fam g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall y. Holes kappa fam f y -> m (Holes kappa fam g y))
-> SRep (Holes kappa fam f) (Rep a)
-> m (SRep (Holes kappa fam g) (Rep a))
forall k (m :: * -> *) (f :: * -> *) (g :: * -> *) (rep :: k -> *).
Monad m =>
(forall y. f y -> m (g y)) -> SRep f rep -> m (SRep g rep)
repMapM ((forall b. f b -> m (Holes kappa fam g b))
-> (forall b.
PrimCnstr kappa fam b =>
b -> m (Holes kappa fam g b))
-> Holes kappa fam f y
-> m (Holes kappa fam g y)
forall (m :: * -> *) (f :: * -> *) (kappa :: [*]) (fam :: [*])
(g :: * -> *) a.
Monad m =>
(forall b. f b -> m (Holes kappa fam g b))
-> (forall b.
PrimCnstr kappa fam b =>
b -> m (Holes kappa fam g b))
-> Holes kappa fam f a
-> m (Holes kappa fam g a)
holesRefineM forall b. f b -> m (Holes kappa fam g b)
f forall b. PrimCnstr kappa fam b => b -> m (Holes kappa fam g b)
g) SRep (Holes kappa fam f) (Rep a)
x
holesSize :: HolesAnn kappa fam ann h a -> Int
holesSize :: HolesAnn kappa fam ann h a -> Int
holesSize (Hole' _ _) = 0
holesSize (Prim' _ _) = 1
holesSize (Roll' _ x :: SRep (HolesAnn kappa fam ann h) (Rep a)
x) = 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((Exists (HolesAnn kappa fam ann h) -> Int)
-> [Exists (HolesAnn kappa fam ann h)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map ((forall x. HolesAnn kappa fam ann h x -> Int)
-> Exists (HolesAnn kappa fam ann h) -> Int
forall k (f :: k -> *) a.
(forall (x :: k). f x -> a) -> Exists f -> a
exElim forall (kappa :: [*]) (fam :: [*]) (ann :: * -> *) (h :: * -> *) a.
HolesAnn kappa fam ann h a -> Int
forall x. HolesAnn kappa fam ann h x -> Int
holesSize) ([Exists (HolesAnn kappa fam ann h)] -> [Int])
-> [Exists (HolesAnn kappa fam ann h)] -> [Int]
forall a b. (a -> b) -> a -> b
$ SRep (HolesAnn kappa fam ann h) (Rep a)
-> [Exists (HolesAnn kappa fam ann h)]
forall k (w :: * -> *) (rep :: k -> *). SRep w rep -> [Exists w]
repLeavesList SRep (HolesAnn kappa fam ann h) (Rep a)
x)
cataM :: (Monad m)
=> (forall b . (CompoundCnstr kappa fam b)
=> ann b -> SRep phi (Rep b) -> m (phi b))
-> (forall b . (PrimCnstr kappa fam b)
=> ann b -> b -> m (phi b))
-> (forall b . ann b -> h b -> m (phi b))
-> HolesAnn kappa fam ann h a
-> m (phi a)
cataM :: (forall b.
CompoundCnstr kappa fam b =>
ann b -> SRep phi (Rep b) -> m (phi b))
-> (forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b))
-> (forall b. ann b -> h b -> m (phi b))
-> HolesAnn kappa fam ann h a
-> m (phi a)
cataM f :: forall b.
CompoundCnstr kappa fam b =>
ann b -> SRep phi (Rep b) -> m (phi b)
f g :: forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b)
g h :: forall b. ann b -> h b -> m (phi b)
h (Roll' ann :: ann a
ann x :: SRep (HolesAnn kappa fam ann h) (Rep a)
x) = (forall y. HolesAnn kappa fam ann h y -> m (phi y))
-> SRep (HolesAnn kappa fam ann h) (Rep a) -> m (SRep phi (Rep a))
forall k (m :: * -> *) (f :: * -> *) (g :: * -> *) (rep :: k -> *).
Monad m =>
(forall y. f y -> m (g y)) -> SRep f rep -> m (SRep g rep)
repMapM ((forall b.
CompoundCnstr kappa fam b =>
ann b -> SRep phi (Rep b) -> m (phi b))
-> (forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b))
-> (forall b. ann b -> h b -> m (phi b))
-> HolesAnn kappa fam ann h y
-> m (phi y)
forall (m :: * -> *) (kappa :: [*]) (fam :: [*]) (ann :: * -> *)
(phi :: * -> *) (h :: * -> *) a.
Monad m =>
(forall b.
CompoundCnstr kappa fam b =>
ann b -> SRep phi (Rep b) -> m (phi b))
-> (forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b))
-> (forall b. ann b -> h b -> m (phi b))
-> HolesAnn kappa fam ann h a
-> m (phi a)
cataM forall b.
CompoundCnstr kappa fam b =>
ann b -> SRep phi (Rep b) -> m (phi b)
f forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b)
g forall b. ann b -> h b -> m (phi b)
h) SRep (HolesAnn kappa fam ann h) (Rep a)
x m (SRep phi (Rep a))
-> (SRep phi (Rep a) -> m (phi a)) -> m (phi a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ann a -> SRep phi (Rep a) -> m (phi a)
forall b.
CompoundCnstr kappa fam b =>
ann b -> SRep phi (Rep b) -> m (phi b)
f ann a
ann
cataM _ g :: forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b)
g _ (Prim' ann :: ann a
ann x :: a
x) = ann a -> a -> m (phi a)
forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b)
g ann a
ann a
x
cataM _ _ h :: forall b. ann b -> h b -> m (phi b)
h (Hole' ann :: ann a
ann x :: h a
x) = ann a -> h a -> m (phi a)
forall b. ann b -> h b -> m (phi b)
h ann a
ann h a
x
synthesizeM :: (Monad m)
=> (forall b . (CompoundCnstr kappa fam b)
=> ann b -> SRep phi (Rep b) -> m (phi b))
-> (forall b . (PrimCnstr kappa fam b)
=> ann b -> b -> m (phi b))
-> (forall b . ann b -> h b -> m (phi b))
-> HolesAnn kappa fam ann h a
-> m (HolesAnn kappa fam phi h a)
synthesizeM :: (forall b.
CompoundCnstr kappa fam b =>
ann b -> SRep phi (Rep b) -> m (phi b))
-> (forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b))
-> (forall b. ann b -> h b -> m (phi b))
-> HolesAnn kappa fam ann h a
-> m (HolesAnn kappa fam phi h a)
synthesizeM f :: forall b.
CompoundCnstr kappa fam b =>
ann b -> SRep phi (Rep b) -> m (phi b)
f g :: forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b)
g h :: forall b. ann b -> h b -> m (phi b)
h = (forall b.
CompoundCnstr kappa fam b =>
ann b
-> SRep (HolesAnn kappa fam phi h) (Rep b)
-> m (HolesAnn kappa fam phi h b))
-> (forall b.
PrimCnstr kappa fam b =>
ann b -> b -> m (HolesAnn kappa fam phi h b))
-> (forall b. ann b -> h b -> m (HolesAnn kappa fam phi h b))
-> HolesAnn kappa fam ann h a
-> m (HolesAnn kappa fam phi h a)
forall (m :: * -> *) (kappa :: [*]) (fam :: [*]) (ann :: * -> *)
(phi :: * -> *) (h :: * -> *) a.
Monad m =>
(forall b.
CompoundCnstr kappa fam b =>
ann b -> SRep phi (Rep b) -> m (phi b))
-> (forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b))
-> (forall b. ann b -> h b -> m (phi b))
-> HolesAnn kappa fam ann h a
-> m (phi a)
cataM (\ann :: ann b
ann r :: SRep (HolesAnn kappa fam phi h) (Rep b)
r -> (phi b
-> SRep (HolesAnn kappa fam phi h) (Rep b)
-> HolesAnn kappa fam phi h b)
-> SRep (HolesAnn kappa fam phi h) (Rep b)
-> phi b
-> HolesAnn kappa fam phi h b
forall a b c. (a -> b -> c) -> b -> a -> c
flip phi b
-> SRep (HolesAnn kappa fam phi h) (Rep b)
-> HolesAnn kappa fam phi h b
forall (kappa :: [*]) (fam :: [*]) a (ann :: * -> *) (h :: * -> *).
CompoundCnstr kappa fam a =>
ann a
-> SRep (HolesAnn kappa fam ann h) (Rep a)
-> HolesAnn kappa fam ann h a
Roll' SRep (HolesAnn kappa fam phi h) (Rep b)
r
(phi b -> HolesAnn kappa fam phi h b)
-> m (phi b) -> m (HolesAnn kappa fam phi h b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ann b -> SRep phi (Rep b) -> m (phi b)
forall b.
CompoundCnstr kappa fam b =>
ann b -> SRep phi (Rep b) -> m (phi b)
f ann b
ann ((forall y. HolesAnn kappa fam phi h y -> phi y)
-> SRep (HolesAnn kappa fam phi h) (Rep b) -> SRep phi (Rep b)
forall k (f :: * -> *) (g :: * -> *) (rep :: k -> *).
(forall y. f y -> g y) -> SRep f rep -> SRep g rep
repMap forall (kappa :: [*]) (fam :: [*]) (ann :: * -> *) (h :: * -> *) a.
HolesAnn kappa fam ann h a -> ann a
forall y. HolesAnn kappa fam phi h y -> phi y
getAnn SRep (HolesAnn kappa fam phi h) (Rep b)
r))
(\ann :: ann b
ann b :: b
b -> (phi b -> b -> HolesAnn kappa fam phi h b)
-> b -> phi b -> HolesAnn kappa fam phi h b
forall a b c. (a -> b -> c) -> b -> a -> c
flip phi b -> b -> HolesAnn kappa fam phi h b
forall (kappa :: [*]) (fam :: [*]) a (ann :: * -> *) (h :: * -> *).
PrimCnstr kappa fam a =>
ann a -> a -> HolesAnn kappa fam ann h a
Prim' b
b (phi b -> HolesAnn kappa fam phi h b)
-> m (phi b) -> m (HolesAnn kappa fam phi h b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ann b -> b -> m (phi b)
forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b)
g ann b
ann b
b)
(\ann :: ann b
ann r :: h b
r -> (phi b -> h b -> HolesAnn kappa fam phi h b)
-> h b -> phi b -> HolesAnn kappa fam phi h b
forall a b c. (a -> b -> c) -> b -> a -> c
flip phi b -> h b -> HolesAnn kappa fam phi h b
forall (ann :: * -> *) a (h :: * -> *) (kappa :: [*]) (fam :: [*]).
ann a -> h a -> HolesAnn kappa fam ann h a
Hole' h b
r (phi b -> HolesAnn kappa fam phi h b)
-> m (phi b) -> m (HolesAnn kappa fam phi h b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ann b -> h b -> m (phi b)
forall b. ann b -> h b -> m (phi b)
h ann b
ann h b
r)
synthesize :: (forall b . (CompoundCnstr kappa fam b)
=> ann b -> SRep phi (Rep b) -> phi b)
-> (forall b . (PrimCnstr kappa fam b)
=> ann b -> b -> phi b)
-> (forall b . ann b -> h b -> phi b)
-> HolesAnn kappa fam ann h a
-> HolesAnn kappa fam phi h a
synthesize :: (forall b.
CompoundCnstr kappa fam b =>
ann b -> SRep phi (Rep b) -> phi b)
-> (forall b. PrimCnstr kappa fam b => ann b -> b -> phi b)
-> (forall b. ann b -> h b -> phi b)
-> HolesAnn kappa fam ann h a
-> HolesAnn kappa fam phi h a
synthesize f :: forall b.
CompoundCnstr kappa fam b =>
ann b -> SRep phi (Rep b) -> phi b
f g :: forall b. PrimCnstr kappa fam b => ann b -> b -> phi b
g h :: forall b. ann b -> h b -> phi b
h = Identity (HolesAnn kappa fam phi h a) -> HolesAnn kappa fam phi h a
forall a. Identity a -> a
runIdentity
(Identity (HolesAnn kappa fam phi h a)
-> HolesAnn kappa fam phi h a)
-> (HolesAnn kappa fam ann h a
-> Identity (HolesAnn kappa fam phi h a))
-> HolesAnn kappa fam ann h a
-> HolesAnn kappa fam phi h a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall b.
CompoundCnstr kappa fam b =>
ann b -> SRep phi (Rep b) -> Identity (phi b))
-> (forall b.
PrimCnstr kappa fam b =>
ann b -> b -> Identity (phi b))
-> (forall b. ann b -> h b -> Identity (phi b))
-> HolesAnn kappa fam ann h a
-> Identity (HolesAnn kappa fam phi h a)
forall (m :: * -> *) (kappa :: [*]) (fam :: [*]) (ann :: * -> *)
(phi :: * -> *) (h :: * -> *) a.
Monad m =>
(forall b.
CompoundCnstr kappa fam b =>
ann b -> SRep phi (Rep b) -> m (phi b))
-> (forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b))
-> (forall b. ann b -> h b -> m (phi b))
-> HolesAnn kappa fam ann h a
-> m (HolesAnn kappa fam phi h a)
synthesizeM (\ann :: ann b
ann -> phi b -> Identity (phi b)
forall (m :: * -> *) a. Monad m => a -> m a
return (phi b -> Identity (phi b))
-> (SRep phi (Rep b) -> phi b)
-> SRep phi (Rep b)
-> Identity (phi b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann b -> SRep phi (Rep b) -> phi b
forall b.
CompoundCnstr kappa fam b =>
ann b -> SRep phi (Rep b) -> phi b
f ann b
ann)
(\ann :: ann b
ann -> phi b -> Identity (phi b)
forall (m :: * -> *) a. Monad m => a -> m a
return (phi b -> Identity (phi b))
-> (b -> phi b) -> b -> Identity (phi b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann b -> b -> phi b
forall b. PrimCnstr kappa fam b => ann b -> b -> phi b
g ann b
ann)
(\ann :: ann b
ann -> phi b -> Identity (phi b)
forall (m :: * -> *) a. Monad m => a -> m a
return (phi b -> Identity (phi b))
-> (h b -> phi b) -> h b -> Identity (phi b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann b -> h b -> phi b
forall b. ann b -> h b -> phi b
h ann b
ann)
lgg :: forall kappa fam h i a
. (All Eq kappa)
=> Holes kappa fam h a -> Holes kappa fam i a
-> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) a
lgg :: Holes kappa fam h a
-> Holes kappa fam i a
-> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) a
lgg (Prim x :: a
x) (Prim y :: a
y)
| Proxy kappa -> a -> a -> Bool
forall x (xs :: [*]).
(All Eq xs, Elem x xs) =>
Proxy xs -> x -> x -> Bool
weq (Proxy kappa
forall k (t :: k). Proxy t
Proxy :: Proxy kappa) a
x a
y = a -> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) a
forall (kappa :: [*]) (fam :: [*]) a (h :: * -> *).
PrimCnstr kappa fam a =>
a -> Holes kappa fam h a
Prim a
x
| Bool
otherwise = (:*:) (Holes kappa fam h) (Holes kappa fam i) a
-> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) a
forall (h :: * -> *) a (kappa :: [*]) (fam :: [*]).
h a -> Holes kappa fam h a
Hole (a -> Holes kappa fam h a
forall (kappa :: [*]) (fam :: [*]) a (h :: * -> *).
PrimCnstr kappa fam a =>
a -> Holes kappa fam h a
Prim a
x Holes kappa fam h a
-> Holes kappa fam i a
-> (:*:) (Holes kappa fam h) (Holes kappa fam i) a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: a -> Holes kappa fam i a
forall (kappa :: [*]) (fam :: [*]) a (h :: * -> *).
PrimCnstr kappa fam a =>
a -> Holes kappa fam h a
Prim a
y)
lgg x :: Holes kappa fam h a
x@(Roll rx :: SRep (Holes kappa fam h) (Rep a)
rx) y :: Holes kappa fam i a
y@(Roll ry :: SRep (Holes kappa fam i) (Rep a)
ry) =
case SRep (Holes kappa fam h) (Rep a)
-> SRep (Holes kappa fam i) (Rep a)
-> Maybe (SRep (Holes kappa fam h :*: Holes kappa fam i) (Rep a))
forall k (w :: * -> *) (f :: k -> *) (z :: * -> *).
SRep w f -> SRep z f -> Maybe (SRep (w :*: z) f)
zipSRep SRep (Holes kappa fam h) (Rep a)
rx SRep (Holes kappa fam i) (Rep a)
ry of
Nothing -> (:*:) (Holes kappa fam h) (Holes kappa fam i) a
-> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) a
forall (h :: * -> *) a (kappa :: [*]) (fam :: [*]).
h a -> Holes kappa fam h a
Hole (Holes kappa fam h a
x Holes kappa fam h a
-> Holes kappa fam i a
-> (:*:) (Holes kappa fam h) (Holes kappa fam i) a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Holes kappa fam i a
y)
Just r :: SRep (Holes kappa fam h :*: Holes kappa fam i) (Rep a)
r -> SRep
(Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i)) (Rep a)
-> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) a
forall (kappa :: [*]) (fam :: [*]) a (h :: * -> *).
CompoundCnstr kappa fam a =>
SRep (Holes kappa fam h) (Rep a) -> Holes kappa fam h a
Roll ((forall y.
(:*:) (Holes kappa fam h) (Holes kappa fam i) y
-> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) y)
-> SRep (Holes kappa fam h :*: Holes kappa fam i) (Rep a)
-> SRep
(Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i)) (Rep a)
forall k (f :: * -> *) (g :: * -> *) (rep :: k -> *).
(forall y. f y -> g y) -> SRep f rep -> SRep g rep
repMap ((HolesAnn kappa fam U1 h y
-> HolesAnn kappa fam U1 i y
-> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) y)
-> (:*:) (Holes kappa fam h) (Holes kappa fam i) y
-> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) y
forall k (f :: k -> *) (x :: k) (g :: k -> *) a.
(f x -> g x -> a) -> (:*:) f g x -> a
uncurry' HolesAnn kappa fam U1 h y
-> HolesAnn kappa fam U1 i y
-> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) y
forall (kappa :: [*]) (fam :: [*]) (h :: * -> *) (i :: * -> *) a.
All Eq kappa =>
Holes kappa fam h a
-> Holes kappa fam i a
-> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) a
lgg) SRep (Holes kappa fam h :*: Holes kappa fam i) (Rep a)
r)
lgg x :: Holes kappa fam h a
x y :: Holes kappa fam i a
y = (:*:) (Holes kappa fam h) (Holes kappa fam i) a
-> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) a
forall (h :: * -> *) a (kappa :: [*]) (fam :: [*]).
h a -> Holes kappa fam h a
Hole (Holes kappa fam h a
x Holes kappa fam h a
-> Holes kappa fam i a
-> (:*:) (Holes kappa fam h) (Holes kappa fam i) a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Holes kappa fam i a
y)
class (CompoundCnstr kappa fam a) => Deep kappa fam a where
dfrom :: a -> SFix kappa fam a
default dfrom :: (GDeep kappa fam (Rep a)) => a -> SFix kappa fam a
dfrom = SRep (HolesAnn kappa fam U1 V1) (Rep a) -> SFix kappa fam a
forall (kappa :: [*]) (fam :: [*]) a.
CompoundCnstr kappa fam a =>
SRep (SFix kappa fam) (Rep a) -> SFix kappa fam a
SFix (SRep (HolesAnn kappa fam U1 V1) (Rep a) -> SFix kappa fam a)
-> (a -> SRep (HolesAnn kappa fam U1 V1) (Rep a))
-> a
-> SFix kappa fam a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep a Any -> SRep (HolesAnn kappa fam U1 V1) (Rep a)
forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (x :: k).
GDeep kappa fam f =>
f x -> SRep (SFix kappa fam) f
gdfrom (Rep a Any -> SRep (HolesAnn kappa fam U1 V1) (Rep a))
-> (a -> Rep a Any) -> a -> SRep (HolesAnn kappa fam U1 V1) (Rep a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall a x. Generic a => a -> Rep a x
from
dto :: SFix kappa fam a -> a
default dto :: (GDeep kappa fam (Rep a)) => SFix kappa fam a -> a
dto (SFix x :: SRep (HolesAnn kappa fam U1 V1) (Rep a)
x) = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
to (Rep a Any -> a)
-> (SRep (HolesAnn kappa fam U1 V1) (Rep a) -> Rep a Any)
-> SRep (HolesAnn kappa fam U1 V1) (Rep a)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SRep (HolesAnn kappa fam U1 V1) (Rep a) -> Rep a Any
forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (x :: k).
GDeep kappa fam f =>
SRep (SFix kappa fam) f -> f x
gdto (SRep (HolesAnn kappa fam U1 V1) (Rep a) -> a)
-> SRep (HolesAnn kappa fam U1 V1) (Rep a) -> a
forall a b. (a -> b) -> a -> b
$ SRep (HolesAnn kappa fam U1 V1) (Rep a)
x
class GDeep kappa fam f where
gdfrom :: f x -> SRep (SFix kappa fam) f
gdto :: SRep (SFix kappa fam) f -> f x
class GDeepAtom kappa fam (isPrim :: Bool) a where
gdfromAtom :: Proxy isPrim -> a -> SFix kappa fam a
gdtoAtom :: Proxy isPrim -> SFix kappa fam a -> a
instance (CompoundCnstr kappa fam a , Deep kappa fam a)
=> GDeepAtom kappa fam 'False a where
gdfromAtom :: Proxy 'False -> a -> SFix kappa fam a
gdfromAtom _ a :: a
a = a -> SFix kappa fam a
forall (kappa :: [*]) (fam :: [*]) a.
Deep kappa fam a =>
a -> SFix kappa fam a
dfrom (a -> SFix kappa fam a) -> a -> SFix kappa fam a
forall a b. (a -> b) -> a -> b
$ a
a
gdtoAtom :: Proxy 'False -> SFix kappa fam a -> a
gdtoAtom _ x :: SFix kappa fam a
x = SFix kappa fam a -> a
forall (kappa :: [*]) (fam :: [*]) a.
Deep kappa fam a =>
SFix kappa fam a -> a
dto SFix kappa fam a
x
instance (PrimCnstr kappa fam a) => GDeepAtom kappa fam 'True a where
gdfromAtom :: Proxy 'True -> a -> SFix kappa fam a
gdfromAtom _ a :: a
a = a -> SFix kappa fam a
forall (kappa :: [*]) (fam :: [*]) a (h :: * -> *).
PrimCnstr kappa fam a =>
a -> Holes kappa fam h a
Prim a
a
gdtoAtom :: Proxy 'True -> SFix kappa fam a -> a
gdtoAtom _ (Prim a :: a
a) = a
a
instance (GDeepAtom kappa fam (IsElem a kappa) a) => GDeep kappa fam (K1 R a) where
gdfrom :: K1 R a x -> SRep (SFix kappa fam) (K1 R a)
gdfrom (K1 a :: a
a) = HolesAnn kappa fam U1 V1 a -> SRep (SFix kappa fam) (K1 R a)
forall k (w :: * -> *) a i. w a -> SRep w (K1 i a)
S_K1 (Proxy (IsElem a kappa) -> a -> HolesAnn kappa fam U1 V1 a
forall (kappa :: [*]) (fam :: [*]) (isPrim :: Bool) a.
GDeepAtom kappa fam isPrim a =>
Proxy isPrim -> a -> SFix kappa fam a
gdfromAtom (Proxy (IsElem a kappa)
forall k (t :: k). Proxy t
Proxy :: Proxy (IsElem a kappa)) a
a)
gdto :: SRep (SFix kappa fam) (K1 R a) -> K1 R a x
gdto (S_K1 a :: SFix kappa fam a
a) = a -> K1 R a x
forall k i c (p :: k). c -> K1 i c p
K1 (Proxy (IsElem a kappa) -> SFix kappa fam a -> a
forall (kappa :: [*]) (fam :: [*]) (isPrim :: Bool) a.
GDeepAtom kappa fam isPrim a =>
Proxy isPrim -> SFix kappa fam a -> a
gdtoAtom (Proxy (IsElem a kappa)
forall k (t :: k). Proxy t
Proxy :: Proxy (IsElem a kappa)) SFix kappa fam a
a)
instance GDeep kappa fam U1 where
gdfrom :: U1 x -> SRep (SFix kappa fam) U1
gdfrom U1 = SRep (SFix kappa fam) U1
forall k (w :: * -> *). SRep w U1
S_U1
gdto :: SRep (SFix kappa fam) U1 -> U1 x
gdto S_U1 = U1 x
forall k (p :: k). U1 p
U1
instance (GDeep kappa fam f , GDeep kappa fam g) => GDeep kappa fam (f :*: g) where
gdfrom :: (:*:) f g x -> SRep (SFix kappa fam) (f :*: g)
gdfrom (x :: f x
x :*: y :: g x
y) = (f x -> SRep (SFix kappa fam) f
forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (x :: k).
GDeep kappa fam f =>
f x -> SRep (SFix kappa fam) f
gdfrom f x
x) SRep (SFix kappa fam) f
-> SRep (SFix kappa fam) g -> SRep (SFix kappa fam) (f :*: g)
forall k (w :: * -> *) (f :: k -> *) (g :: k -> *).
SRep w f -> SRep w g -> SRep w (f :*: g)
:**: (g x -> SRep (SFix kappa fam) g
forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (x :: k).
GDeep kappa fam f =>
f x -> SRep (SFix kappa fam) f
gdfrom g x
y)
gdto :: SRep (SFix kappa fam) (f :*: g) -> (:*:) f g x
gdto (x :: SRep (SFix kappa fam) f
x :**: y :: SRep (SFix kappa fam) g
y) = (SRep (SFix kappa fam) f -> f x
forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (x :: k).
GDeep kappa fam f =>
SRep (SFix kappa fam) f -> f x
gdto SRep (SFix kappa fam) f
x) f x -> g x -> (:*:) f g x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (SRep (SFix kappa fam) g -> g x
forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (x :: k).
GDeep kappa fam f =>
SRep (SFix kappa fam) f -> f x
gdto SRep (SFix kappa fam) g
y)
instance (GDeep kappa fam f , GDeep kappa fam g) => GDeep kappa fam (f :+: g) where
gdfrom :: (:+:) f g x -> SRep (SFix kappa fam) (f :+: g)
gdfrom (L1 x :: f x
x) = SRep (SFix kappa fam) f -> SRep (SFix kappa fam) (f :+: g)
forall k (w :: * -> *) (f :: k -> *) (g :: k -> *).
SRep w f -> SRep w (f :+: g)
S_L1 (f x -> SRep (SFix kappa fam) f
forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (x :: k).
GDeep kappa fam f =>
f x -> SRep (SFix kappa fam) f
gdfrom f x
x)
gdfrom (R1 x :: g x
x) = SRep (SFix kappa fam) g -> SRep (SFix kappa fam) (f :+: g)
forall k (w :: * -> *) (g :: k -> *) (f :: k -> *).
SRep w g -> SRep w (f :+: g)
S_R1 (g x -> SRep (SFix kappa fam) g
forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (x :: k).
GDeep kappa fam f =>
f x -> SRep (SFix kappa fam) f
gdfrom g x
x)
gdto :: SRep (SFix kappa fam) (f :+: g) -> (:+:) f g x
gdto (S_L1 x :: SRep (SFix kappa fam) f
x) = f x -> (:+:) f g x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (SRep (SFix kappa fam) f -> f x
forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (x :: k).
GDeep kappa fam f =>
SRep (SFix kappa fam) f -> f x
gdto SRep (SFix kappa fam) f
x)
gdto (S_R1 x :: SRep (SFix kappa fam) g
x) = g x -> (:+:) f g x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (SRep (SFix kappa fam) g -> g x
forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (x :: k).
GDeep kappa fam f =>
SRep (SFix kappa fam) f -> f x
gdto SRep (SFix kappa fam) g
x)
instance (GMeta i c , GDeep kappa fam f) => GDeep kappa fam (M1 i c f) where
gdfrom :: M1 i c f x -> SRep (SFix kappa fam) (M1 i c f)
gdfrom (M1 x :: f x
x) = SMeta i c
-> SRep (SFix kappa fam) f -> SRep (SFix kappa fam) (M1 i c f)
forall k i (t :: Meta) (w :: * -> *) (f :: k -> *).
SMeta i t -> SRep w f -> SRep w (M1 i t f)
S_M1 SMeta i c
forall k i (c :: k). GMeta i c => SMeta i c
smeta (f x -> SRep (SFix kappa fam) f
forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (x :: k).
GDeep kappa fam f =>
f x -> SRep (SFix kappa fam) f
gdfrom f x
x)
gdto :: SRep (SFix kappa fam) (M1 i c f) -> M1 i c f x
gdto (S_M1 _ x :: SRep (SFix kappa fam) f
x) = f x -> M1 i c f x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (SRep (SFix kappa fam) f -> f x
forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (x :: k).
GDeep kappa fam f =>
SRep (SFix kappa fam) f -> f x
gdto SRep (SFix kappa fam) f
x)