{-|
Module: Data.Type.Refine
Description: class of refinable types
Maintainer: Olaf Klinke
Stability: experimental

This module defines classes 
of refinable types and their 'Generic' representations. 

There are two ways to semi-automatically have a 'Refinable' instance for a given type @X@: 
Either the type is 'Generic', in which case a 'GRefine' instance 
can be derived for its 'Rep'resentation. 

@
instance Refinable X where
@

If the type is not 'Generic', you can use the implementation 

@
instance Refinable X where
    refine = refineDeMorgan
@

that applies the deMorgan laws until the predicate is known to either 
cover or delete the type. 
-}
{-# LANGUAGE GADTs, FlexibleContexts, FlexibleInstances, TypeOperators, DefaultSignatures #-}
module Data.Type.Refine (
    -- * Refinements
    Refinement,
    refinedTypeDef,
    runRefinement,
    -- * Refinable types
    Refinable(..),
    GRefine(..),
    refineDeMorgan,
    -- * Predicates (re-export)
    module Data.Type.Predicate
    ) where
import Data.Type.Predicate
import Type.Reflection (Typeable,SomeTypeRep(..),someTypeRep)
import Data.SubType (GSubType(..),idGSubType,mapGSubType,runGEmbedding)
import Data.Proxy (Proxy(..))
import GHC.Generics
import Topology.StoneSpace (StoneSpace,GStoneSpace(..))
import Data.Dynamic (Dynamic,fromDynamic)

-- * Refinements

-- | Sub-types are given as the predicate transformer duals 
-- of embeddings where the domain is existentially quantified. 
-- The domain is required to be refinable, too.
type Refinement = GSubType GStone GRefine

-- | Extract the type definition of the refined sub-type.
refinedTypeDef :: Refinement f -> SomeTypeRep
refinedTypeDef :: forall (f :: * -> *). Refinement f -> SomeTypeRep
refinedTypeDef GSubType GStone GRefine f
GEmpty = Proxy (V1 ()) -> SomeTypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> SomeTypeRep
someTypeRep (Proxy (V1 ())
forall {k} (t :: k). Proxy t
Proxy :: Proxy (V1 ()))
refinedTypeDef (GEmbed GStone y f
h) = GStone y f -> SomeTypeRep
forall (f :: * -> *) (g :: * -> *).
Typeable (f ()) =>
GStone f g -> SomeTypeRep
gDomain GStone y f
h

-- * Operations on refinements

unionRefinements :: Refinement f -> Refinement f -> Refinement f
unionRefinements :: forall (f :: * -> *). Refinement f -> Refinement f -> Refinement f
unionRefinements GSubType GStone GRefine f
GEmpty GSubType GStone GRefine f
s = GSubType GStone GRefine f
s
unionRefinements GSubType GStone GRefine f
s GSubType GStone GRefine f
GEmpty = GSubType GStone GRefine f
s
unionRefinements (GEmbed (GStone Predicate f -> Predicate y
f)) (GEmbed (GStone Predicate f -> Predicate y
g)) = GStone (y :+: y) f -> GSubType GStone GRefine f
forall {k} (b :: k -> Constraint) (y :: k) (a :: k -> k -> *)
       (c :: k).
b y =>
a y c -> GSubType a b c
GEmbed ((Predicate f -> Predicate (y :+: y)) -> GStone (y :+: y) f
forall (f :: * -> *) (g :: * -> *).
(Predicate g -> Predicate f) -> GStone f g
GStone ((Predicate f -> Predicate y)
-> (Predicate f -> Predicate y)
-> Predicate f
-> Predicate (y :+: y)
forall (z :: * -> *) (a :: * -> *) (b :: * -> *).
(Predicate z -> Predicate a)
-> (Predicate z -> Predicate b)
-> Predicate z
-> Predicate (a :+: b)
universalUnion Predicate f -> Predicate y
f Predicate f -> Predicate y
g))

-- | 'Refinement' is functorial 
mapRefinement :: GStone f g -> Refinement f -> Refinement g
mapRefinement :: forall (f :: * -> *) (g :: * -> *).
GStone f g -> Refinement f -> Refinement g
mapRefinement = GStone f g
-> GSubType GStone GRefine f -> GSubType GStone GRefine g
forall {k} (cat :: k -> k -> *) (x :: k) (y :: k)
       (con :: k -> Constraint).
Category cat =>
cat x y -> GSubType cat con x -> GSubType cat con y
mapGSubType

-- | extract a marshalling function that yields 
-- the correct type as required by 'refinedTypeDef'.
toGDomain :: GRefine g => GStone g f -> Dynamic -> Maybe (g ())
toGDomain :: forall (g :: * -> *) (f :: * -> *).
GRefine g =>
GStone g f -> Dynamic -> Maybe (g ())
toGDomain GStone g f
_ = Dynamic -> Maybe (g ())
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic -- repDynamic

runGRefinement :: GStoneSpace f => Refinement f -> Dynamic -> Maybe (f ())
runGRefinement :: forall (f :: * -> *).
GStoneSpace f =>
Refinement f -> Dynamic -> Maybe (f ())
runGRefinement = (forall (g :: * -> *).
 GRefine g =>
 GStone g f -> Dynamic -> Maybe (g ()))
-> (forall (s :: * -> *). GStone s f -> s () -> f ())
-> GSubType GStone GRefine f
-> Dynamic
-> Maybe (f ())
forall (con :: (* -> *) -> Constraint)
       (cat :: (* -> *) -> (* -> *) -> *) (f :: * -> *).
(forall (g :: * -> *). con g => cat g f -> Dynamic -> Maybe (g ()))
-> (forall (s :: * -> *). cat s f -> s () -> f ())
-> GSubType cat con f
-> Dynamic
-> Maybe (f ())
runGEmbedding GStone g f -> Dynamic -> Maybe (g ())
forall (g :: * -> *).
GRefine g =>
GStone g f -> Dynamic -> Maybe (g ())
forall (g :: * -> *) (f :: * -> *).
GRefine g =>
GStone g f -> Dynamic -> Maybe (g ())
toGDomain GStone s f -> s () -> f ()
forall (s :: * -> *). GStone s f -> s () -> f ()
forall (f :: * -> *) (g :: * -> *) p.
GStoneSpace f =>
GStone g f -> g p -> f p
forall (g :: * -> *) p. GStone g f -> g p -> f p
gSpec

-- | Since the refined sub-type is hidden inside an existential quantification, 
-- we can run the embedding only detour via 'Dynamic'. 
-- It is ensured that all 'Dynamic' values constructed from the type 
-- given by 'refinedTypeDef' will be mapped to a 'Just'. 
--
-- Executing a predicate transformer 'GStone' requires the target to be a 'StoneSpace'. 
runRefinement :: StoneSpace t => Refinement (Rep t) -> Dynamic -> Maybe t
runRefinement :: forall t. StoneSpace t => Refinement (Rep t) -> Dynamic -> Maybe t
runRefinement Refinement (Rep t)
r = (Rep t () -> t) -> Maybe (Rep t ()) -> Maybe t
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Rep t () -> t
forall a x. Generic a => Rep a x -> a
forall x. Rep t x -> t
to (Maybe (Rep t ()) -> Maybe t)
-> (Dynamic -> Maybe (Rep t ())) -> Dynamic -> Maybe t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refinement (Rep t) -> Dynamic -> Maybe (Rep t ())
forall (f :: * -> *).
GStoneSpace f =>
Refinement f -> Dynamic -> Maybe (f ())
runGRefinement Refinement (Rep t)
r

-- * Refinable types

-- | Since 'Predicate' has kind @(Type -> Type) -> Type@ 
-- we have to wrap a monomorphic type in a 'K1'. 
-- This is in line with the usage of constants on Generic types. 
class Refinable c where
    refine :: Predicate (K1 R c) -> Refinement (K1 R c)
    default refine :: (Generic c, Rep c ~ f, GRefine f) => Predicate (K1 R c) -> Refinement (K1 R c)
    refine = GStone f (K1 R c) -> Refinement f -> Refinement (K1 R c)
forall (f :: * -> *) (g :: * -> *).
GStone f g -> Refinement f -> Refinement g
mapRefinement ((Predicate (K1 R c) -> Predicate f) -> GStone f (K1 R c)
forall (f :: * -> *) (g :: * -> *).
(Predicate g -> Predicate f) -> GStone f g
GStone Predicate (K1 R c) -> Predicate f
Predicate (K1 R c) -> Predicate (Rep c)
forall c i. Generic c => Predicate (K1 i c) -> Predicate (Rep c)
mapConst) (Refinement f -> Refinement (K1 R c))
-> (Predicate (K1 R c) -> Refinement f)
-> Predicate (K1 R c)
-> Refinement (K1 R c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Predicate f -> Refinement f
forall (f :: * -> *). GRefine f => Predicate f -> Refinement f
grefine (Predicate f -> Refinement f)
-> (Predicate (K1 R c) -> Predicate f)
-> Predicate (K1 R c)
-> Refinement f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Predicate (K1 R c) -> Predicate f
Predicate (K1 R c) -> Predicate (Rep c)
forall c i. Generic c => Predicate (K1 i c) -> Predicate (Rep c)
mapConst

-- | Class of 'Rep'resentations of refinable types. 
-- The default implementation has inexhaustive pattern matches 
-- for any type with 'Predicate's that go beyond the Boolean connectives 
-- and should therefore be overridden. 
class Typeable f => GRefine f where
    grefine :: Predicate f -> Refinement f
    grefine = Predicate f -> Refinement f
forall (f :: * -> *). GRefine f => Predicate f -> Refinement f
refineDeMorgan

instance GRefine U1 where
    grefine :: Predicate U1 -> Refinement U1
grefine = Predicate U1 -> Refinement U1
forall (f :: * -> *). GRefine f => Predicate f -> Refinement f
refineDeMorgan

instance GRefine f => GRefine (Rec1 f) where
    grefine :: Predicate (Rec1 f) -> Refinement (Rec1 f)
grefine = GStone f (Rec1 f) -> Refinement f -> Refinement (Rec1 f)
forall (f :: * -> *) (g :: * -> *).
GStone f g -> Refinement f -> Refinement g
mapRefinement ((Predicate (Rec1 f) -> Predicate f) -> GStone f (Rec1 f)
forall (f :: * -> *) (g :: * -> *).
(Predicate g -> Predicate f) -> GStone f g
GStone Predicate (Rec1 f) -> Predicate f
forall (f :: * -> *). Predicate (Rec1 f) -> Predicate f
mapRec) (Refinement f -> Refinement (Rec1 f))
-> (Predicate (Rec1 f) -> Refinement f)
-> Predicate (Rec1 f)
-> Refinement (Rec1 f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Predicate f -> Refinement f
forall (f :: * -> *). GRefine f => Predicate f -> Refinement f
grefine (Predicate f -> Refinement f)
-> (Predicate (Rec1 f) -> Predicate f)
-> Predicate (Rec1 f)
-> Refinement f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Predicate (Rec1 f) -> Predicate f
forall (f :: * -> *). Predicate (Rec1 f) -> Predicate f
mapRec

--  TODO: The sub-type forgets the meta-data. 
-- Find a way to push at least constructor and selector names 
-- down into the sub-type.
instance (GRefine f, Typeable i, Typeable m) => GRefine (M1 i m f) where
    grefine :: Predicate (M1 i m f) -> Refinement (M1 i m f)
grefine = GStone f (M1 i m f) -> Refinement f -> Refinement (M1 i m f)
forall (f :: * -> *) (g :: * -> *).
GStone f g -> Refinement f -> Refinement g
mapRefinement ((Predicate (M1 i m f) -> Predicate f) -> GStone f (M1 i m f)
forall (f :: * -> *) (g :: * -> *).
(Predicate g -> Predicate f) -> GStone f g
GStone Predicate (M1 i m f) -> Predicate f
forall i (m :: Meta) (f :: * -> *).
Predicate (M1 i m f) -> Predicate f
mapMeta) (Refinement f -> Refinement (M1 i m f))
-> (Predicate (M1 i m f) -> Refinement f)
-> Predicate (M1 i m f)
-> Refinement (M1 i m f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Predicate f -> Refinement f
forall (f :: * -> *). GRefine f => Predicate f -> Refinement f
grefine (Predicate f -> Refinement f)
-> (Predicate (M1 i m f) -> Predicate f)
-> Predicate (M1 i m f)
-> Refinement f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Predicate (M1 i m f) -> Predicate f
forall i (m :: Meta) (f :: * -> *).
Predicate (M1 i m f) -> Predicate f
mapMeta

instance (GRefine f, GRefine g) => GRefine (f :+: g) where
    grefine :: Predicate (f :+: g) -> Refinement (f :+: g)
grefine Predicate (f :+: g)
p = Refinement (f :+: g)
-> Refinement (f :+: g) -> Refinement (f :+: g)
forall (f :: * -> *). Refinement f -> Refinement f -> Refinement f
unionRefinements
        (GStone f (f :+: g) -> Refinement f -> Refinement (f :+: g)
forall (f :: * -> *) (g :: * -> *).
GStone f g -> Refinement f -> Refinement g
mapRefinement ((Predicate (f :+: g) -> Predicate f) -> GStone f (f :+: g)
forall (f :: * -> *) (g :: * -> *).
(Predicate g -> Predicate f) -> GStone f g
GStone Predicate (f :+: g) -> Predicate f
forall (f :: * -> *) (g :: * -> *).
Predicate (f :+: g) -> Predicate f
insL) (Predicate f -> Refinement f
forall (f :: * -> *). GRefine f => Predicate f -> Refinement f
grefine (Predicate (f :+: g) -> Predicate f
forall (f :: * -> *) (g :: * -> *).
Predicate (f :+: g) -> Predicate f
insL Predicate (f :+: g)
p)))
        (GStone g (f :+: g) -> Refinement g -> Refinement (f :+: g)
forall (f :: * -> *) (g :: * -> *).
GStone f g -> Refinement f -> Refinement g
mapRefinement ((Predicate (f :+: g) -> Predicate g) -> GStone g (f :+: g)
forall (f :: * -> *) (g :: * -> *).
(Predicate g -> Predicate f) -> GStone f g
GStone Predicate (f :+: g) -> Predicate g
forall (f :: * -> *) (g :: * -> *).
Predicate (f :+: g) -> Predicate g
insR) (Predicate g -> Refinement g
forall (f :: * -> *). GRefine f => Predicate f -> Refinement f
grefine (Predicate (f :+: g) -> Predicate g
forall (f :: * -> *) (g :: * -> *).
Predicate (f :+: g) -> Predicate g
insR Predicate (f :+: g)
p)))

-- | 'first' lifted to refinements
refineFst :: GRefine g => Refinement f -> Refinement (f :*: g)
refineFst :: forall (g :: * -> *) (f :: * -> *).
GRefine g =>
Refinement f -> Refinement (f :*: g)
refineFst GSubType GStone GRefine f
GEmpty = GSubType GStone GRefine (f :*: g)
forall {k} (a :: k -> k -> *) (b :: k -> Constraint) (c :: k).
GSubType a b c
GEmpty
refineFst (GEmbed (GStone Predicate f -> Predicate y
f)) = GStone (y :*: g) (f :*: g) -> GSubType GStone GRefine (f :*: g)
forall {k} (b :: k -> Constraint) (y :: k) (a :: k -> k -> *)
       (c :: k).
b y =>
a y c -> GSubType a b c
GEmbed ((Predicate (f :*: g) -> Predicate (y :*: g))
-> GStone (y :*: g) (f :*: g)
forall (f :: * -> *) (g :: * -> *).
(Predicate g -> Predicate f) -> GStone f g
GStone ((Predicate f -> Predicate y)
-> Predicate (f :*: g) -> Predicate (y :*: g)
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
(Predicate f -> Predicate g)
-> Predicate (f :*: h) -> Predicate (g :*: h)
first Predicate f -> Predicate y
f))

-- | 'second' lifted to refinements
refineSnd :: GRefine f => Refinement g -> Refinement (f :*: g)
refineSnd :: forall (f :: * -> *) (g :: * -> *).
GRefine f =>
Refinement g -> Refinement (f :*: g)
refineSnd GSubType GStone GRefine g
GEmpty = GSubType GStone GRefine (f :*: g)
forall {k} (a :: k -> k -> *) (b :: k -> Constraint) (c :: k).
GSubType a b c
GEmpty
refineSnd (GEmbed (GStone Predicate g -> Predicate y
g)) = GStone (f :*: y) (f :*: g) -> GSubType GStone GRefine (f :*: g)
forall {k} (b :: k -> Constraint) (y :: k) (a :: k -> k -> *)
       (c :: k).
b y =>
a y c -> GSubType a b c
GEmbed ((Predicate (f :*: g) -> Predicate (f :*: y))
-> GStone (f :*: y) (f :*: g)
forall (f :: * -> *) (g :: * -> *).
(Predicate g -> Predicate f) -> GStone f g
GStone ((Predicate g -> Predicate y)
-> Predicate (f :*: g) -> Predicate (f :*: y)
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
(Predicate f -> Predicate g)
-> Predicate (h :*: f) -> Predicate (h :*: g)
second Predicate g -> Predicate y
g))

-- | For types that have only the Boolean connectives as predicates, 
-- the only possible sub-types are the empty type and the entire type. 
-- Use this as default implementation of 'refine'.
refineDeMorgan :: GRefine f => Predicate f -> Refinement f
refineDeMorgan :: forall (f :: * -> *). GRefine f => Predicate f -> Refinement f
refineDeMorgan Predicate f
Wildcard = GSubType GStone GRefine f
forall {k} (cat :: k -> k -> *) (con :: k -> Constraint) (x :: k).
(Category cat, con x) =>
GSubType cat con x
idGSubType
refineDeMorgan (Predicate f
p :\/ Predicate f
_) = Predicate f -> GSubType GStone GRefine f
forall (f :: * -> *). GRefine f => Predicate f -> Refinement f
refineDeMorgan Predicate f
p -- the type is join-prime
refineDeMorgan (Predicate f
p :/\ Predicate f
q) = case Predicate f -> GSubType GStone GRefine f
forall (f :: * -> *). GRefine f => Predicate f -> Refinement f
refineDeMorgan Predicate f
p of
    GSubType GStone GRefine f
GEmpty -> GSubType GStone GRefine f
forall {k} (a :: k -> k -> *) (b :: k -> Constraint) (c :: k).
GSubType a b c
GEmpty
    GEmbed GStone y f
_ -> Predicate f -> GSubType GStone GRefine f
forall (f :: * -> *). GRefine f => Predicate f -> Refinement f
refineDeMorgan Predicate f
q
refineDeMorgan (Neg Predicate f
p) = case Predicate f
p of
    Predicate f
Wildcard -> GSubType GStone GRefine f
forall {k} (a :: k -> k -> *) (b :: k -> Constraint) (c :: k).
GSubType a b c
GEmpty
    Neg Predicate f
q    -> Predicate f -> GSubType GStone GRefine f
forall (f :: * -> *). GRefine f => Predicate f -> Refinement f
refineDeMorgan Predicate f
q -- double negation
    Predicate f
q :/\ Predicate f
r  -> Predicate f -> GSubType GStone GRefine f
forall (f :: * -> *). GRefine f => Predicate f -> Refinement f
refineDeMorgan (Predicate f -> Predicate f
forall (a :: * -> *). Predicate a -> Predicate a
Neg Predicate f
q Predicate f -> Predicate f -> Predicate f
forall (a :: * -> *). Predicate a -> Predicate a -> Predicate a
:\/ Predicate f -> Predicate f
forall (a :: * -> *). Predicate a -> Predicate a
Neg Predicate f
r)
    Predicate f
q :\/ Predicate f
r  -> Predicate f -> GSubType GStone GRefine f
forall (f :: * -> *). GRefine f => Predicate f -> Refinement f
refineDeMorgan (Predicate f -> Predicate f
forall (a :: * -> *). Predicate a -> Predicate a
Neg Predicate f
q Predicate f -> Predicate f -> Predicate f
forall (a :: * -> *). Predicate a -> Predicate a -> Predicate a
:/\ Predicate f -> Predicate f
forall (a :: * -> *). Predicate a -> Predicate a
Neg Predicate f
r)
-- Note: The warning about non-exhaustive pattern matches 
-- is deliberate - we have no way to constrain f to 
-- "all types where Predicate has only these constructors". 


instance (GRefine f, GRefine g) => GRefine (f :*: g) where
    grefine :: Predicate (f :*: g) -> Refinement (f :*: g)
grefine Predicate (f :*: g)
Wildcard = Refinement (f :*: g)
forall {k} (cat :: k -> k -> *) (con :: k -> Constraint) (x :: k).
(Category cat, con x) =>
GSubType cat con x
idGSubType
    grefine (Fst Predicate f
p)  = Refinement f -> Refinement (f :*: g)
forall (g :: * -> *) (f :: * -> *).
GRefine g =>
Refinement f -> Refinement (f :*: g)
refineFst (Predicate f -> Refinement f
forall (f :: * -> *). GRefine f => Predicate f -> Refinement f
grefine Predicate f
Predicate f
p)
    grefine (Snd Predicate g
p)  = Refinement g -> Refinement (f :*: g)
forall (f :: * -> *) (g :: * -> *).
GRefine f =>
Refinement g -> Refinement (f :*: g)
refineSnd (Predicate g -> Refinement g
forall (f :: * -> *). GRefine f => Predicate f -> Refinement f
grefine Predicate g
Predicate g
p)
    grefine (Predicate (f :*: g)
p :\/ Predicate (f :*: g)
q) = Refinement (f :*: g)
-> Refinement (f :*: g) -> Refinement (f :*: g)
forall (f :: * -> *). Refinement f -> Refinement f -> Refinement f
unionRefinements (Predicate (f :*: g) -> Refinement (f :*: g)
forall (f :: * -> *). GRefine f => Predicate f -> Refinement f
grefine Predicate (f :*: g)
p) (Predicate (f :*: g) -> Refinement (f :*: g)
forall (f :: * -> *). GRefine f => Predicate f -> Refinement f
grefine Predicate (f :*: g)
q)
    grefine (Predicate (f :*: g)
p :/\ Predicate (f :*: g)
q) = case Predicate (f :*: g) -> Refinement (f :*: g)
forall (f :: * -> *). GRefine f => Predicate f -> Refinement f
grefine Predicate (f :*: g)
p of
        Refinement (f :*: g)
GEmpty -> Refinement (f :*: g)
forall {k} (a :: k -> k -> *) (b :: k -> Constraint) (c :: k).
GSubType a b c
GEmpty
        GEmbed e :: GStone y (f :*: g)
e@(GStone Predicate (f :*: g) -> Predicate y
h) -> GStone y (f :*: g) -> Refinement y -> Refinement (f :*: g)
forall (f :: * -> *) (g :: * -> *).
GStone f g -> Refinement f -> Refinement g
mapRefinement GStone y (f :*: g)
e (Predicate y -> Refinement y
forall (f :: * -> *). GRefine f => Predicate f -> Refinement f
grefine (Predicate (f :*: g) -> Predicate y
h Predicate (f :*: g)
q))
    -- use deMorgan laws to refine a negation
    grefine (Neg Predicate (f :*: g)
p) = case Predicate (f :*: g)
p of
        Predicate (f :*: g)
Wildcard -> Refinement (f :*: g)
forall {k} (a :: k -> k -> *) (b :: k -> Constraint) (c :: k).
GSubType a b c
GEmpty
        Neg Predicate (f :*: g)
q    -> Predicate (f :*: g) -> Refinement (f :*: g)
forall (f :: * -> *). GRefine f => Predicate f -> Refinement f
grefine Predicate (f :*: g)
q -- double negation
        Predicate (f :*: g)
q :/\ Predicate (f :*: g)
r  -> Predicate (f :*: g) -> Refinement (f :*: g)
forall (f :: * -> *). GRefine f => Predicate f -> Refinement f
grefine (Predicate (f :*: g) -> Predicate (f :*: g)
forall (a :: * -> *). Predicate a -> Predicate a
Neg Predicate (f :*: g)
q Predicate (f :*: g) -> Predicate (f :*: g) -> Predicate (f :*: g)
forall (a :: * -> *). Predicate a -> Predicate a -> Predicate a
:\/ Predicate (f :*: g) -> Predicate (f :*: g)
forall (a :: * -> *). Predicate a -> Predicate a
Neg Predicate (f :*: g)
r)
        Predicate (f :*: g)
q :\/ Predicate (f :*: g)
r  -> Predicate (f :*: g) -> Refinement (f :*: g)
forall (f :: * -> *). GRefine f => Predicate f -> Refinement f
grefine (Predicate (f :*: g) -> Predicate (f :*: g)
forall (a :: * -> *). Predicate a -> Predicate a
Neg Predicate (f :*: g)
q Predicate (f :*: g) -> Predicate (f :*: g) -> Predicate (f :*: g)
forall (a :: * -> *). Predicate a -> Predicate a -> Predicate a
:/\ Predicate (f :*: g) -> Predicate (f :*: g)
forall (a :: * -> *). Predicate a -> Predicate a
Neg Predicate (f :*: g)
r)
        Fst Predicate f
q    -> Predicate (f :*: g) -> Refinement (f :*: g)
forall (f :: * -> *). GRefine f => Predicate f -> Refinement f
grefine (Predicate f -> Predicate (f :*: g)
forall (f :: * -> *) (g :: * -> *).
Predicate f -> Predicate (f :*: g)
Fst (Predicate f -> Predicate f
forall (a :: * -> *). Predicate a -> Predicate a
Neg Predicate f
Predicate f
q)) -- not . (\(x,_) -> p x) = \(x,_) -> (not.p) x
        Snd Predicate g
q    -> Predicate (f :*: g) -> Refinement (f :*: g)
forall (f :: * -> *). GRefine f => Predicate f -> Refinement f
grefine (Predicate g -> Predicate (f :*: g)
forall (g :: * -> *) (f :: * -> *).
Predicate g -> Predicate (f :*: g)
Snd (Predicate g -> Predicate g
forall (a :: * -> *). Predicate a -> Predicate a
Neg Predicate g
Predicate g
q)) -- not . (\(_,x) -> p x) = \(_,x) -> (not.p) x

instance (Refinable c, Typeable c) => GRefine (K1 R c) where
    grefine :: Predicate (K1 R c) -> Refinement (K1 R c)
grefine = Predicate (K1 R c) -> Refinement (K1 R c)
forall c. Refinable c => Predicate (K1 R c) -> Refinement (K1 R c)
refine