{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeOperators         #-}

-- | 'Generic' implementations of 'Logical' methods.
--
-- As discussed in the documentation for the 'Logical' class, method
-- implementations are not particularly interesting and can be easily
-- automated. This module provides such automated implementations using
-- 'Generic'.
--
-- This module expects that you already have a logical representation for your
-- type, and there's already a 'Logic' type instance. The logical type must not
-- change the order of constructors as well as the order of fields in each
-- constructor, but the names do not matter. Additionally, each field in the
-- original type must be wrapped in a 'Term' in the logical representation.
--
-- For example, consider the following type definition:
--
-- > data Tree a
-- >   = Leaf a
-- >   | Node (Tree a) (Tree a)
-- >   deriving (Generic)
-- >
-- > data LogicTree a
-- >   = LogicLeaf (Term a)
-- >   | LogicNode (Term (Tree a)) (Term (Tree a))
-- >   deriving (Generic)
--
-- From there, using the generic implementations is trivial:
--
-- > instance (Logical a) => Logical (Tree a) where
-- >   type Logic (Tree a) = LogicTree a
-- >   unify = genericUnify
-- >   subst = genericSubst
-- >   inject = genericInject
-- >   extract = genericExtract
module Kanren.GenericLogical (
  genericUnify,
  genericWalk,
  genericOccursCheck,
  genericInject,
  genericExtract,
  GLogical,
) where

import           Control.Monad ((>=>))
import           Data.Proxy    (Proxy (..))
import           GHC.Generics

import           Kanren.Core

class GLogical f f' where
  gunify :: Proxy f -> f' p -> f' p -> State -> Maybe State
  gwalk :: Proxy f -> State -> f' p -> f' p
  goccursCheck :: Proxy f -> VarId b -> f' p -> State -> Bool
  ginject :: f p -> f' p
  gextract :: f' p -> Maybe (f p)

instance GLogical V1 V1 where
  gunify :: forall p. Proxy V1 -> V1 p -> V1 p -> State -> Maybe State
gunify Proxy V1
_ V1 p
_ V1 p
_ = State -> Maybe State
forall a. a -> Maybe a
Just
  gwalk :: forall p. Proxy V1 -> State -> V1 p -> V1 p
gwalk Proxy V1
_ State
_ = V1 p -> V1 p
forall a. a -> a
id
  goccursCheck :: forall b p. Proxy V1 -> VarId b -> V1 p -> State -> Bool
goccursCheck Proxy V1
_ VarId b
_ V1 p
_ State
_ = Bool
False
  ginject :: forall p. V1 p -> V1 p
ginject = V1 p -> V1 p
forall a. a -> a
id
  gextract :: forall p. V1 p -> Maybe (V1 p)
gextract = V1 p -> Maybe (V1 p)
forall a. a -> Maybe a
Just

instance GLogical U1 U1 where
  gunify :: forall p. Proxy U1 -> U1 p -> U1 p -> State -> Maybe State
gunify Proxy U1
_ U1 p
_ U1 p
_ = State -> Maybe State
forall a. a -> Maybe a
Just
  gwalk :: forall p. Proxy U1 -> State -> U1 p -> U1 p
gwalk Proxy U1
_ State
_ = U1 p -> U1 p
forall a. a -> a
id
  goccursCheck :: forall b p. Proxy U1 -> VarId b -> U1 p -> State -> Bool
goccursCheck Proxy U1
_ VarId b
_ U1 p
_ State
_ = Bool
False
  ginject :: forall p. U1 p -> U1 p
ginject = U1 p -> U1 p
forall a. a -> a
id
  gextract :: forall p. U1 p -> Maybe (U1 p)
gextract = U1 p -> Maybe (U1 p)
forall a. a -> Maybe a
Just

instance (GLogical f f', GLogical g g') => GLogical (f :+: g) (f' :+: g') where
  gunify :: forall p.
Proxy (f :+: g)
-> (:+:) f' g' p -> (:+:) f' g' p -> State -> Maybe State
gunify Proxy (f :+: g)
_ (L1 f' p
x) (L1 f' p
y) = Proxy f -> f' p -> f' p -> State -> Maybe State
forall p. Proxy f -> f' p -> f' p -> State -> Maybe State
forall (f :: * -> *) (f' :: * -> *) p.
GLogical f f' =>
Proxy f -> f' p -> f' p -> State -> Maybe State
gunify (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) f' p
x f' p
y
  gunify Proxy (f :+: g)
_ (R1 g' p
x) (R1 g' p
y) = Proxy g -> g' p -> g' p -> State -> Maybe State
forall p. Proxy g -> g' p -> g' p -> State -> Maybe State
forall (f :: * -> *) (f' :: * -> *) p.
GLogical f f' =>
Proxy f -> f' p -> f' p -> State -> Maybe State
gunify (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @g) g' p
x g' p
y
  gunify Proxy (f :+: g)
_ (:+:) f' g' p
_ (:+:) f' g' p
_           = Maybe State -> State -> Maybe State
forall a b. a -> b -> a
const Maybe State
forall a. Maybe a
Nothing

  gwalk :: forall p.
Proxy (f :+: g) -> State -> (:+:) f' g' p -> (:+:) f' g' p
gwalk Proxy (f :+: g)
_ State
k (L1 f' p
x) = f' p -> (:+:) f' g' p
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (Proxy f -> State -> f' p -> f' p
forall p. Proxy f -> State -> f' p -> f' p
forall (f :: * -> *) (f' :: * -> *) p.
GLogical f f' =>
Proxy f -> State -> f' p -> f' p
gwalk (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) State
k f' p
x)
  gwalk Proxy (f :+: g)
_ State
k (R1 g' p
y) = g' p -> (:+:) f' g' p
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (Proxy g -> State -> g' p -> g' p
forall p. Proxy g -> State -> g' p -> g' p
forall (f :: * -> *) (f' :: * -> *) p.
GLogical f f' =>
Proxy f -> State -> f' p -> f' p
gwalk (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @g) State
k g' p
y)

  goccursCheck :: forall b p.
Proxy (f :+: g) -> VarId b -> (:+:) f' g' p -> State -> Bool
goccursCheck Proxy (f :+: g)
_ VarId b
varId (L1 f' p
x) = Proxy f -> VarId b -> f' p -> State -> Bool
forall b p. Proxy f -> VarId b -> f' p -> State -> Bool
forall (f :: * -> *) (f' :: * -> *) b p.
GLogical f f' =>
Proxy f -> VarId b -> f' p -> State -> Bool
goccursCheck (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) VarId b
varId f' p
x
  goccursCheck Proxy (f :+: g)
_ VarId b
varId (R1 g' p
y) = Proxy g -> VarId b -> g' p -> State -> Bool
forall b p. Proxy g -> VarId b -> g' p -> State -> Bool
forall (f :: * -> *) (f' :: * -> *) b p.
GLogical f f' =>
Proxy f -> VarId b -> f' p -> State -> Bool
goccursCheck (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @g) VarId b
varId g' p
y

  ginject :: forall p. (:+:) f g p -> (:+:) f' g' p
ginject (L1 f p
x) = f' p -> (:+:) f' g' p
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (f p -> f' p
forall p. f p -> f' p
forall (f :: * -> *) (f' :: * -> *) p. GLogical f f' => f p -> f' p
ginject f p
x)
  ginject (R1 g p
y) = g' p -> (:+:) f' g' p
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (g p -> g' p
forall p. g p -> g' p
forall (f :: * -> *) (f' :: * -> *) p. GLogical f f' => f p -> f' p
ginject g p
y)

  gextract :: forall p. (:+:) f' g' p -> Maybe ((:+:) f g p)
gextract (L1 f' p
x) = f p -> (:+:) f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (f p -> (:+:) f g p) -> Maybe (f p) -> Maybe ((:+:) f g p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f' p -> Maybe (f p)
forall p. f' p -> Maybe (f p)
forall (f :: * -> *) (f' :: * -> *) p.
GLogical f f' =>
f' p -> Maybe (f p)
gextract f' p
x
  gextract (R1 g' p
y) = g p -> (:+:) f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (g p -> (:+:) f g p) -> Maybe (g p) -> Maybe ((:+:) f g p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g' p -> Maybe (g p)
forall p. g' p -> Maybe (g p)
forall (f :: * -> *) (f' :: * -> *) p.
GLogical f f' =>
f' p -> Maybe (f p)
gextract g' p
y

instance (GLogical f f', GLogical g g') => GLogical (f :*: g) (f' :*: g') where
  gunify :: forall p.
Proxy (f :*: g)
-> (:*:) f' g' p -> (:*:) f' g' p -> State -> Maybe State
gunify Proxy (f :*: g)
_ (f' p
x1 :*: g' p
y1) (f' p
x2 :*: g' p
y2) =
    Proxy f -> f' p -> f' p -> State -> Maybe State
forall p. Proxy f -> f' p -> f' p -> State -> Maybe State
forall (f :: * -> *) (f' :: * -> *) p.
GLogical f f' =>
Proxy f -> f' p -> f' p -> State -> Maybe State
gunify (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) f' p
x1 f' p
x2 (State -> Maybe State)
-> (State -> Maybe State) -> State -> Maybe State
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Proxy g -> g' p -> g' p -> State -> Maybe State
forall p. Proxy g -> g' p -> g' p -> State -> Maybe State
forall (f :: * -> *) (f' :: * -> *) p.
GLogical f f' =>
Proxy f -> f' p -> f' p -> State -> Maybe State
gunify (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @g) g' p
y1 g' p
y2
  gwalk :: forall p.
Proxy (f :*: g) -> State -> (:*:) f' g' p -> (:*:) f' g' p
gwalk Proxy (f :*: g)
_ State
k (f' p
x :*: g' p
y) = Proxy f -> State -> f' p -> f' p
forall p. Proxy f -> State -> f' p -> f' p
forall (f :: * -> *) (f' :: * -> *) p.
GLogical f f' =>
Proxy f -> State -> f' p -> f' p
gwalk (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) State
k f' p
x f' p -> g' p -> (:*:) f' g' p
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Proxy g -> State -> g' p -> g' p
forall p. Proxy g -> State -> g' p -> g' p
forall (f :: * -> *) (f' :: * -> *) p.
GLogical f f' =>
Proxy f -> State -> f' p -> f' p
gwalk (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @g) State
k g' p
y
  goccursCheck :: forall b p.
Proxy (f :*: g) -> VarId b -> (:*:) f' g' p -> State -> Bool
goccursCheck Proxy (f :*: g)
_ VarId b
varId (f' p
x :*: g' p
y) State
state =
    Proxy f -> VarId b -> f' p -> State -> Bool
forall b p. Proxy f -> VarId b -> f' p -> State -> Bool
forall (f :: * -> *) (f' :: * -> *) b p.
GLogical f f' =>
Proxy f -> VarId b -> f' p -> State -> Bool
goccursCheck (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) VarId b
varId f' p
x State
state
    Bool -> Bool -> Bool
|| Proxy g -> VarId b -> g' p -> State -> Bool
forall b p. Proxy g -> VarId b -> g' p -> State -> Bool
forall (f :: * -> *) (f' :: * -> *) b p.
GLogical f f' =>
Proxy f -> VarId b -> f' p -> State -> Bool
goccursCheck (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @g) VarId b
varId g' p
y State
state
  ginject :: forall p. (:*:) f g p -> (:*:) f' g' p
ginject (f p
x :*: g p
y) = f p -> f' p
forall p. f p -> f' p
forall (f :: * -> *) (f' :: * -> *) p. GLogical f f' => f p -> f' p
ginject f p
x f' p -> g' p -> (:*:) f' g' p
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g p -> g' p
forall p. g p -> g' p
forall (f :: * -> *) (f' :: * -> *) p. GLogical f f' => f p -> f' p
ginject g p
y
  gextract :: forall p. (:*:) f' g' p -> Maybe ((:*:) f g p)
gextract (f' p
x :*: g' p
y) = do
    f p
x' <- f' p -> Maybe (f p)
forall p. f' p -> Maybe (f p)
forall (f :: * -> *) (f' :: * -> *) p.
GLogical f f' =>
f' p -> Maybe (f p)
gextract f' p
x
    g p
y' <- g' p -> Maybe (g p)
forall p. g' p -> Maybe (g p)
forall (f :: * -> *) (f' :: * -> *) p.
GLogical f f' =>
f' p -> Maybe (f p)
gextract g' p
y
    (:*:) f g p -> Maybe ((:*:) f g p)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (f p
x' f p -> g p -> (:*:) f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g p
y')

instance (Logical c) => GLogical (K1 i c) (K1 i' (Term c)) where
  gunify :: forall p.
Proxy (K1 i c)
-> K1 i' (Term c) p -> K1 i' (Term c) p -> State -> Maybe State
gunify Proxy (K1 i c)
_ (K1 Term c
x) (K1 Term c
y) = Term c -> Term c -> State -> Maybe State
forall a. Logical a => Term a -> Term a -> State -> Maybe State
unify' Term c
x Term c
y
  gwalk :: forall p.
Proxy (K1 i c) -> State -> K1 i' (Term c) p -> K1 i' (Term c) p
gwalk Proxy (K1 i c)
_ State
state (K1 Term c
c) = Term c -> K1 i' (Term c) p
forall k i c (p :: k). c -> K1 i c p
K1 (State -> Term c -> Term c
forall a. Logical a => State -> Term a -> Term a
walk' State
state Term c
c)
  goccursCheck :: forall b p.
Proxy (K1 i c) -> VarId b -> K1 i' (Term c) p -> State -> Bool
goccursCheck Proxy (K1 i c)
_ VarId b
varId (K1 Term c
c) = VarId b -> Term c -> State -> Bool
forall a b. Logical a => VarId b -> Term a -> State -> Bool
occursCheck' VarId b
varId Term c
c
  ginject :: forall p. K1 i c p -> K1 i' (Term c) p
ginject (K1 c
x) = Term c -> K1 i' (Term c) p
forall k i c (p :: k). c -> K1 i c p
K1 (c -> Term c
forall a. Logical a => a -> Term a
inject' c
x)
  gextract :: forall p. K1 i' (Term c) p -> Maybe (K1 i c p)
gextract (K1 Term c
x) = c -> K1 i c p
forall k i c (p :: k). c -> K1 i c p
K1 (c -> K1 i c p) -> Maybe c -> Maybe (K1 i c p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term c -> Maybe c
forall a. Logical a => Term a -> Maybe a
extract' Term c
x

instance (GLogical f f') => GLogical (M1 i t f) (M1 i' t' f') where
  gunify :: forall p.
Proxy (M1 i t f)
-> M1 i' t' f' p -> M1 i' t' f' p -> State -> Maybe State
gunify Proxy (M1 i t f)
_ (M1 f' p
x) (M1 f' p
y) = Proxy f -> f' p -> f' p -> State -> Maybe State
forall p. Proxy f -> f' p -> f' p -> State -> Maybe State
forall (f :: * -> *) (f' :: * -> *) p.
GLogical f f' =>
Proxy f -> f' p -> f' p -> State -> Maybe State
gunify (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) f' p
x f' p
y
  gwalk :: forall p.
Proxy (M1 i t f) -> State -> M1 i' t' f' p -> M1 i' t' f' p
gwalk Proxy (M1 i t f)
_ State
k (M1 f' p
m) = f' p -> M1 i' t' f' p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (Proxy f -> State -> f' p -> f' p
forall p. Proxy f -> State -> f' p -> f' p
forall (f :: * -> *) (f' :: * -> *) p.
GLogical f f' =>
Proxy f -> State -> f' p -> f' p
gwalk (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) State
k f' p
m)
  goccursCheck :: forall b p.
Proxy (M1 i t f) -> VarId b -> M1 i' t' f' p -> State -> Bool
goccursCheck Proxy (M1 i t f)
_ VarId b
varId (M1 f' p
m) = Proxy f -> VarId b -> f' p -> State -> Bool
forall b p. Proxy f -> VarId b -> f' p -> State -> Bool
forall (f :: * -> *) (f' :: * -> *) b p.
GLogical f f' =>
Proxy f -> VarId b -> f' p -> State -> Bool
goccursCheck (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @f) VarId b
varId f' p
m
  ginject :: forall p. M1 i t f p -> M1 i' t' f' p
ginject (M1 f p
x) = f' p -> M1 i' t' f' p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f p -> f' p
forall p. f p -> f' p
forall (f :: * -> *) (f' :: * -> *) p. GLogical f f' => f p -> f' p
ginject f p
x)
  gextract :: forall p. M1 i' t' f' p -> Maybe (M1 i t f p)
gextract (M1 f' p
x) = f p -> M1 i t f p
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f p -> M1 i t f p) -> Maybe (f p) -> Maybe (M1 i t f p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f' p -> Maybe (f p)
forall p. f' p -> Maybe (f p)
forall (f :: * -> *) (f' :: * -> *) p.
GLogical f f' =>
f' p -> Maybe (f p)
gextract f' p
x

-- | The generic implementation of 'unify'.
genericUnify
  :: forall a
   . (Generic (Logic a), GLogical (Rep a) (Rep (Logic a)))
  => Logic a
  -> Logic a
  -> State
  -> Maybe State
genericUnify :: forall a.
(Generic (Logic a), GLogical (Rep a) (Rep (Logic a))) =>
Logic a -> Logic a -> State -> Maybe State
genericUnify Logic a
l Logic a
r = Proxy (Rep a)
-> Rep (Logic a) Any -> Rep (Logic a) Any -> State -> Maybe State
forall p.
Proxy (Rep a)
-> Rep (Logic a) p -> Rep (Logic a) p -> State -> Maybe State
forall (f :: * -> *) (f' :: * -> *) p.
GLogical f f' =>
Proxy f -> f' p -> f' p -> State -> Maybe State
gunify (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @(Rep a)) (Logic a -> Rep (Logic a) Any
forall a x. Generic a => a -> Rep a x
forall x. Logic a -> Rep (Logic a) x
from Logic a
l) (Logic a -> Rep (Logic a) Any
forall a x. Generic a => a -> Rep a x
forall x. Logic a -> Rep (Logic a) x
from Logic a
r)

-- | The generic implementation of 'walk'.
genericWalk
  :: forall a
   . (Generic (Logic a), GLogical (Rep a) (Rep (Logic a)))
  => State
  -> Logic a
  -> Logic a
genericWalk :: forall a.
(Generic (Logic a), GLogical (Rep a) (Rep (Logic a))) =>
State -> Logic a -> Logic a
genericWalk State
k Logic a
term = Rep (Logic a) Any -> Logic a
forall a x. Generic a => Rep a x -> a
forall x. Rep (Logic a) x -> Logic a
to (Proxy (Rep a) -> State -> Rep (Logic a) Any -> Rep (Logic a) Any
forall p.
Proxy (Rep a) -> State -> Rep (Logic a) p -> Rep (Logic a) p
forall (f :: * -> *) (f' :: * -> *) p.
GLogical f f' =>
Proxy f -> State -> f' p -> f' p
gwalk (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @(Rep a)) State
k (Logic a -> Rep (Logic a) Any
forall a x. Generic a => a -> Rep a x
forall x. Logic a -> Rep (Logic a) x
from Logic a
term))

-- | The generic implementation of 'walk'.
genericOccursCheck
  :: forall a b
   . (Generic (Logic a), GLogical (Rep a) (Rep (Logic a)))
  => VarId b
  -> Logic a
  -> State
  -> Bool
genericOccursCheck :: forall a b.
(Generic (Logic a), GLogical (Rep a) (Rep (Logic a))) =>
VarId b -> Logic a -> State -> Bool
genericOccursCheck VarId b
varId Logic a
term = Proxy (Rep a) -> VarId b -> Rep (Logic a) Any -> State -> Bool
forall b p.
Proxy (Rep a) -> VarId b -> Rep (Logic a) p -> State -> Bool
forall (f :: * -> *) (f' :: * -> *) b p.
GLogical f f' =>
Proxy f -> VarId b -> f' p -> State -> Bool
goccursCheck (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @(Rep a)) VarId b
varId (Logic a -> Rep (Logic a) Any
forall a x. Generic a => a -> Rep a x
forall x. Logic a -> Rep (Logic a) x
from Logic a
term)

-- | The generic implementation of 'inject'.
genericInject
  :: (Generic a, Generic (Logic a), GLogical (Rep a) (Rep (Logic a)))
  => a
  -> Logic a
genericInject :: forall a.
(Generic a, Generic (Logic a), GLogical (Rep a) (Rep (Logic a))) =>
a -> Logic a
genericInject a
x = Rep (Logic a) Any -> Logic a
forall a x. Generic a => Rep a x -> a
forall x. Rep (Logic a) x -> Logic a
to (Rep a Any -> Rep (Logic a) Any
forall p. Rep a p -> Rep (Logic a) p
forall (f :: * -> *) (f' :: * -> *) p. GLogical f f' => f p -> f' p
ginject (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
x))

-- | The generic implementation of 'extract'.
genericExtract
  :: (Generic a, Generic (Logic a), GLogical (Rep a) (Rep (Logic a)))
  => Logic a
  -> Maybe a
genericExtract :: forall a.
(Generic a, Generic (Logic a), GLogical (Rep a) (Rep (Logic a))) =>
Logic a -> Maybe a
genericExtract Logic a
x = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a) -> Maybe (Rep a Any) -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Rep (Logic a) Any -> Maybe (Rep a Any)
forall p. Rep (Logic a) p -> Maybe (Rep a p)
forall (f :: * -> *) (f' :: * -> *) p.
GLogical f f' =>
f' p -> Maybe (f p)
gextract (Logic a -> Rep (Logic a) Any
forall a x. Generic a => a -> Rep a x
forall x. Logic a -> Rep (Logic a) x
from Logic a
x)