{-# LANGUAGE DeriveGeneric, TypeFamilies #-}
module Example where
import GHC.Generics
import Data.Type.Predicate
import Data.Type.Refine
import Data.SubType
import Data.Kind (Type)
import Data.Dynamic (toDyn)
import Data.Maybe (isJust)
import Topology.StoneSpace

data Foo = Foo1 | Foo2 | Foo3 deriving (Show,Eq,Generic)
instance Refinable Foo where

data Bar = Bar1 | Bar2 deriving (Show,Eq,Generic)
instance Refinable Bar where

instance Refinable (Maybe Foo) where
instance Refinable (Maybe Bar) where

data X a b = X {
    foo :: Maybe a,
    bar :: Maybe b
    } deriving (Show,Generic)

-- The refining property is the conjunction of two pattern matches, 
-- which we can automatically convert to 'Predicate's 
-- thanks to compactness of the type. 
p :: Predicate (Rep (X Foo Bar))
p = let 
    Just pat1 = toPattern (isJust.foo)
    Just pat2 = toPattern (isJust.bar)
    in pat1 :/\ pat2

s :: Refinement (Rep (X Foo Bar))
s = grefine p
yRep = refinedTypeDef s

data Y = Y Foo Bar
instance Generic Y where
    type Rep Y = (:*:) ((:+:) U1 ((:+:) U1 U1)) ((:+:) U1 U1) -- taken from yRep
    from (Y x y) = stripFoo (from x) :*: stripBar (from y)
    to (fooRep :*: barRep) = Y (to (unStripFoo fooRep)) (to (unStripBar barRep))

include :: Y -> Maybe (X Foo Bar)
include = runRefinement s.toDyn.(from :: Y -> Rep Y ())

-- currently, refinements forget meta-data, 
-- whence we have to strip and un-strip it in the conversion.
stripFoo :: Rep Foo p -> (U1 :+: (U1 :+: U1)) p
stripFoo = c . unM1 where
    c (L1 (M1 u)) = L1 u
    c (R1 (L1 (M1 u))) = R1 (L1 u)
    c (R1 (R1 (M1 u))) = R1 (R1 u)


stripBar :: Rep Bar p -> (U1 :+: U1) p
stripBar = c . unM1 where
    c (L1 (M1 u)) = L1 u
    c (R1 (M1 u)) = R1 u
    

unStripFoo :: (U1 :+: (U1 :+: U1)) p -> Rep Foo p
unStripFoo = M1 . c where
    c (L1 u) = L1 (M1 u)
    c (R1 (L1 u)) = R1 (L1 (M1 u))
    c (R1 (R1 u)) = R1 (R1 (M1 u))

unStripBar :: (U1 :+: U1) p -> Rep Bar p
unStripBar = M1 . c where
    c (L1 u) = L1 (M1 u)
    c (R1 u) = R1 (M1 u)